diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 50b979c35177aacb5927474bd9cc319532a08868..28d3f9e637d645d5860b9394e3ccec42fa3b1535 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -21,9 +21,13 @@ import de.tlc4b.util.StopWatch;
public class TLC4B {
- private String mainFileName;
- private String machineFileNameWithoutFileExtension;
- private String path;
+ private String filename;
+ private File mainfile;
+ private String machineFileNameWithoutFileExtension;
+ // 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.");
@@ -109,39 +113,22 @@ public class TLC4B {
System.err.println(e.getMessage());
throw e;
}
- //System.out.println(tlc4b.tlaModule);
+ // System.out.println(tlc4b.tlaModule);
if (TLC4BGlobals.isRunTLC()) {
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
- tlc4b.path);
+ 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.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();
@@ -404,12 +405,12 @@ public class TLC4B {
throw new TLC4BIOException(e1.getMessage());
} catch (IOException e) {
throw new TLC4BIOException(e.getMessage());
- } finally{
+ } finally {
if (deleteOnExit && file.exists()) {
file.deleteOnExit();
}
}
-
+
}
}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 5de3b959dd1764cf41eafc281060aac7e9e43fb7..df9e4d620f4304d32a24cfd058a92e61485f1015 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -1,6 +1,7 @@
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();
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 911a8639c81c3b4da0d36868aec5fce449f0a275..7f8aa1ca2e5435db4cd9504f90de08861fc4b5ec 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -110,8 +110,7 @@ public class Translator {
UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
machineContext);
-
-
+
ConstantsEliminator constantsEliminator = new ConstantsEliminator(
machineContext);
constantsEliminator.start();
diff --git a/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
index 329d7290dcedc3cce236043284a5a4e15bf16ded..3a1c04053ef8d6f87528a980f132f740106ef637 100644
--- a/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
@@ -35,7 +35,7 @@ public class ConstantsEliminator extends DepthFirstAdapter {
private MachineContext machineContext;
private ValuesOfIdentifierFinder valuesOfConstantsFinder;
private final HashMap<Node, Integer> integerValueTable;
-
+
private LinkedHashMap<Node, Node> valueOfIdentifier;
public Node getValueOfConstant(Node con) {
diff --git a/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
index affde5aae4c9b149fcdf3a64558d0c3d1dc243e7..0e2a79e76f920de2d3b08bbc158953a577ed3606 100644
--- a/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
+++ b/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())){
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 7e4b87cdafe6320a9e6b47395483c7872fc8a5ff..d1e41ff0e70439af11f7f595377b8db76a566897 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/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>,
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index e9e826d9093945b3d2a682c72d695aa877cccbde..ca21d0d56a84d5a66b96e213931b79fb8abd4dd8 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/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;
diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
index 37e24e4e8d1270adde7aa635487860992805ecd2..e0c15b1a0bf5648e5f38f6d330ef37cf3de793ad 100644
--- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
+++ b/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);
+ }
+
}
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index a1556b7acb2697db747339451a224518e70342c7..1ba2fc635e07f0c731e788f538982fd2138a5f4a 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -28,11 +28,10 @@ public class Testing2 extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
- String[] a = new String[] {
- machine.getPath(), "-noLTL", "-wdcheck"};
- //TLC4B.main(a);
- TLC4B.test(a,false);
- //test(a);
+ String[] a = new String[] { machine.getPath() };
+ // TLC4B.main(a);
+ TLC4B.test(a, false);
+ // test(a);
}
@Config
diff --git a/src/test/resources/errors/EnumerationError/EnumerationError.cfg b/src/test/resources/errors/EnumerationError/EnumerationError.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..1a3b3e94e9baad9534a25dcc9f6307ef82c563d2
--- /dev/null
+++ b/src/test/resources/errors/EnumerationError/EnumerationError.cfg
@@ -0,0 +1,3 @@
+INIT Init
+NEXT Next
+INVARIANT Invariant1
diff --git a/src/test/resources/errors/EnumerationError/EnumerationError.tla b/src/test/resources/errors/EnumerationError/EnumerationError.tla
new file mode 100644
index 0000000000000000000000000000000000000000..8ba2af500c87cede4ffc0bd9040d0dcc50222313
--- /dev/null
+++ b/src/test/resources/errors/EnumerationError/EnumerationError.tla
@@ -0,0 +1,8 @@
+---- 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