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

Merge branch 'develop'

parents bfc69eae 135c1fd4
No related branches found
No related tags found
No related merge requests found
Pipeline #112166 passed
Stage: test
Show whitespace changes
Inline Side-by-side
Showing
with 1614 additions and 1605 deletions
src/test/java/de/tlc4b/prettyprint/FunctionTest.java
+ 115
− 115
View file @ db198d68
src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+ 409
− 404
View file @ db198d68
......@@ -67,7 +67,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
......@@ -84,7 +84,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
+ "Invariant1 == x = 1\n"
+ "Invariant2 == y = 1\n"
+ "Init == x \\in {1} /\\ y \\in {1} \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x, y>>\n"
+ "====";
......@@ -103,7 +104,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
+ "Invariant1 == x = 1\n"
+ "Invariant2 == y = 1\n"
+ "Init == x \\in {1} /\\ y \\in {1}\n"
+ "foo == x' \\in {1} /\\ y' \\in {1}\n"
+ "Next == foo\n"
......@@ -124,7 +126,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
+ "Invariant1 == x = 1\n"
+ "Invariant2 == y = 1\n"
+ "Init == x \\in {1} /\\ y \\in {1} \n"
+ "foo == x' \\in {x + 1} /\\ UNCHANGED <<y>>\n"
+ "Next == foo\n"
......@@ -144,7 +147,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(p) == x' = p\n"
+ "Next == \\E p \\in {1} : foo(p)\n"
......@@ -164,7 +167,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == \\E p \\in {1} : x' = p\n"
+ "Next == foo\n"
......@@ -185,7 +188,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(p) == \\E p2 \\in {1} : x' = p + p2\n"
+ "Next == \\E p \\in {1} : foo(p)\n"
......@@ -205,7 +208,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == UNCHANGED <<x>>\n"
+ "Next == foo\n"
......@@ -225,7 +228,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == 1 = 1 /\\ UNCHANGED <<x>>\n"
+ "Next == foo\n"
......@@ -247,7 +250,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == x = 1 /\\ x' = x + 1\n"
+ "Next == foo \n"
......@@ -268,7 +271,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(a) == x' = a\n"
+ "Next == \\E a \\in {1}: foo(a) \n"
......@@ -288,7 +291,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x \\in {1} \n"
+ "foo == x' \\in {2} \n"
+ "Next == foo\n"
......@@ -308,7 +311,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == (IF 1 = 1 THEN x' = 1 ELSE UNCHANGED <<x>>)\n"
+ "Next == foo \n"
......@@ -329,7 +332,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == (( ((x = 1) /\\ (x' = 1)) \\/ (x = 2 /\\ x' = 2)))\n"
+ "Next == foo \n"
......@@ -351,7 +354,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x,y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
+ "Invariant1 == x = 1\n"
+ "Invariant2 == y = 1\n"
+ "Init == x = 1 /\\ y = 1\n"
+ "foo == (( ((x = 1) /\\ (x' = 1)) \\/ (x = 2 /\\ UNCHANGED <<x>>)) /\\ UNCHANGED <<y>>)\n"
+ "Next == foo \n"
......@@ -371,7 +375,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
+ "Invariant1 == x = 1\n"
+ "Invariant2 == y = 1\n"
+ "Init == x = 1 /\\ y = 1\n"
+ "foo == x = 1 \n"
+ "/\\ (((x = 1 /\\ x' = 1) \\/ (x = 2 /\\ UNCHANGED <<x>>)) /\\ y' = 1)\n"
......@@ -393,7 +398,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == TRUE /\\ UNCHANGED <<x>>\n"
+ "Next == foo \n"
......
src/test/java/de/tlc4b/prettyprint/RelationTest.java
+ 40
− 40
View file @ db198d68
src/test/java/de/tlc4b/prettyprint/SetTest.java
+ 207
− 208
View file @ db198d68
......@@ -201,7 +201,6 @@ public class SetTest {
+ "EXTENDS BBuiltIns\n"
+ "ASSUME Inter({{z}: z \\in {z \\in ({1, 2}): 1 = 1}}) = {}\n"
+ "====";
System.out.println(expected);
compareEquals(expected, machine);
}
......
src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
+ 50
− 50
View file @ db198d68
src/test/java/de/tlc4b/prettyprint/StringTest.java
+ 31
− 31
View file @ db198d68
src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
+ 3
− 3
View file @ db198d68
......@@ -54,7 +54,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == \\E a \\in {1}, b \\in {2} : x = a + b \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
......@@ -107,7 +107,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x \\in {1}\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
......@@ -125,7 +125,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == (CASE 1 = 1 -> x = 1 [] 1 = 2 -> x = 2 [] OTHER -> x = 4)\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
......
src/test/java/de/tlc4b/tlc/integration/ErrorTest.java
+ 92
− 92
View file @ db198d68
src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
+ 9
− 9
View file @ db198d68
package de.tlc4b.tlc.integration.probprivate;
import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.tlc4b.tlc.TLCResults.TLCResult;
import de.tlc4b.util.AbstractParseMachineTest;
import de.tlc4b.util.PolySuite;
import de.tlc4b.util.TestPair;
import de.tlc4b.util.PolySuite.Config;
import de.tlc4b.util.PolySuite.Configuration;
import de.tlc4b.util.TestPair;
import org.junit.Test;
import org.junit.runner.RunWith;
import static de.tlc4b.tlc.TLCResults.TLCResult.AssertionError;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
@RunWith(PolySuite.class)
public class AssertionErrorTest extends AbstractParseMachineTest {
......@@ -37,7 +37,7 @@ public class AssertionErrorTest extends AbstractParseMachineTest {
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(AssertionError, "public_examples/TLC/AssertionError"));
list.add(new TestPair(AssertionError, "build/prob_examples/public_examples/TLC/AssertionError"));
return getConfiguration(list);
}
}
src/test/java/de/tlc4b/coverage/CoverageTest.java → src/test/java/de/tlc4b/tlc/integration/probprivate/CoverageTest.java
+ 13
− 5
View file @ db198d68
package de.tlc4b.coverage;
package de.tlc4b.tlc.integration.probprivate;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.tlc4b.TLC4B;
import de.tlc4b.tlc.TLCResults.TLCResult;
import de.tlc4b.util.AbstractParseMachineTest;
......@@ -13,6 +10,11 @@ import de.tlc4b.util.PolySuite;
import de.tlc4b.util.PolySuite.Config;
import de.tlc4b.util.PolySuite.Configuration;
import org.junit.Test;
import org.junit.runner.RunWith;
import tlc2.TLCGlobals;
@RunWith(PolySuite.class)
public class CoverageTest extends AbstractParseMachineTest {
......@@ -24,6 +26,12 @@ public class CoverageTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
// The subdirectories of the states directory are named after the time when TLC was started.
// Old versions of TLC (like the one we use) format the time with second precision only,
// leading to name conflicts when two tests are started within the same second.
// This line works around the issue by instead using a millisecond timestamp as the name.
TLCGlobals.metaDir = TLCGlobals.metaRoot + File.separator + System.currentTimeMillis() + File.separator;
String[] a = new String[] { machine.getPath(), "-notlc" };
TLC4B.test(a, true);
}
......@@ -32,7 +40,7 @@ public class CoverageTest extends AbstractParseMachineTest {
public static Configuration getConfig() {
final ArrayList<String> list = new ArrayList<String>();
final ArrayList<String> ignoreList = new ArrayList<String>();
list.add("public_examples/TLC/");
list.add("build/prob_examples/public_examples/TLC/");
list.add("./src/test/resources/");
ignoreList.add("./src/test/resources/compound/");
......
src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
+ 1
− 1
View file @ db198d68
......@@ -38,7 +38,7 @@ public class DeadlockTest extends AbstractParseMachineTest {
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(Deadlock,
"public_examples/TLC/Deadlock"));
"build/prob_examples/public_examples/TLC/Deadlock"));
return getConfiguration(list);
}
}
src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
+ 1
− 1
View file @ db198d68
......@@ -38,7 +38,7 @@ public class GoalTest extends AbstractParseMachineTest {
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(Goal,
"public_examples/TLC/GOAL"));
"build/prob_examples/public_examples/TLC/GOAL"));
return getConfiguration(list);
}
}
src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
+ 1
− 1
View file @ db198d68
......@@ -38,7 +38,7 @@ public class InvariantViolationTest extends AbstractParseMachineTest {
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(InvariantViolation,
"public_examples/TLC/InvariantViolation"));
"build/prob_examples/public_examples/TLC/InvariantViolation"));
return getConfiguration(list);
}
}
src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
+ 83
− 86
View file @ db198d68
package de.tlc4b.tlc.integration.probprivate;
import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import de.tlc4b.TLC4BGlobals;
import org.junit.Test;
import de.tlc4b.TLC4BGlobals;
import static de.tlc4b.tlc.TLCResults.TLCResult.Goal;
import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
public class LawsTest {
@Test
public void BoolLaws() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws.mch"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/BoolLaws.mch"};
assertEquals(NoError, test(a));
}
@Test
public void BoolWithArithLaws() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"};
assertEquals(NoError, test(a));
}
@Test
public void FunLaws() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/FunLaws.mch"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/FunLaws.mch"};
assertEquals(NoError, test(a));
}
@Test
public void FunLawsWithLambda() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/FunLawsWithLambda.mch"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/FunLawsWithLambda.mch"};
assertEquals(NoError, test(a));
}
@Test
public void RelLaws_TLC() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/RelLaws_TLC.mch"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/RelLaws_TLC.mch"};
assertEquals(Goal, test(a));
}
@Test
public void BoolLaws_SetCompr() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws_SetCompr.mch"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/BoolLaws_SetCompr.mch"};
assertEquals(NoError, test(a));
}
@Test
public void BoolLaws_SetComprCLPFD() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"};
assertEquals(NoError, test(a));
}
@Test
public void CardinalityLaws_TLC() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
assertEquals(NoError, test(a));
}
@Test
public void EqualityLaws() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
assertEquals(NoError, test(a));
}
@Test
public void SubsetLaws() throws Exception {
TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
assertEquals(NoError, test(a));
}
}
src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
+ 1
− 1
View file @ db198d68
......@@ -38,7 +38,7 @@ public class NoErrorTest extends AbstractParseMachineTest {
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(NoError,
"public_examples/TLC/NoError"));
"build/prob_examples/public_examples/TLC/NoError"));
return getConfiguration(list);
}
......
src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
+ 9
− 9
View file @ db198d68
package de.tlc4b.tlc.integration.probprivate;
import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.tlc4b.tlc.TLCResults.TLCResult;
import de.tlc4b.util.AbstractParseMachineTest;
import de.tlc4b.util.PolySuite;
import de.tlc4b.util.TestPair;
import de.tlc4b.util.PolySuite.Config;
import de.tlc4b.util.PolySuite.Configuration;
import de.tlc4b.util.TestPair;
import org.junit.Test;
import org.junit.runner.RunWith;
import static de.tlc4b.tlc.TLCResults.TLCResult.WellDefinednessError;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
@RunWith(PolySuite.class)
public class WellDefinednessTest extends AbstractParseMachineTest {
......@@ -37,7 +37,7 @@ public class WellDefinednessTest extends AbstractParseMachineTest {
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(WellDefinednessError, "public_examples/TLC/WellDefinednessError"));
list.add(new TestPair(WellDefinednessError, "build/prob_examples/public_examples/TLC/WellDefinednessError"));
return getConfiguration(list);
}
}
src/test/java/de/tlc4b/typechecking/BooleansTest.java
+ 75
− 75
View file @ db198d68
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment