diff --git a/build.gradle b/build.gradle index 294c5f31558fe17ee8d2a691d0535f87e28c6d66..68144940d3e8b8f8165ea9c3b768cc0f787b3a26 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 8866431f20c28bbe6788e915c4569a873fcb2e68..0000000000000000000000000000000000000000 --- 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 5b271daad9b70363d59292d75c8a89593c7671ac..79837b61ed22c78e0a20ee5e2f988875926a1afe 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 228e7ad60e26f3a7e43b849ce034c5de5b4a0050..c8fab7f42bb3a01224bb5eb57db4e3f261f51f83 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 64b14f3cd8a7437273373aea5c3e09ba977fd965..dab9de1f4258bb3d38c2cbbf26fd68d3d90240b6 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 11d1f88992b5e075ac52c6a3b1df521ef4e39029..0000000000000000000000000000000000000000 --- 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 17567700a0b5f16667cccb5ffcb044edb366eb72..0000000000000000000000000000000000000000 --- 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 73095d7d6e53b86364ad29417cfd1fca56730803..db9985fa3ac223ab625813d70d55470ea6db0a64 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 7e2432f821f1184c8743d1c7fb752181c38414a8..44b007b843e16fabf980c463943058289a84b95e 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 f75ca32309a33cd3584f4c94a97695b8d0c151c8..d8f834534f95d8540da20734aa120511d575d0ad 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 9875872645e7b3440e6b48faf4a891c6aefa1ed1..71ca7356cf5d304946b468113c32402b0b50cbb5 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 d5725d2ddd84060d68adbe9bfbadf7264f44de73..289aedef3ae2d49275e7987574e83507dd06d85d 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 18c1d88154afd1ea93fc3ef2df025225176588fa..47e58edc47e05902aeb39af8c2d033d73dae34e0 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 a3d2dfadad0b3d12c004f62129a8ed25ebb85065..93629145ae72890aa8899a94820b82111db36b77 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 b5328177578ee073e20158dee15a2148d6213583..bd584977bc6d734c37dad534f021abd042c0a976 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 0000000000000000000000000000000000000000..a71a1843f49caba6614939ebc4bcaa6ede91ea41 --- /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