From 8a5f7159d6bb74568c57aa7b7d40c12ecfdec027 Mon Sep 17 00:00:00 2001
From: hansene <dominik_hansen@web.de>
Date: Thu, 30 Jul 2015 20:53:21 +0200
Subject: [PATCH] Adapted the translator to the new parser version
---
build.gradle | 7 +-
src/main/java/de/tlc4b/MP.java | 48 +++++++
src/main/java/de/tlc4b/TLC4B.java | 136 +++++++++---------
src/main/java/de/tlc4b/TLCRunner.java | 9 +-
src/main/java/de/tlc4b/Translator.java | 3 +-
.../tlc4b/analysis/PrecedenceCollector.java | 31 ++--
.../java/de/tlc4b/analysis/Typechecker.java | 15 +-
.../transformation/SeesEliminator.java | 1 -
.../SetComprehensionOptimizer.java | 1 -
.../typerestriction/TypeRestrictor.java | 9 +-
src/main/java/de/tlc4b/btypes/BType.java | 2 +-
src/main/java/de/tlc4b/btypes/BoolType.java | 2 +-
.../java/de/tlc4b/btypes/FunctionType.java | 6 +-
.../tlc4b/btypes/IntegerOrSetOfPairType.java | 2 +-
.../de/tlc4b/btypes/IntegerOrSetType.java | 2 +-
.../java/de/tlc4b/btypes/IntegerType.java | 2 +-
.../java/de/tlc4b/btypes/ModelValueType.java | 2 +-
src/main/java/de/tlc4b/btypes/PairType.java | 6 +-
src/main/java/de/tlc4b/btypes/SetType.java | 4 +-
src/main/java/de/tlc4b/btypes/StringType.java | 4 +-
src/main/java/de/tlc4b/btypes/StructType.java | 4 +-
.../java/de/tlc4b/btypes/UntypedType.java | 2 +-
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 25 +++-
src/main/java/de/tlc4b/tlc/TLCResults.java | 57 +++++---
src/main/java/de/tlc4b/util/StopWatch.java | 24 +++-
src/main/java/de/tlc4b/util/UtilMethods.java | 20 ++-
.../tlc4b/typechecking/TestTypechecker.java | 2 +-
src/test/java/de/tlc4b/util/TestUtil.java | 24 ++--
src/test/java/testing/CompoundScopeTest.java | 66 ---------
src/test/java/testing/CompoundTest.java | 40 ------
30 files changed, 284 insertions(+), 272 deletions(-)
create mode 100644 src/main/java/de/tlc4b/MP.java
delete mode 100644 src/test/java/testing/CompoundScopeTest.java
delete mode 100644 src/test/java/testing/CompoundTest.java
diff --git a/build.gradle b/build.gradle
index 048c586..27ec8e8 100644
--- a/build.gradle
+++ b/build.gradle
@@ -7,8 +7,6 @@ apply plugin: 'findbugs'
project.version = '1.0.0-SNAPSHOT'
project.group = 'de.prob'
-sourceCompatibility = 1.5
-
repositories {
mavenCentral()
maven {
@@ -24,7 +22,7 @@ configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
-def parser_version = '2.4.36-SNAPSHOT'
+def parser_version = '2.5.0-SNAPSHOT'
dependencies {
//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
@@ -37,8 +35,6 @@ dependencies {
//compile(group: 'de.prob', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
-
-
testCompile (group: 'junit', name: 'junit', version: '4.11')
testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.5-SNAPSHOT')
@@ -91,7 +87,6 @@ jar {
jar {
manifest {
attributes "Main-Class" : 'de.tlc4b.TLC4B'
- attributes "Class-Path": 'tlatools.jar'
}
}
diff --git a/src/main/java/de/tlc4b/MP.java b/src/main/java/de/tlc4b/MP.java
new file mode 100644
index 0000000..7ce4afd
--- /dev/null
+++ b/src/main/java/de/tlc4b/MP.java
@@ -0,0 +1,48 @@
+package de.tlc4b;
+
+import java.io.OutputStream;
+import java.io.PrintStream;
+
+public class MP {
+ private static PrintStream out = System.out;
+ private static PrintStream err = System.err;
+
+ private MP() {
+ }
+
+ public static void printlnErr(String errorMessage) {
+ err.print("Error: ");
+ err.println(errorMessage);
+ }
+
+ public static void println(String message) {
+ out.println(message);
+ }
+
+ public static void print(String message) {
+ out.print(message);
+ }
+
+ static class TLCOutputStream extends PrintStream {
+ static final PrintStream origOut = System.out;
+
+ public static void changeOutputStream() {
+ MP.TLCOutputStream tlcOutputStream = new TLCOutputStream(origOut);
+ System.setOut(tlcOutputStream);
+ }
+
+ public static void resetOutputStream() {
+ System.setOut(origOut);
+ }
+
+ public TLCOutputStream(OutputStream out) {
+ super(out, true);
+ }
+
+ @Override
+ public void print(String s) {
+ super.print("TLC: " + s);
+ }
+ }
+
+}
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 134a48e..7a57201 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -21,6 +21,8 @@ import de.tlc4b.exceptions.TranslationException;
import de.tlc4b.tlc.TLCOutputInfo;
import de.tlc4b.tlc.TLCResults;
import de.tlc4b.util.StopWatch;
+import static de.tlc4b.util.StopWatch.Watches.*;
+import static de.tlc4b.MP.*;
public class TLC4B {
@@ -45,32 +47,33 @@ public class TLC4B {
try {
tlc4b.process(args);
} catch (BException e) {
- System.err.println("***** Parsing Error *****");
- System.err.println(e.getMessage());
+ printlnErr("***** Parsing Error *****");
+ printlnErr(e.getMessage());
return;
} catch (TLC4BException e) {
- System.err.println(e.getMessage());
- System.out.println("Model checking time: 0 sec");
- System.out.println("Result: " + e.getError());
+ printlnErr(e.getMessage());
+ println("Model checking time: 0 sec");
+ println("Result: " + e.getError());
return;
} catch (IOException e) {
- System.err.println(e.getMessage());
- System.out.println("Model checking time: 0 sec");
- System.out.println("Result: " + "I/O Error");
+ printlnErr(e.getMessage());
+ println("Model checking time: 0 sec");
+ println("Result: " + "I/O Error");
}
if (TLC4BGlobals.isRunTLC()) {
try {
+
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
tlc4b.buildDir);
+
TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
tlc4b.printResults(results, TLC4BGlobals.isCreateTraceFile());
System.exit(0);
} catch (NoClassDefFoundError e) {
- System.err
- .println("Can not find TLC. The tlatools.jar must be included in the classpath.");
+ printlnErr("Can not find TLC. The tlatools.jar must be included in the classpath.");
}
}
@@ -80,46 +83,42 @@ public class TLC4B {
private void printResults(TLCResults results, boolean createTraceFile) {
printOperationsCount(results);
// options
- System.out.println("Used Options");
- System.out.println("| Number of workers: " + TLC4BGlobals.getWorkers());
- System.out.println("| Invariants check: " + TLC4BGlobals.isInvariant());
- System.out.println("| Deadlock check: "
- + TLC4BGlobals.isDeadlockCheck());
- System.out.println("| Assertion check: " + TLC4BGlobals.isAssertion());
- System.out.println("| Find Goal check: " + TLC4BGlobals.isGOAL());
- System.out
- .println("| LTL formulas check: " + TLC4BGlobals.isCheckLTL());
- System.out.println("| Partial invariant evaluation: "
+ println("Used Options");
+ println("| Number of workers: " + TLC4BGlobals.getWorkers());
+ println("| Invariants check: " + TLC4BGlobals.isInvariant());
+ println("| Deadlock check: " + TLC4BGlobals.isDeadlockCheck());
+ println("| Assertion check: " + TLC4BGlobals.isAssertion());
+ println("| Find Goal check: " + TLC4BGlobals.isGOAL());
+ println("| LTL formulas check: " + TLC4BGlobals.isCheckLTL());
+ println("| Partial invariant evaluation: "
+ TLC4BGlobals.isPartialInvariantEvaluation());
- System.out.println("| Lazy constants setup: "
+ println("| Lazy constants setup: "
+ !TLC4BGlobals.isForceTLCToEvalConstants());
- System.out.println("| Agressive well-definedness check: "
+ println("| Agressive well-definedness check: "
+ TLC4BGlobals.checkWelldefinedness());
- System.out.println("| Prob constant setup: "
- + TLC4BGlobals.isProBconstantsSetup());
- System.out.println("| Symmetry reduction: "
- + TLC4BGlobals.useSymmetry());
- System.out.print("| MIN Int: " + TLC4BGlobals.getMIN_INT());
- System.out.print(" | MAX Int: " + TLC4BGlobals.getMAX_INT());
- System.out.println(" | Standard deferret set size: "
+ println("| Prob constant setup: " + TLC4BGlobals.isProBconstantsSetup());
+ println("| Symmetry reduction: " + TLC4BGlobals.useSymmetry());
+ println("| MIN Int: " + TLC4BGlobals.getMIN_INT());
+ println("| MAX Int: " + TLC4BGlobals.getMAX_INT());
+ println("| Standard deferret set size: "
+ TLC4BGlobals.getDEFERRED_SET_SIZE());
- System.out.println("--------------------------------");
- System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
+ println("--------------------------------");
+ println("Parsing time: " + StopWatch.getRunTime(PARSING_TIME) + " ms");
+ println("Translation time: " + StopWatch.getRunTime(TRANSLATION_TIME)
+ " ms");
- System.out.println("Translation time: "
- + StopWatch.getRunTime("Translation") + " ms");
- System.out.println("Model checking time: "
- + results.getModelCheckingTime() + " sec");
- // System.out.println("Number of workers: " +
+ println("Model checking time: " + results.getModelCheckingTime()
+ + " sec");
+ // MP.printMessage("Number of workers: " +
// TLCGlobals.getNumWorkers());
- System.out.println("States analysed: "
- + results.getNumberOfDistinctStates());
- System.out.println("Transitions fired: "
- + results.getNumberOfTransitions());
- System.out.println("Result: " + results.getResultString());
+ if (results.getViolatedAssertions().size() > 0) {
+ println("Violated assertions: " + results.getViolatedAssertions());
+ }
+ println("States analysed: " + results.getNumberOfDistinctStates());
+ println("Transitions fired: " + results.getNumberOfTransitions());
+ println("Result: " + results.getResultString());
String violatedDefinition = results.getViolatedDefinition();
if (violatedDefinition != null) {
- System.out.print("Violated Definition: " + violatedDefinition);
+ println("Violated Definition: " + violatedDefinition);
}
if (results.hasTrace() && createTraceFile) {
@@ -129,7 +128,7 @@ public class TLC4B {
File traceFile = createFile(mainfile.getParentFile(),
tracefileName, trace, false);
if (traceFile != null) {
- System.out.println("Trace file '" + traceFile.getAbsolutePath()
+ println("Trace file '" + traceFile.getAbsolutePath()
+ "' created.");
}
}
@@ -140,21 +139,21 @@ public class TLC4B {
LinkedHashMap<String, Long> operationCount = results
.getOperationCount();
if (TLC4BGlobals.isPrintCoverage() && operationCount != null) {
- System.out.println("---------- Coverage statistics ----------");
+ println("---------- Coverage statistics ----------");
for (Entry<String, Long> entry : operationCount.entrySet()) {
String key = entry.getKey();
String value = entry.getValue().toString();
- System.out.println(key + ": " + value);
+ println(key + ": " + value);
}
- System.out
- .println("---------- End of coverage statistics ----------");
+ println("---------- End of coverage statistics ----------");
}
}
public static void test(String[] args, boolean deleteFiles)
throws Exception {
- System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
+ System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up
+ // windows
TLC4BGlobals.resetGlobals();
TLC4BGlobals.setDeleteOnExit(deleteFiles);
TLC4BGlobals.setCreateTraceFile(false);
@@ -165,16 +164,17 @@ public class TLC4B {
tlc4b.process(args);
} catch (Exception e) {
e.printStackTrace();
- System.err.println(e.getMessage());
+ printlnErr(e.getMessage());
throw e;
}
if (TLC4BGlobals.isRunTLC()) {
+ MP.TLCOutputStream.changeOutputStream();
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
tlc4b.buildDir);
-
+ MP.TLCOutputStream.resetOutputStream();
+ ;
TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
-
tlc4b.printResults(results, false);
System.exit(0);
@@ -278,30 +278,33 @@ public class TLC4B {
public void process(String[] args) throws IOException, BException {
handleParameter(args);
- System.out.print("Arguments: ");
+ MP.print("Arguments: ");
for (int i = 0; i < args.length; i++) {
String string = args[i];
- System.out.print(string);
- System.out.print(" ");
+ MP.print(string);
+ MP.print(" ");
}
- System.out.println();
+ println("");
handleMainFileName();
if (TLC4BGlobals.isTranslate()) {
- StopWatch.start("Parsing");
- System.out.println("Parsing...");
+ StopWatch.start(PARSING_TIME);
+ MP.print("Parsing... ");
translator = new Translator(machineFileNameWithoutFileExtension,
mainfile, this.ltlFormula, this.constantsSetup);
- StopWatch.stop("Parsing");
-
- StopWatch.start("Translation");
- System.out.println("Translating...");
+ StopWatch.stop(PARSING_TIME);
+ println("(" + StopWatch.getRunTimeAsString(PARSING_TIME) + "ms)");
+
+ StopWatch.start(TRANSLATION_TIME);
+ MP.print("Translating... ");
translator.translate();
this.tlaModule = translator.getModuleString();
this.config = translator.getConfigString();
this.tlcOutputInfo = translator.getTLCOutputInfo();
+ StopWatch.stop(TRANSLATION_TIME);
+ println("(" + StopWatch.getRunTimeAsString(TRANSLATION_TIME)
+ + "ms)");
createFiles();
- StopWatch.stop("Translation");
}
}
@@ -345,7 +348,7 @@ public class TLC4B {
machineFileNameWithoutFileExtension + ".tla", tlaModule,
TLC4BGlobals.isDeleteOnExit());
if (moduleFile != null) {
- System.out.println("TLA+ module '" + moduleFile.getAbsolutePath()
+ println("TLA+ module '" + moduleFile.getAbsolutePath()
+ "' created.");
}
@@ -353,8 +356,8 @@ public class TLC4B {
machineFileNameWithoutFileExtension + ".cfg", config,
TLC4BGlobals.isDeleteOnExit());
if (configFile != null) {
- System.out.println("Configuration file '"
- + configFile.getAbsolutePath() + "' created.");
+ println("Configuration file '" + configFile.getAbsolutePath()
+ + "' created.");
}
createStandardModules();
}
@@ -400,8 +403,7 @@ public class TLC4B {
while ((read = is.read(bytes)) != -1) {
fos.write(bytes, 0, read);
}
- System.out.println("Standard module '" + file.getName()
- + "' created.");
+ println("Standard module '" + file.getName() + "' created.");
} catch (IOException e) {
throw new TLC4BIOException(e.getMessage());
} finally {
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 48aec1e..3087b77 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -90,9 +90,8 @@ public class TLCRunner {
}
public static void runTLC(String machineName, File path) {
-
- System.out.println("--------------------------------");
-
+ MP.println("--------------------------------");
+ MP.TLCOutputStream.changeOutputStream();
ToolIO.setMode(ToolIO.SYSTEM);
ArrayList<String> list = new ArrayList<String>();
@@ -131,10 +130,10 @@ public class TLCRunner {
}
// System.setOut(systemOut);
// ArrayList<String> messages = btlcStream.getArrayList();
-
- System.out.println("--------------------------------");
closeThreads();
// return messages;
+ MP.TLCOutputStream.resetOutputStream();
+ MP.println("--------------------------------");
}
private static void closeThreads() {
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 87bb1cc..6900ba9 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -84,8 +84,7 @@ public class Translator {
// machine
final RecursiveMachineLoader rml = new RecursiveMachineLoader(
machineFile.getParent(), parser.getContentProvider());
- rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(),
- parser.getPragmas());
+ rml.loadAllMachines(machineFile, start, null, parser.getDefinitions());
parsedMachines = rml.getParsedMachines();
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index e495133..63389ad 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -6,6 +6,7 @@ import java.util.Hashtable;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
import de.be4.classicalb.core.parser.node.ADomainExpression;
+import de.be4.classicalb.core.parser.node.ALabelPredicate;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.Node;
@@ -56,21 +57,18 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("AUnionExpression", 8, 8, true);
put("ASetSubtractionExpression", 8, 8, false);
put("AIntervalExpression", 9, 9, true);
-
+
put("ACartesianProductExpression", 8, 13, false);
-
+
put("AAddExpression", 10, 10, true);
-
-
+
put("AModuloExpression", 10, 11, true);
put("AUnaryMinusExpression", 12, 12, false);
put("AConcatExpression", 13, 13, true);
put("ADivExpression", 13, 13, false);
-
-
+
put("AFunctionExpression", 20, 20, false);
-
-
+
}
private Precedence getPrecedence(Node node) {
@@ -113,13 +111,18 @@ public class PrecedenceCollector extends DepthFirstAdapter {
@Override
public void defaultIn(final Node node) {
+ Node parent = node.parent();
Precedence p = getPrecedence(node);
if (p != null) {
precedenceTable.put(node, p);
+ if (parent instanceof ALabelPredicate) {
+ parent = parent.parent();
+ }
- if (node.parent() != null) {
- Precedence parent = precedenceTable.get(node.parent());
- if (Precedence.makeBrackets(p, parent)) {
+ if (parent != null) {
+ Precedence parentPrecedence = precedenceTable
+ .get(node.parent());
+ if (Precedence.makeBrackets(p, parentPrecedence)) {
brackets.add(node);
}
}
@@ -154,16 +157,16 @@ public class PrecedenceCollector extends DepthFirstAdapter {
brackets.add(node);
}
}
-
+
@Override
- public void inADomainExpression(ADomainExpression node) {
+ public void inADomainExpression(ADomainExpression node) {
BType type = typechecker.getType(node.getExpression());
Precedence p;
if (type instanceof FunctionType) {
// Function
p = new Precedence("ADomainExpression", 9, 9, false);
-
+
precedenceTable.put(node, p);
Precedence parent = precedenceTable.get(node.parent());
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index fbd148e..1e438a3 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -118,7 +118,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
public BType getType(Node node) {
- return types.get(node);
+ BType res = types.get(node);
+ if (res == null) {
+ new TypeErrorException("Node '" + node + "' has not type.\n"
+ + node.getStartPos());
+ }
+ return res;
}
@Override
@@ -445,7 +450,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
expected.unify(found, this);
} catch (UnificationException e) {
throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "' at identifier " + node + "\n"
+ + "' , found '" + found + "' at identifier " + name + "\n"
+ node.getStartPos());
}
}
@@ -1127,6 +1132,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
+ System.out.println(node.parent().getClass());
throw new TypeErrorException("Excepted '" + getType(node)
+ "' , found 'BOOL' in ' <=> '");
}
@@ -2478,4 +2484,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
+ public void inALabelPredicate(ALabelPredicate node) {
+ BType type = getType(node);
+ setType(node.getPredicate(), type);
+ }
+
}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
index 2e755f3..22194e8 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
@@ -79,7 +79,6 @@ public class SeesEliminator extends DepthFirstAdapter {
PParseUnit pParseUnit = main.getPParseUnit();
AAbstractMachineParseUnit machineParseUnit = (AAbstractMachineParseUnit) pParseUnit;
- System.out.println(machineParseUnit.getHeader());
for (PMachineClause machineClause : machineParseUnit
.getMachineClauses()) {
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
index f311207..2524422 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedList;
-import java.util.List;
import java.util.Set;
import de.be4.classicalb.core.parser.Utils;
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 22c1f09..deaf979 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -52,6 +52,7 @@ import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType;
import de.tlc4b.exceptions.NotSupportedException;
import de.tlc4b.ltl.LTLFormulaVisitor;
+import de.tlc4b.util.UtilMethods;
public class TypeRestrictor extends DepthFirstAdapter {
@@ -552,17 +553,19 @@ public class TypeRestrictor extends DepthFirstAdapter {
conType = typechecker.getType(machineContext
.getReferenceNode(e));
}
- if (conType.containsIntegerType()
+ if (conType.containsInfiniteType()
&& !(e.parent() instanceof ALambdaExpression)
&& !(e.parent() instanceof AComprehensionSetExpression)) {
AIdentifierExpression id = (AIdentifierExpression) e;
String localVariableName = Utils.getIdentifierAsString(id
.getIdentifier());
throw new NotSupportedException(
- "Unable to restrict the type of the variable '"
+ "Unable to restrict the type '"
+ + conType
+ + "' of identifier '"
+ localVariableName
+ "' to a finite set. TLC is not able to handle infinite sets.\n"
- + e.getStartPos());
+ + UtilMethods.getPositionAsString(e));
}
tree = conType.createSyntaxTreeNode(typechecker);
diff --git a/src/main/java/de/tlc4b/btypes/BType.java b/src/main/java/de/tlc4b/btypes/BType.java
index 01147cf..ed800fc 100644
--- a/src/main/java/de/tlc4b/btypes/BType.java
+++ b/src/main/java/de/tlc4b/btypes/BType.java
@@ -8,6 +8,6 @@ public interface BType extends ITypeConstants{
public boolean isUntyped();
public boolean compare(BType other);
public String getTlaType();
- public boolean containsIntegerType();
+ public boolean containsInfiniteType();
public PExpression createSyntaxTreeNode(Typechecker typechecker);
}
diff --git a/src/main/java/de/tlc4b/btypes/BoolType.java b/src/main/java/de/tlc4b/btypes/BoolType.java
index 4206654..ef7bb6b 100644
--- a/src/main/java/de/tlc4b/btypes/BoolType.java
+++ b/src/main/java/de/tlc4b/btypes/BoolType.java
@@ -47,7 +47,7 @@ public class BoolType implements BType {
return "BOOLEAN";
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
return false;
}
diff --git a/src/main/java/de/tlc4b/btypes/FunctionType.java b/src/main/java/de/tlc4b/btypes/FunctionType.java
index cb16e85..64e4348 100644
--- a/src/main/java/de/tlc4b/btypes/FunctionType.java
+++ b/src/main/java/de/tlc4b/btypes/FunctionType.java
@@ -123,9 +123,9 @@ public class FunctionType extends AbstractHasFollowers {
return "[" + domain.getTlaType() + " -> " + range.getTlaType() + "]";
}
- public boolean containsIntegerType() {
- return this.domain.containsIntegerType()
- || this.range.containsIntegerType();
+ public boolean containsInfiniteType() {
+ return this.domain.containsInfiniteType()
+ || this.range.containsInfiniteType();
}
public PExpression createSyntaxTreeNode(Typechecker typechecker) {
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
index a8d378e..7de577d 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
@@ -223,7 +223,7 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
return null;
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
return false;
}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
index 77765c9..82857bb 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
@@ -59,7 +59,7 @@ public class IntegerOrSetType extends AbstractHasFollowers {
return null;
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
return false;
}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerType.java b/src/main/java/de/tlc4b/btypes/IntegerType.java
index 70cbe3c..fe3d951 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerType.java
@@ -59,7 +59,7 @@ public class IntegerType implements BType {
return false;
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
return true;
}
diff --git a/src/main/java/de/tlc4b/btypes/ModelValueType.java b/src/main/java/de/tlc4b/btypes/ModelValueType.java
index 0be4a04..4017d48 100644
--- a/src/main/java/de/tlc4b/btypes/ModelValueType.java
+++ b/src/main/java/de/tlc4b/btypes/ModelValueType.java
@@ -61,7 +61,7 @@ public class ModelValueType implements BType {
return name;
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
return false;
}
diff --git a/src/main/java/de/tlc4b/btypes/PairType.java b/src/main/java/de/tlc4b/btypes/PairType.java
index 4d7d141..1e9057d 100644
--- a/src/main/java/de/tlc4b/btypes/PairType.java
+++ b/src/main/java/de/tlc4b/btypes/PairType.java
@@ -129,9 +129,9 @@ public class PairType extends AbstractHasFollowers {
return res;
}
- public boolean containsIntegerType() {
- return this.first.containsIntegerType()
- || this.second.containsIntegerType();
+ public boolean containsInfiniteType() {
+ return this.first.containsInfiniteType()
+ || this.second.containsInfiniteType();
}
public PExpression createSyntaxTreeNode(Typechecker typechecker) {
diff --git a/src/main/java/de/tlc4b/btypes/SetType.java b/src/main/java/de/tlc4b/btypes/SetType.java
index cc3d361..8137156 100644
--- a/src/main/java/de/tlc4b/btypes/SetType.java
+++ b/src/main/java/de/tlc4b/btypes/SetType.java
@@ -102,8 +102,8 @@ public class SetType extends AbstractHasFollowers {
return "SUBSET(" + subtype.getTlaType() + ")";
}
- public boolean containsIntegerType() {
- return this.subtype.containsIntegerType();
+ public boolean containsInfiniteType() {
+ return this.subtype.containsInfiniteType();
}
public PExpression createSyntaxTreeNode(Typechecker typechecker) {
diff --git a/src/main/java/de/tlc4b/btypes/StringType.java b/src/main/java/de/tlc4b/btypes/StringType.java
index ed5c511..4771569 100644
--- a/src/main/java/de/tlc4b/btypes/StringType.java
+++ b/src/main/java/de/tlc4b/btypes/StringType.java
@@ -52,8 +52,8 @@ public class StringType implements BType {
return "STRING";
}
- public boolean containsIntegerType() {
- return false;
+ public boolean containsInfiniteType() {
+ return true;
}
public PExpression createSyntaxTreeNode(Typechecker typechecker) {
diff --git a/src/main/java/de/tlc4b/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
index 1466385..30fc041 100644
--- a/src/main/java/de/tlc4b/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -210,10 +210,10 @@ public class StructType extends AbstractHasFollowers {
return res.toString();
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
Iterator<BType> iterator = this.types.values().iterator();
while (iterator.hasNext()) {
- if (iterator.next().containsIntegerType())
+ if (iterator.next().containsInfiniteType())
return true;
}
return false;
diff --git a/src/main/java/de/tlc4b/btypes/UntypedType.java b/src/main/java/de/tlc4b/btypes/UntypedType.java
index edf9e04..a24e490 100644
--- a/src/main/java/de/tlc4b/btypes/UntypedType.java
+++ b/src/main/java/de/tlc4b/btypes/UntypedType.java
@@ -28,7 +28,7 @@ public class UntypedType extends AbstractHasFollowers {
return this.toString();
}
- public boolean containsIntegerType() {
+ public boolean containsInfiniteType() {
return false;
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index cf6736b..54287c2 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -452,12 +452,31 @@ public class TLAPrinter extends DepthFirstAdapter {
if (assertions.size() == 0)
return;
for (int i = 0; i < assertions.size(); i++) {
+ Node assertion = assertions.get(i);
+ String name = null;
+ if (assertion instanceof ALabelPredicate) {
+ ALabelPredicate label = (ALabelPredicate) assertion;
+ name = label.getName().getText();
+ }
+
if (tlaModule.hasInitPredicate()) {
- moduleStringAppend("Assertion" + (i + 1) + " == ");
+ if (name != null) {
+ moduleStringAppend(name);
+ moduleStringAppend(" == ");
+ } else {
+ moduleStringAppend(name);
+ moduleStringAppend("Assertion" + (i + 1) + " == ");
+ }
} else {
- moduleStringAppend("ASSUME Assertion" + (i + 1) + " == ");
+ moduleStringAppend("ASSUME ");
+ if (name != null) {
+ moduleStringAppend(name);
+ moduleStringAppend(" == ");
+ } else {
+ moduleStringAppend("Assertion" + (i + 1) + " == ");
+ }
}
- assertions.get(i).apply(this);
+ assertion.apply(this);
moduleStringAppend("\n");
}
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index d055a7e..e8e6bee 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -34,6 +34,7 @@ public class TLCResults implements ToolGlobals {
private Date startTime;
private Date endTime;
private LinkedHashMap<String, Long> operationsCount;
+ private ArrayList<String> violatedAssertions = new ArrayList<String>();
private int lengthOfTrace;
private String traceString;
@@ -72,6 +73,10 @@ public class TLCResults implements ToolGlobals {
return violatedDefinition;
}
+ public ArrayList<String> getViolatedAssertions(){
+ return this.violatedAssertions;
+ }
+
public int getNumberOfTransitions() {
return numberOfTransitions;
}
@@ -286,31 +291,34 @@ public class TLCResults implements ToolGlobals {
case EC.TLC_ASSUMPTION_FALSE:
// get the violated assumption expr from the OutputCollector
- ExprNode violatedAssumptionExpr = OutputCollector
- .getViolatedAssumption();
- if (violatedAssumptionExpr != null) {
+ ArrayList<ExprNode> violatedAssumptions = OutputCollector
+ .getViolatedAssumptions();
+ System.out.println(violatedAssumptions.size());
+ if (violatedAssumptions.size() > 0) {
// try to find the assume node contain the expr in order to get
// the name of the assumption
- ModuleNode moduleNode = OutputCollector.getModuleNode();
- AssumeNode[] assumptions = moduleNode.getAssumptions();
- for (AssumeNode assumeNode : assumptions) {
- if (assumeNode.getAssume() == violatedAssumptionExpr) {
- ThmOrAssumpDefNode def = assumeNode.getDef();
- // if the assumption is a named assumption, def is
- // unequal null
- // All B assertions are represented as named assumptions
- // in the TLA module
- if (def != null
- && def.getName().toString()
- .startsWith("Assertion")) {
- tlcResult = TLCResult.AssertionError;
- return;
+
+ for (ExprNode exprNode : violatedAssumptions) {
+ AssumeNode assumeNode = findAssumeNode(exprNode);
+ ThmOrAssumpDefNode def = assumeNode.getDef();
+ // if the assumption is a named assumption, def is
+ // unequal null
+ // All B assertions are represented as named assumptions
+ // in the TLA module
+ if (def != null) {
+ String assertionName = def.getName().toString();
+ if(!violatedAssertions.contains(assertionName)){
+ this.violatedAssertions.add(assertionName);
}
+ tlcResult = TLCResult.AssertionError;
}
+
}
}
- // otherwise, it is normal properties error
- tlcResult = TLCResult.PropertiesError;
+ if(tlcResult!= null){
+ // otherwise, it is normal properties error
+ tlcResult = TLCResult.PropertiesError;
+ }
break;
case EC.TLC_TEMPORAL_PROPERTY_VIOLATED:
@@ -340,6 +348,17 @@ public class TLCResults implements ToolGlobals {
}
}
+ private AssumeNode findAssumeNode(ExprNode exprNode) {
+ ModuleNode moduleNode = OutputCollector.getModuleNode();
+ AssumeNode[] assumptions = moduleNode.getAssumptions();
+ for (AssumeNode assumeNode : assumptions) {
+ if (assumeNode.getAssume() == exprNode) {
+ return assumeNode;
+ }
+ }
+ return null;
+ }
+
private TLCResult evaluatingParameter(String[] params) {
for (int i = 0; i < params.length; i++) {
String s = params[i];
diff --git a/src/main/java/de/tlc4b/util/StopWatch.java b/src/main/java/de/tlc4b/util/StopWatch.java
index a0a719b..d93065f 100644
--- a/src/main/java/de/tlc4b/util/StopWatch.java
+++ b/src/main/java/de/tlc4b/util/StopWatch.java
@@ -3,21 +3,31 @@ package de.tlc4b.util;
import java.util.Hashtable;
public class StopWatch {
- private static final Hashtable<String, Long> startTime = new Hashtable<String, Long>();
- private static final Hashtable<String, Long> runTime = new Hashtable<String, Long>();
- public static void start(String id) {
- startTime.put(id, System.currentTimeMillis());
- }
- public static long stop(String id) {
+ private static final Hashtable<Watches, Long> startTime = new Hashtable<Watches, Long>();
+ private static final Hashtable<Watches, Long> runTime = new Hashtable<Watches, Long>();
+
+ public enum Watches{
+ PARSING_TIME, TRANSLATION_TIME, TLC_TIME, OVERALL_TIME
+ }
+
+ public static void start(Watches watch){
+ startTime.put(watch, System.currentTimeMillis());
+ }
+
+ public static long stop(Watches id) {
long stopTime = System.currentTimeMillis()
- startTime.remove(id);
runTime.put(id, stopTime);
return stopTime;
}
- public static long getRunTime(String id){
+ public static long getRunTime(Watches id){
return runTime.get(id);
}
+
+ public static String getRunTimeAsString(Watches id){
+ return runTime.get(id).toString();
+ }
}
\ No newline at end of file
diff --git a/src/main/java/de/tlc4b/util/UtilMethods.java b/src/main/java/de/tlc4b/util/UtilMethods.java
index 822c469..3ff3fe4 100644
--- a/src/main/java/de/tlc4b/util/UtilMethods.java
+++ b/src/main/java/de/tlc4b/util/UtilMethods.java
@@ -3,7 +3,9 @@ package de.tlc4b.util;
import java.util.ArrayList;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.hhu.stups.sablecc.patch.SourcePosition;
public class UtilMethods {
@@ -14,5 +16,21 @@ public class UtilMethods {
AIdentifierExpression id = new AIdentifierExpression(idList);
return id;
}
-
+
+ public static String getPositionAsString(Node node) {
+ StringBuilder sb = new StringBuilder();
+ SourcePosition startPos = node.getStartPos();
+ SourcePosition endPos = node.getEndPos();
+ if (startPos == null) {
+ sb.append("### Unknown position.");
+ } else {
+ sb.append("### Line ");
+ sb.append(startPos.getLine());
+ sb.append(", Column ");
+ sb.append(endPos.getPos());
+ }
+
+ return sb.toString();
+ }
+
}
diff --git a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
index 1d3bcd8..484487a 100644
--- a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
+++ b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
@@ -25,7 +25,7 @@ public class TestTypechecker {
Start start = parser.parse(machine, false);
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- System.out.println(ast2String2.toString());
+ //System.out.println(ast2String2.toString());
MachineContext c = new MachineContext(null, start, null, null);
Typechecker t = new Typechecker(c);
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 98c7291..831ec92 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -31,15 +31,15 @@ public class TestUtil {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
-
- //TODO create standard modules BBuildins
-
+
+ // TODO create standard modules BBuildins
String moduleName = b2tlaTranslator.getMachineName();
- String str1 = translateTLA2B(moduleName,
- b2tlaTranslator.getModuleString());
+ String str1 = de.tla2bAst.Translator.translateModuleString(moduleName,
+ b2tlaTranslator.getModuleString(), null);
- String str2 = translateTLA2B(moduleName, expectedModule);
+ String str2 = de.tla2bAst.Translator.translateModuleString(moduleName,
+ expectedModule, null);
// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, b2tlaTranslator.getModuleString(), null);
// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
@@ -53,8 +53,7 @@ public class TestUtil {
// assertEquals(sb2.toString(), sb1.toString());
}
- public static String translateTLA2B(String moduleName, String tlaString)
- throws TLA2BException {
+ public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName,
tlaString, null);
}
@@ -65,7 +64,6 @@ public class TestUtil {
tlaString, configString);
}
-
public static void compareLTLFormula(String expected, String machine,
String ltlFormula) throws Exception {
Translator b2tlaTranslator = new Translator(machine, ltlFormula);
@@ -121,12 +119,8 @@ public class TestUtil {
System.out.println(b2tlaTranslator.getModuleString());
System.out.println(b2tlaTranslator.getConfigString());
-
- //TODO include config file in back translation from TLA+ to B
-
-
-
-
+ // TODO include config file in back translation from TLA+ to B
+
// String name = b2tlaTranslator.getMachineName();
// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, b2tlaTranslator.getModuleString(),
diff --git a/src/test/java/testing/CompoundScopeTest.java b/src/test/java/testing/CompoundScopeTest.java
deleted file mode 100644
index 89bf8f0..0000000
--- a/src/test/java/testing/CompoundScopeTest.java
+++ /dev/null
@@ -1,66 +0,0 @@
-package testing;
-
-import java.io.File;
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.List;
-import java.util.Map;
-
-import org.junit.Ignore;
-import org.junit.Test;
-
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
-import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Start;
-import de.tlc4b.util.Ast2String;
-
-public class CompoundScopeTest {
-
- @Ignore
- @Test
- public void test() throws BException, IOException {
- String filename = "src/test/resources/M1.mch";
- checkScope(filename);
- }
-
- public void checkScope(String filename) throws BException, IOException {
-
- final File machineFile = new File(filename);
-
- BParser parser = new BParser(filename);
- Start tree = parser.parseFile(machineFile, false);
-
- RecursiveMachineLoader r = new RecursiveMachineLoader(
- machineFile.getParent(), parser.getContentProvider());
-
- List<Pragma> pragmas = new ArrayList<Pragma>();
- pragmas.addAll(parser.getPragmas());
- r.loadAllMachines(machineFile, tree, parser.getSourcePositions(),
- parser.getDefinitions(), pragmas);
- // r.printAsProlog(new PrintWriter(System.out), false);
-
- Map<String, Start> map = r.getParsedMachines();
- ArrayList<String> list = new ArrayList<String>(map.keySet());
-
- // Hashtable<String, MachineContext> machineContextsTable = new
- // Hashtable<String, MachineContext>();
- // Hashtable<String, Typechecker> typecheckerTable = new
- // Hashtable<String, Typechecker>();
- for (int i = 0; i < list.size(); i++) {
- String name = list.get(i);
- // System.out.println(name);
- Start start = map.get(name);
- final Ast2String ast2String2 = new Ast2String();
- start.apply(ast2String2);
- System.out.println(ast2String2.toString());
-
- // MachineContext c = new MachineContext(start,
- // machineContextsTable);
- // machineContextsTable.put(name, c);
-
- }
-
- }
-}
diff --git a/src/test/java/testing/CompoundTest.java b/src/test/java/testing/CompoundTest.java
deleted file mode 100644
index 769fff7..0000000
--- a/src/test/java/testing/CompoundTest.java
+++ /dev/null
@@ -1,40 +0,0 @@
-package testing;
-
-import java.io.File;
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.List;
-
-import org.junit.Test;
-
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
-import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Start;
-
-public class CompoundTest {
-
- @Test
- public void test() throws IOException, BException {
- String filename = "src/test/resources/compound/M1.mch";
- //final int dot = filename.lastIndexOf('.');
- final File machineFile = new File(filename);
- //final String probfilename = filename.substring(0, dot) + ".prob";
-
-
-
- BParser parser = new BParser(filename);
- Start tree = parser.parseFile(machineFile, false);
-
- RecursiveMachineLoader r = new RecursiveMachineLoader(machineFile.getParent(), parser.getContentProvider());
-
-
- List<Pragma> pragmas = new ArrayList<Pragma>();
- pragmas.addAll(parser.getPragmas());
- r.loadAllMachines(machineFile, tree, parser.getSourcePositions(), parser.getDefinitions(), pragmas);
-
- //r.printAsProlog(new PrintWriter(System.out), false);
- }
-
-}
--
GitLab