diff --git a/build.gradle b/build.gradle
index b0fac80442b686b7f2262f661a1947f2f07a145d..ae55582921f58b2eaf4d2514da3c0d61ae40631e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -22,19 +22,16 @@ repositories {
}
}
-configurations { // configuration that holds jars to copy into lib
- releaseJars
-}
-
configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
def parser_version = '2.5.0-SNAPSHOT'
+def tlatools_version = '1.0.2-SNAPSHOT'
dependencies {
//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
- compile (group: 'de.hhu.stups', name: 'tlatools', version: '1.0.2-SNAPSHOT')
+ compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
@@ -45,12 +42,6 @@ dependencies {
testCompile (group: 'junit', name: 'junit', version: '4.11')
testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.0.8-SNAPSHOT')
-
- releaseJars (group: 'de.hhu.stups', name: 'tlatools', version: '1.0.0')
- releaseJars (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
- releaseJars (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
- releaseJars (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
- releaseJars (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
}
jacoco {
@@ -86,25 +77,27 @@ task jacocoIntegrationTestReport(type: JacocoReport) {
sourceSets sourceSets.main
//executionData files('build/jacoco/integrationTests.exec')
executionData fileTree(project.rootDir.absolutePath).include("**/build/jacoco/*.exec")
- }
-
-jar { from sourceSets.main.allJava }
-jar {
- from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) }
-}
-jar {
- manifest {
- attributes "Main-Class" : 'de.tlc4b.TLC4B'
- }
}
+task createJar(type: Jar, dependsOn: build){
+ archiveName = 'TLC4B.jar'
+ //from sourceSets.main.allJava
+ from sourceSets.main.output
+ //from {configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
+ from {configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
+ exclude('**/*.java')
+ manifest {
+ attributes "Main-Class" : 'de.tlc4b.TLC4B'
+ }
+}
-task tlc4b(dependsOn: build) << {
+task tlc4b(dependsOn: createJar) << {
copy {
from('build/libs/')
into('.')
- include('tlc4b-'+project.version+'.jar')
- rename('tlc4b-(.+)', 'TLC4B.jar')
+ include('TLC4B.jar')
+ //include('tlc4b-'+project.version+'.jar')
+ //rename('tlc4b-(.+)', 'TLC4B.jar')
}
}
diff --git a/src/main/java/de/tlc4b/MP.java b/src/main/java/de/tlc4b/MP.java
index 7ce4afdd4402e6a406be2c0c5f8938ce9b6cf335..e2088d513273f929bb7444baeec14b95bc4ffae9 100644
--- a/src/main/java/de/tlc4b/MP.java
+++ b/src/main/java/de/tlc4b/MP.java
@@ -41,7 +41,8 @@ public class MP {
@Override
public void print(String s) {
- super.print("TLC: " + s);
+ s = s.replaceAll("\n", "\n> ");
+ super.print("> " + s);
}
}
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 68c6286e2460f6494716615aecec723d72cc9e67..1a344ff850e26fc9b1fbff3f2240732aafb767d5 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -84,7 +84,7 @@ public class Translator {
// machine
final RecursiveMachineLoader rml = new RecursiveMachineLoader(
machineFile.getParent(), parser.getContentProvider());
- rml.loadAllMachines(machineFile, start, null, parser.getDefinitions());
+ rml.loadAllMachines(machineFile, start, parser.getSourcePositions(), parser.getDefinitions());
parsedMachines = rml.getParsedMachines();
@@ -146,7 +146,7 @@ public class Translator {
unchangedVariablesFinder);
TypeRestrictor typeRestrictor = new TypeRestrictor(start,
- machineContext, typechecker);
+ machineContext, typechecker, constantsEvaluator);
PrecedenceCollector precedenceCollector = new PrecedenceCollector(
start, typechecker, machineContext, typeRestrictor);
@@ -160,8 +160,6 @@ public class Translator {
constantsEvaluator, deferredSetSizeCalculator, typechecker);
generator.generate();
- generator.getTlaModule().sortAllDefinitions(machineContext);
-
UsedStandardModules usedModules = new UsedStandardModules(start,
typechecker, typeRestrictor, generator.getTlaModule());
diff --git a/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
index bba3e86d97f487f000c2dc4f76381939c3448434..a373f1fed0781337f2b400b6e36fdb17155b4f9f 100644
--- a/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
@@ -31,7 +31,7 @@ import de.be4.classicalb.core.parser.node.PPredicate;
*
*/
public class ConstantsEvaluator extends DepthFirstAdapter {
- private Hashtable<Node, HashSet<Node>> dependsOnIdentifierTable;
+ private LinkedHashMap<Node, HashSet<Node>> dependsOnIdentifierTable;
private MachineContext machineContext;
private ValuesOfIdentifierFinder valuesOfConstantsFinder;
private HashMap<Node, Integer> integerValueTable;
@@ -61,12 +61,11 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
}
public ArrayList<PExpression> getRangeOfIdentifier(Node con) {
- ;
return valuesOfConstantsFinder.rangeOfIdentifierTable.get(con);
}
public ConstantsEvaluator(MachineContext machineContext) {
- this.dependsOnIdentifierTable = new Hashtable<Node, HashSet<Node>>();
+ this.dependsOnIdentifierTable = new LinkedHashMap<Node, HashSet<Node>>();
this.integerValueTable = new HashMap<Node, Integer>();
this.machineContext = machineContext;
this.propertiesList = new ArrayList<Node>();
@@ -95,7 +94,6 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
this.valueOfIdentifier = new LinkedHashMap<Node, Node>();
evalIdentifier(machineContext.getConstants().values());
-
evalIdentifier(machineContext.getScalarParameter().values());
}
@@ -110,8 +108,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
continue;
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable
.get(id);
+
for (Node val : idValues) {
HashSet<Node> idsInVal = dependsOnIdentifierTable.get(val);
+ idsInVal.remove(id);
if (idsInVal.size() == 0) {
valueOfIdentifier.put(id, val);
removeIdentifier(ids, id);
@@ -195,8 +195,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
this.rangeOfIdentifierTable = new Hashtable<Node, ArrayList<PExpression>>();
this.identifiers = new HashSet<Node>();
- this.identifiers.addAll(machineContext.getBMachineConstants()
- .values());
+ this.identifiers.addAll(machineContext.getConstants().values());
this.identifiers.addAll(machineContext.getScalarParameter()
.values());
@@ -219,7 +218,6 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
if (machineContext.getConstantsSetup() instanceof ADisjunctPredicate) {
analyseConstantSetupPredicate(machineContext
.getConstantsSetup());
-
for (Node con : this.identifiers) {
ArrayList<PExpression> list = rangeOfIdentifierTable
.get(con);
@@ -264,7 +262,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
PExpression left = equals.getLeft();
Node left_ref = machineContext.getReferences().get(left);
if (rangeOfIdentifierTable.containsKey(left_ref)) {
- System.out.println("hallo");
+ // TODO
}
ArrayList<PExpression> currentRange = rangeOfIdentifierTable
.get(left_ref);
diff --git a/src/main/java/de/tlc4b/analysis/DefinitionsOrder.java b/src/main/java/de/tlc4b/analysis/DefinitionsSorter.java
similarity index 97%
rename from src/main/java/de/tlc4b/analysis/DefinitionsOrder.java
rename to src/main/java/de/tlc4b/analysis/DefinitionsSorter.java
index 70dd44d3f213a168e9ea0aeb566022f1d552bb61..61f051101ce06ba8ec08214a6978bc29ea8fdaaf 100644
--- a/src/main/java/de/tlc4b/analysis/DefinitionsOrder.java
+++ b/src/main/java/de/tlc4b/analysis/DefinitionsSorter.java
@@ -21,7 +21,7 @@ import de.be4.classicalb.core.parser.node.PDefinition;
* @author hansen
*/
-public class DefinitionsOrder extends DepthFirstAdapter {
+public class DefinitionsSorter extends DepthFirstAdapter {
private MachineContext machineContext;
private Hashtable<Node, HashSet<Node>> dependenciesTable;
private HashSet<Node> current;
@@ -32,7 +32,7 @@ public class DefinitionsOrder extends DepthFirstAdapter {
return allDefinitions;
}
- public DefinitionsOrder(MachineContext machineContext,
+ public DefinitionsSorter(MachineContext machineContext,
ArrayList<PDefinition> allDefinitions) {
this.machineContext = machineContext;
dependenciesTable = new Hashtable<Node, HashSet<Node>>();
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index c621ee8da44f8811e8bcfe556f2e1bd252727585..7a8a870f55bc3cba44a5614a7b66fac8f0e1e5f8 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -64,6 +64,7 @@ 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.TIdentifierLiteral;
+import de.tlc4b.MP;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.transformation.DefinitionsSorter;
import de.tlc4b.analysis.transformation.MachineClauseSorter;
@@ -180,7 +181,7 @@ public class MachineContext extends DepthFirstAdapter {
try {
visitor.start();
} catch (ScopeException e) {
- System.out.println("Warning: LTL formula '" + visitor.getName()
+ MP.println("Warning: LTL formula '" + visitor.getName()
+ "' cannot be checked by TLC.");
notSupportedLTLFormulas.add(visitor);
}
@@ -235,13 +236,12 @@ public class MachineContext extends DepthFirstAdapter {
if (node.getHeader() != null) {
node.getHeader().apply(this);
}
-
-
+
List<PMachineClause> machineClauses = node.getMachineClauses();
// Sort the machine clauses: declarations clauses first, then
// properties clauses
MachineClauseSorter.sortMachineClauses(start);
-
+
for (PMachineClause e : machineClauses) {
e.apply(this);
}
@@ -284,7 +284,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
definitionMachineClause = node;
DefinitionsSorter.sortDefinitions(node);
-
+
List<PDefinition> copy = node.getDefinitions();
/*
@@ -416,7 +416,7 @@ public class MachineContext extends DepthFirstAdapter {
return;
}
}
-
+
throw new ScopeException("Unkown definition: '" + name
+ "' at position: " + node.getStartPos());
}
@@ -572,7 +572,8 @@ public class MachineContext extends DepthFirstAdapter {
private ArrayList<MachineContext> lookupExtendedMachines() {
ArrayList<MachineContext> list = new ArrayList<MachineContext>();
- for( Entry<String, AIdentifierExpression> entry : seenMachines.entrySet()){
+ for (Entry<String, AIdentifierExpression> entry : seenMachines
+ .entrySet()) {
String s = entry.getKey();
AIdentifierExpression value = entry.getValue();
if (value.getIdentifier().size() == 1) {
@@ -892,9 +893,10 @@ public class MachineContext extends DepthFirstAdapter {
node.getPredicates().apply(this);
contextTable.remove(contextTable.size() - 1);
}
-
+
@Override
- public void caseAEventBComprehensionSetExpression(AEventBComprehensionSetExpression node){
+ public void caseAEventBComprehensionSetExpression(
+ AEventBComprehensionSetExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
List<PExpression> copy = new ArrayList<PExpression>(
@@ -904,7 +906,7 @@ public class MachineContext extends DepthFirstAdapter {
}
}
node.getPredicates().apply(this);
-
+
node.getExpression().apply(this);
contextTable.remove(contextTable.size() - 1);
}
@@ -1143,4 +1145,3 @@ public class MachineContext extends DepthFirstAdapter {
}
}
-
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index deaf97957295ce73b1604a32c46db9255d3afd5b..ab416a1cf00c472861f77a8474b96fc308ae5ba1 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -47,6 +47,7 @@ import de.be4.classicalb.core.parser.node.Start;
import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AForallLtl;
import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.analysis.ConstantsEvaluator;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType;
@@ -59,6 +60,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
private final MachineContext machineContext;
private final IdentifierDependencies identifierDependencies;
private final Typechecker typechecker;
+ private final ConstantsEvaluator constantsEvaluator;
private final Hashtable<Node, Node> restrictedTypeNodeTable;
private final HashSet<Node> removedNodes;
@@ -75,9 +77,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
public TypeRestrictor(Start start, MachineContext machineContext,
- Typechecker typechecker) {
+ Typechecker typechecker, ConstantsEvaluator constantsEvaluator) {
this.machineContext = machineContext;
this.typechecker = typechecker;
+ this.constantsEvaluator = constantsEvaluator;
this.restrictedTypeNodeTable = new Hashtable<Node, Node>();
this.removedNodes = new HashSet<Node>();
@@ -140,7 +143,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(expression);
restrictedNodeTable.put(identifier, list);
} else {
- list.add(expression);
+ if (!list.contains(expression)) {
+ list.add(expression);
+ }
}
}
@@ -171,14 +176,20 @@ public class TypeRestrictor extends DepthFirstAdapter {
@Override
public void inAPropertiesMachineClause(APropertiesMachineClause node) {
- HashSet<Node> list = new HashSet<Node>();
- list.addAll(machineContext.getConstants().values());
-
- analysePredicate(node.getPredicates(), list, new HashSet<Node>());
HashSet<PExpression> set = new HashSet<PExpression>();
for (Node con : machineContext.getConstants().values()) {
set.add((PExpression) con);
+ Node valueOfConstant = constantsEvaluator.getValueOfConstant(con);
+ if(valueOfConstant!= null){
+ removedNodes.add(valueOfConstant.parent());
+ }
+
}
+ HashSet<Node> list = new HashSet<Node>();
+ list.addAll(machineContext.getConstants().values());
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
+
+
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set),
false);
}
@@ -545,6 +556,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
// formula.
for (PExpression e : copy) {
+ if (constantsEvaluator.getValueOfIdentifierMap().containsKey(e)) {
+ continue;
+ }
+
PExpression tree = null;
ArrayList<Node> restrictedList = restrictedNodeTable.get(e);
if (restrictedList == null) {
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index b5f74ddf0eb6b2aac4006e6b487a57f4177609e4..8791cb0f10074e827712512142cc03fe8457a661 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -318,15 +318,15 @@ public class TLAPrinter extends DepthFirstAdapter {
}
private void printDefinitions() {
- ArrayList<TLADefinition> definitions = tlaModule.getDefinitions();
+ ArrayList<TLADefinition> definitions = tlaModule.getTLADefinitions();
for (int i = 0; i < definitions.size(); i++) {
TLADefinition def = definitions.get(i);
if (def.getDefName() instanceof AEnumeratedSetSet) {
def.getDefName().apply(this);
continue;
}
-
def.getDefName().apply(this);
+
moduleStringAppend(" == ");
Node e = def.getDefinition();
if (e == null) {
@@ -384,9 +384,12 @@ public class TLAPrinter extends DepthFirstAdapter {
return;
for (int i = 0; i < list.size(); i++) {
- moduleStringAppend("ASSUME ");
- list.get(i).apply(this);
- moduleStringAppend("\n");
+ Node node = list.get(i);
+ if(!typeRestrictor.isARemovedNode(node)){
+ moduleStringAppend("ASSUME ");
+ list.get(i).apply(this);
+ moduleStringAppend("\n");
+ }
}
}
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index 9174a97bea44dffc4dc88150d048e960f95c206a..97c016efb8a6f8a49f768a7a23568b2812266de0 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -31,6 +31,7 @@ import de.be4.classicalb.core.parser.node.PPredicate;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.ConstantsEvaluator;
import de.tlc4b.analysis.DefinitionsAnalyser;
+import de.tlc4b.analysis.DefinitionsSorter;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
@@ -67,8 +68,9 @@ public class Generator extends DepthFirstAdapter {
evalSetValuedParameter();
evalScalarParameter();
evalMachineSets();
- evalConstants();
evalDefinitions();
+ evalConstants();
+
evalInvariant();
evalOperations();
evalGoal();
@@ -141,12 +143,13 @@ public class Generator extends DepthFirstAdapter {
Node value = idValueTable.get(param);
if (value != null) {
- tlaModule.definitions.add(new TLADefinition(param, value));
+ tlaModule.tlaDefinitions.add(new TLADefinition(param, value));
continue;
}
Integer intValue = constantsEvaluator.getIntValue(param);
if (intValue != null) {
- tlaModule.definitions.add(new TLADefinition(param, intValue));
+ tlaModule.tlaDefinitions
+ .add(new TLADefinition(param, intValue));
continue;
}
@@ -202,7 +205,7 @@ public class Generator extends DepthFirstAdapter {
Node n = itr2.next();
AEnumeratedSetSet e = (AEnumeratedSetSet) n;
TLADefinition def = new TLADefinition(e, e);
- this.tlaModule.definitions.add(def);
+ this.tlaModule.tlaDefinitions.add(def);
List<PExpression> copy = new ArrayList<PExpression>(e.getElements());
for (PExpression element : copy) {
this.tlaModule.constants.add(element);
@@ -216,9 +219,11 @@ public class Generator extends DepthFirstAdapter {
ADefinitionsMachineClause node = machineContext
.getDefinitionMachineClause();
if (node != null) {
- for (PDefinition def : node.getDefinitions()) {
- this.tlaModule.addToAllDefinitions(def);
- }
+ ArrayList<PDefinition> bDefinitions = new ArrayList<PDefinition>(
+ node.getDefinitions());
+ DefinitionsSorter defOrder = new DefinitionsSorter(machineContext,
+ bDefinitions);
+ this.tlaModule.allDefinitions.addAll(defOrder.getAllDefinitions());
}
}
@@ -249,7 +254,7 @@ public class Generator extends DepthFirstAdapter {
AExpressionDefinitionDefinition exprDef = new AExpressionDefinitionDefinition(
con.getIdentifier().get(0), new LinkedList<PExpression>(),
- (PExpression) value);//.clone());
+ (PExpression) value);// .clone());
machineContext.addReference(exprDef, con);
this.tlaModule.addToAllDefinitions(exprDef);
@@ -304,9 +309,9 @@ public class Generator extends DepthFirstAdapter {
}
} else {
- if (machineContext.getConstantsSetup() == null){
+ if (machineContext.getConstantsSetup() == null) {
tlaModule.assumes
- .addAll(constantsEvaluator.getPropertiesList());
+ .addAll(constantsEvaluator.getPropertiesList());
}
tlaModule.addAssume(propertiesPerdicate);
}
@@ -328,9 +333,10 @@ public class Generator extends DepthFirstAdapter {
this.tlaModule.variables.add(e);
}
}
-
+
@Override
- public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ public void caseAConcreteVariablesMachineClause(
+ AConcreteVariablesMachineClause node) {
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (PExpression e : copy) {
diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
index d56ff85ae7ade3b4bfcd79b2b95e08f60eab0fa2..a13cd764ab42dd15c35142803dd65ec61d2159b7 100644
--- a/src/main/java/de/tlc4b/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -4,27 +4,27 @@ import java.util.ArrayList;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.POperation;
-import de.tlc4b.analysis.DefinitionsOrder;
+import de.tlc4b.analysis.DefinitionsSorter;
import de.tlc4b.analysis.MachineContext;
public class TLAModule {
protected String moduleName;
- protected final ArrayList<TLADefinition> definitions;
+ protected final ArrayList<TLADefinition> tlaDefinitions;
protected final ArrayList<Node> constants;
protected final ArrayList<Node> assumes;
protected final ArrayList<Node> variables;
protected final ArrayList<Node> invariants;
private final ArrayList<Node> initPredicates;
protected final ArrayList<POperation> operations;
- private ArrayList<PDefinition> bDefinitions;
+ private ArrayList<PDefinition> bDefinitions;
private final ArrayList<Node> assertions;
- private ArrayList<PDefinition> allDefinitions;
+ protected ArrayList<PDefinition> allDefinitions;
public TLAModule() {
- this.definitions = new ArrayList<TLADefinition>();
+ this.tlaDefinitions = new ArrayList<TLADefinition>();
this.constants = new ArrayList<Node>();
this.assumes = new ArrayList<Node>();
this.variables = new ArrayList<Node>();
@@ -38,12 +38,6 @@ public class TLAModule {
}
- public void sortAllDefinitions(MachineContext machineContext) {
- DefinitionsOrder defOrder = new DefinitionsOrder(machineContext,
- this.allDefinitions);
- this.allDefinitions = defOrder.getAllDefinitions();
- }
-
public void addToAllDefinitions(PDefinition def) {
this.allDefinitions.add(def);
}
@@ -78,8 +72,8 @@ public class TLAModule {
return moduleName;
}
- public ArrayList<TLADefinition> getDefinitions() {
- return definitions;
+ public ArrayList<TLADefinition> getTLADefinitions() {
+ return tlaDefinitions;
}
public ArrayList<Node> getConstants() {
diff --git a/src/main/resources/standardModules/BBuiltIns.tla b/src/main/resources/standardModules/BBuiltIns.tla
index 688ba0f068ff90261fcc4d153642d1fa1d53562d..3f2ad561bf2c26ce5c014450320b227fe8351fc9 100644
--- a/src/main/resources/standardModules/BBuiltIns.tla
+++ b/src/main/resources/standardModules/BBuiltIns.tla
@@ -19,14 +19,13 @@ BDivision(a,b) ==
[] a < 0 /\ b > 0 -> -((-a) \div b)
[] a >= 0 /\ b < 0 -> -(a \div (-b))
[] a < 0 /\ b < 0 -> (-a) \div (-b)
- [] b = 0 -> Assert(FALSE, "Error: Division by zero.")
- [] OTHER -> Assert(FALSE, "Error: Modulo Operator.")
+ [] Assert(b /= 0, "Error: Division by zero.") -> 0 \* dummy value
\* Rules from AtelierB reference manual (see page 40)
BModulo(a,b) ==
- IF a >= 0 /\ b > 0
+ IF Assert(a >= 0 /\ b > 0, "Error: Both operands of the modulo operator must be natural numbers.")
THEN a % b
- ELSE Assert(FALSE, "Error: Both operands of the modulo operator must be natural numbers.")
+ ELSE 0 \* dummy value
RECURSIVE Sigma(_)
Sigma(S) ==
@@ -43,15 +42,15 @@ Sigma(S) ==
RECURSIVE Pi(_)
Pi(S) ==
- IF S = {} THEN 0
- ELSE
- LET
- e == CHOOSE e \in S: TRUE
- newS == S \ {e}
- IN
- IF newS = {}
- THEN e[2]
- ELSE e[2] * Pi(S \ {e})
+ IF S = {} THEN 0
+ ELSE
+ LET
+ e == CHOOSE e \in S: TRUE
+ newS == S \ {e}
+ IN
+ IF newS = {}
+ THEN e[2]
+ ELSE e[2] * Pi(S \ {e})
\* The product of all second components of pairs which are elements of S
Pow1(S) == (SUBSET S) \ {{}}
@@ -73,11 +72,13 @@ NotStrictSubset(S, T) == ~ (S \subset T)
\* The predicate becomes true if S is not a strict subset of T
RECURSIVE Inter(_)
-Inter(S) == IF S = {}
- THEN Assert(FALSE, "Error: Applied the inter operator to an empty set.")
- ELSE LET e == (CHOOSE e \in S: TRUE)
- IN IF Cardinality(S) = 1
- THEN e
- ELSE e \cap Inter(S \ {e})
+Inter(S) ==
+ IF Assert(S = {}, "Error: Applied the inter operator to an empty set.")
+ THEN
+ LET e == (CHOOSE e \in S: TRUE)
+ IN IF Cardinality(S) = 1
+ THEN e
+ ELSE e \cap Inter(S \ {e})
+ ELSE {} \* dummy value
\* The intersection of all elements of S.
=============================================================================
diff --git a/src/main/resources/standardModules/ExternalFunctions.tla b/src/main/resources/standardModules/ExternalFunctions.tla
index b411bce3f70e2ee4de3df62e72ef03cbd53172b2..d8ab3debd82239d423c943ca716f18247248645c 100644
--- a/src/main/resources/standardModules/ExternalFunctions.tla
+++ b/src/main/resources/standardModules/ExternalFunctions.tla
@@ -3,29 +3,32 @@ EXTENDS Sequences, Integers, TLC, FiniteSets
--------------------------------------------------------------------------------------
(* Strings *)
-RECURSIVE SPLIT1(_,_,_,_)
-LOCAL SPLIT1(s,c,start,i) ==
+
+LOCAL SPLIT1[s \in STRING, c \in STRING, start \in Nat, i \in Nat] ==
CASE i = Len(s)+1 -> IF i /= start
THEN <<SubSeq(s,start,i-1)>>
ELSE <<>>
[] i+Len(c)-1 > Len(s) -> <<SubSeq(s,start,Len(s))>>
[] SubSeq(s,i,i+Len(c)-1) = c -> IF i /= start
- THEN <<SubSeq(s,start,i-1)>> \o SPLIT1(s,c,i+Len(c),i+Len(c))
- ELSE <<>> \o SPLIT1(s,c,i+Len(c),i+Len(c))
- [] OTHER -> SPLIT1(s,c,start,i+1)
+ THEN <<SubSeq(s,start,i-1)>> \o SPLIT1[s,c,i+Len(c),i+Len(c)]
+ ELSE <<>> \o SPLIT1[s,c,i+Len(c),i+Len(c)]
+ [] OTHER -> SPLIT1[s,c,start,i+1]
-STRING_SPLIT(s, c) == SPLIT1(s,c,1,1)
+STRING_SPLIT(s, c) == SPLIT1[s,c,1,1]
INT_TO_STRING(i) == ToString(i)
LOCAL Max(S) == CHOOSE x \in S : \A p \in S : x >= p
-RECURSIVE SORT_SET(_)
-SORT_SET(s) ==
- IF s = {}
- THEN {}
- ELSE LET max == Max(s)
- IN SORT_SET(s\{max}) \cup {<<Cardinality(s), max>>}
+
+SORT_SET(s2)==
+ LET
+ SORT_SET_Recursive[s \in SUBSET Int] ==
+ IF s = {}
+ THEN {}
+ ELSE LET max == Max(s)
+ IN SORT_SET_Recursive[s\{max}] \cup {<<Cardinality(s), max>>}
+ IN SORT_SET_Recursive[s2]
STRING_APPEND(a,b) == a \o b
@@ -45,18 +48,14 @@ STRING_TO_INT(str) ==
item(s,i) == SubSeq(s,i,i)
- RECURSIVE pow(_,_)
- pow(a,b) == IF b = 0 THEN 1 ELSE a * pow(a,b-1)
-
- RECURSIVE STRING_TO_INT1(_,_)
- STRING_TO_INT1(s, i) ==
+ STRING_TO_INT1[s \in STRING, i \in Nat] ==
IF i = Len(s)
THEN STRINGDIGIT_TO_INT(item(s,i))
- ELSE STRINGDIGIT_TO_INT(item(s,i)) * pow(10,Len(s)-i) + STRING_TO_INT1(s,i+1)
+ ELSE STRINGDIGIT_TO_INT(item(s,i)) * 10^(Len(s)-i) + STRING_TO_INT1[s,i+1]
IN
IF item(str, 1) = "-"
- THEN -1 * STRING_TO_INT1(SubSeq(str,2,Len(str)),1)
- ELSE STRING_TO_INT1(str,1)
+ THEN -1 * STRING_TO_INT1[SubSeq(str,2,Len(str)),1]
+ ELSE STRING_TO_INT1[str,1]
DECIMAL_TO_INT(s) ==
STRING_TO_INT(
diff --git a/src/main/resources/standardModules/SequencesAsRelations.tla b/src/main/resources/standardModules/SequencesAsRelations.tla
index af607c3260863615e06de4b01625bd58f79e01f7..a7eed1310b6196f7dffce420f1c607af7e4bb9fa 100644
--- a/src/main/resources/standardModules/SequencesAsRelations.tla
+++ b/src/main/resources/standardModules/SequencesAsRelations.tla
@@ -6,40 +6,40 @@ IsRelSeq(x, S) == \A n \in 1..Cardinality(x): RelCall(x,n) \in S
RelSeqSet(x, S) == IF IsRelSeq(x,S) THEN {x} ELSE {}
-RelSeq(S) == {p \in SUBSET(Nat \times S):
- LET d == {q[1] : q \in p}
+RelSeq(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
IN /\ Cardinality(p) = Cardinality(d)
/\ d = 1..Cardinality(d)}
IsRelSeq1(x, S) == x # {} /\ IsRelSeq(x, S)
\* Testing if x is a non-empty sequence with elements of the set S
-
+
RelSeqSet1(x, S) == IF IsRelSeq1(x,S) THEN {x} ELSE {}
-RelSeq1(S) == {p \in SUBSET(Nat \times S):
- LET d == {q[1] : q \in p}
+RelSeq1(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
IN /\ Cardinality(p) > 0
/\ Cardinality(p) = Cardinality(d)
/\ d = 1..Cardinality(d)}
-LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinality(DOMAIN x)}
+LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinality(DOMAIN x)}
: n \in 0..Cardinality(S)}
-
+
RelISeq(S) == {{<<n, x[n]>>:n \in 1..Len(x)} :x \in ISeq(S)}
\* The set of all injective sequences with elements of S
-RelISeqEleOf(S) == {p \in SUBSET(Nat \times S):
- LET d == {q[1] : q \in p}
+RelISeqEleOf(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
IN /\ Cardinality(p) = Cardinality(d)
/\ d = 1..Cardinality(d)
/\ Cardinality(p) = Cardinality(RelRange(p))}
-
+
RelISeq1(S) == RelISeq(S) \ {{}}
\* The set of all non-empty injective sequences with elements of S
-RelISeq1EleOf(S) == {p \in SUBSET(Nat \times S):
- LET d == {q[1] : q \in p}
+RelISeq1EleOf(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
IN /\ Cardinality(p) > 0
/\ Cardinality(p) = Cardinality(d)
/\ d = 1..Cardinality(d)
@@ -47,81 +47,88 @@ RelISeq1EleOf(S) == {p \in SUBSET(Nat \times S):
LOCAL SeqTest(s) == RelDomain(s) = 1..Cardinality(s)
\* Testing if s is a sequence
-
-RelSeqFirst(s) == IF SeqTest(s)
- THEN RelCall(s, 1)
- ELSE Assert(FALSE, "Error: The argument of the first-operator should be a sequence.")
+
+LOCAL WDcheck(val, condition, message) == IF Assert(condition, message) THEN val ELSE val
+
+RelSeqFirst(s) ==
+ WDcheck(RelCall(s, 1), SeqTest(s), "Error: The argument of the first-operator should be a sequence.")
\* The head of the sequence
-
-RelSeqLast(s) == IF SeqTest(s)
- THEN RelCall(s, Cardinality(s))
- ELSE Assert(FALSE, "Error: The argument of the last-operator should be a sequence.")
+
+RelSeqLast(s) ==
+ WDcheck(RelCall(s, Cardinality(s)), SeqTest(s), "Error: The argument of the last-operator should be a sequence.")
\* The last element of the sequence
-RelSeqSize(s) == IF SeqTest(s)
- THEN Cardinality(s)
- ELSE Assert(FALSE, "Error: The argument of the size-operator should be a sequence.")
+RelSeqSize(s) ==
+ WDcheck(Cardinality(s), SeqTest(s),"Error: The argument of the size-operator should be a sequence.")
\* The size of the sequence s
-
-RelSeqTail(s) == IF SeqTest(s)
- THEN {<<x[1]-1,x[2]>> : x \in {x \in s : x[1] # 1}}
- ELSE Assert(FALSE, "Error: The argument of the tail-operator should be a sequence.")
+
+RelSeqTail(s) ==
+ WDcheck({<<x[1]-1,x[2]>> : x \in {x \in s : x[1] # 1}}, SeqTest(s), "Error: The argument of the tail-operator should be a sequence.")
\* The tail of the sequence s
-
-RelSeqConcat(s1, s2) == IF SeqTest(s1) /\ SeqTest(s2)
- THEN s1 \cup {<<x[1]+Cardinality(s1), x[2]>> : x \in s2}
- ELSE Assert(FALSE, "Error: The arguments of the concatenation-operator should be sequences.")
+
+RelSeqConcat(s1, s2) ==
+ WDcheck(s1 \cup {<<x[1]+Cardinality(s1), x[2]>> : x \in s2} , SeqTest(s1) /\ SeqTest(s2), "Error: The arguments of the concatenation-operator should be sequences.")
\* The concatenation of sequence s1 and sequence s2
-
-RelSeqPrepand(e, s) == IF SeqTest(s)
- THEN {<<1,e>>} \cup {<<x[1]+1, x[2]>> : x \in s}
- ELSE Assert(FALSE, "Error: The second argument of the prepend-operator should be a sequence.")
- \* The sequence obtained by inserting e at the front of sequence s.
-
-RelSeqAppend(s, e) == IF SeqTest(s)
- THEN s \cup {<<Cardinality(s)+ 1,e>>}
- ELSE Assert(FALSE, "Error: The first argument of the append-operator should be a sequence.")
- \* The sequence obtained by appending e to the end of sequence s.
-
-RelSeqReverse(s) == IF SeqTest(s)
- THEN {<<Cardinality(s)-x[1]+1, x[2]>> : x \in s }
- ELSE Assert(FALSE, "Error: The argument of the reverse-operator should be a sequence.")
+
+RelSeqPrepand(e, s) ==
+ IF Assert(SeqTest(s), "Error: The second argument of the prepend-operator should be a sequence.")
+ THEN {<<1,e>>} \cup {<<x[1]+1, x[2]>> : x \in s}
+ ELSE {} \* dummy
+ \* The sequence obtained by inserting e at the front of sequence s.
+
+RelSeqAppend(s, e) ==
+ WDcheck(
+ s \cup {<<Cardinality(s)+ 1,e>>},
+ SeqTest(s),
+ "Error: The first argument of the append operator should be a sequence."
+ )
+ \* The sequence obtained by appending e to the end of sequence s.
+
+RelSeqReverse(s) ==
+ WDcheck(
+ {<<Cardinality(s)-x[1]+1, x[2]>> : x \in s },
+ SeqTest(s),
+ "Error: The argument of the 'rev' operator should be a sequence."
+ )
\* The sequence obtained by reversing the order of the elements.
-
-RelSeqFront(s) == IF SeqTest(s)
- THEN {x \in s : x[1] # Cardinality(s)}
- ELSE Assert(FALSE, "Error: The argument of the front-operator should be a sequence.")
- \* The front of the sequence s (all but last element)
+
+RelSeqFront(s) ==
+ WDcheck(
+ {x \in s : x[1] # Cardinality(s)},
+ SeqTest(s),
+ "Error: The argument of the front-operator should be a sequence."
+ )
+ \* The front of the sequence s (all but last element)
RECURSIVE RelSeqPerm(_)
-RelSeqPerm(S) == IF S = {}
+RelSeqPerm(S) == IF S = {}
THEN {{}}
ELSE LET ps == [x \in S |-> {RelSeqAppend(s, x): s \in RelSeqPerm(S\{x})}]
- IN UNION {ps[x]: x \in S}
+ IN UNION {ps[x]: x \in S}
(* The set of bijective sequences (permutations) *)
(* e.g. {<<1,2,3>>,<<2,1,3>>,<<2,3,1>>,<<3,1,2>>,<<3,2,1>>} for S = {1,2,3} *)
RECURSIVE RelSeqConc(_)
-RelSeqConc(S) ==
+RelSeqConc(S) ==
IF S = {}
THEN {}
ELSE RelSeqConcat(RelSeqFirst(S), RelSeqConc(RelSeqTail(S)) )
(* The sequence obtained by concatenating all sequences *)
(* which are elements of the sequence S. *)
-RelSeqTakeFirstElements(s, n) ==
- IF SeqTest(s) /\ n \in 0..Cardinality(s)
+RelSeqTakeFirstElements(s, n) ==
+ IF
+ /\ Assert(SeqTest(s), "Error: The first argument of the take-first-operator should be a sequence.")
+ /\ Assert(n \in 0..Cardinality(s), "The second argument of the take-first-operator is an invalid number.")
THEN {x \in s: x[1] \leq n}
- ELSE /\ Assert(n \in 0..Cardinality(s),
- "The second argument of the take-first-operator is an invalid number.")
- /\ Assert(FALSE, "Error: The first argument of the take-first-operator should be a sequence.")
+ ELSE {} \* dummy
\* The first n elements of s as a sequence
-
-RelSeqDropFirstElements(s, n) ==
- IF SeqTest(s) /\ n \in 0..Cardinality(s)
+
+RelSeqDropFirstElements(s, n) ==
+ IF /\ Assert(n \in 0..Cardinality(s),
+ "The second argument of the drop-first-operator is an invalid number.")
+ /\ Assert(SeqTest(s), "Error: The first argument of the drop-first-operator should be a sequence.")
THEN {<<x[1]-n,x[2]>> :x \in {x \in s: x[1] > n}}
- ELSE /\ Assert(n \in 0..Cardinality(s),
- "The second argument of the drop-first-operator is an invalid number.")
- /\ Assert(FALSE, "Error: The first argument of the drop-first-operator should be a sequence.")
+ ELSE {} \* dummy
\* The last n elements of s as a sequence
-=============================================================================
\ No newline at end of file
+=============================================================================