diff --git a/build.gradle b/build.gradle
index 95b17659733ed9d1b571551f9498fd92419028e4..1a3534069db76a39ad0ed6e42056d5e7edf68bcf 100644
--- a/build.gradle
+++ b/build.gradle
@@ -15,13 +15,14 @@ repositories {
configurations { // configuration that holds jars to copy into lib
releaseJars }
-def parser_version = '2.4.18-SNAPSHOT'
+def parser_version = '2.4.20-SNAPSHOT'
dependencies {
compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
compile (group: 'de.prob', name: 'prologlib', version: parser_version)
compile (group: 'de.prob', name: 'parserbase', version: parser_version)
compile (group: 'de.prob', name: 'bparser', version: parser_version)
+ compile (group: 'de.prob', name: 'ltlparser', version: parser_version)
testCompile (group: 'junit', name: 'junit', version: '4.+')
testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.3-SNAPSHOT')
@@ -32,7 +33,9 @@ dependencies {
}
-test { exclude('de/b2tla/tlc/integration/**') }
+test {
+ exclude('de/b2tla/tlc/integration/**')
+}
task integrationtests(type: Test){
diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java
index 55c61dca9837a9c84d36b901249ccc4ead2ba38e..e467d870e5d3b723303023842a512b0b269423c4 100644
--- a/src/main/java/de/b2tla/B2TLA.java
+++ b/src/main/java/de/b2tla/B2TLA.java
@@ -17,7 +17,6 @@ import de.b2tla.analysis.UsedStandardModules;
import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES;
import de.b2tla.exceptions.B2TLAIOException;
import de.b2tla.exceptions.B2tlaException;
-import de.b2tla.exceptions.TypeErrorException;
import de.b2tla.tlc.TLCOutput;
import de.b2tla.tlc.TLCOutputInfo;
import de.b2tla.tlc.TLCOutput.ERROR;
diff --git a/src/main/java/de/b2tla/Globals.java b/src/main/java/de/b2tla/Globals.java
index d4c48fe61a0adc59ee270bdb3d77abbf9faaad3f..71c4420a8bd6fac61430889c76f5fe0e71b97754 100644
--- a/src/main/java/de/b2tla/Globals.java
+++ b/src/main/java/de/b2tla/Globals.java
@@ -2,6 +2,9 @@ package de.b2tla;
public class Globals {
public static int DEFERRED_SET_SIZE = 3;
+ public static int MAX_INT = 4;
+ public static int MIN_INT = -1;
+
public static boolean GOAL = true;
public static boolean deadlockCheck = true;
public static boolean runTLC = true;
diff --git a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java b/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
index edf6ced506188e61512cfc73128c08c5fddfad35..db67446d4db38d4a3a53af641967c83fd165d394 100644
--- a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
@@ -3,7 +3,6 @@ package de.b2tla.analysis;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
-import java.util.Iterator;
import java.util.List;
import de.b2tla.exceptions.SubstitutionException;
diff --git a/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java b/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java
index 9cd0f6a825b33e17a3cf286fa69513988983e467..c5e7731a33b4a6d4c44d1a458ab8f5b4498c2d87 100644
--- a/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java
+++ b/src/main/java/de/b2tla/analysis/ConstantExpressionFinder.java
@@ -27,7 +27,6 @@ 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;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class ConstantExpressionFinder extends DepthFirstAdapter {
private MachineContext machineContext;
diff --git a/src/main/java/de/b2tla/analysis/ConstantsEliminator.java b/src/main/java/de/b2tla/analysis/ConstantsEliminator.java
index 4d47eb7f0f6196006f671d329d60d7d7d1fddc87..91bc43beac173391669bc968b7c8eb2dcd7400aa 100644
--- a/src/main/java/de/b2tla/analysis/ConstantsEliminator.java
+++ b/src/main/java/de/b2tla/analysis/ConstantsEliminator.java
@@ -8,10 +8,6 @@ import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedList;
-import tla2sany.modanalyzer.ModuleContext;
-
-import de.b2tla.analysis.ConstantsEvaluator.ConstantsInTreeFinder;
-import de.b2tla.analysis.ConstantsEvaluator.ValuesOfIdentifierFinder;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsOrder.java b/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
index cdc63b9d24569b11b553bdb55bc766eebb8d5982..579e13cec18a58df4004cfcbef3480e8ea0ba907 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
+++ b/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
-import java.util.LinkedList;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
diff --git a/src/main/java/de/b2tla/analysis/MachineContext.java b/src/main/java/de/b2tla/analysis/MachineContext.java
index 7469c64a3cb4b6b76ec3724fba2e76b382670d1b..a11c76027012ecafc7087da56d5cb0ddb57e9875 100644
--- a/src/main/java/de/b2tla/analysis/MachineContext.java
+++ b/src/main/java/de/b2tla/analysis/MachineContext.java
@@ -3,7 +3,6 @@ package de.b2tla.analysis;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
-import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedHashMap;
import java.util.LinkedList;
@@ -62,7 +61,6 @@ import de.be4.classicalb.core.parser.node.POperation;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.Start;
-import de.be4.classicalb.core.parser.node.TDefLiteralPredicate;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class MachineContext extends DepthFirstAdapter {
@@ -924,10 +922,10 @@ public class MachineContext extends DepthFirstAdapter {
* machine clauses getter
*/
- public AAbstractMachineParseUnit getAbstractMachineParseUnit(){
+ public AAbstractMachineParseUnit getAbstractMachineParseUnit() {
return abstractMachineParseUnit;
}
-
+
public AConstraintsMachineClause getConstraintMachineClause() {
return constraintMachineClause;
}
@@ -947,8 +945,13 @@ public class MachineContext extends DepthFirstAdapter {
public APropertiesMachineClause getPropertiesMachineClause() {
return propertiesMachineClause;
}
-
- public void setPropertiesMachineClaus(APropertiesMachineClause propertiesMachineClause){
+
+ public AAssertionsMachineClause getAssertionMachineClause() {
+ return assertionMachineClause;
+ }
+
+ public void setPropertiesMachineClaus(
+ APropertiesMachineClause propertiesMachineClause) {
this.propertiesMachineClause = propertiesMachineClause;
}
@@ -971,8 +974,9 @@ public class MachineContext extends DepthFirstAdapter {
public ADefinitionsMachineClause getDefinitionMachineClause() {
return definitionMachineClause;
}
-
- public void setDefinitionsMachineClause(ADefinitionsMachineClause definitionMachineClause){
+
+ public void setDefinitionsMachineClause(
+ ADefinitionsMachineClause definitionMachineClause) {
this.definitionMachineClause = definitionMachineClause;
}
diff --git a/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java b/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
index 9628ccba0523f19619af7bc5cb94b7b374f8f9b2..ee7f92d39c98b4e489d7f6297361d570184871a0 100644
--- a/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
+++ b/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
@@ -10,7 +10,6 @@ import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
import de.be4.classicalb.core.parser.node.ADeferredSetSet;
-import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AMachineHeader;
@@ -18,9 +17,7 @@ import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.ASeesMachineClause;
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.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class MachineDeclarationsCollector extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java b/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java
index 0bd65c9eac24626f87d0d25220f1edd1e7635d10..d9bb6cd1088fbb90071d579e1fb0d72bd1cbbc84 100644
--- a/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java
@@ -25,7 +25,6 @@ import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.ASelectWhenSubstitution;
import de.be4.classicalb.core.parser.node.ASkipSubstitution;
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.PSubstitution;
diff --git a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java b/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
index 52f76a39fafd050e0ac3b94ebd207747e5deacbf..a93160939d47f92c41f0becf7ed5ca6fd132c017 100644
--- a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
@@ -6,16 +6,9 @@ import java.util.Hashtable;
import de.b2tla.btypes.BType;
import de.b2tla.btypes.IntegerType;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AAddExpression;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
-import de.be4.classicalb.core.parser.node.AEqualPredicate;
-import de.be4.classicalb.core.parser.node.AExistsPredicate;
-import de.be4.classicalb.core.parser.node.AForallPredicate;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
-import de.be4.classicalb.core.parser.node.ANotEqualPredicate;
-import de.be4.classicalb.core.parser.node.ASetSubtractionExpression;
-import de.be4.classicalb.core.parser.node.AUnionExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
diff --git a/src/main/java/de/b2tla/analysis/PrimedNodesMarker.java b/src/main/java/de/b2tla/analysis/PrimedNodesMarker.java
index 6ec4dd411f043f02823d81682becab7b703efe5d..a14730da4e82e5b785fee8a97916bfb87d5a5c3e 100644
--- a/src/main/java/de/b2tla/analysis/PrimedNodesMarker.java
+++ b/src/main/java/de/b2tla/analysis/PrimedNodesMarker.java
@@ -2,7 +2,6 @@ package de.b2tla.analysis;
import java.util.ArrayList;
import java.util.HashSet;
-import java.util.LinkedHashMap;
import java.util.List;
import de.b2tla.exceptions.ScopeException;
@@ -11,13 +10,11 @@ import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
-import de.be4.classicalb.core.parser.node.AFunctionExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.APrimedIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.POperation;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class PrimedNodesMarker extends DepthFirstAdapter {
private ArrayList<POperation> operations;
diff --git a/src/main/java/de/b2tla/analysis/Renamer.java b/src/main/java/de/b2tla/analysis/Renamer.java
index bd5650ee91e9d9c40fcece22047d2ac353f81bf3..131ea70defa09d9587096737f19a824dd4434880 100644
--- a/src/main/java/de/b2tla/analysis/Renamer.java
+++ b/src/main/java/de/b2tla/analysis/Renamer.java
@@ -179,6 +179,8 @@ public class Renamer extends DepthFirstAdapter {
return res;
}
+ private ArrayList<HashSet<String>> localContexts = new ArrayList<HashSet<String>>();
+
private boolean exist(String name) {
if (KEYWORDS.contains(name))
return true;
@@ -186,15 +188,21 @@ public class Renamer extends DepthFirstAdapter {
return true;
if (SequencesKeywords.contains(name))
return true;
+
+ for (int i = 0; i < localContexts.size(); i++) {
+ if(localContexts.get(i).contains(name))
+ return true;
+ }
return false;
}
- private void renameIdentifier(Node node) {
+ private String renameIdentifier(Node node) {
AIdentifierExpression id = (AIdentifierExpression) node;
String name = Utils.getIdentifierAsString(id.getIdentifier());
String newName = incName(name);
namesTable.put(id, newName);
+ return newName;
}
private void evalDefinition(List<PExpression> params) {
@@ -221,21 +229,40 @@ public class Renamer extends DepthFirstAdapter {
evalDefinition(node.getParameters());
}
+
+ // local variables
+
public void inAForallPredicate(AForallPredicate node) {
evalBoundedVariables(node, node.getIdentifiers());
}
+
+ public void outAForallPredicate(AForallPredicate node) {
+ removeLastContext();
+ }
public void inAExistsPredicate(AExistsPredicate node) {
evalBoundedVariables(node, node.getIdentifiers());
}
-
+
+ public void outAExistsPredicate(AExistsPredicate node) {
+ removeLastContext();
+ }
+
public void inALambdaExpression(ALambdaExpression node) {
evalBoundedVariables(node, node.getIdentifiers());
}
+
+ public void outALambdaExpression(ALambdaExpression node) {
+ removeLastContext();
+ }
public void inAComprehensionSetExpression(AComprehensionSetExpression node) {
evalBoundedVariables(node, node.getIdentifiers());
}
+
+ public void outAComprehensionSetExpression(AComprehensionSetExpression node) {
+ removeLastContext();
+ }
public void inAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
evalBoundedVariables(node, node.getIdentifiers());
@@ -247,7 +274,6 @@ public class Renamer extends DepthFirstAdapter {
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
-
evalBoundedVariables(node, node.getIdentifiers());
}
@@ -261,9 +287,16 @@ public class Renamer extends DepthFirstAdapter {
}
private void evalBoundedVariables(Node node, List<PExpression> params) {
+ HashSet<String> context = new HashSet<String>();
for (PExpression e : params) {
- renameIdentifier(e);
+ String newName = renameIdentifier(e);
+ context.add(newName);
}
+ localContexts.add(context);
}
+ public void removeLastContext(){
+ localContexts.remove(localContexts.size()-1);
+ }
+
}
diff --git a/src/main/java/de/b2tla/analysis/StandardMadules.java b/src/main/java/de/b2tla/analysis/StandardMadules.java
index 327ec05d8f25018e61a44f715a3651f1d257cea0..9e27cef2893222f460995144c244b6b6acf72409 100644
--- a/src/main/java/de/b2tla/analysis/StandardMadules.java
+++ b/src/main/java/de/b2tla/analysis/StandardMadules.java
@@ -1,15 +1,13 @@
package de.b2tla.analysis;
import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Set;
public class StandardMadules {
// Functions
public static final String RANGE = "Range";
public static final String IMAGE = "Image";
-
+
public static final String TOTAL_INJECTIVE_FUNCTION = "TotalInjFunc";
public static final String TOTAL_SURJECTIVE_FUNCTION = "TotalSurFunc";
public static final String TOTAL_BIJECTIVE_FUNCTION = "TotalBijFunc";
@@ -18,7 +16,7 @@ public class StandardMadules {
public static final String PARTIAL_INJECTIVE_FUNCTION = "ParInjFunc";
public static final String PARTIAL_SURJECTIVE_FUNCTION = "ParSurFunc";
public static final String PARITAL_BIJECTIVE_FUNCTION = "ParBijFunc";
-
+
// Relations
public static final String RELATION = "Relation";
public static final String REL_DOMAIN = "RelDomain";
@@ -41,38 +39,34 @@ public class StandardMadules {
public static final String REL_CLOSURE = "RelClosure";
public static final String REL_FNC = "RelFnc";
public static final String REL_REL = "RelRel";
-
-
-
+
// FunctionsAsRelations
public static final String REL_CALL = "RelCall";
-
+
public static final String REL_TOTAL_FUNCTION = "RelTotalFunc";
public static final String REL_TOTAL_FUNCTION_ELEMENT_OF = "RelTotalFuncEleOf";
-
+
public static final String REL_TOTAL_INJECTIVE_FUNCTION = "RelTotalInjFunc";
public static final String REL_TOTAL_INJECTIVE_FUNCTION_ELEMENT_OF = "RelTotalInjFuncEleOf";
-
+
public static final String REL_TOTAL_SURJECTIVE_FUNCTION = "RelTotalSurFunc";
public static final String REL_TOTAL_SURJECTIVE_FUNCTION_ELEMENT_OF = "RelTotalSurFuncEleOf";
-
+
public static final String REL_TOTAL_BIJECTIVE_FUNCTION = "RelTotalBijFunc";
public static final String REL_TOTAL_BIJECTIVE_FUNCTION_ELEMENT_OF = "RelTotalBijFuncEleOf";
-
+
public static final String REL_PARTIAL_FUNCTION = "RelParFunc";
public static final String REL_PARTIAL_FUNCTION_ELEMENT_OF = "RelParFuncEleOf";
-
+
public static final String REL_PARTIAL_INJECTIVE_FUNCTION = "RelParInjFunc";
public static final String REL_PARTIAL_INJECTIVE_FUNCTION_ELEMENT_OF = "RelParInjFuncEleOf";
-
+
public static final String REL_PARTIAL_SURJECTIVE_FUNCTION = "RelParSurFunc";
public static final String REL_PARTIAL_SURJECTIVE_FUNCTION_ELEMENT_OF = "RelParSurFuncEleOf";
-
+
public static final String REL_PARTIAL_BIJECTIVE_FUNCTION = "RelParBijFunc";
public static final String REL_PARTIAL_BIJECTIVE_FUNCTION_ELEMENT_OF = "RelParBijFuncEleOf";
-
-
-
+
// SequencesExtended
public static final String SEQUENCE_LAST_ELEMENT = "Last";
public static final String SEQUENCE_PREPEND_ELEMENT = "Prepend";
@@ -85,15 +79,22 @@ public class StandardMadules {
public static final String SEQUENCE_PERMUTATION = "Perm";
public static final String SEQUENCE_REVERSE = "Rev";
public static final String SEQUENCE_GENERAL_CONCATINATION = "Conc";
-
+
public static final String SEQUENCE_TAKE_FIRST_ELEMENTS = "TakeFirstElements";
public static final String SEQUENCE_DROP_FIRST_ELEMENTS = "DropFirstElements";
-
-
+
public static final String REL_INJECTIVE_SEQUENCES = "RelISeq";
public static final String REL_NOT_EMPTY_INJECTIVE_SEQUENCES = "RelISeq1";
-
-
+
+ /*
+ * BBuiltIns
+ */
+
+ public static final String MIN = "Min";
+ public static final String MAX = "Max";
+ public static final String GENERAL_SUMMATION = "Sigma";
+ public static final String GENERAL_PRODUCT = "Pi";
+
public static final ArrayList<String> Relations = new ArrayList<String>();
static {
diff --git a/src/main/java/de/b2tla/analysis/TypeRestrictor.java b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
index 2f8ef13c528a1161e1335c1935ce4fa98bfbff33..1e15f7d514ee07d8b801779cb7a77768e933d695 100644
--- a/src/main/java/de/b2tla/analysis/TypeRestrictor.java
+++ b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
@@ -17,6 +17,8 @@ import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
import de.be4.classicalb.core.parser.node.AForallPredicate;
+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.ALambdaExpression;
@@ -41,14 +43,13 @@ public class TypeRestrictor extends DepthFirstAdapter {
private Hashtable<Node, ArrayList<NodeType>> restrictedTypesSet;
private HashSet<Node> removedNodes;
-
-
+
public TypeRestrictor(Start start, MachineContext machineContext,
Typechecker typechecker) {
this.machineContext = machineContext;
this.restrictedTypesSet = new Hashtable<Node, ArrayList<NodeType>>();
this.removedNodes = new HashSet<Node>();
-
+
cEF = new ConstantExpressionFinder(start, machineContext);
start.apply(this);
@@ -63,10 +64,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
return restrictedTypesSet.containsKey(node);
}
- public boolean removeNode(Node node){
+ public boolean removeNode(Node node) {
return this.removedNodes.contains(node);
}
-
+
private void putRestrictedType(Node identifier, NodeType expression) {
ArrayList<NodeType> list = restrictedTypesSet.get(identifier);
@@ -156,7 +157,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
@Override
- public void caseAForallPredicate(AForallPredicate node) {
+ public void inAForallPredicate(AForallPredicate node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
@@ -164,16 +165,13 @@ public class TypeRestrictor extends DepthFirstAdapter {
// e.apply(this);
list.add(e);
}
- // TODO test if the expression is really a implication, currently a
- // class cast exception is thrown
AImplicationPredicate implication = (AImplicationPredicate) node
.getImplication();
analysePredicate(implication.getLeft(), list);
- node.getImplication().apply(this);
}
@Override
- public void caseAExistsPredicate(AExistsPredicate node) {
+ public void inAExistsPredicate(AExistsPredicate node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
@@ -181,13 +179,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicate(), list);
- if (node.getPredicate() != null) {
- node.getPredicate().apply(this);
- }
}
@Override
- public void caseAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
+ public void inAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
@@ -195,12 +190,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list);
- node.getPredicates().apply(this);
- node.getExpression().apply(this);
}
@Override
- public void caseAQuantifiedIntersectionExpression(
+ public void inAQuantifiedIntersectionExpression(
AQuantifiedIntersectionExpression node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
@@ -209,12 +202,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list);
- node.getPredicates().apply(this);
- node.getExpression().apply(this);
}
@Override
- public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
+ public void inAComprehensionSetExpression(AComprehensionSetExpression node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
@@ -223,11 +214,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
// e.apply(this);
}
analysePredicate(node.getPredicates(), list);
- node.getPredicates().apply(this);
}
@Override
- public void caseALambdaExpression(ALambdaExpression node) {
+ public void inALambdaExpression(ALambdaExpression node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
@@ -235,10 +225,30 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicate(), list);
- node.getPredicate().apply(this);
- node.getExpression().apply(this);
}
+ public void inAGeneralSumExpression(AGeneralSumExpression node) {
+ HashSet<Node> list = new HashSet<Node>();
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ list.add(e);
+ }
+ analysePredicate(node.getPredicates(), list);
+ }
+
+ public void inAGeneralProductExpression(AGeneralProductExpression node)
+ {
+ HashSet<Node> list = new HashSet<Node>();
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ list.add(e);
+ }
+ analysePredicate(node.getPredicates(), list);
+ }
+
+
private Hashtable<Node, HashSet<Node>> expectedIdentifieListTable = new Hashtable<Node, HashSet<Node>>();
@Override
diff --git a/src/main/java/de/b2tla/analysis/Typechecker.java b/src/main/java/de/b2tla/analysis/Typechecker.java
index 8f0eeb6f0bc0001210255d15444b600162cb3b10..ff335453d6038630fffbb6cb1a6334e21e4eca8e 100644
--- a/src/main/java/de/b2tla/analysis/Typechecker.java
+++ b/src/main/java/de/b2tla/analysis/Typechecker.java
@@ -173,17 +173,17 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
- List<PDefinition> copy = new ArrayList<PDefinition>(
- node.getDefinitions());
- for (PDefinition e : copy) {
- setType(e, new UntypedType());
- }
-
- for (PDefinition e : copy) {
- e.apply(this);
- }
+ List<PDefinition> copy = new ArrayList<PDefinition>(
+ node.getDefinitions());
+ for (PDefinition e : copy) {
+ setType(e, new UntypedType());
+ }
+
+ for (PDefinition e : copy) {
+ e.apply(this);
+ }
}
-
+
@Override
// d(a) == 1
public void caseAExpressionDefinitionDefinition(
@@ -276,7 +276,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
-
@Override
public void caseAPropertiesMachineClause(final APropertiesMachineClause node) {
if (node.getPredicates() != null) {
@@ -679,22 +678,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAMaxIntExpression(AMaxIntExpression node) {
- try {
- IntegerType.getInstance().unify(getType(node), this);
- } catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in 'MAXINT'");
- }
+ unify(getType(node), IntegerType.getInstance(), node);
}
@Override
public void caseAMinIntExpression(AMinIntExpression node) {
- try {
- IntegerType.getInstance().unify(getType(node), this);
- } catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in 'MININT'");
- }
+ unify(getType(node), IntegerType.getInstance(), node);
}
@Override
@@ -913,26 +902,16 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseASuccessorExpression(ASuccessorExpression node) {
- SetType found = new SetType(new PairType(IntegerType.getInstance(),
- IntegerType.getInstance()));
- try {
- found.unify(getType(node), this);
- } catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER*INTEGER)' in ' succ '");
- }
+ FunctionType found = new FunctionType(IntegerType.getInstance(),
+ IntegerType.getInstance());
+ unify(getType(node), found, node);
}
@Override
public void caseAPredecessorExpression(APredecessorExpression node) {
- SetType found = new SetType(new PairType(IntegerType.getInstance(),
- IntegerType.getInstance()));
- try {
- found.unify(getType(node), this);
- } catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER*INTEGER)' in ' pred '");
- }
+ FunctionType found = new FunctionType(IntegerType.getInstance(),
+ IntegerType.getInstance());
+ unify(getType(node), found, node);
}
@Override
diff --git a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java b/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
index bb5f653c91715a0fa4f9cd41ad91743ead119a06..c4416bbc2c0c2bc61f206efc12f88894beeedad2 100644
--- a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
@@ -5,7 +5,6 @@ import java.util.Hashtable;
import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.Start;
/**
*
@@ -25,7 +24,7 @@ public class UnchangedVariablesFinder {
}
public UnchangedVariablesFinder(MachineContext c) {
- Start start = c.getTree();
+// Start start = c.getTree();
AssignedVariablesFinder aVF = new AssignedVariablesFinder(c);
//start.apply(aVF);
diff --git a/src/main/java/de/b2tla/analysis/UsedStandardModules.java b/src/main/java/de/b2tla/analysis/UsedStandardModules.java
index 3b2cafa4bbd9120b69dd6887faf7e7e0881665db..924b3b754ac65af65b2fe1376088cc27723b3b20 100644
--- a/src/main/java/de/b2tla/analysis/UsedStandardModules.java
+++ b/src/main/java/de/b2tla/analysis/UsedStandardModules.java
@@ -3,12 +3,10 @@ package de.b2tla.analysis;
import java.util.ArrayList;
import java.util.Comparator;
import java.util.HashSet;
-import java.util.Hashtable;
import java.util.List;
import java.util.Set;
import java.util.Collections;
-import de.b2tla.analysis.nodes.NodeType;
import de.b2tla.btypes.BType;
import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
@@ -56,6 +54,7 @@ import de.be4.classicalb.core.parser.node.ALessEqualPredicate;
import de.be4.classicalb.core.parser.node.ALessPredicate;
import de.be4.classicalb.core.parser.node.AMaxExpression;
import de.be4.classicalb.core.parser.node.AMinExpression;
+import de.be4.classicalb.core.parser.node.AMinIntExpression;
import de.be4.classicalb.core.parser.node.AMinusExpression;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AModuloExpression;
@@ -91,7 +90,6 @@ import de.be4.classicalb.core.parser.node.ASecondProjectionExpression;
import de.be4.classicalb.core.parser.node.ASeq1Expression;
import de.be4.classicalb.core.parser.node.ASeqExpression;
import de.be4.classicalb.core.parser.node.ASizeExpression;
-import de.be4.classicalb.core.parser.node.ASubsetStrictPredicate;
import de.be4.classicalb.core.parser.node.ASuccessorExpression;
import de.be4.classicalb.core.parser.node.ATailExpression;
import de.be4.classicalb.core.parser.node.ATotalBijectionExpression;
@@ -177,21 +175,18 @@ public class UsedStandardModules extends DepthFirstAdapter {
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());
- }
-
+ 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
*/
@@ -245,14 +240,6 @@ public class UsedStandardModules extends DepthFirstAdapter {
usedStandardModules.add(STANDARD_MODULES.Naturals);
}
- public void inAMinExpression(AMinExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
- }
-
- public void inAMaxExpression(AMaxExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
- }
-
public void inADivExpression(ADivExpression node) {
usedStandardModules.add(STANDARD_MODULES.Naturals);
}
@@ -298,6 +285,10 @@ public class UsedStandardModules extends DepthFirstAdapter {
usedStandardModules.add(STANDARD_MODULES.Integers);
}
+ public void inAMinIntExpression(AMinIntExpression node) {
+ usedStandardModules.add(STANDARD_MODULES.Integers);
+ }
+
/**
* FiniteSets
*/
@@ -308,6 +299,15 @@ public class UsedStandardModules extends DepthFirstAdapter {
/**
* BBuiltIns
*/
+
+ public void inAMinExpression(AMinExpression node) {
+ usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ }
+
+ public void inAMaxExpression(AMaxExpression node) {
+ usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ }
+
public void inAGeneralSumExpression(AGeneralSumExpression node) {
searchForIntegerTypeinTypesOFBoundedVariables(node.getIdentifiers());
usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
@@ -431,10 +431,13 @@ public class UsedStandardModules extends DepthFirstAdapter {
// Function call
public void inAFunctionExpression(AFunctionExpression node) {
- BType type = typechecker.getType(node.getIdentifier());
- if (type instanceof SetType) {
- usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
+ if (!(node.parent() instanceof AAssignSubstitution)) {
+ BType type = typechecker.getType(node.getIdentifier());
+ if (type instanceof SetType) {
+ usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
+ }
}
+
}
public void inATotalFunctionExpression(ATotalFunctionExpression node) {
@@ -491,7 +494,11 @@ public class UsedStandardModules extends DepthFirstAdapter {
node.getLhsExpression());
for (PExpression e : copy) {
if (e instanceof AFunctionExpression) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ BType type = typechecker.getType(((AFunctionExpression) e)
+ .getIdentifier());
+ if (type instanceof SetType) {
+ usedStandardModules.add(STANDARD_MODULES.Relations);
+ }
}
}
}
diff --git a/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
index d46d4e9b85b3b58213859c63507115376b3926e7..908621ab9ac44de203fd4534e435003f30a0b5ab 100644
--- a/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
@@ -2,21 +2,16 @@ package de.b2tla.analysis.transformation;
import java.util.ArrayList;
import java.util.Hashtable;
-import java.util.List;
import de.b2tla.analysis.DefinitionCollector;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
-import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
-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;
/**
@@ -26,7 +21,7 @@ import de.be4.classicalb.core.parser.node.Start;
*
* Note: All parameters of a definition are replaced before calls of
* sub-definitions are resolved. This behavior is similar to what ProB does by
- * eliminatingall definitions.
+ * eliminating all definitions.
*
*/
public class DefinitionsEliminator extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index eac7f75e27198e576e0503ee52f72e8096efe9a1..a8656b065521d9145fa96d174a40ebce436de508 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -2,11 +2,11 @@ package de.b2tla.prettyprint;
import java.util.ArrayList;
import java.util.HashSet;
-import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
+import de.b2tla.Globals;
import de.b2tla.analysis.MachineContext;
import de.b2tla.analysis.PrecedenceCollector;
import de.b2tla.analysis.PrimedNodesMarker;
@@ -742,6 +742,7 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAOperation(AOperation node) {
String name = renamer.getNameOfRef(node);
tlaModuleString.append(name);
+
List<PExpression> output = new ArrayList<PExpression>(
node.getReturnValues());
List<PExpression> params = new ArrayList<PExpression>(
@@ -949,6 +950,7 @@ public class TLAPrinter extends DepthFirstAdapter {
*/
inAExistsPredicate(node);
tlaModuleString.append("\\E ");
+
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (int i = 0; i < copy.size(); i++) {
@@ -1172,24 +1174,18 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAMinExpression(AMinExpression node) {
- inAMinExpression(node);
- tlaModuleString.append("CHOOSE min \\in ");
- node.getExpression().apply(this);
- tlaModuleString.append(" : \\A p \\in ");
+ tlaModuleString.append(MIN);
+ tlaModuleString.append("(");
node.getExpression().apply(this);
- tlaModuleString.append(" : min =< p");
- outAMinExpression(node);
+ tlaModuleString.append(")");
}
@Override
public void caseAMaxExpression(AMaxExpression node) {
- inAMaxExpression(node);
- tlaModuleString.append("(CHOOSE max \\in ");
- node.getExpression().apply(this);
- tlaModuleString.append(" : \\A p \\in ");
+ tlaModuleString.append(MAX);
+ tlaModuleString.append("(");
node.getExpression().apply(this);
- tlaModuleString.append(" : max >= p)");
- outAMaxExpression(node);
+ tlaModuleString.append(")");
}
@Override
@@ -1241,53 +1237,54 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAGeneralProductExpression(AGeneralProductExpression node) {
- inAGeneralProductExpression(node);
- tlaModuleString.append("PI({");
-
+ tlaModuleString.append("Pi(");
+ tlaModuleString.append("{");
node.getExpression().apply(this);
tlaModuleString.append(" : ");
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
printIdentifierList(copy);
-
- tlaModuleString.append(" \\in { ");
-
- printIdentifierList(copy);
-
tlaModuleString.append(" \\in ");
- printTypesOfIdentifierList(copy);
- tlaModuleString.append(" : ");
- node.getPredicates().apply(this);
- tlaModuleString.append("}");
-
+ if (typeRestrictor.removeNode(node.getPredicates())) {
+ printTypesOfIdentifierList(copy);
+ } else {
+ tlaModuleString.append("{");
+ printIdentifierList(copy);
+ tlaModuleString.append(" \\in ");
+ printTypesOfIdentifierList(copy);
+ tlaModuleString.append(" : ");
+ node.getPredicates().apply(this);
+ tlaModuleString.append("}");
+ }
tlaModuleString.append("}");
- outAGeneralProductExpression(node);
+ tlaModuleString.append(")");
}
@Override
public void caseAGeneralSumExpression(AGeneralSumExpression node) {
- inAGeneralSumExpression(node);
- tlaModuleString.append("SIGMA({");
-
+ tlaModuleString.append("Sigma(");
+ tlaModuleString.append("{");
node.getExpression().apply(this);
tlaModuleString.append(" : ");
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
printIdentifierList(copy);
-
- tlaModuleString.append(" \\in { ");
-
- printIdentifierList(copy);
-
tlaModuleString.append(" \\in ");
- printTypesOfIdentifierList(copy);
- tlaModuleString.append(" : ");
- node.getPredicates().apply(this);
+ if (typeRestrictor.removeNode(node.getPredicates())) {
+ printTypesOfIdentifierList(copy);
+ } else {
+ tlaModuleString.append("{");
+ printIdentifierList(copy);
+ tlaModuleString.append(" \\in ");
+ printTypesOfIdentifierList(copy);
+ tlaModuleString.append(" : ");
+ node.getPredicates().apply(this);
+ tlaModuleString.append("}");
+ }
tlaModuleString.append("}");
- tlaModuleString.append("})");
- outAGeneralSumExpression(node);
+ tlaModuleString.append(")");
}
@Override
@@ -1304,6 +1301,16 @@ public class TLAPrinter extends DepthFirstAdapter {
outAPredecessorExpression(node);
}
+ @Override
+ public void caseAMaxIntExpression(AMaxIntExpression node) {
+ tlaModuleString.append(Globals.MAX_INT);
+ }
+
+ @Override
+ public void caseAMinIntExpression(AMinIntExpression node) {
+ tlaModuleString.append(Globals.MIN_INT);
+ }
+
/**
* Function
*/
@@ -1509,7 +1516,8 @@ public class TLAPrinter extends DepthFirstAdapter {
node.getRight().apply(this);
tlaModuleString.append("]");
} else {
- if (node.parent() instanceof AMemberPredicate && !typeRestrictor.removeNode(node.parent())) {
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(node.parent())) {
tlaModuleString.append(REL_TOTAL_FUNCTION_ELEMENT_OF);
} else {
tlaModuleString.append(REL_TOTAL_FUNCTION);
@@ -1529,7 +1537,8 @@ public class TLAPrinter extends DepthFirstAdapter {
if (subtype instanceof FunctionType) {
tlaModuleString.append(funcName);
} else {
- if (node.parent() instanceof AMemberPredicate && !typeRestrictor.removeNode(node.parent())) {
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(node.parent())) {
tlaModuleString.append(relEleOfName);
} else {
tlaModuleString.append(relName);
@@ -2146,7 +2155,8 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIseqExpression(AIseqExpression node) {
- if (node.parent() instanceof AMemberPredicate && !typeRestrictor.removeNode(node.parent())) {
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(node.parent())) {
tlaModuleString.append(INJECTIVE_SEQUENCE_ELEMENT_OF);
} else {
tlaModuleString.append(INJECTIVE_SEQUENCE);
@@ -2158,7 +2168,8 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIseq1Expression(AIseq1Expression node) {
- if (node.parent() instanceof AMemberPredicate && !typeRestrictor.removeNode(node.parent())) {
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(node.parent())) {
tlaModuleString.append(INJECTIVE_SEQUENCE_1_ELEMENT_OF);
} else {
tlaModuleString.append(INJECTIVE_SEQUENCE_1);
diff --git a/src/main/java/de/b2tla/tlc/ModuleMatcher.java b/src/main/java/de/b2tla/tlc/ModuleMatcher.java
index 73451ef90613c9761b02907755868bd075f3b563..ac3d8160db8170bebe6b473fee84497f19d946c3 100644
--- a/src/main/java/de/b2tla/tlc/ModuleMatcher.java
+++ b/src/main/java/de/b2tla/tlc/ModuleMatcher.java
@@ -4,8 +4,6 @@ import java.util.HashMap;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
-import de.b2tla.util.StopWatch;
-
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java
index 4de9fe894bfee57ea5e4ea29d5f9647e3d9a29e5..56c3f39828c56217e704ef65a22275b4602bd7d5 100644
--- a/src/main/java/de/b2tla/tlc/TLCOutput.java
+++ b/src/main/java/de/b2tla/tlc/TLCOutput.java
@@ -41,6 +41,10 @@ public class TLCOutput {
parseTrace();
return trace;
}
+
+ public String getModuleName(){
+ return moduleName;
+ }
public boolean hasTrace() {
return states.size() > 0;
diff --git a/src/main/resources/standardModules/BBuiltIns.tla b/src/main/resources/standardModules/BBuiltIns.tla
index d2b83006dcdfde7d65915ea7edde986c560e9a55..6abae1ba5c643af6ded07f6bae01b8912021e362 100644
--- a/src/main/resources/standardModules/BBuiltIns.tla
+++ b/src/main/resources/standardModules/BBuiltIns.tla
@@ -2,10 +2,18 @@
EXTENDS Integers, FiniteSets, TLC
-RECURSIVE SIGMA(_)
-SIGMA(S) == LET e == CHOOSE e \in S: TRUE
- IN IF S = {} THEN 0 ELSE e + SIGMA(S \ {e})
-
+RECURSIVE Sigma(_)
+Sigma(S) == LET e == CHOOSE e \in S: TRUE
+ IN IF S = {} THEN 0 ELSE e + Sigma(S \ {e})
+
+RECURSIVE Pi(_)
+Pi(S) == LET e == CHOOSE e \in S: TRUE
+ IN IF S = {} THEN 0 ELSE e + Pi(S \ {e})
+
+Max == CHOOSE x \in {1} : \A p \in {1} : x >= p
+
+Min == CHOOSE x \in {1} : \A p \in {1} : x =< p
+
succ[x \in Int] == x + 1
pred[x \in Int] == x - 1
diff --git a/src/test/java/de/b2tla/analysis/ConstantsTest.java b/src/test/java/de/b2tla/analysis/ConstantsTest.java
index cea3868c0bb6cbdcd86f96490a80b7e6df5019fb..41b036cf53f0defce62d1d7f340220bcfbaef78b 100644
--- a/src/test/java/de/b2tla/analysis/ConstantsTest.java
+++ b/src/test/java/de/b2tla/analysis/ConstantsTest.java
@@ -3,7 +3,6 @@ package de.b2tla.analysis;
import static de.b2tla.util.TestUtil.compare;
-import org.junit.Ignore;
import org.junit.Test;
public class ConstantsTest {
diff --git a/src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java b/src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java
index 5c76e94f112b8d42f5b8630bc21d60bf1555d378..15d7285a480866c90c59a4b4d6432737dc7de566 100644
--- a/src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java
+++ b/src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java
@@ -2,7 +2,6 @@ package de.b2tla.analysis;
import static de.b2tla.util.TestUtil.compare;
-import org.junit.Ignore;
import org.junit.Test;
public class DefinitionsOrderTest {
diff --git a/src/test/java/de/b2tla/analysis/PrecedenceTest.java b/src/test/java/de/b2tla/analysis/PrecedenceTest.java
index 8f270131c2852749adb4cec1b6d9db4f608d562a..1b8d55bbf423ccd997e83e243dd190176cd5aec7 100644
--- a/src/test/java/de/b2tla/analysis/PrecedenceTest.java
+++ b/src/test/java/de/b2tla/analysis/PrecedenceTest.java
@@ -46,6 +46,19 @@ public class PrecedenceTest {
compare(expected, machine);
}
+ @Test
+ public void testMult() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES 1 * 2 * 3 = 6 \n"
+ + "END";
+
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Integers\n"
+ + "ASSUME 1 * 2 * 3 = 6\n"
+ + "======";
+ compare(expected, machine);
+ }
+
@Test
public void testAndOr() throws Exception {
String machine = "MACHINE test\n"
diff --git a/src/test/java/de/b2tla/analysis/PrimeTest.java b/src/test/java/de/b2tla/analysis/PrimeTest.java
index acb8bd4b5b04cedd85d1f159c0c2585c43f7cf62..c755adfe48628400661969f9f9abff184452b88c 100644
--- a/src/test/java/de/b2tla/analysis/PrimeTest.java
+++ b/src/test/java/de/b2tla/analysis/PrimeTest.java
@@ -9,6 +9,7 @@ public class PrimeTest {
@Test
public void testOperationParameter() throws Exception {
- //TODO
+
+
}
}
diff --git a/src/test/java/de/b2tla/analysis/ScopeTest.java b/src/test/java/de/b2tla/analysis/ScopeTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..b526447b0135bbae08bf91d4a402eb96a2e72b99
--- /dev/null
+++ b/src/test/java/de/b2tla/analysis/ScopeTest.java
@@ -0,0 +1,161 @@
+package de.b2tla.analysis;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+import static de.b2tla.util.TestUtil.checkMachine;
+import de.b2tla.exceptions.ScopeException;
+
+public class ScopeTest {
+
+ @Test(expected = ScopeException.class)
+ public void testDuplicateConstant() throws Exception {
+ String machine = "MACHINE test \n" + "CONSTANTS k, k \n"
+ + "PROPERTIES 1 = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testDuplicateSeenMachine() throws Exception {
+ String machine = "MACHINE test \n" + "SEES M1, M1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testConstraintsMissingMachineParameter() throws Exception {
+ String machine = "MACHINE test \n" + "CONSTRAINTS k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testConstraints() throws Exception {
+ String machine = "MACHINE test(k) \n" + "CONSTRAINTS k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testPropertiesUnknownIdentifier() throws Exception {
+ String machine = "MACHINE test \n" + "PROPERTIES k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testPropertiesConstant() throws Exception {
+ String machine = "MACHINE test \n" + "CONSTANTS k \n"
+ + "PROPERTIES k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testConstantsHasSameNameAsElementOfEnumeratedSet() throws Exception {
+ String machine = "MACHINE test \n" + "SETS k = {k1,k2} \n"
+ + "CONSTANTS k \n"
+ + "PROPERTIES k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testInvariantUnknownIdentifier() throws Exception {
+ String machine = "MACHINE test \n" + "INVARIANT k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testInvariantParameter() throws Exception {
+ String machine = "MACHINE test(k) \n" + "CONSTRAINTS k = 1\n"
+ + "INVARIANT k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testInvariantConstatnParameter() throws Exception {
+ String machine = "MACHINE test\n" + "CONSTANTS k \n"
+ + "PROPERTIES k = 1" + "INVARIANT k = 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testInvariantVariable() throws Exception {
+ String machine = "MACHINE test\n" + "VARIABLES k \n"
+ + "INVARIANT k = 1 \n" + "INITIALISATION k := 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testInitialisationUnknwonIdentifier() throws Exception {
+ String machine = "MACHINE test\n" + "VARIABLES k \n"
+ + "INVARIANT k = 1 \n" + "INITIALISATION k := a \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testOperationsUnknwonIdentifier() throws Exception {
+ String machine = "MACHINE test\n" + "OPERATIONS foo = a := 1" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testSubstitution() throws Exception {
+ String machine = "MACHINE test\n" + "VARIABLES x \n"
+ + "INVARIANT x = 1 \n" + "INITIALISATION x := 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Ignore //TODO
+ @Test(expected = ScopeException.class)
+ public void testConstantSubstitution() throws Exception {
+ String machine = "MACHINE test\n" + "CONSTANTS x \n"
+ + "PROPERTIES x = 1 \n" + "INITIALISATION x := 1 \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testSubstitution2() throws Exception {
+ String machine = "MACHINE test\n" + "CONSTANTS x \n"
+ + "PROPERTIES x = 1 \n" + "VARIABLES a \n"
+ + "INVARIANT a = 1 \n" + "INITIALISATION a := x \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testUnkownOperation() throws Exception {
+ String machine = "MACHINE test\n" + "INITIALISATION foo \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testLocalVariableForAll() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES !x.(x : INT => x > 1) \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testLocalVariableExist() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES #x.(x : INT & x > 1) \n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testLocalVariableLambda() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES %x.(x : INT | x + 1)(1) = 1\n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test
+ public void testNestedLocalExists() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES #x.(x : INT & #x.(x + 1 = 1))\n" + "END";
+ checkMachine(machine);
+ }
+
+ @Test(expected = ScopeException.class)
+ public void testDuplicateLocalVariable() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES #(x,x).(1 = 1 & x = x)\n" + "END";
+ checkMachine(machine);
+ }
+
+}
diff --git a/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java b/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
index fefb9b2d8478bf3eb7f110fa0278a8e5b3bc0486..4a1f5f6b8315ff2d87afbf699038a0bd9a5930b2 100644
--- a/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
+++ b/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
@@ -2,7 +2,6 @@ package de.b2tla.analysis;
import static de.b2tla.util.TestUtil.compare;
-import org.junit.Ignore;
import org.junit.Test;
public class TypeRestrictionsTest {
diff --git a/src/test/java/de/b2tla/analysis/UnchangedVariablesTest.java b/src/test/java/de/b2tla/analysis/UnchangedVariablesTest.java
index 79ecc0bbb1d369886b40f4dfbb7f51dda4042535..6c0ef2c09d7ac9213f0e392dc5cc686bd27003e6 100644
--- a/src/test/java/de/b2tla/analysis/UnchangedVariablesTest.java
+++ b/src/test/java/de/b2tla/analysis/UnchangedVariablesTest.java
@@ -1,8 +1,8 @@
package de.b2tla.analysis;
import static de.b2tla.util.TestUtil.compare;
+import static de.b2tla.util.TestUtil.compareEquals;
-import org.junit.Ignore;
import org.junit.Test;
import de.b2tla.exceptions.SubstitutionException;
@@ -40,9 +40,8 @@ public class UnchangedVariablesTest {
}
- @Ignore
@Test
- public void testFunction() throws Exception {
+ public void testFunctionAssignment() throws Exception {
String machine = "MACHINE test\n"
+ "VARIABLES x\n"
+ "INVARIANT x = %p.(p: {1}| 1)\n"
@@ -51,15 +50,33 @@ public class UnchangedVariablesTest {
+ "END";
String expected = "---- MODULE test ----\n"
- + "VARIABLES x, y \n"
- + "Inv == x = 1 /\\ y = 1\n"
- + "Init == x = 1 /\\ y = 1\n"
- + "foo == IF x = 1 THEN x' = 2 /\\ UNCHANGED <<y>> ELSE y' = 2 /\\ UNCHANGED <<x>>\n"
+ + "VARIABLES x \n"
+ + "Invariant == x = [p \\in {1} |-> 1] \n"
+ + "Init == x = [p \\in {1} |-> 1] \n"
+ + "foo == x' = [x EXCEPT ![1] = 2] \n"
+ "Next == foo\n" + "====";
compare(expected, machine);
}
- @Ignore
+ @Test
+ public void testRelationAssignment() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = {(1,2)}\n"
+ + "INITIALISATION x := {(1,2)}\n"
+ + "OPERATIONS foo = x(1):= 2 \n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Relations\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = {<<1, 2>>}\n"
+ + "Init == x = {<<1, 2>>}\n"
+ + "foo == x' = RelOverride(x, {<<1, 2>>})\n\n"
+ + "Next == \\/ foo\n" + "====";
+ compareEquals(expected, machine);
+ }
+
@Test
public void testIfThenElse() throws Exception {
String machine = "MACHINE test\n" + "VARIABLES x,y\n"
@@ -76,7 +93,6 @@ public class UnchangedVariablesTest {
compare(expected, machine);
}
- @Ignore
@Test
public void testChoice() throws Exception {
String machine = "MACHINE test\n" + "VARIABLES x,y\n"
diff --git a/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java b/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java
index 62d857e17bfee851bad62207d89ca9f62f096190..f2758fa63633f8f1950c7b47492104844e1550ff 100644
--- a/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java
+++ b/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java
@@ -85,71 +85,100 @@ public class BBuildInsTest {
+ "====";
compareEquals(expected, machine);
}
+
+ @Test
+ public void testSigma() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES SIGMA(z).(z : {1,2,3}| z+z) = 12 \n" + "END";
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Naturals, BBuiltIns\n"
+ + "ASSUME Sigma({z + z : z \\in {1, 2, 3}}) = 12\n"
+ + "====";
+ compareEquals(expected, machine);
+ }
- @Ignore
@Test
- public void testPartialFunction() throws Exception {
- String machine = "MACHINE test\n" + "CONSTANTS k\n"
- + "PROPERTIES k = {1,2} +-> {1,2}\n" + "END";
+ public void testSigma2() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES SIGMA(z).(z : {1,2,3} & 1=1| z+z) = 12\n" + "END";
String expected = "---- MODULE test ----\n"
- + "EXTENDS Integers\n"
- + "CONSTANTS k\n"
- + "ASSUME k = [<<a, b>> \\in { <<a, b>> \\in (Int \\times Int) : a = b} |-> a + b][2, 2]\n"
+ + "EXTENDS Naturals, BBuiltIns\n"
+ + "ASSUME Sigma({z + z : z \\in {z \\in {1, 2, 3} : 1 = 1}}) = 12\n"
+ "====";
- // TODO partial function
- compare(expected, machine);
+ compareEquals(expected, machine);
}
- // TODO include Standard module BBuiltIns
@Test
- public void testSigma() throws Exception {
+ public void testPi() throws Exception {
String machine = "MACHINE test\n"
- + "PROPERTIES SIGMA(z).(z : {1,2,3}| z) = 6 \n" + "END";
+ + "PROPERTIES PI(z).(z : {1,2,3}| z+z) = 12 \n" + "END";
String expected = "---- MODULE test ----\n"
- + "EXTENDS Integers, BBuiltIns\n"
- + "ASSUME SIGMA({z : z \\in { z \\in Int : z \\in {1, 2, 3}}}) = 6\n"
+ + "EXTENDS Naturals, BBuiltIns\n"
+ + "ASSUME Pi({z + z : z \\in {1, 2, 3}}) = 12\n"
+ "====";
compareEquals(expected, machine);
}
-
- @Ignore
+
@Test
- public void testPI() throws Exception {
+ public void testPi2() throws Exception {
String machine = "MACHINE test\n"
- + "PROPERTIES PI(z).(z : {1,2,3}| z) = 6 \n" + "END";
- String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
- + "ASSUME PI() = 1\n" + "======";
- compare(expected, machine);
+ + "PROPERTIES PI(z).(z : {1,2,3} & 1=1| z+z) = 12\n" + "END";
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Naturals, BBuiltIns\n"
+ + "ASSUME Pi({z + z : z \\in {z \\in {1, 2, 3} : 1 = 1}}) = 12\n"
+ + "====";
+ compareEquals(expected, machine);
}
- @Ignore
@Test
public void testSucc() throws Exception {
String machine = "MACHINE test\n" + "PROPERTIES succ(3) = 4 \n" + "END";
- String expected = "---- MODULE test----\n" + "EXTENDS BBuiltIns\n"
- + "ASSUME succ(3) = 4\n" + "======";
+ String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n"
+ + "ASSUME succ[3] = 4\n" + "====";
compareEquals(expected, machine);
}
- @Ignore
@Test
public void testPred() throws Exception {
String machine = "MACHINE test\n" + "PROPERTIES pred(2) = 1 \n" + "END";
- String expected = "---- MODULE test----\n" + "EXTENDS BBuiltIns\n"
- + "ASSUME pred(2) = 1\n" + "======";
- compare(expected, machine);
+ String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n"
+ + "ASSUME pred[2] = 1\n" + "====";
+ compareEquals(expected, machine);
}
- @Ignore
@Test
- public void testMinInt() throws Exception {
- // TODO read MinInt and MaxInt from Configuration file
+ public void testMin() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES min({1}) = 1 \n" + "END";
+ String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n"
+ + "ASSUME Min({1}) = 1\n" + "====";
+ compareEquals(expected, machine);
}
-
- @Ignore
+
+ @Test
+ public void testMax() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES max({1}) = 1 \n" + "END";
+ String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n"
+ + "ASSUME Max({1}) = 1\n" + "====";
+ compareEquals(expected, machine);
+ }
+
@Test
public void testMaxInt() throws Exception {
-
+ String machine = "MACHINE test\n"
+ + "PROPERTIES MAXINT = MAXINT \n" + "END";
+ String expected = "---- MODULE test ----\n"
+ + "ASSUME 4 = 4\n" + "====";
+ compare(expected, machine);
}
+ @Test
+ public void testMinInt() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES MININT = MININT \n" + "END";
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Integers\n"
+ + "ASSUME -1 = -1\n" + "====";
+ compare(expected, machine);
+ }
+
}
diff --git a/src/test/java/de/b2tla/prettyprint/FunctionTest.java b/src/test/java/de/b2tla/prettyprint/FunctionTest.java
index 28bf56f9b21270a6aaea99904a2f12ec0974c994..b032839b11b387bb323dc780c71d81fa10c156af 100644
--- a/src/test/java/de/b2tla/prettyprint/FunctionTest.java
+++ b/src/test/java/de/b2tla/prettyprint/FunctionTest.java
@@ -1,9 +1,6 @@
package de.b2tla.prettyprint;
import static de.b2tla.util.TestUtil.*;
-import static org.junit.Assert.*;
-
-import org.junit.Ignore;
import org.junit.Test;
@@ -116,4 +113,15 @@ public class FunctionTest {
}
+ @Test
+ public void testPartialFunction() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES {} = {1,2} +-> {1,2}\n" + "END";
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Functions\n"
+ + "ASSUME {} = ParFunc({1, 2}, {1, 2})\n"
+ + "====";
+ compareEquals(expected, machine);
+ }
+
}
diff --git a/src/test/java/de/b2tla/prettyprint/NumbersTest.java b/src/test/java/de/b2tla/prettyprint/NumbersTest.java
index 85cad918c28f53a439f4debce51b04f61456cc1d..5362a43193ce8ca8e4b342f13cfd91b5d45f06ed 100644
--- a/src/test/java/de/b2tla/prettyprint/NumbersTest.java
+++ b/src/test/java/de/b2tla/prettyprint/NumbersTest.java
@@ -141,31 +141,6 @@ public class NumbersTest {
compare(expected, machine);
}
- @Test
- public void testMin() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = min({1,2,3})\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 1 = CHOOSE min \\in {1,2,3}: \\A p \\in {1,2,3}: min =< p \n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testMax() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 3 = max({1,2,3})\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 3 = CHOOSE max \\in {1,2,3}: \\A p \\in {1,2,3}: max >= p \n"
- + "======";
- compare(expected, machine);
- }
-
-
@Test
public void testAdd() throws Exception {
String machine = "MACHINE test\n"
diff --git a/src/test/java/de/b2tla/prettyprint/RelationTest.java b/src/test/java/de/b2tla/prettyprint/RelationTest.java
index 8f8ae50701737936e4c9eb21ad8be186ed2f067a..47f160c9b36b6d0499c4e67a6908046c0fdf4cfb 100644
--- a/src/test/java/de/b2tla/prettyprint/RelationTest.java
+++ b/src/test/java/de/b2tla/prettyprint/RelationTest.java
@@ -1,13 +1,8 @@
package de.b2tla.prettyprint;
import static de.b2tla.util.TestUtil.*;
-import static org.junit.Assert.assertEquals;
-
-import org.junit.Ignore;
import org.junit.Test;
-import de.b2tla.B2TLA;
-
public class RelationTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
index ee4a5f675333f2b37dadceb9f364f7b0cb5113a7..b0c0aa4919dd4a9b5e708108f64e38b7acadee97 100644
--- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
@@ -2,12 +2,10 @@ package de.b2tla.tlc.integration;
import static org.junit.Assert.assertEquals;
-import org.junit.Ignore;
import org.junit.Test;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput;
-import de.b2tla.tlc.TLCOutput.ERROR;
public class ErrorTest {
diff --git a/src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java b/src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java
index 35e4e1ebc52e27f461912a870a0e0943628671d3..f037047f3254e331f0bbd74e7922412744b790b9 100644
--- a/src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java
+++ b/src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java
@@ -315,7 +315,7 @@ public class ArithmeticOperatorTest {
String machine = "MACHINE test\n" + "CONSTANTS k \n"
+ "PROPERTIES k = succ \n" + "END";
TestTypechecker t = new TestTypechecker(machine);
- assertEquals("POW(INTEGER*INTEGER)", t.constants.get("k").toString());
+ assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString());
}
@Test(expected = TypeErrorException.class)
@@ -330,7 +330,7 @@ public class ArithmeticOperatorTest {
String machine = "MACHINE test\n" + "CONSTANTS k \n"
+ "PROPERTIES k = pred \n" + "END";
TestTypechecker t = new TestTypechecker(machine);
- assertEquals("POW(INTEGER*INTEGER)", t.constants.get("k").toString());
+ assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString());
}
@Test(expected = TypeErrorException.class)
diff --git a/src/test/java/de/b2tla/util/TestUtil.java b/src/test/java/de/b2tla/util/TestUtil.java
index efad08b14a96e6d4f29980fd0689615623487021..860d73bfbf5c927d92a980847524649da4723937 100644
--- a/src/test/java/de/b2tla/util/TestUtil.java
+++ b/src/test/java/de/b2tla/util/TestUtil.java
@@ -43,6 +43,17 @@ public class TestUtil {
}
// assertEquals(sb2.toString(), sb1.toString());
}
+
+ public static void checkMachine(String machine)
+ throws Exception {
+ B2TlaTranslator b2tlaTranslator = new B2TlaTranslator(machine);
+ b2tlaTranslator.translate();
+ System.out.println(b2tlaTranslator.getModuleString());
+
+ String name = b2tlaTranslator.getMachineName();
+ de.tla2b.translation.Tla2BTranslator
+ .translateString(name, b2tlaTranslator.getModuleString(), null);
+ }
public static void print(Start start) {
final Ast2String ast2String2 = new Ast2String();
diff --git a/src/test/java/standard/PrecedenceTest.java b/src/test/java/standard/PrecedenceTest.java
deleted file mode 100644
index 38a97c439aa6436e773e510cd70d4ba75b22f676..0000000000000000000000000000000000000000
--- a/src/test/java/standard/PrecedenceTest.java
+++ /dev/null
@@ -1,64 +0,0 @@
-package standard;
-
-
-import java.util.HashSet;
-import java.util.Hashtable;
-
-import org.junit.Test;
-
-
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.PrecedenceCollector;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UnchangedVariablesFinder;
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.Start;
-
-public class PrecedenceTest {
-
-
-
- @Test
- public void testDisjunctionConjunction() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = 1 & 2 = 2 or 3 = 3 \n"
- + "END";
- new Env(machine);
- }
-
-
- @Test
- public void testMult() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 * 2 * 3 = 6 \n"
- + "END";
- new Env(machine);
- }
-
-
-
-
- class Env {
- Hashtable<String, HashSet<Node>> unchangedVariablesOfOperation;
-
- public Env(String machine) throws BException {
-
- BParser parser = new BParser("Test");
- Start start = parser.parse(machine, false);
- final Ast2String ast2String2 = new Ast2String();
- start.apply(ast2String2);
- System.out.println(ast2String2.toString());
-
- MachineContext c = new MachineContext(start);
- Typechecker t = new Typechecker(c);
- UnchangedVariablesFinder u = new UnchangedVariablesFinder(c);
-
- PrecedenceCollector p = new PrecedenceCollector(start, t.getTypes());
-
- }
-
- }
-}
diff --git a/src/test/java/standard/PrinterTest.java b/src/test/java/standard/PrinterTest.java
deleted file mode 100644
index c09000ad1245d1a96f3199eba4b2803439bcf8da..0000000000000000000000000000000000000000
--- a/src/test/java/standard/PrinterTest.java
+++ /dev/null
@@ -1,67 +0,0 @@
-package standard;
-
-import org.junit.Test;
-
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.PrecedenceCollector;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UnchangedVariablesFinder;
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Start;
-
-public class PrinterTest {
-
- @Test
- public void test3() throws BException {
- String machine = "MACHINE test\n" + "VARIABLES x,y\n"
- + "INVARIANT x = 1 & y = 1\n" + "INITIALISATION x,y := 1,1 \n"
- + "OPERATIONS foo = x := 1\n"
- + " ;bar = IF x = 1 THEN x:= 2 ELSE y := 2 END \n" + "END";
- Env env = new Env(machine);
- System.out.println(env.result);
- // assertEquals(3,env.variablesTable.get("foo").size());
- }
-
- @Test
- public void test4() throws BException {
- String machine = "MACHINE test\n" + "VARIABLES x,y\n"
- + "INVARIANT x = 1 & y = 1\n" + "INITIALISATION x,y := 1,1 \n"
- + "OPERATIONS foo = CHOICE x := 1 OR x:= 2 END\n"
- + " ;bar = y := 1 \n" + "END";
- Env env = new Env(machine);
- System.out.println(env.result);
- // assertEquals(3,env.variablesTable.get("foo").size());
- }
-
- @Test
- public void testIF() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = 1 & 2 = 2 or 3 = 3 \n" + "END";
- Env env = new Env(machine);
- System.out.println(env.result);
- }
-
-}
-
-class Env {
- String result;
-
- public Env(String machine) throws BException {
-
- BParser parser = new BParser("Test");
- Start start = parser.parse(machine, false);
- final Ast2String ast2String2 = new Ast2String();
- start.apply(ast2String2);
- System.out.println(ast2String2.toString());
- System.out.println();
- MachineContext c = new MachineContext(start);
- Typechecker t = new Typechecker(c);
- UnchangedVariablesFinder u = new UnchangedVariablesFinder(c);
- PrecedenceCollector p = new PrecedenceCollector(start, t.getTypes());
- // TLAPrinter printer = new TLAPrinter(c, t, u, p);
- // result = printer.getStringbuilder().toString(); TODO
- }
-
-}
diff --git a/src/test/java/standard/ScopeTest.java b/src/test/java/standard/ScopeTest.java
deleted file mode 100644
index 4bf7bd1509ce6c613e6dd1996635cfd01ad278a2..0000000000000000000000000000000000000000
--- a/src/test/java/standard/ScopeTest.java
+++ /dev/null
@@ -1,229 +0,0 @@
-package standard;
-
-import org.junit.Ignore;
-import org.junit.Test;
-
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.exceptions.ScopeException;
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Start;
-
-public class ScopeTest {
-
- @Test(expected = ScopeException.class)
- public void testDuplicateConstant() throws BException {
- String machine = "MACHINE test \n" + "CONSTANTS k, k \n"
- + "PROPERTIES 1 = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testDuplicateSeenMachine() throws BException {
- String machine = "MACHINE test \n" + "SEES M1, M1 \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testConstraintsMissingMachineParameter() throws BException {
- String machine = "MACHINE test \n" + "CONSTRAINTS k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testConstraints() throws BException {
- String machine = "MACHINE test(k) \n" + "CONSTRAINTS k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testPropertiesUnknownIdentifier() throws BException {
- String machine = "MACHINE test \n" + "PROPERTIES k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testPropertiesConstant() throws BException {
- String machine = "MACHINE test \n" + "CONSTANTS k \n"
- + "PROPERTIES k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testPropertiesDeferredSet() throws BException {
- String machine = "MACHINE test \n" + "SETS k \n"
- + "PROPERTIES k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testPropertiesEnumeratedSet() throws BException {
- String machine = "MACHINE test \n" + "SETS k = {k1,k2} \n"
- + "PROPERTIES k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testPropertiesElementOfEnumeratedSet() throws BException {
- String machine = "MACHINE test \n" + "SETS k = {k1,k2} \n"
- + "PROPERTIES k1 = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testInvariantUnknownIdentifier() throws BException {
- String machine = "MACHINE test \n" + "INVARIANT k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testInvariantParameter() throws BException {
- String machine = "MACHINE test(k) \n" + "CONSTRAINTS k = 1\n"
- + "INVARIANT k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testInvariantConstatnParameter() throws BException {
- String machine = "MACHINE test\n" + "CONSTANTS k \n"
- + "PROPERTIES k = 1" + "INVARIANT k = 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testInvariantVariable() throws BException {
- String machine = "MACHINE test\n" + "VARIABLES k \n"
- + "INVARIANT k = 1 \n" + "INITIALISATION k := 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testInitialisationUnknwonIdentifier() throws BException {
- String machine = "MACHINE test\n" + "VARIABLES k \n"
- + "INVARIANT k = 1 \n" + "INITIALISATION k := a \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testOperationsUnknwonIdentifier() throws BException {
- String machine = "MACHINE test\n" + "OPERATIONS foo = a := 1" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testSubstitution() throws BException {
- String machine = "MACHINE test\n" + "VARIABLES x \n"
- + "INVARIANT x = 1 \n" + "INITIALISATION x := 1 \n" + "END";
- checkScope(machine);
- }
-
- @Ignore //TODO
- @Test(expected = ScopeException.class)
- public void testConstantSubstitution() throws BException {
- String machine = "MACHINE test\n" + "CONSTANTS x \n"
- + "PROPERTIES x = 1 \n" + "INITIALISATION x := 1 \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testSubstitution2() throws BException {
- String machine = "MACHINE test\n" + "CONSTANTS x \n"
- + "PROPERTIES x = 1 \n" + "VARIABLES a \n"
- + "INVARIANT a = 1 \n" + "INITIALISATION a := x \n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testUnkownOperation() throws BException {
- String machine = "MACHINE test\n" + "INITIALISATION foo \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testOperation() throws BException {
- String machine = "MACHINE test\n" + "INITIALISATION foo \n"
- + "OPERATIONS foo = skip \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariableForAll() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES !x.(x : INT => x > 1) \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariableExist() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES #x.(x : INT & x > 1) \n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariableLambda() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES %x.(x : INT | x + 1) = 1\n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariableUnion() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES UNION(x).(x : INT | x + 1) = 1\n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariableInter() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES INTER(x).(x : INT | x + 1) = 1\n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariablePi() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES PI(x).(x : INT | x + 1) = 1\n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalVariableSigma() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES SIGMA(x).(x : INT | x + 1) = 1\n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testLocalOperationParameter() throws BException {
- String machine = "MACHINE test\n"
- + "OPERATIONS foo(a) = PRE a = 1 THEN skip END\n" + "END";
- checkScope(machine);
- }
-
- @Test
- public void testNestedLocalExists() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES #x.(x : INT & #x.(x : INT & x = 1))\n" + "END";
- checkScope(machine);
- }
-
- @Test(expected = ScopeException.class)
- public void testDuplicateLocalVariable() throws BException {
- String machine = "MACHINE test\n"
- + "PROPERTIES #(x,x).(1 = 1 & x = x)\n" + "END";
- checkScope(machine);
- }
-
- public void checkScope(String machine) throws BException {
- BParser parser = new BParser("Test");
- Start start = parser.parse(machine, false);
- final Ast2String ast2String2 = new Ast2String();
- start.apply(ast2String2);
-
- new MachineContext(start);
- }
-
-}