From bdcd30d1a018d3ecad4a140a95fae8f0323eb348 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 30 Jul 2013 16:12:50 +0200
Subject: [PATCH] Optimized the TypeRestrictor.
---
src/main/java/de/b2tla/B2TlaTranslator.java | 3 +-
.../analysis/ConstantExpressionFinder.java | 292 ------------------
.../de/b2tla/analysis/ConstantsEvaluator.java | 56 ++--
.../analysis/IdentifierDependencies.java | 65 ++++
.../b2tla/analysis/PrecedenceCollector.java | 6 +-
.../de/b2tla/analysis/TypeRestrictor.java | 38 ++-
.../java/de/b2tla/analysis/Typechecker.java | 9 +-
src/main/java/de/b2tla/btypes/BType.java | 3 +
src/main/java/de/b2tla/btypes/BoolType.java | 6 +
.../java/de/b2tla/btypes/FunctionType.java | 23 +-
.../b2tla/btypes/IntegerOrSetOfPairType.java | 5 +
.../de/b2tla/btypes/IntegerOrSetType.java | 5 +
.../java/de/b2tla/btypes/IntegerType.java | 7 +
.../java/de/b2tla/btypes/ModelValueType.java | 13 +
src/main/java/de/b2tla/btypes/PairType.java | 27 +-
src/main/java/de/b2tla/btypes/SetType.java | 6 +
src/main/java/de/b2tla/btypes/StringType.java | 6 +
src/main/java/de/b2tla/btypes/StructType.java | 41 ++-
.../java/de/b2tla/btypes/UntypedType.java | 6 +
.../java/de/b2tla/prettyprint/TLAPrinter.java | 25 +-
src/main/java/de/b2tla/tla/Generator.java | 44 ++-
src/main/java/de/b2tla/tlc/TLCOutput.java | 13 +-
.../b2tla/prettyprint/LogicalPredicates.java | 11 +
.../java/de/b2tla/prettyprint/SetTest.java | 2 +-
.../b2tla/prettyprint/SubstitutionsTest.java | 18 ++
.../de/b2tla/tlc/integration/LawsTest.java | 14 +
.../tlc/integration/SingleConfigurations.java | 2 +-
27 files changed, 356 insertions(+), 390 deletions(-)
delete mode 100644 src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java
create mode 100644 src/main/java/de/b2tla/analysis/IdentifierDependencies.java
diff --git a/src/main/java/de/b2tla/B2TlaTranslator.java b/src/main/java/de/b2tla/B2TlaTranslator.java
index 5714910..247d2e5 100644
--- a/src/main/java/de/b2tla/B2TlaTranslator.java
+++ b/src/main/java/de/b2tla/B2TlaTranslator.java
@@ -24,6 +24,7 @@ import de.b2tla.tlc.TLCOutputInfo;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.ltl.core.parser.node.TYesterday;
public class B2TlaTranslator {
@@ -95,7 +96,7 @@ public class B2TlaTranslator {
machineContext);
Generator generator = new Generator(machineContext, typeRestrictor,
- constantsEvaluator, deferredSetSizeCalculator);
+ constantsEvaluator, deferredSetSizeCalculator, typechecker);
generator.generate();
generator.getTlaModule().sortAllDefinitions(machineContext);
diff --git a/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java b/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java
deleted file mode 100644
index c5e7731..0000000
--- a/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java
+++ /dev/null
@@ -1,292 +0,0 @@
-package de.b2tla.analysis;
-
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.List;
-
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
-import de.be4.classicalb.core.parser.node.AAnySubstitution;
-import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
-import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
-import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
-import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
-import de.be4.classicalb.core.parser.node.AExistsPredicate;
-import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.AForallPredicate;
-import de.be4.classicalb.core.parser.node.AIdentifierExpression;
-import de.be4.classicalb.core.parser.node.ALambdaExpression;
-import de.be4.classicalb.core.parser.node.AOperation;
-import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
-import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
-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.PMachineClause;
-import de.be4.classicalb.core.parser.node.Start;
-
-public class ConstantExpressionFinder extends DepthFirstAdapter {
- private MachineContext machineContext;
-
- private final int MAX_DEGREE = 20;
-
- private Hashtable<Node, Integer> constantDegree;
-
- // contains for each quantification a set of all bounded Variables
- private ArrayList<HashSet<Node>> contextTable;
-
- public boolean isconstant(Node node) {
- Integer degree = constantDegree.get(node);
- if (degree != null) {
- if (degree != 0)
- return true;
- else
- return false;
- }
- return true;
- }
-
- public ConstantExpressionFinder(Start start, MachineContext machineContext) {
- this.machineContext = machineContext;
- this.constantDegree = new Hashtable<Node, Integer>();
-
- this.contextTable = new ArrayList<HashSet<Node>>();
- contextTable.add(new HashSet<Node>(machineContext.getConstants()
- .values()));
-
- start.apply(this);
-
- }
-
- public void defaultOut(Node node) {
- Integer degree = constantDegree.get(node);
- setDegree(node.parent(), degree);
-
- }
-
- @Override
- public void caseAIdentifierExpression(AIdentifierExpression node) {
- Node refNode = machineContext.getReferences().get(node);
- if (machineContext.getConstants().values().contains(refNode)) {
- constantDegree.put(node, 19);
- defaultOut(refNode); // TODO verify
- return;
- }
- int degree = 0;
- for (int i = contextTable.size() - 1; i >= 0; i--) {
- HashSet<Node> currentScope = contextTable.get(i);
- if (currentScope.contains(refNode)) {
- constantDegree.put(node, degree);
- defaultOut(node);
- return;
- }
- degree++;
- }
- constantDegree.put(node, MAX_DEGREE);
- defaultOut(node);
-
- }
-
- private void setDegree(Node node, Integer degree) {
- if (degree != null) {
- Integer oldDegree = constantDegree.get(node);
- if (oldDegree != null) {
- constantDegree.put(node, Math.min(degree, oldDegree));
- } else {
- constantDegree.put(node, degree);
- }
- }
- }
-
- @Override
- public void caseAAbstractMachineParseUnit(AAbstractMachineParseUnit node) {
- if (node.getVariant() != null) {
- node.getVariant().apply(this);
- }
-
- if (node.getHeader() != null) {
- node.getHeader().apply(this);
- }
- {
- List<PMachineClause> copy = new ArrayList<PMachineClause>(
- node.getMachineClauses());
-
- for (PMachineClause e : copy) {
- e.apply(this);
- }
- }
- }
-
- @Override
- public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
- node.getPredicates().apply(this);
- }
-
- @Override
- public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
- List<PDefinition> copy = new ArrayList<PDefinition>(
- node.getDefinitions());
- for (PDefinition e : copy) {
- e.apply(this);
- }
- }
-
- @Override
- public void caseAPredicateDefinitionDefinition(
- APredicateDefinitionDefinition node) {
- node.getRhs().apply(this);
- }
-
- @Override
- public void caseASubstitutionDefinitionDefinition(
- ASubstitutionDefinitionDefinition node) {
- node.getRhs().apply(this);
- }
-
- @Override
- public void caseAExpressionDefinitionDefinition(
- AExpressionDefinitionDefinition node) {
- node.getRhs().apply(this);
- }
-
- @Override
- public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
- }
-
- @Override
- public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- }
-
- @Override
- public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- }
-
- @Override
- public void caseAForallPredicate(AForallPredicate node) {
- HashSet<Node> set = new HashSet<Node>();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- set.add(e);
- }
- contextTable.add(set);
- node.getImplication().apply(this);
- contextTable.remove(contextTable.size() - 1);
- Integer degree = constantDegree.get(node);
- if (degree != null) {
- constantDegree.put(node, degree - 1);
- }
- outAForallPredicate(node);
- }
-
- @Override
- public void caseAExistsPredicate(AExistsPredicate node) {
- HashSet<Node> set = new HashSet<Node>();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- set.add(e);
- }
- contextTable.add(set);
- node.getPredicate().apply(this);
- contextTable.remove(contextTable.size() - 1);
- Integer degree = constantDegree.get(node);
- if (degree != null) {
- constantDegree.put(node, degree - 1);
- }
- outAExistsPredicate(node);
- }
-
- @Override
- public void caseAAnySubstitution(AAnySubstitution node) {
- HashSet<Node> set = new HashSet<Node>();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- set.add(e);
- }
-
- contextTable.add(set);
- node.getWhere().apply(this);
- contextTable.remove(contextTable.size() - 1);
- node.getThen().apply(this);
-
- Integer degree = constantDegree.get(node);
- if (degree != null) {
- constantDegree.put(node, degree - 1);
- }
- outAAnySubstitution(node);
- }
-
- @Override
- public void caseALambdaExpression(ALambdaExpression node) {
- inALambdaExpression(node);
- HashSet<Node> set = new HashSet<Node>();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- set.add(e);
- }
- contextTable.add(set);
- if (node.getPredicate() != null) {
- node.getPredicate().apply(this);
- }
- if (node.getExpression() != null) {
- node.getExpression().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- Integer degree = constantDegree.get(node);
- if (degree != null) {
- constantDegree.put(node, degree - 1);
- }
- outALambdaExpression(node);
- }
-
- @Override
- public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
- inAComprehensionSetExpression(node);
- HashSet<Node> set = new HashSet<Node>();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- set.add(e);
- }
- contextTable.add(set);
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- Integer degree = constantDegree.get(node);
- if (degree != null) {
- constantDegree.put(node, degree - 1);
- }
- outAComprehensionSetExpression(node);
- }
-
- @Override
- public void caseAOperation(AOperation node) {
- HashSet<Node> set = new HashSet<Node>();
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getReturnValues());
- for (PExpression e : copy) {
- set.add(e);
- }
- }
-
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
- for (PExpression e : copy) {
- set.add(e);
- }
- }
- contextTable.add(set);
- node.getOperationBody().apply(this);
- contextTable.remove(contextTable.size() - 1);
- }
-
-}
diff --git a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
index bd94de3..dc1ed11 100644
--- a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
+++ b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
@@ -37,17 +37,17 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
private HashMap<Node, Integer> integerValueTable;
private final ArrayList<Node> propertiesList;
private final ArrayList<Node> invariantList;
-
+
private LinkedHashMap<Node, Node> valueOfIdentifier;
public Node getValueOfConstant(Node con) {
return valueOfIdentifier.get(con);
}
- public ArrayList<Node> getInvariantList(){
+ public ArrayList<Node> getInvariantList() {
return this.invariantList;
}
-
+
public ArrayList<Node> getPropertiesList() {
return this.propertiesList;
}
@@ -66,8 +66,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
this.machineContext = machineContext;
this.propertiesList = new ArrayList<Node>();
this.invariantList = new ArrayList<Node>();
-
-
+
ConstantsInTreeFinder constantInTreeFinder = new ConstantsInTreeFinder();
APropertiesMachineClause properties = machineContext
@@ -189,33 +188,34 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
if (constraints != null) {
analysePredicate(
((AConstraintsMachineClause) constraints)
- .getPredicates(), false);
+ .getPredicates(),
+ false);
}
Node properties = machineContext.getPropertiesMachineClause();
if (properties != null) {
analysePredicate(
- ((APropertiesMachineClause) properties).getPredicates(), true);
+ ((APropertiesMachineClause) properties).getPredicates(),
+ true);
}
-
Node invariantClause = machineContext.getInvariantMachineClause();
- if(invariantClause != null){
- analyseInvariantPredicate(((AInvariantMachineClause) invariantClause).getPredicates());
+ if (invariantClause != null) {
+ analyseInvariantPredicate(((AInvariantMachineClause) invariantClause)
+ .getPredicates());
}
}
-
-
- private void analyseInvariantPredicate(Node node){
+
+ private void analyseInvariantPredicate(Node node) {
if (node instanceof AConjunctPredicate) {
AConjunctPredicate conjunction = (AConjunctPredicate) node;
analyseInvariantPredicate(conjunction.getLeft());
analyseInvariantPredicate(conjunction.getRight());
return;
}
-
+
invariantList.add(node);
}
-
+
private void analysePredicate(Node node, boolean isProperties) {
if (node instanceof AEqualPredicate) {
analyseEqualsPredicate((AEqualPredicate) node);
@@ -280,22 +280,28 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
if (left instanceof ACardExpression) {
Node ref = machineContext.getReferences().get(
((ACardExpression) left).getExpression());
- try {
- AIntegerExpression intExpr = (AIntegerExpression) right;
- int size = Integer.parseInt(intExpr.getLiteral().getText());
- integerValueTable.put(ref, size);
- } catch (ClassCastException e) {
+ if (!machineContext.getConstants().containsValue(ref)) {
+ try {
+ AIntegerExpression intExpr = (AIntegerExpression) right;
+ int size = Integer.parseInt(intExpr.getLiteral()
+ .getText());
+ integerValueTable.put(ref, size);
+ } catch (ClassCastException e) {
+ }
}
}
if (right instanceof ACardExpression) {
Node ref = machineContext.getReferences().get(
((ACardExpression) right).getExpression());
- try {
- AIntegerExpression intExpr = (AIntegerExpression) left;
- int size = Integer.parseInt(intExpr.getLiteral().getText());
- integerValueTable.put(ref, size);
- } catch (ClassCastException e) {
+ if (!machineContext.getConstants().containsValue(ref)) {
+ try {
+ AIntegerExpression intExpr = (AIntegerExpression) left;
+ int size = Integer.parseInt(intExpr.getLiteral()
+ .getText());
+ integerValueTable.put(ref, size);
+ } catch (ClassCastException e) {
+ }
}
}
diff --git a/src/main/java/de/b2tla/analysis/IdentifierDependencies.java b/src/main/java/de/b2tla/analysis/IdentifierDependencies.java
new file mode 100644
index 0000000..ce63c85
--- /dev/null
+++ b/src/main/java/de/b2tla/analysis/IdentifierDependencies.java
@@ -0,0 +1,65 @@
+package de.b2tla.analysis;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.PMachineClause;
+
+public class IdentifierDependencies extends DepthFirstAdapter {
+
+ private final MachineContext machineContext;
+ private final HashMap<Node, HashSet<Node>> usedIdentifier;
+
+ public IdentifierDependencies(MachineContext machineContext) {
+ this.machineContext = machineContext;
+
+ this.usedIdentifier = new HashMap<Node, HashSet<Node>>();
+
+ }
+
+ public boolean containsIdentifier(Node node, HashSet<Node> list){
+ //if(!usedIdentifier.containsKey(node)){
+ node.apply(this);
+ //}
+ HashSet<Node> set = usedIdentifier.get(node);
+ for (Node id : list) {
+ if(set.contains(id))
+ return true;
+ }
+ return false;
+ }
+
+ public void defaultOut(Node node) {
+ setSetToNode(node, usedIdentifier.get(node));
+ setSetToNode(node.parent(), usedIdentifier.get(node));
+ }
+
+ @Override
+ public void caseAIdentifierExpression(AIdentifierExpression node) {
+ Node refNode = machineContext.getReferences().get(node);
+ if(refNode == null)
+ refNode = node;
+ HashSet<Node> set = new HashSet<Node>();
+ set.add(refNode);
+ setSetToNode(node, set);
+
+ defaultOut(node);
+ }
+
+ private void setSetToNode(Node node, HashSet<Node> set) {
+ HashSet<Node> oldSet = usedIdentifier.get(node);
+ if (oldSet == null) {
+ oldSet = new HashSet<Node>();
+ }
+ if (set != null) {
+ oldSet.addAll(set);
+ }
+ usedIdentifier.put(node, oldSet);
+ }
+}
diff --git a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java b/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
index 3d54381..f6dbd95 100644
--- a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
@@ -39,7 +39,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("ALessPredicate", 5, 5, false);
put("AGreaterPredicate", 5, 5, false);
put("ALessEqualPredicate", 5, 5, false);
- put("AGreaterEqualPredicate",5,5, false);
+ put("AGreaterEqualPredicate", 5, 5, false);
put("ANotEqualPredicate", 5, 5, false);
put("APowerOfExpression", 14, 14, false);
// put("ANatural1SetExpression", 8, 8, false); // NAT \ {0}
@@ -103,7 +103,9 @@ public class PrecedenceCollector extends DepthFirstAdapter {
public void inAConvertBoolExpression(AConvertBoolExpression node) {
Precedence parent = PRECEDENCES.get(node.parent().getClass()
.getSimpleName());
- precedenceTable.put(node, parent);
+ if (parent != null) {
+ precedenceTable.put(node, parent);
+ }
}
@Override
diff --git a/src/main/java/de/b2tla/analysis/TypeRestrictor.java b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
index 4a2c653..f83347a 100644
--- a/src/main/java/de/b2tla/analysis/TypeRestrictor.java
+++ b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
@@ -42,8 +42,8 @@ import de.be4.ltl.core.parser.node.AForallLtl;
public class TypeRestrictor extends DepthFirstAdapter {
private MachineContext machineContext;
- private ConstantExpressionFinder cEF;
-
+ private final IdentifierDependencies identifierDependencies;
+
private Hashtable<Node, ArrayList<NodeType>> restrictedTypesSet;
private HashSet<Node> removedNodes;
@@ -52,9 +52,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
this.machineContext = machineContext;
this.restrictedTypesSet = new Hashtable<Node, ArrayList<NodeType>>();
this.removedNodes = new HashSet<Node>();
-
- cEF = new ConstantExpressionFinder(start, machineContext);
-
+
+ this.identifierDependencies = new IdentifierDependencies(machineContext);
+
start.apply(this);
checkLTLFormulas();
@@ -120,7 +120,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
public void inAPropertiesMachineClause(APropertiesMachineClause node) {
HashSet<Node> list = new HashSet<Node>();
list.addAll(machineContext.getConstants().values());
- //analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list);
}
private void analysePredicate(Node n, HashSet<Node> list) {
@@ -130,15 +130,20 @@ public class TypeRestrictor extends DepthFirstAdapter {
PExpression right = ((AEqualPredicate) n).getRight();
Node r_right = machineContext.getReferences().get(right);
- if (list.contains(r_left) && cEF.isconstant(right)) {
+ if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
EqualsNode setNode = new EqualsNode(right);
putRestrictedType(r_left, setNode);
- removedNodes.add(n);
+ if(!machineContext.getConstants().containsValue(r_left)){
+ removedNodes.add(n);
+ }
+
}
- if (list.contains(r_right) && cEF.isconstant(left)) {
+ if (list.contains(r_right) && !identifierDependencies.containsIdentifier(left, list)) {
EqualsNode setNode = new EqualsNode(left);
putRestrictedType(r_right, setNode);
- removedNodes.add(n);
+ if(!machineContext.getConstants().containsValue(r_left)){
+ removedNodes.add(n);
+ }
}
return;
}
@@ -147,10 +152,11 @@ public class TypeRestrictor extends DepthFirstAdapter {
PExpression left = ((AMemberPredicate) n).getLeft();
Node r_left = machineContext.getReferences().get(left);
PExpression right = ((AMemberPredicate) n).getRight();
- Node r_right = machineContext.getReferences().get(right);
- if (list.contains(r_left) && cEF.isconstant(right)) {
+ if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
putRestrictedType(r_left, new ElementOfNode(right));
- removedNodes.add(n);
+ if(!machineContext.getConstants().containsValue(r_left)){
+ removedNodes.add(n);
+ }
}
return;
}
@@ -160,9 +166,11 @@ public class TypeRestrictor extends DepthFirstAdapter {
Node r_left = machineContext.getReferences().get(left);
PExpression right = ((ASubsetPredicate) n).getRight();
- if (list.contains(r_left) && cEF.isconstant(right)) {
+ if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
putRestrictedType(r_left, new SubsetNode(right));
- removedNodes.add(n);
+ if(!machineContext.getConstants().containsValue(r_left)){
+ removedNodes.add(n);
+ }
}
return;
}
diff --git a/src/main/java/de/b2tla/analysis/Typechecker.java b/src/main/java/de/b2tla/analysis/Typechecker.java
index 7ba2e0e..69fcf15 100644
--- a/src/main/java/de/b2tla/analysis/Typechecker.java
+++ b/src/main/java/de/b2tla/analysis/Typechecker.java
@@ -571,12 +571,15 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
ABecomesElementOfSubstitution node) {
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
- BType x = new SetType(new UntypedType());
+ SetType set = new SetType(new UntypedType());
+ setType(node.getSet(), set);
for (PExpression e : copy) {
- setType(e, x);
+ setType(e, set.getSubtype());
+ }
+ for (PExpression e : copy) {
+ e.apply(this);
}
- setType(node.getSet(), x);
node.getSet().apply(this);
}
diff --git a/src/main/java/de/b2tla/btypes/BType.java b/src/main/java/de/b2tla/btypes/BType.java
index ad89018..5043fab 100644
--- a/src/main/java/de/b2tla/btypes/BType.java
+++ b/src/main/java/de/b2tla/btypes/BType.java
@@ -1,9 +1,12 @@
package de.b2tla.btypes;
+import de.be4.classicalb.core.parser.node.PExpression;
+
public interface BType extends ITypeConstants{
public BType unify(BType other, ITypechecker typechecker);
public boolean isUntyped();
public boolean compare(BType other);
public String getTlaType();
public boolean containsIntegerType();
+ public PExpression createSyntaxTreeNode();
}
diff --git a/src/main/java/de/b2tla/btypes/BoolType.java b/src/main/java/de/b2tla/btypes/BoolType.java
index dd24cce..ae65354 100644
--- a/src/main/java/de/b2tla/btypes/BoolType.java
+++ b/src/main/java/de/b2tla/btypes/BoolType.java
@@ -1,6 +1,8 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.ABoolSetExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
public class BoolType implements BType {
@@ -48,4 +50,8 @@ public class BoolType implements BType {
return false;
}
+ public PExpression createSyntaxTreeNode() {
+ return new ABoolSetExpression();
+ }
+
}
diff --git a/src/main/java/de/b2tla/btypes/FunctionType.java b/src/main/java/de/b2tla/btypes/FunctionType.java
index ae5150f..6624b2e 100644
--- a/src/main/java/de/b2tla/btypes/FunctionType.java
+++ b/src/main/java/de/b2tla/btypes/FunctionType.java
@@ -1,6 +1,8 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
public class FunctionType extends AbstractHasFollowers {
private BType domain;
@@ -48,10 +50,10 @@ public class FunctionType extends AbstractHasFollowers {
} else if (other instanceof SetType
|| other instanceof IntegerOrSetType
|| other instanceof IntegerOrSetOfPairType) {
- if(domain instanceof AbstractHasFollowers){
+ if (domain instanceof AbstractHasFollowers) {
((AbstractHasFollowers) domain).deleteFollower(this);
}
- if (range instanceof AbstractHasFollowers){
+ if (range instanceof AbstractHasFollowers) {
((AbstractHasFollowers) range).deleteFollower(this);
}
SetType s = new SetType(new PairType(domain, range));
@@ -89,11 +91,12 @@ public class FunctionType extends AbstractHasFollowers {
return true;
} else if (other instanceof SetType) {
BType t = ((SetType) other).getSubtype();
- if(t instanceof PairType){
- return ((PairType) t).getFirst().compare(domain) && ((PairType) t).getSecond().compare(range);
- }else if (t instanceof UntypedType) {
+ if (t instanceof PairType) {
+ return ((PairType) t).getFirst().compare(domain)
+ && ((PairType) t).getSecond().compare(range);
+ } else if (t instanceof UntypedType) {
return true;
- } else
+ } else
return false;
}
return false;
@@ -120,7 +123,13 @@ public class FunctionType extends AbstractHasFollowers {
}
public boolean containsIntegerType() {
- return this.domain.containsIntegerType() || this.range.containsIntegerType();
+ return this.domain.containsIntegerType()
+ || this.range.containsIntegerType();
+ }
+
+ public PExpression createSyntaxTreeNode() {
+ return new ATotalFunctionExpression(domain.createSyntaxTreeNode(),
+ range.createSyntaxTreeNode());
}
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
index 01ba222..44a872f 100644
--- a/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
@@ -2,6 +2,7 @@ package de.b2tla.btypes;
import de.b2tla.exceptions.TypeErrorException;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.PExpression;
import de.hhu.stups.sablecc.patch.SourcePosition;
public class IntegerOrSetOfPairType extends AbstractHasFollowers {
@@ -229,4 +230,8 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
return false;
}
+ public PExpression createSyntaxTreeNode() {
+ return null;
+ }
+
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerOrSetType.java b/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
index 7afee5c..6a8fe02 100644
--- a/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
+++ b/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
@@ -1,6 +1,7 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.PExpression;
public class IntegerOrSetType extends AbstractHasFollowers {
@@ -60,4 +61,8 @@ public class IntegerOrSetType extends AbstractHasFollowers {
public boolean containsIntegerType() {
return false;
}
+
+ public PExpression createSyntaxTreeNode() {
+ return null;
+ }
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerType.java b/src/main/java/de/b2tla/btypes/IntegerType.java
index 5ebaae9..00b9e69 100644
--- a/src/main/java/de/b2tla/btypes/IntegerType.java
+++ b/src/main/java/de/b2tla/btypes/IntegerType.java
@@ -1,6 +1,9 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.AIntegerExpression;
+import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
public class IntegerType implements BType {
@@ -56,4 +59,8 @@ public class IntegerType implements BType {
public boolean containsIntegerType() {
return true;
}
+
+ public PExpression createSyntaxTreeNode() {
+ return new AIntegerSetExpression();
+ }
}
diff --git a/src/main/java/de/b2tla/btypes/ModelValueType.java b/src/main/java/de/b2tla/btypes/ModelValueType.java
index 55f25c3..523b7da 100644
--- a/src/main/java/de/b2tla/btypes/ModelValueType.java
+++ b/src/main/java/de/b2tla/btypes/ModelValueType.java
@@ -1,6 +1,11 @@
package de.b2tla.btypes;
+import java.util.ArrayList;
+
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class ModelValueType implements BType {
private String name;
@@ -58,4 +63,12 @@ public class ModelValueType implements BType {
public boolean containsIntegerType() {
return false;
}
+
+ public PExpression createSyntaxTreeNode() {
+ TIdentifierLiteral literal = new TIdentifierLiteral(name);
+ ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
+ idList.add(literal);
+ AIdentifierExpression id = new AIdentifierExpression(idList);
+ return id;
+ }
}
diff --git a/src/main/java/de/b2tla/btypes/PairType.java b/src/main/java/de/b2tla/btypes/PairType.java
index 77573e4..eebed18 100644
--- a/src/main/java/de/b2tla/btypes/PairType.java
+++ b/src/main/java/de/b2tla/btypes/PairType.java
@@ -1,6 +1,8 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.ACartesianProductExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
public class PairType extends AbstractHasFollowers {
@@ -30,21 +32,22 @@ public class PairType extends AbstractHasFollowers {
}
public void update(BType oldType, BType newType) {
-
+
if (this.first == oldType)
setFirst(newType);
if (this.second == oldType)
setSecond(newType);
}
+
public PairType(BType first, BType second) {
setFirst(first);
setSecond(second);
}
public BType unify(BType other, ITypechecker typechecker) {
- if(!this.compare(other) || this.contains(other))
+ if (!this.compare(other) || this.contains(other))
throw new UnificationException();
-
+
if (other instanceof PairType) {
((PairType) other).setFollowersTo(this, typechecker);
setFirst(first.unify(((PairType) other).first, typechecker));
@@ -91,15 +94,15 @@ public class PairType extends AbstractHasFollowers {
@Override
public boolean contains(BType other) {
- if(this.first.equals(other)|| this.second.equals(other)){
+ if (this.first.equals(other) || this.second.equals(other)) {
return true;
}
- if(first instanceof AbstractHasFollowers){
- if(((AbstractHasFollowers) first).contains(other))
+ if (first instanceof AbstractHasFollowers) {
+ if (((AbstractHasFollowers) first).contains(other))
return true;
}
- if(second instanceof AbstractHasFollowers){
- if(((AbstractHasFollowers) second).contains(other))
+ if (second instanceof AbstractHasFollowers) {
+ if (((AbstractHasFollowers) second).contains(other))
return true;
}
return false;
@@ -115,7 +118,13 @@ public class PairType extends AbstractHasFollowers {
}
public boolean containsIntegerType() {
- return this.first.containsIntegerType() || this.second.containsIntegerType();
+ return this.first.containsIntegerType()
+ || this.second.containsIntegerType();
+ }
+
+ public PExpression createSyntaxTreeNode() {
+ return new ACartesianProductExpression(first.createSyntaxTreeNode(),
+ second.createSyntaxTreeNode());
}
}
diff --git a/src/main/java/de/b2tla/btypes/SetType.java b/src/main/java/de/b2tla/btypes/SetType.java
index a1a4369..98d0046 100644
--- a/src/main/java/de/b2tla/btypes/SetType.java
+++ b/src/main/java/de/b2tla/btypes/SetType.java
@@ -1,6 +1,8 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.APowSubsetExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
public class SetType extends AbstractHasFollowers {
@@ -95,4 +97,8 @@ public class SetType extends AbstractHasFollowers {
return this.subtype.containsIntegerType();
}
+ public PExpression createSyntaxTreeNode() {
+ return new APowSubsetExpression(subtype.createSyntaxTreeNode());
+ }
+
}
diff --git a/src/main/java/de/b2tla/btypes/StringType.java b/src/main/java/de/b2tla/btypes/StringType.java
index 0b2d4f8..961c4a6 100644
--- a/src/main/java/de/b2tla/btypes/StringType.java
+++ b/src/main/java/de/b2tla/btypes/StringType.java
@@ -1,6 +1,8 @@
package de.b2tla.btypes;
import de.b2tla.exceptions.UnificationException;
+import de.be4.classicalb.core.parser.node.AStringSetExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
public class StringType implements BType {
@@ -53,4 +55,8 @@ public class StringType implements BType {
return false;
}
+ public PExpression createSyntaxTreeNode() {
+ return new AStringSetExpression();
+ }
+
}
diff --git a/src/main/java/de/b2tla/btypes/StructType.java b/src/main/java/de/b2tla/btypes/StructType.java
index e50bd12..56b88f6 100644
--- a/src/main/java/de/b2tla/btypes/StructType.java
+++ b/src/main/java/de/b2tla/btypes/StructType.java
@@ -1,13 +1,18 @@
- package de.b2tla.btypes;
+package de.b2tla.btypes;
+import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Set;
import de.b2tla.exceptions.UnificationException;
-
-
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.ARecEntry;
+import de.be4.classicalb.core.parser.node.AStructExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PRecEntry;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class StructType extends AbstractHasFollowers {
@@ -22,22 +27,22 @@ public class StructType extends AbstractHasFollowers {
return types.get(fieldName);
}
- public void setComplete(){
+ public void setComplete() {
complete = true;
}
-
+
public void add(String name, BType type) {
if (type instanceof AbstractHasFollowers) {
((AbstractHasFollowers) type).addFollower(this);
}
types.put(name, type);
}
-
+
@Override
public String toString() {
String res = "struct(";
Iterator<String> keys = types.keySet().iterator();
- if(!keys.hasNext())
+ if (!keys.hasNext())
res += "...";
while (keys.hasNext()) {
String fieldName = (String) keys.next();
@@ -48,7 +53,7 @@ public class StructType extends AbstractHasFollowers {
res += ")";
return res;
}
-
+
public void update(BType oldType, BType newType) {
Iterator<String> itr = this.types.keySet().iterator();
while (itr.hasNext()) {
@@ -166,7 +171,7 @@ public class StructType extends AbstractHasFollowers {
public String getTlaType() {
String res = "[";
Iterator<String> keys = types.keySet().iterator();
- if(!keys.hasNext())
+ if (!keys.hasNext())
res += "...";
while (keys.hasNext()) {
String fieldName = (String) keys.next();
@@ -180,11 +185,25 @@ public class StructType extends AbstractHasFollowers {
public boolean containsIntegerType() {
Iterator<BType> iterator = this.types.values().iterator();
- while (iterator.hasNext()){
- if(iterator.next().containsIntegerType())
+ while (iterator.hasNext()) {
+ if (iterator.next().containsIntegerType())
return true;
}
return false;
}
+ public PExpression createSyntaxTreeNode() {
+ ArrayList<PRecEntry> list = new ArrayList<PRecEntry>();
+ for (String name : types.keySet()) {
+ TIdentifierLiteral literal = new TIdentifierLiteral(name);
+ ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
+ idList.add(literal);
+ AIdentifierExpression id = new AIdentifierExpression(idList);
+ ARecEntry entry = new ARecEntry(id, types.get(name)
+ .createSyntaxTreeNode());
+ list.add(entry);
+ }
+ return new AStructExpression(list);
+ }
+
}
diff --git a/src/main/java/de/b2tla/btypes/UntypedType.java b/src/main/java/de/b2tla/btypes/UntypedType.java
index 6d25141..4ecd78b 100644
--- a/src/main/java/de/b2tla/btypes/UntypedType.java
+++ b/src/main/java/de/b2tla/btypes/UntypedType.java
@@ -1,5 +1,7 @@
package de.b2tla.btypes;
+import de.be4.classicalb.core.parser.node.PExpression;
+
public class UntypedType extends AbstractHasFollowers {
@@ -28,6 +30,10 @@ public class UntypedType extends AbstractHasFollowers {
public boolean containsIntegerType() {
return false;
}
+
+ public PExpression createSyntaxTreeNode() {
+ return null;
+ }
// @Override
// public String toString(){
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index 0c40d16..5650143 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -1415,14 +1415,14 @@ public class TLAPrinter extends DepthFirstAdapter {
}
} else {
BType t = typechecker.getType(e);
- if(t instanceof PairType && childOfCart){
+ if (t instanceof PairType && childOfCart) {
tlaModuleString.append("(");
tlaModuleString.append(t.getTlaType());
tlaModuleString.append(")");
- }else{
+ } else {
tlaModuleString.append(typechecker.getType(e).getTlaType());
}
-
+
}
}
@@ -1612,6 +1612,19 @@ public class TLAPrinter extends DepthFirstAdapter {
}
}
+ private boolean isElementOf(Node node) {
+ Node parent = node.parent();
+ if (parent instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(parent)) {
+ return true;
+ } else {
+ if (parent instanceof ATotalFunctionExpression) {
+ return isElementOf(node.parent());
+ } else
+ return false;
+ }
+ }
+
private void setOfFuntions(Node node, String funcName, String relName,
String relEleOfName, Node left, Node right) {
BType type = this.typechecker.getType(node);
@@ -1619,14 +1632,12 @@ public class TLAPrinter extends DepthFirstAdapter {
if (subtype instanceof FunctionType) {
tlaModuleString.append(funcName);
} else {
- if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.removeNode(node.parent())) {
+ if (isElementOf(node)) {
tlaModuleString.append(relEleOfName);
} else {
tlaModuleString.append(relName);
}
}
-
tlaModuleString.append("(");
left.apply(this);
tlaModuleString.append(", ");
@@ -1761,7 +1772,9 @@ public class TLAPrinter extends DepthFirstAdapter {
printIdentifierList(copy);
tlaModuleString.append(" \\in ");
for (int i = 0; i < copy.size(); i++) {
+ tlaModuleString.append("(");
printTypeOfIdentifier(copy.get(i), true);
+ tlaModuleString.append(")");
if (i < copy.size() - 1)
tlaModuleString.append(" \\times ");
}
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java
index fee1386..1b9a912 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/b2tla/tla/Generator.java
@@ -12,6 +12,9 @@ import de.b2tla.analysis.ConstantsEvaluator;
import de.b2tla.analysis.DefinitionsAnalyser;
import de.b2tla.analysis.MachineContext;
import de.b2tla.analysis.TypeRestrictor;
+import de.b2tla.analysis.Typechecker;
+import de.b2tla.analysis.nodes.NodeType;
+import de.b2tla.btypes.BType;
import de.b2tla.tla.config.ModelValueAssignment;
import de.b2tla.tla.config.SetOfModelValuesAssignment;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
@@ -23,6 +26,7 @@ import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
+import de.be4.classicalb.core.parser.node.AMemberPredicate;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
@@ -35,8 +39,10 @@ import de.be4.classicalb.core.parser.node.PPredicate;
public class Generator extends DepthFirstAdapter {
private MachineContext machineContext;
+ private TypeRestrictor typeRestrictor;
private ConstantsEvaluator constantsEvaluator;
private DefinitionsAnalyser deferredSetSizeCalculator;
+ private Typechecker typechecker;
private TLAModule tlaModule;
private ConfigFile configFile;
@@ -44,10 +50,13 @@ public class Generator extends DepthFirstAdapter {
public Generator(MachineContext machineContext,
TypeRestrictor typeRestrictor,
ConstantsEvaluator constantsEvaluator,
- DefinitionsAnalyser deferredSetSizeCalculator) {
+ DefinitionsAnalyser deferredSetSizeCalculator,
+ Typechecker typechecker) {
this.machineContext = machineContext;
+ this.typeRestrictor = typeRestrictor;
this.constantsEvaluator = constantsEvaluator;
this.deferredSetSizeCalculator = deferredSetSizeCalculator;
+ this.typechecker = typechecker;
this.tlaModule = new TLAModule();
this.configFile = new ConfigFile();
@@ -70,9 +79,11 @@ public class Generator extends DepthFirstAdapter {
}
private void evalInvariant() {
- AInvariantMachineClause invariantClause = machineContext.getInvariantMachineClause();
- if(invariantClause!= null){
- this.tlaModule.invariants.addAll(constantsEvaluator.getInvariantList());
+ AInvariantMachineClause invariantClause = machineContext
+ .getInvariantMachineClause();
+ if (invariantClause != null) {
+ this.tlaModule.invariants.addAll(constantsEvaluator
+ .getInvariantList());
this.configFile.setInvariantNumber(tlaModule.invariants.size());
}
}
@@ -201,10 +212,6 @@ public class Generator extends DepthFirstAdapter {
}
}
}
-
-
-
-
private void evalOperations() {
AOperationsMachineClause node = machineContext
@@ -251,7 +258,20 @@ public class Generator extends DepthFirstAdapter {
Integer value = constantsEvaluator.getIntValue(con);
if (value == null) {
init = true;
- this.tlaModule.variables.add(remainingConstants.get(i));
+ this.tlaModule.variables.add(con);
+ BType type = typechecker.getType(con);
+ AMemberPredicate member = new AMemberPredicate(
+ (PExpression) con.clone(),
+ type.createSyntaxTreeNode());
+
+ ArrayList<NodeType> list = this.typeRestrictor.getRestrictedTypesSet(con);
+ if (list == null || list.size() == 0) {
+ System.out.println(con);
+ tlaModule.addInit(member);
+ }else{
+
+ }
+
} else {
tlaModule.definitions.add(new TLADefinition(con, value));
}
@@ -264,14 +284,14 @@ public class Generator extends DepthFirstAdapter {
} else {
tlaModule.assumes.addAll(constantsEvaluator.getPropertiesList());
- //tlaModule.addAssume(propertiesPerdicate);
+ // tlaModule.addAssume(propertiesPerdicate);
}
}
@Override
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
if (!tlaModule.isInitPredicate(node.getPredicates())) {
- //this.tlaModule.addAssume(node.getPredicates());
+ // this.tlaModule.addAssume(node.getPredicates());
}
}
@@ -284,8 +304,6 @@ public class Generator extends DepthFirstAdapter {
}
}
-
-
@Override
public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
List<PPredicate> copy = new ArrayList<PPredicate>(node.getPredicates());
diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java
index edb4663..3040ef5 100644
--- a/src/main/java/de/b2tla/tlc/TLCOutput.java
+++ b/src/main/java/de/b2tla/tlc/TLCOutput.java
@@ -22,7 +22,8 @@ public class TLCOutput {
String parseError;
public static enum TLCResult {
- Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalProperty
+ Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError,
+ PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
}
public long getRunningTime() {
@@ -33,7 +34,7 @@ public class TLCOutput {
public String getError() {
if (error == TLCResult.InvariantViolation) {
return "Invariant Violation";
- }else if(error == TLCResult.TemporalProperty){
+ } else if (error == TLCResult.TemporalProperty) {
return "Temporal Property Violation";
}
return error.toString();
@@ -142,7 +143,7 @@ public class TLCOutput {
public static TLCResult findError(ArrayList<String> list) {
for (int i = 0; i < list.size(); i++) {
String m = list.get(i);
- if (m.startsWith("Error:")) {
+ if (m.startsWith("Error:") || m.startsWith("\"Error:")) {
return findError(m);
}
}
@@ -167,11 +168,15 @@ public class TLCOutput {
} else if (res[1].equals("Temporal")) {
return TLCResult.TemporalProperty;
} else if (m.equals("Error: TLC threw an unexpected exception.")) {
- return TLCResult.ParseError;
+ return TLCResult.TLCError;
+ } else if (m.startsWith("\"Error: Invalid function call to relation")){
+ return TLCResult.WellDefinednessError;
} else if (m.startsWith("Error: The behavior up to")) {
return null;
} else if (m.startsWith("Error: The following behavior constitutes a counter-example:")) {
return null;
+ }else if (m.startsWith("Error: The error occurred when TLC was evaluating the nested")) {
+ return null;
}
return TLCResult.TLCError;
}
diff --git a/src/test/java/de/b2tla/prettyprint/LogicalPredicates.java b/src/test/java/de/b2tla/prettyprint/LogicalPredicates.java
index 4f9b64a..2edd0b9 100644
--- a/src/test/java/de/b2tla/prettyprint/LogicalPredicates.java
+++ b/src/test/java/de/b2tla/prettyprint/LogicalPredicates.java
@@ -17,6 +17,17 @@ public class LogicalPredicates {
compare(expected, machine);
}
+ @Test
+ public void testConvert() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES TRUE = bool(1=1)" + "END";
+
+ String expected = "---- MODULE test----\n"
+ + "ASSUME TRUE = (1=1) \n"
+ + "======";
+ compare(expected, machine);
+ }
+
@Test
public void testNotEquals() throws Exception {
String machine = "MACHINE test\n"
diff --git a/src/test/java/de/b2tla/prettyprint/SetTest.java b/src/test/java/de/b2tla/prettyprint/SetTest.java
index 67e2f11..981339c 100644
--- a/src/test/java/de/b2tla/prettyprint/SetTest.java
+++ b/src/test/java/de/b2tla/prettyprint/SetTest.java
@@ -7,7 +7,7 @@ import org.junit.Ignore;
import org.junit.Test;
public class SetTest {
-
+
@Test
public void testEmptySet() throws Exception {
String machine = "MACHINE test\n"
diff --git a/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java b/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
index bbc86f8..f45c851 100644
--- a/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
+++ b/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
@@ -76,4 +76,22 @@ public class SubstitutionsTest {
+ "====";
compare(expected, machine);
}
+
+ @Test
+ public void testNotDeterministicElementOf() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x :: {1} \n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x \n"
+ + "Invariant == x = 1\n"
+ + "Init == x \\in {1}\n"
+ + "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ + "====";
+ compare(expected, machine);
+ }
}
diff --git a/src/test/java/de/b2tla/tlc/integration/LawsTest.java b/src/test/java/de/b2tla/tlc/integration/LawsTest.java
index 0c0d4f2..ae97078 100644
--- a/src/test/java/de/b2tla/tlc/integration/LawsTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/LawsTest.java
@@ -66,4 +66,18 @@ public class LawsTest {
String[] a = new String[] { "../probprivate/public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
assertEquals(NoError, B2TLA.test(a,true));
}
+
+ @Test
+ public void EqualityLaws() throws Exception {
+ B2TLAGlobals.setDeleteOnExit(true);
+ String[] a = new String[] { "../probprivate/public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
+ assertEquals(NoError, B2TLA.test(a,true));
+ }
+
+ @Test
+ public void SubsetLaws() throws Exception {
+ B2TLAGlobals.setDeleteOnExit(true);
+ String[] a = new String[] { "../probprivate/public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
+ assertEquals(NoError, B2TLA.test(a,true));
+ }
}
diff --git a/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java b/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java
index 2008db8..b12cd7a 100644
--- a/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java
+++ b/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java
@@ -18,4 +18,4 @@ public class SingleConfigurations {
// assertEquals(NoError, B2TLA.test(a));
// }
-}
+}
\ No newline at end of file
--
GitLab