diff --git a/TODO.txt b/TODO.txt new file mode 100644 index 0000000000000000000000000000000000000000..6197e62b54153e6e497c07f49a31db5112eb457d --- /dev/null +++ b/TODO.txt @@ -0,0 +1,5 @@ +Validation of generated trace files: Parsing the trace files + +Missing constructs: + - SEES, INCLUDES, REFINES, IMPORTS + - sequential composition, while loop \ No newline at end of file diff --git a/build.gradle b/build.gradle index d966d9da75c54980dae2627206e4d901e1c89d9b..8daec41bd59d2fac6db4bb61cc17e54c4350ed12 100644 --- a/build.gradle +++ b/build.gradle @@ -20,7 +20,7 @@ configurations { // configuration that holds jars to copy into lib releaseJars } -def parser_version = '2.4.22-SNAPSHOT' +def parser_version = '2.4.28-SNAPSHOT' dependencies { //compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6') diff --git a/build.xml b/build.xml index 47a9188af65a2cbe6f315938c584579e5c617041..52dcde683431ffdb4ae244df5e3462d21624e571 100644 --- a/build.xml +++ b/build.xml @@ -1,5 +1,6 @@ <project default="copy"> <target name="copy"> <copy file="build/tlc4b/TLC4B.jar" tofile="../../Desktop/ProB/lib/TLC4B.jar"/> + <copy file="build/tlc4b/TLC4B.jar" tofile="/Users/hansen/git/prob_prolog/lib/TLC4B.jar"/> </target> </project> \ No newline at end of file diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java index caabfa87be2ede1460e6f724ece6795ebbaf8a0e..5033f9bf9ac0ae1ed8e368461626e60dad844e60 100644 --- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java +++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java @@ -69,6 +69,10 @@ public class PrecedenceCollector extends DepthFirstAdapter { put("AConcatExpression", 13, 13, true); put("ADivExpression", 13, 13, false); + + put("AFunctionExpression", 20, 20, false); + + } private Precedence getPrecedence(Node node) { diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index c8595a335e210ca306e0fb9d24c16b7bff5b208a..589cf83c0837a13d9e9f54a4794000c96a85aef2 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -1367,8 +1367,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'"); } - setType(node.getExpression(), new SetType(new UntypedType())); + + setType(node.getExpression(), new UntypedType()); node.getExpression().apply(this); + BType type = getType(node.getExpression()); + if (! (type instanceof FunctionType)){ + new SetType(new UntypedType()).unify(type, this); + } } @Override diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java index fb9174a0abbd14b772a095acd3e2ecd8c5a2a800..e9e826d9093945b3d2a682c72d695aa877cccbde 100644 --- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java +++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java @@ -7,18 +7,21 @@ import java.util.Hashtable; import java.util.List; import java.util.Set; +import de.be4.classicalb.core.parser.Utils; import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter; import de.be4.classicalb.core.parser.node.AAnySubstitution; import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution; import de.be4.classicalb.core.parser.node.AComprehensionSetExpression; import de.be4.classicalb.core.parser.node.AConjunctPredicate; import de.be4.classicalb.core.parser.node.AConstraintsMachineClause; +import de.be4.classicalb.core.parser.node.ACoupleExpression; import de.be4.classicalb.core.parser.node.ADisjunctPredicate; import de.be4.classicalb.core.parser.node.AEqualPredicate; import de.be4.classicalb.core.parser.node.AExistsPredicate; import de.be4.classicalb.core.parser.node.AForallPredicate; import de.be4.classicalb.core.parser.node.AGeneralProductExpression; import de.be4.classicalb.core.parser.node.AGeneralSumExpression; +import de.be4.classicalb.core.parser.node.AIdentifierExpression; import de.be4.classicalb.core.parser.node.AImplicationPredicate; import de.be4.classicalb.core.parser.node.AInitialisationMachineClause; import de.be4.classicalb.core.parser.node.AIntersectionExpression; @@ -46,6 +49,7 @@ import de.be4.ltl.core.parser.node.AForallLtl; import de.tlc4b.analysis.MachineContext; import de.tlc4b.analysis.Typechecker; import de.tlc4b.btypes.BType; +import de.tlc4b.exceptions.NotSupportedException; import de.tlc4b.ltl.LTLFormulaVisitor; public class TypeRestrictor extends DepthFirstAdapter { @@ -60,6 +64,8 @@ public class TypeRestrictor extends DepthFirstAdapter { private final Hashtable<Node, ArrayList<Node>> restrictedNodeTable; private final Hashtable<Node, ArrayList<Node>> subtractedNodeTable; + private final Hashtable<Node, ArrayList<Node>> restrictedCoupleTable; + public Node getRestrictedNode(Node node) { return restrictedTypeNodeTable.get(node); } @@ -78,6 +84,7 @@ public class TypeRestrictor extends DepthFirstAdapter { this.restrictedNodeTable = new Hashtable<Node, ArrayList<Node>>(); this.subtractedNodeTable = new Hashtable<Node, ArrayList<Node>>(); + this.restrictedCoupleTable = new Hashtable<Node, ArrayList<Node>>(); this.identifierDependencies = new IdentifierDependencies(machineContext); @@ -218,6 +225,24 @@ public class TypeRestrictor extends DepthFirstAdapter { putRestrictedType(r_right, new ASetExtensionExpression(element)); removedNodes.add(n); } + if (left instanceof ACoupleExpression) { + ACoupleExpression couple = (ACoupleExpression) left; + PExpression first = couple.getList().get(0); + Node r_first = machineContext.getReferenceNode(first); + PExpression second = couple.getList().get(0); + Node r_second = machineContext.getReferenceNode(second); + + if (list.contains(r_first) && list.contains(r_second) + && isAConstantExpression(right, list, ignoreList)) { + ArrayList<PExpression> element = new ArrayList<PExpression>(); + element.add(right); + putRestrictedTypeOfTuple(r_right, + new ASetExtensionExpression(element)); + removedNodes.add(n); + } + + } + return; } @@ -299,6 +324,18 @@ public class TypeRestrictor extends DepthFirstAdapter { } } + private void putRestrictedTypeOfTuple(Node identifier, + PExpression restrictedType) { + ArrayList<Node> list = restrictedCoupleTable.get(identifier); + if (list == null) { + list = new ArrayList<Node>(); + list.add(restrictedType); + restrictedCoupleTable.put(identifier, list); + } else { + list.add(restrictedType); + } + } + public boolean isAConstantExpression(Node node, HashSet<Node> list, HashSet<Node> ignoreList) { HashSet<Node> newList = new HashSet<Node>(); @@ -475,7 +512,6 @@ public class TypeRestrictor extends DepthFirstAdapter { node.getIdentifiers())); } - @Override public void inALetSubstitution(ALetSubstitution node) { HashSet<Node> list = new HashSet<Node>(); @@ -520,6 +556,19 @@ public class TypeRestrictor extends DepthFirstAdapter { conType = typechecker.getType(machineContext .getReferenceNode(e)); } + if (conType.containsIntegerType() + && !(e.parent() instanceof ALambdaExpression) + && !(e.parent() instanceof AComprehensionSetExpression)) { + AIdentifierExpression id = (AIdentifierExpression) e; + String localVariableName = Utils.getIdentifierAsString(id + .getIdentifier()); + throw new NotSupportedException( + "Can not restrict the type of the variable '" + + localVariableName + + "' to a finite set. TLC is not able to handle infinite sets.\n" + + e.getStartPos()); + } + tree = conType.createSyntaxTreeNode(typechecker); } else { tree = (PExpression) restrictedList.get(0); diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index f07ed67e7e8aca5c7b609bb7a538a4fd3707bdd9..c1e861c23962689b6ff2d3bbde139d178fa15969 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -920,7 +920,12 @@ public class TLAPrinter extends DepthFirstAdapter { tlaModuleString.append(" : "); } - node.getPredicate().apply(this); + if (typeRestrictor.isARemovedNode(node.getPredicate())) { + tlaModuleString.append("TRUE"); + } else { + node.getPredicate().apply(this); + } + tlaModuleString.append(" /\\ "); node.getSubstitution().apply(this); printUnchangedVariables(node, true); @@ -1634,7 +1639,7 @@ public class TLAPrinter extends DepthFirstAdapter { } @Override - // Functioncall + // Function call public void caseAFunctionExpression(AFunctionExpression node) { inAFunctionExpression(node); @@ -2050,11 +2055,16 @@ public class TLAPrinter extends DepthFirstAdapter { @Override public void caseACardExpression(ACardExpression node) { - inACardExpression(node); - tlaModuleString.append("Cardinality("); - node.getExpression().apply(this); - tlaModuleString.append(")"); - outACardExpression(node); + BType type = typechecker.getType(node.getExpression()); + if(type instanceof FunctionType){ + tlaModuleString.append("Cardinality(DOMAIN("); + node.getExpression().apply(this); + tlaModuleString.append("))"); + }else{ + tlaModuleString.append("Cardinality("); + node.getExpression().apply(this); + tlaModuleString.append(")"); + } } @Override diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java index d96e9a698b69661e96851c4637821fd428d14317..6d824ff568f4d7160d2a0443fb0db8e851dbd750 100644 --- a/src/main/java/de/tlc4b/tlc/TLCResults.java +++ b/src/main/java/de/tlc4b/tlc/TLCResults.java @@ -90,7 +90,6 @@ public class TLCResults { ArrayList<Message> messages = OutputCollector.getAllMessages(); for (Message m : messages) { - switch (m.getMessageClass()) { case ERROR: evalErrorMessage(m); @@ -147,11 +146,12 @@ public class TLCResults { } private void evalErrorMessage(Message m) { - // System.out.print(m.getMessageCode() + " "+ m.getParameters().length); - // for (int i = 0; i < m.getParameters().length; i++) { - // System.out.print(" "+m.getParameters()[i]); - // } - // System.out.println(); +// System.out.println(------------------); +// System.out.print(m.getMessageCode() + " " + m.getParameters().length); +// for (int i = 0; i < m.getParameters().length; i++) { +// System.out.print(" " + m.getParameters()[i]); +// } +// System.out.println(); switch (m.getMessageCode()) { case EC.TLC_INVARIANT_VIOLATED_INITIAL: case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR: @@ -219,6 +219,8 @@ public class TLCResults { return InvariantViolation; } else if (s.contains("In applying the function")) { return WellDefinednessError; + } else if (s.contains("which is not in the domain of the function")) { + return WellDefinednessError; } else if (s.contains("tlc2.module.TLC.Assert")) { return tlcResult = WellDefinednessError; } else if (s diff --git a/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java index 51083fef343973b5588fd60bdd9a24e45d076dcc..0e18c33e1acd03d18ee0638ba59951cd893ff400 100644 --- a/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java +++ b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java @@ -4,6 +4,8 @@ import static de.tlc4b.util.TestUtil.compare; import org.junit.Test; +import de.tlc4b.exceptions.NotSupportedException; + public class ExpressionConstantTest { @Test @@ -43,7 +45,7 @@ public class ExpressionConstantTest { compare(expected, machine); } - @Test + @Test (expected = NotSupportedException.class) public void testNotConstantBoundedVariable() throws Exception { String machine = "MACHINE test\n" + "PROPERTIES !x,y.(x = y & y = 1 => 1 = 1)\n" + "END"; diff --git a/src/test/java/de/tlc4b/analysis/ScopeTest.java b/src/test/java/de/tlc4b/analysis/ScopeTest.java index 7ab79c9dc81fe22869d4059a86331f135f70ff54..cf65a0f0f8c59abac7f961a6899293aa9f95cbbf 100644 --- a/src/test/java/de/tlc4b/analysis/ScopeTest.java +++ b/src/test/java/de/tlc4b/analysis/ScopeTest.java @@ -147,7 +147,7 @@ public class ScopeTest { @Test public void testNestedLocalExists() throws Exception { String machine = "MACHINE test\n" - + "PROPERTIES #x.(x : INT & #x.(x + 1 = 1))\n" + "END"; + + "PROPERTIES #x.(x : {1} & #x.(x : {1} & x + 1 = 1))\n" + "END"; checkMachine(machine); } diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java index 174c60175ca0c8557d6bebefa27a6c1ac5433a78..37e24e4e8d1270adde7aa635487860992805ecd2 100644 --- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java +++ b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java @@ -2,6 +2,7 @@ package de.tlc4b.analysis; import static de.tlc4b.util.TestUtil.compare; +import org.junit.Ignore; import org.junit.Test; public class TypeRestrictionsTest { @@ -73,6 +74,7 @@ public class TypeRestrictionsTest { compare(expected, machine); } + @Ignore @Test public void testExistQuantification2VariablesNotConstant() throws Exception { String machine = "MACHINE test\n" @@ -194,7 +196,7 @@ public class TypeRestrictionsTest { compare(expected, machine); } - + @Ignore @Test public void testExistDependingVariables() throws Exception { String machine = "MACHINE test\n" @@ -240,5 +242,17 @@ public class TypeRestrictionsTest { compare(expected, machine); } + @Ignore + @Test + public void testCoupleOfParameters() throws Exception { + String machine = "MACHINE test\n" + + "PROPERTIES #a,b.( (a,b) : {(1,1)})\n" + "END"; + + String expected = "---- MODULE test----\n" + "EXTENDS Integers\n" + + "ASSUME \\E <<a,b>> \\in {<<1,1>>} : TRUE \n" + + "======"; + compare(expected, machine); + } + } diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java b/src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java new file mode 100644 index 0000000000000000000000000000000000000000..bf3ff72a179601711918c68251dae60da4ca7207 --- /dev/null +++ b/src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java @@ -0,0 +1,20 @@ +package de.tlc4b.prettyprint; + +import static de.tlc4b.util.TestUtil.compare; + +import org.junit.Test; + +public class FunctionsVsRelations { + + @Test + public void testCardOnAFunction() throws Exception { + String machine = "MACHINE test\n" + + "PROPERTIES 1 = card(%x.(x = 1 | 1))\n" + + "END"; + String expected = "---- MODULE test----\n" + + "EXTENDS FiniteSets\n" + + "ASSUME 1 = Cardinality(DOMAIN([x \\in {1} |-> 1 ]))\n" + + "======"; + compare(expected, machine); + } +} diff --git a/src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java b/src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java new file mode 100644 index 0000000000000000000000000000000000000000..8e8780c92eae7a1c305b9a2e1cff571e1465d58f --- /dev/null +++ b/src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java @@ -0,0 +1,20 @@ +package de.tlc4b.typechecking; + +import static org.junit.Assert.assertEquals; + +import org.junit.Test; + +import de.be4.classicalb.core.parser.exceptions.BException; + +public class FunctionsVsRelations { + + @Test + public void testCardFunction() throws BException { + String machine = "MACHINE test\n" + + "CONSTANTS k \n" + + "PROPERTIES k = %x.(x : {1} | 1) & card(k) = 1 \n" + + "END"; + TestTypechecker t = new TestTypechecker(machine); + assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString()); + } +} diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java index 651c0e5c249d54e8d92917a10739c159c017ae03..438b8c00fb31fc1c39cc14434fa57270b86b0dc7 100644 --- a/src/test/java/de/tlc4b/util/TLC4BTester.java +++ b/src/test/java/de/tlc4b/util/TLC4BTester.java @@ -7,7 +7,7 @@ public class TLC4BTester { public static void main(String[] args) throws Exception { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows - TLC4B.test(args,false); + TLC4B.test(args,true); } } diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java index 41414861b9998ca2837c50f73f0956b7892eb3b6..a1556b7acb2697db747339451a224518e70342c7 100644 --- a/src/test/java/testing/Testing2.java +++ b/src/test/java/testing/Testing2.java @@ -29,9 +29,9 @@ public class Testing2 extends AbstractParseMachineTest { @Test public void testRunTLC() throws Exception { String[] a = new String[] { - machine.getPath()}; - TLC4B.main(a); - //TLC4B.test(a,false); + machine.getPath(), "-noLTL", "-wdcheck"}; + //TLC4B.main(a); + TLC4B.test(a,false); //test(a); } diff --git a/src/test/resources/basics/SubstitutionsTest.mch b/src/test/resources/basics/SubstitutionsTest.mch index 17c44c404d79cd73dad86e3e2435f880b17a6052..919d8179c291cba40b304873150957b9221b681e 100644 --- a/src/test/resources/basics/SubstitutionsTest.mch +++ b/src/test/resources/basics/SubstitutionsTest.mch @@ -1,4 +1,4 @@ -MACHINE FunctionsTest +MACHINE SubstitutionsTest VARIABLES x INVARIANT x : 1..5 INITIALISATION x := 1 @@ -6,5 +6,7 @@ OPERATIONS op1 = PRE 1 = 1 THEN x := 2 END; op2 = LET a, b, c BE a = 1 & b : {1} & c = 2 IN x := 2 END; op3 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 ELSE x:= 3 END; -op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END +op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END; + +op5 = BEGIN LET p BE p = 2 IN x:= p END END END \ No newline at end of file