From 26b2a5adb3202f51a677fa79e4cc1c14a03fefaa Mon Sep 17 00:00:00 2001 From: hansen <dominik_hansen@web.de> Date: Wed, 26 Feb 2014 10:45:17 +0100 Subject: [PATCH] Removed the TLCOuputParser. The output of TLC (error type and trace) is stored in auxiliary variables. --- build.gradle | 1 + src/main/java/de/b2tla/B2TLA.java | 163 +++---- src/main/java/de/b2tla/B2TLAGlobals.java | 21 + src/main/java/de/b2tla/B2TlaTranslator.java | 12 +- src/main/java/de/b2tla/StandardModules.java | 103 ---- src/main/java/de/b2tla/TLCRunner.java | 28 -- .../de/b2tla/analysis/ConstantsEvaluator.java | 45 +- .../de/b2tla/analysis/MachineContext.java | 77 ++- .../MachineDeclarationsCollector.java | 206 -------- .../analysis/NotSupportedConstructs.java | 7 + .../java/de/b2tla/analysis/ScopeChecker.java | 447 ------------------ .../b2tla/analysis/UsedStandardModules.java | 1 + .../IdentifierDependencies.java | 3 +- .../{ => typerestriction}/TypeRestrictor.java | 19 +- .../AssignedVariablesFinder.java | 3 +- .../UnchangedVariablesFinder.java | 3 +- .../java/de/b2tla/prettyprint/TLAPrinter.java | 4 +- src/main/java/de/b2tla/tla/Generator.java | 8 +- .../de/b2tla/tlc/TLCExpressionParser.java | 231 --------- src/main/java/de/b2tla/tlc/TLCOutput.java | 254 ---------- src/main/java/de/b2tla/tlc/TLCResults.java | 227 +++++++++ src/main/java/de/b2tla/tlc/TracePrinter.java | 314 ++++++++++++ src/test/java/de/b2tla/tlc/ParserTest.java | 96 ---- .../de/b2tla/tlc/integration/BasicsTest.java | 10 +- .../de/b2tla/tlc/integration/ErrorTest.java | 43 +- .../de/b2tla/tlc/integration/LTLTest.java | 42 +- .../probprivate/AssertionErrorTest.java | 8 +- .../integration/probprivate/DeadlockTest.java | 8 +- .../tlc/integration/probprivate/GoalTest.java | 9 +- .../probprivate/InvariantViolationTest.java | 8 +- .../tlc/integration/probprivate/LawsTest.java | 23 +- .../integration/probprivate/NoErrorTest.java | 8 +- .../probprivate/WellDefinednessTest.java | 10 +- .../b2tla/util/AbstractParseMachineTest.java | 6 +- src/test/java/de/b2tla/util/TLC4BTester.java | 14 + src/test/java/de/b2tla/util/TestPair.java | 9 +- src/test/java/de/b2tla/util/TestUtil.java | 132 ++++-- src/test/java/standard/SubsitutionTest.java | 3 +- src/test/resources/errors/TraceValues.mch | 76 +++ ...WellDefinednessErrorFunctionAssignment.mch | 7 - 40 files changed, 1012 insertions(+), 1677 deletions(-) delete mode 100644 src/main/java/de/b2tla/StandardModules.java delete mode 100644 src/main/java/de/b2tla/analysis/MachineDeclarationsCollector.java delete mode 100644 src/main/java/de/b2tla/analysis/ScopeChecker.java rename src/main/java/de/b2tla/analysis/{ => typerestriction}/IdentifierDependencies.java (95%) rename src/main/java/de/b2tla/analysis/{ => typerestriction}/TypeRestrictor.java (92%) rename src/main/java/de/b2tla/analysis/{ => unchangedvariables}/AssignedVariablesFinder.java (96%) rename src/main/java/de/b2tla/analysis/{ => unchangedvariables}/UnchangedVariablesFinder.java (96%) delete mode 100644 src/main/java/de/b2tla/tlc/TLCExpressionParser.java delete mode 100644 src/main/java/de/b2tla/tlc/TLCOutput.java create mode 100644 src/main/java/de/b2tla/tlc/TLCResults.java create mode 100644 src/main/java/de/b2tla/tlc/TracePrinter.java delete mode 100644 src/test/java/de/b2tla/tlc/ParserTest.java create mode 100644 src/test/java/de/b2tla/util/TLC4BTester.java create mode 100644 src/test/resources/errors/TraceValues.mch delete mode 100644 src/test/resources/errors/WellDefinednessErrorFunctionAssignment.mch diff --git a/build.gradle b/build.gradle index 030349a..a58a7d6 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 09df230..8dc0a09 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 8b1589d..e5a5fb4 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 e717c22..0ebda89 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 48e122e..0000000 --- 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 b82a1ea..824ff3d 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 5516ec9..057ef9a 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 bab46a8..4e35c64 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 812568b..0000000 --- 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 44af924..3148bcf 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 aa9d7ae..0000000 --- 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 fe8e1dd..bad73b0 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 ce63c85..c0a0367 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 f7fc53d..2ae78ec 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 934a5c6..a682f46 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 cdfd275..ff79eb0 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 d250567..635be7f 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 07361ae..37776ba 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 9e0cb9c..0000000 --- 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 fbe19fa..0000000 --- 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 0000000..bbc4117 --- /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 0000000..72b371c --- /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 99de3c4..0000000 --- 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 d1849fa..5241909 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 f086bdc..dd269d5 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 df33f40..26b17e1 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 385bcce..dd23fcc 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 590d82a..bb004fe 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 336eff1..1f7298d 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 9f611e7..f620c28 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 9155944..5a4668b 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 bdee2c3..1c26915 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 96dfbcd..731e518 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 ee01335..692cb73 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 0000000..e848220 --- /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 d454e5d..47aebd6 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 6d67b21..34a85dd 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 ab3cf6b..5fb65ab 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 0000000..9a245fc --- /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 f0e6c7d..0000000 --- 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 -- GitLab