refactored file handling

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

@@ -21,9 +21,13 @@ import de.tlc4b.util.StopWatch;
 
 public class TLC4B {
 
-	private String mainFileName;
+	private String filename;
+	private File mainfile;
 	private String machineFileNameWithoutFileExtension; 
-	private String path;
+	// e.g. Test of file foo/bar/Test.mch
+	
+	private File buildDir;
+
 	private String tlaModule;
 	private String config;
 	private Translator translator;
@@ -51,7 +55,7 @@ public class TLC4B {
 		if (TLC4BGlobals.isRunTLC()) {
 			try {
 				TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
-						tlc4b.path);
+						tlc4b.mainfile.getParentFile());
 
 				TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
 				results.evalResults();
@@ -85,7 +89,7 @@ public class TLC4B {
 			String trace = results.getTrace();
 			String tracefileName = machineFileNameWithoutFileExtension
 					+ ".tla.trace";
-			File traceFile = createFile(path, tracefileName, trace, false);
+			File traceFile = createFile(mainfile.getParentFile(), tracefileName, trace, false);
 			if (traceFile != null) {
 				System.out.println("Trace file '" + traceFile.getAbsolutePath()
 						+ "' created.");
@@ -112,7 +116,7 @@ public class TLC4B {
 		// System.out.println(tlc4b.tlaModule);
 		if (TLC4BGlobals.isRunTLC()) {
 			TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
-					tlc4b.path);
+					tlc4b.buildDir);
 
 			TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
 			results.evalResults();
@@ -121,27 +125,10 @@ public class TLC4B {
 			tlc4b.printResults(results, false);
 			// System.out.println(results.getTrace());
 
-			
 			System.exit(0);
 		}
 	}
 
-	/*
-	 * private void printTestResultsForTestscript() { TLCResults tlcResults =
-	 * null; // This output is adapted to Ivo's testscript
-	 * System.out.println("------------- Results -------------");
-	 * System.out.println("Model Checking Time: " +
-	 * (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" +
-	 * tlcResults.getResultString()); }
-	 * 
-	 * }
-	 */
-
 	private void handleParameter(String[] args) {
 		int index = 0;
 		while (index < args.length) {
@@ -160,7 +147,7 @@ public class TLC4B {
 			} else if (args[index].toLowerCase().equals("-tool")) {
 				TLC4BGlobals.setTool(false);
 			} else if (args[index].toLowerCase().equals("-tmp")) {
-				path = System.getProperty("java.io.tmpdir");
+				buildDir = new File(System.getProperty("java.io.tmpdir"));
 			} else if (args[index].toLowerCase().equals("-noltl")) {
 				TLC4BGlobals.setCheckltl(false);
 			} else if (args[index].toLowerCase().equals("-lazyconstants")) {
@@ -198,17 +185,17 @@ public class TLC4B {
 				throw new TLC4BIOException("Error: unrecognized option: "
 						+ args[index]);
 			} else {
-				if (mainFileName != null) {
+				if (filename != null) {
 					throw new TLC4BIOException(
-							"Error: more than one input files: " + mainFileName
+							"Error: more than one input files: " + filename
 									+ " and " + args[index]);
 				}
-				mainFileName = args[index];
+				filename = args[index];
 
 			}
 			index++;
 		}
-		if (mainFileName == null) {
+		if (filename == null) {
 			throw new TLC4BIOException("Main machine required!");
 		}
 	}
@@ -220,7 +207,7 @@ public class TLC4B {
 		if (TLC4BGlobals.isTranslate()) {
 			StopWatch.start("Parsing");
 			translator = new Translator(machineFileNameWithoutFileExtension,
-					getFile(), this.ltlFormula, this.constantsSetup);
+					mainfile, this.ltlFormula, this.constantsSetup);
 			StopWatch.stop("Parsing");
 			StopWatch.start("Pure");
 			translator.translate();
@@ -234,37 +221,56 @@ public class TLC4B {
 	}
 
 	private void handleMainFileName() {
-		String name = mainFileName;
-		name = name.replace("\\", File.separator);
-		name = name.replace("/", File.separator);
-
-		mainFileName = name;
+		// the following is fix to handle incorrect file names
+		filename = filename.replace("\\", File.separator);
+		filename = filename.replace("/", File.separator);
+		if (!filename.toLowerCase().endsWith(".mch")) {
+			filename = filename + ".mch";
+		}
 
-		if (name.toLowerCase().endsWith(".mch")) {
-			name = name.substring(0, name.length() - 4);
+		mainfile = new File(filename);
+		if (!mainfile.exists()) {
+			throw new TLC4BIOException("The file " + mainfile.getPath()
+					+ " does not exist.");
 		}
-		if (path == null) {
-			if (name.contains(File.separator)) {
-				path = name.substring(0, name.lastIndexOf(File.separator) + 1);
-			} else {
-				path = "." + File.separator;
+		try {
+			mainfile = mainfile.getCanonicalFile();
+		} catch (IOException e) {
+			throw new TLC4BIOException("The file '" + mainfile.getPath()
+					+ "' can not be accessed.");
 		}
+		
+		
+
+		machineFileNameWithoutFileExtension = mainfile.getName().substring(0,
+				mainfile.getName().length() - 4); // deleting .mch
+
+		
+		
+		if (buildDir == null) {
+			buildDir = new File(mainfile.getParentFile(),
+					machineFileNameWithoutFileExtension);
 		}
 
-		machineFileNameWithoutFileExtension = name.substring(name
-				.lastIndexOf(File.separator) + 1);
 	}
 
 	private void createFiles() {
-		File moduleFile = createFile(path, machineFileNameWithoutFileExtension
-				+ ".tla", tlaModule, TLC4BGlobals.isDeleteOnExit());
+		buildDir.mkdir();
+		if(TLC4BGlobals.isDeleteOnExit()){
+			buildDir.deleteOnExit();
+		}
+		
+		File moduleFile = createFile(buildDir,
+				machineFileNameWithoutFileExtension + ".tla", tlaModule,
+				TLC4BGlobals.isDeleteOnExit());
 		if (moduleFile != null) {
 			System.out.println("TLA+ module '" + moduleFile.getAbsolutePath()
 					+ "' created.");
 		}
 
-		File configFile = createFile(path, machineFileNameWithoutFileExtension
-				+ ".cfg", config, TLC4BGlobals.isDeleteOnExit());
+		File configFile = createFile(buildDir,
+				machineFileNameWithoutFileExtension + ".cfg", config,
+				TLC4BGlobals.isDeleteOnExit());
 		if (configFile != null) {
 			System.out.println("Configuration file '"
 					+ configFile.getAbsolutePath() + "' created.");
@@ -275,66 +281,69 @@ public class TLC4B {
 	private void createStandardModules() {
 		if (translator.getUsedStandardModule().contains(
 				STANDARD_MODULES.Relations)) {
-			createStandardModule(path, STANDARD_MODULES.Relations.toString());
+			createStandardModule(buildDir,
+					STANDARD_MODULES.Relations.toString());
 		}
 
 		if (translator.getUsedStandardModule().contains(
 				STANDARD_MODULES.Functions)) {
-			createStandardModule(path, STANDARD_MODULES.Functions.toString());
+			createStandardModule(buildDir,
+					STANDARD_MODULES.Functions.toString());
 		}
 
 		if (translator.getUsedStandardModule().contains(
 				STANDARD_MODULES.BBuiltIns)) {
-			createStandardModule(path, STANDARD_MODULES.BBuiltIns.toString());
+			createStandardModule(buildDir,
+					STANDARD_MODULES.BBuiltIns.toString());
 		}
 
 		if (translator.getUsedStandardModule().contains(
 				STANDARD_MODULES.FunctionsAsRelations)) {
-			createStandardModule(path,
+			createStandardModule(buildDir,
 					STANDARD_MODULES.FunctionsAsRelations.toString());
 			if (!translator.getUsedStandardModule().contains(
 					STANDARD_MODULES.Functions)) {
-				createStandardModule(path,
+				createStandardModule(buildDir,
 						STANDARD_MODULES.Functions.toString());
 			}
 		}
 
 		if (translator.getUsedStandardModule().contains(
 				STANDARD_MODULES.SequencesExtended)) {
-			createStandardModule(path,
+			createStandardModule(buildDir,
 					STANDARD_MODULES.SequencesExtended.toString());
 		}
 
 		if (translator.getUsedStandardModule().contains(
 				STANDARD_MODULES.SequencesAsRelations)) {
-			createStandardModule(path,
+			createStandardModule(buildDir,
 					STANDARD_MODULES.SequencesAsRelations.toString());
 
 			if (!translator.getUsedStandardModule().contains(
 					STANDARD_MODULES.Relations)) {
-				createStandardModule(path,
+				createStandardModule(buildDir,
 						STANDARD_MODULES.Relations.toString());
 			}
 
 			if (!translator.getUsedStandardModule().contains(
 					STANDARD_MODULES.FunctionsAsRelations)) {
-				createStandardModule(path,
+				createStandardModule(buildDir,
 						STANDARD_MODULES.FunctionsAsRelations.toString());
 			}
 
 			if (!translator.getUsedStandardModule().contains(
 					STANDARD_MODULES.Functions)) {
-				createStandardModule(path,
+				createStandardModule(buildDir,
 						STANDARD_MODULES.Functions.toString());
 			}
 		}
 	}
 
-	private void createStandardModule(String path, String name) {
+	private void createStandardModule(File path, String name) {
 		// standard modules are copied from the standardModules folder to the
 		// current directory
 
-		File file = new File(path + File.separator + name + ".tla");
+		File file = new File(path, name + ".tla");
 		InputStream is = null;
 		FileOutputStream fos = null;
 		try {
@@ -356,8 +365,8 @@ public class TLC4B {
 			while ((read = is.read(bytes)) != -1) {
 				fos.write(bytes, 0, read);
 			}
-			System.out.println("Standard module '" + path + name
-					+ ".tla' created.");
+			System.out.println("Standard module '" + file.getName()
+					+ "' created.");
 		} catch (IOException e) {
 			throw new TLC4BIOException(e.getMessage());
 		} finally {
@@ -378,22 +387,14 @@ public class TLC4B {
 		}
 	}
 
-	private File getFile() {
-		File mainFile = new File(mainFileName);
-		if (!mainFile.exists()) {
-			throw new TLC4BIOException("The file " + mainFileName
-					+ " does not exist.");
-		}
-		return mainFile;
-	}
-
-	public static File createFile(String dir, String fileName, String text,
+	public static File createFile(File dir, String fileName, String text,
 			boolean deleteOnExit) {
-		File file = new File(dir + File.separator + fileName);
 
-		BufferedWriter out;
+		File file = new File(dir, fileName);
+		
 		try {
-			out = new BufferedWriter(new OutputStreamWriter(
+			file.createNewFile();
+			BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
 					new FileOutputStream(file), "UTF-8"));
 			out.write(text);
 			out.close();

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

 package de.tlc4b;
 
 import java.io.BufferedReader;
+import java.io.File;
 import java.io.IOException;
 import java.io.InputStream;
 import java.io.InputStreamReader;
@@ -81,7 +82,7 @@ public class TLCRunner {
 		return stdOut.getLog();
 	}
 
-	public static void runTLC(String machineName, String path) {
+	public static void runTLC(String machineName, File path) {
 
 		System.out.println("--------------------------------");
 
@@ -99,7 +100,7 @@ public class TLCRunner {
 		list.add("-config");
 		list.add(machineName + ".cfg");
 		list.add(machineName);
-		ToolIO.setUserDir(path);
+		ToolIO.setUserDir(path.getPath());
 		String[] args = list.toArray(new String[list.size()]);
 
 		TLC tlc = new TLC();

src/main/java/de/tlc4b/Translator.java

@@ -111,7 +111,6 @@ public class Translator {
 				machineContext);
 
 		
-
 		ConstantsEliminator constantsEliminator = new ConstantsEliminator(
 				machineContext);
 		constantsEliminator.start();

src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java

@@ -194,7 +194,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
 			this.rangeOfIdentifierTable = new Hashtable<Node, ArrayList<PExpression>>();
 
 			this.identifiers = new HashSet<Node>();
-			this.identifiers.addAll(machineContext.getConstants().values());
+			this.identifiers.addAll(machineContext.getBMachineConstants().values());
 			this.identifiers.addAll(machineContext.getScalarParameter()
 					.values());
 
@@ -260,8 +260,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
 				AEqualPredicate equals = (AEqualPredicate) constantsSetup;
 				PExpression left = equals.getLeft();
 				Node left_ref = machineContext.getReferences().get(left);
+				if(rangeOfIdentifierTable.containsKey(left_ref)){
+					System.out.println("hallo");
+				}
 				ArrayList<PExpression> currentRange = rangeOfIdentifierTable.get(left_ref);
-				
 				boolean found = false;
 				for (PExpression pExpression : currentRange) {
 					if(pExpression.toString().equals(equals.getRight().toString())){

src/main/java/de/tlc4b/analysis/MachineContext.java

@@ -90,7 +90,9 @@ public class MachineContext extends DepthFirstAdapter {
 	private final LinkedHashMap<String, Node> enumeratedSets;
 	private final LinkedHashMap<String, Node> enumValues;
 
-	private final LinkedHashMap<String, Node> constants;
+	private LinkedHashMap<String, Node> constants;
+	private final LinkedHashMap<String, Node> bMachineConstants;
+	
 	private final LinkedHashMap<String, Node> variables;
 	private final LinkedHashMap<String, Node> definitions;
 	private final LinkedHashMap<String, Node> operations;
@@ -112,6 +114,8 @@ public class MachineContext extends DepthFirstAdapter {
 
 	protected final Hashtable<Node, Node> referencesTable;
 
+	
+	
 	public MachineContext(String machineName, Start start, String ltlFormula,
 			PPredicate constantsSetup) {
 		this.start = start;
@@ -133,6 +137,7 @@ public class MachineContext extends DepthFirstAdapter {
 		this.enumeratedSets = new LinkedHashMap<String, Node>();
 		this.enumValues = new LinkedHashMap<String, Node>();
 		this.constants = new LinkedHashMap<String, Node>();
+		this.bMachineConstants = new LinkedHashMap<String, Node>();
 		this.variables = new LinkedHashMap<String, Node>();
 		this.definitions = new LinkedHashMap<String, Node>();
 		this.operations = new LinkedHashMap<String, Node>();
@@ -484,6 +489,7 @@ public class MachineContext extends DepthFirstAdapter {
 			String name = Utils.getIdentifierAsString(c.getIdentifier());
 			exist(c.getIdentifier());
 			constants.put(name, c);
+			bMachineConstants.put(name, c);
 		}
 	}
 
@@ -1112,6 +1118,11 @@ public class MachineContext extends DepthFirstAdapter {
 	public boolean constantSetupInTraceFile() {
 		return constantSetupInTraceFile;
 	}
+
+	public LinkedHashMap<String, Node> getBMachineConstants() {
+		return bMachineConstants;
+	}
+
 }
 
 class PMachineClauseComparator implements Comparator<PMachineClause>,

src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java

@@ -7,6 +7,8 @@ import java.util.Hashtable;
 import java.util.List;
 import java.util.Set;
 
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
 import de.be4.classicalb.core.parser.Utils;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.AAnySubstitution;

src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java

@@ -254,5 +254,17 @@ public class TypeRestrictionsTest {
 		compare(expected, machine);
 	}
 	
+	@Ignore // TODO improve type restriction algorithm
+	@Test
+	public void test2Variables() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES #a,b.( a : {1}  & b : {a})\n" + "END";
+		
+		String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+				+ "ASSUME \\E <<a,b>> \\in {<<1,1>>} : TRUE \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
 	
 }

src/test/java/testing/Testing2.java

@@ -28,8 +28,7 @@ public class Testing2 extends AbstractParseMachineTest {
 
 	@Test
 	public void testRunTLC() throws Exception {
-		String[] a = new String[] {
-				machine.getPath(), "-noLTL", "-wdcheck"};
+		String[] a = new String[] { machine.getPath() };
 		// 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