diff --git a/build.gradle b/build.gradle
index 946dc73707cffc16da65f53a7db5d122d4a2b3d6..f3ce79c93c20a6ec89088ec8e79abcb5f79f759d 100644
--- a/build.gradle
+++ b/build.gradle
@@ -37,7 +37,7 @@ dependencies {
testCompile (group: 'junit', name: 'junit', version: '4.7')
testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.4-SNAPSHOT')
- testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.0-SNAPSHOT')
+ testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.5-SNAPSHOT')
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
releaseJars (group: 'de.prob', name: 'prologlib', version: parser_version)
diff --git a/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
index d97d97f409c00004c820f169da14a56320026179..329d7290dcedc3cce236043284a5a4e15bf16ded 100644
--- a/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
@@ -10,6 +10,7 @@ import java.util.LinkedList;
import java.util.Map.Entry;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
@@ -54,7 +55,7 @@ public class ConstantsEliminator extends DepthFirstAdapter {
this.integerValueTable = new HashMap<Node, Integer>();
this.machineContext = machineContext;
}
-
+
public void start() {
ConstantsInTreeFinder constantInTreeFinder = new ConstantsInTreeFinder();
@@ -76,16 +77,13 @@ public class ConstantsEliminator extends DepthFirstAdapter {
// creating a new list of the constants, because constants will be
// removed from the original list
- AConstantsMachineClause constantsMachineClause = machineContext
- .getConstantsMachineClause();
- if (null != constantsMachineClause) {
- LinkedList<Node> oldConstants = new LinkedList<Node>(machineContext
- .getConstantsMachineClause().getIdentifiers());
+ LinkedList<Node> oldConstants = new LinkedList<Node>(machineContext.getConstantArrayList());
+ if (oldConstants.size() > 0) {
evalIdentifier(oldConstants);
}
-
- //TODO adapting the elimination of constants to scalar parameters
- //evalIdentifier(machineContext.getScalarParameter().values());
+
+ // TODO adapting the elimination of constants to scalar parameters
+ // evalIdentifier(machineContext.getScalarParameter().values());
}
private void evalIdentifier(Collection<Node> ids) {
@@ -140,13 +138,9 @@ public class ConstantsEliminator extends DepthFirstAdapter {
}
private void removeConstant(AIdentifierExpression id) {
- AConstantsMachineClause constantsMachineClause = machineContext
- .getConstantsMachineClause();
- constantsMachineClause.getIdentifiers().remove(id);
-
HashMap<String, Node> constants = machineContext.getConstants();
for (Entry<String, Node> entry : constants.entrySet()) {
- if(entry.getValue() == id){
+ if (entry.getValue() == id) {
constants.remove(entry.getKey());
break;
}
@@ -167,10 +161,10 @@ public class ConstantsEliminator extends DepthFirstAdapter {
Node parentParent = conjunction.parent();
if (parentParent instanceof APropertiesMachineClause) {
((APropertiesMachineClause) parentParent).setPredicates(other);
- }else if (parentParent instanceof AConjunctPredicate){
- if (((AConjunctPredicate) parentParent).getLeft() == parent){
+ } else if (parentParent instanceof AConjunctPredicate) {
+ if (((AConjunctPredicate) parentParent).getLeft() == parent) {
((AConjunctPredicate) parentParent).setLeft(other);
- }else{
+ } else {
((AConjunctPredicate) parentParent).setRight(other);
}
}
@@ -270,9 +264,9 @@ public class ConstantsEliminator extends DepthFirstAdapter {
analyseEqualsPredicate((AEqualPredicate) n);
return;
} else if (n instanceof AGreaterPredicate) {
- //analyseGreaterPredicate((AGreaterPredicate) n);
+ // analyseGreaterPredicate((AGreaterPredicate) n);
} else if (n instanceof ALessEqualPredicate) {
- //analyseLessEqualPredicate((ALessEqualPredicate) n);
+ // analyseLessEqualPredicate((ALessEqualPredicate) n);
} else if (n instanceof AConjunctPredicate) {
analysePredicate(((AConjunctPredicate) n).getLeft());
analysePredicate(((AConjunctPredicate) n).getRight());
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 8f603c19bd5a5584291eb942b5aa1d6e4244ec7f..837641969cbfd6bec11394dec15b160206ef3fd0 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -10,9 +10,11 @@ import java.util.Hashtable;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
+import java.util.Map.Entry;
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.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
@@ -79,6 +81,7 @@ public class MachineContext extends DepthFirstAdapter {
private final ArrayList<LTLFormulaVisitor> ltlVisitors;
private final PPredicate constantsSetup;
+ private boolean originallyHadConstants = false;
// machine identifier
private final LinkedHashMap<String, Node> setParameter;
private final LinkedHashMap<String, Node> scalarParameter;
@@ -98,7 +101,6 @@ public class MachineContext extends DepthFirstAdapter {
private AConstraintsMachineClause constraintMachineClause;
private ASeesMachineClause seesMachineClause;
private ASetsContextClause setsMachineClause;
- private AConstantsMachineClause constantsMachineClause;
private ADefinitionsMachineClause definitionMachineClause;
private APropertiesMachineClause propertiesMachineClause;
private AInvariantMachineClause invariantMachineClause;
@@ -474,7 +476,21 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- this.constantsMachineClause = node;
+ originallyHadConstants = true;
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression c = (AIdentifierExpression) e;
+ String name = Utils.getIdentifierAsString(c.getIdentifier());
+ exist(c.getIdentifier());
+ constants.put(name, c);
+ }
+ }
+
+ @Override
+ public void caseAAbstractConstantsMachineClause(
+ AAbstractConstantsMachineClause node) {
+ originallyHadConstants = true;
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (PExpression e : copy) {
@@ -979,6 +995,14 @@ public class MachineContext extends DepthFirstAdapter {
return scalarParameter;
}
+ public ArrayList<Node> getConstantArrayList() {
+ ArrayList<Node> list = new ArrayList<Node>();
+ for (Entry<String, Node> entry : constants.entrySet()) {
+ list.add(entry.getValue());
+ }
+ return list;
+ }
+
public LinkedHashMap<String, Node> getConstants() {
return constants;
}
@@ -1047,10 +1071,6 @@ public class MachineContext extends DepthFirstAdapter {
return setsMachineClause;
}
- public AConstantsMachineClause getConstantsMachineClause() {
- return constantsMachineClause;
- }
-
public APropertiesMachineClause getPropertiesMachineClause() {
return propertiesMachineClause;
}
@@ -1089,6 +1109,9 @@ public class MachineContext extends DepthFirstAdapter {
return constantsSetup;
}
+ public boolean originallyHadConstants() {
+ return originallyHadConstants;
+ }
}
class PMachineClauseComparator implements Comparator<PMachineClause>,
@@ -1099,8 +1122,9 @@ class PMachineClauseComparator implements Comparator<PMachineClause>,
static {
// declarations clauses
- priority.put(ASeesMachineClause.class, 11);
- priority.put(ASetsMachineClause.class, 10);
+ priority.put(ASeesMachineClause.class, 12);
+ priority.put(ASetsMachineClause.class, 11);
+ priority.put(AAbstractConstantsMachineClause.class, 10);
priority.put(AConstantsMachineClause.class, 9);
priority.put(AVariablesMachineClause.class, 8);
priority.put(AConcreteVariablesMachineClause.class, 7);
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index a735877e2b5b9aa4ad426ecd6bb44ebd3ca5c1f9..559140c2640cba38d9675d0cf725207d4953d06a 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -56,7 +56,6 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("ASetSubtractionExpression", 8, 8, false);
put("AIntervalExpression", 9, 9, true);
- put("AAddExpression", 10, 10, true);
put("AAddExpression", 10, 10, true);
put("AModuloExpression", 10, 11, true);
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 58d21f244c243c687b13877f32239f6ae203cc1b..d5939c6544ac8753e0a7a4e513c8f594a87cb32c 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -76,7 +76,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
-
+
private void checkConstantsSetup() {
PPredicate p = machineContext.getConstantsSetup();
if (p != null) {
@@ -87,8 +87,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException("Can not infer type of constant '"
- + c + "': " + getType(n));
+ throw new TypeErrorException(
+ "Can not infer type of constant '" + c + "': "
+ + getType(n));
}
}
}
@@ -100,7 +101,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getPredicate().apply(this);
}
-
public void setType(Node node, BType t) {
this.types.put(node, t);
if (t instanceof AbstractHasFollowers) {
@@ -205,6 +205,18 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
+ @Override
+ public void caseAAbstractConstantsMachineClause(
+ AAbstractConstantsMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression id = (AIdentifierExpression) e;
+ UntypedType u = new UntypedType();
+ setType(id, u);
+ }
+ }
+
@Override
public void caseAVariablesMachineClause(AVariablesMachineClause node) {
List<PExpression> copy = new ArrayList<PExpression>(
@@ -215,9 +227,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(v, u);
}
}
-
+
@Override
- public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ public void caseAConcreteVariablesMachineClause(
+ AConcreteVariablesMachineClause node) {
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (PExpression e : copy) {
@@ -226,8 +239,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(v, u);
}
}
-
-
+
/**
* Definitions
*/
@@ -327,7 +339,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- for (Entry<String, Node> entry : machineContext.getScalarParameter().entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getScalarParameter()
+ .entrySet()) {
String name = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 912acc2edf9b98507edd4702787b40551fd16f65..69e237151d5b0f97dbc804bfebbdd432fcbaa03c 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -52,7 +52,7 @@ public class TLCOutputInfo {
this.constants = machineContext.getConstants().keySet();
this.hasInit = tlaModule.getInitPredicates().size() > 0;
- if (machineContext.getConstantsMachineClause() != null) {
+ if (machineContext.originallyHadConstants()) {
this.constantSetup = true;
}
@@ -69,7 +69,6 @@ public class TLCOutputInfo {
namesMapping.put(newName, name);
typesTable.put(newName, typechecker.getType(node));
}
-
}
}
diff --git a/src/test/java/de/tlc4b/prettyprint/ClausesTest.java b/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
index 213ae762fff335e96db2076265ca212e56007122..a4a78c37e1f9a1cb92d72a483a5b04b2031df9e7 100644
--- a/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
@@ -29,4 +29,28 @@ public class ClausesTest {
compare(expected, machine);
}
+ @Test
+ public void testAbstractConstants() throws Exception {
+ String machine = "MACHINE test\n"
+ + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES k = 1\n"
+ + "END";
+ String expected = "---- MODULE test ----\n"
+ + "k == 1 "
+ + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testConcreteConstants() throws Exception {
+ String machine = "MACHINE test\n"
+ + "CONCRETE_CONSTANTS k\n"
+ + "PROPERTIES k = 1\n"
+ + "END";
+ String expected = "---- MODULE test ----\n"
+ + "k == 1 "
+ + "======";
+ compare(expected, machine);
+ }
+
}
diff --git a/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
index 47bfb0fc2b08d6c13aa138b967e14fc9e63957e9..d42a95784f371448ec170fa68541b09deda09940 100644
--- a/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
+++ b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
@@ -29,7 +29,7 @@ public abstract class AbstractParseMachineTest {
return dir.listFiles(new MachineFilenameFilter());
}
- protected static File[] getMachinesRecursive(String path, ArrayList<String> ignoreList) {
+ protected static File[] getMachinesRecursively(String path, ArrayList<String> ignoreList) {
File[] files = walk(path, ignoreList).toArray(new File[0]);
return files;
}
@@ -74,7 +74,7 @@ public abstract class AbstractParseMachineTest {
final ArrayList<TLCResult> expectedValues = new ArrayList<TLCResult>();
for (String path : list) {
- File[] machines = getMachinesRecursive(path, ignoreList);
+ File[] machines = getMachinesRecursively(path, ignoreList);
allMachines.addAll(Arrays.asList(machines));
for (int i = 0; i < machines.length; i++) {
expectedValues.add(TLCResult.NoError);