diff --git a/Makefile b/Makefile index 3a797611ccacdbf8be06bb831e42f7059f7f88c9..06451129d846a5bb896a31b796d239e1b2f382fb 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,8 @@ -build/libs/TLA2B.jar: src/main/java/de/tla2b/*/*.java src/main/java/de/tla2b/*.java build.gradle +build/libs/TLA2B.jar: src/main/java/de/tla2b/*/*.java src/main/java/de/tla2b/*.java src/main/java/de/tla2bAst/*.java build.gradle gradle createJar install: build/libs/TLA2B.jar cp build/libs/TLA2B.jar ../../prob_prolog/lib/ +test: build/libs/TLA2B.jar + java -jar build/libs/TLA2B.jar $(FILE).tla + probcli $(FILE).prob -ppf user_output diff --git a/build.gradle b/build.gradle index f2199994a6bda16c054180fbe804d7ff79c14f55..a502adb65fa66286bd7ec43094307b64a427b1ff 100644 --- a/build.gradle +++ b/build.gradle @@ -4,7 +4,7 @@ apply plugin: 'maven-publish' apply plugin: 'jacoco' apply plugin: 'signing' -project.version = '1.1.4-SNAPSHOT' +project.version = '1.1.4' project.group = 'de.hhu.stups' project.archivesBaseName = "tla2bAST" final isSnapshot = project.version.endsWith("-SNAPSHOT") diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java index cf4910815a1accd168ca92b00b86afa723810971..3edbe00a488ffde83e9c51728684a86028f25fd4 100644 --- a/src/main/java/de/tla2b/analysis/BOperation.java +++ b/src/main/java/de/tla2b/analysis/BOperation.java @@ -64,7 +64,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants, .getModuleNode().getVariableDecls())); evalParams(); + // System.out.println("Construction B Operation for TLA+ action: " + name); findUnchangedVariables(); + // System.out.println(" UNCHANGED = " + unchangedVariables.toString()); separateGuardsAndBeforeAfterPredicates(node); findAssignments(); } @@ -187,19 +189,22 @@ public class BOperation extends BuiltInOPs implements ASTConstants, if (OPCODE_eq == getOpCode(opApplNode.getOperator() .getName())) { - ExprOrOpArgNode arg1 = opApplNode.getArgs()[0]; + ExprOrOpArgNode arg1 = opApplNode.getArgs()[0]; // we have equality arg1 = RHS try { OpApplNode arg11 = (OpApplNode) arg1; if (getOpCode(arg11.getOperator().getName()) == OPCODE_prime) { OpApplNode v = (OpApplNode) arg11.getArgs()[0]; SymbolNode var = v.getOperator(); + // we have equality var' = RHS if (!primedVariablesFinder .getTwiceUsedVariables().contains(var)) { - // var is only used once in all before after - // predicates + // var' is only used once in all before after predicates + // meaning we do not need it as parameter of the ANY + // and can add an assignment var := RHS assignments.put(v.getOperator(), - opApplNode.getArgs()[1]); + opApplNode.getArgs()[1]); // RHS of assignment beforeAfterPredicates.remove(node); + // System.out.println("Detected assignment " + var.getName().toString() + "' = <RHS>"); } } @@ -242,8 +247,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants, return; } default: { - if (opApplNode.level < 2) { - guards.add(node); + if (opApplNode.level < 2) { + guards.add(node); // should we be checking nonLeibnizParams is empty ? return; } else { beforeAfterPredicates.add(node); diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java index dced95d2e4027e847ba7637d76f324a87f050db8..e109115772c43f83080e7a01b67f8cb0cf699461 100644 --- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java +++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java @@ -60,7 +60,9 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons String defName = opDef.getName().toString(); // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, if (defName.equals("GOAL") || defName.startsWith("ANIMATION_FUNCTION") - || defName.startsWith("ANIMATION_IMG") || defName.startsWith("SET_PREF_")) { + || defName.startsWith("ANIMATION_IMG") + || defName.startsWith("SET_PREF_") || defName.startsWith("HEURISTIC_FUNCTION") + || defName.startsWith("SCOPE") || defName.startsWith("scope_")) { usedDefinitions.add(opDef); } } diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java index a0990034d75bb460e225557c60ca777e90d3bab5..7f603f42b8de405c1cd1e0d5233aee51bfe4d5ea 100644 --- a/src/main/java/de/tla2bAst/BAstCreator.java +++ b/src/main/java/de/tla2bAst/BAstCreator.java @@ -2187,8 +2187,8 @@ public class BAstCreator extends BuiltInOPs break; } case OPCODE_unchanged: { - // System.out.println("hier"); OpApplNode node = (OpApplNode) n.getArgs()[0]; + // System.out.println(" Translating UNCHANGED : " + node.toString()); if (node.getOperator().getKind() == VariableDeclKind) { if (!this.toplevelUnchangedVariableNames.contains(getName(node.getOperator()))) { AEqualPredicate equal = new AEqualPredicate();