From e1baa649adb23ba35d568fdeae4fd416d0135f15 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 18 Mar 2014 11:15:17 +0100
Subject: [PATCH] improved the detection & translation of restricted types
---
src/main/java/de/tlc4b/TLC4B.java | 14 +-
src/main/java/de/tlc4b/TLC4BGlobals.java | 12 +
src/main/java/de/tlc4b/Translator.java | 17 +-
.../tlc4b/analysis/PrecedenceCollector.java | 36 ++-
.../java/de/tlc4b/analysis/Typechecker.java | 35 ++-
.../tlc4b/analysis/UsedStandardModules.java | 68 +++---
.../tlc4b/analysis/nodes/ElementOfNode.java | 15 --
.../de/tlc4b/analysis/nodes/EqualsNode.java | 15 --
.../de/tlc4b/analysis/nodes/NodeType.java | 7 -
.../de/tlc4b/analysis/nodes/SubsetNode.java | 16 --
.../typerestriction/TypeRestrictor.java | 229 ++++++++++++------
.../UnchangedVariablesFinder.java | 12 +
.../java/de/tlc4b/ltl/LTLFormulaPrinter.java | 49 +++-
.../java/de/tlc4b/ltl/LTLFormulaVisitor.java | 37 +--
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 214 ++++++++--------
src/main/java/de/tlc4b/tla/Generator.java | 111 +++------
src/main/java/de/tlc4b/tla/TLAModule.java | 2 +-
src/main/java/de/tlc4b/tlc/TLCOutputInfo.java | 9 +-
src/main/java/de/tlc4b/tlc/TLCResults.java | 7 +-
.../java/de/tlc4b/analysis/ConstantsTest.java | 1 -
.../analysis/ExpressionConstantTest.java | 6 +-
.../java/de/tlc4b/analysis/ScopeTest.java | 2 +-
.../tlc4b/analysis/TypeRestrictionsTest.java | 14 +-
.../java/de/tlc4b/ltl/LtlFormulaTest.java | 27 ++-
.../de/tlc4b/prettyprint/FunctionTest.java | 4 +-
.../prettyprint/MachineParameterTest.java | 1 -
.../de/tlc4b/prettyprint/NumbersTest.java | 2 +-
.../de/tlc4b/prettyprint/OperationsTest.java | 10 +-
.../de/tlc4b/tlc/integration/LTLTest.java | 2 +-
src/test/java/de/tlc4b/util/TestUtil.java | 3 +
src/test/resources/basics/SetsTest.mch | 2 +-
src/test/resources/ltl/FairnessCounter.mch | 4 +-
32 files changed, 549 insertions(+), 434 deletions(-)
delete mode 100644 src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java
delete mode 100644 src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java
delete mode 100644 src/main/java/de/tlc4b/analysis/nodes/NodeType.java
delete mode 100644 src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 5cf711a..0fb79e7 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -33,10 +33,10 @@ public class TLC4B {
private String constantsSetup;
public static void main(String[] args) throws IOException {
- TLC4B b2tla = new TLC4B();
+ TLC4B tlc4b = new TLC4B();
try {
- b2tla.progress(args);
+ tlc4b.progress(args);
} catch (BException e) {
System.err.println("***** Parsing Error *****");
System.err.println(e.getMessage());
@@ -50,14 +50,14 @@ public class TLC4B {
if (TLC4BGlobals.isRunTLC()) {
try {
- TLCRunner.runTLC(b2tla.machineFileNameWithoutFileExtension,
- b2tla.path);
+ TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
+ tlc4b.path);
// b2tla.evalOutput(output, B2TLAGlobals.isCreateTraceFile());
// System.out.println("------------------------------");
- TLCResults results = new TLCResults(b2tla.tlcOutputInfo);
+ TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
- b2tla.printResults(results, TLC4BGlobals.isCreateTraceFile());
+ tlc4b.printResults(results, TLC4BGlobals.isCreateTraceFile());
System.exit(0);
} catch (NoClassDefFoundError e) {
@@ -168,6 +168,8 @@ public class TLC4B {
path = System.getProperty("java.io.tmpdir");
} else if (args[index].toLowerCase().equals("-noltl")) {
TLC4BGlobals.setCheckltl(false);
+ } else if (args[index].toLowerCase().equals("-lazyconstants")) {
+ TLC4BGlobals.setForceTLCToEvalConstants(false);
} else if (args[index].toLowerCase().equals("-testscript")) {
TLC4BGlobals.setRunTestscript(true);
} else if (args[index].toLowerCase().equals("-notrace")) {
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 362a7b9..f4812a2 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -23,6 +23,8 @@ public class TLC4BGlobals {
private static boolean cleanup;
+ private static boolean forceTLCToEvalConstants;
+
private static int workers;
@@ -43,6 +45,8 @@ public class TLC4BGlobals {
checkLTL = true;
checkWD= false;
+ setForceTLCToEvalConstants(true);
+
setProBconstantsSetup(false);
setCleanup(true);
@@ -206,5 +210,13 @@ public class TLC4BGlobals {
public static boolean checkWelldefinedness(){
return TLC4BGlobals.checkWD;
}
+
+ public static boolean isForceTLCToEvalConstants() {
+ return forceTLCToEvalConstants;
+ }
+
+ public static void setForceTLCToEvalConstants(boolean forceTLCToEvalConstants) {
+ TLC4BGlobals.forceTLCToEvalConstants = forceTLCToEvalConstants;
+ }
}
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 14060bf..748a6dc 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -106,8 +106,7 @@ public class Translator {
UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
machineContext);
- PrecedenceCollector precedenceCollector = new PrecedenceCollector(
- start, typechecker.getTypes(), machineContext);
+
ConstantsEliminator constantsEliminator = new ConstantsEliminator(
machineContext);
@@ -118,11 +117,10 @@ public class Translator {
TypeRestrictor typeRestrictor = new TypeRestrictor(start,
machineContext, typechecker);
- UsedStandardModules usedModules = new UsedStandardModules(typechecker,
- typeRestrictor);
- start.apply(usedModules);
- usedStandardModules = usedModules.getUsedModules();
+ PrecedenceCollector precedenceCollector = new PrecedenceCollector(
+ start, typechecker.getTypes(), machineContext, typeRestrictor);
+
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
machineContext);
@@ -132,6 +130,11 @@ public class Translator {
generator.getTlaModule().sortAllDefinitions(machineContext);
+ UsedStandardModules usedModules = new UsedStandardModules(start, typechecker,
+ typeRestrictor, generator.getTlaModule());
+
+ usedStandardModules = usedModules.getUsedModules();
+
PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
.getTlaModule().getOperations(), machineContext);
primedNodesMarker.start();
@@ -146,7 +149,7 @@ public class Translator {
configString = printer.getConfigString().toString();
tlcOutputInfo = new TLCOutputInfo(machineContext, renamer,
- typechecker.getTypes());
+ typechecker.getTypes(), generator.getTlaModule());
}
public String getMachineString() {
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index c3de071..3c535b2 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -5,10 +5,14 @@ import java.util.Hashtable;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
+import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression;
+import de.be4.classicalb.core.parser.node.AIntersectionExpression;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
+import de.be4.classicalb.core.parser.node.ASetSubtractionExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.btypes.BType;
import de.tlc4b.btypes.IntegerType;
@@ -26,10 +30,17 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("AExistsPredicate", 1, 1, false);
put("AForallPredicate", 1, 1, false);
put("AEquivalencePredicate", 2, 2, false);
- put("ADisjunctPredicate", 3, 3, true);
+ put("ADisjunctPredicate", 3, 3, true); //or
+
+ /** and **/
put("AConjunctPredicate", 3, 3, true);
- put("APreconditionSubstitution", 3, 3, true); // and
- put("AAssertionSubstitution", 3, 3, true); // and
+ put("APreconditionSubstitution", 3, 3, true);
+ put("AAssertionSubstitution", 3, 3, true);
+ put("ASelectWhenSubstitution", 3, 3, true);
+ put("AParallelSubstitution", 3, 3, true);
+
+ put("ASelectSubstitution", 3, 3, true); //and or or
+
put("AEqualPredicate", 5, 5, false);
put("ALessPredicate", 5, 5, false);
put("AGreaterPredicate", 5, 5, false);
@@ -66,7 +77,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
return brackets;
}
- public PrecedenceCollector(Start start, Hashtable<Node, BType> types, MachineContext machineContext) {
+ public PrecedenceCollector(Start start, Hashtable<Node, BType> types, MachineContext machineContext, TypeRestrictor typeRestrictor) {
precedenceTable = new Hashtable<Node, Precedence>();
brackets = new HashSet<Node>();
typeTable = types;
@@ -76,6 +87,10 @@ public class PrecedenceCollector extends DepthFirstAdapter {
machineContext.getConstantsSetup().apply(this);
}
+ for (Node node : typeRestrictor.getAllRestrictedNodes()) {
+ node.apply(this);
+ }
+
}
@Override
@@ -91,13 +106,15 @@ public class PrecedenceCollector extends DepthFirstAdapter {
Precedence p = getPrecedence(node);
if (p != null) {
precedenceTable.put(node, p);
-
- Precedence parent = precedenceTable.get(node.parent());
- if (Precedence.makeBrackets(p, parent)) {
- brackets.add(node);
+
+ if(node.parent()!= null){
+ Precedence parent = precedenceTable.get(node.parent());
+ if (Precedence.makeBrackets(p, parent)) {
+ brackets.add(node);
+ }
}
}
- // System.out.println(node.getClass().getSimpleName() + " " + p );
+ //System.out.println(node.getClass().getSimpleName() + " " + p );
}
public void inAConvertBoolExpression(AConvertBoolExpression node) {
@@ -128,6 +145,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
}
}
+ @Override
public void inAMinusOrSetSubtractExpression(
AMinusOrSetSubtractExpression node) {
BType type = typeTable.get(node);
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index e629240..7282161 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -1182,16 +1182,33 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
private boolean compareElementsOfList(ArrayList<Node> list) {
try {
- HashSet<Integer> set = new HashSet<Integer>();
- for (int i = 0; i < list.size(); i++) {
- AIntegerExpression aInt = (AIntegerExpression) list.get(i);
- int integer = Integer.parseInt(aInt.getLiteral().getText());
- set.add(integer);
- }
- if (list.size() == set.size()) {
- return true;
- }
+ if (list.get(0) instanceof AIntegerExpression) {
+ HashSet<Integer> set = new HashSet<Integer>();
+ for (int i = 0; i < list.size(); i++) {
+ AIntegerExpression aInt = (AIntegerExpression) list.get(i);
+ int integer = Integer.parseInt(aInt.getLiteral().getText());
+ set.add(integer);
+ }
+ if (list.size() == set.size()) {
+ return true;
+ }
+ } else if (list.get(0) instanceof AIdentifierExpression) {
+ HashSet<Node> set = new HashSet<Node>();
+ for (int i = 0; i < list.size(); i++) {
+ AIdentifierExpression id = (AIdentifierExpression) list
+ .get(i);
+ Node enumValue = machineContext.getReferences().get(id);
+ if (!machineContext.getEnumValues()
+ .containsValue(enumValue)) {
+ return false;
+ }
+ set.add(enumValue);
+ }
+ if (list.size() == set.size()) {
+ return true;
+ }
+ }
} catch (ClassCastException e) {
}
return false;
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 1dfc41b..57584ed 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -13,19 +13,17 @@ import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AClosureExpression;
import de.be4.classicalb.core.parser.node.ACompositionExpression;
-import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AConcatExpression;
import de.be4.classicalb.core.parser.node.ADirectProductExpression;
import de.be4.classicalb.core.parser.node.ADivExpression;
import de.be4.classicalb.core.parser.node.ADomainExpression;
import de.be4.classicalb.core.parser.node.ADomainRestrictionExpression;
import de.be4.classicalb.core.parser.node.ADomainSubtractionExpression;
-import de.be4.classicalb.core.parser.node.AExistsPredicate;
+import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AFin1SubsetExpression;
import de.be4.classicalb.core.parser.node.AFinSubsetExpression;
import de.be4.classicalb.core.parser.node.AFirstExpression;
import de.be4.classicalb.core.parser.node.AFirstProjectionExpression;
-import de.be4.classicalb.core.parser.node.AForallPredicate;
import de.be4.classicalb.core.parser.node.AFrontExpression;
import de.be4.classicalb.core.parser.node.AFunctionExpression;
import de.be4.classicalb.core.parser.node.AGeneralConcatExpression;
@@ -43,7 +41,6 @@ import de.be4.classicalb.core.parser.node.AIntervalExpression;
import de.be4.classicalb.core.parser.node.AIseq1Expression;
import de.be4.classicalb.core.parser.node.AIseqExpression;
import de.be4.classicalb.core.parser.node.AIterationExpression;
-import de.be4.classicalb.core.parser.node.ALambdaExpression;
import de.be4.classicalb.core.parser.node.ALastExpression;
import de.be4.classicalb.core.parser.node.ALessEqualPredicate;
import de.be4.classicalb.core.parser.node.ALessPredicate;
@@ -96,12 +93,16 @@ import de.be4.classicalb.core.parser.node.ATransFunctionExpression;
import de.be4.classicalb.core.parser.node.ATransRelationExpression;
import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.btypes.BType;
import de.tlc4b.btypes.FunctionType;
import de.tlc4b.btypes.IntegerType;
import de.tlc4b.btypes.SetType;
+import de.tlc4b.tla.TLAModule;
public class UsedStandardModules extends DepthFirstAdapter {
@@ -124,15 +125,25 @@ public class UsedStandardModules extends DepthFirstAdapter {
modules.add(STANDARD_MODULES.SequencesAsRelations);
}
- private Set<STANDARD_MODULES> usedStandardModules;
- private Typechecker typechecker;
- private TypeRestrictor typeRestrictor;
+ private final Set<STANDARD_MODULES> usedStandardModules;
+ private final Typechecker typechecker;
- public UsedStandardModules(Typechecker typechecker,
- TypeRestrictor typeRestrictor) {
+ public UsedStandardModules(Start start, Typechecker typechecker,
+ TypeRestrictor typeRestrictor, TLAModule tlaModule) {
this.usedStandardModules = new HashSet<STANDARD_MODULES>();
this.typechecker = typechecker;
- this.typeRestrictor = typeRestrictor;
+
+ List<PDefinition> definitions = tlaModule.getAllDefinitions();
+ if (definitions != null) {
+ for (PDefinition pDefinition : definitions) {
+ pDefinition.apply(this);
+ }
+ }
+ for (Node node : typeRestrictor.getAllRestrictedNodes()) {
+ node.apply(this);
+ }
+
+ start.apply(this);
}
class StandardModuleComparator implements Comparator<STANDARD_MODULES> {
@@ -159,35 +170,14 @@ public class UsedStandardModules extends DepthFirstAdapter {
*
*/
- private void searchForIntegerTypeinTypesOFBoundedVariables(
- List<PExpression> list) {
- for (PExpression e : list) {
- if (typeRestrictor.hasARestrictedType(e)) {
- continue;
- }
- BType t = typechecker.getType(e);
- if (t.containsIntegerType()) {
- usedStandardModules.add(STANDARD_MODULES.Integers);
- }
+ @Override
+ public void inAExpressionDefinitionDefinition(
+ AExpressionDefinitionDefinition node) {
+ if (TLC4BGlobals.isForceTLCToEvalConstants()){
+ usedStandardModules.add(STANDARD_MODULES.TLC);
}
}
- public void inAForallPredicate(AForallPredicate node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
- }
-
- public void inAExistsPredicate(AExistsPredicate node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
- }
-
- public void inALambdaExpression(ALambdaExpression node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
- }
-
- public void inAComprehensionSetExpression(AComprehensionSetExpression node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
- }
-
/**
* Naturals
*/
@@ -310,12 +300,10 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
@@ -354,13 +342,11 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inAQuantifiedIntersectionExpression(
AQuantifiedIntersectionExpression node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
- searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
- //usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ // usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
/**
diff --git a/src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java b/src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java
deleted file mode 100644
index 176ed35..0000000
--- a/src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java
+++ /dev/null
@@ -1,15 +0,0 @@
-package de.tlc4b.analysis.nodes;
-
-import de.be4.classicalb.core.parser.node.PExpression;
-
-public class ElementOfNode implements NodeType {
- PExpression expr;
-
- public ElementOfNode(PExpression expr) {
- this.expr = expr;
- }
-
- public PExpression getExpression() {
- return expr;
- }
-}
diff --git a/src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java b/src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java
deleted file mode 100644
index 774252c..0000000
--- a/src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java
+++ /dev/null
@@ -1,15 +0,0 @@
-package de.tlc4b.analysis.nodes;
-
-import de.be4.classicalb.core.parser.node.PExpression;
-
-public class EqualsNode implements NodeType {
- PExpression expr;
-
- public EqualsNode(PExpression subExpr) {
- this.expr = subExpr;
- }
-
- public PExpression getExpression() {
- return expr;
- }
-}
diff --git a/src/main/java/de/tlc4b/analysis/nodes/NodeType.java b/src/main/java/de/tlc4b/analysis/nodes/NodeType.java
deleted file mode 100644
index 336eb05..0000000
--- a/src/main/java/de/tlc4b/analysis/nodes/NodeType.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package de.tlc4b.analysis.nodes;
-
-import de.be4.classicalb.core.parser.node.PExpression;
-
-public interface NodeType {
- public PExpression getExpression();
-}
diff --git a/src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java b/src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java
deleted file mode 100644
index a83e961..0000000
--- a/src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java
+++ /dev/null
@@ -1,16 +0,0 @@
-package de.tlc4b.analysis.nodes;
-
-import de.be4.classicalb.core.parser.node.PExpression;
-
-public class SubsetNode implements NodeType{
- PExpression expr;
-
- public SubsetNode(PExpression expr){
- this.expr = expr;
- }
-
- public PExpression getExpression() {
- return expr;
- }
-
-}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 2a3c794..12a36d5 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -1,9 +1,11 @@
package de.tlc4b.analysis.typerestriction;
import java.util.ArrayList;
+import java.util.Collection;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
+import java.util.Set;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
@@ -18,16 +20,21 @@ import de.be4.classicalb.core.parser.node.AGeneralProductExpression;
import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
import de.be4.classicalb.core.parser.node.AImplicationPredicate;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
+import de.be4.classicalb.core.parser.node.AIntersectionExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
import de.be4.classicalb.core.parser.node.ALetSubstitution;
import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.ANotMemberPredicate;
import de.be4.classicalb.core.parser.node.AOperation;
+import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.APreconditionSubstitution;
import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
+import de.be4.classicalb.core.parser.node.ASetExtensionExpression;
+import de.be4.classicalb.core.parser.node.ASetSubtractionExpression;
import de.be4.classicalb.core.parser.node.ASubsetPredicate;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -37,33 +44,42 @@ import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AForallLtl;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Typechecker;
-import de.tlc4b.analysis.nodes.ElementOfNode;
-import de.tlc4b.analysis.nodes.EqualsNode;
-import de.tlc4b.analysis.nodes.NodeType;
-import de.tlc4b.analysis.nodes.SubsetNode;
+import de.tlc4b.btypes.BType;
import de.tlc4b.ltl.LTLFormulaVisitor;
public class TypeRestrictor extends DepthFirstAdapter {
- private MachineContext machineContext;
+ private final MachineContext machineContext;
private final IdentifierDependencies identifierDependencies;
+ private final Typechecker typechecker;
- private Hashtable<Node, ArrayList<NodeType>> restrictedTypesSet;
- private HashSet<Node> removedNodes;
+ private final Hashtable<Node, Node> restrictedTypeNodeTable;
+ private final HashSet<Node> removedNodes;
- public void addRemoveNode(Node node){
- this.removedNodes.add(node);
+ private final Hashtable<Node, ArrayList<Node>> restrictedNodeTable;
+ private final Hashtable<Node, ArrayList<Node>> subtractedNodeTable;
+
+ public Node getRestrictedNode(Node node) {
+ return restrictedTypeNodeTable.get(node);
+ }
+
+ public Collection<Node> getAllRestrictedNodes() {
+ return restrictedTypeNodeTable.values();
}
-
+
public TypeRestrictor(Start start, MachineContext machineContext,
Typechecker typechecker) {
this.machineContext = machineContext;
- this.restrictedTypesSet = new Hashtable<Node, ArrayList<NodeType>>();
+ this.typechecker = typechecker;
+
+ this.restrictedTypeNodeTable = new Hashtable<Node, Node>();
this.removedNodes = new HashSet<Node>();
+ this.restrictedNodeTable = new Hashtable<Node, ArrayList<Node>>();
+ this.subtractedNodeTable = new Hashtable<Node, ArrayList<Node>>();
+
this.identifierDependencies = new IdentifierDependencies(machineContext);
-
start.apply(this);
checkLTLFormulas();
@@ -82,12 +98,22 @@ public class TypeRestrictor extends DepthFirstAdapter {
HashSet<Node> list = new HashSet<Node>();
list.add(id);
analysePredicate(bNode, list, new HashSet<Node>());
+
+ PExpression e = (PExpression) id;
+ HashSet<PExpression> set = new HashSet<PExpression>();
+ set.add(e);
+ createRestrictedTypeofLocalVariables(set);
} else if (ltlNode instanceof AForallLtl) {
Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode)
.getForallIdentifier().getText());
HashSet<Node> list = new HashSet<Node>();
list.add(id);
analysePredicate(bNode, list, new HashSet<Node>());
+
+ PExpression e = (PExpression) id;
+ HashSet<PExpression> set = new HashSet<PExpression>();
+ set.add(e);
+ createRestrictedTypeofLocalVariables(set);
}
bNode.apply(this);
}
@@ -95,25 +121,28 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
}
- public ArrayList<NodeType> getRestrictedTypesSet(Node node) {
- return restrictedTypesSet.get(node);
+ public boolean isARemovedNode(Node node) {
+ return this.removedNodes.contains(node);
}
- public boolean hasARestrictedType(Node node) {
- return restrictedTypesSet.containsKey(node);
- }
+ private void putRestrictedType(Node identifier, Node expression) {
+ ArrayList<Node> list = restrictedNodeTable.get(identifier);
- public boolean removeNode(Node node) {
- return this.removedNodes.contains(node);
+ if (list == null) {
+ list = new ArrayList<Node>();
+ list.add(expression);
+ restrictedNodeTable.put(identifier, list);
+ } else {
+ list.add(expression);
+ }
}
- private void putRestrictedType(Node identifier, NodeType expression) {
- ArrayList<NodeType> list = restrictedTypesSet.get(identifier);
-
+ private void putSubstractedType(Node identifier, Node expression) {
+ ArrayList<Node> list = subtractedNodeTable.get(identifier);
if (list == null) {
- list = new ArrayList<NodeType>();
+ list = new ArrayList<Node>();
list.add(expression);
- restrictedTypesSet.put(identifier, list);
+ subtractedNodeTable.put(identifier, list);
} else {
list.add(expression);
}
@@ -122,31 +151,44 @@ public class TypeRestrictor extends DepthFirstAdapter {
@Override
public void inAConstraintsMachineClause(AConstraintsMachineClause node) {
HashSet<Node> list = new HashSet<Node>();
- list.addAll(machineContext.getSetParamter().values());
+ //list.addAll(machineContext.getSetParamter().values());
list.addAll(machineContext.getScalarParameter().values());
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ HashSet<PExpression> set = new HashSet<PExpression>();
+ for (Node param : list) {
+ set.add((PExpression) param);
+ }
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set));
}
@Override
public void inAPropertiesMachineClause(APropertiesMachineClause node) {
HashSet<Node> list = new HashSet<Node>();
list.addAll(machineContext.getConstants().values());
-
+
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ HashSet<PExpression> set = new HashSet<PExpression>();
+ for (Node con : machineContext.getConstants().values()) {
+ set.add((PExpression) con);
+ }
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set));
}
-
public void analyseDisjunktionPredicate(PPredicate node, HashSet<Node> list) {
if (node instanceof ADisjunctPredicate) {
ADisjunctPredicate dis = (ADisjunctPredicate) node;
analyseDisjunktionPredicate(dis.getLeft(), list);
analyseDisjunktionPredicate(dis.getRight(), list);
- }else{
+ } else {
analysePredicate(node, list, new HashSet<Node>());
}
}
-
- private void analysePredicate(Node n, HashSet<Node> list, HashSet<Node> ignoreList) {
+
+ private void analysePredicate(Node n, HashSet<Node> list,
+ HashSet<Node> ignoreList) {
+ if(removedNodes.contains(n))
+ return;
+
if (n instanceof AEqualPredicate) {
PExpression left = ((AEqualPredicate) n).getLeft();
Node r_left = machineContext.getReferences().get(left);
@@ -155,20 +197,17 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
- EqualsNode setNode = new EqualsNode(right);
- putRestrictedType(r_left, setNode);
- if (!machineContext.getConstants().containsValue(r_left)) {
- removedNodes.add(n);
- }
-
+ ArrayList<PExpression> element = new ArrayList<PExpression>();
+ element.add(right);
+ putRestrictedType(r_left, new ASetExtensionExpression(element));
+ removedNodes.add(n);
}
if (list.contains(r_right)
&& isAConstantExpression(right, list, ignoreList)) {
- EqualsNode setNode = new EqualsNode(left);
- putRestrictedType(r_right, setNode);
- if (!machineContext.getConstants().containsValue(r_left)) {
- removedNodes.add(n);
- }
+ ArrayList<PExpression> element = new ArrayList<PExpression>();
+ element.add(right);
+ putRestrictedType(r_right, new ASetExtensionExpression(element));
+ removedNodes.add(n);
}
return;
}
@@ -179,10 +218,20 @@ public class TypeRestrictor extends DepthFirstAdapter {
PExpression right = ((AMemberPredicate) n).getRight();
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
- putRestrictedType(r_left, new ElementOfNode(right));
- if (!machineContext.getConstants().containsValue(r_left)) {
- removedNodes.add(n);
- }
+ putRestrictedType(r_left, right);
+ removedNodes.add(n);
+ }
+ return;
+ }
+
+ if (n instanceof ANotMemberPredicate) {
+ PExpression left = ((ANotMemberPredicate) n).getLeft();
+ Node r_left = machineContext.getReferences().get(left);
+ PExpression right = ((ANotMemberPredicate) n).getRight();
+ if (list.contains(r_left)
+ && isAConstantExpression(right, list, ignoreList)) {
+ putSubstractedType(r_left, right);
+ removedNodes.add(n);
}
return;
}
@@ -194,17 +243,17 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
- putRestrictedType(r_left, new SubsetNode(right));
- if (!machineContext.getConstants().containsValue(r_left)) {
- removedNodes.add(n);
- }
+ putRestrictedType(r_left, new APowSubsetExpression(right));
+ removedNodes.add(n);
}
return;
}
if (n instanceof AConjunctPredicate) {
- analysePredicate(((AConjunctPredicate) n).getLeft(), list, ignoreList);
- analysePredicate(((AConjunctPredicate) n).getRight(), list, ignoreList);
+ analysePredicate(((AConjunctPredicate) n).getLeft(), list,
+ ignoreList);
+ analysePredicate(((AConjunctPredicate) n).getRight(), list,
+ ignoreList);
return;
}
@@ -222,16 +271,18 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
if (n instanceof APredicateParseUnit) {
- analysePredicate(((APredicateParseUnit) n).getPredicate(), list, ignoreList);
+ analysePredicate(((APredicateParseUnit) n).getPredicate(), list,
+ ignoreList);
return;
}
}
-
- public boolean isAConstantExpression(Node node, HashSet<Node> list, HashSet<Node> ignoreList){
+
+ public boolean isAConstantExpression(Node node, HashSet<Node> list,
+ HashSet<Node> ignoreList) {
HashSet<Node> newList = new HashSet<Node>();
newList.addAll(list);
newList.addAll(ignoreList);
- if(identifierDependencies.containsIdentifier(node, newList)){
+ if (identifierDependencies.containsIdentifier(node, newList)) {
return false;
}
return true;
@@ -248,6 +299,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
AImplicationPredicate implication = (AImplicationPredicate) node
.getImplication();
analysePredicate(implication.getLeft(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
@Override
@@ -259,6 +311,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
@Override
@@ -270,6 +323,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
@Override
@@ -282,6 +336,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
@Override
@@ -291,9 +346,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
node.getIdentifiers());
for (PExpression e : copy) {
list.add(e);
- // e.apply(this);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
@Override
@@ -305,6 +360,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
@@ -315,6 +371,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
@@ -325,28 +382,22 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
- private Hashtable<Node, HashSet<Node>> expectedIdentifieListTable = new Hashtable<Node, HashSet<Node>>();
+ private Hashtable<Node, HashSet<PExpression>> expectedIdentifieListTable = new Hashtable<Node, HashSet<PExpression>>();
@Override
public void caseAInitialisationMachineClause(
AInitialisationMachineClause node) {
expectedIdentifieListTable.put(node.getSubstitutions(),
- new HashSet<Node>());
+ new HashSet<PExpression>());
node.getSubstitutions().apply(this);
}
@Override
public void caseAOperation(AOperation node) {
- HashSet<Node> list = new HashSet<Node>();
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getReturnValues());
- for (PExpression e : copy) {
- list.add(e);
- }
- }
+ HashSet<PExpression> list = new HashSet<PExpression>();
{
List<PExpression> copy = new ArrayList<PExpression>(
node.getParameters());
@@ -358,24 +409,25 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (node.getOperationBody() != null) {
node.getOperationBody().apply(this);
}
+ createRestrictedTypeofLocalVariables(list);
}
@Override
public void inAPreconditionSubstitution(APreconditionSubstitution node) {
- HashSet<Node> list = getExpectedIdentifier(node);
- analysePredicate(node.getPredicate(), list, new HashSet<Node>());
+ HashSet<Node> set = new HashSet<Node>(getExpectedIdentifier(node));
+ analysePredicate(node.getPredicate(), set, new HashSet<Node>());
}
- private HashSet<Node> getExpectedIdentifier(Node node) {
- HashSet<Node> list = expectedIdentifieListTable.get(node);
+ private HashSet<PExpression> getExpectedIdentifier(Node node) {
+ HashSet<PExpression> list = expectedIdentifieListTable.get(node);
if (list == null)
- list = new HashSet<Node>();
+ list = new HashSet<PExpression>();
return list;
}
@Override
public void inASelectSubstitution(ASelectSubstitution node) {
- HashSet<Node> list = getExpectedIdentifier(node);
+ HashSet<Node> list = new HashSet<Node>(getExpectedIdentifier(node));
analysePredicate(node.getCondition(), list, new HashSet<Node>());
}
@@ -389,6 +441,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
list.addAll(getExpectedIdentifier(node));
analysePredicate(node.getWhere(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
}
@Override
@@ -401,6 +454,38 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
list.addAll(getExpectedIdentifier(node));
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ }
+
+ private void createRestrictedTypeofLocalVariables(Set<PExpression> copy) {
+ for (PExpression e : copy) {
+ PExpression tree = null;
+ ArrayList<Node> restrictedList = restrictedNodeTable.get(e);
+ if (restrictedList == null) {
+ BType conType = typechecker.getType(e);
+ tree = conType.createSyntaxTreeNode(typechecker);
+ } else {
+ tree = (PExpression) restrictedList.get(0);
+ for (int i = 1; i < restrictedList.size(); i++) {
+ PExpression n = (PExpression) restrictedList.get(i);
+ tree = new AIntersectionExpression(tree, n);
+ }
+
+ }
+ ArrayList<Node> substractedList = subtractedNodeTable.get(e);
+ if (substractedList != null) {
+ for (int i = 0; i < substractedList.size(); i++) {
+ PExpression n = (PExpression) substractedList.get(i);
+ tree = new ASetSubtractionExpression(tree, n);
+
+ }
+ }
+ this.restrictedTypeNodeTable.put(e, tree);
+ }
+ }
+
+ public void addRemoveNode(Node node) {
+ this.removedNodes.add(node);
}
}
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
index 1a51f57..6f9a66b 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
@@ -57,6 +57,18 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
public HashSet<Node> getUnchangedVariables(Node node) {
return unchangedVariablesTable.get(node);
}
+
+ public boolean hasUnchangedVariables(Node node){
+ HashSet<Node> set = unchangedVariablesTable.get(node);
+ if(set== null){
+ return false;
+ }else{
+ if(set.size() == 0){
+ return false;
+ }else
+ return true;
+ }
+ }
public HashSet<Node> getUnchangedVariablesNull(Node node) {
return unchangedVariablesNull.get(node);
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
index e466d73..a525616 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
@@ -1,8 +1,11 @@
package de.tlc4b.ltl;
-import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.Start;
import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
+import de.be4.ltl.core.parser.node.AAndFair1Ltl;
+import de.be4.ltl.core.parser.node.AAndFair2Ltl;
import de.be4.ltl.core.parser.node.AAndLtl;
import de.be4.ltl.core.parser.node.AEnabledLtl;
import de.be4.ltl.core.parser.node.AExistsLtl;
@@ -18,19 +21,24 @@ import de.be4.ltl.core.parser.node.AStrongFairLtl;
import de.be4.ltl.core.parser.node.ATrueLtl;
import de.be4.ltl.core.parser.node.AUnparsedLtl;
import de.be4.ltl.core.parser.node.AWeakFairLtl;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.prettyprint.TLAPrinter;
public class LTLFormulaPrinter extends DepthFirstAdapter {
private final LTLFormulaVisitor ltlFormulaVisitor;
private final TLAPrinter tlaPrinter;
+ private final TypeRestrictor typeRestrictor;
public LTLFormulaPrinter(TLAPrinter tlaPrinter,
- LTLFormulaVisitor ltlFormulaVisitor) {
+ LTLFormulaVisitor ltlFormulaVisitor, TypeRestrictor typeRestrictor) {
this.ltlFormulaVisitor = ltlFormulaVisitor;
this.tlaPrinter = tlaPrinter;
+ this.typeRestrictor = typeRestrictor;
+
ltlFormulaVisitor.getLTLFormulaStart().apply(this);
+
}
@Override
@@ -45,7 +53,6 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
tlaPrinter.moduleStringAppend("<>(");
node.getLtl().apply(this);
tlaPrinter.moduleStringAppend(")");
- System.out.println(node.parent().getClass());
}
@Override
@@ -69,7 +76,23 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
tlaPrinter.moduleStringAppend(" /\\ ");
node.getRight().apply(this);
}
+
+ @Override
+ public void caseAAndFair1Ltl(AAndFair1Ltl node)
+ {
+ node.getLeft().apply(this);
+ tlaPrinter.moduleStringAppend(" /\\ ");
+ node.getRight().apply(this);
+ }
+ @Override
+ public void caseAAndFair2Ltl(AAndFair2Ltl node)
+ {
+ node.getLeft().apply(this);
+ tlaPrinter.moduleStringAppend(" /\\ ");
+ node.getRight().apply(this);
+ }
+
@Override
public void caseAOrLtl(AOrLtl node) {
node.getLeft().apply(this);
@@ -122,10 +145,14 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
tlaPrinter.moduleStringAppend(" \\in ");
Node id = this.ltlFormulaVisitor.getLTLIdentifier(node
.getExistsIdentifier().getText());
- tlaPrinter.printTypeOfIdentifier((AIdentifierExpression) id, false);
+ typeRestrictor.getRestrictedNode(id).apply(tlaPrinter);
tlaPrinter.moduleStringAppend(": ");
- ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
- tlaPrinter.moduleStringAppend(" /\\ ");
+ Start start = (Start) ltlFormulaVisitor.getBAst(node);
+ APredicateParseUnit p = (APredicateParseUnit) start.getPParseUnit();
+ if(!typeRestrictor.isARemovedNode(p.getPredicate())){
+ ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
+ tlaPrinter.moduleStringAppend(" /\\ ");
+ }
node.getLtl().apply(this);
}
@@ -136,10 +163,14 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
tlaPrinter.moduleStringAppend(" \\in ");
Node id = this.ltlFormulaVisitor.getLTLIdentifier(node
.getForallIdentifier().getText());
- tlaPrinter.printTypeOfIdentifier((AIdentifierExpression) id, false);
+ typeRestrictor.getRestrictedNode(id).apply(tlaPrinter);
tlaPrinter.moduleStringAppend(": ");
- ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
- tlaPrinter.moduleStringAppend(" /\\ ");
+ Start start = (Start) ltlFormulaVisitor.getBAst(node);
+ APredicateParseUnit p = (APredicateParseUnit) start.getPParseUnit();
+ if(!typeRestrictor.isARemovedNode(p.getPredicate())){
+ ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
+ tlaPrinter.moduleStringAppend(" => ");
+ }
node.getLtl().apply(this);
}
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index 750f05a..9f9bd43 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -34,7 +34,9 @@ import de.be4.ltl.core.parser.node.AYesterdayLtl;
import de.be4.ltl.core.parser.node.PLtl;
import de.be4.ltl.core.parser.node.Start;
import de.be4.ltl.core.parser.parser.Parser;
+import de.tlc4b.analysis.Ast2String;
import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.exceptions.LTLParseException;
import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.prettyprint.TLAPrinter;
@@ -44,13 +46,29 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
private final String name;
private final Start ltlFormulaStart;
private final MachineContext machineContext;
-
+
private final LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node> ltlNodeToBNodeTable;
private final ArrayList<LTLBPredicate> bPredicates;
private final Hashtable<String, AIdentifierExpression> ltlIdentifierTable;
private ArrayList<Hashtable<String, AIdentifierExpression>> contextTable;
+
+ public LTLFormulaVisitor(String name, String ltlFormula,
+ MachineContext machineContext) {
+ this.name = name;
+ this.ltlFormulaStart = parse(ltlFormula);
+ this.machineContext = machineContext;
+
+ this.bPredicates = new ArrayList<LTLBPredicate>();
+ this.ltlNodeToBNodeTable = new LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node>();
+ this.ltlIdentifierTable = new Hashtable<String, AIdentifierExpression>();
+
+ this.contextTable = new ArrayList<Hashtable<String, AIdentifierExpression>>();
+
+ }
+
+
public ArrayList<LTLBPredicate> getBPredicates() {
return bPredicates;
}
@@ -76,19 +94,6 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return this.name;
}
- public LTLFormulaVisitor(String name, String ltlFormula,
- MachineContext machineContext) {
- this.name = name;
- this.ltlFormulaStart = parse(ltlFormula);
- this.machineContext = machineContext;
-
- this.bPredicates = new ArrayList<LTLBPredicate>();
- this.ltlNodeToBNodeTable = new LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node>();
- this.ltlIdentifierTable = new Hashtable<String, AIdentifierExpression>();
-
- this.contextTable = new ArrayList<Hashtable<String, AIdentifierExpression>>();
- }
-
public void start() {
ltlFormulaStart.apply(this);
}
@@ -97,9 +102,9 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return ltlFormulaStart;
}
- public void printLTLFormula(TLAPrinter tlaPrinter) {
+ public void printLTLFormula(TLAPrinter tlaPrinter, TypeRestrictor typeRestrictor) {
// LTLFormulaPrinter ltlFormulaPrinter =
- new LTLFormulaPrinter(tlaPrinter, this);
+ new LTLFormulaPrinter(tlaPrinter, this, typeRestrictor);
}
public static Start parse(String ltlFormula) {
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 1e6b7fe..f3d27de 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -16,9 +16,6 @@ import de.tlc4b.analysis.PrimedNodesMarker;
import de.tlc4b.analysis.Renamer;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.analysis.UsedStandardModules;
-import de.tlc4b.analysis.nodes.EqualsNode;
-import de.tlc4b.analysis.nodes.NodeType;
-import de.tlc4b.analysis.nodes.SubsetNode;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
import de.tlc4b.btypes.BType;
@@ -179,7 +176,7 @@ public class TLAPrinter extends DepthFirstAdapter {
for (int i = 0; i < visitors.size(); i++) {
LTLFormulaVisitor visitor = visitors.get(i);
tlaModuleString.append(visitor.getName() + " == ");
- visitor.printLTLFormula(this);
+ visitor.printLTLFormula(this, typeRestrictor);
tlaModuleString.append("\n");
}
}
@@ -276,11 +273,11 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append("\n");
}
- ArrayList<PDefinition> bDefinition = tlaModule.getAllDefinitions();
- if (null == bDefinition) {
+ ArrayList<PDefinition> bDefinitions = tlaModule.getAllDefinitions();
+ if (null == bDefinitions) {
return;
}
- for (PDefinition node : bDefinition) {
+ for (PDefinition node : bDefinitions) {
node.apply(this);
}
if (configFile.isGoal()) {
@@ -357,11 +354,11 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append("Init == ");
for (int i = 0; i < inits.size(); i++) {
Node init = inits.get(i);
- if(init instanceof ADisjunctPredicate){
+ if (init instanceof ADisjunctPredicate) {
tlaModuleString.append("(");
}
init.apply(this);
- if(init instanceof ADisjunctPredicate){
+ if (init instanceof ADisjunctPredicate) {
tlaModuleString.append(")");
}
if (i < inits.size() - 1)
@@ -414,7 +411,8 @@ public class TLAPrinter extends DepthFirstAdapter {
PExpression e = newList.get(i);
e.apply(this);
tlaModuleString.append(" \\in ");
- printTypeOfIdentifier(e, false);
+ typeRestrictor.getRestrictedNode(e).apply(this);
+ ;
if (i < newList.size() - 1) {
tlaModuleString.append(", ");
}
@@ -668,7 +666,7 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIfSubstitution(AIfSubstitution node) {
- if(node.getElsifSubstitutions().size() > 0){
+ if (node.getElsifSubstitutions().size() > 0) {
printElseIFSubsitution(node);
return;
}
@@ -691,8 +689,8 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(")");
printUnchangedVariables(node, true);
}
-
- private void printElseIFSubsitution(AIfSubstitution node){
+
+ private void printElseIFSubsitution(AIfSubstitution node) {
tlaModuleString.append("(CASE ");
node.getCondition().apply(this);
tlaModuleString.append(" -> ");
@@ -711,7 +709,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
tlaModuleString.append(")");
printUnchangedVariables(node, true);
-
+
}
@Override
@@ -720,7 +718,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(" -> ");
node.getThenSubstitution().apply(this);
printUnchangedVariables(node, true);
-
+
}
public void printUnchangedVariablesNull(Node node, boolean printAnd) {
@@ -747,6 +745,7 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAParallelSubstitution(AParallelSubstitution node) {
+ inAParallelSubstitution(node);
for (Iterator<PSubstitution> itr = node.getSubstitutions().iterator(); itr
.hasNext();) {
PSubstitution e = itr.next();
@@ -754,19 +753,21 @@ public class TLAPrinter extends DepthFirstAdapter {
e.apply(this);
if (itr.hasNext()) {
- tlaModuleString.append("\n\t/\\ ");
+ tlaModuleString.append(" /\\ ");
}
}
printUnchangedVariables(node, true);
+ outAParallelSubstitution(node);
}
@Override
public void caseAPreconditionSubstitution(APreconditionSubstitution node) {
inAPreconditionSubstitution(node);
-
- node.getPredicate().apply(this);
- tlaModuleString.append("\n\t/\\ ");
+ if (!typeRestrictor.isARemovedNode(node.getPredicate())) {
+ node.getPredicate().apply(this);
+ tlaModuleString.append("\n\t/\\ ");
+ }
node.getSubstitution().apply(this);
outAPreconditionSubstitution(node);
@@ -784,40 +785,54 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseASelectSubstitution(ASelectSubstitution node) {
inASelectSubstitution(node);
- tlaModuleString.append("(( ");
+ // TODO remove brackets
- tlaModuleString.append("((");
- node.getCondition().apply(this);
- tlaModuleString.append(")");
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getWhenSubstitutions());
- tlaModuleString.append(" /\\ ");
- tlaModuleString.append("(");
+ if (missingVariableFinder.hasUnchangedVariables(node)
+ && (copy.size() > 0 || node.getElse() != null)) {
+ tlaModuleString.append("(");
+ }
+ if (!typeRestrictor.isARemovedNode(node.getCondition())) {
+ if (copy.size() > 0 || node.getElse() != null) {
+ tlaModuleString.append("(");
+ }
+ node.getCondition().apply(this);
+ tlaModuleString.append(" /\\ ");
+ }
node.getThen().apply(this);
- tlaModuleString.append("))");
+ if (!typeRestrictor.isARemovedNode(node.getCondition())) {
+ if (copy.size() > 0 || node.getElse() != null) {
+ tlaModuleString.append(")");
+ }
+ }
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getWhenSubstitutions());
for (PSubstitution e : copy) {
- tlaModuleString.append("\n\t\\/ ");
+ tlaModuleString.append(" \\/ ");
e.apply(this);
}
if (node.getElse() != null) {
- tlaModuleString.append("\n\t/\\ ");
+ tlaModuleString.append(" /\\ ");
node.getElse().apply(this);
}
- tlaModuleString.append(")");
+
+ if (missingVariableFinder.hasUnchangedVariables(node)
+ && (copy.size() > 0 || node.getElse() != null)) {
+ tlaModuleString.append(")");
+ }
printUnchangedVariables(node, true);
- tlaModuleString.append(")");
+
outASelectSubstitution(node);
}
@Override
public void caseASelectWhenSubstitution(ASelectWhenSubstitution node) {
- tlaModuleString.append("(");
+ inASelectWhenSubstitution(node);
node.getCondition().apply(this);
tlaModuleString.append(" /\\ ");
node.getSubstitution().apply(this);
- tlaModuleString.append(")");
+ outASelectWhenSubstitution(node);
}
@Override
@@ -831,7 +846,8 @@ public class TLAPrinter extends DepthFirstAdapter {
PExpression e = copy.get(i);
e.apply(this);
tlaModuleString.append(" \\in ");
- printTypeOfIdentifier(e, false);
+ typeRestrictor.getRestrictedNode(e).apply(this);
+ // printTypeOfIdentifier(e, false);
if (i < copy.size() - 1) {
tlaModuleString.append(", ");
}
@@ -839,8 +855,11 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(" : ");
}
- node.getWhere().apply(this);
- tlaModuleString.append("\n\t/\\ ");
+ if (!typeRestrictor.isARemovedNode(node.getWhere())) {
+ node.getWhere().apply(this);
+ tlaModuleString.append("\n\t/\\ ");
+ }
+
node.getThen().apply(this);
printUnchangedVariables(node, true);
outAAnySubstitution(node);
@@ -857,7 +876,7 @@ public class TLAPrinter extends DepthFirstAdapter {
PExpression e = copy.get(i);
e.apply(this);
tlaModuleString.append(" \\in ");
- printTypeOfIdentifier(e, false);
+ typeRestrictor.getRestrictedNode(e).apply(this);
if (i < copy.size() - 1) {
tlaModuleString.append(", ");
}
@@ -985,8 +1004,8 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAConjunctPredicate(AConjunctPredicate node) {
- boolean left = typeRestrictor.removeNode(node.getLeft());
- boolean right = typeRestrictor.removeNode(node.getRight());
+ boolean left = typeRestrictor.isARemovedNode(node.getLeft());
+ boolean right = typeRestrictor.isARemovedNode(node.getRight());
int i = left ? (right ? 1 : 2) : (right ? 3 : 4);
switch (i) {
@@ -1021,8 +1040,10 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAImplicationPredicate(AImplicationPredicate node) {
inAImplicationPredicate(node);
- node.getLeft().apply(this);
- tlaModuleString.append(" => ");
+ if (!typeRestrictor.isARemovedNode(node.getLeft())) {
+ node.getLeft().apply(this);
+ tlaModuleString.append(" => ");
+ }
node.getRight().apply(this);
outAImplicationPredicate(node);
}
@@ -1069,7 +1090,8 @@ public class TLAPrinter extends DepthFirstAdapter {
PExpression e = copy.get(i);
e.apply(this);
tlaModuleString.append(" \\in ");
- printTypeOfIdentifier(e, false);
+ typeRestrictor.getRestrictedNode(e).apply(this);
+ ;
if (i < copy.size() - 1) {
tlaModuleString.append(", ");
}
@@ -1093,13 +1115,13 @@ public class TLAPrinter extends DepthFirstAdapter {
PExpression e = copy.get(i);
e.apply(this);
tlaModuleString.append(" \\in ");
- printTypeOfIdentifier(e, false);
+ typeRestrictor.getRestrictedNode(e).apply(this);
if (i < copy.size() - 1) {
tlaModuleString.append(", ");
}
}
tlaModuleString.append(" : ");
- if (typeRestrictor.removeNode(node.getPredicate())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicate())) {
tlaModuleString.append("TRUE");
} else {
node.getPredicate().apply(this);
@@ -1143,7 +1165,29 @@ public class TLAPrinter extends DepthFirstAdapter {
if (null == name) {
name = node.getName().getText().trim();
}
- printBDefinition(name, node.getParameters(), node.getRhs());
+ tlaModuleString.append(name);
+
+ List<PExpression> args = node.getParameters();
+ if (args.size() > 0) {
+ tlaModuleString.append("(");
+ for (int i = 0; i < args.size(); i++) {
+ if (i != 0)
+ tlaModuleString.append(", ");
+ args.get(i).apply(this);
+ }
+ tlaModuleString.append(")");
+ }
+
+ tlaModuleString.append(" == ");
+ if (TLC4BGlobals.isForceTLCToEvalConstants()) {
+ tlaModuleString.append("TLCEval(");
+ }
+ node.getRhs().apply(this);
+ if (TLC4BGlobals.isForceTLCToEvalConstants()) {
+ tlaModuleString.append(")");
+ }
+ tlaModuleString.append("\n");
+ // printBDefinition(name, node.getParameters(), node.getRhs());
}
@Override
@@ -1388,7 +1432,7 @@ public class TLAPrinter extends DepthFirstAdapter {
printIdentifierList(copy);
tlaModuleString.append(" \\in ");
- if (typeRestrictor.removeNode(node.getPredicates())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicates())) {
printTypesOfIdentifierList(copy);
} else {
tlaModuleString.append("{");
@@ -1420,7 +1464,7 @@ public class TLAPrinter extends DepthFirstAdapter {
printIdentifierList(copy);
tlaModuleString.append(" \\in ");
- if (typeRestrictor.removeNode(node.getPredicates())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicates())) {
printTypesOfIdentifierList(copy);
} else {
tlaModuleString.append("{");
@@ -1478,51 +1522,13 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(">>");
}
- public void printTypeOfIdentifier(PExpression e, boolean childOfCart) {
- // NodeType n = typeRestrictor.getRestrictedTypes().get(e);
- ArrayList<NodeType> list = typeRestrictor.getRestrictedTypesSet(e);
- if (list != null) {
- for (int i = 0; i < list.size(); i++) {
- if (i != 0)
- tlaModuleString.append(" \\cap (");
- printNodeType(list.get(i));
- if (i != 0)
- tlaModuleString.append(")");
- }
- } else {
- BType t = typechecker.getType(e);
- if (t instanceof PairType && childOfCart) {
- tlaModuleString.append("(");
- tlaModuleString.append(t.getTlaType());
- tlaModuleString.append(")");
- } else {
- tlaModuleString.append(typechecker.getType(e).getTlaType());
- }
-
- }
- }
-
- private void printNodeType(NodeType n) {
- if (n instanceof EqualsNode) {
- tlaModuleString.append("{");
- n.getExpression().apply(this);
- tlaModuleString.append("}");
- } else if (n instanceof SubsetNode) {
- tlaModuleString.append("SUBSET(");
- n.getExpression().apply(this);
- tlaModuleString.append(")");
- } else {
- n.getExpression().apply(this);
- }
- }
-
private void printTypesOfIdentifierList(List<PExpression> copy) {
if (copy.size() > 1) {
tlaModuleString.append("(");
}
for (int i = 0; i < copy.size(); i++) {
tlaModuleString.append("(");
- printTypeOfIdentifier(copy.get(i), false);
+ typeRestrictor.getRestrictedNode(copy.get(i)).apply(this);
tlaModuleString.append(")");
if (i < copy.size() - 1)
tlaModuleString.append(" \\times ");
@@ -1557,7 +1563,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(" \\in ");
- if (typeRestrictor.removeNode(node.getPredicate())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicate())) {
printTypesOfIdentifierList(copy);
} else {
tlaModuleString.append("{");
@@ -1577,7 +1583,7 @@ public class TLAPrinter extends DepthFirstAdapter {
printIdentifierList(copy);
tlaModuleString.append(" \\in ");
- if (typeRestrictor.removeNode(node.getPredicate())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicate())) {
printTypesOfIdentifierList(copy);
} else {
@@ -1616,13 +1622,13 @@ public class TLAPrinter extends DepthFirstAdapter {
}
tlaModuleString.append("]");
} else {
-
- if(TLC4BGlobals.checkWelldefinedness()){
+
+ if (TLC4BGlobals.checkWelldefinedness()) {
tlaModuleString.append(REL_CALL + "(");
- }else{
+ } else {
tlaModuleString.append(REL_CALL_WITHOUT_WD_CHECK + "(");
}
-
+
node.getIdentifier().apply(this);
tlaModuleString.append(", ");
List<PExpression> copy = new ArrayList<PExpression>(
@@ -1681,7 +1687,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append("]");
} else {
if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.removeNode(node.parent())) {
+ && !typeRestrictor.isARemovedNode(node.parent())) {
tlaModuleString.append(REL_TOTAL_FUNCTION_ELEMENT_OF);
} else {
tlaModuleString.append(REL_TOTAL_FUNCTION);
@@ -1697,7 +1703,7 @@ public class TLAPrinter extends DepthFirstAdapter {
private boolean isElementOf(Node node) {
Node parent = node.parent();
if (parent instanceof AMemberPredicate
- && !typeRestrictor.removeNode(parent)
+ && !typeRestrictor.isARemovedNode(parent)
// && !this.tlaModule.getInitPredicates().contains(parent)
) {
return true;
@@ -1761,7 +1767,7 @@ public class TLAPrinter extends DepthFirstAdapter {
if (subtype instanceof FunctionType) {
Node parent = node.parent();
if (parent instanceof AMemberPredicate
- && !typeRestrictor.removeNode(parent)
+ && !typeRestrictor.isARemovedNode(parent)
// && !this.tlaModule.getInitPredicates().contains(parent)
) {
AMemberPredicate member = (AMemberPredicate) parent;
@@ -1885,7 +1891,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(" \\in ");
printTypesOfIdentifierList(copy);
tlaModuleString.append(": ");
- if (typeRestrictor.removeNode(node.getPredicates())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicates())) {
tlaModuleString.append("TRUE");
} else {
node.getPredicates().apply(this);
@@ -1901,13 +1907,13 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(" \\in ");
for (int i = 0; i < copy.size(); i++) {
tlaModuleString.append("(");
- printTypeOfIdentifier(copy.get(i), true);
+ typeRestrictor.getRestrictedNode(copy.get(i)).apply(this);
tlaModuleString.append(")");
if (i < copy.size() - 1)
tlaModuleString.append(" \\times ");
}
tlaModuleString.append(": ");
- if (typeRestrictor.removeNode(node.getPredicates())) {
+ if (typeRestrictor.isARemovedNode(node.getPredicates())) {
tlaModuleString.append("TRUE");
} else {
node.getPredicates().apply(this);
@@ -2005,13 +2011,17 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseASubsetPredicate(ASubsetPredicate node) {
+ if (node.getRight() == null) {
+ tlaModuleString.append("TRUE");
+ return;
+ }
+
inASubsetPredicate(node);
node.getLeft().apply(this);
tlaModuleString.append(" \\in SUBSET(");
// tlaModuleString.append(" \\subseteq ");
node.getRight().apply(this);
tlaModuleString.append(")");
-
outASubsetPredicate(node);
}
@@ -2493,7 +2503,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
} else {
if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.removeNode(node.parent())) {
+ && !typeRestrictor.isARemovedNode(node.parent())) {
tlaModuleString.append(INJECTIVE_SEQUENCE_ELEMENT_OF);
} else {
tlaModuleString.append(INJECTIVE_SEQUENCE);
@@ -2511,7 +2521,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
} else {
if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.removeNode(node.parent())) {
+ && !typeRestrictor.isARemovedNode(node.parent())) {
tlaModuleString.append(INJECTIVE_SEQUENCE_1_ELEMENT_OF);
} else {
tlaModuleString.append(INJECTIVE_SEQUENCE_1);
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index 1e7d059..a7a117d 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -31,10 +31,7 @@ import de.tlc4b.analysis.ConstantsEvaluator;
import de.tlc4b.analysis.DefinitionsAnalyser;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Typechecker;
-import de.tlc4b.analysis.nodes.ElementOfNode;
-import de.tlc4b.analysis.nodes.NodeType;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
-import de.tlc4b.btypes.BType;
import de.tlc4b.tla.config.ModelValueAssignment;
import de.tlc4b.tla.config.SetOfModelValuesAssignment;
@@ -44,7 +41,6 @@ public class Generator extends DepthFirstAdapter {
private TypeRestrictor typeRestrictor;
private ConstantsEvaluator constantsEvaluator;
private DefinitionsAnalyser deferredSetSizeCalculator;
- private Typechecker typechecker;
private TLAModule tlaModule;
private ConfigFile configFile;
@@ -58,7 +54,6 @@ public class Generator extends DepthFirstAdapter {
this.typeRestrictor = typeRestrictor;
this.constantsEvaluator = constantsEvaluator;
this.deferredSetSizeCalculator = deferredSetSizeCalculator;
- this.typechecker = typechecker;
this.tlaModule = new TLAModule();
this.configFile = new ConfigFile();
@@ -153,6 +148,11 @@ public class Generator extends DepthFirstAdapter {
continue;
}
+ Node restrictedNode = typeRestrictor.getRestrictedNode(param);
+ AMemberPredicate memberPredicate = new AMemberPredicate(
+ (PExpression) param, (PExpression) restrictedNode);
+ tlaModule.addInit(memberPredicate);
+
init = true;
this.tlaModule.variables.add(param);
}
@@ -161,9 +161,13 @@ public class Generator extends DepthFirstAdapter {
.getConstraintMachineClause();
if (init) {
configFile.setInit();
- tlaModule.addInit(clause.getPredicates());
+ if (!typeRestrictor.isARemovedNode(clause.getPredicates())) {
+ tlaModule.addInit(clause.getPredicates());
+ }
+
} else {
- tlaModule.addAssume(clause.getPredicates());
+ if (!typeRestrictor.isARemovedNode(clause.getPredicates()))
+ tlaModule.addAssume(clause.getPredicates());
}
}
@@ -238,7 +242,7 @@ public class Generator extends DepthFirstAdapter {
while (cons.hasNext()) {
AIdentifierExpression con = (AIdentifierExpression) cons.next();
Node value = conValueTable.get(con);
- //tlaModule.definitions.add(new TLADefinition(con, value));
+ // tlaModule.definitions.add(new TLADefinition(con, value));
AExpressionDefinitionDefinition exprDef = new AExpressionDefinitionDefinition(
con.getIdentifier().get(0), new LinkedList<PExpression>(),
@@ -251,104 +255,60 @@ public class Generator extends DepthFirstAdapter {
ArrayList<Node> remainingConstants = new ArrayList<Node>();
remainingConstants.addAll(machineContext.getConstants().values());
remainingConstants.removeAll(conValueTable.keySet());
-
+
Node propertiesPerdicate = machineContext.getPropertiesMachineClause()
.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){
+
+ 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);
+ 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;
-
- ArrayList<NodeType> a = typeRestrictor.getRestrictedTypesSet(con);
- if(a != null && a.size() > 0 ){
- for (int j = 0; j < a.size(); j++) {
- NodeType type = a.get(j);
- if(type instanceof ElementOfNode){
- Node parent = type.getExpression().parent();
- typeRestrictor.addRemoveNode(parent);
- tlaModule.addInit(parent);
- }
- continue;
- }
-
- }
-
- BType conType = typechecker.getType(con);
-
- if (!conType.containsIntegerType()) {
- PExpression n = conType
- .createSyntaxTreeNode(typechecker);
- AMemberPredicate member = new AMemberPredicate(
- (PExpression) con.clone(), n);
-
- ArrayList<NodeType> list = this.typeRestrictor
- .getRestrictedTypesSet(con);
- if (list == null || list.size() == 0) {
- tlaModule.addInit(member);
- } else {
- for (int j = 0; j < list.size(); j++) {
- NodeType val = list.get(j);
- if(val instanceof ElementOfNode){
- Node eleOfNode = val.getExpression().parent();
- tlaModule.addInit(eleOfNode);
- this.typeRestrictor.addRemoveNode(eleOfNode);
- }
- }
- }
- }
- } else {
- //tlaModule.definitions.add(new TLADefinition(con, value));
- }
+ Node restrictedNode = typeRestrictor.getRestrictedNode(con);
+ AMemberPredicate memberPredicate = new AMemberPredicate(
+ (PExpression) con, (PExpression) restrictedNode);
+ tlaModule.addInit(memberPredicate);
}
-
- if(numberOfIteratedConstants > 1){
+
+ if (numberOfIteratedConstants > 1) {
tlaModule.addInit(machineContext.getConstantsSetup());
}
-
-
+
if (init) {
configFile.setInit();
- tlaModule.addInit(propertiesPerdicate);
+ if (!typeRestrictor.isARemovedNode(propertiesPerdicate))
+ tlaModule.addInit(propertiesPerdicate);
}
-
-
} else {
tlaModule.assumes.addAll(constantsEvaluator.getPropertiesList());
// tlaModule.addAssume(propertiesPerdicate);
}
-
-
-
+
}
@Override
- public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
+ public void inAPropertiesMachineClause(APropertiesMachineClause node) {
if (!tlaModule.isInitPredicate(node.getPredicates())) {
// this.tlaModule.addAssume(node.getPredicates());
}
@@ -364,7 +324,7 @@ public class Generator extends DepthFirstAdapter {
}
@Override
- public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
+ public void inAAssertionsMachineClause(AAssertionsMachineClause node) {
List<PPredicate> copy = new ArrayList<PPredicate>(node.getPredicates());
for (PPredicate e : copy) {
this.tlaModule.addAssertion(e);
@@ -373,8 +333,7 @@ public class Generator extends DepthFirstAdapter {
}
@Override
- public void caseAInitialisationMachineClause(
- AInitialisationMachineClause node) {
+ public void inAInitialisationMachineClause(AInitialisationMachineClause node) {
this.configFile.setInit();
this.tlaModule.addInit(node.getSubstitutions());
}
diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
index 702aad7..4eb277c 100644
--- a/src/main/java/de/tlc4b/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -1,7 +1,6 @@
package de.tlc4b.tla;
import java.util.ArrayList;
-
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.POperation;
@@ -36,6 +35,7 @@ public class TLAModule {
this.invariants = new ArrayList<Node>();
this.allDefinitions = new ArrayList<PDefinition>();
+
}
public void sortAllDefinitions(MachineContext machineContext){
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 2bc5956..25b95a4 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -9,6 +9,7 @@ import de.be4.classicalb.core.parser.node.Node;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Renamer;
import de.tlc4b.btypes.BType;
+import de.tlc4b.tla.TLAModule;
public class TLCOutputInfo {
@@ -16,6 +17,11 @@ public class TLCOutputInfo {
Hashtable<String, BType> typesTable;
Set<String> constants;
boolean constantSetup= false;
+ private boolean init= false;
+
+ public boolean hasInitialisation(){
+ return init;
+ }
public String getBName(String tlaName){
return namesMapping.get(tlaName);
@@ -42,11 +48,12 @@ public class TLCOutputInfo {
}
public TLCOutputInfo(MachineContext machineContext, Renamer renamer,
- Hashtable<Node, BType> types) {
+ Hashtable<Node, BType> types, TLAModule tlaModule) {
namesMapping = new Hashtable<String, String>();
typesTable = new Hashtable<String, BType>();
constants = machineContext.getConstants().keySet();
+ init = tlaModule.getInitPredicates().size()>0;
if(machineContext.getConstantsMachineClause() != null){
this.constantSetup = true;
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 71dabb6..924e15b 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -26,7 +26,7 @@ public class TLCResults {
private TLCOutputInfo tlcOutputInfo;
public static enum TLCResult {
- Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerationError, TLCError, TemporalPropertyViolation, WellDefinednessError;
+ Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerationError, TLCError, TemporalPropertyViolation, WellDefinednessError, InitialStateError;
}
public boolean hasTrace() {
@@ -64,6 +64,11 @@ public class TLCResults {
evalTrace();
}
+ if(tlcResult == NoError & tlcOutputInfo.hasInitialisation() & numberOfDistinctStates == 0){
+ // Can not setup constants
+ tlcResult = InitialStateError;
+ }
+
}
private void evalTrace() {
diff --git a/src/test/java/de/tlc4b/analysis/ConstantsTest.java b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
index f74c1a9..7cf4e94 100644
--- a/src/test/java/de/tlc4b/analysis/ConstantsTest.java
+++ b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
@@ -106,7 +106,6 @@ public class ConstantsTest {
compare(expected, machine);
}
-
@Test
public void testConstants2() throws Exception {
String machine = "MACHINE test\n"
diff --git a/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
index 1efa162..51083fe 100644
--- a/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
+++ b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
@@ -14,7 +14,7 @@ public class ExpressionConstantTest {
String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+ "k == 1 \n"
- + "ASSUME \\A x \\in {k} : x = k => 1 = 1 \n"
+ + "ASSUME \\A x \\in {k} : 1 = 1 \n"
+ "======";
compare(expected, machine);
}
@@ -38,7 +38,7 @@ public class ExpressionConstantTest {
+ "PROPERTIES !x.(x = 1 => !y.(y= x => 1 = 1))\n" + "END";
String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
- + "ASSUME \\A x \\in {1} : x = 1 => \\A y \\in {x} : y = x => 1 = 1 \n"
+ + "ASSUME \\A x \\in {1} : \\A y \\in {x} : 1 = 1 \n"
+ "======";
compare(expected, machine);
}
@@ -50,7 +50,7 @@ public class ExpressionConstantTest {
String expected = "---- MODULE test----\n"
+ "EXTENDS Integers \n"
- + "ASSUME \\A x \\in (-1..4), y \\in {1} : x = y => 1 = 1 \n"
+ + "ASSUME \\A x \\in Int, y \\in {1} : x = y => 1 = 1 \n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/analysis/ScopeTest.java b/src/test/java/de/tlc4b/analysis/ScopeTest.java
index 77fab20..7ab79c9 100644
--- a/src/test/java/de/tlc4b/analysis/ScopeTest.java
+++ b/src/test/java/de/tlc4b/analysis/ScopeTest.java
@@ -68,7 +68,7 @@ public class ScopeTest {
}
@Test
- public void testInvariantConstatnParameter() throws Exception {
+ public void testInvariantConstantParameter() throws Exception {
String machine = "MACHINE test\n" + "CONSTANTS k \n"
+ "PROPERTIES k = 1" + "INVARIANT k = 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 bd5ee36..174c601 100644
--- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
+++ b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
@@ -17,7 +17,6 @@ public class TypeRestrictionsTest {
compare(expected, machine);
}
-
@Test
public void testExistentielQuantification() throws Exception {
String machine = "MACHINE test\n"
@@ -80,7 +79,7 @@ public class TypeRestrictionsTest {
+ "PROPERTIES #x,y.(x = 1 & x = y) \n" + "END";
String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
- + "ASSUME \\E x \\in {1}, y \\in -1..4: x = y \n"
+ + "ASSUME \\E x \\in {1}, y \\in Int: x = y \n"
+ "======";
compare(expected, machine);
}
@@ -97,7 +96,7 @@ public class TypeRestrictionsTest {
}
@Test
- public void testSetComprehension2VariablesConstant() throws Exception {
+ public void testExist2VariablesConstant() throws Exception {
String machine = "MACHINE test\n"
+ "CONSTANTS k \n"
+ "PROPERTIES k = 1 & #x,y.(x = 1 & y = k + 1)\n" + "END";
@@ -141,7 +140,7 @@ public class TypeRestrictionsTest {
String expected = "---- MODULE test ----\n" + "EXTENDS Integers\n"
+ "k == 1 \n"
- + "ASSUME \\A x \\in {k} : x = k => 1 = 1 \n"
+ + "ASSUME \\A x \\in {k} : 1 = 1 \n"
+ "====";
compare(expected, machine);
}
@@ -154,7 +153,7 @@ public class TypeRestrictionsTest {
String expected = "---- MODULE test ----\n" + "EXTENDS Integers\n"
+ "k == 1 \n"
- + "ASSUME \\A x \\in {k} : x = k => 1 = 1 \n"
+ + "ASSUME \\A x \\in {k} : 1 = 1 \n"
+ "====";
compare(expected, machine);
}
@@ -177,7 +176,7 @@ public class TypeRestrictionsTest {
+ "k == 1 .. 4\n"
+ "Invariant == x = 1\n"
+ "Init == x = 1 \n"
- + "foo(a) == a \\in k /\\ x' = a\n"
+ + "foo(a) == x' = a\n"
+ "Next == \\E a \\in k: foo(a) \n"
+ "====";
compare(expected, machine);
@@ -196,7 +195,6 @@ public class TypeRestrictionsTest {
}
-
@Test
public void testExistDependingVariables() throws Exception {
String machine = "MACHINE test\n"
@@ -205,7 +203,7 @@ public class TypeRestrictionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Integers \n"
- + "ASSUME \\E x \\in {1}, y \\in -1..4 : y = x \n"
+ + "ASSUME \\E x \\in {1}, y \\in Int : y = x \n"
+ "====";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
index e4915b7..44e14d9 100644
--- a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
@@ -13,8 +13,6 @@ import de.tlc4b.exceptions.TypeErrorException;
public class LtlFormulaTest {
-
-
@Test (expected = ScopeException.class)
public void testScopeException() throws Exception {
String machine = "MACHINE test\n"
@@ -283,27 +281,46 @@ public class LtlFormulaTest {
compareLTL(expected, machine, "SF(foo)");
}
-
@Test
public void testExistentialQuantification() throws Exception {
String machine = "MACHINE test\n"
+ "END";
String expected = "---- MODULE test ----\n"
- + "ltl == \\E p \\in {1}: p = 1 /\\ p = 1\n"
+ + "ltl == \\E p \\in {1}: p = 1\n"
+ "====";
compareLTL(expected, machine, "#p.({p=1} & {p = 1})");
}
+ @Test
+ public void testExistentialQuantification2() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ String expected = "---- MODULE test ----\n"
+ + "ltl == \\E p \\in {1}: 1 = 1 /\\ p = 1\n"
+ + "====";
+ compareLTL(expected, machine, "#p.({p=1 & 1 = 1} & {p = 1})");
+ }
+
@Test
public void testForallQuantification() throws Exception {
String machine = "MACHINE test\n"
+ "END";
String expected = "---- MODULE test ----\n"
- + "ltl == \\A p \\in {1}: p = 1 /\\ p = 1\n"
+ + "ltl == \\A p \\in {1}: p = 1\n"
+ "====";
compareLTL(expected, machine, "!p.({p=1} => {p = 1})");
}
+ @Test
+ public void testForallQuantification2() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ String expected = "---- MODULE test ----\n"
+ + "ltl == \\A p \\in {1}: 1 = 1 => p = 1\n"
+ + "====";
+ compareLTL(expected, machine, "!p.({p=1 & 1=1 } => {p = 1})");
+ }
+
@Ignore
@Test
public void testLTLFormulaInDefinitions() throws Exception {
diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
index 815d684..e4587e0 100644
--- a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
@@ -50,7 +50,7 @@ public class FunctionTest {
+ "END";
String expected = "---- MODULE test ----\n"
+ "EXTENDS Integers\n"
- + "ASSUME 4 = [<<a, b>> \\in { <<a, b>> \\in ((-1..4) \\times (-1..4)) : a = b} |-> a + b][2, 2]\n"
+ + "ASSUME 4 = [<<a, b>> \\in { <<a, b>> \\in ((Int) \\times (Int)) : a = b} |-> a + b][2, 2]\n"
+ "====";
compare(expected, machine);
}
@@ -63,7 +63,7 @@ public class FunctionTest {
+ "END";
String expected = "---- MODULE test ----\n"
+ "EXTENDS Integers\n"
- + "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in ((-1..4) \\times (-1..4)) : a = b}}\n"
+ + "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in ((Int) \\times (Int)) : a = b}}\n"
+ "====";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
index feb7404..de03a6e 100644
--- a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
@@ -14,7 +14,6 @@ public class MachineParameterTest {
String expected = "---- MODULE test----\n"
+ "a == 1\n"
- + "ASSUME a = 1\n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/NumbersTest.java b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
index d3c079b..08e5952 100644
--- a/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
@@ -256,7 +256,7 @@ public class NumbersTest {
+ "END";
String expected = "---- MODULE test----\n"
+ "EXTENDS Integers\n"
- + "ASSUME {x \\in (-1..4): 1 = 1 => x = 1} = {}\n"
+ + "ASSUME {x \\in (Int): 1 = 1 => x = 1} = {}\n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
index b4339ec..53eec85 100644
--- a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
@@ -146,7 +146,7 @@ public class OperationsTest {
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Init == x = 1 \n"
- + "foo(p) == p = 1 /\\ x' = p\n"
+ + "foo(p) == x' = p\n"
+ "Next == \\E p \\in {1} : foo(p)\n"
+ "====";
compare(expected, machine);
@@ -166,7 +166,7 @@ public class OperationsTest {
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Init == x = 1 \n"
- + "foo == \\E p \\in {1} : p = 1 /\\ x' = p\n"
+ + "foo == \\E p \\in {1} : x' = p\n"
+ "Next == foo\n"
+ "====";
compare(expected, machine);
@@ -270,7 +270,7 @@ public class OperationsTest {
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Init == x = 1 \n"
- + "foo(a) == a = 1 /\\ x' = a\n"
+ + "foo(a) == x' = a\n"
+ "Next == \\E a \\in {1}: foo(a) \n"
+ "====";
compare(expected, machine);
@@ -373,8 +373,8 @@ public class OperationsTest {
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
+ "Init == x = 1 /\\ y = 1\n"
- + "foo == x = 1 /\\ (( ((x = 1) /\\ (x' = 1))\n"
- + "\\/ (x = 2 /\\ UNCHANGED <<x>>))) /\\ y' = 1\n"
+ + "foo == x = 1 \n"
+ + "/\\ (((x = 1 /\\ x' = 1) \\/ (x = 2 /\\ UNCHANGED <<x>>)) /\\ y' = 1)\n"
+ "Next == foo \n"
+ "====";
compare(expected, machine);
diff --git a/src/test/java/de/tlc4b/tlc/integration/LTLTest.java b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
index bf2d1d4..a17f149 100644
--- a/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
@@ -31,7 +31,7 @@ public class LTLTest {
@Test
public void testFairnessCounterLTL() throws Exception {
String[] a = new String[] { ".\\src\\test\\resources\\ltl\\FairnessCounter.mch" };
- assertEquals(TemporalPropertyViolation, test(a));
+ assertEquals(NoError, test(a));
}
@Test
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 4a4e079..c3bb57a 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -19,6 +19,7 @@ import java.util.List;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.TLC4BGlobals;
import de.tlc4b.Translator;
import de.tlc4b.analysis.Ast2String;
import de.tlc4b.tlc.TLCResults.TLCResult;
@@ -27,6 +28,8 @@ public class TestUtil {
public static void compare(String expectedModule, String machine)
throws Exception {
+ TLC4BGlobals.setForceTLCToEvalConstants(false);
+
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
diff --git a/src/test/resources/basics/SetsTest.mch b/src/test/resources/basics/SetsTest.mch
index 66aca59..615e487 100644
--- a/src/test/resources/basics/SetsTest.mch
+++ b/src/test/resources/basics/SetsTest.mch
@@ -3,6 +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} }
+& (1,TRUE,2) : {a,b,c | a : {1} & b : {TRUE} & c : {2}}
& UNION(z).(z: {1,2} & 1 = 1| {z}) = {1,2}
END
\ No newline at end of file
diff --git a/src/test/resources/ltl/FairnessCounter.mch b/src/test/resources/ltl/FairnessCounter.mch
index 86ca009..b904c71 100644
--- a/src/test/resources/ltl/FairnessCounter.mch
+++ b/src/test/resources/ltl/FairnessCounter.mch
@@ -1,6 +1,6 @@
-MACHINE CounterLTL
+MACHINE FairnessCounter
DEFINITIONS
-ASSERT_LTL_1 == "SF(Reset) => F {x = 0}"
+ASSERT_LTL_1 == "WF(Reset) & WF(Inc) => F {x = 0}"
VARIABLES x
INVARIANT
x : 0..20
--
GitLab