diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 369207fb8d56c19196f5c6a38dc186e5eb81b7bc..5ee14561fdf7963f94bb46f00b8fff6a733bfe81 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -5,6 +5,7 @@ import java.io.IOException;
import java.util.ArrayList;
import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.PPredicate;
@@ -68,6 +69,10 @@ public class Translator {
BParser parser = new BParser(machineName);
start = parser.parseFile(machineFile, false);
+ // Definitions of definitions files are injected in the ast of the main machine
+ final RecursiveMachineLoader rml = new RecursiveMachineLoader(
+ machineFile.getParent(), parser.getContentProvider());
+ rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(), parser.getPragmas());
if(constantSetup!= null){
BParser con = new BParser();
@@ -93,9 +98,9 @@ public class Translator {
}
public void translate() {
- new DefinitionsEliminator(start);
-
new NotSupportedConstructs(start);
+
+ new DefinitionsEliminator(start);
MachineContext machineContext = new MachineContext(machineName, start,
ltlFormula, constantsSetup);
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 590d9c44d9d91a50f3b97836cc6d6f72f61542da..8f603c19bd5a5584291eb942b5aa1d6e4244ec7f 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -101,7 +101,6 @@ public class MachineContext extends DepthFirstAdapter {
private AConstantsMachineClause constantsMachineClause;
private ADefinitionsMachineClause definitionMachineClause;
private APropertiesMachineClause propertiesMachineClause;
- private AVariablesMachineClause variablesMachineClause;
private AInvariantMachineClause invariantMachineClause;
private AInitialisationMachineClause initialisationMachineClause;
private AOperationsMachineClause operationMachineClause;
@@ -437,8 +436,6 @@ public class MachineContext extends DepthFirstAdapter {
}
}
- // TODO import, include, ..
-
@Override
public void caseASetsContextClause(ASetsContextClause node) {
this.setsMachineClause = node;
@@ -490,7 +487,19 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- this.variablesMachineClause = node;
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression v = (AIdentifierExpression) e;
+ String name = Utils.getIdentifierAsString(v.getIdentifier());
+ exist(v.getIdentifier());
+ variables.put(name, v);
+ }
+ }
+
+ @Override
+ public void caseAConcreteVariablesMachineClause(
+ AConcreteVariablesMachineClause node) {
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (PExpression e : copy) {
@@ -724,8 +733,6 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAAssignSubstitution(AAssignSubstitution node) {
- // TODO maybe give better feedback to the user, e.g. cannot assign a
- // value to constant 'c'
ArrayList<LinkedHashMap<String, Node>> temp = contextTable;
{
List<PExpression> copy = new ArrayList<PExpression>(
@@ -788,10 +795,7 @@ public class MachineContext extends DepthFirstAdapter {
if (node.getName() != null) {
AIdentifierExpression op = (AIdentifierExpression) node.getName();
String name = Utils.getIdentifierAsString(op.getIdentifier());
- Node o = operations.get(name); // TODO operation
- // of an
- // external
- // machine
+ Node o = operations.get(name);
if (o != null) {
this.referencesTable.put(op, o);
} else {
@@ -1060,10 +1064,6 @@ public class MachineContext extends DepthFirstAdapter {
this.propertiesMachineClause = propertiesMachineClause;
}
- public AVariablesMachineClause getVariablesMachineClause() {
- return variablesMachineClause;
- }
-
public AInvariantMachineClause getInvariantMachineClause() {
return invariantMachineClause;
}
diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
index c123bbe89e2018470610bd89365ed5fc9484104b..1798fb444d4f14b2c64c118c02e33d5024a586ce 100644
--- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
+++ b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
@@ -2,31 +2,72 @@ package de.tlc4b.analysis;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACaseSubstitution;
+import de.be4.classicalb.core.parser.node.AExtendsMachineClause;
+import de.be4.classicalb.core.parser.node.AImportsMachineClause;
+import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
+import de.be4.classicalb.core.parser.node.APromotesMachineClause;
+import de.be4.classicalb.core.parser.node.ARefinesModelClause;
+import de.be4.classicalb.core.parser.node.ASeesModelClause;
import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
+import de.be4.classicalb.core.parser.node.AUsesMachineClause;
import de.be4.classicalb.core.parser.node.AWhileSubstitution;
import de.be4.classicalb.core.parser.node.Start;
import de.tlc4b.exceptions.NotSupportedException;
-public class NotSupportedConstructs extends DepthFirstAdapter{
-
- public NotSupportedConstructs(Start start){
+public class NotSupportedConstructs extends DepthFirstAdapter {
+
+ public NotSupportedConstructs(Start start) {
start.apply(this);
}
-
- public void inAWhileSubstitution(AWhileSubstitution node)
- {
- throw new NotSupportedException("While substitutions are currently not supported.");
- }
-
- public void inACaseSubstitution(ACaseSubstitution node)
- {
- throw new NotSupportedException("Case substitutions are currently not supported.");
- }
-
- public void inASequenceSubstitution(ASequenceSubstitution node)
- {
- throw new NotSupportedException("Sequence substitutions ';' are currently not supported.");
- }
-
+
+ public void inARefinesModelClause(ARefinesModelClause node) {
+ throw new NotSupportedException(
+ "Refines clause is currently not supported.");
+ }
+
+ public void inAUsesMachineClause(AUsesMachineClause node) {
+ throw new NotSupportedException(
+ "USES clause is currently not supported.");
+ }
+
+ public void inAPromotesMachineClause(APromotesMachineClause node) {
+ throw new NotSupportedException(
+ "Promotes clause is currently not supported.");
+ }
+
+ public void inASeesModelClause(ASeesModelClause node) {
+ throw new NotSupportedException(
+ "Sees clause is currently not supported.");
+ }
+
+ public void inAIncludesMachineClause(AIncludesMachineClause node) {
+ throw new NotSupportedException(
+ "INCLUDES clause is currently not supported.");
+ }
+
+ public void inAExtendsMachineClause(AExtendsMachineClause node) {
+ throw new NotSupportedException(
+ "EXTENDS clause is currently not supported.");
+ }
+
+ public void inAImportsMachineClause(AImportsMachineClause node) {
+ throw new NotSupportedException(
+ "IMPORTS clause is currently not supported.");
+ }
+
+ public void inAWhileSubstitution(AWhileSubstitution node) {
+ throw new NotSupportedException(
+ "While substitutions are currently not supported.");
+ }
+
+ public void inACaseSubstitution(ACaseSubstitution node) {
+ throw new NotSupportedException(
+ "Case substitutions are currently not supported.");
+ }
+
+ public void inASequenceSubstitution(ASequenceSubstitution node) {
+ throw new NotSupportedException(
+ "Sequence substitutions ';' are currently not supported.");
+ }
}
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index 9a05094e989bdc3e3f206ddb2503dcac9adafb88..a735877e2b5b9aa4ad426ecd6bb44ebd3ca5c1f9 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -5,12 +5,14 @@ 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.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.FunctionType;
import de.tlc4b.btypes.IntegerType;
public class PrecedenceCollector extends DepthFirstAdapter {
@@ -58,8 +60,10 @@ public class PrecedenceCollector extends DepthFirstAdapter {
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);
+
}
private Precedence getPrecedence(Node node) {
@@ -143,6 +147,25 @@ public class PrecedenceCollector extends DepthFirstAdapter {
brackets.add(node);
}
}
+
+ @Override
+ 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());
+ if (Precedence.makeBrackets(p, parent)) {
+ brackets.add(node);
+ }
+ }
+
+ }
@Override
public void inAMinusOrSetSubtractExpression(
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index 396464f5823680470027401c0b7242ccfec7fbbf..410402e97e47822aec963e574c2982e6329ce381 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -10,6 +10,7 @@ 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.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
@@ -19,11 +20,13 @@ import de.be4.classicalb.core.parser.node.AGeneralProductExpression;
import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
+import de.be4.classicalb.core.parser.node.ALetSubstitution;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression;
import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.AVarSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -341,6 +344,52 @@ public class Renamer extends DepthFirstAdapter {
localContexts.add(context);
}
+ @Override
+ public void caseAAnySubstitution(AAnySubstitution node) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.addAll(node.getIdentifiers());
+ evalBoundedVariables(node, list);
+
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ e.apply(this);
+ }
+ node.getWhere().apply(this);
+ node.getThen().apply(this);
+ removeLastContext();
+ }
+
+ @Override
+ public void caseALetSubstitution(ALetSubstitution node) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.addAll(node.getIdentifiers());
+ evalBoundedVariables(node, list);
+
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ e.apply(this);
+ }
+ node.getPredicate().apply(this);
+ node.getSubstitution().apply(this);
+ removeLastContext();
+ }
+
+ @Override
+ public void caseAVarSubstitution(AVarSubstitution node) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.addAll(node.getIdentifiers());
+ evalBoundedVariables(node, list);
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ e.apply(this);
+ }
+ node.getSubstitution().apply(this);
+ removeLastContext();
+ }
+
public void removeLastContext() {
localContexts.remove(localContexts.size() - 1);
}
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index a81f8f71e81754fef4c96322581a3843bed83642..1eefd1275e9a2c87bd2e812502b54922c8b77522 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -143,6 +143,8 @@ public final class StandardMadules {
public static final String REL_SEQUENCE_SIZE = "RelSeqSize";
public static final String IS_REL_SEQUENCE = "isRelSeq";
public static final String REL_SEQUENCE_SET = "RelSeqSet";
+ public static final String REL_SET_OF_SEQUENCES = "RelSeq";
+ public static final String REL_SET_OF_NON_EMPTY_SEQUENCES = "RelSeq1";
public static final String IS_REL_SEQUENCE_1 = "isRelSeq1";
public static final String REL_SEQUENCE_1_SET = "RelSeqSet1";
public static final String REL_INJECTIVE_SEQUENCE = "RelISeq";
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index ea233f40711cedbeb70307370a267f199ffaa39f..58d21f244c243c687b13877f32239f6ae203cc1b 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -57,6 +57,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
c.getTree().apply(this);
checkLTLFormulas();
+ checkConstantsSetup();
}
private void checkLTLFormulas() {
@@ -75,6 +76,23 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
+
+ private void checkConstantsSetup() {
+ PPredicate p = machineContext.getConstantsSetup();
+ if (p != null) {
+ setType(p, BoolType.getInstance());
+ p.apply(this);
+ for (Entry<String, Node> entry : machineContext.getConstants()
+ .entrySet()) {
+ String c = entry.getKey();
+ Node n = entry.getValue();
+ if (getType(n).isUntyped()) {
+ throw new TypeErrorException("Can not infer type of constant '"
+ + c + "': " + getType(n));
+ }
+ }
+ }
+ }
@Override
public void caseAPredicateParseUnit(APredicateParseUnit node) {
@@ -197,7 +215,19 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(v, u);
}
}
-
+
+ @Override
+ public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression v = (AIdentifierExpression) e;
+ UntypedType u = new UntypedType();
+ setType(v, u);
+ }
+ }
+
+
/**
* Definitions
*/
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
index 11287b5f6fa4fcaa7805755505c677ab2b46dbfc..068edbc5591a31f3dde4969f8085d5f566d10ac0 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
@@ -4,6 +4,7 @@ import java.util.Hashtable;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
@@ -26,16 +27,25 @@ import de.be4.classicalb.core.parser.node.Start;
public class DefinitionCollector extends DepthFirstAdapter {
private Hashtable<String, PDefinition> definitionsTable;
+ private ADefinitionsMachineClause definitionsMachineClause;
public Hashtable<String, PDefinition> getDefinitions(){
return new Hashtable<String, PDefinition>(definitionsTable);
}
+ public ADefinitionsMachineClause getDefinitionsMachineClause(){
+ return this.definitionsMachineClause;
+ }
public DefinitionCollector(Start tree) {
definitionsTable = new Hashtable<String, PDefinition>();
tree.apply(this);
}
-
+
+ @Override
+ public void inADefinitionsMachineClause(ADefinitionsMachineClause node) {
+ this.definitionsMachineClause = node;
+ }
+
@Override
public void caseAPredicateDefinitionDefinition(
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index 39e8517fe77d7217ba50b4cb69ae6bbff3398ffb..fbcea22edf06a061ac8f043720bad06b3d954187 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -63,16 +63,26 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
List<PDefinition> copy = new ArrayList<PDefinition>(
node.getDefinitions());
for (PDefinition e : copy) {
+ if (e instanceof AExpressionDefinitionDefinition) {
+ String name = ((AExpressionDefinitionDefinition) e).getName()
+ .getText().toString();
+ if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")
+ || name.startsWith("SET_PREF_")
+ || name.startsWith("ANIMATION_FUNCTION"))
+ continue;
+ }
e.apply(this);
}
for (PDefinition e : copy) {
if (e instanceof AExpressionDefinitionDefinition) {
String name = ((AExpressionDefinitionDefinition) e).getName()
.getText().toString();
- if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")|| name.startsWith("SET_PREF_"))
+ if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")
+ || name.startsWith("SET_PREF_"))
continue;
} else if (e instanceof APredicateDefinitionDefinition) {
- String name = ((APredicateDefinitionDefinition) e).getName().getText().toString();
+ String name = ((APredicateDefinitionDefinition) e).getName()
+ .getText().toString();
if (name.equals("GOAL"))
continue;
}
@@ -94,7 +104,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
String paramName = Utils.getIdentifierAsString(p.getIdentifier());
-
+
Node arg = arguments.get(i);
arg.apply(this);
context.put(paramName, node.getParameters().get(i));
@@ -124,7 +134,6 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
context.put(paramName, node.getParameters().get(i));
}
contextStack.add(context);
-
clone.getRhs().apply(this);
node.replaceBy(clone.getRhs());
contextStack.remove(context);
@@ -144,16 +153,15 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
String paramName = Utils.getIdentifierAsString(p.getIdentifier());
-
+
Node arg = arguments.get(i);
arg.apply(this);
context.put(paramName, node.getParameters().get(i));
- //context.put(paramName, arguments.get(i));
+ // context.put(paramName, arguments.get(i));
}
contextStack.add(context);
clone.getRhs().apply(this);
node.replaceBy(clone.getRhs());
-
contextStack.remove(context);
}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 754dca4cbaa30db638d136dc0f932b8e41fe0835..fb9174a0abbd14b772a095acd3e2ecd8c5a2a800 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -198,6 +198,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
+ right.apply(this);
ArrayList<PExpression> element = new ArrayList<PExpression>();
element.add(right);
if (machineContext.getVariables().values().contains(r_left)) {
@@ -207,9 +208,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
removedNodes.add(n);
}
if (list.contains(r_right)
- && isAConstantExpression(right, list, ignoreList)) {
+ && isAConstantExpression(left, list, ignoreList)) {
+ left.apply(this);
ArrayList<PExpression> element = new ArrayList<PExpression>();
- element.add(right);
+ element.add(left);
if (machineContext.getVariables().values().contains(r_right)) {
r_right = variablesHashTable.get(r_right);
}
@@ -256,6 +258,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
+ right.apply(this);
if (machineContext.getVariables().values().contains(r_left)) {
r_left = variablesHashTable.get(r_left);
}
@@ -268,11 +271,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (n instanceof AConjunctPredicate) {
Node left = ((AConjunctPredicate) n).getLeft();
Node right = ((AConjunctPredicate) n).getRight();
- analysePredicate(left, list,
- ignoreList);
- analysePredicate(right, list,
- ignoreList);
- if(removedNodes.contains(left) && removedNodes.contains(right)){
+ analysePredicate(left, list, ignoreList);
+ analysePredicate(right, list, ignoreList);
+ if (removedNodes.contains(left) && removedNodes.contains(right)) {
removedNodes.add(n);
}
return;
@@ -474,6 +475,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
node.getIdentifiers()));
}
+
@Override
public void inALetSubstitution(ALetSubstitution node) {
HashSet<Node> list = new HashSet<Node>();
@@ -491,7 +493,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
private Hashtable<Node, Node> variablesHashTable;
public void inABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
- if(!(node.getPredicate() instanceof AExistsPredicate)){
+ if (!(node.getPredicate() instanceof AExistsPredicate)) {
variablesHashTable = new Hashtable<Node, Node>();
HashSet<Node> list = new HashSet<Node>();
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 98202ddf7cdff9751a7f792c52b8156099022b21..e0e5b6e7f9693aaf694c7cde7dd408a3255fa657 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -304,7 +304,7 @@ public class TLAPrinter extends DepthFirstAdapter {
ArrayList<Node> list = this.tlaModule.getAssume();
if (list.size() == 0)
return;
-
+
for (int i = 0; i < list.size(); i++) {
tlaModuleString.append("ASSUME ");
list.get(i).apply(this);
@@ -352,7 +352,7 @@ public class TLAPrinter extends DepthFirstAdapter {
if (inits.size() == 0)
return;
tlaModuleString.append("Init == ");
- if(inits.size() > 1)
+ if (inits.size() > 1)
tlaModuleString.append("\n\t/\\ ");
for (int i = 0; i < inits.size(); i++) {
Node init = inits.get(i);
@@ -1040,14 +1040,14 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAConjunctPredicate(AConjunctPredicate node) {
boolean left = typeRestrictor.isARemovedNode(node.getLeft());
boolean right = typeRestrictor.isARemovedNode(node.getRight());
-
- if(left && right){
+
+ if (left && right) {
tlaModuleString.append("TRUE");
- } else if (left){
+ } else if (left) {
node.getRight().apply(this);
- } else if (right){
+ } else if (right) {
node.getLeft().apply(this);
- }else{
+ } else {
inAConjunctPredicate(node);
node.getLeft().apply(this);
tlaModuleString.append(" /\\ ");
@@ -1715,7 +1715,8 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append("]");
} else {
if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.isARemovedNode(node.parent())) {
+ && !typeRestrictor.isARemovedNode(node.parent())
+ && !this.tlaModule.getInitPredicates().contains(node.parent())) {
tlaModuleString.append(REL_TOTAL_FUNCTION_ELEMENT_OF);
} else {
tlaModuleString.append(REL_TOTAL_FUNCTION);
@@ -1732,8 +1733,7 @@ public class TLAPrinter extends DepthFirstAdapter {
Node parent = node.parent();
if (parent instanceof AMemberPredicate
&& !typeRestrictor.isARemovedNode(parent)
- // && !this.tlaModule.getInitPredicates().contains(parent)
- ) {
+ && !this.tlaModule.getInitPredicates().contains(parent)) {
return true;
} else {
String clazz = parent.getClass().getName();
@@ -1806,7 +1806,7 @@ public class TLAPrinter extends DepthFirstAdapter {
right.apply(this);
tlaModuleString.append(")");
return;
- }else {
+ } else {
tlaModuleString.append(funcName);
}
} else {
@@ -1883,9 +1883,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
tlaModuleString.append(")");
return;
-
}
-
tlaModuleString.append("{");
{
List<PExpression> copy = new ArrayList<PExpression>(
@@ -2461,31 +2459,13 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseASeqExpression(ASeqExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
- if (node.parent() instanceof AMemberPredicate) {
- AMemberPredicate member = (AMemberPredicate) node.parent();
- tlaModuleString.append(REL_SEQUENCE_SET);
- tlaModuleString.append("(");
- member.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
- } else if (node.parent() instanceof ANotMemberPredicate) {
- ANotMemberPredicate member = (ANotMemberPredicate) node
- .parent();
- tlaModuleString.append(REL_SEQUENCE_SET);
- tlaModuleString.append("(");
- member.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
- }
-
+ tlaModuleString.append(REL_SET_OF_SEQUENCES);
} else {
tlaModuleString.append("Seq");
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
}
+ tlaModuleString.append("(");
+ node.getExpression().apply(this);
+ tlaModuleString.append(")");
}
@Override
@@ -2593,31 +2573,13 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseASeq1Expression(ASeq1Expression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
- if (node.parent() instanceof AMemberPredicate) {
- AMemberPredicate member = (AMemberPredicate) node.parent();
- tlaModuleString.append(REL_SEQUENCE_1_SET);
- tlaModuleString.append("(");
- member.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
- } else if (node.parent() instanceof ANotMemberPredicate) {
- ANotMemberPredicate member = (ANotMemberPredicate) node
- .parent();
- tlaModuleString.append(REL_SEQUENCE_1_SET);
- tlaModuleString.append("(");
- member.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
- }
+ tlaModuleString.append(REL_SET_OF_NON_EMPTY_SEQUENCES);
} else {
-
tlaModuleString.append(SEQUENCE_1);
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
}
+ tlaModuleString.append("(");
+ node.getExpression().apply(this);
+ tlaModuleString.append(")");
}
@Override
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index 61591cb733e0d0afd64f9acc833a36eeeeba7ae5..cebdacfd065e4fda30b7643456656a3dbf27a4ea 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -10,6 +10,7 @@ import java.util.Map.Entry;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
+import de.be4.classicalb.core.parser.node.AConcreteVariablesMachineClause;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
@@ -153,7 +154,7 @@ public class Generator extends DepthFirstAdapter {
AMemberPredicate memberPredicate = new AMemberPredicate(
(PExpression) param, (PExpression) restrictedNode);
tlaModule.addInit(memberPredicate);
-
+
init = true;
this.tlaModule.variables.add(param);
}
@@ -165,7 +166,7 @@ public class Generator extends DepthFirstAdapter {
if (!typeRestrictor.isARemovedNode(clause.getPredicates())) {
tlaModule.addInit(clause.getPredicates());
}
-
+
} else {
if (!typeRestrictor.isARemovedNode(clause.getPredicates()))
tlaModule.addAssume(clause.getPredicates());
@@ -239,12 +240,13 @@ public class Generator extends DepthFirstAdapter {
return;
LinkedHashMap<Node, Node> conValueTable = constantsEvaluator
.getValueOfIdentifierMap();
- Iterator<Entry<Node, Node>> iterator = conValueTable.entrySet().iterator();
- while (iterator.hasNext()){
+ Iterator<Entry<Node, Node>> iterator = conValueTable.entrySet()
+ .iterator();
+ while (iterator.hasNext()) {
Entry<Node, Node> entry = iterator.next();
AIdentifierExpression con = (AIdentifierExpression) entry.getKey();
Node value = entry.getValue();
-
+
AExpressionDefinitionDefinition exprDef = new AExpressionDefinitionDefinition(
con.getIdentifier().get(0), new LinkedList<PExpression>(),
(PExpression) value.clone());
@@ -259,7 +261,7 @@ public class Generator extends DepthFirstAdapter {
Node propertiesPerdicate = machineContext.getPropertiesMachineClause()
.getPredicates();
- if (remainingConstants.size() != 0) {
+ if (remainingConstants.size() > 0) {
boolean init = false;
int numberOfIteratedConstants = 0;
@@ -302,8 +304,11 @@ public class Generator extends DepthFirstAdapter {
}
} else {
- tlaModule.assumes.addAll(constantsEvaluator.getPropertiesList());
- // tlaModule.addAssume(propertiesPerdicate);
+ if (machineContext.getConstantsSetup() == null){
+ tlaModule.assumes
+ .addAll(constantsEvaluator.getPropertiesList());
+ }
+ tlaModule.addAssume(propertiesPerdicate);
}
}
@@ -323,6 +328,15 @@ public class Generator extends DepthFirstAdapter {
this.tlaModule.variables.add(e);
}
}
+
+ @Override
+ public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ this.tlaModule.variables.add(e);
+ }
+ }
@Override
public void inAAssertionsMachineClause(AAssertionsMachineClause node) {
diff --git a/src/main/resources/standardModules/SequencesAsRelations.tla b/src/main/resources/standardModules/SequencesAsRelations.tla
index 3263177b203188962fe99457bbeba1edb5dde1f5..e97b03587cf0749bd29f37eeb2818d50ba62134f 100644
--- a/src/main/resources/standardModules/SequencesAsRelations.tla
+++ b/src/main/resources/standardModules/SequencesAsRelations.tla
@@ -6,11 +6,23 @@ IsRelSeq(x, S) == \A n \in 1..Cardinality(x): RelCall(x,n) \in S
RelSeqSet(x, S) == IF IsRelSeq(x,S) THEN {x} ELSE {}
+RelSeq(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
+ IN /\ Cardinality(p) = Cardinality(d)
+ /\ d = 1..Cardinality(d)}
+
IsRelSeq1(x, S) == x # {} /\ IsRelSeq(x, S)
\* Testing if x is a non-empty sequence with elements of the set S
RelSeqSet1(x, S) == IF IsRelSeq1(x,S) THEN {x} ELSE {}
+RelSeq1(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
+ IN /\ Cardinality(p) > 0
+ /\ Cardinality(p) = Cardinality(d)
+ /\ d = 1..Cardinality(d)}
+
+
LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinality(DOMAIN x)}
: n \in 0..Cardinality(S)}
diff --git a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
index 601bb9b09e6e3f542241a6c5ed62aa16016b080d..ff158fce7be4a80a4c2c73051cab7fbfa9bf6d1c 100644
--- a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
@@ -42,5 +42,12 @@ public class SpecialTest {
}
+ @Test
+ public void testDefinitionsLoad() throws Exception {
+ String[] a = new String[] {
+ "./src/test/resources/special/LoadDefinitions.mch"};
+ assertEquals(NoError, test(a));
+ }
+
}
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index 10825f9612990fd2b32cb299bc3ef81bdfdfcb91..41414861b9998ca2837c50f73f0956b7892eb3b6 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -1,7 +1,7 @@
package testing;
-
import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
+import static de.tlc4b.util.TestUtil.test;
import java.io.File;
import java.util.ArrayList;
@@ -18,8 +18,8 @@ import de.tlc4b.util.PolySuite.Config;
import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
-public class Testing2 extends AbstractParseMachineTest{
-
+public class Testing2 extends AbstractParseMachineTest {
+
private final File machine;
public Testing2(File machine, TLCResult result) {
@@ -28,9 +28,11 @@ public class Testing2 extends AbstractParseMachineTest{
@Test
public void testRunTLC() throws Exception {
- String[] a = new String[] {machine.getPath()};
+ String[] a = new String[] {
+ machine.getPath()};
TLC4B.main(a);
//TLC4B.test(a,false);
+ //test(a);
}
@Config
@@ -39,5 +41,5 @@ public class Testing2 extends AbstractParseMachineTest{
list.add(new TestPair(NoError, "./src/test/resources/testing"));
return getConfiguration(list);
}
-
+
}
diff --git a/src/test/resources/laws/SequencesAsRelationsTest.mch b/src/test/resources/laws/SequencesAsRelationsTest.mch
index 4d4b924ee4a2131575c2dae0142a83807dab4824..27e77ccc20f8ced8b90a2b4021418b3593a8dc27 100644
--- a/src/test/resources/laws/SequencesAsRelationsTest.mch
+++ b/src/test/resources/laws/SequencesAsRelationsTest.mch
@@ -10,6 +10,11 @@ PROPERTIES
& {} : seq({1+0})
& {} : seq({})
+& {x,y| x : 1..10 & y : {3}} : seq({3})
+& {} \/ {} : seq({1})
+& {x,y| x : 1..10 & y : {3}} : seq1({3})
+& {} \/ {} /: seq1({1})
+
/* Set of sequences */
& {(1+0,1)} : seq1({1})
diff --git a/src/test/resources/special/Definitions.def b/src/test/resources/special/Definitions.def
new file mode 100644
index 0000000000000000000000000000000000000000..2b6227ad5efba36a3fa5fe6f17aeb4523ece4024
--- /dev/null
+++ b/src/test/resources/special/Definitions.def
@@ -0,0 +1,3 @@
+DEFINITIONS
+d3 == 3;
+d4 == 4;
\ No newline at end of file
diff --git a/src/test/resources/special/LoadDefinitions.mch b/src/test/resources/special/LoadDefinitions.mch
new file mode 100644
index 0000000000000000000000000000000000000000..563737f0712a60442f3a7f26ccd03d0bda591c59
--- /dev/null
+++ b/src/test/resources/special/LoadDefinitions.mch
@@ -0,0 +1,8 @@
+MACHINE LoadDefinitions
+DEFINITIONS
+"Definitions.def";
+d1 == 1;
+d2 == 2;
+PROPERTIES
+d1+ d2 = d3 & d4 = d3 + d1
+END
\ No newline at end of file