From 1519ab96162de87eb1b0d2ae12d1be7d536b4b95 Mon Sep 17 00:00:00 2001 From: hansen <dominik_hansen@web.de> Date: Wed, 31 Jul 2013 13:40:37 +0200 Subject: [PATCH] Fixed a Bug finding an Assertion Error --- build.gradle | 2 +- src/main/java/de/b2tla/TLCRunner.java | 1 - .../java/de/b2tla/prettyprint/TLAPrinter.java | 4 ++ src/main/java/de/b2tla/tla/Generator.java | 17 +++---- src/main/java/de/b2tla/tlc/TLCOutput.java | 22 +++++---- .../de/b2tla/tlc/integration/ErrorTest.java | 25 ++++++++--- .../tlc/integration/SingleConfigurations.java | 21 --------- .../AssertionErrorTest.java} | 31 +++++-------- .../integration/probprivate/DeadlockTest.java | 44 ++++++++++++++++++ .../tlc/integration/probprivate/GoalTest.java | 43 ++++++++++++++++++ .../probprivate/InvariantViolationTest.java | 44 ++++++++++++++++++ .../{ => probprivate}/LawsTest.java | 2 +- .../integration/probprivate/NoErrorTest.java | 45 +++++++++++++++++++ .../probprivate/WellDefinednessTest.java | 45 +++++++++++++++++++ src/test/resources/errors/AssertionError.mch | 8 ++++ src/test/resources/errors/AssertionError2.mch | 8 ++++ 16 files changed, 297 insertions(+), 65 deletions(-) delete mode 100644 src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java rename src/test/java/de/b2tla/tlc/integration/{ProBPrivateTests.java => probprivate/AssertionErrorTest.java} (52%) create mode 100644 src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java create mode 100644 src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java create mode 100644 src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java rename src/test/java/de/b2tla/tlc/integration/{ => probprivate}/LawsTest.java (95%) create mode 100644 src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java create mode 100644 src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java create mode 100644 src/test/resources/errors/AssertionError.mch create mode 100644 src/test/resources/errors/AssertionError2.mch diff --git a/build.gradle b/build.gradle index e923aec..0425b65 100644 --- a/build.gradle +++ b/build.gradle @@ -42,7 +42,7 @@ test { task integrationtests(type: Test){ doFirst{ println("Running integration tests") } scanForTestClasses = true - include('de/b2tla/tlc/integration/**') + include('de/b2tla/tlc/integration/probprivate/**') } jar { from sourceSets.main.allJava } diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java index 7d54661..44e3b38 100644 --- a/src/main/java/de/b2tla/TLCRunner.java +++ b/src/main/java/de/b2tla/TLCRunner.java @@ -82,7 +82,6 @@ public class TLCRunner { } catch (InterruptedException e) { e.printStackTrace(); } - return stdOut.getLog(); } diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java index 5650143..be5c79b 100644 --- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java +++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java @@ -23,6 +23,7 @@ import de.b2tla.btypes.FunctionType; import de.b2tla.btypes.IntegerType; import de.b2tla.btypes.PairType; import de.b2tla.btypes.SetType; +import de.b2tla.btypes.UntypedType; import de.b2tla.ltl.LTLFormulaVisitor; import de.b2tla.tla.ConfigFile; import de.b2tla.tla.TLADefinition; @@ -1590,6 +1591,9 @@ public class TLAPrinter extends DepthFirstAdapter { @Override public void caseATotalFunctionExpression(ATotalFunctionExpression node) { BType type = this.typechecker.getType(node); + if(type == null){ + type = new SetType(new FunctionType(new UntypedType(), new UntypedType())); + } BType subtype = ((SetType) type).getSubtype(); if (subtype instanceof FunctionType) { tlaModuleString.append("["); diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java index 1b9a912..083dfc9 100644 --- a/src/main/java/de/b2tla/tla/Generator.java +++ b/src/main/java/de/b2tla/tla/Generator.java @@ -260,18 +260,19 @@ public class Generator extends DepthFirstAdapter { init = true; this.tlaModule.variables.add(con); BType type = typechecker.getType(con); - AMemberPredicate member = new AMemberPredicate( - (PExpression) con.clone(), - type.createSyntaxTreeNode()); - ArrayList<NodeType> list = this.typeRestrictor.getRestrictedTypesSet(con); + PExpression n = type.createSyntaxTreeNode(); + AMemberPredicate member = new AMemberPredicate( + (PExpression) con.clone(), n); + + ArrayList<NodeType> list = this.typeRestrictor + .getRestrictedTypesSet(con); if (list == null || list.size() == 0) { - System.out.println(con); tlaModule.addInit(member); - }else{ - + } else { + } - + } else { tlaModule.definitions.add(new TLADefinition(con, value)); } diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java index 3040ef5..9279f9b 100644 --- a/src/main/java/de/b2tla/tlc/TLCOutput.java +++ b/src/main/java/de/b2tla/tlc/TLCOutput.java @@ -22,8 +22,7 @@ public class TLCOutput { String parseError; public static enum TLCResult { - Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, - PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError + Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError } public long getRunningTime() { @@ -143,8 +142,11 @@ public class TLCOutput { public static TLCResult findError(ArrayList<String> list) { for (int i = 0; i < list.size(); i++) { String m = list.get(i); - if (m.startsWith("Error:") || m.startsWith("\"Error:")) { - return findError(m); + if (m.startsWith("Error:") || m.startsWith("\"Error:") + || m.startsWith("The exception was a")) { + TLCResult res = findError(m); + if (res != null) + return findError(m); } } return TLCResult.NoError; @@ -163,19 +165,23 @@ public class TLCOutput { } else if (invName.startsWith("Assertion")) { return TLCResult.AssertionError; } + } else if (m.contains("The invariant of Assertion")) { + return TLCResult.AssertionError; } else if (res[1].equals("Assumption")) { return TLCResult.PropertiesError; } else if (res[1].equals("Temporal")) { return TLCResult.TemporalProperty; } else if (m.equals("Error: TLC threw an unexpected exception.")) { - return TLCResult.TLCError; - } else if (m.startsWith("\"Error: Invalid function call to relation")){ + return null; + } else if (m.startsWith("\"Error: Invalid function call to relation")) { return TLCResult.WellDefinednessError; } else if (m.startsWith("Error: The behavior up to")) { return null; - } else if (m.startsWith("Error: The following behavior constitutes a counter-example:")) { + } else if (m + .startsWith("Error: The following behavior constitutes a counter-example:")) { return null; - }else if (m.startsWith("Error: The error occurred when TLC was evaluating the nested")) { + } else if (m + .startsWith("Error: The error occurred when TLC was evaluating the nested")) { return null; } return TLCResult.TLCError; diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java index 2efca12..dad6dd5 100644 --- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java +++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java @@ -1,5 +1,6 @@ package de.b2tla.tlc.integration; +import static de.b2tla.tlc.TLCOutput.TLCResult.*; import static org.junit.Assert.assertEquals; import org.junit.BeforeClass; @@ -7,7 +8,6 @@ import org.junit.Test; import de.b2tla.B2TLA; import de.b2tla.B2TLAGlobals; -import de.b2tla.tlc.TLCOutput; public class ErrorTest { @@ -19,19 +19,19 @@ public class ErrorTest { @Test public void testInvariantError() throws Exception { String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch" }; - assertEquals(TLCOutput.TLCResult.InvariantViolation, B2TLA.test(a,true)); + assertEquals(InvariantViolation, B2TLA.test(a,true)); } @Test public void testDeadlock() throws Exception { String[] a = new String[] { "./src/test/resources/errors/Deadlock.mch" }; - assertEquals(TLCOutput.TLCResult.Deadlock, B2TLA.test(a,true)); + assertEquals(Deadlock, B2TLA.test(a,true)); } @Test public void testPropertiesError() throws Exception { String[] a = new String[] { "./src/test/resources/errors/PropertiesError.mch" }; - assertEquals(TLCOutput.TLCResult.PropertiesError, B2TLA.test(a,true)); + assertEquals(PropertiesError, B2TLA.test(a,true)); } @Test @@ -43,13 +43,26 @@ public class ErrorTest { @Test public void testNoError() throws Exception { String[] a = new String[] { "./src/test/resources/errors/NoError.mch" }; - assertEquals(TLCOutput.TLCResult.NoError, B2TLA.test(a,true)); + assertEquals(NoError, B2TLA.test(a,true)); } @Test public void testEnumerationError() throws Exception { String[] a = new String[] { "./src/test/resources/errors/EnumerationError.mch" }; - assertEquals(TLCOutput.TLCResult.TLCError, B2TLA.test(a,true)); + assertEquals(TLCError, B2TLA.test(a,true)); + } + + @Test + public void testAssertionError() throws Exception { + String[] a = new String[] { "./src/test/resources/errors/AssertionError.mch" }; + assertEquals(AssertionError, B2TLA.test(a,true)); + } + + + @Test + public void testConstantAssertionError() throws Exception { + String[] a = new String[] { "./src/test/resources/errors/AssertionError2.mch" }; + assertEquals(AssertionError, B2TLA.test(a,true)); } } diff --git a/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java b/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java deleted file mode 100644 index b12cd7a..0000000 --- a/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java +++ /dev/null @@ -1,21 +0,0 @@ -package de.b2tla.tlc.integration; - -import static de.b2tla.tlc.TLCOutput.TLCResult.NoError; -import static org.junit.Assert.assertEquals; - -import org.junit.Test; - -import de.b2tla.B2TLA; -import de.b2tla.B2TLAGlobals; - -public class SingleConfigurations { - - -// @Test -// public void TautologiesPl() throws Exception { -// B2TLAGlobals.setDeleteOnExit(true); -// String[] a = new String[] { "../probprivate/public_examples/TLC/others/TautologiesPL.mch", "-nodead"}; -// assertEquals(NoError, B2TLA.test(a)); -// } - -} \ No newline at end of file diff --git a/src/test/java/de/b2tla/tlc/integration/ProBPrivateTests.java b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java similarity index 52% rename from src/test/java/de/b2tla/tlc/integration/ProBPrivateTests.java rename to src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java index d7357ea..ae6a348 100644 --- a/src/test/java/de/b2tla/tlc/integration/ProBPrivateTests.java +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java @@ -1,7 +1,7 @@ -package de.b2tla.tlc.integration; +package de.b2tla.tlc.integration.probprivate; -import static org.junit.Assert.*; -import static de.b2tla.tlc.TLCOutput.TLCResult.*; +import static de.b2tla.tlc.TLCOutput.TLCResult.AssertionError; +import static org.junit.Assert.assertEquals; import java.io.File; import java.util.ArrayList; @@ -9,42 +9,35 @@ import java.util.ArrayList; import org.junit.Test; import org.junit.runner.RunWith; +import de.b2tla.B2TLA; import de.b2tla.tlc.TLCOutput.TLCResult; -import de.b2tla.util.*; +import de.b2tla.util.AbstractParseMachineTest; +import de.b2tla.util.PolySuite; +import de.b2tla.util.TestPair; import de.b2tla.util.PolySuite.Config; import de.b2tla.util.PolySuite.Configuration; -import de.b2tla.B2TLA; -import de.b2tla.B2TLAGlobals; - @RunWith(PolySuite.class) -public class ProBPrivateTests extends AbstractParseMachineTest { +public class AssertionErrorTest extends AbstractParseMachineTest { private final File machine; private final TLCResult error; - - public ProBPrivateTests(File machine, TLCResult result) { + + public AssertionErrorTest(File machine, TLCResult result) { this.machine = machine; this.error = result; } - + @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, B2TLA.test(a,true)); + assertEquals(error, B2TLA.test(a, false)); } @Config public static Configuration getConfig() { final ArrayList<TestPair> list = new ArrayList<TestPair>(); - list.add(new TestPair(InvariantViolation, "../probprivate/public_examples/TLC/InvariantViolation")); - list.add(new TestPair(Deadlock, "../probprivate/public_examples/TLC/Deadlock")); - list.add(new TestPair(Goal, "../probprivate/public_examples/TLC/GOAL")); - list.add(new TestPair(NoError, "../probprivate/public_examples/TLC/NoError")); list.add(new TestPair(AssertionError, "../probprivate/public_examples/TLC/AssertionError")); return getConfiguration(list); } - - } - diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java new file mode 100644 index 0000000..c2ceea8 --- /dev/null +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java @@ -0,0 +1,44 @@ +package de.b2tla.tlc.integration.probprivate; + +import static de.b2tla.tlc.TLCOutput.TLCResult.Deadlock; +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.b2tla.B2TLA; +import de.b2tla.tlc.TLCOutput.TLCResult; +import de.b2tla.util.AbstractParseMachineTest; +import de.b2tla.util.PolySuite; +import de.b2tla.util.TestPair; +import de.b2tla.util.PolySuite.Config; +import de.b2tla.util.PolySuite.Configuration; + +@RunWith(PolySuite.class) +public class DeadlockTest extends AbstractParseMachineTest { + + private final File machine; + private final TLCResult error; + + public DeadlockTest(File machine, TLCResult result) { + this.machine = machine; + this.error = result; + } + + @Test + public void testRunTLC() throws Exception { + String[] a = new String[] { machine.getPath() }; + assertEquals(error, B2TLA.test(a, true)); + } + + @Config + public static Configuration getConfig() { + final ArrayList<TestPair> list = new ArrayList<TestPair>(); + list.add(new TestPair(Deadlock, + "../probprivate/public_examples/TLC/Deadlock")); + return getConfiguration(list); + } +} diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java new file mode 100644 index 0000000..0eee8c4 --- /dev/null +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java @@ -0,0 +1,43 @@ +package de.b2tla.tlc.integration.probprivate; + +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.b2tla.B2TLA; +import de.b2tla.tlc.TLCOutput.TLCResult; +import de.b2tla.util.AbstractParseMachineTest; +import de.b2tla.util.PolySuite; +import de.b2tla.util.TestPair; +import de.b2tla.util.PolySuite.Config; +import de.b2tla.util.PolySuite.Configuration; + +@RunWith(PolySuite.class) +public class GoalTest extends AbstractParseMachineTest{ + + + private final File machine; + private final TLCResult error; + + public GoalTest(File machine, TLCResult result) { + this.machine = machine; + this.error = result; + } + + @Test + public void testRunTLC() throws Exception { + String[] a = new String[] { machine.getPath()}; + assertEquals(error, B2TLA.test(a,false)); + } + + @Config + public static Configuration getConfig() { + final ArrayList<TestPair> list = new ArrayList<TestPair>(); + list.add(new TestPair(TLCResult.Goal, "../probprivate/public_examples/TLC/GOAL")); + return getConfiguration(list); + } +} diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java new file mode 100644 index 0000000..47d280b --- /dev/null +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java @@ -0,0 +1,44 @@ +package de.b2tla.tlc.integration.probprivate; + +import static de.b2tla.tlc.TLCOutput.TLCResult.InvariantViolation; +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.b2tla.B2TLA; +import de.b2tla.tlc.TLCOutput.TLCResult; +import de.b2tla.util.AbstractParseMachineTest; +import de.b2tla.util.PolySuite; +import de.b2tla.util.TestPair; +import de.b2tla.util.PolySuite.Config; +import de.b2tla.util.PolySuite.Configuration; + +@RunWith(PolySuite.class) +public class InvariantViolationTest extends AbstractParseMachineTest { + + private final File machine; + private final TLCResult error; + + public InvariantViolationTest(File machine, TLCResult result) { + this.machine = machine; + this.error = result; + } + + @Test + public void testRunTLC() throws Exception { + String[] a = new String[] { machine.getPath() }; + assertEquals(error, B2TLA.test(a, true)); + } + + @Config + public static Configuration getConfig() { + final ArrayList<TestPair> list = new ArrayList<TestPair>(); + list.add(new TestPair(InvariantViolation, + "../probprivate/public_examples/TLC/InvariantViolation")); + return getConfiguration(list); + } +} diff --git a/src/test/java/de/b2tla/tlc/integration/LawsTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java similarity index 95% rename from src/test/java/de/b2tla/tlc/integration/LawsTest.java rename to src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java index ae97078..d5d0ef0 100644 --- a/src/test/java/de/b2tla/tlc/integration/LawsTest.java +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java @@ -1,4 +1,4 @@ -package de.b2tla.tlc.integration; +package de.b2tla.tlc.integration.probprivate; import static de.b2tla.tlc.TLCOutput.TLCResult.*; import static org.junit.Assert.assertEquals; diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java new file mode 100644 index 0000000..39a75a2 --- /dev/null +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java @@ -0,0 +1,45 @@ +package de.b2tla.tlc.integration.probprivate; + +import static de.b2tla.tlc.TLCOutput.TLCResult.NoError; +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.b2tla.B2TLA; +import de.b2tla.tlc.TLCOutput.TLCResult; +import de.b2tla.util.AbstractParseMachineTest; +import de.b2tla.util.PolySuite; +import de.b2tla.util.TestPair; +import de.b2tla.util.PolySuite.Config; +import de.b2tla.util.PolySuite.Configuration; + +@RunWith(PolySuite.class) +public class NoErrorTest extends AbstractParseMachineTest { + + private final File machine; + private final TLCResult error; + + public NoErrorTest(File machine, TLCResult result) { + this.machine = machine; + this.error = result; + } + + @Test + public void testRunTLC() throws Exception { + String[] a = new String[] { machine.getPath() }; + assertEquals(error, B2TLA.test(a, true)); + } + + @Config + public static Configuration getConfig() { + final ArrayList<TestPair> list = new ArrayList<TestPair>(); + list.add(new TestPair(NoError, + "../probprivate/public_examples/TLC/NoError")); + return getConfiguration(list); + } + +} diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java new file mode 100644 index 0000000..36bd581 --- /dev/null +++ b/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java @@ -0,0 +1,45 @@ +package de.b2tla.tlc.integration.probprivate; + +import static de.b2tla.tlc.TLCOutput.TLCResult.WellDefinednessError; +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.b2tla.B2TLA; +import de.b2tla.tlc.TLCOutput.TLCResult; +import de.b2tla.util.AbstractParseMachineTest; +import de.b2tla.util.PolySuite; +import de.b2tla.util.TestPair; +import de.b2tla.util.PolySuite.Config; +import de.b2tla.util.PolySuite.Configuration; + +@RunWith(PolySuite.class) +public class WellDefinednessTest extends AbstractParseMachineTest { + + + + private final File machine; + private final TLCResult error; + + public WellDefinednessTest(File machine, TLCResult result) { + this.machine = machine; + this.error = result; + } + + @Test + public void testRunTLC() throws Exception { + String[] a = new String[] { machine.getPath() }; + assertEquals(error, B2TLA.test(a,true)); + } + + @Config + public static Configuration getConfig() { + final ArrayList<TestPair> list = new ArrayList<TestPair>(); + list.add(new TestPair(WellDefinednessError, "../probprivate/public_examples/TLC/WellDefinednessError")); + return getConfiguration(list); + } +} diff --git a/src/test/resources/errors/AssertionError.mch b/src/test/resources/errors/AssertionError.mch new file mode 100644 index 0000000..77ea74e --- /dev/null +++ b/src/test/resources/errors/AssertionError.mch @@ -0,0 +1,8 @@ +MACHINE AssertionError +ASSERTIONS x = 1 +VARIABLES x +INVARIANT x : 1..2 +INITIALISATION x := 1 +OPERATIONS +foo = PRE x = 1 THEN x:= 2 END +END \ No newline at end of file diff --git a/src/test/resources/errors/AssertionError2.mch b/src/test/resources/errors/AssertionError2.mch new file mode 100644 index 0000000..de88790 --- /dev/null +++ b/src/test/resources/errors/AssertionError2.mch @@ -0,0 +1,8 @@ +MACHINE AssertionError +ASSERTIONS 2 = 1 +VARIABLES x +INVARIANT x : 1..2 +INITIALISATION x := 1 +OPERATIONS +foo = PRE x = 1 THEN x:= 2 END +END \ No newline at end of file -- GitLab