diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index d1e41ff0e70439af11f7f595377b8db76a566897..aa242f56283545108685a40ded53cce155adba98 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -92,7 +92,7 @@ public class MachineContext extends DepthFirstAdapter {
private LinkedHashMap<String, Node> constants;
private final LinkedHashMap<String, Node> bMachineConstants;
-
+
private final LinkedHashMap<String, Node> variables;
private final LinkedHashMap<String, Node> definitions;
private final LinkedHashMap<String, Node> operations;
@@ -114,8 +114,6 @@ public class MachineContext extends DepthFirstAdapter {
protected final Hashtable<Node, Node> referencesTable;
-
-
public MachineContext(String machineName, Start start, String ltlFormula,
PPredicate constantsSetup) {
this.start = start;
@@ -126,7 +124,8 @@ public class MachineContext extends DepthFirstAdapter {
LTLFormulaVisitor ltlVisitor = null;
if (null != ltlFormula) {
- ltlVisitor = new LTLFormulaVisitor("ltl", ltlFormula, this);
+ ltlVisitor = new LTLFormulaVisitor("ltl", this);
+ ltlVisitor.parseLTLString(ltlFormula);
this.ltlVisitors.add(ltlVisitor);
}
@@ -298,16 +297,10 @@ public class MachineContext extends DepthFirstAdapter {
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.");
- }
+ LTLFormulaVisitor visitor = new LTLFormulaVisitor(name, this);
+ visitor.parseDefinition(def);
+ this.ltlVisitors.add(visitor);
+
definitionsToRemove.add(def);
} else if (name.startsWith("ANIMATION_")) {
definitionsToRemove.add(def);
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index e8befd7778f176842a1678061824aff13c539c40..ed50c8f38887093c115d40bcd86134919c6540ca 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -1,5 +1,6 @@
package de.tlc4b.ltl;
+import java.io.IOException;
import java.io.PushbackReader;
import java.io.StringReader;
import java.util.ArrayList;
@@ -10,12 +11,15 @@ import java.util.List;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AStringExpression;
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.AActionLtl;
import de.be4.ltl.core.parser.node.AEnabledLtl;
import de.be4.ltl.core.parser.node.AExistsLtl;
@@ -34,6 +38,7 @@ 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;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.exceptions.LTLParseException;
@@ -43,31 +48,49 @@ import de.tlc4b.prettyprint.TLAPrinter;
public class LTLFormulaVisitor extends DepthFirstAdapter {
private final String name;
- private final Start ltlFormulaStart;
private final MachineContext machineContext;
-
+ private String ltlFormula;
+ private Start ltlFormulaStart;
+
private final LinkedHashMap<de.be4.ltl.core.parser.node.Node, de.be4.classicalb.core.parser.node.Node> ltlNodeToBNodeTable;
private final ArrayList<LTLBPredicate> bPredicates;
private final Hashtable<String, AIdentifierExpression> ltlIdentifierTable;
private ArrayList<Hashtable<String, AIdentifierExpression>> contextTable;
-
- public LTLFormulaVisitor(String name, String ltlFormula,
- MachineContext machineContext) {
+ public LTLFormulaVisitor(String name, 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 parseDefinition(AExpressionDefinitionDefinition def) {
+ if (!(def.getRhs() instanceof AStringExpression)) {
+ throw new LTLParseException(
+ "Error: LTL formula is not in a string representation.");
+ }
+ AStringExpression stringNode = (AStringExpression) def.getRhs();
+ this.ltlFormula = stringNode.getContent().getText();
+ try {
+ this.ltlFormulaStart = parse(ltlFormula);
+ } catch (Exception e) {
+ String line = "Parsing definition " + name + " (line "
+ + def.getStartPos().getLine() + "):\n";
+ throw new LTLParseException(line + e.getMessage());
+ }
+ }
+
+ public void parseLTLString(String ltlString) {
+ try {
+ this.ltlFormulaStart = parse(ltlFormula);
+ } catch (Exception e) {
+ throw new LTLParseException(e.getMessage());
+ }
+ }
+
public ArrayList<LTLBPredicate> getBPredicates() {
return bPredicates;
}
@@ -101,24 +124,20 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return ltlFormulaStart;
}
- public void printLTLFormula(TLAPrinter tlaPrinter, TypeRestrictor typeRestrictor) {
+ public void printLTLFormula(TLAPrinter tlaPrinter,
+ TypeRestrictor typeRestrictor) {
// LTLFormulaPrinter ltlFormulaPrinter =
new LTLFormulaPrinter(tlaPrinter, this, typeRestrictor);
}
- public static Start parse(String ltlFormula) {
+ public static Start parse(String ltlFormula) throws ParserException,
+ LexerException, IOException {
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());
- }
+ ast = p.parse();
return ast;
}
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index 40596ce62bf46f32ea3c96e9a04031c6b4d2367f..4a936a7b82e06041d5f131e6470d3ff5215bea27 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -28,7 +28,7 @@ public class Testing2 extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
- String[] a = new String[] { machine.getPath() };
+ String[] a = new String[] { machine.getPath(), "-nodead", "-noinv" };
TLC4B.main(a);
//TLC4B.test(a, false);
// test(a);