diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java
index bb0655a2de9aed0dfbe80f56fc2222bfac219b47..09df230e3fbd0f6cbe105808851188fda78f4a3f 100644
--- a/src/main/java/de/b2tla/B2TLA.java
+++ b/src/main/java/de/b2tla/B2TLA.java
@@ -35,6 +35,7 @@ public class B2TLA {
private B2TlaTranslator translator;
private TLCOutputInfo tlcOutputInfo;
private String ltlFormula;
+ private String constantsSetup;
public static void main(String[] args) throws IOException {
B2TLA b2tla = new B2TLA();
@@ -70,6 +71,7 @@ public class B2TLA {
throws IOException {
B2TLAGlobals.resetGlobals();
B2TLAGlobals.setDeleteOnExit(deleteFiles);
+ // B2TLAGlobals.setCleanup(true);
B2TLA b2tla = new B2TLA();
try {
b2tla.progress(args);
@@ -159,7 +161,7 @@ public class B2TLA {
} else if (args[index].toLowerCase().equals("-del")) {
B2TLAGlobals.setDeleteOnExit(true);
- }else if (args[index].toLowerCase().equals("-workers")) {
+ } else if (args[index].toLowerCase().equals("-workers")) {
index = index + 1;
if (index == args.length) {
throw new B2TLAIOException(
@@ -167,8 +169,14 @@ public class B2TLA {
}
int workers = Integer.parseInt(args[index]);
B2TLAGlobals.setWorkers(workers);
- }
- else if (args[index].toLowerCase().equals("-ltlformula")) {
+ } else if (args[index].toLowerCase().equals("-constantssetup")) {
+ index = index + 1;
+ if (index == args.length) {
+ throw new B2TLAIOException(
+ "Error: String requiered after option '-constantsetup'.");
+ }
+ constantsSetup = args[index];
+ } else if (args[index].toLowerCase().equals("-ltlformula")) {
index = index + 1;
if (index == args.length) {
throw new B2TLAIOException(
@@ -202,7 +210,7 @@ public class B2TLA {
StopWatch.start("Parsing");
translator = new B2TlaTranslator(
machineFileNameWithoutFileExtension, getFile(),
- this.ltlFormula);
+ this.ltlFormula, this.constantsSetup);
StopWatch.stop("Parsing");
StopWatch.start("Pure");
translator.translate();
diff --git a/src/main/java/de/b2tla/B2TLAGlobals.java b/src/main/java/de/b2tla/B2TLAGlobals.java
index 233b7cec3b07f8a20b3720e06aeb8a4b0b640fc5..8b1589d95d6b3ce0d0195345ec11e5b800357cec 100644
--- a/src/main/java/de/b2tla/B2TLAGlobals.java
+++ b/src/main/java/de/b2tla/B2TLAGlobals.java
@@ -16,6 +16,8 @@ public class B2TLAGlobals {
private static boolean translate;
private static boolean hideTLCConsoleOutput;
private static boolean createTraceFile;
+
+ private static boolean cleanup;
private static int workers;
@@ -36,6 +38,8 @@ public class B2TLAGlobals {
checkInvariant = true;
checkLTL = true;
+ setCleanup(true);
+
workers = 1;
// for debugging purposes
@@ -162,5 +166,13 @@ public class B2TLAGlobals {
public static int getWorkers(){
return B2TLAGlobals.workers;
}
+
+ public static boolean isCleanup() {
+ return cleanup;
+ }
+
+ public static void setCleanup(boolean cleanup) {
+ B2TLAGlobals.cleanup = cleanup;
+ }
}
diff --git a/src/main/java/de/b2tla/B2TlaTranslator.java b/src/main/java/de/b2tla/B2TlaTranslator.java
index b1f484c07729a0b5010674bf95bc16bd7547fcd2..e717c22239140f60646a3fcd72021ffb8679ea30 100644
--- a/src/main/java/de/b2tla/B2TlaTranslator.java
+++ b/src/main/java/de/b2tla/B2TlaTranslator.java
@@ -9,6 +9,7 @@ import de.b2tla.analysis.ConstantsEliminator;
import de.b2tla.analysis.ConstantsEvaluator;
import de.b2tla.analysis.DefinitionsAnalyser;
import de.b2tla.analysis.MachineContext;
+import de.b2tla.analysis.NotSupportedConstructs;
import de.b2tla.analysis.UnchangedVariablesFinder;
import de.b2tla.analysis.PrecedenceCollector;
import de.b2tla.analysis.PrimedNodesMarker;
@@ -24,6 +25,8 @@ import de.b2tla.tlc.TLCOutputInfo;
import de.b2tla.util.StopWatch;
import de.be4.classicalb.core.parser.BParser;
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;
@@ -35,6 +38,7 @@ public class B2TlaTranslator {
private String configString;
private String machineName;
private String ltlFormula;
+ private PPredicate constantsSetup;
private ArrayList<STANDARD_MODULES> usedStandardModules;
private TLCOutputInfo tlcOutputInfo;
@@ -46,8 +50,9 @@ public class B2TlaTranslator {
start.apply(ast2String2);
System.out.println(ast2String2.toString());
}
-
- public B2TlaTranslator(String machineString, String ltlFormula) throws BException {
+
+ public B2TlaTranslator(String machineString, String ltlFormula)
+ throws BException {
this.machineString = machineString;
this.ltlFormula = ltlFormula;
BParser parser = new BParser("Testing");
@@ -57,30 +62,49 @@ public class B2TlaTranslator {
System.out.println(ast2String2.toString());
}
- public B2TlaTranslator(String machineName, File machineFile, String ltlFormula)
+ public B2TlaTranslator(String machineName, File machineFile, String ltlFormula, String constantSetup)
throws IOException, BException {
this.machineName = machineName;
this.ltlFormula = ltlFormula;
+
BParser parser = new BParser(machineName);
start = parser.parseFile(machineFile, false);
- final Ast2String ast2String2 = new Ast2String();
+
+
+ if(constantSetup!= null){
+ BParser con = new BParser("Constants");
+ Start start2 = con.parse("#FORMULA " + constantSetup, false);
+ APredicateParseUnit parseUnit = (APredicateParseUnit) start2.getPParseUnit();
+ this.constantsSetup = parseUnit.getPredicate();
+
+ final Ast2String ast2String2 = new Ast2String();
+ start2.apply(ast2String2);
+ System.out.println(ast2String2.toString());
+ }
+
+ final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- // System.out.println(ast2String2.toString());
+ System.out.println(ast2String2.toString());
}
public void translate() {
DefinitionsEliminator defEliminator = new DefinitionsEliminator(start);
-
- MachineContext machineContext = new MachineContext(machineName, start, ltlFormula);
+
+ new NotSupportedConstructs(start);
+
+ MachineContext machineContext = new MachineContext(machineName, start,
+ ltlFormula, constantsSetup);
this.machineName = machineContext.getMachineName();
-
+
Typechecker typechecker = new Typechecker(machineContext);
- UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(machineContext);
-
+ UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
+ machineContext);
+
PrecedenceCollector precedenceCollector = new PrecedenceCollector(
start, typechecker.getTypes());
- ConstantsEliminator constantsEliminator = new ConstantsEliminator(machineContext);
+ ConstantsEliminator constantsEliminator = new ConstantsEliminator(
+ machineContext);
constantsEliminator.start();
ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(
@@ -92,7 +116,7 @@ public class B2TlaTranslator {
typeRestrictor);
start.apply(usedModules);
usedStandardModules = usedModules.getUsedModules();
-
+
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
machineContext);
@@ -105,7 +129,7 @@ public class B2TlaTranslator {
PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
.getTlaModule().getOperations(), machineContext);
primedNodesMarker.start();
-
+
Renamer renamer = new Renamer(machineContext);
TLAPrinter printer = new TLAPrinter(machineContext, typechecker,
unchangedVariablesFinder, precedenceCollector, usedModules,
diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java
index cf31a410dfee6c52c5e9f8186bac8e982037705e..b82a1ea8a5774f4fd22d1dc917b1cb347f71fe2e 100644
--- a/src/main/java/de/b2tla/TLCRunner.java
+++ b/src/main/java/de/b2tla/TLCRunner.java
@@ -67,6 +67,10 @@ public class TLCRunner {
if (!B2TLAGlobals.isDeadlockCheck()) {
list.add("-deadlock");
}
+
+ if(B2TLAGlobals.isCheckltl()){
+ list.add("-cleanup");
+ }
// list.add("-coverage");
// list.add("1");
diff --git a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java b/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
index f2a8d0b144e1a1e64ce4fb2d9c28ff8a83cae152..934a5c61f4362316d3a69281bdd1592cb842db01 100644
--- a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
@@ -10,12 +10,14 @@ import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
+import de.be4.classicalb.core.parser.node.ABlockSubstitution;
import de.be4.classicalb.core.parser.node.AChoiceOrSubstitution;
import de.be4.classicalb.core.parser.node.AChoiceSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AFunctionExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AIfElsifSubstitution;
import de.be4.classicalb.core.parser.node.AIfSubstitution;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
import de.be4.classicalb.core.parser.node.AOperation;
@@ -72,6 +74,15 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
}
}
+ @Override
+ public void caseABlockSubstitution(ABlockSubstitution node) {
+ inABlockSubstitution(node);
+ if (node.getSubstitution() != null) {
+ node.getSubstitution().apply(this);
+ }
+ outABlockSubstitution(node);
+ }
+
@Override
public void caseAOperation(AOperation node) {
node.getOperationBody().apply(this);
@@ -150,7 +161,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
list.add(identifier);
}
assignedVariablesTable.put(node, list);
- defaultCase(node);
+ defaultOut(node);
}
@Override
@@ -195,6 +206,16 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
defaultOut(node);
}
+ @Override
+ public void caseAIfElsifSubstitution(AIfElsifSubstitution node) {
+ HashSet<Node> list = new HashSet<Node>();
+ node.getThenSubstitution().apply(this);
+ list.addAll(getVariableList(node.getThenSubstitution()));
+
+ assignedVariablesTable.put(node, list);
+ defaultOut(node);
+ }
+
@Override
public void caseAParallelSubstitution(AParallelSubstitution node) {
List<PSubstitution> copy = new ArrayList<PSubstitution>(
diff --git a/src/main/java/de/b2tla/analysis/MachineContext.java b/src/main/java/de/b2tla/analysis/MachineContext.java
index ad7153a6f99510dd252cf6203103b29f4457afd7..bab46a8730e83a9d6fcfd1e8cb7a50e9437f428d 100644
--- a/src/main/java/de/b2tla/analysis/MachineContext.java
+++ b/src/main/java/de/b2tla/analysis/MachineContext.java
@@ -21,6 +21,7 @@ import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AConcreteVariablesMachineClause;
+import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
import de.be4.classicalb.core.parser.node.ADeferredSetSet;
@@ -76,6 +77,7 @@ public class MachineContext extends DepthFirstAdapter {
private final Start start;
private final Hashtable<String, MachineContext> machineContextsTable;
private ArrayList<LTLFormulaVisitor> ltlVisitors;
+ private PPredicate constantSetup;
// machine identifier
private final LinkedHashMap<String, Node> setParameter;
@@ -131,9 +133,10 @@ public class MachineContext extends DepthFirstAdapter {
// start.apply(this);
// }
- public MachineContext(String machineName, Start start, String ltlFormula) {
+ public MachineContext(String machineName, Start start, String ltlFormula, PPredicate constantSetup) {
this.start = start;
this.machineName = machineName;
+ this.constantSetup = constantSetup;
this.referencesTable = new Hashtable<Node, Node>();
this.ltlVisitors = new ArrayList<LTLFormulaVisitor>();
@@ -564,7 +567,12 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
this.propertiesMachineClause = node;
-
+
+ if(constantSetup != null){
+ AConjunctPredicate and = new AConjunctPredicate(constantSetup, node.getPredicates());
+ node.setPredicates(and);
+ }
+
/**
* check identifier scope in properties clauses
*/
diff --git a/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java b/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
new file mode 100644
index 0000000000000000000000000000000000000000..44af9247865862dd842abcb1c1ac9a5f87011c0b
--- /dev/null
+++ b/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
@@ -0,0 +1,25 @@
+package de.b2tla.analysis;
+
+import de.b2tla.exceptions.NotSupportedException;
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.ACaseSubstitution;
+import de.be4.classicalb.core.parser.node.AWhileSubstitution;
+import de.be4.classicalb.core.parser.node.Start;
+
+public class NotSupportedConstructs extends DepthFirstAdapter{
+
+ public NotSupportedConstructs(Start start){
+ start.apply(this);
+ }
+
+ public void inAWhileSubstitution(AWhileSubstitution node)
+ {
+ throw new NotSupportedException("While substitutions are currently not supported.");
+ }
+
+ public void inACaseSubstitution(ACaseSubstitution node)
+ {
+ throw new NotSupportedException("Case substitutions are currently not supported.");
+ }
+
+}
diff --git a/src/main/java/de/b2tla/analysis/Typechecker.java b/src/main/java/de/b2tla/analysis/Typechecker.java
index d26f33afbf446bb92f27f24167f8bc8f706eedd5..afba565867bee66997820a7dbf6fed59b67a0180 100644
--- a/src/main/java/de/b2tla/analysis/Typechecker.java
+++ b/src/main/java/de/b2tla/analysis/Typechecker.java
@@ -540,6 +540,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
+ @Override
+ public void caseAIfElsifSubstitution(AIfElsifSubstitution node) {
+ setType(node.getCondition(), BoolType.getInstance());
+ node.getCondition().apply(this);
+ node.getThenSubstitution().apply(this);
+ }
+
@Override
public void caseAAssignSubstitution(AAssignSubstitution node) {
List<PExpression> copy = new ArrayList<PExpression>(
diff --git a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java b/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
index 863a18bcb950de5ff9c8de91e33f56e66ebd8a50..cdfd2753e0e9d077df6618ef76f5aae227705439 100644
--- a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
@@ -10,11 +10,13 @@ import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AAssertionSubstitution;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
+import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.ABlockSubstitution;
import de.be4.classicalb.core.parser.node.AChoiceOrSubstitution;
import de.be4.classicalb.core.parser.node.AChoiceSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
+import de.be4.classicalb.core.parser.node.AIfElsifSubstitution;
import de.be4.classicalb.core.parser.node.AIfSubstitution;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
import de.be4.classicalb.core.parser.node.ALetSubstitution;
@@ -51,10 +53,10 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
private final Hashtable<Node, HashSet<Node>> unchangedVariablesNull;
- public HashSet<Node> getUnchangedVariables(Node node){
+ public HashSet<Node> getUnchangedVariables(Node node) {
return unchangedVariablesTable.get(node);
}
-
+
public HashSet<Node> getUnchangedVariablesNull(Node node) {
return unchangedVariablesNull.get(node);
}
@@ -129,6 +131,12 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
check(node);
}
+ @Override
+ public void caseABecomesElementOfSubstitution(
+ ABecomesElementOfSubstitution node) {
+ check(node);
+ }
+
@Override
public void caseAParallelSubstitution(AParallelSubstitution node) {
check(node);
@@ -201,7 +209,6 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
@Override
public void caseAIfSubstitution(AIfSubstitution node) {
check(node);
-
// Separating variables and output parameters
HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
HashSet<Node> foundVariables = new HashSet<Node>(foundIdentifiers);
@@ -233,6 +240,15 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
}
+ @Override
+ public void caseAIfElsifSubstitution(AIfElsifSubstitution node) {
+ expectedOutputParametersTable.put(node.getThenSubstitution(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getThenSubstitution(),
+ expectedVariablesTable.get(node));
+ node.getThenSubstitution().apply(this);
+ }
+
@Override
public void caseAPreconditionSubstitution(APreconditionSubstitution node) {
// check(node);
diff --git a/src/main/java/de/b2tla/exceptions/NotSupportedException.java b/src/main/java/de/b2tla/exceptions/NotSupportedException.java
new file mode 100644
index 0000000000000000000000000000000000000000..8d7abb93602c5eae37387990425d4536b20bd66f
--- /dev/null
+++ b/src/main/java/de/b2tla/exceptions/NotSupportedException.java
@@ -0,0 +1,15 @@
+package de.b2tla.exceptions;
+
+@SuppressWarnings("serial")
+public class NotSupportedException extends B2tlaException{
+
+
+ public NotSupportedException(String e){
+ super(e);
+ }
+
+ @Override
+ public String getError() {
+ return "NotSupportedException";
+ }
+}
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index aa3d7f33ee474221bdbae4b8245819a0ac84b31f..d2505674eae1b2373860f056307f1f18e0927966 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -134,17 +134,17 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append("))");
}
-
+
public void printWeakFairnessWithParameter(String s) {
Node operation = machineContext.getOperations().get(s.trim());
-
+
tlaModuleString.append("([]<><<");
printOperationCall(operation);
tlaModuleString.append(">>_vars \\/ []<>~ENABLED(");
printOperationCall(operation);
tlaModuleString.append(") \\/ []<> ENABLED(");
printOperationCall(operation);
- tlaModuleString.append(" /\\ ");
+ tlaModuleString.append(" /\\ ");
printVarsStuttering();
tlaModuleString.append("))");
@@ -661,6 +661,10 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIfSubstitution(AIfSubstitution node) {
+ if(node.getElsifSubstitutions().size() > 0){
+ printElseIFSubsitution(node);
+ return;
+ }
tlaModuleString.append("(IF ");
node.getCondition().apply(this);
tlaModuleString.append(" THEN ");
@@ -680,6 +684,37 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(")");
printUnchangedVariables(node, true);
}
+
+ private void printElseIFSubsitution(AIfSubstitution node){
+ tlaModuleString.append("(CASE ");
+ node.getCondition().apply(this);
+ tlaModuleString.append(" -> ");
+ node.getThen().apply(this);
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getElsifSubstitutions());
+ for (PSubstitution e : copy) {
+ tlaModuleString.append(" [] ");
+ e.apply(this);
+ }
+ tlaModuleString.append(" [] OTHER -> ");
+ if (node.getElse() != null) {
+ node.getElse().apply(this);
+ } else {
+ printUnchangedVariablesNull(node, false);
+ }
+ tlaModuleString.append(")");
+ printUnchangedVariables(node, true);
+
+ }
+
+ @Override
+ public void caseAIfElsifSubstitution(AIfElsifSubstitution node) {
+ node.getCondition().apply(this);
+ tlaModuleString.append(" -> ");
+ node.getThenSubstitution().apply(this);
+ printUnchangedVariables(node, true);
+
+ }
public void printUnchangedVariablesNull(Node node, boolean printAnd) {
HashSet<Node> unchangedVariablesSet = missingVariableFinder
@@ -2546,18 +2581,17 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAGeneralConcatExpression(AGeneralConcatExpression node) {
BType result = typechecker.getType(node.getExpression());
- if (result instanceof FunctionType && ((FunctionType) result).getRange() instanceof FunctionType) {
+ if (result instanceof FunctionType
+ && ((FunctionType) result).getRange() instanceof FunctionType) {
- }else{
- BType expected2 = new SetType(new PairType(IntegerType.getInstance(),
- new SetType(new PairType(IntegerType.getInstance(),
- new UntypedType()))));
+ } else {
+ BType expected2 = new SetType(new PairType(
+ IntegerType.getInstance(), new SetType(new PairType(
+ IntegerType.getInstance(), new UntypedType()))));
typechecker.unify(expected2, result, node);
}
-
- printSequenceOrRelation(node,
- SEQUENCE_GENERAL_CONCATINATION,
+ printSequenceOrRelation(node, SEQUENCE_GENERAL_CONCATINATION,
REL_SEQUENCE_GENERAL_CONCATINATION, node.getExpression(), null);
}
@@ -2613,7 +2647,8 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseACartesianProductExpression(ACartesianProductExpression node) {
- inACartesianProductExpression(node); //TODO cartesianproduct vs AMultOrCartExpression
+ inACartesianProductExpression(node); // TODO cartesianproduct vs
+ // AMultOrCartExpression
node.getLeft().apply(this);
tlaModuleString.append(" \\times ");
node.getRight().apply(this);
diff --git a/src/test/java/de/b2tla/prettyprint/SetTest.java b/src/test/java/de/b2tla/prettyprint/SetTest.java
index c1cbb5df128eea9b624cb34e3bc1bde601a5d8ae..85d68569c4d0b39d5e8f7411598977902963e538 100644
--- a/src/test/java/de/b2tla/prettyprint/SetTest.java
+++ b/src/test/java/de/b2tla/prettyprint/SetTest.java
@@ -3,7 +3,6 @@ package de.b2tla.prettyprint;
import static de.b2tla.util.TestUtil.*;
import static org.junit.Assert.*;
-import org.junit.Ignore;
import org.junit.Test;
public class SetTest {
@@ -48,16 +47,6 @@ public class SetTest {
compare(expected, machine);
}
- @Ignore
- @Test
- public void testSetComprehension3() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES (1,TRUE,2) : {a,b,c | (a,b,c) : {1} * {TRUE} * {2} } \n" + "END";
- String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
- + "ASSUME {1} = {x \\in {1}: 1 = 1 } \n"
- + "======";
- }
-
@Test
public void testPowerSet() throws Exception {
diff --git a/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java b/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
index f45c8511742a4d6fbdbbe34385bf084c0c4d0811..83708cefc72222ec2bb85f4ef08609c565060a43 100644
--- a/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
+++ b/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
@@ -2,6 +2,7 @@ package de.b2tla.prettyprint;
import static de.b2tla.util.TestUtil.compare;
+import org.junit.Ignore;
import org.junit.Test;
public class SubstitutionsTest {
@@ -94,4 +95,25 @@ public class SubstitutionsTest {
+ "====";
compare(expected, machine);
}
+
+ @Test
+ public void testIFElseIFSubstitution() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION IF 1=1 THEN x:= 1 ELSIF 1=2 THEN x:= 2 ELSE x:= 4 END \n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x \n"
+ + "Invariant == x = 1\n"
+ + "Init == (CASE 1 = 1 -> x = 1 [] 1 = 2 -> x = 2 [] OTHER -> x = 4)\n"
+ + "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ + "====";
+ compare(expected, machine);
+ }
+
+
+
}
diff --git a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
index b1ae13553db19f260e1e5174d001db9b3d636e74..d1849faa00f9d8a9739a6cfd9c7dbd8d9b48b669 100644
--- a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
@@ -10,7 +10,6 @@ import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
-import de.b2tla.B2TLAGlobals;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
index 5bcebb7bfb1321adc85c45101af6db79a493eee4..f086bdc2e88cf1f62ad9f6d8129d48385c7fc7e6 100644
--- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
@@ -3,12 +3,10 @@ package de.b2tla.tlc.integration;
import static de.b2tla.tlc.TLCOutput.TLCResult.*;
import static org.junit.Assert.*;
-import org.junit.BeforeClass;
import org.junit.Ignore;
import org.junit.Test;
import de.b2tla.B2TLA;
-import de.b2tla.B2TLAGlobals;
public class ErrorTest {
diff --git a/src/test/java/de/b2tla/typechecking/TestTypechecker.java b/src/test/java/de/b2tla/typechecking/TestTypechecker.java
index 533ec05451da468df9ee96331cda7365a54c5587..83c4b6ef5381f88861dda8c1a0996fe0f6c813ab 100644
--- a/src/test/java/de/b2tla/typechecking/TestTypechecker.java
+++ b/src/test/java/de/b2tla/typechecking/TestTypechecker.java
@@ -26,7 +26,7 @@ public class TestTypechecker {
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
System.out.println(ast2String2.toString());
- MachineContext c = new MachineContext(null, start, null);
+ MachineContext c = new MachineContext(null, start, null, null);
Typechecker t = new Typechecker(c);
for (String name : c.getSetParamter().keySet()) {
diff --git a/src/test/resources/basics/SetsTest.mch b/src/test/resources/basics/SetsTest.mch
index 120edd4cadf1f92e96592253b45045ca3ed2c759..66aca591201ba865a2dd06e3fcdc8a2cc7ed7d2e 100644
--- a/src/test/resources/basics/SetsTest.mch
+++ b/src/test/resources/basics/SetsTest.mch
@@ -3,4 +3,6 @@ PROPERTIES
union({{},{1},{1},{2},{2,3},{4}}) = {1,2,3,4}
& union({}) = {}
& UNION(x).(x :{2,4} | {y | y : 0..x}) = {0, 1, 2, 3, 4}
+& (1,TRUE,2) : {a,b,c | (a,b,c) : {1} * {TRUE} * {2} }
+& UNION(z).(z: {1,2} & 1 = 1| {z}) = {1,2}
END
\ No newline at end of file
diff --git a/src/test/resources/laws/SetLaws.mch b/src/test/resources/laws/SetLaws.mch
new file mode 100644
index 0000000000000000000000000000000000000000..1870a3384307f5852adea62f4c2ed1d4015c3de0
--- /dev/null
+++ b/src/test/resources/laws/SetLaws.mch
@@ -0,0 +1,174 @@
+MACHINE SetLaws
+
+SETS
+ setX = {el1,el2,el3}
+
+VARIABLES
+ SS, TT, VV
+
+DEFINITIONS
+ /*GOAL == (FIN1(SS)) = (FIN(SS)-{{}});*/
+ law1 == (SS \/ SS = SS & SS = SS \/ {} & SS = SS /\ SS & SS = SS \ {});
+ law2 == (SS /\ {} = {} & {} = SS \ SS & ({} \ SS = {}));
+ law3 == (SS \/ TT = TT \/ SS & SS /\ TT = TT /\ SS);
+ law4 == (( SS \/ (TT \/ VV) = (SS \/TT) \/ VV) & ( SS /\ (TT /\ VV) = (SS /\ TT) /\ VV));
+ law5 == ( SS \/ (TT /\ VV) = (SS \/ TT) /\ (SS \/ VV));
+ law6 == ( SS /\ (TT \/ VV) = (SS /\ TT) \/ (SS /\ VV));
+ law7 == ( (SS /\ TT) \/ (SS \ TT) = SS);
+ law8 == ((SS \ TT) /\ TT = {});
+ law9 == (SS \ (TT \ VV) = (SS \ TT) \/ (SS /\ VV));
+ law10 == ((SS \ TT) \ VV = (SS \ (TT \/ VV)));
+ law11 == (SS \/ (TT \ VV) = (SS \/ TT) \ (VV \ SS));
+ law12 == (SS /\ (TT \ VV) = (SS /\ TT) \ VV);
+ law13 == ((SS \/ TT) \ VV = (SS \ VV) \/ (TT \ VV));
+ law14 == (SS \ (TT /\ VV) = ( SS \ TT) \/ (SS \ VV));
+
+ orderlaw1 == (SS <: SS \/ TT & TT <: SS \/ TT);
+ orderlaw2 == ( ( SS <: VV & TT <: VV) => (SS\/TT <: VV));
+ orderlaw3 == (SS /\ TT <: SS & SS /\ TT <: TT);
+ orderlaw4 == ( (VV <: SS & VV <: TT) => (VV <: SS /\ TT));
+
+ setcomprlaw1 == ( {xx | xx: SS & xx:TT} = SS /\ TT);
+ setcomprlaw2 == ( {xx | xx: setX & (xx: SS or xx:TT)} = SS \/ TT);
+ setcomprlaw3 == ( {xx | xx: setX & xx: SS & (xx: TT or xx:VV)} = SS /\ (VV \/TT));
+ setcomprlaw4 == ( {xx | xx: SS & not(xx:TT)} = SS \ TT);
+
+ foralllaw1 == (!xx.(xx:SS & xx:TT => xx: SS /\ TT));
+ foralllaw2 == (!xx.(xx:SS & not(xx:TT) => (xx: SS \ TT & xx /: TT)));
+
+ existslaw1 == (#xx.(xx:SS & xx:TT & xx:VV) => not(SS /\ TT /\ VV = {}));
+ existslaw2 == (#xx.(xx:SS & xx/:TT) => not(SS \/ TT = TT) & not(SS \ TT = {}));
+
+
+ /* laws for <<:, <:, /<: and /<<: */
+ orderlaw5 == ( SS <<: VV or SS /<<: VV );
+ orderlaw6 == ( (VV <<: SS & SS <: TT) => (VV <<: TT));
+ orderlaw7 == ( (VV <: SS & SS <<: TT) => (VV <<: TT));
+ orderlaw8 == ( SS <: VV or SS /<: VV );
+ orderlaw9 == ( SS : POW(TT) or SS /: POW(TT) );
+
+ otherlaw1 == ( (SS <: VV & SS /<<: VV) => SS = VV);
+ otherlaw1b ==( SS <: VV => (SS /= VV <=> SS <<: VV));
+ otherlaw2 == ( (SS <<: VV ) => (SS /= VV & card(VV)>0));
+ otherlaw3 == ( (SS = VV ) => SS /<<: VV);
+ otherlaw4 == ( SS <<: VV => SS <: VV);
+ otherlaw5 == ( SS <<: VV => #xx.(xx:VV & xx/:SS));
+ otherlaw6 == ( SS <: VV <=> !x.(x:SS => x:VV) );
+
+ cardlaw1 == (SS <<: VV => (card(SS) < card(VV)));
+ cardlaw2 == (SS <: VV => (card(SS) <= card(VV)));
+ cardlaw3 == (card(SS) < card(VV) => (VV /<: SS));
+ cardlaw4 == (card(SS \/ VV) <= (card(SS) + card(VV)));
+ cardlaw5 == (card(SS) = card(VV) => (VV /<<: SS));
+ cardlaw6 == (card(SS) <= card(VV) => (VV /<<: SS));
+ cardlaw7 == (SS = VV => (card(SS) = card(VV)));
+ cardlaw8 == (card(SS /\ VV) <= card(SS) & card(SS /\ VV) <= card(VV));
+
+ difflaw1 == (SS /\ VV = {} <=> SS <: setX - VV);
+ difflaw2 == (SS \ VV = SS-VV);
+ difflaw3 == (VV-SS = VV\SS)
+
+INVARIANT
+ SS : POW(setX) & TT : POW(setX) & VV : POW(setX) &
+ law1 & law2 & law3 & law4 & law5 & law6 & law7 & law8 &
+ law9 & law10 & law11 & law12 & law13 & law14 &
+ orderlaw1 & orderlaw2 & orderlaw3 & orderlaw4 &
+ setcomprlaw1 & setcomprlaw2 & setcomprlaw3 & setcomprlaw4 &
+ foralllaw1 & foralllaw2 & existslaw1 & existslaw2 &
+
+ orderlaw5 & orderlaw6 & orderlaw7 &
+ orderlaw8 & orderlaw9 &
+ otherlaw1 & otherlaw1b & otherlaw2 & otherlaw3 & otherlaw4 & otherlaw5 & otherlaw6 &
+
+ cardlaw1 & cardlaw2 & cardlaw3 & cardlaw4 & cardlaw5 & cardlaw6 & cardlaw7 & cardlaw8
+ &
+ difflaw1 & difflaw2
+ &
+ difflaw3 &
+
+ (SS<<:VV or not(SS<<:VV)) & not(SS<<:VV & not(SS<<:VV)) &
+ (SS<:VV or not(SS<:VV)) & not(SS<:VV & not(SS<:VV)) &
+ /* */
+ (SS/<<:VV or not(SS/<<:VV)) & not(SS/<<:VV & not(SS/<<:VV)) &
+ (SS/<:VV or not(SS/<:VV)) & not(SS/<:VV & not(SS/<:VV)) &
+ (SS/:POW(TT) or not(SS/:POW(TT))) & not(SS/:POW(TT) & not(SS/:POW(TT))) &
+ (SS:POW(TT) or not(SS:POW(TT))) & not(SS:POW(TT) & not(SS:POW(TT))) &
+ ((POW1(SS)) = (POW(SS)-{{}})) &
+ card(POW1(SS)) = card(POW(SS)) - 1 &
+ card(POW(SS)-{{}}) = card(POW(SS)) - 1 &
+ ((FIN1(SS)) = (FIN(SS)-{{}})) &
+ {} : POW(SS) &
+ {} : FIN(SS) & /* this was false due to a bug in the Parser, which returned FIN1 for FIN */
+ {} /: POW1(SS) & {} /: FIN1(SS) &
+
+ (UNION(ss).(ss<:SS | ss) = SS) &
+ (card(SS) /= 1 <=> UNION(ss).(ss<<:SS | ss) = SS) &
+ (INTER(ss).(ss<:SS | ss) = {}) &
+
+ (SS : POW(TT) <=> SS <: TT) &
+ (SS=TT <=> POW(SS) = POW(TT)) &
+ (POW(SS-TT) = { xx | xx<:SS & xx /\ TT = {} })
+
+ & /* new, July 2008 */
+ SS /\ setX = SS &
+ SS \/ setX = setX &
+ SS \/ (setX \ SS) = setX &
+ SS /\ (setX \ SS) = {} &
+ (setX \ (setX \ SS) = SS)
+ &
+ (SS /\ TT = {} <=> not(#x.(x:SS & x:TT)) ) &
+ (SS /\ TT /\ VV = {} <=> not(#x.(x:SS & x:TT & x:VV)) ) &
+ (SS <: TT <=> not(#y.(y:SS & y/: TT)))
+
+ &
+ (SS/={} <=> #ee.(ee:SS) )
+ &
+ (SS /\ TT /= {} <=> #ee.(ee:SS & ee:TT) )
+ &
+ ( SS /<: TT <=> #ee.(ee:SS & ee/:TT))
+ &
+ ( SS<<:TT <=> (SS<:TT & #ee.(ee:TT & ee/:SS)))
+ &
+ (id(SS)=SS*SS <=> card(SS)<2) &
+ /* (SS*VV = TT*VV <=> (((SS={} or VV={}) & (TT={} or VV={})) or (SS=TT & VV=VV))) & ERROR in TLC */
+ (id(SS)=id(TT) <=> SS=TT) &
+ (id(SS) <: id(TT) <=> SS <: TT) &
+
+ /* laws on page 124 of B-Book */
+ (inter({SS}) = {x| !y.(y:{SS} => x:y)}) &
+ (inter({SS,TT}) = {x| !y.(y:{SS,TT} => x:y)}) &
+ (inter({SS,TT,VV}) = {x| !y.(y:{SS,TT,VV} => x:y)}) &
+ (union({}) = {x| x<:TT & #y.(y:{} & x:y)}) &
+ (union({SS}) = {x| #y.(y:{SS} & x:y)}) &
+ (union({SS,TT}) = {x| #y.(y:{SS,TT} & x:y)}) &
+ (union({SS,TT,VV}) = {x| #y.(y:{SS,TT,VV} & x:y)}) &
+
+ /* laws from page 127 of B-Book */
+ (inter({SS}) = SS) &
+ (union({SS}) = SS) &
+ (inter({SS,TT}) = SS /\ TT) &
+ (union({SS,TT}) = SS \/ TT)
+ASSERTIONS
+ /* (UNION(ss).(ss<:SS | ss) = SS);
+ (POW1(SS) = POW(SS) - {{}}); */
+ VV - SS = VV - SS
+INITIALISATION
+
+ SS,TT,VV := {},{},{}
+
+OPERATIONS
+/* cc <-- powss1 = BEGIN cc := POW(SS-TT) END;
+cc <-- powss2 = BEGIN cc := { xx | xx<:SS & xx /\ TT = {} } END; */
+ add_SS(el) = PRE el: setX & el /: SS THEN SS := SS \/ {el} END;
+ add_TT(el) = PRE el: setX & el /: TT THEN TT := TT \/ {el} END;
+ add_VV(el) = PRE el: setX & el /: VV THEN VV := VV \/ {el} END ;
+
+ set_SS_setX = BEGIN SS := setX END;
+ set_TT_setX = BEGIN TT := setX END;
+ set_VV_setX = BEGIN VV := setX END/* ;
+
+ laws_ok = PRE law1 & law2 & law3 & law4 & law5 &
+ law6 & law7 & law8 & law9 & law10 & law11 THEN skip END */
+
+END
+