diff --git a/build.gradle b/build.gradle
index 030349a116c645fcaf14ef7813556d34e636f128..a58a7d6fce0dd53a25d6149c7847975b52652258 100644
--- a/build.gradle
+++ b/build.gradle
@@ -41,6 +41,7 @@ dependencies {
test {
exclude('de/b2tla/tlc/integration/probprivate')
exclude('de/b2tla/tlc/integration/testing')
+
}
diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java
index 09df230e3fbd0f6cbe105808851188fda78f4a3f..8dc0a0978d42e2c209d9ad5aa284e7e7a0265995 100644
--- a/src/main/java/de/b2tla/B2TLA.java
+++ b/src/main/java/de/b2tla/B2TLA.java
@@ -9,18 +9,15 @@ import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
-import java.io.Writer;
import java.util.ArrayList;
-import tlc2.TLCGlobals;
import de.b2tla.B2TLAGlobals;
-import de.b2tla.analysis.UsedStandardModules;
import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES;
import de.b2tla.exceptions.B2TLAIOException;
import de.b2tla.exceptions.B2tlaException;
-import de.b2tla.tlc.TLCOutput;
import de.b2tla.tlc.TLCOutputInfo;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
+import de.b2tla.tlc.TLCResults;
import de.b2tla.util.StopWatch;
import de.be4.classicalb.core.parser.exceptions.BException;
@@ -56,21 +53,56 @@ public class B2TLA {
try {
ArrayList<String> output = TLCRunner.runTLC(
b2tla.machineFileNameWithoutFileExtension, b2tla.path);
- b2tla.evalOutput(output, B2TLAGlobals.isCreateTraceFile());
+ // b2tla.evalOutput(output, B2TLAGlobals.isCreateTraceFile());
+ // System.out.println("------------------------------");
+
+ TLCResults results = new TLCResults(b2tla.tlcOutputInfo);
+ results.evalResults();
+ b2tla.printResults(results, output,
+ B2TLAGlobals.isCreateTraceFile());
+
} catch (NoClassDefFoundError e) {
- System.out
- .println("Can not find TLC. The tla2tools must be included in the classpath.");
- System.out.println(e.getMessage());
+ System.err
+ .println("Can not find TLC. The tlatools.jar must be included in the classpath.");
+ // System.out.println(e.getMessage());
}
}
}
- public static TLCResult test(String[] args, boolean deleteFiles)
+ private void printResults(TLCResults results, ArrayList<String> output,
+ boolean createTraceFile) {
+
+ System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
+ + " ms");
+ System.out.println("Translation time: " + StopWatch.getRunTime("Pure") + " ms");
+ System.out.println("Model checking time: "
+ + results.getModelCheckingTime() + " sec");
+ System.out.println("States analysed: "
+ + results.getNumberOfDistinctStates());
+ System.out.println("Transitions fired: "
+ + results.getNumberOfTransitions());
+ System.out.println("Result: " + results.getResultString());
+
+ if (results.hasTrace() && createTraceFile) {
+ String trace = results.getTrace();
+ String tracefileName = machineFileNameWithoutFileExtension
+ + ".tla.trace";
+ File traceFile = createFile(path, tracefileName, trace, false);
+ if (traceFile != null) {
+ System.out.println("Trace file '" + traceFile.getAbsolutePath()
+ + "' created.");
+ }
+ }
+
+ }
+
+ public static void test(String[] args, boolean deleteFiles)
throws IOException {
B2TLAGlobals.resetGlobals();
B2TLAGlobals.setDeleteOnExit(deleteFiles);
+ B2TLAGlobals.setTestingMode(true);
// B2TLAGlobals.setCleanup(true);
B2TLA b2tla = new B2TLA();
try {
@@ -78,60 +110,34 @@ public class B2TLA {
} catch (Exception e) {
e.printStackTrace();
System.err.println(e.getMessage());
- return null;
+ return;
}
if (B2TLAGlobals.isRunTLC()) {
- ArrayList<String> output = TLCRunner.runTLCInANewJVM(
- b2tla.machineFileNameWithoutFileExtension, b2tla.path);
- TLCResult error = TLCOutput.findError(output);
- System.out.println(error);
- return error;
+ TLCRunner.runTLC(b2tla.machineFileNameWithoutFileExtension,
+ b2tla.path);
+
+ TLCResults results = new TLCResults(b2tla.tlcOutputInfo);
+ results.evalResults();
+ TLCResult result = results.getTLCResult();
+ System.out.println("Result: " + result);
+ System.exit(0);
}
- return null;
+ System.exit(1);
}
- private void evalOutput(ArrayList<String> output, boolean createTraceFile) {
- TLCOutput tlcOutput = new TLCOutput(
- machineFileNameWithoutFileExtension,
- output.toArray(new String[output.size()]), tlcOutputInfo);
- tlcOutput.parseTLCOutput();
- if (B2TLAGlobals.isRunTestscript()) {
- printTestResultsForTestscript(tlcOutput);
- return;
- }
-
- System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
- + " ms");
- System.out.println("Translation time: " + StopWatch.getRunTime("Pure"));
- System.out.println("Model checking time: " + tlcOutput.getRunningTime()
- + " sec");
- System.out.println("States analysed: " + tlcOutput.getDistinctStates());
- System.out.println("Transitions fired: " + tlcOutput.getTransitions());
- System.out.println("Result: " + tlcOutput.getResultString());
- if (tlcOutput.hasTrace() && createTraceFile) {
- StringBuilder trace = tlcOutput.getErrorTrace();
- String tracefileName = machineFileNameWithoutFileExtension
- + ".tla.trace";
- File traceFile = createFile(path, tracefileName, trace.toString(),
- false);
- if (traceFile != null) {
- System.out.println("Trace file '" + traceFile.getAbsolutePath()
- + "'created.");
- }
- }
- }
- private void printTestResultsForTestscript(TLCOutput tlcOutput) {
+ private void printTestResultsForTestscript() {
+ TLCResults tlcResults = null;
// This output is adapted to Ivo's testscript
System.out.println("------------- Results -------------");
System.out.println("Model Checking Time: "
- + (tlcOutput.getRunningTime() * 1000) + " ms");
- System.out.println("States analysed: " + tlcOutput.getDistinctStates());
- System.out.println("Transitions fired: " + tlcOutput.getTransitions());
- if (tlcOutput.getResult() != TLCResult.NoError) {
+ + (tlcResults.getModelCheckingTime() * 1000) + " ms");
+ System.out.println("States analysed: " + tlcResults.getNumberOfDistinctStates());
+ System.out.println("Transitions fired: " + tlcResults.getNumberOfTransitions());
+ if (tlcResults.getTLCResult() != TLCResult.NoError) {
System.err.println("@@");
- System.err.println("12" + tlcOutput.getResultString());
+ System.err.println("12" + tlcResults.getResultString());
}
}
@@ -170,10 +176,11 @@ public class B2TLA {
int workers = Integer.parseInt(args[index]);
B2TLAGlobals.setWorkers(workers);
} else if (args[index].toLowerCase().equals("-constantssetup")) {
+ B2TLAGlobals.setProBconstantsSetup(true);
index = index + 1;
if (index == args.length) {
throw new B2TLAIOException(
- "Error: String requiered after option '-constantsetup'.");
+ "Error: String requiered after option '-constantssetup'.");
}
constantsSetup = args[index];
} else if (args[index].toLowerCase().equals("-ltlformula")) {
@@ -365,54 +372,6 @@ public class B2TLA {
}
}
- public static void createUsedStandardModules(String path,
- ArrayList<UsedStandardModules.STANDARD_MODULES> standardModules) {
- if (standardModules.contains(STANDARD_MODULES.Relations)) {
- File naturalsFile = new File(path + File.separator
- + "Relations.tla");
- if (!naturalsFile.exists()) {
- try {
- naturalsFile.createNewFile();
- } catch (IOException e) {
- e.printStackTrace();
- }
- }
-
- try {
- Writer fw = new FileWriter(naturalsFile);
- fw.write(StandardModules.Relations);
- fw.close();
- System.out.println("Standard module '" + naturalsFile.getName()
- + "' created.");
- } catch (IOException e) {
- e.printStackTrace();
- }
-
- }
-
- if (standardModules.contains(STANDARD_MODULES.BBuiltIns)) {
- File bBuiltInsFile = new File(path + File.separator
- + "BBuiltIns.tla");
- if (!bBuiltInsFile.exists()) {
- try {
- bBuiltInsFile.createNewFile();
- } catch (IOException e) {
- e.printStackTrace();
- }
- }
- try {
- Writer fw = new FileWriter(bBuiltInsFile);
- fw.write(StandardModules.BBuiltIns);
- fw.close();
- System.out.println("Standard modules BBuiltIns.tla created.");
- } catch (IOException e) {
- e.printStackTrace();
- }
-
- }
-
- }
-
private File getFile() {
File mainFile = new File(mainFileName);
if (!mainFile.exists()) {
diff --git a/src/main/java/de/b2tla/B2TLAGlobals.java b/src/main/java/de/b2tla/B2TLAGlobals.java
index 8b1589d95d6b3ce0d0195345ec11e5b800357cec..e5a5fb47a2cd40a980603a92ea55ecf02520637f 100644
--- a/src/main/java/de/b2tla/B2TLAGlobals.java
+++ b/src/main/java/de/b2tla/B2TLAGlobals.java
@@ -9,6 +9,7 @@ public class B2TLAGlobals {
private static boolean checkDeadlock;
private static boolean checkInvariant;
private static boolean checkLTL;
+ private static boolean proBconstantsSetup;
private static boolean deleteFilesOnExit;
@@ -17,6 +18,8 @@ public class B2TLAGlobals {
private static boolean hideTLCConsoleOutput;
private static boolean createTraceFile;
+ private static boolean testingMode;
+
private static boolean cleanup;
private static int workers;
@@ -37,6 +40,7 @@ public class B2TLAGlobals {
checkDeadlock = true;
checkInvariant = true;
checkLTL = true;
+ setProBconstantsSetup(false);
setCleanup(true);
@@ -52,6 +56,7 @@ public class B2TLAGlobals {
// the created B2TLA standard modules (e.g.
// Relation, but not Naturals etc.).
runTestscript = false;
+ testingMode = false;
createTraceFile = true;
}
@@ -174,5 +179,21 @@ public class B2TLAGlobals {
public static void setCleanup(boolean cleanup) {
B2TLAGlobals.cleanup = cleanup;
}
+
+ public static boolean isProBconstantsSetup() {
+ return proBconstantsSetup;
+ }
+
+ public static void setProBconstantsSetup(boolean proBconstantsSetup) {
+ B2TLAGlobals.proBconstantsSetup = proBconstantsSetup;
+ }
+
+ public static void setTestingMode(boolean b){
+ B2TLAGlobals.testingMode = b;
+ }
+
+ public static boolean getTestingMode(){
+ return B2TLAGlobals.testingMode;
+ }
}
diff --git a/src/main/java/de/b2tla/B2TlaTranslator.java b/src/main/java/de/b2tla/B2TlaTranslator.java
index e717c22239140f60646a3fcd72021ffb8679ea30..0ebda89cb4a695c568661d2748e881634066e14f 100644
--- a/src/main/java/de/b2tla/B2TlaTranslator.java
+++ b/src/main/java/de/b2tla/B2TlaTranslator.java
@@ -10,15 +10,15 @@ import de.b2tla.analysis.ConstantsEvaluator;
import de.b2tla.analysis.DefinitionsAnalyser;
import de.b2tla.analysis.MachineContext;
import de.b2tla.analysis.NotSupportedConstructs;
-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.UsedStandardModules;
import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES;
import de.b2tla.analysis.transformation.DefinitionsEliminator;
+import de.b2tla.analysis.typerestriction.TypeRestrictor;
+import de.b2tla.analysis.unchangedvariables.UnchangedVariablesFinder;
import de.b2tla.prettyprint.TLAPrinter;
import de.b2tla.tla.Generator;
import de.b2tla.tlc.TLCOutputInfo;
@@ -48,7 +48,7 @@ public class B2TlaTranslator {
start = parser.parse(machineString, false);
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- System.out.println(ast2String2.toString());
+ //System.out.println(ast2String2.toString());
}
public B2TlaTranslator(String machineString, String ltlFormula)
@@ -59,7 +59,7 @@ public class B2TlaTranslator {
start = parser.parse(machineString, false);
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- System.out.println(ast2String2.toString());
+ //System.out.println(ast2String2.toString());
}
public B2TlaTranslator(String machineName, File machineFile, String ltlFormula, String constantSetup)
@@ -79,12 +79,12 @@ public class B2TlaTranslator {
final Ast2String ast2String2 = new Ast2String();
start2.apply(ast2String2);
- System.out.println(ast2String2.toString());
+ //System.out.println(ast2String2.toString());
}
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- System.out.println(ast2String2.toString());
+ //System.out.println(ast2String2.toString());
}
public void translate() {
diff --git a/src/main/java/de/b2tla/StandardModules.java b/src/main/java/de/b2tla/StandardModules.java
deleted file mode 100644
index 48e122e9168a4fd3c760b802c73ca072209b9df0..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/StandardModules.java
+++ /dev/null
@@ -1,103 +0,0 @@
-package de.b2tla;
-
-public class StandardModules {
-
- public final static String BBuiltIns = "---- MODULE BBuiltIns ----\n"
- + "EXTENDS Integers, FiniteSets \n"
- + "RECURSIVE SIGMA(_) \n"
- + "SIGMA(S) == "
- + "LET e == CHOOSE e \\in S: TRUE"
- + " IN IF S = {} THEN 0 ELSE e + SIGMA(S \\ {e}) \n"
- + "succ[x \\in Int] == x + 1 \n "
- + "pred[x \\in Int] == x - 1 \n"
- + "POW1(S) == (SUBSET S) \\ {{}} \n"
- + "FIN(S) == {x \\in SUBSET S: IsFiniteSet(x)} \n"
- + "FIN1(S) == {x \\in SUBSET S: IsFiniteSet(x) /\\ x # {}}"
- + "a \\subset b == a \\subseteq b /\\ a # b \n"
- + "notSubset(a, b) == ~ (a \\subseteq b) \n"
- + "notStrictSubset(a, b) == ~ (a \\subset b ) \n"
- + "RECURSIVE INTER(_) \n"
- + "INTER(S) == "
- + "LET e == (CHOOSE e \\in S: TRUE) \n"
- + " IN IF Cardinality(S) = 1 THEN e ELSE e \\cap INTER(S \\ {e}) \n"
- + "=========";
-
- public final static String Relations = "---- MODULE Relations -----\n"
- + "EXTENDS TLC, Sequences, FiniteSets, Integers \n"
- + "domain(r) == {x[1]: x \\in r}\n"
- + "range(r) == {x[2]: x \\in r} \n"
- + "id(S) == {<<x,x>>: x \\in S}\n"
- + "set_of_relations(x,y) == SUBSET (x \\times y)\n"
- + "domain_restriction(S, r) == {x \\in r: x[1] \\in S} \n"
- + "domain_substraction(S, r) == {x \\in r: x[1] \\notin S} \n"
- + "range_restriction(S, r) == {x \\in r: x[2] \\in S} \n"
- + "range_substraction(S, r) == {x \\in r: x[2] \\notin S} \n"
- + "rel_inverse(r) == {<<x[2],x[1]>>: x \\in r} \n"
- + "relational_image(r, S) =={y[2] :y \\in {x \\in r: x[1] \\in S}} \n"
- + "relational_overriding(r, r2) == {x \\in r: x[1] \\notin domain(r2)} \\cup r2 \n"
- + "relational_overriding2(r, p, v) == {x \\in r: x[1] # p} \\cup {<<p, v>>} \n"
- + "direct_product(r1, r2) == {<<x, u>> \\in (domain(r1) \\cup domain(r2)) \\times (range(r1) \\times range(r2)): \n"
- + " u[1] \\in relational_image(r1, {x}) /\\ u[2] \\in relational_image(r2,{x})}"
- + "direct_product2(r1, r2) == {u \\in (domain(r1) \\cup domain(r2)) \\times (range(r1) \\times range(r2)):"
- + " <<u[1],u[2][1]>> \\in r1 /\\ <<u[1],u[2][2]>> \\in r2} \n"
- + "relational_composition(r1, r2) == {<<u[1][1],u[2][2]>> : u \\in \n"
- + " {x \\in range_restriction(domain(r2),r1) \\times domain_restriction(range(r1) ,r2): x[1][2] = x[2][1]}} \n"
- + "prj1(E, F) == {u \\in E \\times F \\times E: u[1] = u[3]} \n"
- + "prj2(E, F) == {u \\in E \\times F \\times F: u[2] = u[3]} \n"
- + "RECURSIVE iterate(_,_) \n"
- + "iterate(r, n) == CASE n = 0 -> id(domain(r) \\cup range(r)) \n"
- + " [] n = 1 -> r \n"
- + " [] OTHER -> iterate(relational_composition(r,r), n-1) \n"
- + "RECURSIVE closure1(_) \n"
- + "closure1(R) == IF relational_composition(R,R) \\R # {} \n"
- + " THEN R \\cup closure1(relational_composition(R,R)) \n"
- + " ELSE R \n"
- + "closure(R) == closure1( R \\cup {<<x[1],x[1]>>: x \\in R} \\cup {<<x[2],x[2]>>: x \\in R}) \n"
- + "relational_call(r, x) == (CHOOSE y \\in r: y[1] = x)[2] \n"
-
-
-
- + "is_partial_func(f) == \\A x \\in domain(f): Cardinality(relational_image(f, {x})) =< 1 \n"
- + "is_partial_func2(f, S, S2) == /\\ \\A x \\in f: x[1] \\in S /\\ x[2] \\in S2 /\\ relational_image(f, {x[1]}) = {x[2]} \n"
-
-
- + "func_ran(f) == {f[x] : x \\in DOMAIN f} \n"
- + "make_rel(f) == {<<x, f[x]>>: x \\in DOMAIN f} \n"
-
- //total
- //func
- + "i_total_func(S,S2) == {f \\in [S -> S2]: Cardinality(DOMAIN f) = Cardinality(func_ran(f))} \n"
- //rel
- + "total_func_rel(S, S2) == make_rel([S -> S2]) \n"
- + "i_total_func_rel(S, S2) == make_rel(i_total_func(S, S2)) \n"
-
-
- //partial function
- + "partial_func(S, S2) == UNION{[x -> S2] :x \\in SUBSET S} \n"
- + "partial_func_rel(S, S2) == {make_rel(f): f \\in UNION{[x -> S2] :x \\in SUBSET S}}\n"
- + "i_partial_func(S, S2)== {f \\in partial_func(S, S2): Cardinality(DOMAIN f) = Cardinality(func_ran(f))}"
-
- + "is_func(f) == \\A x \\in domain(f): Cardinality(relational_image(f, {x})) < 2 \n"
- + "total_func(S, S2) == {x \\in (SUBSET (S \\times S2)): is_func(x) /\\ domain(x)= S} \n"
-
- + "is_total_func(f, S, S2) == domain(f) = S /\\ \\A x \\in f: x[1] \\in S /\\ x[2] \\in S2 /\\ relational_image(f, {x[1]}) = {x[2]} \n"
-
- + "is_injectiv_func(f) == \\A x \\in range(f): Cardinality(relational_image(rel_inverse(f), {x})) =< 1 \n"
- + "total_injection(S, S2) == {x \\in (SUBSET (S \\times S2)): is_func(x) /\\ domain(x)= S /\\ is_injectiv_func(x) } \n"
- + "partial_injection(S, S2) == {x \\in (SUBSET (S \\times S2)): is_func(x) /\\ is_injectiv_func(x) } \n"
-
- + "total_surjection(S, S2) == {x \\in (SUBSET (S \\times S2)): is_func(x)/\\ domain(x)= S /\\ S2 = range(x)} \n"
- + "partial_surjection(S, S2) == {x \\in (SUBSET (S \\times S2)): is_func(x)/\\ S2 = range(x)} \n"
-
- + "total_bijection(S, S2) == {x \\in (SUBSET (S \\times S2)): is_func(x) /\\ domain(x) = S /\\ is_injectiv_func(x) /\\ S2 = range(x)} \n"
-
- + "iseq(S) == {x \\in SUBSET {<<x,y>> \\in (1 .. Cardinality(S)) \\times S : TRUE }: \n"
- + " /\\ Cardinality(x) =< Cardinality(S)\n"
- + " /\\ \\E z \\in 0.. Cardinality(S): domain(x) = 1..z\n"
- + " /\\ is_func(x)\n"
- + " /\\ is_injectiv_func(x)} \n"
- + "iseq1(S) == iseq(S) \\ {{}} \n"
- + "concat(s, s2) == {<<i, IF i \\leq Cardinality(s) THEN relational_call(s, i) ELSE relational_call(s2, i-Cardinality(s))>>: i \\in 1.. (Cardinality(s) + Cardinality(s2))} \n"
- + "============";
-
-}
diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java
index b82a1ea8a5774f4fd22d1dc917b1cb347f71fe2e..824ff3dc3835161b247662a5e5ec69a7b9193255 100644
--- a/src/main/java/de/b2tla/TLCRunner.java
+++ b/src/main/java/de/b2tla/TLCRunner.java
@@ -1,14 +1,12 @@
package de.b2tla;
import java.io.BufferedReader;
-import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.PrintStream;
-import java.lang.reflect.Field;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
@@ -19,8 +17,6 @@ import de.b2tla.util.BTLCPrintStream;
import util.SimpleFilenameToStream;
import util.ToolIO;
import tlc2.TLC;
-import tlc2.tool.ModelChecker;
-import tlc2.tool.TLCStateInfo;
public class TLCRunner {
@@ -77,7 +73,6 @@ public class TLCRunner {
String[] args = list.toArray(new String[list.size()]);
System.out.println("Starting JVM...");
final Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
-
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
stdOut.start();
StreamGobbler errOut = new StreamGobbler(p.getErrorStream());
@@ -134,31 +129,8 @@ public class TLCRunner {
System.setOut(systemOut);
- String [] a = ToolIO.getAllMessages();
- for (int i = 0; i < a.length; i++) {
- //System.out.println(a[i]);
- }
- //ToolIO.printAllMessages();
-
ArrayList<String> messages = btlcStream.getArrayList();
-
- Field field;
- try {
- field = TLC.class.getDeclaredField("instance");
- field.setAccessible(true);
- ModelChecker mc = (ModelChecker) field.get(tlc);
- //System.out.println(mc.trace.printTrace(arg0, arg1););
- //TLCStateInfo[] states = value.trace.getTrace();
-// for (int i = 0; i < states.length; i++) {
-// System.out.println(states[i]);
-// }
-
- } catch (Exception e1) {
- // TODO Auto-generated catch block
- e1.printStackTrace();
- }
-
System.out.println("--------------------------------");
closeThreads();
return messages;
diff --git a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
index 5516ec9c5816fe8cf2414b74ebfc2e19615ae3c8..057ef9a5487bd790bbab137382a2dc5f4efadd79 100644
--- a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
+++ b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
@@ -12,19 +12,21 @@ import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
+import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AGreaterPredicate;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AIntegerExpression;
import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
import de.be4.classicalb.core.parser.node.ALessEqualPredicate;
+import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
/**
- * In the class the order of constants is determined. Constants can depend on
+ * In this class the order of constants is determined. Constants can depend on
* other constants: as an example in the expression k = k2 + 1 the value of the
* constant k depends on k2. Constants are translated as definitions to TLA+ and
* these definitions must be in order.
@@ -69,6 +71,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
ConstantsInTreeFinder constantInTreeFinder = new ConstantsInTreeFinder();
+ if(machineContext.getConstantsSetup()!= null){
+ machineContext.getConstantsSetup().apply(constantInTreeFinder);
+ }
+
APropertiesMachineClause properties = machineContext
.getPropertiesMachineClause();
if (null != properties) {
@@ -139,7 +145,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
HashSet<Node> set = dependsOnIdentifierTable.get(node);
Node parent = node.parent();
HashSet<Node> parentSet = dependsOnIdentifierTable.get(parent);
- parentSet.addAll(set);
+ if(parentSet!= null){
+ parentSet.addAll(set);
+ }
+
}
@Override
@@ -147,6 +156,12 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
defaultIn(node);
node.getPredicates().apply(this);
}
+
+ @Override
+ public void caseAPredicateParseUnit(APredicateParseUnit node){
+ defaultIn(node);
+ node.getPredicate();
+ }
@Override
public void caseAConstraintsMachineClause(AConstraintsMachineClause node) {
@@ -191,11 +206,17 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
.getPredicates(),
false);
}
+
+ if(machineContext.getConstantsSetup() != null){
+ analysePredicate(machineContext.getConstantsSetup(), true);
+ }
+
Node properties = machineContext.getPropertiesMachineClause();
if (properties != null) {
- analysePredicate(
- ((APropertiesMachineClause) properties).getPredicates(),
- true);
+ PPredicate predicate = (PPredicate) ((APropertiesMachineClause) properties)
+ .getPredicates();
+ analysePredicate(predicate, true);
+
}
Node invariantClause = machineContext.getInvariantMachineClause();
@@ -219,13 +240,13 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
private void analysePredicate(Node node, boolean isProperties) {
if (node instanceof AEqualPredicate) {
analyseEqualsPredicate((AEqualPredicate) node);
- }
-// else if (node instanceof AGreaterPredicate) {
-// analyseGreaterPredicate((AGreaterPredicate) node);
-// }
-// else if (node instanceof ALessEqualPredicate) {
-// analyseLessEqualPredicate((ALessEqualPredicate) node);
-// }
+ }
+ // else if (node instanceof AGreaterPredicate) {
+ // analyseGreaterPredicate((AGreaterPredicate) node);
+ // }
+ // else if (node instanceof ALessEqualPredicate) {
+ // analyseLessEqualPredicate((ALessEqualPredicate) node);
+ // }
else if (node instanceof AConjunctPredicate) {
AConjunctPredicate conjunction = (AConjunctPredicate) node;
analysePredicate(conjunction.getLeft(), isProperties);
diff --git a/src/main/java/de/b2tla/analysis/MachineContext.java b/src/main/java/de/b2tla/analysis/MachineContext.java
index bab46a8730e83a9d6fcfd1e8cb7a50e9437f428d..4e35c6479ab45801dcc6319c0cbcac3f5e871020 100644
--- a/src/main/java/de/b2tla/analysis/MachineContext.java
+++ b/src/main/java/de/b2tla/analysis/MachineContext.java
@@ -76,8 +76,8 @@ public class MachineContext extends DepthFirstAdapter {
private PMachineHeader header;
private final Start start;
private final Hashtable<String, MachineContext> machineContextsTable;
- private ArrayList<LTLFormulaVisitor> ltlVisitors;
- private PPredicate constantSetup;
+ private final ArrayList<LTLFormulaVisitor> ltlVisitors;
+ private final PPredicate constantsSetup;
// machine identifier
private final LinkedHashMap<String, Node> setParameter;
@@ -86,6 +86,7 @@ public class MachineContext extends DepthFirstAdapter {
private final LinkedHashMap<String, Node> deferredSets;
private final LinkedHashMap<String, Node> enumeratedSets;
private final LinkedHashMap<String, Node> enumValues;
+
private final LinkedHashMap<String, Node> constants;
private final LinkedHashMap<String, Node> variables;
private final LinkedHashMap<String, Node> definitions;
@@ -110,33 +111,10 @@ public class MachineContext extends DepthFirstAdapter {
private final Hashtable<Node, Node> referencesTable;
- // 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(String machineName, Start start, String ltlFormula, PPredicate constantSetup) {
+ public MachineContext(String machineName, Start start, String ltlFormula, PPredicate constantsSetup) {
this.start = start;
this.machineName = machineName;
- this.constantSetup = constantSetup;
+ this.constantsSetup = constantsSetup;
this.referencesTable = new Hashtable<Node, Node>();
this.ltlVisitors = new ArrayList<LTLFormulaVisitor>();
@@ -149,19 +127,41 @@ public class MachineContext extends DepthFirstAdapter {
this.setParameter = new LinkedHashMap<String, Node>();
this.scalarParameter = new LinkedHashMap<String, Node>();
- deferredSets = new LinkedHashMap<String, Node>();
- enumeratedSets = new LinkedHashMap<String, Node>();
- enumValues = new LinkedHashMap<String, Node>();
- constants = new LinkedHashMap<String, Node>();
- variables = 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.variables = new LinkedHashMap<String, Node>();
this.definitions = new LinkedHashMap<String, Node>();
- operations = new LinkedHashMap<String, Node>();
- seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
+ this.operations = new LinkedHashMap<String, Node>();
+ this.seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
this.machineContextsTable = new Hashtable<String, MachineContext>();
start.apply(this);
checkLTLFormulas();
+
+ checkConstantsSetup();
+ }
+
+ private void checkConstantsSetup() {
+ if(constantsSetup == null){
+ return;
+ }
+
+ this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
+
+ ArrayList<MachineContext> list = lookupExtendedMachines();
+ for (int i = 0; i < list.size(); i++) {
+ MachineContext s = list.get(i);
+ contextTable.add(s.getDeferredSets());
+ contextTable.add(s.getEnumeratedSets());
+ contextTable.add(s.getEnumValues());
+ contextTable.add(s.getConstants());
+ contextTable.add(s.getDefinitions());
+ }
+ constantsSetup.apply(this);
+
}
private void checkLTLFormulas() {
@@ -568,11 +568,6 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
this.propertiesMachineClause = node;
- if(constantSetup != null){
- AConjunctPredicate and = new AConjunctPredicate(constantSetup, node.getPredicates());
- node.setPredicates(and);
- }
-
/**
* check identifier scope in properties clauses
*/
@@ -1080,6 +1075,10 @@ public class MachineContext extends DepthFirstAdapter {
ADefinitionsMachineClause definitionMachineClause) {
this.definitionMachineClause = definitionMachineClause;
}
+
+ public PPredicate getConstantsSetup() {
+ return constantsSetup;
+ }
}
diff --git a/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java b/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
deleted file mode 100644
index 812568b139a05f82552e855b6a57a09ad8ea183b..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java
+++ /dev/null
@@ -1,206 +0,0 @@
-
-/*
- * currently not used
- */
-package de.b2tla.analysis;
-
-import java.util.ArrayList;
-import java.util.Hashtable;
-import java.util.LinkedList;
-import java.util.List;
-
-import de.b2tla.exceptions.ScopeException;
-import de.be4.classicalb.core.parser.Utils;
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
-import de.be4.classicalb.core.parser.node.ADeferredSetSet;
-import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
-import de.be4.classicalb.core.parser.node.AIdentifierExpression;
-import de.be4.classicalb.core.parser.node.AMachineHeader;
-import de.be4.classicalb.core.parser.node.AOperation;
-import de.be4.classicalb.core.parser.node.ASeesMachineClause;
-import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
-import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
-
-public class MachineDeclarationsCollector extends DepthFirstAdapter {
-
- private String machineName;
- private final Node start;
-
- private final Hashtable<String, Node> machineParameters;
- private final Hashtable<String, Node> deferredSets;
- private final Hashtable<String, Node> enumeratedSets;
- private final Hashtable<String, Node> enumValues;
- private final Hashtable<String, Node> constants;
- private final Hashtable<String, Node> variables;
- private final Hashtable<String, Node> operations;
-
- private final Hashtable<String, AIdentifierExpression> seenMachines;
-
- public MachineDeclarationsCollector(Node start) {
- this.start = start;
- machineParameters = new Hashtable<String, Node>();
- deferredSets = new Hashtable<String, Node>();
- enumeratedSets = new Hashtable<String, Node>();
- enumValues = new Hashtable<String, Node>();
- constants = new Hashtable<String, Node>();
- variables = new Hashtable<String, Node>();
- operations = new Hashtable<String, Node>();
- seenMachines = new Hashtable<String, AIdentifierExpression>();
-
- start.apply(this);
- }
-
- public String getName() {
- return machineName;
- }
-
- public Node getStart() {
- return start;
- }
-
- public Hashtable<String, Node> getConstants() {
- return constants;
- }
-
- public Hashtable<String, Node> getVariables() {
- return variables;
- }
-
- public Hashtable<String, Node> getOperations() {
- return operations;
- }
-
- public Hashtable<String, Node> getDeferredSets() {
- return deferredSets;
- }
-
- public Hashtable<String, Node> getEnumeratedSets() {
- return enumeratedSets;
- }
-
- public Hashtable<String, Node> getEnumValues() {
- return enumValues;
- }
-
- public Hashtable<String, Node> getMachineParameters() {
- return machineParameters;
- }
-
- public Hashtable<String, AIdentifierExpression> getSeenMachines() {
- return seenMachines;
- }
-
- private void exist(LinkedList<TIdentifierLiteral> list) {
- String name = Utils.getIdentifierAsString(list);
- if (constants.containsKey(name) || variables.containsKey(name)
- || operations.containsKey(name)
- || deferredSets.containsKey(name)
- || enumeratedSets.containsKey(name)
- || enumValues.containsKey(name)
- || machineParameters.containsKey(name)
- || seenMachines.containsKey(name)) {
- throw new ScopeException("Duplicate identifier: '" + name + "'");
- }
- }
-
- @Override
- public void caseASeesMachineClause(ASeesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getMachineNames());
- for (PExpression e : copy) {
- AIdentifierExpression p = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(p.getIdentifier());
-
- try {
- exist(p.getIdentifier());
- } catch (ScopeException e2) {
- throw new ScopeException("Machine '" + name
- + "' is seen twice.");
- }
-
- seenMachines.put(name, p);
- }
- }
-
- @Override
- public void caseAMachineHeader(AMachineHeader node) {
- {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getName());
- machineName = Utils.getIdentifierAsString(copy);
-
- }
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
- for (PExpression e : copy) {
- AIdentifierExpression p = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(p.getIdentifier());
- exist(p.getIdentifier());
- machineParameters.put(name, p);
- }
- }
- }
-
- @Override
- public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- AIdentifierExpression c = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(c.getIdentifier());
- exist(c.getIdentifier());
- constants.put(name, c);
- }
- }
-
- @Override
- public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- AIdentifierExpression v = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(v.getIdentifier());
- exist(v.getIdentifier());
- variables.put(name, v);
- }
- }
-
- @Override
- public void caseADeferredSetSet(ADeferredSetSet node) {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
- String name = Utils.getIdentifierAsString(copy);
- exist(node.getIdentifier());
- deferredSets.put(name, node);
- }
-
- @Override
- public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
- {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
- String name = Utils.getIdentifierAsString(copy);
- exist(node.getIdentifier());
- enumeratedSets.put(name, node);
- }
- List<PExpression> copy = new ArrayList<PExpression>(node.getElements());
- for (PExpression e : copy) {
- AIdentifierExpression v = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(v.getIdentifier());
- exist(v.getIdentifier());
- enumValues.put(name, v);
- }
- }
-
- @Override
- public void caseAOperation(AOperation node) {
- String name = Utils.getIdentifierAsString(node.getOpName());
- exist(node.getOpName());
- operations.put(name, node);
- }
-
-}
diff --git a/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java b/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
index 44af9247865862dd842abcb1c1ac9a5f87011c0b..3148bcf16f30021622e62a4a1d3fb26456b82e1e 100644
--- a/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
+++ b/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
@@ -3,6 +3,7 @@ package de.b2tla.analysis;
import de.b2tla.exceptions.NotSupportedException;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACaseSubstitution;
+import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
import de.be4.classicalb.core.parser.node.AWhileSubstitution;
import de.be4.classicalb.core.parser.node.Start;
@@ -21,5 +22,11 @@ public class NotSupportedConstructs extends DepthFirstAdapter{
{
throw new NotSupportedException("Case substitutions are currently not supported.");
}
+
+ public void inASequenceSubstitution(ASequenceSubstitution node)
+ {
+ throw new NotSupportedException("Sequence substitutions ';' are currently not supported.");
+ }
+
}
diff --git a/src/main/java/de/b2tla/analysis/ScopeChecker.java b/src/main/java/de/b2tla/analysis/ScopeChecker.java
deleted file mode 100644
index aa9d7ae0d6e28c02c065309df039e948c35517b6..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/analysis/ScopeChecker.java
+++ /dev/null
@@ -1,447 +0,0 @@
-package de.b2tla.analysis;
-
-import java.util.ArrayList;
-import java.util.Hashtable;
-import java.util.List;
-
-
-import de.b2tla.exceptions.ScopeException;
-import de.be4.classicalb.core.parser.Utils;
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
-import de.be4.classicalb.core.parser.node.AAssignSubstitution;
-import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
-import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
-import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
-import de.be4.classicalb.core.parser.node.AExistsPredicate;
-import de.be4.classicalb.core.parser.node.AForallPredicate;
-import de.be4.classicalb.core.parser.node.AGeneralProductExpression;
-import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
-import de.be4.classicalb.core.parser.node.AIdentifierExpression;
-import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
-import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
-import de.be4.classicalb.core.parser.node.ALambdaExpression;
-import de.be4.classicalb.core.parser.node.AMachineHeader;
-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.APropertiesMachineClause;
-import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
-import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression;
-import de.be4.classicalb.core.parser.node.ASeesMachineClause;
-import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
-import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.be4.classicalb.core.parser.node.PMachineClause;
-import de.be4.classicalb.core.parser.node.POperation;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
-
-public class ScopeChecker extends DepthFirstAdapter {
-
- private final Hashtable<Node, Node> referencesTable;
-
- private ArrayList<Hashtable<String, Node>> contextTable;
-
- private final Hashtable<String, MachineDeclarationsCollector> scopeTable;
-
- private final MachineDeclarationsCollector declarations;
-
- public Hashtable<Node, Node> getReferencesTable() {
- return referencesTable;
- }
-
- public ScopeChecker(MachineDeclarationsCollector c,
- Hashtable<String, MachineDeclarationsCollector> table) {
-
- declarations = c;
-
- if (table == null)
- scopeTable = new Hashtable<String, MachineDeclarationsCollector>();
- else
- scopeTable = table;
-
- referencesTable = new Hashtable<Node, Node>();
-
- c.getStart().apply(this);
- }
-
- private void putLocalVariableIntoCurrentScope(AIdentifierExpression node)
- throws ScopeException {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
- Hashtable<String, Node> currentScope = contextTable.get(contextTable
- .size() - 1);
- if (currentScope.containsKey(name)) {
- throw new ScopeException("Duplicate Identifier: " + name);
- } else {
- currentScope.put(name, node);
- }
- }
-
- @Override
- public void caseAIdentifierExpression(AIdentifierExpression node) {
- lookupIdentifier(node);
-
- }
-
- private void lookupIdentifier(AIdentifierExpression node) {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
- for (int i = contextTable.size() - 1; i >= 0; i--) {
- Hashtable<String, Node> currentScope = contextTable.get(i);
- if (currentScope.containsKey(name)) {
- this.referencesTable.put(node, currentScope.get(name));
- return;
- }
- }
- throw new ScopeException("Unkown Identifier: '" + name
- + "' at position: " + node.getStartPos());
- }
-
- @Override
- public void caseAAbstractMachineParseUnit(AAbstractMachineParseUnit node) {
- inAAbstractMachineParseUnit(node);
- if (node.getVariant() != null) {
- node.getVariant().apply(this);
- }
-
- if (node.getHeader() != null) {
- node.getHeader().apply(this);
- }
- {
- List<PMachineClause> copy = new ArrayList<PMachineClause>(
- node.getMachineClauses());
-
- for (PMachineClause e : copy) {
- e.apply(this);
- }
- }
- outAAbstractMachineParseUnit(node);
- }
-
- @Override
- public void caseAMachineHeader(AMachineHeader node) {
- }
-
- @Override
- public void caseASeesMachineClause(ASeesMachineClause node) {
- }
-
- @Override
- public void caseAConstraintsMachineClause(AConstraintsMachineClause node) {
- this.contextTable = new ArrayList<Hashtable<String, Node>>();
- this.contextTable.add(declarations.getMachineParameters());
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- }
-
- @Override
- public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
- }
-
- @Override
- public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- }
-
- private ArrayList<MachineDeclarationsCollector> lookupExtendedMachines() {
- ArrayList<MachineDeclarationsCollector> list = new ArrayList<MachineDeclarationsCollector>();
- for (String s : declarations.getSeenMachines().keySet()) {
- AIdentifierExpression i = declarations.getSeenMachines().get(s);
- if (i.getIdentifier().size() == 1) {
- list.add(scopeTable.get(s));
- }
- }
- list.add(declarations);
- return list;
- }
-
- @Override
- public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
-
- this.contextTable = new ArrayList<Hashtable<String, Node>>();
-
- ArrayList<MachineDeclarationsCollector> list = lookupExtendedMachines();
- for (int i = 0; i < list.size(); i++) {
- MachineDeclarationsCollector s = list.get(i);
- contextTable.add(s.getDeferredSets());
- contextTable.add(s.getEnumeratedSets());
- contextTable.add(s.getEnumValues());
- contextTable.add(s.getConstants());
- }
-
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- }
-
- @Override
- public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- }
-
- @Override
- public void caseAInvariantMachineClause(AInvariantMachineClause node) {
- this.contextTable = new ArrayList<Hashtable<String, Node>>();
-
- ArrayList<MachineDeclarationsCollector> list = lookupExtendedMachines();
- for (int i = 0; i < list.size(); i++) {
- MachineDeclarationsCollector s = list.get(i);
- this.contextTable.add(s.getMachineParameters());
- this.contextTable.add(s.getDeferredSets());
- this.contextTable.add(s.getEnumeratedSets());
- this.contextTable.add(s.getEnumValues());
- this.contextTable.add(s.getConstants());
- this.contextTable.add(s.getVariables());
- }
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- }
-
- @Override
- public void caseAInitialisationMachineClause(
- AInitialisationMachineClause node) {
- this.contextTable = new ArrayList<Hashtable<String, Node>>();
-
- ArrayList<MachineDeclarationsCollector> list = lookupExtendedMachines();
- for (int i = 0; i < list.size(); i++) {
- MachineDeclarationsCollector s = list.get(i);
-
- this.contextTable.add(s.getMachineParameters());
- this.contextTable.add(s.getDeferredSets());
- this.contextTable.add(s.getEnumeratedSets());
- this.contextTable.add(s.getEnumValues());
- this.contextTable.add(s.getConstants());
- this.contextTable.add(s.getVariables());
- }
- if (node.getSubstitutions() != null) {
- node.getSubstitutions().apply(this);
- }
- }
-
- @Override
- public void caseAOperationsMachineClause(AOperationsMachineClause node) {
- this.contextTable = new ArrayList<Hashtable<String, Node>>();
-
- ArrayList<MachineDeclarationsCollector> list = lookupExtendedMachines();
- for (int i = 0; i < list.size(); i++) {
- MachineDeclarationsCollector s = list.get(i);
- this.contextTable.add(s.getMachineParameters());
- this.contextTable.add(s.getDeferredSets());
- this.contextTable.add(s.getEnumeratedSets());
- this.contextTable.add(s.getEnumValues());
- this.contextTable.add(s.getConstants());
- this.contextTable.add(s.getVariables());
- }
-
- List<POperation> copy = new ArrayList<POperation>(node.getOperations());
- for (POperation e : copy) {
- e.apply(this);
- }
- }
-
- @Override
- public void caseAOperation(AOperation node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getReturnValues());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getOpName());
- for (TIdentifierLiteral e : copy) {
- e.apply(this);
- }
- }
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getOperationBody() != null) {
- node.getOperationBody().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseAAssignSubstitution(AAssignSubstitution node) {
- // TODO maybe give better feedback to the user, e.g. can not assign a
- // value to constant 'c'
- ArrayList<Hashtable<String, Node>> temp = contextTable;
- {
- contextTable = new ArrayList<Hashtable<String, Node>>();
- contextTable.add(declarations.getVariables());
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getLhsExpression());
- for (PExpression e : copy) {
- e.apply(this);
- }
- }
- {
- contextTable = temp;
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getRhsExpressions());
- for (PExpression e : copy) {
- e.apply(this);
- }
- }
- }
-
- @Override
- public void caseAOpSubstitution(AOpSubstitution node) {
- if (node.getName() != null) {
- AIdentifierExpression op = (AIdentifierExpression) node.getName();
- String name = Utils.getIdentifierAsString(op.getIdentifier());
- Node o = declarations.getOperations().get(name); // TODO operation
- // of an
- // external
- // machine
- if (o != null) {
- this.referencesTable.put(op, o);
- } else {
- throw new ScopeException("Unknown operation '" + name + "'");
- }
- }
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
- for (PExpression e : copy) {
- e.apply(this);
- }
- }
- }
-
- @Override
- public void caseAForallPredicate(AForallPredicate node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getImplication() != null) {
- node.getImplication().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseAExistsPredicate(AExistsPredicate node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getPredicate() != null) {
- node.getPredicate().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseALambdaExpression(ALambdaExpression node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getPredicate() != null) {
- node.getPredicate().apply(this);
- }
- if (node.getExpression() != null) {
- node.getExpression().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- if (node.getExpression() != null) {
- node.getExpression().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseAQuantifiedIntersectionExpression(
- AQuantifiedIntersectionExpression node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- if (node.getExpression() != null) {
- node.getExpression().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseAGeneralProductExpression(AGeneralProductExpression node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- if (node.getExpression() != null) {
- node.getExpression().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
- @Override
- public void caseAGeneralSumExpression(AGeneralSumExpression node) {
- contextTable.add(new Hashtable<String, Node>());
- {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
- for (PExpression e : copy) {
- putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
- }
- }
- if (node.getPredicates() != null) {
- node.getPredicates().apply(this);
- }
- if (node.getExpression() != null) {
- node.getExpression().apply(this);
- }
- contextTable.remove(contextTable.size() - 1);
- }
-
-}
diff --git a/src/main/java/de/b2tla/analysis/UsedStandardModules.java b/src/main/java/de/b2tla/analysis/UsedStandardModules.java
index fe8e1dd6d0445df58eb717bc62dcbefc05c0f5cd..bad73b0c8c69a31e1eb171f8989f8e4a267e0849 100644
--- a/src/main/java/de/b2tla/analysis/UsedStandardModules.java
+++ b/src/main/java/de/b2tla/analysis/UsedStandardModules.java
@@ -7,6 +7,7 @@ import java.util.List;
import java.util.Set;
import java.util.Collections;
+import de.b2tla.analysis.typerestriction.TypeRestrictor;
import de.b2tla.btypes.BType;
import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
diff --git a/src/main/java/de/b2tla/analysis/IdentifierDependencies.java b/src/main/java/de/b2tla/analysis/typerestriction/IdentifierDependencies.java
similarity index 95%
rename from src/main/java/de/b2tla/analysis/IdentifierDependencies.java
rename to src/main/java/de/b2tla/analysis/typerestriction/IdentifierDependencies.java
index ce63c85dd6587b217a30f8c6c10207c967940940..c0a0367775a92cdc62656717915967aee3dd84cd 100644
--- a/src/main/java/de/b2tla/analysis/IdentifierDependencies.java
+++ b/src/main/java/de/b2tla/analysis/typerestriction/IdentifierDependencies.java
@@ -1,10 +1,11 @@
-package de.b2tla.analysis;
+package de.b2tla.analysis.typerestriction;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
+import de.b2tla.analysis.MachineContext;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
diff --git a/src/main/java/de/b2tla/analysis/TypeRestrictor.java b/src/main/java/de/b2tla/analysis/typerestriction/TypeRestrictor.java
similarity index 92%
rename from src/main/java/de/b2tla/analysis/TypeRestrictor.java
rename to src/main/java/de/b2tla/analysis/typerestriction/TypeRestrictor.java
index f7fc53dd26480f6f9740547f7c002bec3bb96268..2ae78ec3d90fdfe08e06e3522ef5ce10538cdbab 100644
--- a/src/main/java/de/b2tla/analysis/TypeRestrictor.java
+++ b/src/main/java/de/b2tla/analysis/typerestriction/TypeRestrictor.java
@@ -1,10 +1,12 @@
-package de.b2tla.analysis;
+package de.b2tla.analysis.typerestriction;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
+import de.b2tla.analysis.MachineContext;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.analysis.nodes.ElementOfNode;
import de.b2tla.analysis.nodes.EqualsNode;
import de.b2tla.analysis.nodes.NodeType;
@@ -15,6 +17,7 @@ import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
+import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
import de.be4.classicalb.core.parser.node.AForallPredicate;
@@ -35,6 +38,7 @@ import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.ASubsetPredicate;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AForallLtl;
@@ -59,6 +63,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
this.identifierDependencies = new IdentifierDependencies(machineContext);
+
start.apply(this);
checkLTLFormulas();
@@ -126,9 +131,21 @@ public class TypeRestrictor extends DepthFirstAdapter {
public void inAPropertiesMachineClause(APropertiesMachineClause node) {
HashSet<Node> list = new HashSet<Node>();
list.addAll(machineContext.getConstants().values());
+
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
+
+ public void analyseDisjunktionPredicate(PPredicate node, HashSet<Node> list) {
+ if (node instanceof ADisjunctPredicate) {
+ ADisjunctPredicate dis = (ADisjunctPredicate) node;
+ analyseDisjunktionPredicate(dis.getLeft(), list);
+ analyseDisjunktionPredicate(dis.getRight(), list);
+ }else{
+ analysePredicate(node, list, new HashSet<Node>());
+ }
+ }
+
private void analysePredicate(Node n, HashSet<Node> list, HashSet<Node> ignoreList) {
if (n instanceof AEqualPredicate) {
PExpression left = ((AEqualPredicate) n).getLeft();
diff --git a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java b/src/main/java/de/b2tla/analysis/unchangedvariables/AssignedVariablesFinder.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
rename to src/main/java/de/b2tla/analysis/unchangedvariables/AssignedVariablesFinder.java
index 934a5c61f4362316d3a69281bdd1592cb842db01..a682f462fe8fb6b55c933ed4d223be16f64b1f56 100644
--- a/src/main/java/de/b2tla/analysis/AssignedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/unchangedvariables/AssignedVariablesFinder.java
@@ -1,10 +1,11 @@
-package de.b2tla.analysis;
+package de.b2tla.analysis.unchangedvariables;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
+import de.b2tla.analysis.MachineContext;
import de.b2tla.exceptions.SubstitutionException;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
diff --git a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java b/src/main/java/de/b2tla/analysis/unchangedvariables/UnchangedVariablesFinder.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
rename to src/main/java/de/b2tla/analysis/unchangedvariables/UnchangedVariablesFinder.java
index cdfd2753e0e9d077df6618ef76f5aae227705439..ff79eb09b1a38d9254f8e5db24959f52d93e2f17 100644
--- a/src/main/java/de/b2tla/analysis/UnchangedVariablesFinder.java
+++ b/src/main/java/de/b2tla/analysis/unchangedvariables/UnchangedVariablesFinder.java
@@ -1,10 +1,11 @@
-package de.b2tla.analysis;
+package de.b2tla.analysis.unchangedvariables;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
+import de.b2tla.analysis.MachineContext;
import de.b2tla.exceptions.SubstitutionException;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index d2505674eae1b2373860f056307f1f18e0927966..635be7f6ce1a4d856787ce376f511c99c4711bf5 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -8,16 +8,16 @@ import java.util.List;
import de.b2tla.B2TLAGlobals;
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.UsedStandardModules;
import de.b2tla.analysis.nodes.EqualsNode;
import de.b2tla.analysis.nodes.NodeType;
import de.b2tla.analysis.nodes.SubsetNode;
+import de.b2tla.analysis.typerestriction.TypeRestrictor;
+import de.b2tla.analysis.unchangedvariables.UnchangedVariablesFinder;
import de.b2tla.btypes.BType;
import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java
index 07361ae05a8c6db2f384b0376942dccabd982770..37776ba8358e841b8c9b712564124fffd00a4bbf 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/b2tla/tla/Generator.java
@@ -11,10 +11,10 @@ import de.b2tla.B2TLAGlobals;
import de.b2tla.analysis.ConstantsEvaluator;
import de.b2tla.analysis.DefinitionsAnalyser;
import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.TypeRestrictor;
import de.b2tla.analysis.Typechecker;
import de.b2tla.analysis.nodes.ElementOfNode;
import de.b2tla.analysis.nodes.NodeType;
+import de.b2tla.analysis.typerestriction.TypeRestrictor;
import de.b2tla.btypes.BType;
import de.b2tla.tla.config.ModelValueAssignment;
import de.b2tla.tla.config.SetOfModelValuesAssignment;
@@ -237,7 +237,7 @@ public class Generator extends DepthFirstAdapter {
while (cons.hasNext()) {
AIdentifierExpression con = (AIdentifierExpression) cons.next();
Node value = conValueTable.get(con);
- tlaModule.definitions.add(new TLADefinition(con, value));
+ //tlaModule.definitions.add(new TLADefinition(con, value));
AExpressionDefinitionDefinition exprDef = new AExpressionDefinitionDefinition(
con.getIdentifier().get(0), new LinkedList<PExpression>(),
@@ -250,7 +250,7 @@ public class Generator extends DepthFirstAdapter {
ArrayList<Node> remainingConstants = new ArrayList<Node>();
remainingConstants.addAll(machineContext.getConstants().values());
remainingConstants.removeAll(conValueTable.keySet());
-
+
Node propertiesPerdicate = machineContext.getPropertiesMachineClause()
.getPredicates();
if (remainingConstants.size() != 0) {
@@ -301,7 +301,7 @@ public class Generator extends DepthFirstAdapter {
}
} else {
- tlaModule.definitions.add(new TLADefinition(con, value));
+ //tlaModule.definitions.add(new TLADefinition(con, value));
}
}
diff --git a/src/main/java/de/b2tla/tlc/TLCExpressionParser.java b/src/main/java/de/b2tla/tlc/TLCExpressionParser.java
deleted file mode 100644
index 9e0cb9ca8999045faee92c8fb565ded5a81bdf8f..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/tlc/TLCExpressionParser.java
+++ /dev/null
@@ -1,231 +0,0 @@
-package de.b2tla.tlc;
-
-import java.util.Hashtable;
-import java.util.regex.Matcher;
-import java.util.regex.Pattern;
-
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.FunctionType;
-import de.b2tla.btypes.PairType;
-import de.b2tla.btypes.SetType;
-
-public class TLCExpressionParser {
-
- private StringBuilder sb;
- private String string;
- private Hashtable<String, BType> types;
-
- public static String parseLine(String line) {
- TLCExpressionParser parser = new TLCExpressionParser(line, null);
- parser.parse();
- return parser.sb.toString();
- }
-
- public static String parseLine(String line, Hashtable<String, BType> types) {
- TLCExpressionParser parser = new TLCExpressionParser(line, types);
- parser.parse();
- return parser.sb.toString();
- }
-
- public TLCExpressionParser(String stringToTranslate,
- Hashtable<String, BType> t) {
- this.string = stringToTranslate;
- this.sb = new StringBuilder();
- this.types = t;
- }
-
- public void parse() {
- string = string.replaceAll("\\s", "");
- parsePredicate();
- }
-
- private BType getType(String var) {
- if (types != null) {
- return types.get(var);
- } else {
- return null;
- }
- }
-
- private void parsePredicate() throws MatchException {
- try {
- match("/\\");
- } catch (MatchException e) {
- }
- String var = parseIdentifier();
- BType varType = getType(var);
- replace("=", " = ");
- parseExpr(varType);
-
- while (comes("/\\")) {
- replace("/\\", " & ");
- String var2 = parseIdentifier();
- BType varType2 = getType(var2);
- replace("=", " = ");
- parseExpr(varType2);
- }
- }
-
- private void parseExpr(BType type) throws MatchException {
- if (comes("<<")) {
- parseTuple(type);
- } else if (parseNumber()) {
- } else if (null != parseIdentifier()) {
- } else if (comes("(")) {
- parseFunction(type);
- } else if (comes("{")) {
- parseSet(type);
- } else {
- throw new RuntimeException("Error while parsing trace. Can not parse: " + string);
- }
- return;
- }
-
- private void parseSet(BType type) throws MatchException {
- BType subtype = null;
- if (type != null) {
- subtype = ((SetType) type).getSubtype();
- }
- replace("{", "{");
- if (comes("}")) {
- replace("}", "}");
- return;
- }
- parseExpr(subtype);
- while (comes(",")) {
- replace(",", ",");
- parseExpr(subtype);
- }
- replace("}", "}");
- }
-
- private void parseFunction(BType type) throws MatchException {
- BType domain = null;
- BType range = null;
- if (type != null) {
- FunctionType f = (FunctionType) type;
- domain = f.getDomain();
- range = f.getRange();
- }
-
- replace("(", "{");
- sb.append("(");
- parseExpr(domain);
- replace(":>", ",");
- parseExpr(range);
- sb.append(")");
-
- while (comes("@@")) {
- replace("@@", ",");
-
- sb.append("(");
- parseExpr(domain);
- replace(":>", ",");
- parseExpr(range);
- sb.append(")");
-
- }
- replace(")", "}");
- }
-
- private String parseIdentifier() throws MatchException {
- Pattern Number = Pattern.compile("\\w+");
- Matcher matcher = Number.matcher(string);
- if (matcher.lookingAt()) {
- String res = matcher.group();
- sb.append(res);
- string = string.substring(matcher.end());
- return res;
- } else {
- return null;
- }
- }
-
- private boolean parseNumber() throws MatchException {
- Pattern Number = Pattern.compile("-?(\\d)+");
- Matcher matcher = Number.matcher(string);
- if (matcher.lookingAt()) {
- String res = matcher.group();
- sb.append(res);
-
- // detects intervals e.g. 1..8 TODO
- String interval = string.substring(matcher.end());
- if (interval.startsWith("..")) {
- sb.append("..");
- matcher.find();
- sb.append(matcher.group());
- }
-
- string = string.substring(matcher.end());
- return true;
- } else {
- return false;
- }
- }
-
- private void parseTuple(BType type) throws MatchException {
- if (!comes("<<")) {
- throw new MatchException();
- }
- boolean isSequence = true;
- BType first = null;
- BType second = null;
- if (type != null) {
- if (type instanceof PairType) {
- isSequence = false;
- first = ((PairType) type).getFirst();
- second = ((PairType) type).getSecond();
- } else if (type instanceof SetType) {
- isSequence = false;
- SetType set = (SetType) type;
- PairType pair = (PairType) set.getSubtype();
- first = pair.getSecond();
- second = pair.getSecond();
- } else {
- FunctionType f = (FunctionType) type;
- first = f.getRange();
- second = f.getRange();
- }
- }
-
- replace("<<", isSequence ? "[" : "(");
- if (comes(">>")) {
- replace(">>", isSequence ? "]" : ")");
- return;
- }else{
- parseExpr(first);
- while (comes(",")) {
- replace(",", ",");
- parseExpr(second);
- }
- }
- replace(">>", isSequence ? "]" : ")");
- }
-
- private boolean comes(String stringToMatch) {
- if (string.startsWith(stringToMatch)) {
- return true;
- } else {
- return false;
- }
- }
-
- private void replace(String stringToMatch, String replaceBy)
- throws MatchException {
- match(stringToMatch);
- sb.append(replaceBy);
- }
-
- private void match(String stringToMatch) throws MatchException {
- if (string.startsWith(stringToMatch)) {
- string = string.substring(stringToMatch.length());
- } else {
- throw new MatchException();
- }
- }
-
- class MatchException extends RuntimeException {
- private static final long serialVersionUID = 1L;
- }
-
-}
diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java
deleted file mode 100644
index fbe19fab746fcd27f70f9f55a02fd8d5f0d90234..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/tlc/TLCOutput.java
+++ /dev/null
@@ -1,254 +0,0 @@
-package de.b2tla.tlc;
-
-import java.text.ParseException;
-import java.text.SimpleDateFormat;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.Date;
-import java.util.regex.Matcher;
-import java.util.regex.Pattern;
-
-import de.b2tla.B2TLAGlobals;
-
-public class TLCOutput {
- private final String moduleName;
- private String[] messages;
- private TLCOutputInfo tlcOutputInfo;
-
- Date startingTime;
- Date finishingTime;
- TLCResult result;
- ArrayList<String> states = new ArrayList<String>();
- StringBuilder trace;
- String parseError;
- int transitions = -1;
- int distinctStates = -1;
-
- public static enum TLCResult {
- Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalPropertyError, WellDefinednessError
- }
-
- public int getTransitions() {
- return transitions;
- }
-
- public int getDistinctStates() {
- return distinctStates;
- }
-
- public long getRunningTime() {
- long time = (finishingTime.getTime() - startingTime.getTime()) / 1000;
- return time;
- }
-
- public TLCResult getResult() {
- return result;
- }
-
- public String getResultString() {
- if (result == TLCResult.InvariantViolation) {
- return "Invariant Violation";
- } else if (result == TLCResult.TemporalPropertyError) {
- return "Temporal Property Violation";
- }
- return result.toString();
- }
-
- public StringBuilder getErrorTrace() {
- parseTrace();
- return trace;
- }
-
- public String getModuleName() {
- return moduleName;
- }
-
- public boolean hasTrace() {
- return states.size() > 0;
- }
-
- public TLCOutput(String moduleName, String[] messages,
- TLCOutputInfo tlcOutputInfo) {
- this.moduleName = moduleName;
- this.messages = messages;
- this.tlcOutputInfo = tlcOutputInfo;
- }
-
- public void parseTLCOutput() {
- for (int i = 0; i < messages.length; i++) {
- String m = messages[i];
- if (m.startsWith("Starting...")) {
- startingTime = parseTime(m);
- } else if (m.startsWith("Finished.")) {
- finishingTime = parseTime(m);
- } else if (m.startsWith("Error:")) {
- TLCResult e = findError(m);
- if (e != null) {
- this.result = e;
- }
- } else if (m.endsWith("states left on queue.")) {
- parseStates(m);
- } else if (m.startsWith("State")) {
- states.add(m);
- } else if (m.startsWith("*** Errors:")) {
- parseError = m;
- }
- }
- if (result == null) {
- ArrayList<String> list = new ArrayList<String>(Arrays.asList(messages));
- this.result = findError(list);
- }
-
- }
-
- private void parseStates(String m) {
- final Pattern pattern = Pattern.compile("\\d+");
- final Matcher matcher = pattern.matcher(m);
-
- final ArrayList<Integer> ints = new ArrayList<Integer>();
- while (matcher.find()) {
- ints.add(Integer.parseInt(matcher.group()));
- }
- transitions = ints.get(0);
- distinctStates = ints.get(1);
- }
-
- private void parseTrace() {
- // ModuleMatcher moduleMatcher = new ModuleMatcher(moduleName,
- // ToolIO.getUserDir());
-
- trace = new StringBuilder();
-
- if (tlcOutputInfo.hasConstants()) {
- String m1 = states.get(0);
- String[] a = m1.split("/\\\\");
- Pattern pattern = Pattern.compile("\\w+");
- String constantSetup = "";
- for (int i = 1; i < a.length; i++) {
- String line = a[i];
- Matcher matcher = pattern.matcher(line);
- matcher.find();
- String identifier = matcher.group();
- if (tlcOutputInfo.isAConstant(identifier)) {
- if (!constantSetup.equals("")) {
- constantSetup += " /\\ ";
- }
- constantSetup += line;
- }
- }
- //System.out.println(constantSetup);
- if (constantSetup.equals("")) {
- /**
- * There is only one possibility to setup the constants. As a
- * consequence ProB has to find the values for the constants so
- * that the predicate 1=1 is satisfied.
- */
- trace.append("1 = 1 \n");
- } else {
- constantSetup = TLCExpressionParser.parseLine(constantSetup,
- tlcOutputInfo.getTypes());
- trace.append(constantSetup);
- trace.append("\n");
- }
-
- }
-
- 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 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());
- trace.append(res);
- trace.append("\n");
- }
-
- }
-
- public static TLCResult findError(ArrayList<String> list) {
- for (int i = 0; i < list.size(); i++) {
- String m = list.get(i);
- if (m.startsWith("In applying the function")) {
- return TLCResult.WellDefinednessError;
- } else if (m.contains("tlc2.module.TLC.Assert")) {
- return TLCResult.WellDefinednessError;
- } else if (m.startsWith("Error:") || m.startsWith("\"Error:")
- || m.startsWith("The exception was a")) {
- System.out.println(m);
- TLCResult res = findError(m);
- if (res != null)
- return res;
- }
- }
- return TLCResult.NoError;
- }
-
- private static TLCResult findError(String m) {
- String[] res = m.split(" ");
- if (res[1].equals("Deadlock")) {
- return TLCResult.Deadlock;
- } else if (res[1].equals("Invariant")) {
- String invName = res[2];
- if (invName.startsWith("Invariant")) {
- return TLCResult.InvariantViolation;
- } else if (invName.equals("NotGoal")) {
- return TLCResult.Goal;
- } else if (invName.startsWith("Assertion")) {
- return TLCResult.AssertionError;
- }
- } else if (m.contains("The invariant of Assertion")) {
- return TLCResult.AssertionError;
- } else if (res[1].equals("Assumption")) {
- return TLCResult.PropertiesError;
- } else if (res[1].equals("Temporal")) {
- return TLCResult.TemporalPropertyError;
- } else if (m.equals("Error: TLC threw an unexpected exception.")) {
- return null;
- } else if (m.startsWith("Error: Attempted to apply function:")) {
- return TLCResult.WellDefinednessError;
- } else if (m.startsWith("\"Error: Invalid function call to relation")) {
- return TLCResult.WellDefinednessError;
- } else if (m.startsWith("Error: The behavior up to")) {
- return null;
- } else if (m.contains("In applying the function")) {
- return TLCResult.WellDefinednessError;
- } else if (m.startsWith("\"Error: Function assignment")) {
- return TLCResult.WellDefinednessError;
- } else if(m.startsWith("Error: Evaluating assumption")){
- return TLCResult.WellDefinednessError;
- }
- else if (m
- .startsWith("Error: The following behavior constitutes a counter-example:")) {
- return null;
- } else if (m
- .startsWith("Error: The error occurred when TLC was evaluating the nested")) {
- return null;
- } else if (m.startsWith("Error: Evaluating assumption")) {
- return null;
- } else if (m.contains("tlc2.tool.EvalException")) {
- return null;
- }
-
- return TLCResult.TLCError;
- }
-
- private static Date parseTime(String m) {
- String time = m.substring(m.indexOf("(") + 1, m.indexOf(")"));
- SimpleDateFormat sdf = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss");
- Date date;
- try {
- date = sdf.parse(time);
- } catch (ParseException e) {
- // Should never happen
- throw new RuntimeException(e);
- }
- return date;
- }
-}
diff --git a/src/main/java/de/b2tla/tlc/TLCResults.java b/src/main/java/de/b2tla/tlc/TLCResults.java
new file mode 100644
index 0000000000000000000000000000000000000000..bbc41176dd0c941c7b49e89db656c70397ff2cd8
--- /dev/null
+++ b/src/main/java/de/b2tla/tlc/TLCResults.java
@@ -0,0 +1,227 @@
+package de.b2tla.tlc;
+
+import java.util.ArrayList;
+import java.util.Date;
+
+import de.b2tla.B2TLAGlobals;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import tlc2.output.EC;
+import static tlc2.output.MP.*;
+import tlc2.output.Message;
+import tlc2.output.OutputCollector;
+import tlc2.tool.TLCStateInfo;
+
+public class TLCResults {
+
+ private TLCResult tlcResult;
+ private Date startTime;
+ private Date endTime;
+
+ private int lengthOfTrace;
+ private String traceString;
+
+ private int numberOfDistinctStates;
+ private int numberOfTransitions;
+
+ private TLCOutputInfo tlcOutputInfo;
+
+ public static enum TLCResult {
+ Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerationError, TLCError, TemporalPropertyError, WellDefinednessError;
+ }
+
+ public boolean hasTrace() {
+ return lengthOfTrace > 0;
+ }
+
+ public TLCResults(TLCOutputInfo tlcOutputInfo) {
+ this.tlcOutputInfo = tlcOutputInfo;
+ this.lengthOfTrace = 0;
+ }
+
+ public int getNumberOfDistinctStates() {
+ return numberOfDistinctStates;
+ }
+
+ public String getTrace() {
+ return traceString;
+ }
+
+ public int getNumberOfTransitions() {
+ return numberOfTransitions;
+ }
+
+ public int getModelCheckingTime() {
+ return (int) (endTime.getTime() - startTime.getTime()) / 1000;
+ }
+
+ public void evalResults() {
+
+ evalAllMessages();
+
+ if (hasTrace()
+ || (B2TLAGlobals.getTestingMode() && OutputCollector
+ .getInitialState() != null)) {
+ evalTrace();
+ }
+
+ }
+
+ private void evalTrace() {
+ ArrayList<TLCStateInfo> trace = OutputCollector.getTrace();
+ TracePrinter printer = null;
+ if (trace != null) {
+ printer = new TracePrinter(trace, tlcOutputInfo);
+ } else if (OutputCollector.getInitialState() != null) {
+ printer = new TracePrinter(OutputCollector.getInitialState(),
+ tlcOutputInfo);
+ }
+ traceString = printer.getTrace().toString();
+ }
+
+ private void evalAllMessages() {
+
+ ArrayList<Message> messages = OutputCollector.getAllMessages();
+ for (Message m : messages) {
+
+ switch (m.getMessageClass()) {
+ case ERROR:
+ evalErrorMessage(m);
+ break;
+ case TLCBUG:
+ break;
+ case STATE:
+ lengthOfTrace++;
+ break;
+ case WARNING:
+ break;
+ case NONE:
+ evalStatusMessage(m);
+ break;
+
+ }
+ }
+
+ if (this.tlcResult == null) {
+ // this.tlcResult = TLCError;
+ }
+
+ }
+
+ private void evalStatusMessage(Message m) {
+
+ switch (m.getMessageCode()) {
+
+ case EC.TLC_STARTING:
+ startTime = m.getDate();
+ break;
+ case EC.TLC_FINISHED:
+ endTime = m.getDate();
+ break;
+
+ case EC.TLC_STATS:
+ numberOfTransitions = Integer.parseInt(m.getParameters()[0]);
+ numberOfDistinctStates = Integer.parseInt(m.getParameters()[1]);
+ break;
+
+ case EC.TLC_STATS_DFID:
+
+ break;
+
+ case EC.TLC_SUCCESS:
+ tlcResult = TLCResult.NoError;
+ break;
+ }
+
+ }
+
+ private void evalErrorMessage(Message m) {
+ switch (m.getMessageCode()) {
+ case EC.TLC_INVARIANT_VIOLATED_INITIAL:
+ case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR:
+ if (m.getParameters()[0].startsWith("Assertion")) {
+ tlcResult = AssertionError;
+ } else if (m.getParameters()[0].equals("NotGoal")) {
+ tlcResult = Goal;
+ } else {
+ tlcResult = TLCResult.InvariantViolation;
+ }
+ break;
+
+ case EC.TLC_INITIAL_STATE: {
+ String arg1 = m.getParameters()[0];
+ if (arg1.contains("Attempted to compute the number of elements in the overridden")) {
+
+ }
+ tlcResult = EnumerationError;
+ return;
+ }
+
+ case EC.TLC_DEADLOCK_REACHED:
+ tlcResult = TLCResult.Deadlock;
+ break;
+
+ case EC.TLC_ASSUMPTION_FALSE:
+ tlcResult = TLCResult.PropertiesError;
+ break;
+
+ case EC.TLC_TEMPORAL_PROPERTY_VIOLATED:
+ tlcResult = TLCResult.TemporalPropertyError;
+ break;
+
+ case EC.TLC_ASSUMPTION_EVALUATION_ERROR:
+ tlcResult = evaluatingParameter(m.getParameters());
+ break;
+
+ case EC.TLC_VALUE_ASSERT_FAILED:
+ tlcResult = WellDefinednessError;
+ break;
+
+ case EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE:
+ if (m.getParameters()[0].contains("tlc2.module.TLC.Assert")) {
+ tlcResult = WellDefinednessError;
+ }
+ break;
+
+ case EC.GENERAL:
+ tlcResult = evaluatingParameter(m.getParameters());
+ break;
+
+ }
+ }
+
+ private TLCResult evaluatingParameter(String[] params) {
+ for (int i = 0; i < params.length; i++) {
+ String s = params[i];
+ if (s.contains("not enumerable")) {
+ return EnumerationError;
+ } else if (s.contains("The invariant of Assertion")) {
+ return AssertionError;
+ } else if (s.contains("The invariant of Invariant")) {
+ return InvariantViolation;
+ } else if (s.contains("In applying the function")) {
+ return WellDefinednessError;
+ } else if (s.contains("tlc2.module.TLC.Assert")) {
+ return tlcResult = WellDefinednessError;
+ }
+
+ }
+ // unkown error
+ return null;
+ }
+
+ public TLCResult getTLCResult() {
+ return tlcResult;
+ }
+
+ public String getResultString() {
+ if (tlcResult == TLCResult.InvariantViolation) {
+ return "Invariant Violation";
+ } else if (tlcResult == TLCResult.TemporalPropertyError) {
+ return "Temporal Property Violation";
+ }
+ if (tlcResult == null) {
+ return TLCError.toString();
+ }
+ return tlcResult.toString();
+ }
+}
diff --git a/src/main/java/de/b2tla/tlc/TracePrinter.java b/src/main/java/de/b2tla/tlc/TracePrinter.java
new file mode 100644
index 0000000000000000000000000000000000000000..72b371c9dadb3c9d62206b904d88835d68335a7e
--- /dev/null
+++ b/src/main/java/de/b2tla/tlc/TracePrinter.java
@@ -0,0 +1,314 @@
+package de.b2tla.tlc;
+
+import java.util.ArrayList;
+
+import de.b2tla.btypes.BType;
+import de.b2tla.btypes.FunctionType;
+import de.b2tla.btypes.PairType;
+import de.b2tla.btypes.SetType;
+import de.b2tla.btypes.StructType;
+import tlc2.tool.TLCState;
+import tlc2.tool.TLCStateInfo;
+import tlc2.value.FcnLambdaValue;
+import tlc2.value.FcnRcdValue;
+import tlc2.value.IntervalValue;
+import tlc2.value.LazyValue;
+import tlc2.value.ModelValue;
+import tlc2.value.RecordValue;
+import tlc2.value.SetCapValue;
+import tlc2.value.SetCupValue;
+import tlc2.value.SetDiffValue;
+import tlc2.value.SetEnumValue;
+import tlc2.value.SetOfFcnsValue;
+import tlc2.value.SetOfRcdsValue;
+import tlc2.value.SetOfTuplesValue;
+import tlc2.value.SetPredValue;
+import tlc2.value.StringValue;
+import tlc2.value.SubsetValue;
+import tlc2.value.TupleValue;
+import tlc2.value.UnionValue;
+import tlc2.value.Value;
+import tlc2.value.ValueVec;
+import util.UniqueString;
+import static tlc2.value.ValueConstants.*;
+
+public class TracePrinter {
+
+ ArrayList<TLCStateInfo> trace;
+ TLCState initialState;
+ TLCOutputInfo tlcOutputInfo;
+
+ StringBuilder traceBuilder;
+
+ public TracePrinter(ArrayList<TLCStateInfo> trace,
+ TLCOutputInfo tlcOutputInfo) {
+ this.trace = trace;
+ this.tlcOutputInfo = tlcOutputInfo;
+
+ evalTrace();
+ }
+
+
+ public TracePrinter(TLCState initialState, TLCOutputInfo tlcOutputInfo) {
+ this.initialState = initialState;
+ this.tlcOutputInfo = tlcOutputInfo;
+
+ evalTrace();
+ }
+
+ public StringBuilder getTrace(){
+ return traceBuilder;
+ }
+
+
+ private void evalTrace() {
+ traceBuilder = new StringBuilder();
+
+ if(trace != null){
+ for (int i = 0; i < trace.size(); i++) {
+ if (i > 0) {
+ traceBuilder.append("\n");
+ }
+ traceBuilder.append(evalExpression(trace.get(i).state));
+ }
+ }else {
+ traceBuilder.append(evalExpression(initialState));
+ }
+
+ System.out.println(traceBuilder);
+ }
+
+ private StringBuilder evalExpression(TLCState state) {
+ StringBuilder expression = new StringBuilder();
+
+ for (int i = 0; i < TLCState.vars.length; i++) {
+ if (i > 0) {
+ expression.append(" & ");
+ }
+ UniqueString var = TLCState.vars[i].getName();
+ BType type = tlcOutputInfo.getBType(var.toString());
+ String value = parseValue(state.lookup(var), type).toString();
+ expression.append(var).append(" = ").append(value);
+ }
+ return expression;
+ }
+
+ private StringBuilder parseValue(Value val, BType type) {
+ //System.out.println(val.getClass());
+ StringBuilder res = new StringBuilder();
+ int valueType = val.getKind();
+ switch (valueType) {
+ case INTVALUE:
+ case BOOLVALUE:
+ return res.append(val);
+
+ case INTERVALVALUE: {
+ IntervalValue i = (IntervalValue) val;
+ res.append("(");
+ res.append(i.low).append("..").append(i.high);
+ res.append(")");
+ return res;
+ }
+
+ case SETENUMVALUE:
+ SetType set = (SetType) type;
+ res.append("{");
+ res.append(parseValueVec(((SetEnumValue) val).elems,
+ set.getSubtype()));
+ res.append("}");
+ return res;
+
+ case TUPLEVALUE:
+ if (type instanceof PairType) {
+ BType first = ((PairType) type).getFirst();
+ BType second = ((PairType) type).getSecond();
+ res.append("(");
+ res.append(parseValue(((TupleValue) val).elems[0], first));
+ res.append(", ");
+ res.append(parseValue(((TupleValue) val).elems[1], second));
+ res.append(")");
+ return res;
+ } else if (type instanceof FunctionType) {
+ BType subtype = ((FunctionType) type).getRange();
+ res.append("[");
+ res.append(parseEnumerationValue(((TupleValue) val).elems,
+ subtype));
+ res.append("]");
+ return res;
+ }
+ return null;
+
+ case RECORDVALUE:{
+ RecordValue rec = (RecordValue) val;
+ StructType struct = (StructType) type;
+ res.append("rec(");
+ for (int i = 0; i < rec.names.length; i++) {
+ if (i > 0) {
+ res.append(", ");
+ }
+ String name = rec.names[i].toString();
+ BType t = struct.getType(name);
+ res.append(name).append(" : ");
+ res.append(parseValue(rec.values[i], t));
+ }
+ res.append(")");
+ return res;
+ }
+
+
+ case FCNRCDVALUE:
+ FcnRcdValue function = (FcnRcdValue) val;
+ FunctionType funcType = (FunctionType) type;
+ res.append("{");
+ for (int i = 0; i < function.domain.length; i++) {
+ if (i > 0) {
+ res.append(", ");
+ }
+ res.append("(");
+ res.append(parseValue(function.domain[i], funcType.getDomain()));
+ res.append(", ");
+ res.append(parseValue(function.values[i], funcType.getRange()));
+ res.append(")");
+ }
+ res.append("}");
+ return res;
+
+ case MODELVALUE:
+ ModelValue modelValue = (ModelValue) val;
+ // TODO B name of model value
+ String name = tlcOutputInfo.getBName(modelValue.toString());
+ res.append(modelValue.toString());
+ return res;
+
+ case SETOFTUPLESVALUE: {
+ SetOfTuplesValue s = (SetOfTuplesValue) val;
+ SetType t = (SetType) type;
+ PairType pair = (PairType) t.getSubtype();
+ res.append(parseValue(s.sets[0], new SetType(pair.getFirst())));
+ res.append("*");
+ res.append(parseValue(s.sets[1], new SetType(pair.getSecond())));
+ return res;
+ }
+
+ case SETCUPVALUE: {
+ SetCupValue s = (SetCupValue) val;
+ res.append(parseValue(s.set1, type));
+ res.append("\\/");
+ res.append(parseValue(s.set2, type));
+ return res;
+ }
+ case SETCAPVALUE: {
+ SetCapValue s = (SetCapValue) val;
+ res.append(parseValue(s.set1, type));
+ res.append("/\\");
+ res.append(parseValue(s.set2, type));
+ return res;
+ }
+
+ case SETDIFFVALUE: {
+ SetDiffValue s = (SetDiffValue) val;
+ res.append(parseValue(s.set1, type));
+ res.append("-");
+ res.append(parseValue(s.set2, type));
+ return res;
+ }
+
+ case SUBSETVALUE:{
+ SubsetValue s = (SubsetValue) val;
+ SetType t = (SetType) type;
+ res.append("POW(").append(parseValue(s.set, t.getSubtype())).append(")");
+ return res;
+ }
+ case UNIONVALUE:{
+ UnionValue s = (UnionValue) val;
+ SetType t = (SetType) type;
+ res.append("union(");
+ res.append(parseValue(s.set, new SetType(t)));
+ res.append(")");
+ return res;
+ }
+
+ case SETOFRCDSVALUE:{
+ SetOfRcdsValue s = (SetOfRcdsValue) val;
+ SetType t = (SetType) type;
+ StructType struct = (StructType) t.getSubtype();
+ res.append("struct(");
+ for (int i = 0; i < s.names.length; i++) {
+ if(i>0){
+ res.append(", ");
+ }
+ res.append(s.names[i]);
+ res.append(":");
+ BType fieldType = struct.getType(s.names[i].toString());
+ res.append(parseValue(s.values[i], new SetType(fieldType)));
+ }
+ res.append(")");
+ return res;
+ }
+
+ case SETOFFCNSVALUE:{
+ SetOfFcnsValue s = (SetOfFcnsValue) val;
+ SetType t = (SetType) type;
+ FunctionType func = (FunctionType) t.getSubtype();
+ res.append("(");
+ res.append(parseValue(s.domain, new SetType(func.getDomain())));
+ res.append(" --> ");
+ res.append(parseValue(s.range, new SetType(func.getRange())));
+ res.append(")");
+ return res;
+ }
+
+ case STRINGVALUE:{
+ StringValue s = (StringValue) val;
+ res.append("\"").append(s.getVal()).append("\"");
+ return res;
+ }
+
+ case FCNLAMBDAVALUE:{
+ FcnLambdaValue s = (FcnLambdaValue) val;
+ res.append(parseValue(s.fcnRcd, type));
+ return res;
+ }
+ case SETPREDVALUE:{
+ SetPredValue s = (SetPredValue) val;
+ res.append(parseValue(s.inVal, type));
+ return res;
+ }
+
+ case LAZYVALUE:{
+ LazyValue s = (LazyValue) val;
+ res.append(parseValue(s.val, type));
+ return res;
+ }
+
+
+ }
+ System.err.println("Type: " + val.getKind());
+ throw new RuntimeException("not supported construct: " + val);
+ }
+
+ private StringBuilder parseValueVec(ValueVec elems, BType bType) {
+ StringBuilder res = new StringBuilder();
+ for (int i = 0; i < elems.size(); i++) {
+ if (i > 0) {
+ res.append(", ");
+ }
+ Value val = elems.elementAt(i);
+ res.append(parseValue(val, bType));
+ }
+ return res;
+ }
+
+ private StringBuilder parseEnumerationValue(Value[] a, BType bType) {
+
+ StringBuilder res = new StringBuilder();
+ for (int i = 0; i < a.length; i++) {
+ if (i > 0) {
+ res.append(",");
+ }
+ res.append(parseValue(a[i], bType));
+ }
+ return res;
+ }
+
+}
diff --git a/src/test/java/de/b2tla/tlc/ParserTest.java b/src/test/java/de/b2tla/tlc/ParserTest.java
deleted file mode 100644
index 99de3c4f37cd32fd848af6240483245dbaa1b8ff..0000000000000000000000000000000000000000
--- a/src/test/java/de/b2tla/tlc/ParserTest.java
+++ /dev/null
@@ -1,96 +0,0 @@
-package de.b2tla.tlc;
-
-import static de.b2tla.util.TestUtil.*;
-
-import java.util.Hashtable;
-
-import org.junit.Test;
-
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.BoolType;
-import de.b2tla.btypes.IntegerType;
-import de.b2tla.btypes.PairType;
-
-public class ParserTest {
-
- @Test
- public void testTupleOneElement() throws Exception {
- String tla = " x = <<1>>";
- String b = "x = [1]";
- compareExpr(b, tla);
- }
-
- @Test
- public void testEmptyTuple() throws Exception {
- String tla = " x = <<>>";
- String b = "x = []";
- compareExpr(b, tla);
- }
-
- @Test
- public void testTupleTwoElements() throws Exception {
- String tla = " x = <<1,1>>";
- String b = "x = [1,1]";
- compareExpr(b, tla);
- }
-
- @Test
- public void testModelvalue() throws Exception {
- String tla = " x = model";
- String b = "x = model";
- compareExpr(b, tla);
- }
-
- @Test
- public void testModelvalue2() throws Exception {
- String tla = " x = {a,b}";
- String b = "x = {a,b}";
- compareExpr(b, tla);
- }
-
- @Test
- public void testFunction() throws Exception {
- String tla = "x = (3 :> TRUE @@ 4 :> TRUE)";
- String b = "x = { (3,TRUE), (4,TRUE)}";
- compareExpr(b, tla);
- }
-
- @Test
- public void testSetOneElement() throws Exception {
- String tla = "x = {3}";
- String b = "x = {3}";
- compareExpr(b, tla);
- }
-
- @Test
- public void testEmptySet() throws Exception {
- String tla = "x = {}";
- String b = "x = {}";
- compareExpr(b, tla);
- }
-
- @Test
- public void testSetOfTuple() throws Exception {
- String tla = "x = {<<1,2,3>>}";
- String b = "x = {[1,2,3]}";
- compareExpr(b, tla);
- }
-
- @Test
- public void testPairVsSequence() throws Exception {
- String tla = "x = <<1,TRUE>>";
- String b = "x = (1,TRUE)";
- Hashtable<String, BType> types = new Hashtable<String, BType>();
- types.put("x",
- new PairType(IntegerType.getInstance(), BoolType.getInstance()));
- compareExpr(b, tla, types);
- }
-
- @Test
- public void testPedicates() throws Exception {
- String tla = "x = {<<1,2,3>>}\n /\\ y = <<1>>";
- String b = "x = {[1,2,3]} & y = [1]";
- compareExpr(b, tla);
- }
-
-}
diff --git a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
index d1849faa00f9d8a9739a6cfd9c7dbd8d9b48b669..5241909ee89aec52839b86b8adeb7046c6e934af 100644
--- a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
@@ -1,6 +1,6 @@
package de.b2tla.tlc.integration;
-import static de.b2tla.tlc.TLCOutput.TLCResult.NoError;
+import static de.b2tla.tlc.TLCResults.TLCResult.NoError;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,13 +9,13 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
+import static de.b2tla.util.TestUtil.test;
@RunWith(PolySuite.class)
public class BasicsTest extends AbstractParseMachineTest {
@@ -31,13 +31,13 @@ public class BasicsTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, true));
+ assertEquals(error, test(a));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
- list.add(new TestPair(NoError, "./src/test/resources/basics"));
+ //list.add(new TestPair(NoError, "./src/test/resources/basics"));
list.add(new TestPair(NoError, "./src/test/resources/laws"));
return getConfiguration(list);
}
diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
index f086bdc2e88cf1f62ad9f6d8129d48385c7fc7e6..dd269d536efac42c3dedb456dabbf113af5a6776 100644
--- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
@@ -1,93 +1,92 @@
package de.b2tla.tlc.integration;
-import static de.b2tla.tlc.TLCOutput.TLCResult.*;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
import static org.junit.Assert.*;
import org.junit.Ignore;
import org.junit.Test;
-import de.b2tla.B2TLA;
+import static de.b2tla.util.TestUtil.test;
public class ErrorTest {
+ @Test
+ public void testTraceValues() throws Exception {
+ String[] a = new String[] { "./src/test/resources/errors/TraceValues.mch" };
+ assertEquals(Deadlock, test(a));
+ }
+
@Test
public void testInvariantError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch" };
- assertEquals(InvariantViolation, B2TLA.test(a,true));
+ assertEquals(InvariantViolation, test(a));
}
@Test
public void testDeadlock() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/Deadlock.mch" };
- assertEquals(Deadlock, B2TLA.test(a,true));
+ assertEquals(Deadlock, test(a));
}
@Test
public void testPropertiesError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/PropertiesError.mch" };
- assertEquals(PropertiesError, B2TLA.test(a,true));
+ assertEquals(PropertiesError, test(a));
}
@Test
public void testNoFile() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/NoFile.mch" };
- assertEquals(null, B2TLA.test(a,true));
+ assertEquals(null, test(a));
}
@Test
public void testNoError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/NoError.mch" };
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
+ @Ignore
@Test
public void testEnumerationError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/EnumerationError.mch" };
- assertEquals(TLCError, B2TLA.test(a,true));
+ assertEquals(EnumerationError, test(a));
}
@Test
public void testAssertionError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/AssertionError.mch" };
- assertEquals(AssertionError, B2TLA.test(a,true));
+ assertEquals(AssertionError, test(a));
}
@Test
public void testConstantAssertionError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/AssertionError2.mch" };
- assertEquals(AssertionError, B2TLA.test(a,true));
+ assertEquals(AssertionError, test(a));
}
@Test
public void testTemporalPropertyError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/LTLError.mch" };
- assertEquals(TemporalPropertyError, B2TLA.test(a,true));
+ assertEquals(TemporalPropertyError, test(a));
}
@Test
public void testWelldefinednessError1() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/WelldefinednessError1.mch" };
- assertEquals(WellDefinednessError, B2TLA.test(a,true));
+ assertEquals(WellDefinednessError, test(a));
}
@Test
public void testWelldefinednessError2() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/WelldefinednessError2.mch" };
- assertEquals(WellDefinednessError, B2TLA.test(a,true));
+ assertEquals(WellDefinednessError, test(a));
}
@Test
public void testWelldefinednessError3() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/WelldefinednessError3.mch" };
- assertEquals(WellDefinednessError, B2TLA.test(a,true));
+ assertEquals(WellDefinednessError, test(a));
}
-
- @Ignore
- @Test
- public void testWellDefinednessErrorFunctionAssignment() throws Exception {
- String[] a = new String[] { "./src/test/resources/errors/WellDefinednessErrorFunctionAssignment.mch" };
- assertEquals(WellDefinednessError, B2TLA.test(a,true));
- }
-
}
diff --git a/src/test/java/de/b2tla/tlc/integration/LTLTest.java b/src/test/java/de/b2tla/tlc/integration/LTLTest.java
index df33f404d4d1d0f30a90bc8a0be253777c7f852b..26b17e191231c6cbeb15c57702ccea9871088297 100644
--- a/src/test/java/de/b2tla/tlc/integration/LTLTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/LTLTest.java
@@ -1,13 +1,12 @@
package de.b2tla.tlc.integration;
import static org.junit.Assert.assertEquals;
-
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
import org.junit.BeforeClass;
import org.junit.Test;
-import de.b2tla.B2TLA;
import de.b2tla.B2TLAGlobals;
-import de.b2tla.tlc.TLCOutput;
+import static de.b2tla.util.TestUtil.test;
public class LTLTest {
@@ -15,40 +14,35 @@ public class LTLTest {
public static void onlyOnce() {
B2TLAGlobals.setDeleteOnExit(true);
}
-
+
@Test
public void testCounterLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\CounterLTL.mch"};
- //B2TLA.main(a);
- assertEquals(TLCOutput.TLCResult.NoError, B2TLA.test(a,true));
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\CounterLTL.mch" };
+ assertEquals(NoError, test(a));
}
-
+
@Test
public void testFairnessCounterLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\FairnessCounter.mch"};
- //B2TLA.main(a);
- assertEquals(TLCOutput.TLCResult.TemporalPropertyError, B2TLA.test(a,true));
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\FairnessCounter.mch" };
+ assertEquals(TemporalPropertyError, test(a));
}
-
+
@Test
public void testUniversalQuantificaitonLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\UniveralQuatification.mch"};
- //B2TLA.main(a);
- assertEquals(TLCOutput.TLCResult.TemporalPropertyError, B2TLA.test(a,true));
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\UniveralQuatification.mch" };
+ assertEquals(TemporalPropertyError, test(a));
}
-
+
@Test
public void testExistentialQuantificationLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\ExistentialQuantification.mch"};
- //B2TLA.main(a);
- assertEquals(TLCOutput.TLCResult.NoError, B2TLA.test(a,true));
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\ExistentialQuantification.mch" };
+ assertEquals(NoError, test(a));
}
-
+
@Test
public void testFairnessParameter() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\Fairness_Parameter.mch"};
- //B2TLA.main(a);
- assertEquals(TLCOutput.TLCResult.NoError, B2TLA.test(a,true));
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\Fairness_Parameter.mch" };
+ assertEquals(NoError, test(a));
}
-
+
}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
index 385bccea541ea643de9ca7953cccaa36f4d81990..dd23fccf05495d377b846f3d1129b41bd23a3939 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
@@ -1,6 +1,7 @@
package de.b2tla.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCOutput.TLCResult.AssertionError;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.b2tla.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,8 +10,7 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
@@ -31,7 +31,7 @@ public class AssertionErrorTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, true));
+ assertEquals(error, test(a));
}
@Config
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
index 590d82a863c7df77b9746c8d77141044acf02d82..bb004fec57d0818cb4d1ffebb1b0fef45d0a8c0d 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
@@ -1,6 +1,7 @@
package de.b2tla.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCOutput.TLCResult.Deadlock;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.b2tla.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,8 +10,7 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
@@ -31,7 +31,7 @@ public class DeadlockTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, true));
+ assertEquals(error, test(a));
}
@Config
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
index 336eff120e364d3bde8d9893148f94b8362ecc31..1f7298d3908008dcc33773d74ce7dfce064891e6 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
@@ -1,6 +1,8 @@
package de.b2tla.tlc.integration.probprivate;
import static org.junit.Assert.assertEquals;
+import static de.b2tla.util.TestUtil.test;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
import java.io.File;
import java.util.ArrayList;
@@ -8,8 +10,7 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
@@ -30,13 +31,13 @@ public class GoalTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, true));
+ assertEquals(error, test(a));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
- list.add(new TestPair(TLCResult.Goal,
+ list.add(new TestPair(Goal,
"../prob_examples/public_examples/TLC/GOAL"));
return getConfiguration(list);
}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
index 9f611e7568f63d54ebf3c121558398062a8870e9..f620c285edbb28784fb2a058ea4e3118a31cb2c1 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
@@ -1,6 +1,7 @@
package de.b2tla.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCOutput.TLCResult.InvariantViolation;
+import static de.b2tla.util.TestUtil.test;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,8 +10,7 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
@@ -31,7 +31,7 @@ public class InvariantViolationTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, true));
+ assertEquals(error, test(a));
}
@Config
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
index 915594423800fcd7414dfe5dd6b8dcd99d320c85..5a4668b15b88817f666b038bc609133239501703 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
@@ -1,6 +1,7 @@
package de.b2tla.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCOutput.TLCResult.*;
+import static de.b2tla.util.TestUtil.test;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
import static org.junit.Assert.assertEquals;
@@ -15,69 +16,69 @@ public class LawsTest {
public void BoolLaws() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws.mch"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void BoolWithArithLaws() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void FunLaws() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/FunLaws.mch"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void FunLawsWithLambda() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/FunLawsWithLambda.mch"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void RelLaws_TLC() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/RelLaws_TLC.mch"};
- assertEquals(Goal, B2TLA.test(a,true));
+ assertEquals(Goal, test(a));
}
@Test
public void BoolLaws_SetCompr() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws_SetCompr.mch"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void BoolLaws_SetComprCLPFD() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void CardinalityLaws_TLC() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void EqualityLaws() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
@Test
public void SubsetLaws() throws Exception {
B2TLAGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
- assertEquals(NoError, B2TLA.test(a,true));
+ assertEquals(NoError, test(a));
}
}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
index bdee2c30650c2fb58220f158b43bcd4762318e48..1c2691506c4542be20f375924e2f59e6b8a67dd0 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
@@ -1,6 +1,7 @@
package de.b2tla.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCOutput.TLCResult.NoError;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.b2tla.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,8 +10,7 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
@@ -31,7 +31,7 @@ public class NoErrorTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, true));
+ assertEquals(error, test(a));
}
@Config
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
index 96dfbcdec88c740e15e43dd04c9f8236b4dbfec5..731e518b5e2b21a31a515e804256645eb783dfeb 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
@@ -1,6 +1,7 @@
package de.b2tla.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCOutput.TLCResult.WellDefinednessError;
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.b2tla.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,8 +10,7 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
@@ -20,8 +20,6 @@ import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class WellDefinednessTest extends AbstractParseMachineTest {
-
-
private final File machine;
private final TLCResult error;
@@ -33,7 +31,7 @@ public class WellDefinednessTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a,true));
+ assertEquals(error, test(a));
}
@Config
diff --git a/src/test/java/de/b2tla/util/AbstractParseMachineTest.java b/src/test/java/de/b2tla/util/AbstractParseMachineTest.java
index ee01335755846e2ad4254091f779dd752c20cce8..692cb73d97d14ac1681ae83d41c6b872006c9f03 100644
--- a/src/test/java/de/b2tla/util/AbstractParseMachineTest.java
+++ b/src/test/java/de/b2tla/util/AbstractParseMachineTest.java
@@ -5,7 +5,7 @@ import java.io.FilenameFilter;
import java.util.ArrayList;
import java.util.Arrays;
-import de.b2tla.tlc.TLCOutput;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.b2tla.util.PolySuite.Configuration;
public abstract class AbstractParseMachineTest {
@@ -31,7 +31,7 @@ public abstract class AbstractParseMachineTest {
protected static Configuration getConfiguration(ArrayList<TestPair> list) {
final ArrayList<File> allMachines = new ArrayList<File>();
- final ArrayList<TLCOutput.TLCResult> expectedValues = new ArrayList<TLCOutput.TLCResult>();
+ final ArrayList<TLCResult> expectedValues = new ArrayList<TLCResult>();
for (TestPair testPair : list) {
File[] machines = getMachines(testPair.getPath());
allMachines.addAll(Arrays.asList(machines));
@@ -53,7 +53,7 @@ public abstract class AbstractParseMachineTest {
return allMachines.get(index).getName();
}
- public TLCOutput.TLCResult getExpectedValue(int index) {
+ public TLCResult getExpectedValue(int index) {
return expectedValues.get(index);
}
};
diff --git a/src/test/java/de/b2tla/util/TLC4BTester.java b/src/test/java/de/b2tla/util/TLC4BTester.java
new file mode 100644
index 0000000000000000000000000000000000000000..e8482200e2137bc9661cc00cb6167a3b18028ba0
--- /dev/null
+++ b/src/test/java/de/b2tla/util/TLC4BTester.java
@@ -0,0 +1,14 @@
+package de.b2tla.util;
+
+import java.io.IOException;
+
+import de.b2tla.B2TLA;
+
+public class TLC4BTester {
+
+ public static void main(String[] args) throws IOException {
+ System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
+ B2TLA.test(args,true);
+ }
+
+}
diff --git a/src/test/java/de/b2tla/util/TestPair.java b/src/test/java/de/b2tla/util/TestPair.java
index d454e5d925f9c7ad204603a33bc5e78e8b45542b..47aebd6acdea4d8a13f92847d65220831de584c9 100644
--- a/src/test/java/de/b2tla/util/TestPair.java
+++ b/src/test/java/de/b2tla/util/TestPair.java
@@ -1,17 +1,18 @@
package de.b2tla.util;
-import de.b2tla.tlc.TLCOutput;
+import de.b2tla.tlc.TLCResults.TLCResult;
+
public class TestPair {
- private final TLCOutput.TLCResult error;
+ private final TLCResult error;
private final String path;
- public TestPair(TLCOutput.TLCResult error, String path) {
+ public TestPair(TLCResult error, String path) {
this.error = error;
this.path = path;
}
- public TLCOutput.TLCResult getResult() {
+ public TLCResult getResult() {
return error;
}
diff --git a/src/test/java/de/b2tla/util/TestUtil.java b/src/test/java/de/b2tla/util/TestUtil.java
index 6d67b2107114040aba5c94fb68f6c7f317ed4ce0..34a85ddae96c2790510a3b9afa0956659c231087 100644
--- a/src/test/java/de/b2tla/util/TestUtil.java
+++ b/src/test/java/de/b2tla/util/TestUtil.java
@@ -3,21 +3,30 @@ package de.b2tla.util;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.fail;
+import java.io.BufferedReader;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
+import java.io.InputStream;
+import java.io.InputStreamReader;
+import java.util.ArrayList;
+import java.util.Arrays;
import java.util.Hashtable;
-import util.ToolIO;
+
+
+
+import java.util.List;
import de.b2tla.B2TLA;
+import de.b2tla.B2TLAGlobals;
import de.b2tla.B2TlaTranslator;
+import de.b2tla.TLCRunner;
import de.b2tla.analysis.Ast2String;
import de.b2tla.btypes.BType;
-import de.b2tla.tlc.TLCExpressionParser;
+import de.b2tla.tlc.TLCResults.TLCResult;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
-import de.tla2b.translation.TLA2B;
public class TestUtil {
@@ -127,30 +136,6 @@ public class TestUtil {
return translator.getModuleString();
}
- public static void compare2(String expected, String machine)
- throws Exception {
- B2TlaTranslator b2tlaTranslator = new B2TlaTranslator(machine);
- b2tlaTranslator.translate();
- String name = b2tlaTranslator.getMachineName();
- String module = b2tlaTranslator.getModuleString();
-
- String dir = "build/testfiles/";
- createTempfile(dir, name + ".tla", module);
-
- B2TLA.createUsedStandardModules(dir,
- b2tlaTranslator.getUsedStandardModule());
- ToolIO.setMode(ToolIO.TOOL);
- String sb1 = TLA2B.translateFile(dir + name);
- // result
- createTempfile(dir, name + ".tla", expected);
- String sb2 = TLA2B.translateFile(dir + name);
-
- if (!sb2.toString().equals(sb1)) {
- // assertEquals(expected, actual);
- fail("expected:\n" + expected + "\nbut was:\n" + module);
- }
- }
-
public static void createTempfile(String dir, String fileName,
String moduleString) {
File d = new File(dir);
@@ -173,22 +158,89 @@ public class TestUtil {
e.printStackTrace();
}
}
+
+
+ public static TLCResult test(String[] args) throws IOException {
+ System.out.println("Starting JVM...");
+ final Process p = startJVM("", TLC4BTester.class.getCanonicalName(), args);
+ StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
+ stdOut.start();
+ StreamGobbler errOut = new StreamGobbler(p.getErrorStream());
+ errOut.start();
+ try {
+ p.waitFor();
+ } catch (InterruptedException e) {
+ e.printStackTrace();
+ }
+
+
+ for (int i = stdOut.getLog().size()-1; i > 1 ; i--) {
+ String s = stdOut.getLog().get(i);
+ if(s.startsWith("Result:")){
+ String resultString = s.substring(s.indexOf(':') + 2);
+ System.out.println(resultString);
+ return TLCResult.valueOf(resultString);
+ }
+ }
+ return null;
+ }
+
+
+
+
+
+ private static Process startJVM(final String optionsAsString,
+ final String mainClass, final String[] arguments)
+ throws IOException {
+
+ String separator = System.getProperty("file.separator");
+
+ String jvm = System.getProperty("java.home") + separator + "bin"
+ + separator + "java";
+ String classpath = System.getProperty("java.class.path");
+
+ List<String> command = new ArrayList<String>();
+ command.add(jvm);
+ command.add("-cp");
+ command.add(classpath);
+ command.add(mainClass);
+ command.addAll(Arrays.asList(arguments));
+
+ ProcessBuilder processBuilder = new ProcessBuilder(command);
+ Process process = processBuilder.start();
+ return process;
+ }
+
+}
- public static void compareExpr(String expected, String tla) {
- String res = TLCExpressionParser.parseLine(tla);
- System.out.println(res);
- res = res.replaceAll("\\s", "");
- expected = expected.replaceAll("\\s", "");
- assertEquals(expected, res);
+
+
+class StreamGobbler extends Thread {
+ private InputStream is;
+ private ArrayList<String> log;
+
+ public ArrayList<String> getLog() {
+ return log;
}
- public static void compareExpr(String expected, String tla,
- Hashtable<String, BType> types) {
- String res = TLCExpressionParser.parseLine(tla, types);
- System.out.println(res);
- res = res.replaceAll("\\s", "");
- expected = expected.replaceAll("\\s", "");
- assertEquals(expected, res);
+ StreamGobbler(InputStream is) {
+ this.is = is;
+ this.log = new ArrayList<String>();
}
+ public void run() {
+ try {
+ InputStreamReader isr = new InputStreamReader(is);
+ BufferedReader br = new BufferedReader(isr);
+ String line = null;
+ while ((line = br.readLine()) != null) {
+ System.out.println("> " + line);
+ log.add(line);
+ }
+
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
}
+
diff --git a/src/test/java/standard/SubsitutionTest.java b/src/test/java/standard/SubsitutionTest.java
index ab3cf6b4d0412fc0f170ebcd1779e0cef922c2c4..5fb65abf19d28171e59ccc2cd21f2bf10733127f 100644
--- a/src/test/java/standard/SubsitutionTest.java
+++ b/src/test/java/standard/SubsitutionTest.java
@@ -10,10 +10,11 @@ import org.junit.Test;
+
import de.b2tla.analysis.Ast2String;
import de.b2tla.analysis.MachineContext;
import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UnchangedVariablesFinder;
+import de.b2tla.analysis.unchangedvariables.UnchangedVariablesFinder;
import de.b2tla.exceptions.SubstitutionException;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
diff --git a/src/test/resources/errors/TraceValues.mch b/src/test/resources/errors/TraceValues.mch
new file mode 100644
index 0000000000000000000000000000000000000000..9a245fc47b95d677a0c4838fed9e01e00ac6d881
--- /dev/null
+++ b/src/test/resources/errors/TraceValues.mch
@@ -0,0 +1,76 @@
+MACHINE TraceValues
+SETS S = {s1,s2,s3}
+VARIABLES
+ numberValue,
+ trueValue,
+ falseValue,
+ boolValue,
+ intervalValue,
+ setValue,
+ pairValue,
+ sequenceValue,
+ relationValue,
+ recordValue,
+ functionAsASet,
+ enumerated,
+ setOfTupleValue, /* Cartesian product */
+ setCapValue,
+ setCupValue,
+ setDiffValue,
+ lambdaValue,
+ subsetValue,
+ unionValue,
+ structValue,
+ functionType,
+ stringValue,
+ setPredValue
+INVARIANT
+ numberValue = 1
+ & trueValue = TRUE
+ & falseValue = FALSE
+ & boolValue = BOOL
+ & intervalValue = 1..10
+ & setValue = {1,2}
+ & pairValue = (1, TRUE)
+ & sequenceValue = [1,2,3,4]
+ & relationValue = {(1,2), (1,3)}
+ & recordValue = rec(a: 1, b: TRUE)
+ & functionAsASet = {(1, 1), (3,1)}
+ & enumerated = {s1,s2,s3}
+ & setOfTupleValue = S * S
+ & setCapValue = {x,y| x : 1..2 & y: 1..2}
+ & setCupValue = {x,y| x : 1..3 & y: 1..2}
+ & setDiffValue = {x,y| x : 3..3 & y: 1..2}
+ & lambdaValue = %x,y.(x: 1..3 & y : 1..3 | x+y)
+ & subsetValue = POW(S)
+ & unionValue = union({x| x : POW(BOOL) })
+ & structValue = struct(a: 1..2, b: BOOL)
+ & functionType = 1..3 --> BOOL
+ & stringValue = "hello"
+ & setPredValue = {x,y| x : 1..2 & y: 1..2}
+INITIALISATION
+ numberValue := 1
+ || trueValue := TRUE
+ || falseValue := FALSE
+ || boolValue := BOOL
+ || intervalValue := 1..10
+ || setValue := {1,2}
+ || pairValue := (1, TRUE)
+ || sequenceValue := [1,2,3,4]
+ || relationValue := {(1,2), (1,3)}
+ || recordValue := rec(a: 1, b: TRUE)
+ || functionAsASet := {(1, 1), (3,1)}
+ || enumerated := {s1,s2,s3}
+ || setOfTupleValue := S * S
+ || setCapValue := {x,y| x : 1..2 & y: 1..2} /\ {x,y| x : 1..3 & y: 1..2}
+ || setCupValue := {x,y| x : 1..2 & y: 1..2} \/ {x,y| x : 1..3 & y: 1..2}
+ || setDiffValue := {x,y| x : 1..3 & y: 1..2} - {x,y| x : 1..2 & y: 1..2}
+ || lambdaValue := %x,y.(x: 1..3 & y : 1..3 | x+y)
+ || subsetValue := POW(S)
+ || unionValue := union({x| x : POW(BOOL) })
+ || structValue := struct(a: 1..2, b: BOOL)
+ || functionType := 1..3 --> BOOL
+ || stringValue := "hello"
+ || setPredValue := {x,y| x : 1..2 & y: 1..2}
+OPERATIONS foo = PRE 1 = 2 THEN skip END
+END
\ No newline at end of file
diff --git a/src/test/resources/errors/WellDefinednessErrorFunctionAssignment.mch b/src/test/resources/errors/WellDefinednessErrorFunctionAssignment.mch
deleted file mode 100644
index f0e6c7dc59f30612915263506a2aa45cc3e0078e..0000000000000000000000000000000000000000
--- a/src/test/resources/errors/WellDefinednessErrorFunctionAssignment.mch
+++ /dev/null
@@ -1,7 +0,0 @@
-MACHINE WellDefinednessErrorFunctionAssignment
-VARIABLES f
-INVARIANT f : 1..2 +-> 1..3
-INITIALISATION f := {}
-OPERATIONS
-foo = f(1):= 1
-END
\ No newline at end of file