diff --git a/build.gradle b/build.gradle
index 1a3534069db76a39ad0ed6e42056d5e7edf68bcf..e923aec4563860df131604b47fde5c3c9bb55303 100644
--- a/build.gradle
+++ b/build.gradle
@@ -30,6 +30,7 @@ dependencies {
releaseJars (group: 'de.prob', name: 'prologlib', version: parser_version)
releaseJars (group: 'de.prob', name: 'parserbase', version: parser_version)
releaseJars (group: 'de.prob', name: 'bparser', version: parser_version)
+ releaseJars (group: 'de.prob', name: 'ltlparser', version: parser_version)
}
diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java
index e467d870e5d3b723303023842a512b0b269423c4..db8ff976dd82b97df67035c77f3f24abe371a086 100644
--- a/src/main/java/de/b2tla/B2TLA.java
+++ b/src/main/java/de/b2tla/B2TLA.java
@@ -33,7 +33,8 @@ public class B2TLA {
private String config;
private B2TlaTranslator translator;
private TLCOutputInfo tlcOutputInfo;
-
+ private String ltlFormula;
+
public static void main(String[] args) throws IOException {
StopWatch.start("Translation");
B2TLA b2tla = new B2TLA();
@@ -85,7 +86,7 @@ public class B2TLA {
tlcOutput.parseTLCOutput();
System.out.println("Model checking time: " + tlcOutput.getRunningTime()
+ " sec");
-
+
System.out.println("Result: " + tlcOutput.getError());
if (tlcOutput.hasTrace() && createTraceFile) {
StringBuilder trace = tlcOutput.getErrorTrace();
@@ -110,6 +111,15 @@ public class B2TLA {
Globals.invariant = false;
} else if (args[index].toLowerCase().equals("-tool")) {
Globals.tool = true;
+ } else if (args[index].toLowerCase().equals("-noltl")) {
+ Globals.checkltl = false;
+ } else if (args[index].toLowerCase().equals("-ltlformula")) {
+ index = index + 1;
+ if (index == args.length) {
+ throw new B2TLAIOException(
+ "Error: LTL formula requiered after option '-ltlformula'.");
+ }
+ ltlFormula = args[index];
} else if (args[index].charAt(0) == '-') {
throw new B2TLAIOException("Error: unrecognized option: "
+ args[index]);
@@ -134,7 +144,7 @@ public class B2TLA {
handleMainFileName();
if (Globals.translate) {
- translator = new B2TlaTranslator(machineName, getFile());
+ translator = new B2TlaTranslator(machineName, getFile(), this.ltlFormula);
translator.translate();
this.tlaModule = translator.getModuleString();
@@ -189,7 +199,7 @@ public class B2TLA {
STANDARD_MODULES.BBuiltIns)) {
createStandardModule(path, STANDARD_MODULES.BBuiltIns.toString());
}
-
+
if (translator.getUsedStandardModule().contains(
STANDARD_MODULES.FunctionsAsRelations)) {
createStandardModule(path,
diff --git a/src/main/java/de/b2tla/B2TlaTranslator.java b/src/main/java/de/b2tla/B2TlaTranslator.java
index 4006acbecc6a9f8416688e7ff56547b9fcde43ed..9327ff5e896c76a86983de8130b21f62e0deff71 100644
--- a/src/main/java/de/b2tla/B2TlaTranslator.java
+++ b/src/main/java/de/b2tla/B2TlaTranslator.java
@@ -9,14 +9,15 @@ import de.b2tla.analysis.ConstantsEliminator;
import de.b2tla.analysis.ConstantsEvaluator;
import de.b2tla.analysis.DefinitionsAnalyser;
import de.b2tla.analysis.MachineContext;
+import de.b2tla.analysis.UnchangedVariablesFinder;
import de.b2tla.analysis.PrecedenceCollector;
import de.b2tla.analysis.PrimedNodesMarker;
import de.b2tla.analysis.Renamer;
import de.b2tla.analysis.TypeRestrictor;
import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UnchangedVariablesFinder;
import de.b2tla.analysis.UsedStandardModules;
import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES;
+import de.b2tla.ltl.LTLFormulaVisitor;
import de.b2tla.prettyprint.TLAPrinter;
import de.b2tla.tla.Generator;
import de.b2tla.tlc.TLCOutputInfo;
@@ -31,6 +32,7 @@ public class B2TlaTranslator {
private String moduleString;
private String configString;
private String machineName;
+ private String ltlFormula;
private ArrayList<STANDARD_MODULES> usedStandardModules;
private TLCOutputInfo tlcOutputInfo;
@@ -42,9 +44,20 @@ public class B2TlaTranslator {
start.apply(ast2String2);
System.out.println(ast2String2.toString());
}
+
+ public B2TlaTranslator(String machineString, String ltlFormula) throws BException {
+ this.machineString = machineString;
+ this.ltlFormula = ltlFormula;
+ BParser parser = new BParser("Testing");
+ start = parser.parse(machineString, false);
+ final Ast2String ast2String2 = new Ast2String();
+ start.apply(ast2String2);
+ System.out.println(ast2String2.toString());
+ }
- public B2TlaTranslator(String machineName, File machineFile)
+ public B2TlaTranslator(String machineName, File machineFile, String ltlFormula)
throws IOException, BException {
+ this.ltlFormula = ltlFormula;
BParser parser = new BParser(machineName);
start = parser.parseFile(machineFile, false);
final Ast2String ast2String2 = new Ast2String();
@@ -53,13 +66,15 @@ public class B2TlaTranslator {
}
public void translate() {
-
- MachineContext machineContext = new MachineContext(start);
+
+ MachineContext machineContext = new MachineContext(start, ltlFormula);
this.machineName = machineContext.getMachineName();
+
Typechecker typechecker = new Typechecker(machineContext);
- UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
- machineContext);
+
+ UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(machineContext);
+
PrecedenceCollector precedenceCollector = new PrecedenceCollector(
start, typechecker.getTypes());
diff --git a/src/main/java/de/b2tla/Globals.java b/src/main/java/de/b2tla/Globals.java
index 71c4420a8bd6fac61430889c76f5fe0e71b97754..137921c1c0358d434dde441a77a55de1326237fd 100644
--- a/src/main/java/de/b2tla/Globals.java
+++ b/src/main/java/de/b2tla/Globals.java
@@ -10,6 +10,7 @@ public class Globals {
public static boolean runTLC = true;
public static boolean translate = true;
public static boolean invariant = true;
+ public static boolean checkltl = true;
public static boolean tool = false;
public static boolean deleteOnExit = false;
diff --git a/src/main/java/de/b2tla/Main.java b/src/main/java/de/b2tla/Main.java
deleted file mode 100644
index dca1eb77582078063017242fc1c798b719c00b1b..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/Main.java
+++ /dev/null
@@ -1,53 +0,0 @@
-package de.b2tla;
-import java.io.File;
-import java.io.IOException;
-import java.io.PrintWriter;
-import java.util.ArrayList;
-import java.util.List;
-
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
-import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Start;
-
-
-public class Main {
-
-
- public static void main(String[] args) throws IOException, BException {
-
-
- String filename = "M1.mch";
- final File machineFile = new File(filename);
- //final String probfilename = filename.substring(0, dot) + ".prob";
-
-
-
- BParser parser = new BParser(filename);
- Start tree = parser.parseFile(machineFile, false);
-
- //System.out.println(parser.getDefinitions().getDefinitionNames());
-
-
- RecursiveMachineLoader r = new RecursiveMachineLoader(machineFile.getParent(), parser.getContentProvider());
-
-
- List<Pragma> pragmas = new ArrayList<Pragma>();
- pragmas.addAll(parser.getPragmas());
- r.loadAllMachines(machineFile, tree, parser.getSourcePositions(), parser.getDefinitions(), pragmas);
-
- r.printAsProlog(new PrintWriter(System.out), false);
-
-
-// //System.out.println(r.getParsedMachines());
-// System.out.println(r.getParsedMachines().size());
-// for (String name : r.getParsedMachines().keySet()) {
-// System.out.print(name+ " ");
-// System.out.println(r.getParsedMachines().get(name));
-// }
-
-
- }
-
-}
diff --git a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java b/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
index db67446d4db38d4a3a53af641967c83fd165d394..f2a8d0b144e1a1e64ce4fb2d9c28ff8a83cae152 100644
--- a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
@@ -88,8 +88,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
getVariableList(node.getSubstitutions()));
/*
- * In the INITIALISATION clause all variables must be assigned. TODO
- * ouput parameter must be assigned too?
+ * In the INITIALISATION clause all variables must be assigned.
*/
HashSet<Node> allVariables = new HashSet<Node>(machineContext
.getVariables().values());
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
index acc969cd8afe965af8c865eab591abc4d9a17169..4b2d2a35b8f872be7ff239e7647989f110a68b1e 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
+++ b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
@@ -13,6 +13,14 @@ import de.be4.classicalb.core.parser.node.AIntegerExpression;
import de.be4.classicalb.core.parser.node.AIntervalExpression;
import de.be4.classicalb.core.parser.node.Node;
+/**
+ *
+ *
+ *
+ * @author hansen
+ *
+ */
+
public class DefinitionsAnalyser extends DepthFirstAdapter{
private MachineContext machineContext;
private HashMap<Node, Integer> deferredSetSizeTable;
@@ -60,6 +68,7 @@ public class DefinitionsAnalyser extends DepthFirstAdapter{
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
+ //TODO never reached
Node ref_node = machineContext.getReferences().get(node);
if(deferredSetSizeTable.containsKey(ref_node)){
try {
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsOrder.java b/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
index 579e13cec18a58df4004cfcbef3480e8ea0ba907..16a50a3fbbd35a33cfb49e1754d0be91156f1bc6 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
+++ b/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
@@ -14,6 +14,13 @@ import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
+/**
+ * A BDefinitions can depend on another BDefinitions. For the translation to
+ * TLA+ the definitions must be sorted.
+ *
+ * @author hansen
+ */
+
public class DefinitionsOrder extends DepthFirstAdapter {
private MachineContext machineContext;
private Hashtable<Node, HashSet<Node>> dependenciesTable;
@@ -25,7 +32,6 @@ public class DefinitionsOrder extends DepthFirstAdapter {
return allDefinitions;
}
-
public DefinitionsOrder(MachineContext machineContext,
ArrayList<PDefinition> allDefinitions) {
this.machineContext = machineContext;
@@ -35,9 +41,8 @@ public class DefinitionsOrder extends DepthFirstAdapter {
def.apply(this);
}
-
this.allDefinitions = sort(new ArrayList<PDefinition>(allDefinitions));
-
+
}
private ArrayList<PDefinition> sort(ArrayList<PDefinition> list) {
@@ -70,7 +75,7 @@ public class DefinitionsOrder extends DepthFirstAdapter {
}
}
}
-
+
if (result.size() != list.size()) {
throw new RuntimeException("Found cyclic Definitions.");
}
@@ -118,32 +123,32 @@ public class DefinitionsOrder extends DepthFirstAdapter {
}
public void inADefinitionExpression(ADefinitionExpression node) {
-
+
Node refNode = machineContext.getReferences().get(node);
/*
- * If refNode is null, then the whole branch was cloned when a constant assignment was generated
+ * If refNode is null, then the whole branch was cloned when a constant
+ * assignment was generated
*/
-
- if(null != refNode){
+
+ if (null != refNode) {
current.add(refNode);
}
-
+
}
public void inAIdentifierExpression(AIdentifierExpression node) {
Node identifierRef = machineContext.getReferences().get(node);
- if(identifierRef == null)
+ if (identifierRef == null)
return;
-
- if(machineContext.getConstants().containsValue(identifierRef)){
+
+ if (machineContext.getConstants().containsValue(identifierRef)) {
current.add(identifierRef);
return;
}
-
- if (machineContext.getReferences().get(identifierRef) instanceof PDefinition){
+
+ if (machineContext.getReferences().get(identifierRef) instanceof PDefinition) {
current.add(identifierRef);
}
-
-
+
}
}
diff --git a/src/main/java/de/b2tla/analysis/MachineContext.java b/src/main/java/de/b2tla/analysis/MachineContext.java
index a11c76027012ecafc7087da56d5cb0ddb57e9875..ef17d962b0d57c52f0b3cf23b13424de2f73315e 100644
--- a/src/main/java/de/b2tla/analysis/MachineContext.java
+++ b/src/main/java/de/b2tla/analysis/MachineContext.java
@@ -1,14 +1,18 @@
package de.b2tla.analysis;
import java.util.ArrayList;
+import java.util.Collection;
import java.util.Collections;
import java.util.Comparator;
+import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
import de.b2tla.exceptions.ScopeException;
+import de.b2tla.ltl.LTLBPredicate;
+import de.b2tla.ltl.LTLFormulaVisitor;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
@@ -41,6 +45,7 @@ import de.be4.classicalb.core.parser.node.AOpSubstitution;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.APrimedIdentifierExpression;
import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
@@ -50,6 +55,7 @@ import de.be4.classicalb.core.parser.node.ARecordFieldExpression;
import de.be4.classicalb.core.parser.node.ASeesMachineClause;
import de.be4.classicalb.core.parser.node.ASetsContextClause;
import de.be4.classicalb.core.parser.node.ASetsMachineClause;
+import de.be4.classicalb.core.parser.node.AStringExpression;
import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
import de.be4.classicalb.core.parser.node.Node;
@@ -69,6 +75,7 @@ public class MachineContext extends DepthFirstAdapter {
private PMachineHeader header;
private final Start start;
private final Hashtable<String, MachineContext> machineContextsTable;
+ private ArrayList<LTLFormulaVisitor> ltlVisitors;
// machine identifier
private final LinkedHashMap<String, Node> setParameter;
@@ -87,7 +94,7 @@ public class MachineContext extends DepthFirstAdapter {
private AAbstractMachineParseUnit abstractMachineParseUnit;
private AConstraintsMachineClause constraintMachineClause;
private ASeesMachineClause seesMachineClause;
- private ASetsContextClause setsMachineClause; // TODO
+ private ASetsContextClause setsMachineClause;
private AConstantsMachineClause constantsMachineClause;
private ADefinitionsMachineClause definitionMachineClause;
private APropertiesMachineClause propertiesMachineClause;
@@ -101,31 +108,39 @@ public class MachineContext extends DepthFirstAdapter {
private final Hashtable<Node, Node> referencesTable;
- public MachineContext(Start start,
- Hashtable<String, MachineContext> machineContextsTable) {
+ // public MachineContext(Start start,
+ // Hashtable<String, MachineContext> machineContextsTable) {
+ // this.start = start;
+ // this.ltlVisitors = new ArrayList<LTLFormulaVisitor>();
+ // this.referencesTable = new Hashtable<Node, Node>();
+ //
+ // this.setParameter = new LinkedHashMap<String, Node>();
+ // this.scalarParameter = new LinkedHashMap<String, Node>();
+ //
+ // this.deferredSets = new LinkedHashMap<String, Node>();
+ // this.enumeratedSets = new LinkedHashMap<String, Node>();
+ // this.enumValues = new LinkedHashMap<String, Node>();
+ // this.constants = new LinkedHashMap<String, Node>();
+ // this.definitions = new LinkedHashMap<String, Node>();
+ // this.variables = new LinkedHashMap<String, Node>();
+ // this.operations = new LinkedHashMap<String, Node>();
+ // this.seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
+ //
+ // this.machineContextsTable = machineContextsTable;
+ //
+ // start.apply(this);
+ // }
+
+ public MachineContext(Start start, String ltlFormula) {
this.start = start;
this.referencesTable = new Hashtable<Node, Node>();
+ this.ltlVisitors = new ArrayList<LTLFormulaVisitor>();
- this.setParameter = new LinkedHashMap<String, Node>();
- this.scalarParameter = new LinkedHashMap<String, Node>();
-
- this.deferredSets = new LinkedHashMap<String, Node>();
- this.enumeratedSets = new LinkedHashMap<String, Node>();
- this.enumValues = new LinkedHashMap<String, Node>();
- this.constants = new LinkedHashMap<String, Node>();
- this.definitions = new LinkedHashMap<String, Node>();
- this.variables = new LinkedHashMap<String, Node>();
- this.operations = new LinkedHashMap<String, Node>();
- this.seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
-
- this.machineContextsTable = machineContextsTable;
-
- start.apply(this);
- }
-
- public MachineContext(Start start) {
- this.start = start;
- this.referencesTable = new Hashtable<Node, Node>();
+ LTLFormulaVisitor ltlVisitor = null;
+ if (null != ltlFormula) {
+ ltlVisitor = new LTLFormulaVisitor("ltl", ltlFormula, this);
+ this.ltlVisitors.add(ltlVisitor);
+ }
this.setParameter = new LinkedHashMap<String, Node>();
this.scalarParameter = new LinkedHashMap<String, Node>();
@@ -141,6 +156,34 @@ public class MachineContext extends DepthFirstAdapter {
this.machineContextsTable = new Hashtable<String, MachineContext>();
start.apply(this);
+
+ checkLTLFormulas();
+ }
+
+ private void checkLTLFormulas() {
+ for (int i = 0; i < ltlVisitors.size(); i++) {
+ LTLFormulaVisitor visitor = ltlVisitors.get(i);
+ visitor.start();
+ }
+ }
+
+ public void checkLTLBPredicate(LTLBPredicate ltlbPredicate) {
+ contextTable = new ArrayList<LinkedHashMap<String, Node>>();
+ contextTable.add(getDeferredSets());
+ contextTable.add(getEnumeratedSets());
+ contextTable.add(getEnumValues());
+ contextTable.add(getConstants());
+ contextTable.add(getVariables());
+ contextTable.add(getDefinitions());
+
+ LinkedHashMap<String, Node> identifierHashTable = ltlbPredicate
+ .getIdentifierList();
+ if (identifierHashTable.size() > 0) {
+ LinkedHashMap<String, Node> currentContext = new LinkedHashMap<String, Node>();
+ currentContext.putAll(identifierHashTable);
+ contextTable.add(currentContext);
+ }
+ ltlbPredicate.getBFormula().apply(this);
}
private void exist(LinkedList<TIdentifierLiteral> list) {
@@ -204,6 +247,12 @@ public class MachineContext extends DepthFirstAdapter {
}
}
+ @Override
+ public void caseAPredicateParseUnit(APredicateParseUnit node) {
+
+ node.getPredicate().apply(this);
+ }
+
/**
* Definitions
*/
@@ -211,16 +260,32 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
definitionMachineClause = node;
- List<PDefinition> copy = new ArrayList<PDefinition>(
- node.getDefinitions());
+ List<PDefinition> copy = node.getDefinitions();
/*
* The definitions are not in a predefined order. In particular
* definitions can depend on each other. First all definitions are added
* to the definitions context table. Then all definitions are visited.
*/
+ Collection<PDefinition> definitionsToRemove = new HashSet<PDefinition>();
+
for (PDefinition e : copy) {
if (e instanceof AExpressionDefinitionDefinition) {
+ AExpressionDefinitionDefinition def = (AExpressionDefinitionDefinition) e;
+ String name = def.getName().getText();
+ if (name.startsWith("ASSERT_LTL")) {
+ try {
+ AStringExpression stringNode = (AStringExpression) def
+ .getRhs();
+ LTLFormulaVisitor visitor = new LTLFormulaVisitor(name,
+ stringNode.getContent().getText(), this);
+ this.ltlVisitors.add(visitor);
+ } catch (ClassCastException castException) {
+ throw new ScopeException(
+ "Error: LTL formula is not in a string representation.");
+ }
+ definitionsToRemove.add(def);
+ }
evalDefinitionName(((AExpressionDefinitionDefinition) e)
.getName().getText().toString(), e);
} else if (e instanceof APredicateDefinitionDefinition) {
@@ -231,7 +296,12 @@ public class MachineContext extends DepthFirstAdapter {
.getName().getText().toString(), e);
}
}
-
+ /*
+ * At this point all ASSERT_LTL formulas of the definitions are removed.
+ * LTL formulas are stored in the Arraylist {@value #ltlVisitors}.
+ */
+ copy.removeAll(definitionsToRemove);
+
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
ArrayList<MachineContext> list = lookupExtendedMachines();
for (int i = 0; i < list.size(); i++) {
@@ -250,7 +320,7 @@ public class MachineContext extends DepthFirstAdapter {
}
private void evalDefinitionName(String name, Node node) {
- if (name.equals("ASSERT_LTL")) {
+ if (name.startsWith("ASSERT_LTL")) {
return;
}
existString(name);
@@ -646,8 +716,11 @@ public class MachineContext extends DepthFirstAdapter {
if (e instanceof AFunctionExpression) {
contextTable = varTable;
((AFunctionExpression) e).getIdentifier().apply(this);
+
+ // full context table
+ contextTable = temp;
for (Node n : ((AFunctionExpression) e).getParameters()) {
- contextTable = temp;
+
n.apply(this);
}
} else {
@@ -918,6 +991,10 @@ public class MachineContext extends DepthFirstAdapter {
return referencesTable;
}
+ public ArrayList<LTLFormulaVisitor> getLTLFormulas() {
+ return ltlVisitors;
+ }
+
/*
* machine clauses getter
*/
diff --git a/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java b/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
index ee7f92d39c98b4e489d7f6297361d570184871a0..812568b139a05f82552e855b6a57a09ad8ea183b 100644
--- a/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
+++ b/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
@@ -1,3 +1,7 @@
+
+/*
+ * currently not used
+ */
package de.b2tla.analysis;
import java.util.ArrayList;
diff --git a/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java b/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java
deleted file mode 100644
index d9bb6cd1088fbb90071d579e1fb0d72bd1cbbc84..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/analysis/MissingVariablesFinder.java
+++ /dev/null
@@ -1,315 +0,0 @@
-package de.b2tla.analysis;
-
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.List;
-
-import de.b2tla.exceptions.SubstitutionException;
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AAnySubstitution;
-import de.be4.classicalb.core.parser.node.AAssertionSubstitution;
-import de.be4.classicalb.core.parser.node.AAssignSubstitution;
-import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
-import de.be4.classicalb.core.parser.node.ABlockSubstitution;
-import de.be4.classicalb.core.parser.node.AChoiceOrSubstitution;
-import de.be4.classicalb.core.parser.node.AChoiceSubstitution;
-import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
-import de.be4.classicalb.core.parser.node.AIfSubstitution;
-import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
-import de.be4.classicalb.core.parser.node.ALetSubstitution;
-import de.be4.classicalb.core.parser.node.AOperation;
-import de.be4.classicalb.core.parser.node.AParallelSubstitution;
-import de.be4.classicalb.core.parser.node.APreconditionSubstitution;
-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.PExpression;
-import de.be4.classicalb.core.parser.node.PSubstitution;
-
-/**
- * This class is a tree walker which calculates all missing variables
- * assignments for each node inside a operation body. Missing variables
- * assignments correspond to unchanged variables in TLA+. B definitions or the
- * initialisation are not visited by this class.
- *
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- *
- */
-
-class MissingVariablesFinder extends DepthFirstAdapter {
- private final MachineContext machineContext;
- private final Hashtable<Node, HashSet<Node>> assignedIdentifiersTable;
-
- // this table contains a set of all variables which must be assigned in the
- // node or in the sub nodes of the node
- private final Hashtable<Node, HashSet<Node>> expectedVariablesTable;
- private final Hashtable<Node, HashSet<Node>> expectedOutputParametersTable;
-
- private final Hashtable<Node, HashSet<Node>> missingVariablesTable;
-
- private final Hashtable<Node, HashSet<Node>> missingVariablesNull;
-
- public Hashtable<Node, HashSet<Node>> getMissingVariablesTable() {
- return missingVariablesTable;
- }
-
- public Hashtable<Node, HashSet<Node>> getMissingVariablesNull() {
- return missingVariablesNull;
- }
-
- public MissingVariablesFinder(MachineContext c,
- Hashtable<Node, HashSet<Node>> assignedVariablesTable) {
- this.machineContext = c;
- this.assignedIdentifiersTable = assignedVariablesTable;
-
- this.expectedVariablesTable = new Hashtable<Node, HashSet<Node>>();
- this.expectedOutputParametersTable = new Hashtable<Node, HashSet<Node>>();
-
- this.missingVariablesTable = new Hashtable<Node, HashSet<Node>>();
- this.missingVariablesNull = new Hashtable<Node, HashSet<Node>>();
-
- c.getTree().apply(this);
- }
-
- @Override
- public void caseAInitialisationMachineClause(
- AInitialisationMachineClause node) {
- }
-
- @Override
- public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
- }
-
- @Override
- public void caseAOperation(AOperation node) {
- HashSet<Node> expectedOutputParameter = new HashSet<Node>();
- List<PExpression> returnValues = new ArrayList<PExpression>(
- node.getReturnValues());
- for (PExpression e : returnValues) {
- expectedOutputParameter.add(e);
- }
-
- Node body = node.getOperationBody();
- expectedOutputParametersTable.put(body, expectedOutputParameter);
- expectedVariablesTable.put(body, new HashSet<Node>(machineContext
- .getVariables().values()));
-
- body.apply(this);
-
- // missingVariablesTable.put(node, missingVariablesTable.get(body));
- }
-
- private void check(Node node) {
- HashSet<Node> found = assignedIdentifiersTable.get(node);
- HashSet<Node> missingVariables = new HashSet<Node>(
- expectedVariablesTable.get(node));
- missingVariables.removeAll(found);
- missingVariablesTable.put(node, missingVariables);
-
- HashSet<Node> missingOutputParameter = new HashSet<Node>(
- expectedOutputParametersTable.get(node));
- missingOutputParameter.removeAll(found);
- if (missingOutputParameter.size() > 0) {
- throw new SubstitutionException(
- "To the following output parameters no values are assigned: "
- + missingOutputParameter);
- }
- }
-
- @Override
- public void caseAAssignSubstitution(AAssignSubstitution node) {
- check(node);
- }
-
- @Override
- public void caseABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
- check(node);
- }
-
- @Override
- public void caseAParallelSubstitution(AParallelSubstitution node) {
- check(node);
-
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getSubstitutions());
- for (PSubstitution e : copy) {
-
- expectedOutputParametersTable.put(e, new HashSet<Node>());
- expectedVariablesTable.put(e, new HashSet<Node>());
- e.apply(this);
- }
- }
-
- @Override
- public void caseAAnySubstitution(AAnySubstitution node) {
- check(node);
-
- expectedOutputParametersTable.put(node.getThen(), new HashSet<Node>());
- expectedVariablesTable.put(node.getThen(), new HashSet<Node>());
- node.getThen().apply(this);
- }
-
- @Override
- public void caseALetSubstitution(ALetSubstitution node) {
- check(node);
-
- expectedOutputParametersTable.put(node.getSubstitution(),
- new HashSet<Node>());
- expectedVariablesTable.put(node.getSubstitution(), new HashSet<Node>());
- node.getSubstitution().apply(this);
- }
-
- @Override
- public void caseAChoiceSubstitution(AChoiceSubstitution node) {
- check(node);
-
- // Separating variables and output parameters
- HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
- HashSet<Node> variables = new HashSet<Node>(foundIdentifiers);
- variables.removeAll(expectedOutputParametersTable.get(node));
-
- // System.out.println(parameters);
-
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getSubstitutions());
- for (PSubstitution e : copy) {
- // each child of CHOICE must assign all variables and all output
- // parameter
- expectedOutputParametersTable.put(e,
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(e, variables);
- e.apply(this);
- }
- }
-
- @Override
- public void caseAChoiceOrSubstitution(AChoiceOrSubstitution node) {
- Node sub = node.getSubstitution();
- expectedOutputParametersTable.put(sub,
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(sub, expectedVariablesTable.get(node));
-
- sub.apply(this);
-
- missingVariablesTable.put(node, missingVariablesTable.get(sub));
-
- }
-
- @Override
- public void caseAIfSubstitution(AIfSubstitution node) {
- check(node);
-
- // Separating variables and output parameters
- HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
- HashSet<Node> foundVariables = new HashSet<Node>(foundIdentifiers);
- foundVariables.removeAll(expectedOutputParametersTable.get(node));
-
- expectedOutputParametersTable.put(node.getThen(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getThen(), foundVariables);
- node.getThen().apply(this);
-
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getElsifSubstitutions());
- for (PSubstitution e : copy) {
- expectedOutputParametersTable.put(e,
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(e, foundVariables);
- e.apply(this);
- }
-
- if (node.getElse() != null) {
- expectedOutputParametersTable.put(node.getElse(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getElse(), foundVariables);
- node.getElse().apply(this);
- } else {
- missingVariablesNull.put(node,
- assignedIdentifiersTable.get(node.getThen()));
- }
-
- }
-
- @Override
- public void caseAPreconditionSubstitution(APreconditionSubstitution node) {
- // check(node);
- //
- // // Separating variables and output parameters
- // HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
- // System.out.println(foundIdentifiers);
- // HashSet<Node> foundVariables = new HashSet<Node>(foundIdentifiers);
- // foundVariables.removeAll(expectedOutputParametersTable.get(node));
-
- expectedOutputParametersTable.put(node.getSubstitution(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getSubstitution(),
- expectedVariablesTable.get(node));
- node.getSubstitution().apply(this);
- }
-
- @Override
- public void caseAAssertionSubstitution(AAssertionSubstitution node) {
- expectedOutputParametersTable.put(node.getSubstitution(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getSubstitution(),
- expectedVariablesTable.get(node));
- node.getSubstitution().apply(this);
- }
-
- @Override
- public void caseABlockSubstitution(ABlockSubstitution node) {
- expectedOutputParametersTable.put(node.getSubstitution(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getSubstitution(),
- expectedVariablesTable.get(node));
- node.getSubstitution().apply(this);
- }
-
- @Override
- public void caseASelectSubstitution(ASelectSubstitution node) {
- check(node);
- // Separating variables and output parameters
- HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
- HashSet<Node> variables = new HashSet<Node>(foundIdentifiers);
- variables.removeAll(expectedOutputParametersTable.get(node));
-
- expectedOutputParametersTable.put(node.getThen(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getThen(), variables);
- node.getThen().apply(this);
- {
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getWhenSubstitutions());
- for (PSubstitution e : copy) {
- expectedOutputParametersTable.put(e,
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(e, variables);
- e.apply(this);
- }
- }
-
- if (node.getElse() != null) {
- expectedOutputParametersTable.put(node.getElse(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getElse(), variables);
- node.getElse().apply(this);
- }
- }
-
- @Override
- public void caseASelectWhenSubstitution(ASelectWhenSubstitution node) {
- check(node);
- expectedOutputParametersTable.put(node.getSubstitution(),
- expectedOutputParametersTable.get(node));
- expectedVariablesTable.put(node.getSubstitution(),
- expectedVariablesTable.get(node));
- node.getSubstitution().apply(this);
- }
-
- @Override
- public void caseASkipSubstitution(ASkipSubstitution node) {
- check(node);
- }
-}
diff --git a/src/main/java/de/b2tla/analysis/TypeRestrictor.java b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
index 1e15f7d514ee07d8b801779cb7a77768e933d695..be2ec09bf54533107cfdef570ad12d2d8e6d1760 100644
--- a/src/main/java/de/b2tla/analysis/TypeRestrictor.java
+++ b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
@@ -9,6 +9,8 @@ import de.b2tla.analysis.nodes.ElementOfNode;
import de.b2tla.analysis.nodes.EqualsNode;
import de.b2tla.analysis.nodes.NodeType;
import de.b2tla.analysis.nodes.SubsetNode;
+import de.b2tla.ltl.LTLBPredicate;
+import de.b2tla.ltl.LTLFormulaVisitor;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
@@ -26,6 +28,7 @@ import de.be4.classicalb.core.parser.node.ALetSubstitution;
import de.be4.classicalb.core.parser.node.AMemberPredicate;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.APreconditionSubstitution;
+import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression;
@@ -35,6 +38,8 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PSubstitution;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.ltl.core.parser.node.AExistsLtl;
+import de.be4.ltl.core.parser.node.AForallLtl;
public class TypeRestrictor extends DepthFirstAdapter {
@@ -54,6 +59,31 @@ public class TypeRestrictor extends DepthFirstAdapter {
start.apply(this);
+ checkLTLFormulas();
+ }
+
+ private void checkLTLFormulas() {
+ for (LTLFormulaVisitor visitor : machineContext.getLTLFormulas()) {
+
+ for (de.be4.ltl.core.parser.node.Node ltlNode : visitor
+ .getUnparsedHashTable().keySet()) {
+ Node bNode = visitor.getBAst(ltlNode);
+
+ if(ltlNode instanceof AExistsLtl){
+ Node id = visitor.getLTLIdentifier(((AExistsLtl) ltlNode).getExistsIdentifier().getText());
+ HashSet<Node> list = new HashSet<Node>();
+ list.add(id);
+ analysePredicate(bNode, list);
+ }else if (ltlNode instanceof AForallLtl){
+ Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode).getForallIdentifier().getText());
+ HashSet<Node> list = new HashSet<Node>();
+ list.add(id);
+ analysePredicate(bNode, list);
+ }
+ bNode.apply(this);
+ }
+
+ }
}
public ArrayList<NodeType> getRestrictedTypesSet(Node node) {
@@ -153,7 +183,15 @@ public class TypeRestrictor extends DepthFirstAdapter {
analysePredicate(((AConjunctPredicate) n).getRight(), list);
return;
}
-
+
+ if(n instanceof Start){
+ analysePredicate(((Start) n).getPParseUnit(), list);
+ }
+
+ if(n instanceof APredicateParseUnit){
+ analysePredicate(((APredicateParseUnit) n).getPredicate(), list);
+ return;
+ }
}
@Override
@@ -236,9 +274,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicates(), list);
}
-
- public void inAGeneralProductExpression(AGeneralProductExpression node)
- {
+
+ public void inAGeneralProductExpression(AGeneralProductExpression node) {
HashSet<Node> list = new HashSet<Node>();
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
@@ -246,8 +283,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list);
- }
-
+ }
private Hashtable<Node, HashSet<Node>> expectedIdentifieListTable = new Hashtable<Node, HashSet<Node>>();
diff --git a/src/main/java/de/b2tla/analysis/Typechecker.java b/src/main/java/de/b2tla/analysis/Typechecker.java
index ff335453d6038630fffbb6cb1a6334e21e4eca8e..fc6eb771a3a17408d3ee49153656792e4f7237a1 100644
--- a/src/main/java/de/b2tla/analysis/Typechecker.java
+++ b/src/main/java/de/b2tla/analysis/Typechecker.java
@@ -1,6 +1,7 @@
package de.b2tla.analysis;
import java.util.ArrayList;
+import java.util.Collection;
import java.util.Collections;
import java.util.Hashtable;
import java.util.LinkedHashMap;
@@ -23,6 +24,8 @@ import de.b2tla.btypes.StructType;
import de.b2tla.btypes.UntypedType;
import de.b2tla.exceptions.TypeErrorException;
import de.b2tla.exceptions.UnificationException;
+import de.b2tla.ltl.LTLBPredicate;
+import de.b2tla.ltl.LTLFormulaVisitor;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
@@ -36,12 +39,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
private final Hashtable<Node, BType> types;
private final Hashtable<Node, Node> referenceTable;
- private final MachineContext context;
+ private final MachineContext machineContext;
public Typechecker(MachineContext machineContext,
Hashtable<String, MachineContext> contextTable,
Hashtable<String, Typechecker> typecheckerTable) {
- this.context = machineContext;
+ this.machineContext = machineContext;
this.types = new Hashtable<Node, BType>();
this.referenceTable = machineContext.getReferences();
}
@@ -49,8 +52,32 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public Typechecker(MachineContext c) {
this.types = new Hashtable<Node, BType>();
this.referenceTable = c.getReferences();
- this.context = c;
+ this.machineContext = c;
c.getTree().apply(this);
+
+ checkLTLFormulas();
+ }
+
+ private void checkLTLFormulas() {
+ ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
+ for (int i = 0; i < visitors.size(); i++) {
+ LTLFormulaVisitor visitor = visitors.get(i);
+ Collection<AIdentifierExpression> parameter = visitor.getParameter();
+ for (AIdentifierExpression param : parameter) {
+ setType(param, new UntypedType());
+ }
+ for (int j = 0; j < visitor.getBPredicates().size(); j++) {
+ LTLBPredicate ltlBPredicate = visitor.getBPredicates().get(j);
+ ltlBPredicate.getBFormula().apply(this);
+ }
+ }
+
+ }
+
+ @Override
+ public void caseAPredicateParseUnit(APredicateParseUnit node) {
+ setType(node.getPredicate(), BoolType.getInstance());
+ node.getPredicate().apply(this);
}
public Hashtable<Node, BType> getTypes() {
@@ -58,7 +85,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
public MachineContext getContext() {
- return context;
+ return machineContext;
}
public void setType(Node node, BType t) {
@@ -266,7 +293,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- LinkedHashMap<String, Node> parameter = context.getScalarParameter();
+ LinkedHashMap<String, Node> parameter = machineContext
+ .getScalarParameter();
for (String c : parameter.keySet()) {
Node n = parameter.get(c);
if (getType(n).isUntyped()) {
@@ -282,7 +310,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- LinkedHashMap<String, Node> constants = context.getConstants();
+ LinkedHashMap<String, Node> constants = machineContext.getConstants();
for (String c : constants.keySet()) {
Node n = constants.get(c);
if (getType(n).isUntyped()) {
@@ -296,7 +324,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseAInvariantMachineClause(AInvariantMachineClause node) {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
- LinkedHashMap<String, Node> variables = context.getVariables();
+ LinkedHashMap<String, Node> variables = machineContext.getVariables();
for (String c : variables.keySet()) {
Node n = variables.get(c);
if (getType(n).isUntyped()) {
diff --git a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java b/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
index c4416bbc2c0c2bc61f206efc12f88894beeedad2..863a18bcb950de5ff9c8de91e33f56e66ebd8a50 100644
--- a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
@@ -1,38 +1,316 @@
package de.b2tla.analysis;
+import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
+import java.util.List;
-
+import de.b2tla.exceptions.SubstitutionException;
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AAnySubstitution;
+import de.be4.classicalb.core.parser.node.AAssertionSubstitution;
+import de.be4.classicalb.core.parser.node.AAssignSubstitution;
+import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
+import de.be4.classicalb.core.parser.node.ABlockSubstitution;
+import de.be4.classicalb.core.parser.node.AChoiceOrSubstitution;
+import de.be4.classicalb.core.parser.node.AChoiceSubstitution;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
+import de.be4.classicalb.core.parser.node.AIfSubstitution;
+import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
+import de.be4.classicalb.core.parser.node.ALetSubstitution;
+import de.be4.classicalb.core.parser.node.AOperation;
+import de.be4.classicalb.core.parser.node.AParallelSubstitution;
+import de.be4.classicalb.core.parser.node.APreconditionSubstitution;
+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.PExpression;
+import de.be4.classicalb.core.parser.node.PSubstitution;
/**
+ * This class is a tree walker which calculates all missing variables
+ * assignments for each node inside a operation body. Missing variables
+ * assignments correspond to unchanged variables in TLA+. B definitions or the
+ * initialisation are not visited by this class.
*
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
*
*/
-public class UnchangedVariablesFinder {
+
+public class UnchangedVariablesFinder extends DepthFirstAdapter {
+ private final MachineContext machineContext;
+ private final Hashtable<Node, HashSet<Node>> assignedIdentifiersTable;
+
+ // this table contains a set of all variables which must be assigned in the
+ // node or in the sub nodes of the node
+ private final Hashtable<Node, HashSet<Node>> expectedVariablesTable;
+ private final Hashtable<Node, HashSet<Node>> expectedOutputParametersTable;
+
private final Hashtable<Node, HashSet<Node>> unchangedVariablesTable;
+
private final Hashtable<Node, HashSet<Node>> unchangedVariablesNull;
-
- public Hashtable<Node, HashSet<Node>> getUnchangedVariablesTable() {
- return unchangedVariablesTable;
+
+ public HashSet<Node> getUnchangedVariables(Node node){
+ return unchangedVariablesTable.get(node);
}
- public Hashtable<Node, HashSet<Node>> getUnchangedVariablesNull() {
- return unchangedVariablesNull;
+ public HashSet<Node> getUnchangedVariablesNull(Node node) {
+ return unchangedVariablesNull.get(node);
}
public UnchangedVariablesFinder(MachineContext c) {
-// Start start = c.getTree();
+ this.machineContext = c;
AssignedVariablesFinder aVF = new AssignedVariablesFinder(c);
- //start.apply(aVF);
- // assignedVariablesTable = aVF.getAssignedVariablesTable();
- MissingVariablesFinder mVF = new MissingVariablesFinder(c,
- aVF.getAssignedVariablesTable());
- //start.apply(mVF);
- this.unchangedVariablesTable = mVF.getMissingVariablesTable();
- this.unchangedVariablesNull = mVF.getMissingVariablesNull();
- }
-}
\ No newline at end of file
+ this.assignedIdentifiersTable = aVF.getAssignedVariablesTable();
+
+ this.expectedVariablesTable = new Hashtable<Node, HashSet<Node>>();
+ this.expectedOutputParametersTable = new Hashtable<Node, HashSet<Node>>();
+
+ this.unchangedVariablesTable = new Hashtable<Node, HashSet<Node>>();
+ this.unchangedVariablesNull = new Hashtable<Node, HashSet<Node>>();
+
+ c.getTree().apply(this);
+ }
+
+ @Override
+ public void caseAInitialisationMachineClause(
+ AInitialisationMachineClause node) {
+ }
+
+ @Override
+ public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
+ }
+
+ @Override
+ public void caseAOperation(AOperation node) {
+ HashSet<Node> expectedOutputParameter = new HashSet<Node>();
+ List<PExpression> returnValues = new ArrayList<PExpression>(
+ node.getReturnValues());
+ for (PExpression e : returnValues) {
+ expectedOutputParameter.add(e);
+ }
+
+ Node body = node.getOperationBody();
+ expectedOutputParametersTable.put(body, expectedOutputParameter);
+ expectedVariablesTable.put(body, new HashSet<Node>(machineContext
+ .getVariables().values()));
+
+ body.apply(this);
+
+ // missingVariablesTable.put(node, missingVariablesTable.get(body));
+ }
+
+ private void check(Node node) {
+ HashSet<Node> found = assignedIdentifiersTable.get(node);
+ HashSet<Node> missingVariables = new HashSet<Node>(
+ expectedVariablesTable.get(node));
+ missingVariables.removeAll(found);
+ unchangedVariablesTable.put(node, missingVariables);
+
+ HashSet<Node> missingOutputParameter = new HashSet<Node>(
+ expectedOutputParametersTable.get(node));
+ missingOutputParameter.removeAll(found);
+ if (missingOutputParameter.size() > 0) {
+ throw new SubstitutionException(
+ "To the following output parameters no values are assigned: "
+ + missingOutputParameter);
+ }
+ }
+
+ @Override
+ public void caseAAssignSubstitution(AAssignSubstitution node) {
+ check(node);
+ }
+
+ @Override
+ public void caseABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
+ check(node);
+ }
+
+ @Override
+ public void caseAParallelSubstitution(AParallelSubstitution node) {
+ check(node);
+
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getSubstitutions());
+ for (PSubstitution e : copy) {
+
+ expectedOutputParametersTable.put(e, new HashSet<Node>());
+ expectedVariablesTable.put(e, new HashSet<Node>());
+ e.apply(this);
+ }
+ }
+
+ @Override
+ public void caseAAnySubstitution(AAnySubstitution node) {
+ check(node);
+
+ expectedOutputParametersTable.put(node.getThen(), new HashSet<Node>());
+ expectedVariablesTable.put(node.getThen(), new HashSet<Node>());
+ node.getThen().apply(this);
+ }
+
+ @Override
+ public void caseALetSubstitution(ALetSubstitution node) {
+ check(node);
+
+ expectedOutputParametersTable.put(node.getSubstitution(),
+ new HashSet<Node>());
+ expectedVariablesTable.put(node.getSubstitution(), new HashSet<Node>());
+ node.getSubstitution().apply(this);
+ }
+
+ @Override
+ public void caseAChoiceSubstitution(AChoiceSubstitution node) {
+ check(node);
+
+ // Separating variables and output parameters
+ HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
+ HashSet<Node> variables = new HashSet<Node>(foundIdentifiers);
+ variables.removeAll(expectedOutputParametersTable.get(node));
+
+ // System.out.println(parameters);
+
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getSubstitutions());
+ for (PSubstitution e : copy) {
+ // each child of CHOICE must assign all variables and all output
+ // parameter
+ expectedOutputParametersTable.put(e,
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(e, variables);
+ e.apply(this);
+ }
+ }
+
+ @Override
+ public void caseAChoiceOrSubstitution(AChoiceOrSubstitution node) {
+ Node sub = node.getSubstitution();
+ expectedOutputParametersTable.put(sub,
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(sub, expectedVariablesTable.get(node));
+
+ sub.apply(this);
+
+ unchangedVariablesTable.put(node, unchangedVariablesTable.get(sub));
+
+ }
+
+ @Override
+ public void caseAIfSubstitution(AIfSubstitution node) {
+ check(node);
+
+ // Separating variables and output parameters
+ HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
+ HashSet<Node> foundVariables = new HashSet<Node>(foundIdentifiers);
+ foundVariables.removeAll(expectedOutputParametersTable.get(node));
+
+ expectedOutputParametersTable.put(node.getThen(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getThen(), foundVariables);
+ node.getThen().apply(this);
+
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getElsifSubstitutions());
+ for (PSubstitution e : copy) {
+ expectedOutputParametersTable.put(e,
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(e, foundVariables);
+ e.apply(this);
+ }
+
+ if (node.getElse() != null) {
+ expectedOutputParametersTable.put(node.getElse(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getElse(), foundVariables);
+ node.getElse().apply(this);
+ } else {
+ unchangedVariablesNull.put(node,
+ assignedIdentifiersTable.get(node.getThen()));
+ }
+
+ }
+
+ @Override
+ public void caseAPreconditionSubstitution(APreconditionSubstitution node) {
+ // check(node);
+ //
+ // // Separating variables and output parameters
+ // HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
+ // System.out.println(foundIdentifiers);
+ // HashSet<Node> foundVariables = new HashSet<Node>(foundIdentifiers);
+ // foundVariables.removeAll(expectedOutputParametersTable.get(node));
+
+ expectedOutputParametersTable.put(node.getSubstitution(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getSubstitution(),
+ expectedVariablesTable.get(node));
+ node.getSubstitution().apply(this);
+ }
+
+ @Override
+ public void caseAAssertionSubstitution(AAssertionSubstitution node) {
+ expectedOutputParametersTable.put(node.getSubstitution(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getSubstitution(),
+ expectedVariablesTable.get(node));
+ node.getSubstitution().apply(this);
+ }
+
+ @Override
+ public void caseABlockSubstitution(ABlockSubstitution node) {
+ expectedOutputParametersTable.put(node.getSubstitution(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getSubstitution(),
+ expectedVariablesTable.get(node));
+ node.getSubstitution().apply(this);
+ }
+
+ @Override
+ public void caseASelectSubstitution(ASelectSubstitution node) {
+ check(node);
+ // Separating variables and output parameters
+ HashSet<Node> foundIdentifiers = assignedIdentifiersTable.get(node);
+ HashSet<Node> variables = new HashSet<Node>(foundIdentifiers);
+ variables.removeAll(expectedOutputParametersTable.get(node));
+
+ expectedOutputParametersTable.put(node.getThen(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getThen(), variables);
+ node.getThen().apply(this);
+ {
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getWhenSubstitutions());
+ for (PSubstitution e : copy) {
+ expectedOutputParametersTable.put(e,
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(e, variables);
+ e.apply(this);
+ }
+ }
+
+ if (node.getElse() != null) {
+ expectedOutputParametersTable.put(node.getElse(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getElse(), variables);
+ node.getElse().apply(this);
+ }
+ }
+
+ @Override
+ public void caseASelectWhenSubstitution(ASelectWhenSubstitution node) {
+ check(node);
+ expectedOutputParametersTable.put(node.getSubstitution(),
+ expectedOutputParametersTable.get(node));
+ expectedVariablesTable.put(node.getSubstitution(),
+ expectedVariablesTable.get(node));
+ node.getSubstitution().apply(this);
+ }
+
+ @Override
+ public void caseASkipSubstitution(ASkipSubstitution node) {
+ check(node);
+ }
+}
diff --git a/src/main/java/de/b2tla/exceptions/LTLParseException.java b/src/main/java/de/b2tla/exceptions/LTLParseException.java
new file mode 100644
index 0000000000000000000000000000000000000000..74c017d00ae0a23895bf22ef8502af75c30e560e
--- /dev/null
+++ b/src/main/java/de/b2tla/exceptions/LTLParseException.java
@@ -0,0 +1,15 @@
+package de.b2tla.exceptions;
+
+@SuppressWarnings("serial")
+public class LTLParseException extends B2tlaException{
+
+ public LTLParseException(String e) {
+ super(e);
+ }
+
+ @Override
+ public String getError() {
+ return "LTLParseError";
+ }
+
+}
diff --git a/src/main/java/de/b2tla/ltl/LTLBPredicate.java b/src/main/java/de/b2tla/ltl/LTLBPredicate.java
new file mode 100644
index 0000000000000000000000000000000000000000..15e36dbea88c0c544f5ca290664f491dbc4a81b0
--- /dev/null
+++ b/src/main/java/de/b2tla/ltl/LTLBPredicate.java
@@ -0,0 +1,30 @@
+package de.b2tla.ltl;
+
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
+
+public class LTLBPredicate {
+ LinkedHashMap<String, de.be4.classicalb.core.parser.node.Node> identifierHashTable;
+
+ de.be4.classicalb.core.parser.node.Node predicate;
+
+ public LTLBPredicate(LinkedHashMap<String, de.be4.classicalb.core.parser.node.Node> identifierHashTable, de.be4.classicalb.core.parser.node.Node predicate){
+ this.identifierHashTable = identifierHashTable;
+ this.predicate = predicate;
+ }
+
+ public LTLBPredicate(
+ ArrayList<de.be4.classicalb.core.parser.node.Node> arrayList,
+ de.be4.classicalb.core.parser.node.Start start) {
+ // TODO Auto-generated constructor stub
+ }
+
+ public de.be4.classicalb.core.parser.node.Node getBFormula(){
+ return predicate;
+ }
+
+ public LinkedHashMap<String, de.be4.classicalb.core.parser.node.Node> getIdentifierList(){
+ return identifierHashTable;
+ }
+
+}
diff --git a/src/main/java/de/b2tla/ltl/LTLFormulaPrinter.java b/src/main/java/de/b2tla/ltl/LTLFormulaPrinter.java
new file mode 100644
index 0000000000000000000000000000000000000000..b26de46fde09bbe9cd3cbd2b27258c26cadf6a43
--- /dev/null
+++ b/src/main/java/de/b2tla/ltl/LTLFormulaPrinter.java
@@ -0,0 +1,137 @@
+package de.b2tla.ltl;
+
+import de.b2tla.prettyprint.TLAPrinter;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
+import de.be4.ltl.core.parser.node.AAndLtl;
+import de.be4.ltl.core.parser.node.AEnabledLtl;
+import de.be4.ltl.core.parser.node.AExistsLtl;
+import de.be4.ltl.core.parser.node.AFalseLtl;
+import de.be4.ltl.core.parser.node.AFinallyLtl;
+import de.be4.ltl.core.parser.node.AForallLtl;
+import de.be4.ltl.core.parser.node.AGloballyLtl;
+import de.be4.ltl.core.parser.node.AImpliesLtl;
+import de.be4.ltl.core.parser.node.ANotLtl;
+import de.be4.ltl.core.parser.node.AOrLtl;
+import de.be4.ltl.core.parser.node.AStrongFairLtl;
+import de.be4.ltl.core.parser.node.ATrueLtl;
+import de.be4.ltl.core.parser.node.AUnparsedLtl;
+import de.be4.ltl.core.parser.node.AWeakFairLtl;
+
+public class LTLFormulaPrinter extends DepthFirstAdapter {
+
+ private final LTLFormulaVisitor ltlFormulaVisitor;
+ private final TLAPrinter tlaPrinter;
+
+ public LTLFormulaPrinter(TLAPrinter tlaPrinter,
+ LTLFormulaVisitor ltlFormulaVisitor) {
+ this.ltlFormulaVisitor = ltlFormulaVisitor;
+ this.tlaPrinter = tlaPrinter;
+
+ ltlFormulaVisitor.getLTLFormulaStart().apply(this);
+ }
+
+ @Override
+ public void caseAGloballyLtl(AGloballyLtl node) {
+ tlaPrinter.moduleStringAppend("[](");
+ node.getLtl().apply(this);
+ tlaPrinter.moduleStringAppend(")");
+ }
+
+ @Override
+ public void caseAFinallyLtl(AFinallyLtl node) {
+ tlaPrinter.moduleStringAppend("<>(");
+ node.getLtl().apply(this);
+ tlaPrinter.moduleStringAppend(")");
+ }
+
+ @Override
+ public void caseATrueLtl(ATrueLtl node) {
+ tlaPrinter.moduleStringAppend("TRUE");
+ }
+
+ @Override
+ public void caseAFalseLtl(AFalseLtl node) {
+ tlaPrinter.moduleStringAppend("FALSE");
+ }
+
+ @Override
+ public void caseAUnparsedLtl(AUnparsedLtl node) {
+ ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
+ }
+
+ @Override
+ public void caseAAndLtl(AAndLtl node) {
+ node.getLeft().apply(this);
+ tlaPrinter.moduleStringAppend(" /\\ ");
+ node.getRight().apply(this);
+ }
+
+ @Override
+ public void caseAOrLtl(AOrLtl node) {
+ node.getLeft().apply(this);
+ tlaPrinter.moduleStringAppend(" \\/ ");
+ node.getRight().apply(this);
+ }
+
+ @Override
+ public void caseANotLtl(ANotLtl node) {
+ tlaPrinter.moduleStringAppend("\\neg(");
+ node.getLtl().apply(this);
+ tlaPrinter.moduleStringAppend(")");
+ }
+
+ @Override
+ public void caseAImpliesLtl(AImpliesLtl node) {
+ node.getLeft().apply(this);
+ tlaPrinter.moduleStringAppend(" => ");
+ node.getRight().apply(this);
+ }
+
+ @Override
+ public void caseAEnabledLtl(AEnabledLtl node) {
+ tlaPrinter.moduleStringAppend("ENABLED(");
+ tlaPrinter.moduleStringAppend(node.getOperation().getText());
+ tlaPrinter.moduleStringAppend(")");
+ }
+
+ @Override
+ public void caseAWeakFairLtl(AWeakFairLtl node) {
+ tlaPrinter.printWeakFairness(node.getOperation().getText());
+ }
+
+ @Override
+ public void caseAStrongFairLtl(AStrongFairLtl node) {
+ tlaPrinter.printStrongFairness(node.getOperation().getText());
+ }
+
+ @Override
+ public void caseAExistsLtl(AExistsLtl node) {
+ tlaPrinter.moduleStringAppend("\\E ");
+ tlaPrinter.moduleStringAppend(node.getExistsIdentifier().getText());
+ tlaPrinter.moduleStringAppend(" \\in ");
+ Node id = this.ltlFormulaVisitor.getLTLIdentifier(node
+ .getExistsIdentifier().getText());
+ tlaPrinter.printTypeOfIdentifier((AIdentifierExpression) id);
+ tlaPrinter.moduleStringAppend(": ");
+ ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
+ tlaPrinter.moduleStringAppend(" /\\ ");
+ node.getLtl().apply(this);
+ }
+
+ @Override
+ public void caseAForallLtl(AForallLtl node) {
+ tlaPrinter.moduleStringAppend("\\A ");
+ tlaPrinter.moduleStringAppend(node.getForallIdentifier().getText());
+ tlaPrinter.moduleStringAppend(" \\in ");
+ Node id = this.ltlFormulaVisitor.getLTLIdentifier(node
+ .getForallIdentifier().getText());
+ tlaPrinter.printTypeOfIdentifier((AIdentifierExpression) id);
+ tlaPrinter.moduleStringAppend(": ");
+ ltlFormulaVisitor.getBAst(node).apply(tlaPrinter);
+ tlaPrinter.moduleStringAppend(" /\\ ");
+ node.getLtl().apply(this);
+ }
+
+}
diff --git a/src/main/java/de/b2tla/ltl/LTLFormulaVisitor.java b/src/main/java/de/b2tla/ltl/LTLFormulaVisitor.java
new file mode 100644
index 0000000000000000000000000000000000000000..2b7fc3d809115664e1dac13aa106794a1368e395
--- /dev/null
+++ b/src/main/java/de/b2tla/ltl/LTLFormulaVisitor.java
@@ -0,0 +1,270 @@
+package de.b2tla.ltl;
+
+import java.io.IOException;
+import java.io.PushbackReader;
+import java.io.StringReader;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.Hashtable;
+import java.util.LinkedHashMap;
+import java.util.List;
+
+import de.b2tla.analysis.MachineContext;
+import de.b2tla.exceptions.LTLParseException;
+import de.b2tla.exceptions.ScopeException;
+import de.b2tla.prettyprint.TLAPrinter;
+import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
+import de.be4.ltl.core.parser.internal.LtlLexer;
+import de.be4.ltl.core.parser.lexer.Lexer;
+import de.be4.ltl.core.parser.lexer.LexerException;
+import de.be4.ltl.core.parser.node.AEnabledLtl;
+import de.be4.ltl.core.parser.node.AExistsLtl;
+import de.be4.ltl.core.parser.node.AForallLtl;
+import de.be4.ltl.core.parser.node.AHistoricallyLtl;
+import de.be4.ltl.core.parser.node.AOnceLtl;
+import de.be4.ltl.core.parser.node.AReleaseLtl;
+import de.be4.ltl.core.parser.node.ASinceLtl;
+import de.be4.ltl.core.parser.node.AStrongFairLtl;
+import de.be4.ltl.core.parser.node.ATriggerLtl;
+import de.be4.ltl.core.parser.node.AUnparsedLtl;
+import de.be4.ltl.core.parser.node.AUntilLtl;
+import de.be4.ltl.core.parser.node.AWeakFairLtl;
+import de.be4.ltl.core.parser.node.AWeakuntilLtl;
+import de.be4.ltl.core.parser.node.AYesterdayLtl;
+import de.be4.ltl.core.parser.node.PLtl;
+import de.be4.ltl.core.parser.node.Start;
+import de.be4.ltl.core.parser.parser.Parser;
+import de.be4.ltl.core.parser.parser.ParserException;
+
+public class LTLFormulaVisitor extends DepthFirstAdapter {
+
+ private final String name;
+ private final Start ltlFormulaStart;
+ private final MachineContext machineContext;
+
+ private final LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node> ltlNodeToBNodeTable;
+ private final ArrayList<LTLBPredicate> bPredicates;
+ private final Hashtable<String, AIdentifierExpression> ltlIdentifierTable;
+
+ private ArrayList<Hashtable<String, AIdentifierExpression>> contextTable;
+
+ public ArrayList<LTLBPredicate> getBPredicates() {
+ return bPredicates;
+ }
+
+ public Collection<AIdentifierExpression> getParameter() {
+ return ltlIdentifierTable.values();
+ }
+
+ public AIdentifierExpression getLTLIdentifier(String identifier) {
+ return ltlIdentifierTable.get(identifier);
+ }
+
+ public LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node> getUnparsedHashTable() {
+ return ltlNodeToBNodeTable;
+ }
+
+ public de.be4.classicalb.core.parser.node.Node getBAst(
+ de.be4.ltl.core.parser.node.Node unparsedLtl) {
+ return ltlNodeToBNodeTable.get(unparsedLtl);
+ }
+
+ public String getName() {
+ return this.name;
+ }
+
+ public LTLFormulaVisitor(String name, String ltlFormula,
+ MachineContext machineContext) {
+ this.name = name;
+ this.ltlFormulaStart = parse(ltlFormula);
+ this.machineContext = machineContext;
+
+ this.bPredicates = new ArrayList<LTLBPredicate>();
+ this.ltlNodeToBNodeTable = new LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node>();
+ this.ltlIdentifierTable = new Hashtable<String, AIdentifierExpression>();
+
+ this.contextTable = new ArrayList<Hashtable<String, AIdentifierExpression>>();
+ }
+
+ public void start() {
+ ltlFormulaStart.apply(this);
+ }
+
+ public Start getLTLFormulaStart() {
+ return ltlFormulaStart;
+ }
+
+ public void printLTLFormula(TLAPrinter tlaPrinter) {
+ LTLFormulaPrinter ltlFormulaPrinter = new LTLFormulaPrinter(tlaPrinter,
+ this);
+ }
+
+ public static Start parse(String ltlFormula) {
+ StringReader reader = new StringReader(ltlFormula);
+ PushbackReader r = new PushbackReader(reader);
+ Lexer l = new LtlLexer(r);
+ Parser p = new Parser(l);
+ Start ast = null;
+ try {
+ ast = p.parse();
+
+ } catch (Exception e) {
+ e.printStackTrace();
+ throw new LTLParseException(e.getMessage());
+ }
+ return ast;
+ }
+
+ @Override
+ public void caseAUnparsedLtl(AUnparsedLtl node) {
+ de.be4.classicalb.core.parser.node.Start start = parseBPredicate(node
+ .getPredicate().getText());
+
+ ltlNodeToBNodeTable.put(node, start);
+
+ LTLBPredicate ltlBPredicate = new LTLBPredicate(
+ new LinkedHashMap<String, Node>(), start);
+ this.bPredicates.add(ltlBPredicate);
+
+ machineContext.checkLTLBPredicate(ltlBPredicate);
+ }
+
+ private de.be4.classicalb.core.parser.node.Start parseBPredicate(String text) {
+ String bPredicate = "#PREDICATE " + text;
+ BParser parser = new BParser("Testing");
+ de.be4.classicalb.core.parser.node.Start start = null;
+ try {
+ start = parser.parse(bPredicate, false);
+ } catch (BException e) {
+ e.printStackTrace();
+ }
+
+ return start;
+ }
+
+ @Override
+ public void caseAExistsLtl(AExistsLtl node) {
+ handleQuantification(node, node.getExistsIdentifier().getText(), node
+ .getPredicate().getText(), node.getLtl());
+
+ }
+
+ @Override
+ public void caseAForallLtl(AForallLtl node) {
+ handleQuantification(node, node.getForallIdentifier().getText(), node
+ .getPredicate().getText(), node.getLtl());
+ }
+
+ private void handleQuantification(de.be4.ltl.core.parser.node.Node node,
+ String parameterName, String bPredicateString, PLtl ltl) {
+ // create an identifier (b ast node) for the parameter of the
+ // quantification
+ List<TIdentifierLiteral> list = new ArrayList<TIdentifierLiteral>();
+ list.add(new TIdentifierLiteral(parameterName));
+ AIdentifierExpression parameterNode = new AIdentifierExpression(list);
+
+ // add the created identifier to the current context
+ Hashtable<String, AIdentifierExpression> currentContext = new Hashtable<String, AIdentifierExpression>();
+ currentContext.put(parameterName, parameterNode);
+ this.contextTable.add(currentContext);
+
+ // collection the all parameters in
+ ltlIdentifierTable.put(parameterName, parameterNode);
+
+ // parse the b predicate and create a reference to the b ast node
+ de.be4.classicalb.core.parser.node.Start start = parseBPredicate(bPredicateString);
+ ltlNodeToBNodeTable.put(node, start);
+
+ // collect all identifiers which can be used in the bPredicate and
+ // verify the bPredicate
+ LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(),
+ start);
+ this.bPredicates.add(ltlBPredicate);
+ machineContext.checkLTLBPredicate(ltlBPredicate);
+
+ // remaining LTL formula
+ ltl.apply(this);
+
+ // remove currentContext from contextTable
+ contextTable.remove(contextTable.size() - 1);
+
+ }
+
+ private LinkedHashMap<String, Node> getUnifiedContext() {
+ LinkedHashMap<String, Node> context = new LinkedHashMap<String, Node>();
+ for (int i = 0; i < contextTable.size(); i++) {
+ context.putAll(contextTable.get(i));
+ }
+ return context;
+ }
+
+ @Override
+ public void caseAEnabledLtl(AEnabledLtl node) {
+ String operationName = node.getOperation().getText();
+ if (!machineContext.getOperations().containsKey(operationName)) {
+ throw new ScopeException("Unkown operation " + operationName + ".");
+ }
+ }
+
+ @Override
+ public void caseAWeakFairLtl(AWeakFairLtl node) {
+ String operationName = node.getOperation().getText();
+ if (!machineContext.getOperations().containsKey(operationName)) {
+ throw new ScopeException("Unkown operation " + operationName + ".");
+ }
+ }
+
+ @Override
+ public void caseAStrongFairLtl(AStrongFairLtl node) {
+ String operationName = node.getOperation().getText();
+ if (!machineContext.getOperations().containsKey(operationName)) {
+ throw new ScopeException("Unkown operation " + operationName + ".");
+ }
+ }
+
+ public void inAUntilLtl(AUntilLtl node) {
+ throw new ScopeException(
+ "The 'until' operator is not supported by TLC.");
+ }
+
+ public void inAWeakuntilLtl(AWeakuntilLtl node) {
+ throw new ScopeException(
+ "The 'weak until' operator is not supported by TLC.");
+ }
+
+ public void inAReleaseLtl(AReleaseLtl node) {
+ throw new ScopeException(
+ "The 'release' operator is not supported by TLC.");
+ }
+
+ public void inASinceLtl(ASinceLtl node) {
+ throw new ScopeException(
+ "The 'since' operator is not supported by TLC.");
+ }
+
+ public void inATriggerLtl(ATriggerLtl node) {
+ throw new ScopeException(
+ "The 'trigger' operator is not supported by TLC.");
+ }
+
+ public void inAHistoricallyLtl(AHistoricallyLtl node) {
+ throw new ScopeException(
+ "The 'history' operator is not supported by TLC.");
+ }
+
+ public void inAOnceLtl(AOnceLtl node) {
+ throw new ScopeException("The 'once' operator is not supported by TLC.");
+ }
+
+ public void inAYesterdayLtl(AYesterdayLtl node) {
+ throw new ScopeException(
+ "The 'yesterday' operator is not supported by TLC.");
+ }
+
+}
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index a8656b065521d9145fa96d174a40ebce436de508..6a9df8697271ddb886d2775611ce8e2c4a5ba7d7 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -8,12 +8,12 @@ import java.util.List;
import de.b2tla.Globals;
import de.b2tla.analysis.MachineContext;
+import de.b2tla.analysis.UnchangedVariablesFinder;
import de.b2tla.analysis.PrecedenceCollector;
import de.b2tla.analysis.PrimedNodesMarker;
import de.b2tla.analysis.Renamer;
import de.b2tla.analysis.TypeRestrictor;
import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UnchangedVariablesFinder;
import de.b2tla.analysis.UsedStandardModules;
import de.b2tla.analysis.nodes.EqualsNode;
import de.b2tla.analysis.nodes.NodeType;
@@ -22,6 +22,7 @@ import de.b2tla.btypes.BType;
import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
import de.b2tla.btypes.SetType;
+import de.b2tla.ltl.LTLFormulaVisitor;
import de.b2tla.tla.ConfigFile;
import de.b2tla.tla.TLADefinition;
import de.b2tla.tla.TLAModule;
@@ -46,7 +47,7 @@ public class TLAPrinter extends DepthFirstAdapter {
private MachineContext machineContext;
private Typechecker typechecker;
- private UnchangedVariablesFinder unchangedVariablesFinder;
+ private UnchangedVariablesFinder missingVariableFinder;
private PrecedenceCollector precedenceCollector;
private UsedStandardModules usedStandardModules;
private TypeRestrictor typeRestrictor;
@@ -64,7 +65,7 @@ public class TLAPrinter extends DepthFirstAdapter {
Renamer renamer) {
this.typechecker = typechecker;
this.machineContext = machineContext;
- this.unchangedVariablesFinder = unchangedVariablesFinder;
+ this.missingVariableFinder = unchangedVariablesFinder;
this.precedenceCollector = precedenceCollector;
this.usedStandardModules = usedStandardModules;
this.typeRestrictor = typeRestrictor;
@@ -75,9 +76,6 @@ public class TLAPrinter extends DepthFirstAdapter {
this.tlaModuleString = new StringBuilder();
this.configFileString = new StringBuilder();
-
- // Start start = machineContext.getTree();
- // start.apply(this);
}
public void start() {
@@ -91,18 +89,93 @@ public class TLAPrinter extends DepthFirstAdapter {
printAssertions();
printInit();
printOperations();
+ printSpecFormula();
+ printLTLFormulas();
tlaModuleString.append("====");
printConfig();
}
- private void printConfig() {
- if (this.configFile.isInit()) {
- this.configFileString.append("INIT Init\n");
+ private void printSpecFormula() {
+
+ if (this.configFile.isSpec()) {
+ tlaModuleString.append("vars == ");
+ printVarsAsTuple();
+ tlaModuleString.append("\n");
+
+ tlaModuleString.append("VWF == ");
+ printWeakFairness("Next");
+ tlaModuleString.append("\n");
+ tlaModuleString.append("Spec == Init /\\ [][Next]_vars /\\ VWF\n");
}
- if (this.configFile.isInit()) {
- this.configFileString.append("NEXT Next\n");
+
+ }
+
+ public void printStrongFairness(String s) {
+ tlaModuleString
+ .append(String
+ .format("([]<><<%s>>_vars \\/ <>[]~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
+ s, s, s));
+ printVarsStuttering();
+ tlaModuleString.append("))");
+
+ }
+
+ public void printWeakFairness(String s) {
+ tlaModuleString
+ .append(String
+ .format("([]<><<%s>>_vars \\/ []<>~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
+ s, s, s));
+ printVarsStuttering();
+ tlaModuleString.append("))");
+
+ }
+
+ private void printVarsStuttering() {
+ ArrayList<Node> vars = this.tlaModule.getVariables();
+ for (int i = 0; i < vars.size(); i++) {
+ vars.get(i).apply(this);
+ tlaModuleString.append("' = ");
+ vars.get(i).apply(this);
+ if (i < vars.size() - 1)
+ tlaModuleString.append(",");
+ }
+ }
+
+ private void printVarsAsTuple() {
+ ArrayList<Node> vars = this.tlaModule.getVariables();
+ if (vars.size() == 0)
+ return;
+ tlaModuleString.append("<<");
+ for (int i = 0; i < vars.size(); i++) {
+ vars.get(i).apply(this);
+ if (i < vars.size() - 1)
+ tlaModuleString.append(",");
+ }
+ tlaModuleString.append(">>");
+ }
+
+ private void printLTLFormulas() {
+ ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
+ for (int i = 0; i < visitors.size(); i++) {
+ LTLFormulaVisitor visitor = visitors.get(i);
+ tlaModuleString.append(visitor.getName() + " == ");
+ visitor.printLTLFormula(this);
+ tlaModuleString.append("\n");
+ }
+ }
+
+ private void printConfig() {
+ if (this.configFile.isSpec()) {
+ this.configFileString.append("SPECIFICATION Spec\n");
+ } else {
+ if (this.configFile.isInit()) {
+ this.configFileString.append("INIT Init\n");
+ }
+ if (this.configFile.isInit()) {
+ this.configFileString.append("NEXT Next\n");
+ }
}
if (configFile.isInvariant()) {
this.configFileString.append("INVARIANT Invariant\n");
@@ -120,8 +193,14 @@ public class TLAPrinter extends DepthFirstAdapter {
}
- // CONSTANTS
+ for (int i = 0; i < machineContext.getLTLFormulas().size(); i++) {
+ LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas().get(
+ i);
+ this.configFileString.append("PROPERTIES " + ltlVisitor.getName()
+ + "\n");
+ }
+ // CONSTANTS
ArrayList<ConfigFileAssignment> assignments = configFile
.getAssignments();
if (assignments.size() != 0) {
@@ -132,6 +211,10 @@ public class TLAPrinter extends DepthFirstAdapter {
}
}
+ public void moduleStringAppend(String str) {
+ this.tlaModuleString.append(str);
+ }
+
private void printHeader() {
tlaModuleString.append("---- MODULE ");
tlaModuleString.append(this.tlaModule.getModuleName());
@@ -365,28 +448,15 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
- inAEnumeratedSetSet(node);
- {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
-
- String setName = Utils.getIdentifierAsString(copy);
-
- tlaModuleString.append(renamer.getNameOfRef(node) + " == {");
- }
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getElements());
- for (int i = 0; i < copy.size(); i++) {
- copy.get(i).apply(this);
- if (i < copy.size() - 1) {
- tlaModuleString.append(", ");
- }
+ List<PExpression> copy = new ArrayList<PExpression>(node.getElements());
+ tlaModuleString.append(renamer.getNameOfRef(node) + " == {");
+ for (int i = 0; i < copy.size(); i++) {
+ copy.get(i).apply(this);
+ if (i < copy.size() - 1) {
+ tlaModuleString.append(", ");
}
}
tlaModuleString.append("}\n");
- outAEnumeratedSetSet(node);
-
}
@Override
@@ -517,8 +587,8 @@ public class TLAPrinter extends DepthFirstAdapter {
}
public void printUnchangedVariables(Node node, boolean printAnd) {
- HashSet<Node> unchangedVariablesSet = unchangedVariablesFinder
- .getUnchangedVariablesTable().get(node);
+ HashSet<Node> unchangedVariablesSet = missingVariableFinder
+ .getUnchangedVariables(node);
if (null != unchangedVariablesSet) {
ArrayList<Node> unchangedVariables = new ArrayList<Node>(
unchangedVariablesSet);
@@ -589,8 +659,8 @@ public class TLAPrinter extends DepthFirstAdapter {
}
public void printUnchangedVariablesNull(Node node, boolean printAnd) {
- HashSet<Node> unchangedVariablesSet = unchangedVariablesFinder
- .getUnchangedVariablesNull().get(node);
+ HashSet<Node> unchangedVariablesSet = missingVariableFinder
+ .getUnchangedVariablesNull(node);
if (null != unchangedVariablesSet) {
ArrayList<Node> unchangedVariables = new ArrayList<Node>(
unchangedVariablesSet);
@@ -742,9 +812,10 @@ 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());
+
+ // TODO handle output parameter of a operation
+ // List<PExpression> output = new ArrayList<PExpression>(
+ // node.getReturnValues());
List<PExpression> params = new ArrayList<PExpression>(
node.getParameters());
List<PExpression> newList = new ArrayList<PExpression>();
@@ -950,7 +1021,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++) {
@@ -1329,7 +1400,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
}
- private void printTypeOfIdentifier(PExpression e) {
+ public void printTypeOfIdentifier(PExpression e) {
// NodeType n = typeRestrictor.getRestrictedTypes().get(e);
ArrayList<NodeType> list = typeRestrictor.getRestrictedTypesSet(e);
if (list != null) {
diff --git a/src/main/java/de/b2tla/tla/ConfigFile.java b/src/main/java/de/b2tla/tla/ConfigFile.java
index d17f29f923d95363d63dc934c10745c045ee300e..7766721e561429bf00776f55125bce29becbccff 100644
--- a/src/main/java/de/b2tla/tla/ConfigFile.java
+++ b/src/main/java/de/b2tla/tla/ConfigFile.java
@@ -9,6 +9,7 @@ public class ConfigFile {
private final ArrayList<ConfigFileAssignment> assignments;
private boolean invariant;
+ private boolean spec;
private boolean init;
private boolean next;
private int assertionsSize;
@@ -25,6 +26,10 @@ public class ConfigFile {
return assignments;
}
+ public boolean isSpec(){
+ return spec;
+ }
+
public boolean isInvariant() {
return invariant;
@@ -68,6 +73,9 @@ public class ConfigFile {
return assertionsSize;
}
+ public void setSpec(){
+ this.spec = true;
+ }
public void setGoal(){
this.goal = true;
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java
index e9bc25998da21ff92493af8693363e34e44edebf..bbc6a7f22b26a5b050c9dd4f552d75f60d1df1db 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/b2tla/tla/Generator.java
@@ -64,6 +64,15 @@ public class Generator extends DepthFirstAdapter {
evalOperations();
evalGoal();
machineContext.getTree().apply(this);
+
+ evalSpec();
+ }
+
+ private void evalSpec() {
+ if (this.configFile.isInit() && this.configFile.isNext()
+ && machineContext.getLTLFormulas().size() > 0) {
+ this.configFile.setSpec();
+ }
}
private void evalGoal() {
@@ -175,7 +184,8 @@ public class Generator extends DepthFirstAdapter {
}
private void evalDefinitions() {
- ADefinitionsMachineClause node = machineContext.getDefinitionMachineClause();
+ ADefinitionsMachineClause node = machineContext
+ .getDefinitionMachineClause();
if (node != null) {
for (PDefinition def : node.getDefinitions()) {
this.tlaModule.addToAllDefinitions(def);
@@ -212,7 +222,6 @@ public class Generator extends DepthFirstAdapter {
(PExpression) value.clone());
machineContext.getReferences().put(exprDef, con);
-
this.tlaModule.addToAllDefinitions(exprDef);
}
diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java
index 56c3f39828c56217e704ef65a22275b4602bd7d5..fbd5c476017a80c316d7f70754249e8bc82b04a6 100644
--- a/src/main/java/de/b2tla/tlc/TLCOutput.java
+++ b/src/main/java/de/b2tla/tlc/TLCOutput.java
@@ -22,7 +22,7 @@ public class TLCOutput {
String parseError;
public static enum ERROR {
- Deadlock, Goal, Invariant, ParseError, NoError, Assertion, PropertiesError, EnumerateError, TLCError
+ Deadlock, Goal, Invariant, ParseError, NoError, Assertion, PropertiesError, EnumerateError, TLCError, TemporalProperty
}
public long getRunningTime() {
@@ -31,8 +31,10 @@ public class TLCOutput {
}
public String getError() {
- if(error == ERROR.Invariant){
+ if (error == ERROR.Invariant) {
return "Invariant Violation";
+ }else if(error == ERROR.TemporalProperty){
+ return "Temporal Property Violation";
}
return error.toString();
}
@@ -41,8 +43,8 @@ public class TLCOutput {
parseTrace();
return trace;
}
-
- public String getModuleName(){
+
+ public String getModuleName() {
return moduleName;
}
@@ -121,13 +123,16 @@ public class TLCOutput {
for (int i = 0; i < states.size(); i++) {
String m = states.get(i);
// System.out.println(m);
- String location = m.substring(0, m.indexOf("\n"));
+ // String location = m.substring(0, m.indexOf("\n"));
// String operationName = moduleMatcher.getName(location);
-
+ int pos = m.indexOf("\n");
+ if (pos == -1)
+ break; // e.g. 'State 10: Stuttering'
String predicate = m.substring(m.indexOf("\n") + 1);
- //String res = TLCExpressionParser.parseLine(predicate);
- //TODO OUTPUT
- String res = TLCExpressionParser.parseLine(predicate, tlcOutputInfo.getTypes());
+ // String res = TLCExpressionParser.parseLine(predicate);
+ // TODO OUTPUT
+ String res = TLCExpressionParser.parseLine(predicate,
+ tlcOutputInfo.getTypes());
trace.append(res);
trace.append("\n");
}
@@ -159,10 +164,14 @@ public class TLCOutput {
}
} else if (res[1].equals("Assumption")) {
return ERROR.PropertiesError;
+ } else if (res[1].equals("Temporal")) {
+ return ERROR.TemporalProperty;
} else if (m.equals("Error: TLC threw an unexpected exception.")) {
return ERROR.ParseError;
} else if (m.startsWith("Error: The behavior up to")) {
return null;
+ } else if (m.startsWith("Error: The following behavior constitutes a counter-example:")) {
+ return null;
}
System.out.println(m);
return ERROR.TLCError;
diff --git a/src/test/java/de/b2tla/analysis/ScopeTest.java b/src/test/java/de/b2tla/analysis/ScopeTest.java
index b526447b0135bbae08bf91d4a402eb96a2e72b99..5f3840976d1c9de0661d9c28b34ac391cd2b6000 100644
--- a/src/test/java/de/b2tla/analysis/ScopeTest.java
+++ b/src/test/java/de/b2tla/analysis/ScopeTest.java
@@ -101,7 +101,7 @@ public class ScopeTest {
checkMachine(machine);
}
- @Ignore //TODO
+ @Ignore //TODO machineContext line 657
@Test(expected = ScopeException.class)
public void testConstantSubstitution() throws Exception {
String machine = "MACHINE test\n" + "CONSTANTS x \n"
diff --git a/src/test/java/de/b2tla/ltl/LtlFormulaTest.java b/src/test/java/de/b2tla/ltl/LtlFormulaTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..ab3d9cebfe5b21ba5c3b619d8217a90cbe7ccc37
--- /dev/null
+++ b/src/test/java/de/b2tla/ltl/LtlFormulaTest.java
@@ -0,0 +1,325 @@
+package de.b2tla.ltl;
+
+
+import static de.b2tla.util.TestUtil.compareLTL;
+import static de.b2tla.util.TestUtil.compareEqualsConfig;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+import de.b2tla.exceptions.ScopeException;
+import de.b2tla.exceptions.TypeErrorException;
+
+
+public class LtlFormulaTest {
+
+
+
+ @Test (expected = ScopeException.class)
+ public void testScopeException() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+ compareLTL("", machine, "G{y = 1}");
+ }
+
+ @Test (expected = TypeErrorException.class)
+ public void testTypeError() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+ compareLTL("", machine, "G{x = FALSE}");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testUnkownOperation() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "e(foo)");
+ }
+
+ @Ignore
+ @Test
+ public void testGobally() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = 1\n"
+ + "Init == x = 1\n"
+ + "foo == x' = 1\n\n"
+ + "Next == \\/ foo\n"
+ + "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ + "ltl == [](x = 1)\n"
+ + "====";
+ compareLTL(expected, machine, "G{x = 1}");
+ }
+
+ @Ignore
+ @Test
+ public void testFinally() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = 1\n"
+ + "Init == x = 1\n"
+ + "foo == x' = 1\n\n"
+ + "Next == \\/ foo\n"
+ + "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ + "ltl == <>(x = 1)\n"
+ + "====";
+ compareLTL(expected, machine, "F{x = 1}");
+ }
+
+ @Test
+ public void testTrue() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "ltl == TRUE\n"
+ + "====";
+ compareLTL(expected, machine, "true");
+ }
+
+ @Test
+ public void testFalse() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "ltl == FALSE\n"
+ + "====";
+ compareLTL(expected, machine, "false");
+ }
+
+ @Test
+ public void testImplication() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "ltl == FALSE => TRUE\n"
+ + "====";
+ compareLTL(expected, machine, "false => true");
+ }
+
+ @Test
+ public void testAnd() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "ltl == TRUE /\\ FALSE\n"
+ + "====";
+ compareLTL(expected, machine, "true & false");
+ }
+
+ @Test
+ public void testOr() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "ltl == TRUE \\/ FALSE\n"
+ + "====";
+ compareLTL(expected, machine, "true or false");
+ }
+
+ @Test
+ public void testNegation() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "ltl == \\neg(TRUE)\n"
+ + "====";
+ compareLTL(expected, machine, "not(true)");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testUntil() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "true U false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testWeakUntil() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "true W false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testRelease() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "true R false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testHistory() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "H false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testOnce() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "O false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testYesterday() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "Y false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testSince() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "true S false");
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testTrigger() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ compareLTL("", machine, "true T false");
+ }
+
+ @Ignore
+ @Test
+ public void testEnabled() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = 1\n"
+ + "Init == x = 1\n"
+ + "foo == x' = 1\n\n"
+ + "Next == \\/ foo\n"
+ + "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ + "ltl == ENABLED(foo)\n"
+ + "====";
+ compareLTL(expected, machine, "e(foo)");
+ }
+
+ @Ignore
+ @Test
+ public void testWeakFairness() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = 1\n"
+ + "Init == x = 1\n"
+ + "foo == x' = 1\n\n"
+ + "Next == \\/ foo\n"
+ + "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ + "ltl == ENABLED(foo)\n"
+ + "====";
+ compareLTL(expected, machine, "WF(foo)");
+ }
+
+ @Ignore
+ @Test
+ public void testStrongFairness() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = 1\n"
+ + "Init == x = 1\n"
+ + "foo == x' = 1\n\n"
+ + "Next == \\/ foo\n"
+ + "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ + "ltl == ENABLED(foo)\n"
+ + "====";
+ compareLTL(expected, machine, "SF(foo)");
+ }
+
+
+ @Test
+ public void testExistentialQuantification() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ String expected = "---- MODULE test ----\n"
+ + "ltl == \\E p \\in {1}: p = 1 /\\ TRUE\n"
+ + "====";
+ compareLTL(expected, machine, "#p.({p=1} & true)");
+ }
+
+ @Test
+ public void testForallQuantification() throws Exception {
+ String machine = "MACHINE test\n"
+ + "END";
+ String expected = "---- MODULE test ----\n"
+ + "ltl == \\A p \\in {1}: p = 1 /\\ TRUE\n"
+ + "====";
+ compareLTL(expected, machine, "!p.({p=1} => true)");
+ }
+
+ @Ignore
+ @Test
+ public void testLTLFormulaInDefinitions() throws Exception {
+ final String machine = "MACHINE test\n"
+ + "DEFINITIONS ASSERT_LTL == \"false\" \n"
+ + "VARIABLES x\n"
+ + "INVARIANT x = 1\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS foo = x := 1"
+ + "END";
+
+ final String expected = "---- MODULE test ----\n"
+ + "VARIABLES x\n"
+ + "Invariant == x = 1\n"
+ + "Init == x = 1\n"
+ + "foo == x' = 1\n\n"
+ + "Next == \\/ foo\n"
+ + "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ + "ASSERT_LTL == FALSE\n"
+ + "====";
+ final String config = "SPECIFICATION Spec\nINVARIANT Invariant\nPROPERTIES ASSERT_LTL\n";
+
+ compareEqualsConfig(expected, config, machine);
+ }
+
+}
diff --git a/src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java b/src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java
index d1959f034799664a35be4397ec5e45435f733178..8e4df28d60475147c0bd12e0d45c007f44c9c89a 100644
--- a/src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java
+++ b/src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java
@@ -6,13 +6,13 @@ import org.junit.Test;
public class EnumeratedSetsTest {
@Test
- public void testSetComprehensionEquals() throws Exception {
- // TODO verify config
+ public void testTwoEnumeratedSets() throws Exception {
String machine = "MACHINE test\n" + "SETS set = {a,b,c}; set2 = {d}\n"
+ "END";
String expected = "---- MODULE test ----\n" + "CONSTANTS a, b, c, d\n"
+ "set == {a, b, c}\n" + "set2 == {d}\n" + "====";
- compareEquals(expected, machine);
+ final String config = "CONSTANTS\na = a\nb = b\nc = c\nd = d\n";
+ compareEqualsConfig(expected, config, machine);
}
}
diff --git a/src/test/java/de/b2tla/tlc/integration/LTLTest.java b/src/test/java/de/b2tla/tlc/integration/LTLTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..94f347b82726996abe4f78c6530e64e8b924afa3
--- /dev/null
+++ b/src/test/java/de/b2tla/tlc/integration/LTLTest.java
@@ -0,0 +1,19 @@
+package de.b2tla.tlc.integration;
+
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCOutput;
+
+public class LTLTest {
+
+ @Test
+ public void testRelations() throws Exception {
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\CounterLTL.mch"};
+ B2TLA.main(a);
+ //assertEquals(TLCOutput.ERROR.TemporalProperty, B2TLA.test(a));
+ }
+
+}
diff --git a/src/test/java/de/b2tla/typechecking/TestTypechecker.java b/src/test/java/de/b2tla/typechecking/TestTypechecker.java
index 6dd249f360efbc68368217d3462c3595a7508f8e..663db02b45fc4abb309cf663ff54696fbc693b34 100644
--- a/src/test/java/de/b2tla/typechecking/TestTypechecker.java
+++ b/src/test/java/de/b2tla/typechecking/TestTypechecker.java
@@ -26,7 +26,7 @@ public class TestTypechecker {
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
System.out.println(ast2String2.toString());
- MachineContext c = new MachineContext(start);
+ MachineContext c = new MachineContext(start, null);
Typechecker t = new Typechecker(c);
for (String name : c.getSetParamter().keySet()) {
diff --git a/src/test/java/de/b2tla/util/TestUtil.java b/src/test/java/de/b2tla/util/TestUtil.java
index 860d73bfbf5c927d92a980847524649da4723937..6d67b2107114040aba5c94fb68f6c7f317ed4ce0 100644
--- a/src/test/java/de/b2tla/util/TestUtil.java
+++ b/src/test/java/de/b2tla/util/TestUtil.java
@@ -44,6 +44,18 @@ public class TestUtil {
// assertEquals(sb2.toString(), sb1.toString());
}
+
+ public static void compareLTL(String expectedModule, String machine, String ltlFormula)
+ throws Exception {
+ B2TlaTranslator b2tlaTranslator = new B2TlaTranslator(machine, ltlFormula);
+ b2tlaTranslator.translate();
+ System.out.println(b2tlaTranslator.getModuleString());
+ String name = b2tlaTranslator.getMachineName();
+ de.tla2b.translation.Tla2BTranslator
+ .translateString(name, b2tlaTranslator.getModuleString(), null);
+ assertEquals(expectedModule, b2tlaTranslator.getModuleString());
+ }
+
public static void checkMachine(String machine)
throws Exception {
B2TlaTranslator b2tlaTranslator = new B2TlaTranslator(machine);
@@ -61,6 +73,23 @@ public class TestUtil {
System.out.println(ast2String2.toString());
}
+ public static void compareEqualsConfig(String expectedModule,
+ String expectedConfig, String machine) throws Exception {
+ B2TlaTranslator b2tlaTranslator = new B2TlaTranslator(machine);
+ b2tlaTranslator.translate();
+ // print(b2tlaTranslator.getStart());
+ System.out.println(b2tlaTranslator.getModuleString());
+ System.out.println(b2tlaTranslator.getConfigString());
+
+ String name = b2tlaTranslator.getMachineName();
+ de.tla2b.translation.Tla2BTranslator
+ .translateString(name, b2tlaTranslator.getModuleString(),
+ b2tlaTranslator.getConfigString());
+
+ assertEquals(expectedModule, b2tlaTranslator.getModuleString());
+ assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
+ }
+
public static void compareConfig(String expectedModule,
String expectedConfig, String machine) throws Exception {
B2TlaTranslator b2tlaTranslator = new B2TlaTranslator(machine);
diff --git a/src/test/java/standard/CompoundScopeTest.java b/src/test/java/standard/CompoundScopeTest.java
index f1ea58bd7928fd75e30fca03190bb6d6ea6a09df..b9c3993de94eb447580c54b9963161a0422f4a51 100644
--- a/src/test/java/standard/CompoundScopeTest.java
+++ b/src/test/java/standard/CompoundScopeTest.java
@@ -56,8 +56,8 @@ public class CompoundScopeTest {
start.apply(ast2String2);
System.out.println(ast2String2.toString());
- MachineContext c = new MachineContext(start, machineContextsTable);
- machineContextsTable.put(name, c);
+ //MachineContext c = new MachineContext(start, machineContextsTable);
+ //machineContextsTable.put(name, c);
}
diff --git a/src/test/resources/ltl/CounterLTL.mch b/src/test/resources/ltl/CounterLTL.mch
new file mode 100644
index 0000000000000000000000000000000000000000..ce5fae9d50d5b15a073d10b1f7b56828c1f989ee
--- /dev/null
+++ b/src/test/resources/ltl/CounterLTL.mch
@@ -0,0 +1,11 @@
+MACHINE CounterLTL
+DEFINITIONS
+ASSERT_LTL_1 == "F {x = 10}"
+VARIABLES x
+INVARIANT
+ x : 1..10
+INITIALISATION x:=1
+OPERATIONS
+ Inc = PRE x < 10 THEN x:= x + 1 END;
+ Reset = PRE x = 10 THEN x := 1 END
+END
\ No newline at end of file