From 3d7f912c6a7b486db7eb742f5b5711c8c064d3d2 Mon Sep 17 00:00:00 2001 From: Dominik Hansen <Dominik.Hansen@uni-duesseldorf.de> Date: Mon, 27 May 2013 15:21:31 +0200 Subject: [PATCH] Modified B-TLC output. Former-commit-id: b0c4ac66b46c4d35d9162fe6ec43d4f3cd4687a7 --- build.gradle | 52 ++++++------------- build.xml | 30 ----------- src/main/java/de/b2tla/B2TLA.java | 4 +- src/main/java/de/b2tla/Globals.java | 2 - src/main/java/de/b2tla/TLCRunner.java | 11 ++++ src/main/java/de/b2tla/TLCTester.java | 14 ----- src/main/java/de/b2tla/Testing.java | 16 ------ .../java/de/b2tla/prettyprint/TLAPrinter.java | 16 +++++- src/main/java/de/b2tla/tlc/TLCOutput.java | 11 ++-- .../java/de/b2tla/util/BTLCPrintStream.java | 4 +- .../de/b2tla/prettyprint/ConstantsTest.java | 2 + .../prettyprint/MachineParameterTest.java | 3 +- .../de/b2tla/prettyprint/OperationsTest.java | 3 ++ .../de/b2tla/prettyprint/RenamerTest.java | 1 + .../de/b2tla/tlc/integration/ErrorTest.java | 8 ++- src/test/resources/error/EnumerationError.mch | 5 ++ 16 files changed, 71 insertions(+), 111 deletions(-) delete mode 100644 build.xml delete mode 100644 src/main/java/de/b2tla/TLCTester.java delete mode 100644 src/main/java/de/b2tla/Testing.java create mode 100644 src/test/resources/error/EnumerationError.mch diff --git a/build.gradle b/build.gradle index 294c5f3..6814494 100644 --- a/build.gradle +++ b/build.gradle @@ -12,78 +12,60 @@ repositories { mavenRepo name: 'cobra_ext', url: "http://cobra.cs.uni-duesseldorf.de/artifactory/repo" } -configurations { - // configuration that holds jars to copy into lib - releaseJars - } +configurations { // configuration that holds jars to copy into lib + releaseJars } def parser_version = '2.4.18-SNAPSHOT' dependencies { - compile files('libs/tla2tools.jar') + compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6') compile (group: 'de.prob', name: 'prologlib', version: parser_version) compile (group: 'de.prob', name: 'parserbase', version: parser_version) compile (group: 'de.prob', name: 'bparser', version: parser_version) - + testCompile (group: 'junit', name: 'junit', version: '4.+') testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.3-SNAPSHOT') - + releaseJars (group: 'de.prob', name: 'prologlib', version: parser_version) releaseJars (group: 'de.prob', name: 'parserbase', version: parser_version) releaseJars (group: 'de.prob', name: 'bparser', version: parser_version) - } - -ant.importBuild 'build.xml' - -compileJava { - dependsOn tla2tools } -test { - exclude('de/b2tla/tlc/integration/**') -} + +test { exclude('de/b2tla/tlc/integration/**') } task integrationtest(type: Test){ - forkEvery = 1 - doFirst{ - println("Running integration tests") - } + doFirst{ println("Running integration tests") } scanForTestClasses = true include('de/b2tla/tlc/integration/**') } jar { from sourceSets.main.allJava } -jar { +jar { from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) } } manifest.mainAttributes("Main-Class" : 'de.b2tla.B2TLA') manifest.mainAttributes("Class-Path": './tla/ tla2tools.jar') -task copy(dependsOn: build) << { +task b2tla(dependsOn: build) << { copy { from('build/libs/') into('build/b2tla') include('b2tla-'+project.version+'.jar') rename('(b2tla)-(.+)', 'B2TLA.jar') } - copy { - from('src/main/resources/') { include '**/*' } - into 'build/b2tla' - } - copy { - from('build/b2tla') - into('externalLibs/') - include('B2TLA.jar') - } } -task deploy(type: Zip, dependsOn: copy) { - from('build/') { include 'b2tla/**' } - archiveName = 'b2tla.zip' - doLast{ println "Created archive: "+archivePath } +task deploy(dependsOn: build) { + copy { + from('build/libs/') + into('build/b2tla') + include('b2tla-'+project.version+'.jar') + rename('(b2tla)-(.+)', 'B2TLA.jar') + } } diff --git a/build.xml b/build.xml deleted file mode 100644 index 8866431..0000000 --- a/build.xml +++ /dev/null @@ -1,30 +0,0 @@ -<project default="tla"> - <target name="tla.check"> - <condition property="tla.exists"> - <available file="externalLibs" type="dir" /> - </condition> - </target> - - <target name="tla" depends="tla.check" unless="tla.exists"> - <mkdir dir="externalLibs/" /> - <get src="http://ftp.research.microsoft.com/downloads/41b4a0aa-5fad-4118-916a-45ed9fd48bf0/tla.zip" dest="externalLibs/" /> - <unzip src="externalLibs/tla.zip" dest="externalLibs/" /> - </target> - - <target name="tla2tools.check"> - <condition property="tla2tools.exists"> - <available file="libs/tla2tools.jar"/> - </condition> - </target> - - <target name="tla2tools" depends="tla2tools.check" unless="tla2tools.exists"> - <mkdir dir="libs/" /> - <get src="http://tla.msr-inria.inria.fr/tlatoolbox/dist/tla2tools.jar" dest="libs/" /> - </target> - - - <target name="delete"> - <delete dir="externalLibs" /> - </target> - -</project> \ No newline at end of file diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java index 5b271da..79837b6 100644 --- a/src/main/java/de/b2tla/B2TLA.java +++ b/src/main/java/de/b2tla/B2TLA.java @@ -66,7 +66,7 @@ public class B2TLA { } if (Globals.runTLC) { - ArrayList<String> output = TLCRunner.runTLC( + ArrayList<String> output = TLCRunner.runTLCInANewJVM( b2tla.machineName, b2tla.path); ERROR error = TLCOutput.findError(output); System.out.println(error); @@ -80,7 +80,7 @@ public class B2TLA { TLCOutput tlcOutput = new TLCOutput(machineName, output.toArray(new String[output.size()])); tlcOutput.parseTLCOutput(); - System.out.println("ERROR: " + tlcOutput.getError()); + System.out.println("Result: " + tlcOutput.getError()); StringBuilder trace = tlcOutput.getErrorTrace(); if (tlcOutput.hasTrace() && createTraceFile) { String tracefileName = machineName + ".tla.trace"; diff --git a/src/main/java/de/b2tla/Globals.java b/src/main/java/de/b2tla/Globals.java index 228e7ad..c8fab7f 100644 --- a/src/main/java/de/b2tla/Globals.java +++ b/src/main/java/de/b2tla/Globals.java @@ -1,7 +1,5 @@ package de.b2tla; -import de.b2tla.tlc.TLCOutput; - public class Globals { public static int DEFERRED_SET_SIZE = 3; public static boolean GOAL = true; diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java index 64b14f3..dab9de1 100644 --- a/src/main/java/de/b2tla/TLCRunner.java +++ b/src/main/java/de/b2tla/TLCRunner.java @@ -42,6 +42,9 @@ public class TLCRunner { if (!Globals.deadlockCheck) { list.add("-deadlock"); } + //list.add("-coverage"); + //list.add("1"); + String[] args = list.toArray(new String[list.size()]); ProcessHelper helper = new ProcessHelper(); System.out.println("Starting JVM..."); @@ -89,9 +92,17 @@ public class TLCRunner { System.setOut(systemOut); ArrayList<String> messages = btlcStream.getArrayList(); + String[] ms =ToolIO.getAllMessages(); + System.out.println("--------------------------------"); + for (int i = 0; i < ms.length; i++) { + System.out.println(">> "+ms[i]); + } closeThreads(); + //return new ArrayList<String>(Arrays.asList(ms)); return messages; + + //TLCOutput tlcOutput = new TLCOutput(machineName, messages); //tlcOutput.parseTLCOutput(); // TLCOutputEvaluator evaluator = new TLCOutputEvaluator(machineName, diff --git a/src/main/java/de/b2tla/TLCTester.java b/src/main/java/de/b2tla/TLCTester.java deleted file mode 100644 index 11d1f88..0000000 --- a/src/main/java/de/b2tla/TLCTester.java +++ /dev/null @@ -1,14 +0,0 @@ -package de.b2tla; - -import java.io.IOException; - -import de.be4.classicalb.core.parser.exceptions.BException; - -public class TLCTester { - - - public static void main(String[] args) throws IOException, BException{ - String[] a = new String[]{ ".\\src\\test\\resources\\error\\ParseError.mch"}; - B2TLA.main(a); - } -} diff --git a/src/main/java/de/b2tla/Testing.java b/src/main/java/de/b2tla/Testing.java deleted file mode 100644 index 1756770..0000000 --- a/src/main/java/de/b2tla/Testing.java +++ /dev/null @@ -1,16 +0,0 @@ -package de.b2tla; -import java.io.File; -import java.io.IOException; - -import de.be4.classicalb.core.parser.BParser; -import de.be4.classicalb.core.parser.exceptions.BException; - -public class Testing { - - public static void main(String[] args) throws IOException, BException { - int[] array = {1,2,3,4}; - System.out.println(array[4]); - final BParser parser = new BParser("m"); - parser.parseFile(new File("src/folder/M2.mch"), false); - } -} diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java index 73095d7..db9985f 100644 --- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java +++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java @@ -121,7 +121,7 @@ public class TLAPrinter extends DepthFirstAdapter { if (this.configFile.isInit()) { this.configFileString.append("INIT Init\n"); } - if (this.configFile.isNext()) { + if (this.configFile.isInit()) { this.configFileString.append("NEXT Next\n"); } if (configFile.isInvariant()) { @@ -276,8 +276,20 @@ public class TLAPrinter extends DepthFirstAdapter { private void printOperations() { ArrayList<POperation> ops = this.tlaModule.getOperations(); - if (ops.size() == 0) + if (ops.size() == 0) { + ArrayList<Node> vars = tlaModule.getVariables(); + if (vars.size() > 0) { + tlaModuleString.append("Next == 1 = 2 /\\ UNCHANGED <<"); + for (int i = 0; i < vars.size(); i++) { + vars.get(i).apply(this); + if (i < vars.size() - 1) { + tlaModuleString.append(", "); + } + } + tlaModuleString.append(">>\n"); + } return; + } for (int i = 0; i < ops.size(); i++) { ops.get(i).apply(this); } diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java index 7e2432f..44b007b 100644 --- a/src/main/java/de/b2tla/tlc/TLCOutput.java +++ b/src/main/java/de/b2tla/tlc/TLCOutput.java @@ -11,8 +11,8 @@ public class TLCOutput { private final String moduleName; private String[] messages; - Date startTime; - Date finishedTime; + Date startingTime; + Date finishingTime; ERROR error; ArrayList<String> states = new ArrayList<String>(); StringBuilder trace; @@ -23,7 +23,7 @@ public class TLCOutput { } public long getRunningTime() { - long time = (finishedTime.getTime() - startTime.getTime()) / 1000; + long time = (finishingTime.getTime() - startingTime.getTime()) / 1000; return time; } @@ -48,10 +48,9 @@ public class TLCOutput { for (int i = 0; i < messages.length; i++) { String m = messages[i]; if (m.startsWith("Starting...")) { - // startingTime = m; - startTime = parseTime(m); + startingTime = parseTime(m); } else if (m.startsWith("Finished.")) { - finishedTime = parseTime(m); + finishingTime = parseTime(m); } else if (m.startsWith("Error:")) { ERROR e = findError(m); if(e != null){ diff --git a/src/main/java/de/b2tla/util/BTLCPrintStream.java b/src/main/java/de/b2tla/util/BTLCPrintStream.java index f75ca32..d8f8345 100644 --- a/src/main/java/de/b2tla/util/BTLCPrintStream.java +++ b/src/main/java/de/b2tla/util/BTLCPrintStream.java @@ -33,7 +33,7 @@ public class BTLCPrintStream extends PrintStream { public void println(String str){ synchronized (BTLCPrintStream.class){ if(!Globals.tool){ - console.println("> " + str); + console.println("" + str); } array.add(str); } @@ -41,7 +41,7 @@ public class BTLCPrintStream extends PrintStream { @Override public void print(String str){ synchronized (BTLCPrintStream.class){ - console.println(str); + console.println("> " +str); array.add(str); } } diff --git a/src/test/java/de/b2tla/prettyprint/ConstantsTest.java b/src/test/java/de/b2tla/prettyprint/ConstantsTest.java index 9875872..71ca735 100644 --- a/src/test/java/de/b2tla/prettyprint/ConstantsTest.java +++ b/src/test/java/de/b2tla/prettyprint/ConstantsTest.java @@ -17,6 +17,7 @@ public class ConstantsTest { + "k == 1 \n" + "VARIABLES k2 \n" + "Init == k = 1 /\\ k2 \\in {k} \n" + + "Next == 1 = 2 /\\ UNCHANGED <<k2>>\n" + "======"; compare(expected, machine); } @@ -31,6 +32,7 @@ public class ConstantsTest { String expected = "---- MODULE test----\n" + "EXTENDS Integers\n" + "VARIABLES k \n" + "Init == k \\in {1} \n" + + "Next == 1 = 2 /\\ UNCHANGED <<k>>\n" + "======"; compare(expected, machine); } diff --git a/src/test/java/de/b2tla/prettyprint/MachineParameterTest.java b/src/test/java/de/b2tla/prettyprint/MachineParameterTest.java index d5725d2..289aede 100644 --- a/src/test/java/de/b2tla/prettyprint/MachineParameterTest.java +++ b/src/test/java/de/b2tla/prettyprint/MachineParameterTest.java @@ -28,8 +28,9 @@ public class MachineParameterTest { String expectedModule = "---- MODULE test----\n" + "VARIABLES a\n" + "Init == a \\in {1,2,3}\n" + + "Next == 1 = 2 /\\ UNCHANGED <<a>>\n" + "======"; - String expectedConfig = "INIT Init"; + String expectedConfig = "INIT Init\nNEXT Next"; compareConfig(expectedModule, expectedConfig, machine); } diff --git a/src/test/java/de/b2tla/prettyprint/OperationsTest.java b/src/test/java/de/b2tla/prettyprint/OperationsTest.java index 18c1d88..47e58ed 100644 --- a/src/test/java/de/b2tla/prettyprint/OperationsTest.java +++ b/src/test/java/de/b2tla/prettyprint/OperationsTest.java @@ -18,6 +18,7 @@ public class OperationsTest { + "VARIABLES x \n" + "Inv == x = 1\n" + "Init == x = 1 \n" + + "Next == 1 = 2 /\\ UNCHANGED <<x>>\n" + "===="; compare(expected, machine); } @@ -55,6 +56,7 @@ public class OperationsTest { + "VARIABLES x \n" + "Invariant == x = 1\n" + "Init == x = 1 \n" + + "Next == 1 = 2 /\\ UNCHANGED <<x>>\n" + "===="; compare(expected, machine); } @@ -71,6 +73,7 @@ public class OperationsTest { + "VARIABLES x, y \n" + "Invariant == x = 1 /\\ y = 1\n" + "Init == x = 1 /\\ y = 1 \n" + + "Next == 1 = 2 /\\ UNCHANGED <<x, y>>\n" + "===="; compare(expected, machine); } diff --git a/src/test/java/de/b2tla/prettyprint/RenamerTest.java b/src/test/java/de/b2tla/prettyprint/RenamerTest.java index a3d2dfa..9362914 100644 --- a/src/test/java/de/b2tla/prettyprint/RenamerTest.java +++ b/src/test/java/de/b2tla/prettyprint/RenamerTest.java @@ -31,6 +31,7 @@ public class RenamerTest { + "VARIABLES WITH_1 \n" + "Inv == WITH_1 = 1\n" + "Init == WITH_1 = 1 \n" + + "Next == 1 = 2 /\\ UNCHANGED <<WITH_1>>\n" + "===="; compare(expected, machine); } diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java index b532817..bd58497 100644 --- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java +++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java @@ -10,7 +10,7 @@ import de.b2tla.tlc.TLCOutput; import de.b2tla.tlc.TLCOutput.ERROR; public class ErrorTest { - + @Test public void testInvariantError() throws Exception { String[] a = new String[] { ".\\src\\test\\resources\\error\\InvariantError.mch" }; @@ -46,5 +46,11 @@ public class ErrorTest { String[] a = new String[] { ".\\src\\test\\resources\\error\\NoError.mch" }; assertEquals(TLCOutput.ERROR.NoError, B2TLA.test(a)); } + + @Test + public void testEnumerationError() throws Exception { + String[] a = new String[] { ".\\src\\test\\resources\\error\\EnumerationError.mch" }; + assertEquals(TLCOutput.ERROR.NoError, B2TLA.test(a)); + } } diff --git a/src/test/resources/error/EnumerationError.mch b/src/test/resources/error/EnumerationError.mch new file mode 100644 index 0000000..a71a184 --- /dev/null +++ b/src/test/resources/error/EnumerationError.mch @@ -0,0 +1,5 @@ +MACHINE EnumerationError +VARIABLES x +INVARIANT x = [1] +INITIALISATION x:(x: seq({1}) & x^x = [1,1]) +END \ No newline at end of file -- GitLab