Skip to content
Snippets Groups Projects
Commit 0c493167 authored by dgelessus's avatar dgelessus
Browse files

Fix indents

parent 42234266
No related branches found
No related tags found
No related merge requests found
Pipeline #157628 passed
......@@ -275,15 +275,15 @@ public class TypeRestrictionsTest {
+ "OPERATIONS\n"
+ "foo = ANY y WHERE y=1 THEN x:=y END\n"
+ "END";
String expected = "---- MODULE test ----\n" +
"VARIABLES x\n" +
"Invariant1 == x = 1\n" +
"Init == x = 1\n" +
"\n" +
"foo == \\E y \\in {1} : x' = y\n" +
"\n" +
"Next == \\/ foo\n" +
"====";
String expected = "---- MODULE test ----\n"
+ "VARIABLES x\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1\n"
+ "\n"
+ "foo == \\E y \\in {1} : x' = y\n"
+ "\n"
+ "Next == \\/ foo\n"
+ "====";
compare(expected, machine);
}
......@@ -296,15 +296,15 @@ public class TypeRestrictionsTest {
+ "OPERATIONS\n"
+ "foo = ANY y WHERE y:{1} THEN x:=y END\n"
+ "END";
String expected = "---- MODULE test ----\n" +
"VARIABLES x\n" +
"Invariant1 == x = 1\n" +
"Init == x = 1\n" +
"\n" +
"foo == \\E y \\in {1} : x' = y\n" +
"\n" +
"Next == \\/ foo\n" +
"====";
String expected = "---- MODULE test ----\n"
+ "VARIABLES x\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1\n"
+ "\n"
+ "foo == \\E y \\in {1} : x' = y\n"
+ "\n"
+ "Next == \\/ foo\n"
+ "====";
compare(expected, machine);
}
......@@ -320,15 +320,15 @@ public class TypeRestrictionsTest {
+ "OPERATIONS\n"
+ "foo = ANY y WHERE IF B=TRUE THEN y=1 ELSE y=1 END THEN x:=y END\n"
+ "END";
String expected = "---- MODULE test ----\n" +
"VARIABLES x\n" +
"Invariant1 == x = 1\n" +
"Init == x = 1\n" +
"\n" +
"foo == \\E y \\in {1} : x' = y\n" +
"\n" +
"Next == \\/ foo\n" +
"====";
String expected = "---- MODULE test ----\n"
+ "VARIABLES x\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1\n"
+ "\n"
+ "foo == \\E y \\in {1} : x' = y\n"
+ "\n"
+ "Next == \\/ foo\n"
+ "====";
compare(expected, machine);
}
}
......@@ -20,34 +20,34 @@ public class FixedBugsTest {
@Test
public void testFunctionAssignment() throws Exception {
String machine = "MACHINE Test\n" +
"VARIABLES x\n" +
"INVARIANT x : 1..3 +-> 1..3\n" +
"INITIALISATION x := {}\n" +
"OPERATIONS foo = SELECT x = {} THEN x(1) := 1 END\n" +
"END";
String machine = "MACHINE Test\n"
+ "VARIABLES x\n"
+ "INVARIANT x : 1..3 +-> 1..3\n"
+ "INITIALISATION x := {}\n"
+ "OPERATIONS foo = SELECT x = {} THEN x(1) := 1 END\n"
+ "END";
assertEquals(Deadlock, testString(machine));
}
@Test
public void testNestedFunctionAssignment2() throws Exception {
String machine = "MACHINE Test\n" +
"VARIABLES x\n" +
"INVARIANT x : 1..3 +-> (1..3 +-> 1..3)\n" +
"INITIALISATION x := {}\n" +
"OPERATIONS foo = SELECT x = {} THEN x(1)(2) := 1 END\n" +
"END";
String machine = "MACHINE Test\n"
+ "VARIABLES x\n"
+ "INVARIANT x : 1..3 +-> (1..3 +-> 1..3)\n"
+ "INITIALISATION x := {}\n"
+ "OPERATIONS foo = SELECT x = {} THEN x(1)(2) := 1 END\n"
+ "END";
assertEquals(Deadlock, testString(machine));
}
@Test
public void testNestedFunctionAssignment3() throws Exception {
String machine = "MACHINE Test\n" +
"VARIABLES x\n" +
"INVARIANT x : 1..3 +-> (1..3 +-> (1..3 +-> 1..3))\n" +
"INITIALISATION x := {}\n" +
"OPERATIONS foo = SELECT x = {} THEN x(1)(2)(3) := 1 END\n" +
"END";
String machine = "MACHINE Test\n"
+ "VARIABLES x\n"
+ "INVARIANT x : 1..3 +-> (1..3 +-> (1..3 +-> 1..3))\n"
+ "INITIALISATION x := {}\n"
+ "OPERATIONS foo = SELECT x = {} THEN x(1)(2)(3) := 1 END\n"
+ "END";
assertEquals(Deadlock, testString(machine));
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment