diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 24504794bddb8a9481bfacaee8f61e9123735305..89610f7bf341b3f93738699f49726790f0233c53 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -288,18 +288,19 @@ public class TLC4B {
handleMainFileName();
if (TLC4BGlobals.isTranslate()) {
StopWatch.start("Parsing");
+ System.out.println("Parsing...");
translator = new Translator(machineFileNameWithoutFileExtension,
mainfile, this.ltlFormula, this.constantsSetup);
StopWatch.stop("Parsing");
- System.out.println("Parsing Completed.");
+
StopWatch.start("Translation");
+ System.out.println("Translating...");
translator.translate();
this.tlaModule = translator.getModuleString();
this.config = translator.getConfigString();
this.tlcOutputInfo = translator.getTLCOutputInfo();
createFiles();
StopWatch.stop("Translation");
- System.out.println("Translation Completed.");
}
}
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 27b5ff2ce9752c6af62520340786fcd2fc2a9fe6..87bb1cca6fb9b18f8e47d290aff659da5fb187b5 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -3,6 +3,7 @@ package de.tlc4b;
import java.io.File;
import java.io.IOException;
import java.util.HashSet;
+import java.util.Map;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
@@ -22,9 +23,12 @@ import de.tlc4b.analysis.Typechecker;
import de.tlc4b.analysis.UsedStandardModules;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
import de.tlc4b.analysis.transformation.DefinitionsEliminator;
+import de.tlc4b.analysis.transformation.SeesEliminator;
+import de.tlc4b.analysis.transformation.SetComprehensionOptimizer;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.analysis.unchangedvariables.InvariantPreservationAnalysis;
import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
+import de.tlc4b.exceptions.TLC4BIOException;
import de.tlc4b.prettyprint.TLAPrinter;
import de.tlc4b.tla.Generator;
import de.tlc4b.tlc.TLCOutputInfo;
@@ -34,6 +38,7 @@ public class Translator {
private String machineString;
private Start start;
+ private Map<String, Start> parsedMachines;
private String moduleString;
private String configString;
private String machineName;
@@ -64,12 +69,16 @@ public class Translator {
}
public Translator(String machineName, File machineFile, String ltlFormula,
- String constantSetup) throws IOException, BException {
+ String constantSetup) throws BException, IOException {
this.machineName = machineName;
this.ltlFormula = ltlFormula;
BParser parser = new BParser(machineName);
- start = parser.parseFile(machineFile, false);
+ try {
+ start = parser.parseFile(machineFile, false);
+ } catch (NoClassDefFoundError e) {
+ throw new TLC4BIOException("Definitions file cannot be found.");
+ }
// Definitions of definitions files are injected in the ast of the main
// machine
@@ -77,6 +86,8 @@ public class Translator {
machineFile.getParent(), parser.getContentProvider());
rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(),
parser.getPragmas());
+
+ parsedMachines = rml.getParsedMachines();
if (constantSetup != null) {
BParser con = new BParser();
@@ -104,15 +115,18 @@ public class Translator {
}
public void translate() {
- new NotSupportedConstructs(start);
+ // ast transformation
+ SeesEliminator.eliminateSeesClauses(start, parsedMachines);
- new DefinitionsEliminator(start);
+ new NotSupportedConstructs(start);
+ DefinitionsEliminator.eliminateDefinitions(start);
+ SetComprehensionOptimizer.optimizeSetComprehensions(start);
+
MachineContext machineContext = new MachineContext(machineName, start,
ltlFormula, constantsSetup);
this.machineName = machineContext.getMachineName();
- if(machineContext
- .machineContainsOperations()){
+ if (machineContext.machineContainsOperations()) {
TLC4BGlobals.setPrintCoverage(true);
}
@@ -149,7 +163,8 @@ public class Translator {
UsedStandardModules usedModules = new UsedStandardModules(start,
typechecker, typeRestrictor, generator.getTlaModule());
- standardModulesToBeCreated = usedModules.getStandardModulesToBeCreated();
+ standardModulesToBeCreated = usedModules
+ .getStandardModulesToBeCreated();
PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
.getTlaModule().getOperations(), machineContext);
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index fa0ad62db198d93fd159d30c3dbd8faf7c429153..c621ee8da44f8811e8bcfe556f2e1bd252727585 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -1,10 +1,7 @@
package de.tlc4b.analysis;
-import java.io.Serializable;
import java.util.ArrayList;
import java.util.Collection;
-import java.util.Collections;
-import java.util.Comparator;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedHashMap;
@@ -29,6 +26,7 @@ import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.ADefinitionSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
+import de.be4.classicalb.core.parser.node.AEventBComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AForallPredicate;
@@ -54,7 +52,6 @@ import de.be4.classicalb.core.parser.node.ARecEntry;
import de.be4.classicalb.core.parser.node.ARecordFieldExpression;
import de.be4.classicalb.core.parser.node.ASeesMachineClause;
import de.be4.classicalb.core.parser.node.ASetsContextClause;
-import de.be4.classicalb.core.parser.node.ASetsMachineClause;
import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
import de.be4.classicalb.core.parser.node.Node;
@@ -68,6 +65,8 @@ import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.analysis.transformation.DefinitionsSorter;
+import de.tlc4b.analysis.transformation.MachineClauseSorter;
import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.ltl.LTLBPredicate;
import de.tlc4b.ltl.LTLFormulaVisitor;
@@ -83,8 +82,8 @@ public class MachineContext extends DepthFirstAdapter {
private boolean constantSetupInTraceFile = false;
// machine identifier
- private final LinkedHashMap<String, Node> setParameter;
- private final LinkedHashMap<String, Node> scalarParameter;
+ private final LinkedHashMap<String, Node> machineSetParameter;
+ private final LinkedHashMap<String, Node> machineScalarParameter;
private final LinkedHashMap<String, Node> deferredSets;
private final LinkedHashMap<String, Node> enumeratedSets;
@@ -129,8 +128,8 @@ public class MachineContext extends DepthFirstAdapter {
this.ltlVisitors.add(ltlVisitor);
}
- this.setParameter = new LinkedHashMap<String, Node>();
- this.scalarParameter = new LinkedHashMap<String, Node>();
+ this.machineSetParameter = new LinkedHashMap<String, Node>();
+ this.machineScalarParameter = new LinkedHashMap<String, Node>();
this.deferredSets = new LinkedHashMap<String, Node>();
this.enumeratedSets = new LinkedHashMap<String, Node>();
@@ -210,17 +209,17 @@ public class MachineContext extends DepthFirstAdapter {
private void exist(LinkedList<TIdentifierLiteral> list) {
String name = Utils.getIdentifierAsString(list);
- existString(name);
+ identifierAlreadyExists(name);
}
- private void existString(String name) {
+ private void identifierAlreadyExists(String name) {
if (constants.containsKey(name) || variables.containsKey(name)
|| operations.containsKey(name)
|| deferredSets.containsKey(name)
|| enumeratedSets.containsKey(name)
|| enumValues.containsKey(name)
- || setParameter.containsKey(name)
- || scalarParameter.containsKey(name)
+ || machineSetParameter.containsKey(name)
+ || machineScalarParameter.containsKey(name)
|| seenMachines.containsKey(name)
|| definitions.containsKey(name)) {
throw new ScopeException("Duplicate identifier: '" + name + "'");
@@ -236,13 +235,14 @@ public class MachineContext extends DepthFirstAdapter {
if (node.getHeader() != null) {
node.getHeader().apply(this);
}
- List<PMachineClause> copy = new ArrayList<PMachineClause>(
- node.getMachineClauses());
- PMachineClauseComparator comperator = new PMachineClauseComparator();
+
+
+ List<PMachineClause> machineClauses = node.getMachineClauses();
// Sort the machine clauses: declarations clauses first, then
// properties clauses
- Collections.sort(copy, comperator);
- for (PMachineClause e : copy) {
+ MachineClauseSorter.sortMachineClauses(start);
+
+ for (PMachineClause e : machineClauses) {
e.apply(this);
}
}
@@ -263,9 +263,9 @@ public class MachineContext extends DepthFirstAdapter {
String name = Utils.getIdentifierAsString(p.getIdentifier());
exist(p.getIdentifier());
if (Character.isUpperCase(name.charAt(0))) {
- this.setParameter.put(name, p);
+ this.machineSetParameter.put(name, p);
} else {
- this.scalarParameter.put(name, p);
+ this.machineScalarParameter.put(name, p);
}
}
}
@@ -283,6 +283,8 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
definitionMachineClause = node;
+ DefinitionsSorter.sortDefinitions(node);
+
List<PDefinition> copy = node.getDefinitions();
/*
@@ -341,7 +343,7 @@ public class MachineContext extends DepthFirstAdapter {
}
private void evalDefinitionName(String name, Node node) {
- existString(name);
+ identifierAlreadyExists(name);
definitions.put(name, node);
}
@@ -586,8 +588,8 @@ public class MachineContext extends DepthFirstAdapter {
this.constraintMachineClause = node;
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- this.contextTable.add(this.scalarParameter);
- this.contextTable.add(this.setParameter);
+ this.contextTable.add(this.machineScalarParameter);
+ this.contextTable.add(this.machineSetParameter);
if (node.getPredicates() != null) {
node.getPredicates().apply(this);
}
@@ -890,6 +892,22 @@ public class MachineContext extends DepthFirstAdapter {
node.getPredicates().apply(this);
contextTable.remove(contextTable.size() - 1);
}
+
+ @Override
+ public void caseAEventBComprehensionSetExpression(AEventBComprehensionSetExpression node){
+ contextTable.add(new LinkedHashMap<String, Node>());
+ {
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
+ }
+ }
+ node.getPredicates().apply(this);
+
+ node.getExpression().apply(this);
+ contextTable.remove(contextTable.size() - 1);
+ }
@Override
public void caseAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
@@ -991,11 +1009,11 @@ public class MachineContext extends DepthFirstAdapter {
}
public LinkedHashMap<String, Node> getSetParamter() {
- return setParameter;
+ return machineSetParameter;
}
public LinkedHashMap<String, Node> getScalarParameter() {
- return scalarParameter;
+ return machineScalarParameter;
}
public ArrayList<Node> getConstantArrayList() {
@@ -1126,42 +1144,3 @@ public class MachineContext extends DepthFirstAdapter {
}
-class PMachineClauseComparator implements Comparator<PMachineClause>,
- Serializable {
-
- private static final long serialVersionUID = 2606332412649258695L;
- private static Hashtable<Object, Integer> priority = new Hashtable<Object, Integer>();
- static {
- // declarations clauses
-
- 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);
- priority.put(ADefinitionsMachineClause.class, 6);
-
- // properties clauses
- priority.put(AConstraintsMachineClause.class, 5);
- priority.put(APropertiesMachineClause.class, 4);
- priority.put(AInvariantMachineClause.class, 3);
- priority.put(AAssertionsMachineClause.class, 2);
- priority.put(AOperationsMachineClause.class, 1);
- priority.put(AInitialisationMachineClause.class, 0);
- }
-
- public int compare(PMachineClause arg0, PMachineClause arg1) {
- if (priority.get(arg0.getClass()).intValue() < priority.get(
- arg1.getClass()).intValue()) {
- return 1;
- }
- if (priority.get(arg0.getClass()).intValue() > priority.get(
- arg1.getClass()).intValue()) {
- return -1;
- }
-
- return 0;
- }
-
-}
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index bcd4aaf60c7d3c823c9c67b354a866b48ca29cd4..8ff4abbe734a2f12e40c98ff195b220e5d24447e 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -230,39 +230,53 @@ public final class StandardMadules {
public static final boolean containsNameFromModuleRelations(String name) {
return Relations.contains(name);
}
-
+
/**
* External Functions
*
- * All external functions must be defined in the standard module ExternalFunctions.tla
- * (src/main/resources/standardModules/).
- * The B machine must contain a definition declaring the external function.
- * The typing definition (e.g. EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));)
- * is not mandatory.
+ * All external functions must be defined in the standard module
+ * ExternalFunctions.tla (src/main/resources/standardModules/). The B
+ * machine must contain a definition declaring the external function. The
+ * typing definition (e.g. EXTERNAL_FUNCTION_STRING_SPLIT ==
+ * ((STRING*STRING) --> (INTEGER<->STRING));) is not mandatory.
*
* The B definitions will be ignored in the {@link TLAPrinter}.
*
*
*/
-
+
public static final String EXTERNAL_printf = "printf";
public static final String INT_TO_STRING = "INT_TO_STRING";
public static final String STRING_SPLIT = "STRING_SPLIT";
public static final String SORT_SET = "SORT_SET";
public static final String STRING_APPEND = "STRING_APPEND";
+ public static final String STRING_TO_INT = "STRING_TO_INT";
+ public static final String DECIMAL_TO_INT = "DECIMAL_TO_INT";
private static final ArrayList<String> ExternalFunctions = new ArrayList<String>();
static {
ExternalFunctions.add(EXTERNAL_printf);
ExternalFunctions.add(INT_TO_STRING);
ExternalFunctions.add(STRING_SPLIT);
- ExternalFunctions.add(SORT_SET);
ExternalFunctions.add(STRING_APPEND);
+ ExternalFunctions.add(STRING_TO_INT);
+
+ ExternalFunctions.add(SORT_SET);
+ ExternalFunctions.add(DECIMAL_TO_INT);
}
- public static boolean isKeywordInModuleExternalFunctions(String name){
+ public static boolean isAbstractConstant(String name) {
+ if (name.equals(SORT_SET)
+ || name.equals(DECIMAL_TO_INT)) {
+ return true;
+ } else {
+ return false;
+ }
+
+ }
+
+ public static boolean isKeywordInModuleExternalFunctions(String name) {
return ExternalFunctions.contains(name);
}
-
-
+
}
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index f811ebd328eb5607c16449ecf1031cee3ee97454..cb927d6fdc779ae337b5f8c3e630f146dc3ad94a 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -2,7 +2,6 @@ package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.Collection;
-import java.util.Collections;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedList;
@@ -58,7 +57,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
checkLTLFormulas();
checkConstantsSetup();
-
+
}
private void checkLTLFormulas() {
@@ -133,9 +132,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
{
List<PMachineClause> copy = new ArrayList<PMachineClause>(
node.getMachineClauses());
- PMachineClauseComparator comperator = new PMachineClauseComparator();
- // Sort the machine clauses
- Collections.sort(copy, comperator);
for (PMachineClause e : copy) {
e.apply(this);
}
@@ -286,15 +282,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getRhs().apply(this);
}
-
-
@Override
public void caseADefinitionExpression(ADefinitionExpression node) {
BType expected = getType(node);
- String name = node.getDefLiteral().getText().toString();
- if(StandardMadules.isKeywordInModuleExternalFunctions(name)){
-
- }
+ // String name = node.getDefLiteral().getText().toString();
Node originalDef = referenceTable.get(node);
BType found = getType(originalDef);
@@ -309,7 +300,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
List<PExpression> copy = new ArrayList<PExpression>(
node.getParameters());
for (int i = 0; i < params.size(); i++) {
- setType(copy.get(i), getType(params.get(i)));
+ BType type = getType(params.get(i));
+ setType(copy.get(i), type);
copy.get(i).apply(this);
}
}
@@ -440,12 +432,15 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseAIdentifierExpression(AIdentifierExpression node) {
Node originalIdentifier = referenceTable.get(node);
BType expected = getType(node);
+
if (expected == null) {
System.out.println("Not implemented in Typechecker:"
+ node.parent().getClass());
throw new RuntimeException(node + " Pos: " + node.getStartPos());
}
BType found = getType(originalIdentifier);
+
+ String name = Utils.getIdentifierAsString(node.getIdentifier());
try {
expected.unify(found, this);
} catch (UnificationException e) {
@@ -453,7 +448,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
+ "' , found '" + found + "' at identifier " + node + "\n"
+ node.getStartPos());
}
-
}
@Override
@@ -1281,6 +1275,61 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
+
+ }
+
+ @Override
+ public void caseAEventBComprehensionSetExpression(
+ AEventBComprehensionSetExpression node) {
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression v = (AIdentifierExpression) e;
+ setType(v, new UntypedType());
+ }
+
+ setType(node.getPredicates(), BoolType.getInstance());
+ node.getPredicates().apply(this);
+
+ setType(node.getExpression(), new UntypedType());
+ node.getExpression().apply(this);
+
+
+ BType found = new SetType(getType(node.getExpression()));
+
+ BType expected = getType(node);
+ try {
+ found.unify(expected, this);
+ } catch (UnificationException e) {
+ throw new TypeErrorException("Excepted '" + expected + "' , found "
+ + found + "'");
+ }
+
+
+// List<PExpression> copy = new ArrayList<PExpression>(
+// node.getIdentifiers());
+// for (PExpression e : copy) {
+// AIdentifierExpression v = (AIdentifierExpression) e;
+// UntypedType u = new UntypedType();
+// setType(v, u);
+// }
+//
+// setType(node.getPredicates(), BoolType.getInstance());
+// node.getPredicates().apply(this);
+//
+// setType(node.getExpression(), new UntypedType());
+// node.getExpression().apply(this);
+//
+// BType expr = getType(node.getExpression());
+// System.out.println(getType(node.getExpression()));
+//
+// BType expected = getType(node);
+// SetType set = new SetType(getType(node.getExpression()));
+// unify(expected, set, node);
+// BType type = getType(node);
+// System.out.println(getType(node));
+
+
}
public static BType makePair(ArrayList<BType> list) {
@@ -1373,11 +1422,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
throw new TypeErrorException("Excepted '" + expected + "' , found "
+ found + "'");
}
-
+
setType(node.getExpression(), new UntypedType());
node.getExpression().apply(this);
BType type = getType(node.getExpression());
- if (! (type instanceof FunctionType)){
+ if (!(type instanceof FunctionType)) {
new SetType(new UntypedType()).unify(type, this);
}
}
@@ -1813,6 +1862,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
for (PExpression e : copy) {
setType(e, new UntypedType());
e.apply(this);
+ }
+
+ for (PExpression e : copy) {
list.add(getType(e));
}
@@ -2377,7 +2429,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
BType expected = getType(node);
try {
- found.unify(expected, this);
+ unify(expected, found, node);
} catch (UnificationException e) {
throw new TypeErrorException("Excepted '" + expected + "' , found "
+ found + "'");
@@ -2391,17 +2443,19 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
String fieldName = Utils.getIdentifierAsString(i.getIdentifier());
s.add(fieldName, new UntypedType());
setType(node.getRecord(), s);
+
node.getRecord().apply(this);
BType found = ((StructType) getType(node.getRecord()))
.getType(fieldName);
BType expected = getType(node);
try {
- found.unify(expected, this);
+ unify(expected, found, node);
} catch (UnificationException e) {
throw new TypeErrorException("Excepted '" + expected + "' , found "
+ found + "'");
}
+
}
@Override
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index 1068dedef3fa339587e16ab32d064e5ba8c099ae..38fb4969b12ec1767b1a9f59770cddde2821aefb 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -37,7 +37,11 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
private Hashtable<String, PDefinition> definitionsTable;
private ArrayList<Hashtable<String, PExpression>> contextStack;
- public DefinitionsEliminator(Start node) {
+ public static void eliminateDefinitions(Start start){
+ new DefinitionsEliminator(start);
+ }
+
+ private DefinitionsEliminator(Start node) {
DefinitionCollector collector = new DefinitionCollector(node);
definitionsTable = collector.getDefinitions();
contextStack = new ArrayList<Hashtable<String, PExpression>>();
@@ -61,9 +65,19 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
@Override
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
- List<PDefinition> copy = new ArrayList<PDefinition>(
+ /**
+ * Definitions from other definitions files were injected into the
+ * DefinitionsCLause. However, their parent was not correctly set to the
+ * DefinitionsClause. Hence e.replaceBy(null) would not eliminate them.
+ * Therefore, we have to create a new list and have to the use the
+ * setDefinitions method form {link ADefinitionsMachineClause}.
+ **/
+
+ List<PDefinition> newDefinitionsList = new ArrayList<PDefinition>();
+ List<PDefinition> oldDefinitionsList = new ArrayList<PDefinition>(
node.getDefinitions());
- for (PDefinition e : copy) {
+ for (PDefinition e : oldDefinitionsList) {
+ // replace all definitions calls inside the definitions bodies
if (e instanceof AExpressionDefinitionDefinition) {
String name = ((AExpressionDefinitionDefinition) e).getName()
.getText().toString();
@@ -74,26 +88,39 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
}
e.apply(this);
}
- for (PDefinition e : copy) {
+
+ // add certain definitions to the new definitions list in order to
+ // obtain them for the translation
+ for (PDefinition e : oldDefinitionsList) {
+
if (e instanceof AExpressionDefinitionDefinition) {
+
String name = ((AExpressionDefinitionDefinition) e).getName()
.getText().toString();
if (name.startsWith("ASSERT_LTL")
|| name.startsWith("scope_")
|| name.startsWith("SET_PREF_")
|| StandardMadules
- .isKeywordInModuleExternalFunctions(name))
- continue;
+ .isKeywordInModuleExternalFunctions(name)) {
+
+ newDefinitionsList.add(e);
+ }
} else if (e instanceof APredicateDefinitionDefinition) {
String name = ((APredicateDefinitionDefinition) e).getName()
.getText().toString();
if (name.equals("GOAL")
|| StandardMadules
- .isKeywordInModuleExternalFunctions(name))
- continue;
+ .isKeywordInModuleExternalFunctions(name)) {
+ newDefinitionsList.add(e);
+ }
}
- e.replaceBy(null);
}
+ for (PDefinition def : newDefinitionsList) {
+ // we have delete all parents of the definitions in order to set
+ // them in the next step (seems to be a bug in SabbleCC)
+ def.replaceBy(null);
+ }
+ node.setDefinitions(newDefinitionsList);
}
@Override
@@ -123,7 +150,6 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
@Override
public void caseADefinitionExpression(ADefinitionExpression node) {
-
String name = node.getDefLiteral().getText();
ArrayList<PExpression> arguments = new ArrayList<PExpression>(
node.getParameters());
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsSorter.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsSorter.java
new file mode 100644
index 0000000000000000000000000000000000000000..8061e7c03b8f8e5dbe773241407d025c297007af
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsSorter.java
@@ -0,0 +1,136 @@
+package de.tlc4b.analysis.transformation;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.LinkedHashMap;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.ADefinitionExpression;
+import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
+import de.be4.classicalb.core.parser.node.ADefinitionSubstitution;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
+import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.PDefinition;
+
+public class DefinitionsSorter extends DepthFirstAdapter {
+ final LinkedHashMap<String, HashSet<String>> dependencies;
+ final LinkedHashMap<String, HashSet<String>> allDependencies;
+ final LinkedHashMap<String, PDefinition> definitionsTable;
+ final ArrayList<PDefinition> res;
+ String current = null;
+
+ public DefinitionsSorter(ADefinitionsMachineClause clause) {
+ dependencies = new LinkedHashMap<String, HashSet<String>>();
+ allDependencies = new LinkedHashMap<String, HashSet<String>>();
+ definitionsTable = new LinkedHashMap<String, PDefinition>();
+ res = new ArrayList<PDefinition>();
+
+ clause.apply(this);
+
+ for (String defName : dependencies.keySet()) {
+ resolveDependencies(defName);
+ }
+
+ ArrayList<String> defs = new ArrayList<String>(allDependencies.keySet());
+
+
+ while (!res.containsAll(definitionsTable.values())) {
+ Iterator<String> iterator = new ArrayList<String>(defs).iterator();
+ while (iterator.hasNext()) {
+ String next = iterator.next();
+
+ HashSet<String> deps = allDependencies.get(next);
+
+ deps.retainAll(defs);
+
+ if (deps.size() == 0) {
+ PDefinition pDefinition = definitionsTable.get(next);
+ pDefinition.replaceBy(null);
+ res.add(pDefinition);
+ defs.remove(next);
+ }
+ }
+ }
+ clause.setDefinitions(res);
+
+ }
+
+ private void resolveDependencies(String defName) {
+ if (allDependencies.containsKey(defName)) {
+ return;
+ }
+ HashSet<String> allDeps = new HashSet<String>();
+ HashSet<String> deps = dependencies.get(defName);
+ for (String def : deps) {
+ resolveDependencies(def);
+ allDeps.add(def);
+ allDeps.addAll(allDependencies.get(def));
+ }
+ allDependencies.put(defName, allDeps);
+
+ }
+
+ public static void sortDefinitions(ADefinitionsMachineClause clause) {
+ new DefinitionsSorter(clause);
+
+ }
+
+ @Override
+ public void inAPredicateDefinitionDefinition(
+ APredicateDefinitionDefinition node) {
+ String name = node.getName().getText().toString();
+ addDefinition(name);
+ definitionsTable.put(name, node);
+ current = name;
+ }
+
+ @Override
+ public void inASubstitutionDefinitionDefinition(
+ ASubstitutionDefinitionDefinition node) {
+ String name = node.getName().getText().toString();
+ addDefinition(name);
+ definitionsTable.put(name, node);
+ current = name;
+ }
+
+ @Override
+ public void inAExpressionDefinitionDefinition(
+ AExpressionDefinitionDefinition node) {
+ String name = node.getName().getText().toString();
+ addDefinition(name);
+ definitionsTable.put(name, node);
+ current = name;
+ }
+
+ @Override
+ public void inADefinitionExpression(ADefinitionExpression node) {
+ String name = node.getDefLiteral().getText().toString();
+ addDefinitionCall(name);
+ }
+
+ @Override
+ public void inADefinitionPredicate(ADefinitionPredicate node) {
+ String name = node.getDefLiteral().getText().toString();
+ addDefinitionCall(name);
+ }
+
+ @Override
+ public void inADefinitionSubstitution(ADefinitionSubstitution node) {
+ String name = node.getDefLiteral().getText().toString();
+ addDefinitionCall(name);
+ }
+
+ private void addDefinition(String name) {
+ if (!dependencies.keySet().contains(name)) {
+ dependencies.put(name, new HashSet<String>());
+ }
+ }
+
+ private void addDefinitionCall(String name) {
+ dependencies.get(current).add(name);
+ }
+
+}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/MachineClauseSorter.java b/src/main/java/de/tlc4b/analysis/transformation/MachineClauseSorter.java
new file mode 100644
index 0000000000000000000000000000000000000000..98ea212bce3f8a25d12afc481a80b228c403667b
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/transformation/MachineClauseSorter.java
@@ -0,0 +1,87 @@
+package de.tlc4b.analysis.transformation;
+
+import java.io.Serializable;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.Hashtable;
+import java.util.LinkedList;
+
+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.AConcreteVariablesMachineClause;
+import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
+import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
+import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
+import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
+import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
+import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
+import de.be4.classicalb.core.parser.node.ASeesMachineClause;
+import de.be4.classicalb.core.parser.node.ASetsMachineClause;
+import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
+import de.be4.classicalb.core.parser.node.PMachineClause;
+import de.be4.classicalb.core.parser.node.Start;
+
+public class MachineClauseSorter extends DepthFirstAdapter {
+
+ public static void sortMachineClauses(Start start) {
+ MachineClauseSorter sorter = new MachineClauseSorter();
+ start.apply(sorter);
+ }
+
+ @Override
+ public void caseAAbstractMachineParseUnit(AAbstractMachineParseUnit node) {
+
+ LinkedList<PMachineClause> machineClauses = node.getMachineClauses();
+
+ PMachineClauseComparator comperator = new PMachineClauseComparator();
+ // Sort the machine clauses:
+ // 1. import clauses
+ // 2. declaration clauses
+ // 3. properties clauses
+ // 4. operation clauses
+ Collections.sort(machineClauses, comperator);
+ }
+}
+
+class PMachineClauseComparator implements Comparator<PMachineClause>,
+ Serializable {
+
+ private static final long serialVersionUID = 2606332412649258695L;
+ private static Hashtable<Object, Integer> priority = new Hashtable<Object, Integer>();
+ static {
+ // declarations clauses
+
+ 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);
+ priority.put(ADefinitionsMachineClause.class, 6);
+
+ // properties clauses
+ priority.put(AConstraintsMachineClause.class, 5);
+ priority.put(APropertiesMachineClause.class, 4);
+ priority.put(AInvariantMachineClause.class, 3);
+ priority.put(AAssertionsMachineClause.class, 2);
+ priority.put(AOperationsMachineClause.class, 1);
+ priority.put(AInitialisationMachineClause.class, 0);
+ }
+
+ public int compare(PMachineClause arg0, PMachineClause arg1) {
+ if (priority.get(arg0.getClass()).intValue() < priority.get(
+ arg1.getClass()).intValue()) {
+ return 1;
+ }
+ if (priority.get(arg0.getClass()).intValue() > priority.get(
+ arg1.getClass()).intValue()) {
+ return -1;
+ }
+
+ return 0;
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
new file mode 100644
index 0000000000000000000000000000000000000000..e7283719de7900fbd94a9a14f40cb3e530cbcb6d
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
@@ -0,0 +1,199 @@
+package de.tlc4b.analysis.transformation;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.LinkedHashMap;
+import java.util.LinkedList;
+import java.util.Map;
+
+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.AConjunctPredicate;
+import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
+import de.be4.classicalb.core.parser.node.ASeesMachineClause;
+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.Start;
+
+public class SeesEliminator extends DepthFirstAdapter {
+
+ private final Start main;
+ private final Map<String, Start> parsedMachines;
+
+ public static void eliminateSeesClauses(Start start,
+ Map<String, Start> parsedMachines) {
+ new SeesEliminator(start, parsedMachines);
+ }
+
+ private SeesEliminator(Start start, Map<String, Start> parsedMachines) {
+ this.main = start;
+ this.parsedMachines = parsedMachines;
+ MachineClauseSorter.sortMachineClauses(start);
+ start.apply(this);
+ }
+
+ public void inASeesMachineClause(ASeesMachineClause node) {
+ LinkedList<PExpression> machineNames = node.getMachineNames();
+ for (PExpression pExpression : machineNames) {
+ AIdentifierExpression id = (AIdentifierExpression) pExpression;
+ String identifierAsString = Utils.getIdentifierAsString(id
+ .getIdentifier());
+ Start start = parsedMachines.get(identifierAsString);
+ DefinitionsEliminator.eliminateDefinitions(start);
+ eliminateSeesClauses(start, parsedMachines);
+ new MachineClauseAdder(main, start);
+ if(node.parent() != null){
+ node.replaceBy(null);
+ }
+ }
+ }
+
+ class MachineClauseAdder extends DepthFirstAdapter {
+ private final ArrayList<PMachineClause> machineClausesList;
+ private final HashMap<Class<? extends PMachineClause>, PMachineClause> machineClauseHashMap;
+ private final LinkedList<PMachineClause> additionalMachineClauseList;
+
+ public MachineClauseAdder(Start main, Start start) {
+ this.machineClausesList = new ArrayList<PMachineClause>();
+ this.machineClauseHashMap = new LinkedHashMap<Class<? extends PMachineClause>, PMachineClause>();
+ this.additionalMachineClauseList = new LinkedList<PMachineClause>();
+
+ PParseUnit pParseUnit = main.getPParseUnit();
+ AAbstractMachineParseUnit machineParseUnit = (AAbstractMachineParseUnit) pParseUnit;
+
+ for (PMachineClause machineClause : machineParseUnit
+ .getMachineClauses()) {
+ machineClausesList.add(machineClause);
+ machineClauseHashMap.put(machineClause.getClass(),
+ machineClause);
+ }
+
+ start.apply(this);
+
+
+ LinkedList<PMachineClause> newMachineClauseList = new LinkedList<PMachineClause>();
+ for (PMachineClause pMachineClause : machineClausesList) {
+ pMachineClause.replaceBy(null); // delete parent of clause
+ newMachineClauseList.add(pMachineClause);
+ }
+ newMachineClauseList.addAll(additionalMachineClauseList);
+ machineParseUnit.setMachineClauses(newMachineClauseList);
+ }
+
+ @Override
+ public void caseAConstantsMachineClause(AConstantsMachineClause node) {
+ AConstantsMachineClause main = (AConstantsMachineClause) machineClauseHashMap
+ .get(node.getClass());
+
+ if (main != null) {
+ ArrayList<PExpression> oldConstantsList = new ArrayList<PExpression>(
+ main.getIdentifiers());
+ ArrayList<PExpression> newConstantsList = new ArrayList<PExpression>();
+ for (PExpression pExpression : oldConstantsList) {
+ pExpression.replaceBy(null); // delete parent
+ newConstantsList.add(pExpression);
+ }
+ ArrayList<PExpression> otherConstants = new ArrayList<PExpression>(
+ node.getIdentifiers());
+
+ for (PExpression pExpression : otherConstants) {
+ pExpression.replaceBy(null); // delete parent
+ newConstantsList.add(pExpression);
+
+ }
+ main.setIdentifiers(newConstantsList);
+ } else {
+ additionalMachineClauseList.add(node);
+ }
+ }
+
+ public void caseAAbstractConstantsMachineClause(
+ AAbstractConstantsMachineClause node) {
+ AAbstractConstantsMachineClause main = (AAbstractConstantsMachineClause) machineClauseHashMap
+ .get(node.getClass());
+
+ if (main != null) {
+ ArrayList<PExpression> oldConstantsList = new ArrayList<PExpression>(
+ main.getIdentifiers());
+ ArrayList<PExpression> newConstantsList = new ArrayList<PExpression>();
+ for (PExpression pExpression : oldConstantsList) {
+ pExpression.replaceBy(null); // delete parent
+ newConstantsList.add(pExpression);
+ }
+ ArrayList<PExpression> otherConstants = new ArrayList<PExpression>(
+ node.getIdentifiers());
+
+ for (PExpression pExpression : otherConstants) {
+ pExpression.replaceBy(null); // delete parent
+ newConstantsList.add(pExpression);
+
+ }
+ main.setIdentifiers(newConstantsList);
+ } else {
+ additionalMachineClauseList.add(node);
+ }
+
+ }
+
+ @Override
+ public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
+ APropertiesMachineClause main = null;
+ for (PMachineClause clause : machineClausesList) {
+ if (clause instanceof APropertiesMachineClause) {
+ main = (APropertiesMachineClause) clause;
+ }
+ }
+
+ if (main != null) {
+ AConjunctPredicate con = new AConjunctPredicate();
+ con.setLeft(main.getPredicates());
+ con.setRight(node.getPredicates());
+ main.setPredicates(con);
+ } else {
+ additionalMachineClauseList.add(node);
+ }
+
+ }
+
+ @Override
+ public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
+ ADefinitionsMachineClause main = null;
+ for (PMachineClause clause : machineClausesList) {
+ if (clause instanceof ADefinitionsMachineClause) {
+ main = (ADefinitionsMachineClause) clause;
+ }
+ }
+
+ if (main != null) {
+ ArrayList<PDefinition> oldDefinitions = new ArrayList<PDefinition>(
+ main.getDefinitions());
+ ArrayList<PDefinition> newDefinitionsList = new ArrayList<PDefinition>();
+ for (PDefinition pExpression : oldDefinitions) {
+ pExpression.replaceBy(null); // delete parent
+ newDefinitionsList.add(pExpression);
+ }
+ ArrayList<PDefinition> otherConstants = new ArrayList<PDefinition>(
+ node.getDefinitions());
+
+ for (PDefinition definition : otherConstants) {
+ if (definition.parent() != null) {
+ definition.replaceBy(null); // delete parent
+ }
+ newDefinitionsList.add(definition);
+
+ }
+ main.setDefinitions(newDefinitionsList);
+ } else {
+ additionalMachineClauseList.add(node);
+ }
+ }
+
+ }
+}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
new file mode 100644
index 0000000000000000000000000000000000000000..1207e8b7afc1262e68606c1a8f7c6066ba1df5bb
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -0,0 +1,265 @@
+package de.tlc4b.analysis.transformation;
+
+import java.util.ArrayList;
+import java.util.Hashtable;
+import java.util.LinkedList;
+
+import de.be4.classicalb.core.parser.Utils;
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
+import de.be4.classicalb.core.parser.node.AConjunctPredicate;
+import de.be4.classicalb.core.parser.node.ACoupleExpression;
+import de.be4.classicalb.core.parser.node.ADomainExpression;
+import de.be4.classicalb.core.parser.node.AEqualPredicate;
+import de.be4.classicalb.core.parser.node.AEventBComprehensionSetExpression;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.Start;
+
+public class SetComprehensionOptimizer extends DepthFirstAdapter {
+
+ public static void optimizeSetComprehensions(Start start) {
+ SetComprehensionOptimizer optimizer = new SetComprehensionOptimizer();
+ start.apply(optimizer);
+ }
+
+ @Override
+ public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
+ if (node.parent() instanceof ADomainExpression) {
+ LinkedList<PExpression> identifiers = node.getIdentifiers();
+
+ final ArrayList<String> list = new ArrayList<String>();
+ final AIdentifierExpression last = (AIdentifierExpression) identifiers
+ .getLast();
+ for (int i = 0; i < identifiers.size() - 1; i++) {
+ AIdentifierExpression id = (AIdentifierExpression) identifiers
+ .get(i);
+ String name = Utils.getIdentifierAsString(id.getIdentifier());
+ list.add(name);
+ }
+
+ Hashtable<String, PExpression> values = new Hashtable<String, PExpression>();
+ ArrayList<AEqualPredicate> equalList = new ArrayList<AEqualPredicate>();
+ analysePredicate(node.getPredicates(), list, values, equalList);
+
+ if (values.keySet().containsAll(list)) {
+ // delete nodes
+ new NodesRemover(node.getPredicates(), equalList, values);
+
+ AEventBComprehensionSetExpression eventBcomprehension = new AEventBComprehensionSetExpression();
+ ArrayList<PExpression> ids = new ArrayList<PExpression>();
+ ids.add(last);
+ eventBcomprehension.setIdentifiers(ids);
+
+ ACoupleExpression couple = new ACoupleExpression();
+
+ ArrayList<PExpression> exprs = new ArrayList<PExpression>();
+ for (int i = 0; i < list.size(); i++) {
+ exprs.add(values.get(list.get(i)));
+ }
+ couple.setList(exprs);
+ eventBcomprehension.setExpression(couple);
+
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft((AIdentifierExpression) last.clone());
+ AComprehensionSetExpression compre = new AComprehensionSetExpression();
+ ArrayList<PExpression> ids2 = new ArrayList<PExpression>();
+ ids2.add((AIdentifierExpression) last.clone());
+ compre.setIdentifiers(ids2);
+ compre.setPredicates(node.getPredicates());
+ member.setRight(compre);
+ eventBcomprehension.setPredicates(member);
+
+ node.parent().replaceBy(eventBcomprehension);
+
+ eventBcomprehension.apply(this);
+ }
+ }
+
+ if (node.parent() != null)
+ testGeneric(node);
+
+ }
+
+ private void testGeneric(AComprehensionSetExpression node) {
+ final LinkedList<PExpression> identifiers = node.getIdentifiers();
+ final ArrayList<String> list = new ArrayList<String>();
+ final Hashtable<String, AIdentifierExpression> identifierTable = new Hashtable<String, AIdentifierExpression>();
+ for (int i = 0; i < identifiers.size(); i++) {
+ AIdentifierExpression id = (AIdentifierExpression) identifiers
+ .get(i);
+ String name = Utils.getIdentifierAsString(id.getIdentifier());
+ list.add(name);
+ identifierTable.put(name, id);
+ }
+
+ Hashtable<String, PExpression> values = new Hashtable<String, PExpression>();
+ ArrayList<AEqualPredicate> equalList = new ArrayList<AEqualPredicate>();
+ analysePredicate(node.getPredicates(), list, values, equalList);
+ if (values.size() > 0 && list.size()-values.size() > 0) {
+ // delete nodes
+ new NodesRemover(node.getPredicates(), equalList, values);
+
+ AEventBComprehensionSetExpression eventBcomprehension = new AEventBComprehensionSetExpression();
+ ArrayList<PExpression> ids = new ArrayList<PExpression>();
+ ArrayList<PExpression> ids2 = new ArrayList<PExpression>();
+ ArrayList<PExpression> ids3 = new ArrayList<PExpression>();
+ for (String p : list) {
+ if (!values.containsKey(p)) {
+ PExpression clone = (PExpression) identifierTable.get(p)
+ .clone();
+ ids.add(clone);
+ PExpression clone2 = (PExpression) identifierTable.get(p)
+ .clone();
+ ids2.add(clone2);
+ PExpression clone3 = (PExpression) identifierTable.get(p)
+ .clone();
+ ids3.add(clone3);
+ }
+ }
+ eventBcomprehension.setIdentifiers(ids);
+
+ ACoupleExpression couple = new ACoupleExpression();
+ ArrayList<PExpression> exprs = new ArrayList<PExpression>();
+ for (int i = 0; i < list.size(); i++) {
+ String name = list.get(i);
+ if (values.containsKey(name)) {
+ exprs.add(values.get(name));
+ } else {
+ PExpression clone = (PExpression) identifierTable.get(name)
+ .clone();
+ exprs.add(clone);
+ }
+
+ }
+ couple.setList(exprs);
+ eventBcomprehension.setExpression(couple);
+
+ AMemberPredicate member = new AMemberPredicate();
+ if (ids2.size() > 1) {
+ ACoupleExpression couple2 = new ACoupleExpression();
+ couple2.setList(ids2);
+ member.setLeft(couple2);
+ } else {
+ member.setLeft(ids2.get(0));
+ }
+
+ AComprehensionSetExpression compre = new AComprehensionSetExpression();
+ compre.setIdentifiers(ids3);
+ compre.setPredicates(node.getPredicates());
+ member.setRight(compre);
+ eventBcomprehension.setPredicates(member);
+
+ node.replaceBy(eventBcomprehension);
+
+ eventBcomprehension.apply(this);
+ }
+
+ }
+
+ private void analysePredicate(PPredicate predicate, ArrayList<String> list,
+ Hashtable<String, PExpression> values,
+ ArrayList<AEqualPredicate> equalList) {
+ if (predicate instanceof AConjunctPredicate) {
+ AConjunctPredicate con = (AConjunctPredicate) predicate;
+ analysePredicate(con.getLeft(), list, values, equalList);
+ analysePredicate(con.getRight(), list, values, equalList);
+ } else if (predicate instanceof AEqualPredicate) {
+ AEqualPredicate equal = (AEqualPredicate) predicate;
+ if (equal.getLeft() instanceof AIdentifierExpression) {
+ AIdentifierExpression id = (AIdentifierExpression) equal
+ .getLeft();
+ String name = Utils.getIdentifierAsString(id.getIdentifier());
+ if (list.contains(name) && !values.containsKey(name)) {
+ if (equal.getRight() instanceof AIdentifierExpression) {
+ AIdentifierExpression id2 = (AIdentifierExpression) equal
+ .getRight();
+ String name2 = Utils.getIdentifierAsString(id2
+ .getIdentifier());
+ if (values.containsKey(name2)){
+ return;
+ }
+ }
+ equalList.add(equal);
+ values.put(name, equal.getRight());
+ }
+ } else if (!equalList.contains(equal)
+ && equal.getRight() instanceof AIdentifierExpression) {
+ AIdentifierExpression id = (AIdentifierExpression) equal
+ .getRight();
+ String name = Utils.getIdentifierAsString(id.getIdentifier());
+ if (list.contains(name) && !values.containsKey(name)) {
+ if (equal.getLeft() instanceof AIdentifierExpression) {
+ AIdentifierExpression id2 = (AIdentifierExpression) equal
+ .getLeft();
+ String name2 = Utils.getIdentifierAsString(id2
+ .getIdentifier());
+ if (values.contains(name2))
+ return;
+ }
+ equalList.add(equal);
+ values.put(name, equal.getLeft());
+ }
+ }
+
+ }
+ }
+
+ class NodesRemover extends DepthFirstAdapter {
+ final ArrayList<AEqualPredicate> removeList;
+ final Hashtable<String, PExpression> values;
+
+ public NodesRemover(PPredicate predicate,
+ ArrayList<AEqualPredicate> equalList,
+ Hashtable<String, PExpression> values) {
+ this.removeList = equalList;
+ this.values = values;
+
+ for (AEqualPredicate pred : removeList) {
+ pred.replaceBy(null);
+ }
+
+ predicate.apply(this);
+
+ }
+
+ @Override
+ public void caseAConjunctPredicate(AConjunctPredicate node) {
+ if (node.getLeft() != null) {
+ node.getLeft().apply(this);
+ }
+ if (node.getRight() != null) {
+ node.getRight().apply(this);
+ }
+ outAConjunctPredicate(node);
+ }
+
+ @Override
+ public void outAConjunctPredicate(AConjunctPredicate node) {
+ if (node.parent() != null) {
+ if (node.getLeft() == null && node.getRight() == null) {
+ node.replaceBy(null);
+ } else if (node.getLeft() == null) {
+ PPredicate right = node.getRight();
+ node.replaceBy(right);
+ } else if (node.getRight() == null) {
+ node.replaceBy(node.getLeft());
+ }
+ }
+ }
+
+ @Override
+ public void caseAIdentifierExpression(AIdentifierExpression node) {
+ String name = Utils.getIdentifierAsString(node.getIdentifier());
+
+ PExpression value = values.get(name);
+ if (value != null) {
+ node.replaceBy((PExpression) value.clone());
+ }
+
+ }
+ }
+
+}
diff --git a/src/main/java/de/tlc4b/btypes/PairType.java b/src/main/java/de/tlc4b/btypes/PairType.java
index 6e3afd0f305a7f879f01a5057608f0257e1469f0..4d7d141622b9d22ac3f80317e20afd7a731a065c 100644
--- a/src/main/java/de/tlc4b/btypes/PairType.java
+++ b/src/main/java/de/tlc4b/btypes/PairType.java
@@ -64,16 +64,24 @@ public class PairType extends AbstractHasFollowers {
@Override
public String toString() {
String res = "";
- if (first instanceof PairType) {
- res += "(" + first + ")";
- } else
- res += first;
- res += "*";
- if (second instanceof PairType) {
- res += "(" + second + ")";
- } else
- res += second;
- return res;
+ if(this.equals(first)|| this.equals(second)){
+ res += "(Recursive Type)";
+ return res;
+ }else{
+ if (first instanceof PairType) {
+ res += "(" + first + ")";
+ } else
+ res += first;
+ res += "*";
+ if (second instanceof PairType) {
+ res += "(" + second + ")";
+ } else
+ res += second;
+ return res;
+ }
+
+
+
}
public boolean isUntyped() {
@@ -95,6 +103,9 @@ public class PairType extends AbstractHasFollowers {
@Override
public boolean contains(BType other) {
+ if (this.equals(this.first) || this.equals(this.second)) {
+ return true;
+ }
if (this.first.equals(other) || this.second.equals(other)) {
return true;
}
diff --git a/src/main/java/de/tlc4b/btypes/SetType.java b/src/main/java/de/tlc4b/btypes/SetType.java
index 2661434a1ecc1ecad02c24958d94fef2884a5831..cc3d3613a0ce8f4867c1d5a4cb974d2e57ce5028 100644
--- a/src/main/java/de/tlc4b/btypes/SetType.java
+++ b/src/main/java/de/tlc4b/btypes/SetType.java
@@ -56,7 +56,12 @@ public class SetType extends AbstractHasFollowers {
@Override
public String toString() {
- return "POW(" + subtype + ")";
+ if(this.equals(subtype)){
+ return "POW(recursive call)";
+ }else{
+ return "POW(" + subtype + ")";
+ }
+
}
public boolean isUntyped() {
@@ -81,6 +86,9 @@ public class SetType extends AbstractHasFollowers {
@Override
public boolean contains(BType other) {
+ if(this.equals(subtype)){
+ return true;
+ }
if (this.subtype.equals(other)) {
return true;
}
diff --git a/src/main/java/de/tlc4b/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
index 100ce21cdf92031aa8408b7aafe6537c733cead7..1466385fdc3afd6446c54d989b42bdd33d86c15b 100644
--- a/src/main/java/de/tlc4b/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -97,13 +97,19 @@ public class StructType extends AbstractHasFollowers {
BType res = this.types.get(fieldName).unify(sType,
typechecker);
this.types.put(fieldName, res);
+ if(res instanceof AbstractHasFollowers){
+ ((AbstractHasFollowers) res).addFollower(this);
+ }
} else {
+ this.types.put(fieldName, sType);
if (sType instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) sType).addFollower(this);
+ AbstractHasFollowers f = (AbstractHasFollowers) sType;
+ f.deleteFollower(other);
+ f.addFollower(this);
}
- this.types.put(fieldName, sType);
}
}
+ ((StructType) other).setFollowersTo(this, typechecker);
complete = this.complete || s.complete;
return this;
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 8276701550722999f06042be7a4ed60ef37cdc7b..0f2190c500b259351f805a4008d9036925b43ae9 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -310,8 +310,8 @@ public class TLAPrinter extends DepthFirstAdapter {
if (i > 0) {
moduleStringAppend(", ");
}
- moduleStringAppend(usedStandardModules.getExtendedModules().get(i)
- .toString());
+ moduleStringAppend(usedStandardModules.getExtendedModules()
+ .get(i).toString());
}
moduleStringAppend("\n");
}
@@ -325,7 +325,7 @@ public class TLAPrinter extends DepthFirstAdapter {
def.getDefName().apply(this);
continue;
}
-
+
def.getDefName().apply(this);
moduleStringAppend(" == ");
Node e = def.getDefinition();
@@ -1115,7 +1115,8 @@ public class TLAPrinter extends DepthFirstAdapter {
if (name == null) {
name = Utils.getIdentifierAsString(node.getIdentifier());
}
- if(name.equals(SORT_SET)){
+ if (StandardMadules.isAbstractConstant(name)) {
+ // in order to pass the member check
moduleStringAppend("{}");
return;
}
@@ -1325,7 +1326,7 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAExpressionDefinitionDefinition(
AExpressionDefinitionDefinition node) {
String oldName = node.getName().getText().trim();
- if(StandardMadules.isKeywordInModuleExternalFunctions(oldName)){
+ if (StandardMadules.isKeywordInModuleExternalFunctions(oldName)) {
return;
}
String name = renamer.getName(node);
@@ -1368,7 +1369,7 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printBDefinition(String name, List<PExpression> args,
Node rightSide) {
- if(StandardMadules.isKeywordInModuleExternalFunctions(name)){
+ if (StandardMadules.isKeywordInModuleExternalFunctions(name)) {
return;
}
moduleStringAppend(name);
@@ -1777,26 +1778,26 @@ public class TLAPrinter extends DepthFirstAdapter {
// Function call
public void caseAFunctionExpression(AFunctionExpression node) {
inAFunctionExpression(node);
-
-
- if(node.getIdentifier() instanceof AIdentifierExpression){
- AIdentifierExpression id = (AIdentifierExpression) node.getIdentifier();
+
+ if (node.getIdentifier() instanceof AIdentifierExpression) {
+ AIdentifierExpression id = (AIdentifierExpression) node
+ .getIdentifier();
String name = Utils.getIdentifierAsString(id.getIdentifier());
- if(name.equals(SORT_SET)){
- moduleStringAppend(SORT_SET);
- //node.getIdentifier().apply(this);
+ if (StandardMadules.isAbstractConstant(name)) {
+
+ moduleStringAppend(name);
+ // node.getIdentifier().apply(this);
moduleStringAppend("(");
List<PExpression> copy = new ArrayList<PExpression>(
node.getParameters());
copy.get(0).apply(this);
moduleStringAppend(")");
return;
-
+
}
}
-
-
+
BType type = this.typechecker.getType(node.getIdentifier());
if (type instanceof FunctionType) {
node.getIdentifier().apply(this);
@@ -2132,6 +2133,20 @@ public class TLAPrinter extends DepthFirstAdapter {
outAComprehensionSetExpression(node);
}
+ @Override
+ public void caseAEventBComprehensionSetExpression(
+ AEventBComprehensionSetExpression node) {
+ inAEventBComprehensionSetExpression(node);
+
+ moduleStringAppend("{");
+ node.getExpression().apply(this);
+ moduleStringAppend(": ");
+ node.getPredicates().apply(this);
+ moduleStringAppend("}");
+
+ outAEventBComprehensionSetExpression(node);
+ }
+
private void printAuxiliaryVariables(int size) {
for (int i = 0; i < size - 1; i++) {
moduleStringAppend("<<");
@@ -2704,7 +2719,8 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAIseqExpression(AIseqExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
- if (node.parent() instanceof AMemberPredicate
+
+ if (isElementOfRecursive(node.parent())
&& !typeRestrictor.isARemovedNode(node.parent())) {
moduleStringAppend(REL_INJECTIVE_SEQUENCE_ELEMENT_OF);
} else {
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index d95c8f6b91c1eb32b1d6b3b6bf61f2912f580dc4..d055a7e270cbce5abeba1fe33c77f0bdd89c81a6 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -343,7 +343,9 @@ public class TLCResults implements ToolGlobals {
private TLCResult evaluatingParameter(String[] params) {
for (int i = 0; i < params.length; i++) {
String s = params[i];
- if (s.contains("not enumerable")) {
+ if (s == null) {
+ break;
+ } else if (s.contains("not enumerable")) {
return EnumerationError;
} else if (s.contains("The invariant of Assertion")) {
return AssertionError;
diff --git a/src/main/resources/standardModules/ExternalFunctions.tla b/src/main/resources/standardModules/ExternalFunctions.tla
index ca46e6a219bd64b9fb22874740fe037d81e4e384..81f00fbcdad3d4ae9ee59c1baafb9d35d2f193f8 100644
--- a/src/main/resources/standardModules/ExternalFunctions.tla
+++ b/src/main/resources/standardModules/ExternalFunctions.tla
@@ -5,22 +5,22 @@ EXTENDS Sequences, Integers, TLC, FiniteSets
(* Strings *)
RECURSIVE SPLIT1(_,_,_,_)
LOCAL SPLIT1(s,c,start,i) ==
- CASE i = Len(s)+1 -> IF i /= start
- THEN <<SubSeq(s,start,i-1)>>
+ CASE i = Len(s)+1 -> IF i /= start
+ THEN <<SubSeq(s,start,i-1)>>
ELSE <<>>
[] i+Len(c)-1 > Len(s) -> <<SubSeq(s,start,Len(s))>>
- [] SubSeq(s,i,i+Len(c)-1) = c -> IF i /= start
- THEN <<SubSeq(s,start,i-1)>> \o SPLIT1(s,c,i+Len(c),i+Len(c))
- ELSE <<>> \o SPLIT1(s,c,i+Len(c),i+Len(c))
+ [] SubSeq(s,i,i+Len(c)-1) = c -> IF i /= start
+ THEN <<SubSeq(s,start,i-1)>> \o SPLIT1(s,c,i+Len(c),i+Len(c))
+ ELSE <<>> \o SPLIT1(s,c,i+Len(c),i+Len(c))
[] OTHER -> SPLIT1(s,c,start,i+1)
STRING_SPLIT(s, c) == SPLIT1(s,c,1,1)
-LOCAL DIGIT_TO_STRING(x) ==
+LOCAL DIGIT_TO_STRING(x) ==
CASE x = 0 -> "0"
[] x = 1 -> "1"
- [] x= 2 -> "2"
+ [] x= 2 -> "2"
[] x = 3 -> "3"
[] x = 4 -> "4"
[] x= 5 -> "5"
@@ -30,26 +30,63 @@ LOCAL DIGIT_TO_STRING(x) ==
[] 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)
+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) ==
+ IF i < 0
+ THEN "-" \o INT_TO_STRING1(-i)
+ ELSE INT_TO_STRING1(i)
-LOCAL Max(S) == CHOOSE x \in S : \A p \in S : x >= p
+LOCAL Max(S) == CHOOSE x \in S : \A p \in S : x >= p
RECURSIVE SORT_SET(_)
SORT_SET(s) ==
- IF s = {}
- THEN {}
- ELSE LET max == Max(s)
- IN SORT_SET(s\{max}) \cup {<<Cardinality(s), max>>}
-
-STRING_APPEND(a,b) == a \o b
+ IF s = {}
+ THEN {}
+ ELSE LET max == Max(s)
+ IN SORT_SET(s\{max}) \cup {<<Cardinality(s), max>>}
+
+STRING_APPEND(a,b) == a \o b
+
+STRING_TO_INT(str) ==
+ LET
+ STRINGDIGIT_TO_INT(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
+
+ item(s,i) == SubSeq(s,i,i)
+
+ RECURSIVE pow(_,_)
+ pow(a,b) == IF b = 0 THEN 1 ELSE a * pow(a,b-1)
+
+ RECURSIVE STRING_TO_INT1(_,_)
+ STRING_TO_INT1(s, i) ==
+ IF i = Len(s)
+ THEN STRINGDIGIT_TO_INT(item(s,i))
+ ELSE STRINGDIGIT_TO_INT(item(s,i)) * pow(10,Len(s)-i) + STRING_TO_INT1(s,i+1)
+ IN
+ IF item(str, 1) = "-"
+ THEN -1 * STRING_TO_INT1(SubSeq(str,2,Len(str)),1)
+ ELSE STRING_TO_INT1(str,1)
+
+DECIMAL_TO_INT(s) ==
+ STRING_TO_INT(
+ STRING_APPEND(
+ (STRING_SPLIT(s,"."))[1]
+ ,(STRING_SPLIT(s,"."))[2]
+ )
+ )
-----------------------------------------------------------------------------
printf(s,v) == PrintT(s) /\ PrintT(v)
-
-=============================================================================
\ No newline at end of file
+
+=============================================================================
diff --git a/src/test/java/de/tlc4b/analysis/DeferredSetSize.java b/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
similarity index 75%
rename from src/test/java/de/tlc4b/analysis/DeferredSetSize.java
rename to src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
index a97c0aabdd53397cad209c8974ceca5ffd633098..b83222309c31d06bd25722644eabea0e9d09a166 100644
--- a/src/test/java/de/tlc4b/analysis/DeferredSetSize.java
+++ b/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
@@ -1,10 +1,10 @@
package de.tlc4b.analysis;
-import static de.tlc4b.util.TestUtil.compareConfig;
+import static de.tlc4b.util.TestUtil.compareModuleAndConfig;
import org.junit.Test;
-public class DeferredSetSize {
+public class DeferredSetSizeTest {
@Test
public void testDeferredSetStandard() throws Exception {
String machine = "MACHINE test\n"
@@ -14,7 +14,7 @@ public class DeferredSetSize {
+ "CONSTANTS S\n"
+ "======";
String expectedConfig = "CONSTANTS S = {S1, S2, S3} ";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@Test
@@ -29,7 +29,7 @@ public class DeferredSetSize {
+ "ASSUME Cardinality(S) = 4 \n"
+ "======";
String expectedConfig = "CONSTANTS S = {S1, S2, S3, S4} ";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@Test
@@ -44,6 +44,6 @@ public class DeferredSetSize {
+ "ASSUME 4 = Cardinality(S) \n"
+ "======";
String expectedConfig = "CONSTANTS S = {S1, S2, S3, S4} ";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
}
diff --git a/src/test/java/de/tlc4b/analysis/NotSupportedTest.java b/src/test/java/de/tlc4b/analysis/NotSupportedTest.java
deleted file mode 100644
index e7e67a600cce7e176736fe7918ae797162e8f690..0000000000000000000000000000000000000000
--- a/src/test/java/de/tlc4b/analysis/NotSupportedTest.java
+++ /dev/null
@@ -1,16 +0,0 @@
-package de.tlc4b.analysis;
-
-import static de.tlc4b.util.TestUtil.checkMachine;
-
-import org.junit.Test;
-
-import de.tlc4b.exceptions.NotSupportedException;
-
-public class NotSupportedTest {
-
- @Test(expected = NotSupportedException.class)
- public void testDuplicateSeenMachine() throws Exception {
- String machine = "MACHINE test \n" + "SEES M1 \n" + "END";
- checkMachine(machine);
- }
-}
diff --git a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..d433d16336656001e289cb83c27c71ccefbce8f5
--- /dev/null
+++ b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
@@ -0,0 +1,32 @@
+package de.tlc4b.analysis;
+
+import static de.tlc4b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class SetComprehensionOptimizerTest {
+
+ @Test
+ public void testSetComprehension1() throws Exception {
+ String machine = "MACHINE test\n"
+ + "CONSTANTS k \n"
+ + "PROPERTIES k = {x,y | x : 1..10 & y = x + 1} \n" + "END";
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Naturals\n"
+ + "k == {<<x, x + 1>>: x \\in {x \\in ((1 .. 10)): TRUE}} \n"
+ + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testSetComprehension2() throws Exception {
+ String machine = "MACHINE test\n"
+ + "CONSTANTS k \n"
+ + "PROPERTIES k = {x,y| x : 1..10 & x = y & y = x} \n" + "END";
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Naturals\n"
+ + "k == {<<x, x + 1>>: x \\in {x \\in ((1 .. 10)): TRUE}} \n"
+ + "======";
+ compare(expected, machine);
+ }
+}
diff --git a/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java b/src/test/java/de/tlc4b/coverage/CoverageTest.java
similarity index 89%
rename from src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
rename to src/test/java/de/tlc4b/coverage/CoverageTest.java
index 9614e6fccdac24e6def4855a1146ebb928214694..a106b1f20a8fee813f5516f57ea6df335af43583 100644
--- a/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
+++ b/src/test/java/de/tlc4b/coverage/CoverageTest.java
@@ -14,11 +14,11 @@ import de.tlc4b.util.PolySuite.Config;
import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
-public class IntegrationCoverageTest extends AbstractParseMachineTest {
+public class CoverageTest extends AbstractParseMachineTest {
private final File machine;
- public IntegrationCoverageTest(File machine, TLCResult result) {
+ public CoverageTest(File machine, TLCResult result) {
this.machine = machine;
}
diff --git a/src/test/java/de/tlc4b/exceptions/ScopeExceptionTest.java b/src/test/java/de/tlc4b/exceptions/ScopeExceptionTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..cb422859ca52816e2fb1c44d4efea31234006c2a
--- /dev/null
+++ b/src/test/java/de/tlc4b/exceptions/ScopeExceptionTest.java
@@ -0,0 +1,48 @@
+package de.tlc4b.exceptions;
+
+import static de.tlc4b.util.TestUtil.checkMachine;
+
+import org.junit.Test;
+
+public class ScopeExceptionTest {
+
+ @Test (expected = ScopeException.class)
+ public void testDuplicateIdentifierEnumeratedSet() throws Exception {
+ String machine = "MACHINE test\n"
+ + "SETS S; S ={A,B} \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testDuplicateIdentifierDeferredSet() throws Exception {
+ String machine = "MACHINE test\n"
+ + "SETS S; S \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testDuplicateIdentifierEnumValue() throws Exception {
+ String machine = "MACHINE test\n"
+ + "SETS S= {a,a} \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testDuplicateIdentifierMachineSetParameterDeferredSet() throws Exception {
+ String machine = "MACHINE test(AB, AB)\n"
+ + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = ScopeException.class)
+ public void testDuplicateIdentifierMachineScalarParameter() throws Exception {
+ String machine = "MACHINE test(a, a)\n"
+ + "CONSTRAINTS a : BOOL \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+}
diff --git a/src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java b/src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java
index f57b8edd2a473bd9d6618b10d9145f12b2b1ad57..4a3e57327ccd597a123e7b05e5155272042c3daa 100644
--- a/src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java
@@ -7,11 +7,15 @@ import org.junit.Test;
public class EnumeratedSetsTest {
@Test
public void testTwoEnumeratedSets() throws Exception {
- String machine = "MACHINE test\n" + "SETS set = {a,b,c}; set2 = {d}\n"
+ String machine = "MACHINE test\n"
+ + "SETS set = {a,b,c}; set2 = {d}\n"
+ "END";
- String expected = "---- MODULE test ----\n" + "CONSTANTS a, b, c, d\n"
- + "set == {a, b, c}\n" + "set2 == {d}\n" + "====";
+ String expected = "---- MODULE test ----\n"
+ + "CONSTANTS a, b, c, d\n"
+ + "set == {a, b, c}\n"
+ + "set2 == {d}\n"
+ + "====";
final String config = "CONSTANTS\na = a\nb = b\nc = c\nd = d\n";
compareEqualsConfig(expected, config, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
index 9c5dcc8d3c803d90eb6f7ae187f9e753bc0ce0a4..c26f8ceadf80386dd5db1b028bf9d5b225d8d70c 100644
--- a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
@@ -30,7 +30,7 @@ public class MachineParameterTest {
+ "Next == 1 = 2 /\\ UNCHANGED <<a>>\n"
+ "======";
String expectedConfig = "INIT Init\nNEXT Next";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@Test
@@ -55,7 +55,7 @@ public class MachineParameterTest {
+ "CONSTANTS AA\n"
+ "======";
String expectedConfig = "CONSTANTS AA = {AA1, AA2, AA3}";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@Test
@@ -70,7 +70,7 @@ public class MachineParameterTest {
+ "ASSUME Cardinality(B) = 2\n"
+ "====";
String expectedConfig = "CONSTANTS B = {B1, B2, B3}";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
}
diff --git a/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java b/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
index 5a7795c686c3cbb0c9ffcbf2fbd4120ca95f3ec6..b5faf7e61d667ba89e97d2b1a16b19236cbc27e1 100644
--- a/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
@@ -6,7 +6,7 @@ import org.junit.Test;
public class SetsClauseTest {
@Test
- public void testDefferedSet() throws Exception {
+ public void testDeferredSet() throws Exception {
String machine = "MACHINE test\n"
+ "SETS d \n"
+ "END";
@@ -16,7 +16,23 @@ public class SetsClauseTest {
String expectedConfig = "CONSTANTS\n" +
"d = {d1, d2, d3}\n";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
+ }
+
+ @Test
+ public void testDeferredSet2() throws Exception {
+ String machine = "MACHINE test\n"
+ + "SETS d \n"
+ + "CONSTANTS k \n"
+ + "PROPERTIES k : d \n"
+ + "END";
+ String expectedModule = "---- MODULE test----\n"
+ + "CONSTANTS d2asisdfapsdjfa\n"
+ + "======";
+ String expectedConfig = "CONSTANTS\n" +
+ "d = {d1, d2, d3}\n";
+
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@Test
@@ -29,6 +45,6 @@ public class SetsClauseTest {
+ "S == {a, b, c}"
+ "======";
String expectedConfig = "CONSTANTS a = a\n b = b \n c = c";
- compareConfig(expectedModule, expectedConfig, machine);
+ compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
}
diff --git a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
index a3531aea3b72eed388ca5a01c286a434bfb1e1b9..743559e754f9877a34aac5247472c71c8729261b 100644
--- a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
@@ -37,6 +37,7 @@ public class BasicTest extends AbstractParseMachineTest {
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(NoError, "./src/test/resources/composition/sees"));
list.add(new TestPair(NoError, "./src/test/resources/basics"));
list.add(new TestPair(NoError, "./src/test/resources/laws"));
return getConfiguration(list);
diff --git a/src/test/java/de/tlc4b/typechecking/SetsClauseTest.java b/src/test/java/de/tlc4b/typechecking/SetsClauseTest.java
index 95a7be21d89fb91f09820d4e2b34646c652f6107..90fdd909635144ddf6739aaa3c44c3ff599fce13 100644
--- a/src/test/java/de/tlc4b/typechecking/SetsClauseTest.java
+++ b/src/test/java/de/tlc4b/typechecking/SetsClauseTest.java
@@ -2,6 +2,7 @@ package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
+import org.junit.Ignore;
import org.junit.Test;
import de.be4.classicalb.core.parser.exceptions.BException;
@@ -20,4 +21,15 @@ public class SetsClauseTest {
assertEquals("DEF", t.constants.get("k").toString());
}
+ @Ignore
+ @Test
+ public void testDeferredSet2() throws BException {
+ String machine = "MACHINE test(DEF)\n"
+ + "CONSTANTS k \n"
+ + "PROPERTIES k : DEF \n"
+ + "END";
+ TestTypechecker t = new TestTypechecker(machine);
+ assertEquals("DEF", t.constants.get("k").toString());
+ }
+
}
diff --git a/src/test/java/de/tlc4b/typechecking/SetsTest.java b/src/test/java/de/tlc4b/typechecking/SetsTest.java
index 1afcd259ae8c37a966dd552507c048c9a3f6997b..2d5303a58ed412970681eea6bd37ae022b207f47 100644
--- a/src/test/java/de/tlc4b/typechecking/SetsTest.java
+++ b/src/test/java/de/tlc4b/typechecking/SetsTest.java
@@ -72,6 +72,30 @@ public class SetsTest {
assertEquals("POW(INTEGER*BOOL)", t.constants.get("k").toString());
}
+ @Test
+ public void testEventBSetComprehension() throws BException {
+ String machine = "MACHINE test\n"
+ + "CONSTANTS k,k2,k3 \n"
+ + "PROPERTIES k = {x,y| x = k2(k3) & y : {TRUE}} & k2(2)=1\n"
+ + "END";
+ TestTypechecker t = new TestTypechecker(machine);
+ assertEquals("POW(INTEGER*BOOL)", t.constants.get("k").toString());
+ assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k2").toString());
+ assertEquals("INTEGER", t.constants.get("k3").toString());
+ }
+
+ @Test
+ public void testEventBSetComprehension2() throws BException {
+ String machine = "MACHINE test\n"
+ + "CONSTANTS k,k2 \n"
+ + "PROPERTIES k = {a,b| a : k2 & b = a'foo} & k2={rec(foo:\"123\",bar:TRUE)}\n"
+ + "END";
+ TestTypechecker t = new TestTypechecker(machine);
+ assertEquals("POW(struct(foo:STRING,bar:BOOL)*STRING)", t.constants.get("k").toString());
+ assertEquals("POW(struct(foo:STRING,bar:BOOL))", t.constants.get("k2").toString());
+ }
+
+
@Test (expected = TypeErrorException.class)
public void testSetComprehensionException() throws BException {
String machine = "MACHINE test\n"
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 12a628e428b0c53acad6cbc02cd6b36fc91f4beb..24349b05707627582c0b4fa163cbfe28f6f0fbef 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -12,6 +12,7 @@ import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
+import util.ToolIO;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.exceptions.TLA2BException;
@@ -25,6 +26,7 @@ public class TestUtil {
public static void compare(String expectedModule, String machine)
throws Exception {
TLC4BGlobals.setForceTLCToEvalConstants(false);
+ ToolIO.setMode(ToolIO.TOOL);
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
@@ -112,7 +114,7 @@ public class TestUtil {
assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
}
- public static void compareConfig(String expectedModule,
+ public static void compareModuleAndConfig(String expectedModule,
String expectedConfig, String machine) throws Exception {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
@@ -120,6 +122,12 @@ public class TestUtil {
System.out.println(b2tlaTranslator.getModuleString());
System.out.println(b2tlaTranslator.getConfigString());
+
+ //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/resources/basics/ExternalFunctionsTest.mch b/src/test/resources/basics/ExternalFunctionsTest.mch
index c4f4af14bebd37ad2e1343446632bb74098ba28f..4a2116bede8cde19749eda599ba5772d3fe8855f 100644
--- a/src/test/resources/basics/ExternalFunctionsTest.mch
+++ b/src/test/resources/basics/ExternalFunctionsTest.mch
@@ -7,13 +7,15 @@ DEFINITIONS
STRING_SPLIT(x,y) == ["foo"];
EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));
EXTERNAL_FUNCTION_REC(A,B) == (STRING * A)-->B;
+ STRING_TO_INT(S) == 0;
+ EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);
+ STRING_APPEND(x,y) == "str";
+ EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
+
REC(F,A) == {};
EXTERNAL_FUNCTION_REC_LET(A) == (STRING * A)-->A;
REC_LET(F,A) == {};
- STRING_APPEND(x,y) == "str";
- EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
-
ABSTRACT_CONSTANTS SORT_SET
PROPERTIES
SORT_SET: POW(INTEGER) <-> POW(INTEGER*INTEGER) &
@@ -31,6 +33,9 @@ ASSERTIONS
STRING_APPEND("a","bc") = "abc";
STRING_APPEND("abc","") = "abc";
STRING_APPEND("","abc") = "abc";
- STRING_APPEND("","") = ""
+ STRING_APPEND("","") = "";
+ STRING_TO_INT("123") = 123;
+ STRING_TO_INT("000123") = 123;
+ STRING_TO_INT("-123") = -123
END
diff --git a/src/test/resources/composition/sees/M1.mch b/src/test/resources/composition/sees/M1.mch
new file mode 100644
index 0000000000000000000000000000000000000000..1170faa2e0c3a1c8b8b183aa5aee02415ac560f1
--- /dev/null
+++ b/src/test/resources/composition/sees/M1.mch
@@ -0,0 +1,8 @@
+MACHINE M1
+SEES M2
+VARIABLES x
+INVARIANT x : 1..10
+INITIALISATION x := k2
+OPERATIONS
+ Skip = skip
+END
diff --git a/src/test/resources/composition/sees/M2.mch b/src/test/resources/composition/sees/M2.mch
new file mode 100644
index 0000000000000000000000000000000000000000..8d955de80bb2e06b138d295e0a8a1d0dac8dab85
--- /dev/null
+++ b/src/test/resources/composition/sees/M2.mch
@@ -0,0 +1,7 @@
+MACHINE M2
+SEES M3
+CONSTANTS
+ k2
+PROPERTIES
+ k2 = k3 + 1
+END
diff --git a/src/test/resources/composition/sees/M3.mch b/src/test/resources/composition/sees/M3.mch
new file mode 100644
index 0000000000000000000000000000000000000000..fb4b2fbae3167d866d3f724ff0708c7cc5ee5bdf
--- /dev/null
+++ b/src/test/resources/composition/sees/M3.mch
@@ -0,0 +1,6 @@
+MACHINE M3
+CONSTANTS
+ k3
+PROPERTIES
+ k3 = 3
+END