diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 3424581e381415f4d7f66be5d7d898ad894a0f59..3872e5eb48979ebe95eba849bc19d78dc5223a4f 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -15,6 +15,8 @@ public class TLC4BGlobals {
private static boolean partialInvariantEvaluation;
private static boolean useSymmetry;
private static boolean printCoverage;
+
+ private static boolean checkOnlyMainAssertions;
private static boolean deleteFilesOnExit;
@@ -52,6 +54,7 @@ public class TLC4BGlobals {
useSymmetry = false;
printCoverage = false;
forceTLCToEvalConstants = false;
+ checkOnlyMainAssertions = true;
proBconstantsSetup = false;
@@ -257,5 +260,9 @@ public class TLC4BGlobals {
public static boolean isPrintCoverage() {
return printCoverage;
}
+
+ public static boolean isCheckOnlyMainAssertions(){
+ return checkOnlyMainAssertions;
+ }
}
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 6900ba98f1162698e343df1a1d4a39e4bba7e4c8..68c6286e2460f6494716615aecec723d72cc9e67 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -120,6 +120,7 @@ public class Translator {
new NotSupportedConstructs(start);
DefinitionsEliminator.eliminateDefinitions(start);
+ //TODO move set comprehension optimizer behind the type checker
SetComprehensionOptimizer.optimizeSetComprehensions(start);
MachineContext machineContext = new MachineContext(machineName, start,
@@ -132,7 +133,7 @@ public class Translator {
Typechecker typechecker = new Typechecker(machineContext);
UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
machineContext);
-
+
ConstantsEliminator constantsEliminator = new ConstantsEliminator(
machineContext);
constantsEliminator.start();
@@ -146,12 +147,14 @@ public class Translator {
TypeRestrictor typeRestrictor = new TypeRestrictor(start,
machineContext, typechecker);
-
+
PrecedenceCollector precedenceCollector = new PrecedenceCollector(
start, typechecker, machineContext, typeRestrictor);
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
machineContext);
+
+
Generator generator = new Generator(machineContext, typeRestrictor,
constantsEvaluator, deferredSetSizeCalculator, typechecker);
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index a8eeceecab5d18aca59f288fa77d66bfc2a690c0..b3f4cda30b9f1c6083d15b666b0ff6cf407b091c 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -107,7 +107,7 @@ import de.tlc4b.tla.TLAModule;
public class UsedStandardModules extends DepthFirstAdapter {
public static enum STANDARD_MODULES {
- Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations, ExternalFunctions
+ Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations, ExternalFunctions, Foo
}
private final static ArrayList<STANDARD_MODULES> modules = new ArrayList<UsedStandardModules.STANDARD_MODULES>();
@@ -167,8 +167,8 @@ public class UsedStandardModules extends DepthFirstAdapter {
return list;
}
- public HashSet<STANDARD_MODULES> getStandardModulesToBeCreated(){
- // dependencies of standard modules
+ public HashSet<STANDARD_MODULES> getStandardModulesToBeCreated() {
+ // dependencies of standard modules
HashSet<STANDARD_MODULES> res = new HashSet<STANDARD_MODULES>();
for (STANDARD_MODULES module : extendedStandardModules) {
switch (module) {
@@ -202,10 +202,11 @@ public class UsedStandardModules extends DepthFirstAdapter {
default:
break;
}
-
+
}
return res;
}
+
@Override
public void inAExpressionDefinitionDefinition(
AExpressionDefinitionDefinition node) {
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
index 22194e8fed6465e686329d355f7dfc8c5202458f..c90ba2108061750fc300fe64a73ca63a47401cb4 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
@@ -10,6 +10,7 @@ import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
+import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
@@ -20,7 +21,9 @@ import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PMachineClause;
import de.be4.classicalb.core.parser.node.PParseUnit;
+import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.TLC4BGlobals;
public class SeesEliminator extends DepthFirstAdapter {
@@ -52,13 +55,14 @@ public class SeesEliminator extends DepthFirstAdapter {
LinkedList<PExpression> machineNames = node.getMachineNames();
for (PExpression pExpression : machineNames) {
AIdentifierExpression id = (AIdentifierExpression) pExpression;
- String machineName = Utils.getIdentifierAsString(id
- .getIdentifier());
- if(!resolvedMachines.contains(machineName)){
+ String machineName = Utils
+ .getIdentifierAsString(id.getIdentifier());
+ if (!resolvedMachines.contains(machineName)) {
resolvedMachines.add(machineName);
Start start = parsedMachines.get(machineName);
DefinitionsEliminator.eliminateDefinitions(start);
- eliminateSeenMachinesRecursively(start, parsedMachines, resolvedMachines);
+ eliminateSeenMachinesRecursively(start, parsedMachines,
+ resolvedMachines);
new MachineClauseAdder(main, start);
if (node.parent() != null) {
node.replaceBy(null);
@@ -197,5 +201,35 @@ public class SeesEliminator extends DepthFirstAdapter {
}
}
+ public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
+ if (TLC4BGlobals.isCheckOnlyMainAssertions())
+ return;
+ AAssertionsMachineClause main = (AAssertionsMachineClause) machineClauseHashMap
+ .get(node.getClass());
+ if (main == null) {
+ additionalMachineClauseList.add(node);
+ } else {
+ ArrayList<PPredicate> old = new ArrayList<PPredicate>(
+ main.getPredicates());
+ ArrayList<PPredicate> newList = new ArrayList<PPredicate>();
+ for (PPredicate p : old) {
+ p.replaceBy(null); // delete parent
+ newList.add(p);
+ }
+ ArrayList<PPredicate> otherAssertions = new ArrayList<PPredicate>(
+ node.getPredicates());
+
+ for (PPredicate p : otherAssertions) {
+ if (p.parent() != null) {
+ p.replaceBy(null); // delete parent
+ }
+ newList.add(p);
+
+ }
+ main.setPredicates(newList);
+ }
+
+ }
+
}
}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
index 25244227b1b859a00d2ad66683222b9aa6cc8110..2aa937b98f315efbca0e6c767f1262b185033a83 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -146,9 +146,9 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
} else {
node.replaceBy(eventBcomprehension);
}
- // eventBcomprehension.apply(this);
+ eventBcomprehension.apply(this);
} else {
- // node.getPredicates().apply(this);
+ node.getPredicates().apply(this);
}
}
@@ -289,11 +289,11 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
}
}
}
-
+
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
String name = Utils.getIdentifierAsString(node.getIdentifier());
-
+ //todo the name is not a unique of the node
PExpression value = values.get(name);
if (value != null) {
node.replaceBy((PExpression) value.clone());
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 856f54ad76e94b1891ac33e793bbe6d5c1944bfa..d55e8f024fb92cb3d27be63806d45adfb574c2e0 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -458,29 +458,34 @@ public class TLAPrinter extends DepthFirstAdapter {
ALabelPredicate label = (ALabelPredicate) assertion;
name = label.getName().getText();
}
+
+ if(name == null){
+ name = "Assertion" + (i + 1);
+ }
+
if (tlaModule.hasInitPredicate()) {
- if (name != null) {
moduleStringAppend(name);
moduleStringAppend(" == ");
- } else {
- moduleStringAppend("Assertion" + (i + 1) + " == ");
- }
} else {
moduleStringAppend("ASSUME ");
- if (name != null) {
moduleStringAppend(name);
moduleStringAppend(" == ");
- } else {
- moduleStringAppend("Assertion" + (i + 1) + " == ");
- }
}
+ //assertionMode = true;
+ //assertionName = name;
+ //parameterCounter = 0;
assertion.apply(this);
+ //assertionMode = false;
moduleStringAppend("\n");
}
}
}
+ private static boolean assertionMode = false;
+ private static String assertionName = null;
+ private static Integer parameterCounter = 0;
+
private void printInit() {
ArrayList<Node> inits = this.tlaModule.getInitPredicates();
if (inits.size() == 0)
@@ -1267,19 +1272,76 @@ public class TLAPrinter extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
+ int start = parameterCounter;
+ int end = parameterCounter + copy.size();
+ parameterCounter = end + 1;
+ if (assertionMode) {
+
+ moduleStringAppend("(");
+ moduleStringAppend("TLCSet(");
+ moduleStringAppend(""+start);
+ moduleStringAppend(", TRUE) /\\ ");
+ for (int i = start; i < end; i++) {
+ moduleStringAppend("TLCSet(");
+ moduleStringAppend("" + (i + 1));
+ moduleStringAppend(", \"NULL\")");
+ moduleStringAppend(" /\\ ");
+ }
+ }
+
moduleStringAppend("\\A ");
for (int i = 0; i < copy.size(); i++) {
PExpression e = copy.get(i);
e.apply(this);
moduleStringAppend(" \\in ");
typeRestrictor.getRestrictedNode(e).apply(this);
- ;
if (i < copy.size() - 1) {
moduleStringAppend(", ");
}
}
moduleStringAppend(" : ");
- node.getImplication().apply(this);
+ if (assertionMode) {
+ int j = start;
+ for (int i = 0; i < copy.size(); i++) {
+ PExpression e = copy.get(i);
+ moduleStringAppend("TLCSet(");
+ moduleStringAppend("" + (i + 1));
+ moduleStringAppend(", ");
+ e.apply(this);
+ moduleStringAppend(")");
+ moduleStringAppend(" /\\ ");
+ j ++;
+ }
+
+ assertionMode = false;
+
+ moduleStringAppend(" IF ");
+ node.getImplication().apply(this);
+ moduleStringAppend(" THEN TRUE ");
+ moduleStringAppend(" ELSE SaveValue(<< \"");
+ moduleStringAppend(assertionName);
+ moduleStringAppend("\", ");
+ for (int i = start; i < end; i++) {
+ moduleStringAppend("TLCGet(");
+ moduleStringAppend("" + (i + 1));
+ moduleStringAppend(")");
+ if(i<copy.size()-1){
+ moduleStringAppend(", ");
+ }
+
+ }
+ moduleStringAppend(" >>) ");
+ moduleStringAppend("/\\ TLCSet(");
+ moduleStringAppend(""+start);
+ moduleStringAppend(", FALSE)");
+ moduleStringAppend(")");
+ moduleStringAppend(" /\\ TLCGet(");
+ moduleStringAppend("" + start);
+ moduleStringAppend(")");
+ } else {
+ node.getImplication().apply(this);
+ }
+
outAForallPredicate(node);
}
diff --git a/src/main/resources/standardModules/ExternalFunctions.tla b/src/main/resources/standardModules/ExternalFunctions.tla
index 81f00fbcdad3d4ae9ee59c1baafb9d35d2f193f8..b411bce3f70e2ee4de3df62e72ef03cbd53172b2 100644
--- a/src/main/resources/standardModules/ExternalFunctions.tla
+++ b/src/main/resources/standardModules/ExternalFunctions.tla
@@ -17,28 +17,7 @@ LOCAL SPLIT1(s,c,start,i) ==
STRING_SPLIT(s, c) == SPLIT1(s,c,1,1)
-LOCAL DIGIT_TO_STRING(x) ==
- CASE x = 0 -> "0"
- [] x = 1 -> "1"
- [] x= 2 -> "2"
- [] x = 3 -> "3"
- [] x = 4 -> "4"
- [] x= 5 -> "5"
- [] x= 6 -> "6"
- [] x= 7 -> "7"
- [] x=8 -> "8"
- [] x=9 -> "9"
-
-RECURSIVE INT_TO_STRING1(_)
-LOCAL INT_TO_STRING1(i) ==
- IF i < 10
- THEN DIGIT_TO_STRING(i)
- ELSE INT_TO_STRING1(i\div10) \o DIGIT_TO_STRING(i%10)
-
-INT_TO_STRING(i) ==
- IF i < 0
- THEN "-" \o INT_TO_STRING1(-i)
- ELSE INT_TO_STRING1(i)
+INT_TO_STRING(i) == ToString(i)
LOCAL Max(S) == CHOOSE x \in S : \A p \in S : x >= p
RECURSIVE SORT_SET(_)
diff --git a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
index e0d860f7124504b885572cd890b133c3ad8d2bee..ef866176c6cf2185ce9975baecfd0056fd979df0 100644
--- a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
+++ b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
@@ -2,6 +2,7 @@ package de.tlc4b.analysis;
import static de.tlc4b.util.TestUtil.compare;
+import org.junit.Ignore;
import org.junit.Test;
public class SetComprehensionOptimizerTest {
@@ -76,6 +77,7 @@ public class SetComprehensionOptimizerTest {
compare(expected, machine);
}
+
@Test
public void testDomain() throws Exception {
String machine = "MACHINE test\n"
@@ -87,6 +89,31 @@ public class SetComprehensionOptimizerTest {
compare(expected, machine);
}
+ @Ignore
+ @Test
+ public void testDomain2() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES {a,b| a : 1..3 & b = dom({x,y| y : 1..10 & x = y+1}) } /= {} \n" + "END";
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Naturals\n"
+ + "ASSUME {<<a, {y + 1: y \\in {y \\in ((1 .. 10)): TRUE}}>>: a \\in {a \\in ((1 .. 3)): TRUE}} # {} \n"
+ + "======";
+ compare(expected, machine);
+ }
+
+ @Ignore
+ @Test
+ public void testDomain3() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES {a,b| a = 1 & b = dom({a,b| a : 1..10 & a = b+1}) } /= {} \n" + "END";
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Naturals\n"
+ + "ASSUME {<<a, {y + 1: y \\in {y \\in ((1 .. 10)): TRUE}}>>: a \\in {a \\in ((1 .. 3)): TRUE}} # {} \n"
+ + "======";
+ compare(expected, machine);
+ }
+
+
@Test
public void testDoubleDomain() throws Exception {
String machine = "MACHINE test\n"