Fixed bug: 'can not find config file'

src/main/java/de/tlc4b/TLC4B.java

@@ -55,8 +55,7 @@ public class TLC4B {
 		if (TLC4BGlobals.isRunTLC()) {
 			try {
 				TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
-						tlc4b.mainfile.getParentFile());
-
+						tlc4b.buildDir);
 				TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
 				results.evalResults();
 				tlc4b.printResults(results, TLC4BGlobals.isCreateTraceFile());
@@ -89,7 +88,8 @@ public class TLC4B {
 			String trace = results.getTrace();
 			String tracefileName = machineFileNameWithoutFileExtension
 					+ ".tla.trace";
-			File traceFile = createFile(mainfile.getParentFile(), tracefileName, trace, false);
+			File traceFile = createFile(mainfile.getParentFile(),
+					tracefileName, trace, false);
 			if (traceFile != null) {
 				System.out.println("Trace file '" + traceFile.getAbsolutePath()
 						+ "' created.");
@@ -113,17 +113,14 @@ public class TLC4B {
 			System.err.println(e.getMessage());
 			throw e;
 		}
-		// System.out.println(tlc4b.tlaModule);
 		if (TLC4BGlobals.isRunTLC()) {
 			TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
 					tlc4b.buildDir);
 
 			TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
 			results.evalResults();
-			// System.out.println("Result: " + results.getTLCResult());
 
 			tlc4b.printResults(results, false);
-			// System.out.println(results.getTrace());
 
 			System.exit(0);
 		}
@@ -240,23 +237,18 @@ public class TLC4B {
 					+ "' can not be accessed.");
 		}
 
-		
-
 		machineFileNameWithoutFileExtension = mainfile.getName().substring(0,
 				mainfile.getName().length() - 4); // deleting .mch
 
-		
-		
 		if (buildDir == null) {
 			buildDir = new File(mainfile.getParentFile(),
 					machineFileNameWithoutFileExtension);
 		}
-
 	}
 
 	private void createFiles() {
-		buildDir.mkdir();
-		if(TLC4BGlobals.isDeleteOnExit()){
+		boolean dirCreated = buildDir.mkdir();
+		if (dirCreated && TLC4BGlobals.isDeleteOnExit()) {
 			buildDir.deleteOnExit();
 		}
 
@@ -391,9 +383,9 @@ public class TLC4B {
 			boolean deleteOnExit) {
 
 		File file = new File(dir, fileName);
-		
+		boolean exists = false;
 		try {
-			file.createNewFile();
+			exists = file.createNewFile();
 			BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
 					new FileOutputStream(file), "UTF-8"));
 			out.write(text);
@@ -406,7 +398,7 @@ public class TLC4B {
 		} catch (IOException e) {
 			throw new TLC4BIOException(e.getMessage());
 		} finally {
-			if (deleteOnExit && file.exists()) {
+			if (deleteOnExit && exists) {
 				file.deleteOnExit();
 			}
 		}

src/main/java/de/tlc4b/TLCRunner.java

@@ -68,7 +68,6 @@ public class TLCRunner {
 		// list.add("1");
 
 		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();
@@ -97,12 +96,12 @@ public class TLCRunner {
 			list.add("" + TLC4BGlobals.getWorkers());
 		}
 
-		list.add("-config");
-		list.add(machineName + ".cfg");
+		//list.add("-config");
+		//list.add(machineName + ".cfg");
 		list.add(machineName);
+		System.out.println(path.getPath());
 		ToolIO.setUserDir(path.getPath());
 		String[] args = list.toArray(new String[list.size()]);
-
 		TLC tlc = new TLC();
 
 		// handle parameters

src/main/java/de/tlc4b/tlc/TLCResults.java

@@ -51,6 +51,9 @@ public class TLCResults {
 	}
 
 	public int getModelCheckingTime() {
+		if(endTime == null || startTime == null){
+			return -1;
+		}
 		return (int) (endTime.getTime() - startTime.getTime()) / 1000;
 	}
 

src/test/java/testing/Testing2.java

@@ -29,8 +29,8 @@ public class Testing2 extends AbstractParseMachineTest {
 	@Test
 	public void testRunTLC() throws Exception {
 		String[] a = new String[] { machine.getPath() };
-		// TLC4B.main(a);
-		TLC4B.test(a, false);
+		TLC4B.main(a);
+		//TLC4B.test(a, false);
 		// test(a);
 	}
 

src/test/resources/errors/EnumerationError/EnumerationError.cfg

-INIT Init
-NEXT Next
-INVARIANT Invariant1

src/test/resources/errors/EnumerationError/EnumerationError.tla

----- MODULE EnumerationError ----
-EXTENDS Sequences
-VARIABLES x
-Invariant1 == x = <<1>>
-Init == x \in Seq({1}) /\ x \o x = <<1, 1>>
-
-Next == 1 = 2 /\ UNCHANGED <<x>>
-====
\ No newline at end of file