diff --git a/build.gradle b/build.gradle index 377d90e315d7750d85457d8910df395bf494c847..719b1678bbeb6d87dd348ab0d3119bbfdd51e46e 100644 --- a/build.gradle +++ b/build.gradle @@ -41,7 +41,7 @@ dependencies { test { exclude('de/b2tla/tlc/integration/probprivate') - exclude('de/b2tla/tlc/integration/testing') + exclude('testing') } diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java index 15a896e2ab3c4641435ccdec5d4338390a28b4c9..6f698e536f97ff2a5a8e6db7818af830ec111326 100644 --- a/src/main/java/de/b2tla/B2TLA.java +++ b/src/main/java/de/b2tla/B2TLA.java @@ -40,6 +40,7 @@ public class B2TLA { try { b2tla.progress(args); } catch (BException e) { + System.err.println("***** Parsing Error *****"); System.err.println(e.getMessage()); return; } catch (B2tlaException e) { diff --git a/src/main/java/de/b2tla/B2TlaTranslator.java b/src/main/java/de/b2tla/B2TlaTranslator.java index 0ebda89cb4a695c568661d2748e881634066e14f..b409d9ff5be4947a2aa7a366e57dd656382a999f 100644 --- a/src/main/java/de/b2tla/B2TlaTranslator.java +++ b/src/main/java/de/b2tla/B2TlaTranslator.java @@ -28,7 +28,6 @@ import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.node.APredicateParseUnit; import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.Start; -import de.be4.ltl.core.parser.node.TYesterday; public class B2TlaTranslator { @@ -72,8 +71,15 @@ public class B2TlaTranslator { if(constantSetup!= null){ - BParser con = new BParser("Constants"); - Start start2 = con.parse("#FORMULA " + constantSetup, false); + BParser con = new BParser(); + Start start2 = null; + try { + start2 = con.parse("#FORMULA " + constantSetup, false); + } catch (BException e) { + System.err.println("An error occured while parsing the constants setup predicate."); + throw e; + } + APredicateParseUnit parseUnit = (APredicateParseUnit) start2.getPParseUnit(); this.constantsSetup = parseUnit.getPredicate(); @@ -101,7 +107,7 @@ public class B2TlaTranslator { machineContext); PrecedenceCollector precedenceCollector = new PrecedenceCollector( - start, typechecker.getTypes()); + start, typechecker.getTypes(), machineContext); ConstantsEliminator constantsEliminator = new ConstantsEliminator( machineContext); diff --git a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java index 057ef9a5487bd790bbab137382a2dc5f4efadd79..c4d1c7ab13fe3a9db26d18d0979f5b45b677cc91 100644 --- a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java +++ b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java @@ -14,11 +14,9 @@ import de.be4.classicalb.core.parser.node.AConjunctPredicate; import de.be4.classicalb.core.parser.node.AConstraintsMachineClause; import de.be4.classicalb.core.parser.node.ADisjunctPredicate; import de.be4.classicalb.core.parser.node.AEqualPredicate; -import de.be4.classicalb.core.parser.node.AGreaterPredicate; import de.be4.classicalb.core.parser.node.AIdentifierExpression; import de.be4.classicalb.core.parser.node.AIntegerExpression; import de.be4.classicalb.core.parser.node.AInvariantMachineClause; -import de.be4.classicalb.core.parser.node.ALessEqualPredicate; import de.be4.classicalb.core.parser.node.APredicateParseUnit; import de.be4.classicalb.core.parser.node.APropertiesMachineClause; import de.be4.classicalb.core.parser.node.Node; @@ -57,11 +55,15 @@ public class ConstantsEvaluator extends DepthFirstAdapter { public LinkedHashMap<Node, Node> getValueOfIdentifierMap() { return valueOfIdentifier; } - + public Integer getIntValue(Node node) { return integerValueTable.get(node); } + public ArrayList<PExpression> getRangeOfIdentifier(Node con){; + return valuesOfConstantsFinder.rangeOfIdentifierTable.get(con); + } + public ConstantsEvaluator(MachineContext machineContext) { this.dependsOnIdentifierTable = new Hashtable<Node, HashSet<Node>>(); this.integerValueTable = new HashMap<Node, Integer>(); @@ -71,10 +73,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter { ConstantsInTreeFinder constantInTreeFinder = new ConstantsInTreeFinder(); - if(machineContext.getConstantsSetup()!= null){ - machineContext.getConstantsSetup().apply(constantInTreeFinder); - } - + if (machineContext.getConstantsSetup() != null) { + machineContext.getConstantsSetup().apply(constantInTreeFinder); + } + APropertiesMachineClause properties = machineContext .getPropertiesMachineClause(); if (null != properties) { @@ -145,10 +147,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter { HashSet<Node> set = dependsOnIdentifierTable.get(node); Node parent = node.parent(); HashSet<Node> parentSet = dependsOnIdentifierTable.get(parent); - if(parentSet!= null){ + if (parentSet != null) { parentSet.addAll(set); } - + } @Override @@ -156,9 +158,9 @@ public class ConstantsEvaluator extends DepthFirstAdapter { defaultIn(node); node.getPredicates().apply(this); } - + @Override - public void caseAPredicateParseUnit(APredicateParseUnit node){ + public void caseAPredicateParseUnit(APredicateParseUnit node) { defaultIn(node); node.getPredicate(); } @@ -184,19 +186,23 @@ public class ConstantsEvaluator extends DepthFirstAdapter { class ValuesOfIdentifierFinder extends DepthFirstAdapter { private Hashtable<Node, HashSet<Node>> valuesOfIdentifierTable; + private Hashtable<Node, ArrayList<PExpression>> rangeOfIdentifierTable; private HashSet<Node> identifiers; public ValuesOfIdentifierFinder() { - valuesOfIdentifierTable = new Hashtable<Node, HashSet<Node>>(); + this.valuesOfIdentifierTable = new Hashtable<Node, HashSet<Node>>(); + this.rangeOfIdentifierTable = new Hashtable<Node, ArrayList<PExpression>>(); this.identifiers = new HashSet<Node>(); - identifiers.addAll(machineContext.getConstants().values()); - identifiers.addAll(machineContext.getScalarParameter().values()); + this.identifiers.addAll(machineContext.getConstants().values()); + this.identifiers.addAll(machineContext.getScalarParameter() + .values()); Iterator<Node> itr = identifiers.iterator(); while (itr.hasNext()) { Node id = itr.next(); valuesOfIdentifierTable.put(id, new HashSet<Node>()); + rangeOfIdentifierTable.put(id, new ArrayList<PExpression>()); } Node constraints = machineContext.getConstraintMachineClause(); @@ -206,11 +212,26 @@ public class ConstantsEvaluator extends DepthFirstAdapter { .getPredicates(), false); } - - if(machineContext.getConstantsSetup() != null){ - analysePredicate(machineContext.getConstantsSetup(), true); + + if (machineContext.getConstantsSetup() != null) { + if (machineContext.getConstantsSetup() instanceof ADisjunctPredicate) { + analyseConstantSetupPredicate(machineContext + .getConstantsSetup()); + + for (Node con : this.identifiers) { + ArrayList<PExpression> list = rangeOfIdentifierTable.get(con); + if(list.size() == 1){ + // there only one value for the constant con, hence con remains a constant + valuesOfIdentifierTable.get(con).add(list.get(0)); + } + } + }else{ + analysePredicate(machineContext.getConstantsSetup(), true); + } + + } - + Node properties = machineContext.getPropertiesMachineClause(); if (properties != null) { PPredicate predicate = (PPredicate) ((APropertiesMachineClause) properties) @@ -226,6 +247,35 @@ public class ConstantsEvaluator extends DepthFirstAdapter { } } + private void analyseConstantSetupPredicate(PPredicate constantsSetup) { + if (constantsSetup instanceof ADisjunctPredicate) { + ADisjunctPredicate dis = (ADisjunctPredicate) constantsSetup; + analyseConstantSetupPredicate(dis.getLeft()); + analyseConstantSetupPredicate(dis.getRight()); + } else if (constantsSetup instanceof AConjunctPredicate) { + AConjunctPredicate con = (AConjunctPredicate) constantsSetup; + analyseConstantSetupPredicate(con.getLeft()); + analyseConstantSetupPredicate(con.getRight()); + } else if (constantsSetup instanceof AEqualPredicate) { + AEqualPredicate equals = (AEqualPredicate) constantsSetup; + PExpression left = equals.getLeft(); + Node left_ref = machineContext.getReferences().get(left); + ArrayList<PExpression> currentRange = rangeOfIdentifierTable.get(left_ref); + + boolean found = false; + for (PExpression pExpression : currentRange) { + if(pExpression.toString().equals(equals.getRight().toString())){ + found = true; + } + } + if(found == false){ + currentRange.add((PExpression) equals.getRight()); + } + + } + + } + private void analyseInvariantPredicate(Node node) { if (node instanceof AConjunctPredicate) { AConjunctPredicate conjunction = (AConjunctPredicate) node; @@ -240,14 +290,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter { private void analysePredicate(Node node, boolean isProperties) { if (node instanceof AEqualPredicate) { analyseEqualsPredicate((AEqualPredicate) node); - } - // else if (node instanceof AGreaterPredicate) { - // analyseGreaterPredicate((AGreaterPredicate) node); - // } - // else if (node instanceof ALessEqualPredicate) { - // analyseLessEqualPredicate((ALessEqualPredicate) node); - // } - else if (node instanceof AConjunctPredicate) { + } else if (node instanceof AConjunctPredicate) { AConjunctPredicate conjunction = (AConjunctPredicate) node; analysePredicate(conjunction.getLeft(), isProperties); analysePredicate(conjunction.getRight(), isProperties); @@ -259,42 +302,6 @@ public class ConstantsEvaluator extends DepthFirstAdapter { } } - private void analyseLessEqualPredicate(ALessEqualPredicate node) { - PExpression left = node.getLeft(); - Node left_ref = machineContext.getReferences().get(left); - PExpression right = node.getRight(); - Node right_ref = machineContext.getReferences().get(right); - if (identifiers.contains(left_ref)) { - AIntegerExpression intExpr = (AIntegerExpression) right; - int value = Integer.parseInt(intExpr.getLiteral().getText()); - integerValueTable.put(left_ref, value); - } - - if (identifiers.contains(right_ref)) { - AIntegerExpression intExpr = (AIntegerExpression) left; - int value = Integer.parseInt(intExpr.getLiteral().getText()); - integerValueTable.put(right_ref, value); - } - } - - private void analyseGreaterPredicate(AGreaterPredicate node) { - PExpression left = node.getLeft(); - Node left_ref = machineContext.getReferences().get(left); - PExpression right = node.getRight(); - Node right_ref = machineContext.getReferences().get(right); - if (identifiers.contains(left_ref)) { - AIntegerExpression intExpr = (AIntegerExpression) right; - int value = Integer.parseInt(intExpr.getLiteral().getText()); - integerValueTable.put(left_ref, value + 1); - } - - if (identifiers.contains(right_ref)) { - AIntegerExpression intExpr = (AIntegerExpression) left; - int value = Integer.parseInt(intExpr.getLiteral().getText()); - integerValueTable.put(right_ref, value - 1); - } - } - private void analyseEqualsPredicate(AEqualPredicate node) { PExpression left = node.getLeft(); Node left_ref = machineContext.getReferences().get(left); diff --git a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java b/src/main/java/de/b2tla/analysis/PrecedenceCollector.java index f6dbd95d4f01e99b73a3bb1c9a99c5b712b84b3b..1c6b0ae6eb481b23423d3f20271cc6ce025d7f2f 100644 --- a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java +++ b/src/main/java/de/b2tla/analysis/PrecedenceCollector.java @@ -71,11 +71,16 @@ public class PrecedenceCollector extends DepthFirstAdapter { return brackets; } - public PrecedenceCollector(Start start, Hashtable<Node, BType> types) { + public PrecedenceCollector(Start start, Hashtable<Node, BType> types, MachineContext machineContext) { precedenceTable = new Hashtable<Node, Precedence>(); brackets = new HashSet<Node>(); typeTable = types; start.apply(this); + + if(machineContext.getConstantsSetup() != null){ + machineContext.getConstantsSetup().apply(this); + } + } @Override diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java index 635be7f6ce1a4d856787ce376f511c99c4711bf5..144b004b9852871dbf18d8e6f0f88df9477f6539 100644 --- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java +++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java @@ -356,7 +356,14 @@ public class TLAPrinter extends DepthFirstAdapter { return; tlaModuleString.append("Init == "); for (int i = 0; i < inits.size(); i++) { - inits.get(i).apply(this); + Node init = inits.get(i); + if(init instanceof ADisjunctPredicate){ + tlaModuleString.append("("); + } + init.apply(this); + if(init instanceof ADisjunctPredicate){ + tlaModuleString.append(")"); + } if (i < inits.size() - 1) tlaModuleString.append(" /\\ "); } diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java index 37776ba8358e841b8c9b712564124fffd00a4bbf..91050277c5f55417cc7041547a8f7b54f42d3723 100644 --- a/src/main/java/de/b2tla/tla/Generator.java +++ b/src/main/java/de/b2tla/tla/Generator.java @@ -30,6 +30,7 @@ import de.be4.classicalb.core.parser.node.AInvariantMachineClause; import de.be4.classicalb.core.parser.node.AMemberPredicate; import de.be4.classicalb.core.parser.node.AOperationsMachineClause; import de.be4.classicalb.core.parser.node.APropertiesMachineClause; +import de.be4.classicalb.core.parser.node.ASetExtensionExpression; import de.be4.classicalb.core.parser.node.AVariablesMachineClause; import de.be4.classicalb.core.parser.node.Node; import de.be4.classicalb.core.parser.node.PDefinition; @@ -255,9 +256,28 @@ public class Generator extends DepthFirstAdapter { .getPredicates(); if (remainingConstants.size() != 0) { boolean init = false; + int numberOfIteratedConstants = 0; + + for (int i = 0; i < remainingConstants.size(); i++) { + init = true; Node con = remainingConstants.get(i); this.tlaModule.variables.add(con); + + ArrayList<PExpression> rangeList = constantsEvaluator.getRangeOfIdentifier(con); + if(rangeList.size() > 0){ + numberOfIteratedConstants++; + ArrayList<PExpression> clone = new ArrayList<PExpression>(); + for (PExpression pExpression : rangeList) { + clone.add((PExpression) pExpression.clone()); + } + ASetExtensionExpression set = new ASetExtensionExpression(clone); + AMemberPredicate member = new AMemberPredicate((AIdentifierExpression) con, set); + tlaModule.addInit(member); + continue; + } + + Integer value = constantsEvaluator.getIntValue(con); if (value == null) { init = true; @@ -305,15 +325,26 @@ public class Generator extends DepthFirstAdapter { } } + + if(numberOfIteratedConstants > 1){ + tlaModule.addInit(machineContext.getConstantsSetup()); + } + + if (init) { configFile.setInit(); tlaModule.addInit(propertiesPerdicate); } + + } else { tlaModule.assumes.addAll(constantsEvaluator.getPropertiesList()); // tlaModule.addAssume(propertiesPerdicate); } + + + } @Override diff --git a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java index 5241909ee89aec52839b86b8adeb7046c6e934af..58f4a4a56ab995148f475d6105060ce23ab259d9 100644 --- a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java +++ b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java @@ -37,7 +37,7 @@ public class BasicsTest extends AbstractParseMachineTest { @Config public static Configuration getConfig() { final ArrayList<TestPair> list = new ArrayList<TestPair>(); - //list.add(new TestPair(NoError, "./src/test/resources/basics")); + list.add(new TestPair(NoError, "./src/test/resources/basics")); list.add(new TestPair(NoError, "./src/test/resources/laws")); return getConfiguration(list); } diff --git a/src/test/java/de/b2tla/util/TestUtil.java b/src/test/java/de/b2tla/util/TestUtil.java index 282eb7843357b884e714350e8db8c48a4c5e86ff..14ebba8123dca772e6d354bfc9c1f9f955543940 100644 --- a/src/test/java/de/b2tla/util/TestUtil.java +++ b/src/test/java/de/b2tla/util/TestUtil.java @@ -178,9 +178,8 @@ public class TestUtil { //System.out.println(s); if(s.startsWith("Result:")){ String resultString = s.substring(s.indexOf(':') + 2); + resultString = resultString.replaceAll("\\s+",""); System.out.println(resultString); - resultString = resultString.replaceAll("\\s",""); - //System.out.println(resultString); return TLCResult.valueOf(resultString); } } diff --git a/src/test/resources/special/ConstantSetup.mch b/src/test/resources/special/ConstantSetup.mch new file mode 100644 index 0000000000000000000000000000000000000000..6e96835271198150c986a819f55c607efb36cd2b --- /dev/null +++ b/src/test/resources/special/ConstantSetup.mch @@ -0,0 +1,10 @@ +MACHINE ConstantSetup +CONSTANTS a, b +PROPERTIES a : NAT & b : NAT +VARIABLES x, y +INVARIANT + x : NAT & y : NAT +INITIALISATION x := a || y := b +OPERATIONS +foo = skip +END \ No newline at end of file