diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index d00f2f7f89f75addac0c71fe79a74ffdc7cddfa4..24504794bddb8a9481bfacaee8f61e9123735305 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -17,6 +17,7 @@ import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
import de.tlc4b.exceptions.TLC4BIOException;
import de.tlc4b.exceptions.TLC4BException;
+import de.tlc4b.exceptions.TranslationException;
import de.tlc4b.tlc.TLCOutputInfo;
import de.tlc4b.tlc.TLCResults;
import de.tlc4b.util.StopWatch;
@@ -105,8 +106,8 @@ public class TLC4B {
System.out.println("--------------------------------");
System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
+ " ms");
- System.out.println("Translation time: " + StopWatch.getRunTime("Pure")
- + " ms");
+ System.out.println("Translation time: "
+ + StopWatch.getRunTime("Translation") + " ms");
System.out.println("Model checking time: "
+ results.getModelCheckingTime() + " sec");
// System.out.println("Number of workers: " +
@@ -290,13 +291,15 @@ public class TLC4B {
translator = new Translator(machineFileNameWithoutFileExtension,
mainfile, this.ltlFormula, this.constantsSetup);
StopWatch.stop("Parsing");
- StopWatch.start("Pure");
+ System.out.println("Parsing Completed.");
+ StopWatch.start("Translation");
translator.translate();
this.tlaModule = translator.getModuleString();
this.config = translator.getConfigString();
this.tlcOutputInfo = translator.getTLCOutputInfo();
createFiles();
- StopWatch.stop("Pure");
+ StopWatch.stop("Translation");
+ System.out.println("Translation Completed.");
}
}
@@ -355,63 +358,9 @@ public class TLC4B {
}
private void createStandardModules() {
- if (translator.getUsedStandardModule().contains(
- STANDARD_MODULES.Relations)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.Relations.toString());
- }
-
- if (translator.getUsedStandardModule().contains(
- STANDARD_MODULES.Functions)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.Functions.toString());
- }
-
- if (translator.getUsedStandardModule().contains(
- STANDARD_MODULES.BBuiltIns)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.BBuiltIns.toString());
- }
-
- if (translator.getUsedStandardModule().contains(
- STANDARD_MODULES.FunctionsAsRelations)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.FunctionsAsRelations.toString());
- if (!translator.getUsedStandardModule().contains(
- STANDARD_MODULES.Functions)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.Functions.toString());
- }
- }
-
- if (translator.getUsedStandardModule().contains(
- STANDARD_MODULES.SequencesExtended)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.SequencesExtended.toString());
- }
-
- if (translator.getUsedStandardModule().contains(
- STANDARD_MODULES.SequencesAsRelations)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.SequencesAsRelations.toString());
-
- if (!translator.getUsedStandardModule().contains(
- STANDARD_MODULES.Relations)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.Relations.toString());
- }
-
- if (!translator.getUsedStandardModule().contains(
- STANDARD_MODULES.FunctionsAsRelations)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.FunctionsAsRelations.toString());
- }
-
- if (!translator.getUsedStandardModule().contains(
- STANDARD_MODULES.Functions)) {
- createStandardModule(buildDir,
- STANDARD_MODULES.Functions.toString());
- }
+ for (STANDARD_MODULES module : translator
+ .getStandardModuleToBeCreated()) {
+ createStandardModule(buildDir, module.toString());
}
}
@@ -433,6 +382,14 @@ public class TLC4B {
.getClassLoader()
.getResourceAsStream("standardModules/" + name + ".tla");
}
+
+ if (is == null) {
+ // should never happen
+ throw new TranslationException(
+ "Unable to determine the source of the standard module: "
+ + name);
+ }
+
fos = new FileOutputStream(file);
int read = 0;
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 88abc3976ac94c1121fec8d470b9e691da7037c3..3424581e381415f4d7f66be5d7d898ad894a0f59 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -51,11 +51,11 @@ public class TLC4BGlobals {
partialInvariantEvaluation = false;
useSymmetry = false;
printCoverage = false;
- setForceTLCToEvalConstants(true);
+ forceTLCToEvalConstants = false;
- setProBconstantsSetup(false);
+ proBconstantsSetup = false;
- setCleanup(true);
+ cleanup = true;
workers = 1;
@@ -249,12 +249,12 @@ public class TLC4BGlobals {
public static void setSymmetryUse(boolean b) {
useSymmetry = b;
}
-
- public static void setPrintCoverage(boolean b){
+
+ public static void setPrintCoverage(boolean b) {
printCoverage = b;
}
-
- public static boolean isPrintCoverage(){
+
+ public static boolean isPrintCoverage() {
return printCoverage;
}
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index efc50e442f88dccbcfd455b4b4a62d707137f6a5..27b5ff2ce9752c6af62520340786fcd2fc2a9fe6 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -2,7 +2,7 @@ package de.tlc4b;
import java.io.File;
import java.io.IOException;
-import java.util.ArrayList;
+import java.util.HashSet;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
@@ -39,7 +39,7 @@ public class Translator {
private String machineName;
private String ltlFormula;
private PPredicate constantsSetup;
- private ArrayList<STANDARD_MODULES> usedStandardModules;
+ private HashSet<STANDARD_MODULES> standardModulesToBeCreated;
private TLCOutputInfo tlcOutputInfo;
private String translatedLTLFormula;
@@ -149,7 +149,7 @@ public class Translator {
UsedStandardModules usedModules = new UsedStandardModules(start,
typechecker, typeRestrictor, generator.getTlaModule());
- usedStandardModules = usedModules.getUsedModules();
+ standardModulesToBeCreated = usedModules.getStandardModulesToBeCreated();
PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
.getTlaModule().getOperations(), machineContext);
@@ -195,11 +195,11 @@ public class Translator {
}
public boolean containsUsedStandardModule(STANDARD_MODULES module) {
- return usedStandardModules.contains(module);
+ return standardModulesToBeCreated.contains(module);
}
- public ArrayList<UsedStandardModules.STANDARD_MODULES> getUsedStandardModule() {
- return usedStandardModules;
+ public HashSet<UsedStandardModules.STANDARD_MODULES> getStandardModuleToBeCreated() {
+ return standardModulesToBeCreated;
}
public String getTranslatedLTLFormula() {
diff --git a/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java b/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
index 81ce5f7339e3eff65528b58762731975421f6401..3a6278f4303a509c806178fe69b10fdfdfd4d78b 100644
--- a/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
+++ b/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
@@ -16,11 +16,8 @@ import de.be4.classicalb.core.parser.node.Node;
import de.tlc4b.TLC4BGlobals;
/**
- *
- *
- *
* @author hansen
- *
+ * In this class we search for preferences set in the definitions clause, e.g. minint or maxint.
*/
public class DefinitionsAnalyser extends DepthFirstAdapter {
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 24c46ea9e0b6b2563fd4efe43f05e4aed932d7e8..fa0ad62db198d93fd159d30c3dbd8faf7c429153 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -414,6 +414,7 @@ public class MachineContext extends DepthFirstAdapter {
return;
}
}
+
throw new ScopeException("Unkown definition: '" + name
+ "' at position: " + node.getStartPos());
}
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 763d0798b9cd3a6130423c853c44d023ff7771e0..1a9019f8ec220d20fa2b7fd3949ad25ddbaf6413 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -4,6 +4,8 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;
+import de.tlc4b.prettyprint.TLAPrinter;
+
public final class StandardMadules {
private StandardMadules() {
@@ -228,5 +230,37 @@ 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.
+ *
+ * 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";
+
+ 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);
+ }
+ 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 589cf83c0837a13d9e9f54a4794000c96a85aef2..f811ebd328eb5607c16449ecf1031cee3ee97454 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -286,9 +286,15 @@ 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)){
+
+ }
Node originalDef = referenceTable.get(node);
BType found = getType(originalDef);
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 5c081db5301e16c0901a739f194e4bb161db3e65..a8eeceecab5d18aca59f288fa77d66bfc2a690c0 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -14,6 +14,7 @@ import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AClosureExpression;
import de.be4.classicalb.core.parser.node.ACompositionExpression;
import de.be4.classicalb.core.parser.node.AConcatExpression;
+import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.ADirectProductExpression;
import de.be4.classicalb.core.parser.node.ADivExpression;
import de.be4.classicalb.core.parser.node.ADomainExpression;
@@ -106,7 +107,7 @@ import de.tlc4b.tla.TLAModule;
public class UsedStandardModules extends DepthFirstAdapter {
public static enum STANDARD_MODULES {
- Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations,
+ Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations, ExternalFunctions
}
private final static ArrayList<STANDARD_MODULES> modules = new ArrayList<UsedStandardModules.STANDARD_MODULES>();
@@ -122,22 +123,21 @@ public class UsedStandardModules extends DepthFirstAdapter {
modules.add(STANDARD_MODULES.FunctionsAsRelations);
modules.add(STANDARD_MODULES.SequencesExtended);
modules.add(STANDARD_MODULES.SequencesAsRelations);
+ modules.add(STANDARD_MODULES.ExternalFunctions);
}
- private final Set<STANDARD_MODULES> usedStandardModules;
+ private final Set<STANDARD_MODULES> extendedStandardModules;
private final Typechecker typechecker;
public UsedStandardModules(Start start, Typechecker typechecker,
TypeRestrictor typeRestrictor, TLAModule tlaModule) {
- this.usedStandardModules = new HashSet<STANDARD_MODULES>();
+ this.extendedStandardModules = new HashSet<STANDARD_MODULES>();
this.typechecker = typechecker;
-
-
if (TLC4BGlobals.useSymmetry()) {
- usedStandardModules.add(STANDARD_MODULES.TLC);
+ extendedStandardModules.add(STANDARD_MODULES.TLC);
}
-
+
List<PDefinition> definitions = tlaModule.getAllDefinitions();
if (definitions != null) {
for (PDefinition pDefinition : definitions) {
@@ -151,9 +151,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
start.apply(this);
}
- public ArrayList<STANDARD_MODULES> getUsedModules() {
+ public ArrayList<STANDARD_MODULES> getExtendedModules() {
ArrayList<STANDARD_MODULES> list = new ArrayList<STANDARD_MODULES>(
- usedStandardModules);
+ extendedStandardModules);
if (list.contains(STANDARD_MODULES.Integers)) {
list.remove(STANDARD_MODULES.Naturals);
}
@@ -163,22 +163,66 @@ public class UsedStandardModules extends DepthFirstAdapter {
Integer i2 = Integer.valueOf(modules.indexOf(s2));
return i1.compareTo(i2);
}
- }
-
- );
+ });
return list;
}
- /**
- * Bounded Variables
- *
- */
-
+ public HashSet<STANDARD_MODULES> getStandardModulesToBeCreated(){
+ // dependencies of standard modules
+ HashSet<STANDARD_MODULES> res = new HashSet<STANDARD_MODULES>();
+ for (STANDARD_MODULES module : extendedStandardModules) {
+ switch (module) {
+ case ExternalFunctions:
+ res.add(STANDARD_MODULES.ExternalFunctions);
+ break;
+ case FunctionsAsRelations:
+ res.add(STANDARD_MODULES.FunctionsAsRelations);
+ res.add(STANDARD_MODULES.Functions);
+ break;
+ case SequencesAsRelations:
+ res.add(STANDARD_MODULES.SequencesAsRelations);
+ res.add(STANDARD_MODULES.Relations);
+ res.add(STANDARD_MODULES.FunctionsAsRelations);
+ res.add(STANDARD_MODULES.Functions);
+ break;
+ case BBuiltIns:
+ res.add(STANDARD_MODULES.BBuiltIns);
+ break;
+ case Functions:
+ res.add(STANDARD_MODULES.Functions);
+ break;
+ case Relations:
+ res.add(STANDARD_MODULES.Relations);
+ break;
+ case Sequences:
+ break;
+ case SequencesExtended:
+ res.add(STANDARD_MODULES.SequencesExtended);
+ break;
+ default:
+ break;
+ }
+
+ }
+ return res;
+ }
@Override
public void inAExpressionDefinitionDefinition(
AExpressionDefinitionDefinition node) {
if (TLC4BGlobals.isForceTLCToEvalConstants()) {
- usedStandardModules.add(STANDARD_MODULES.TLC);
+ extendedStandardModules.add(STANDARD_MODULES.TLC);
+ }
+ String name = node.getName().getText().trim();
+ if (StandardMadules.isKeywordInModuleExternalFunctions(name)) {
+ extendedStandardModules.add(STANDARD_MODULES.ExternalFunctions);
+ }
+ }
+
+ @Override
+ public void inADefinitionPredicate(ADefinitionPredicate node) {
+ String name = node.getDefLiteral().getText().trim();
+ if (StandardMadules.isKeywordInModuleExternalFunctions(name)) {
+ extendedStandardModules.add(STANDARD_MODULES.ExternalFunctions);
}
}
@@ -188,72 +232,72 @@ public class UsedStandardModules extends DepthFirstAdapter {
@Override
public void caseANaturalSetExpression(ANaturalSetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
@Override
public void caseANatural1SetExpression(ANatural1SetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
@Override
public void caseANatSetExpression(ANatSetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
@Override
public void caseANat1SetExpression(ANat1SetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inALessEqualPredicate(ALessEqualPredicate node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inALessPredicate(ALessPredicate node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAGreaterEqualPredicate(AGreaterEqualPredicate node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAGreaterPredicate(AGreaterPredicate node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAAddExpression(AAddExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAIntervalExpression(AIntervalExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inADivExpression(ADivExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAPowerOfExpression(APowerOfExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAModuloExpression(AModuloExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
public void inAMinusOrSetSubtractExpression(
AMinusOrSetSubtractExpression node) {
BType t = typechecker.getType(node);
if (t instanceof IntegerType) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
}
public void inAMultOrCartExpression(AMultOrCartExpression node) {
BType t = typechecker.getType(node);
if (t instanceof IntegerType) {
- usedStandardModules.add(STANDARD_MODULES.Naturals);
+ extendedStandardModules.add(STANDARD_MODULES.Naturals);
} else {
// usedStandardModules.add(STANDARD_MODULES.RelationsNew);
}
@@ -264,26 +308,26 @@ public class UsedStandardModules extends DepthFirstAdapter {
*/
public void inAIntSetExpression(AIntSetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Integers);
+ extendedStandardModules.add(STANDARD_MODULES.Integers);
}
public void inAIntegerSetExpression(AIntegerSetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Integers);
+ extendedStandardModules.add(STANDARD_MODULES.Integers);
}
public void inAUnaryMinusExpression(AUnaryMinusExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Integers);
+ extendedStandardModules.add(STANDARD_MODULES.Integers);
}
public void inAMinIntExpression(AMinIntExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Integers);
+ extendedStandardModules.add(STANDARD_MODULES.Integers);
}
/**
* FiniteSets
*/
public void inACardExpression(ACardExpression node) {
- usedStandardModules.add(STANDARD_MODULES.FiniteSets);
+ extendedStandardModules.add(STANDARD_MODULES.FiniteSets);
}
/**
@@ -291,57 +335,57 @@ public class UsedStandardModules extends DepthFirstAdapter {
*/
public void inAMinExpression(AMinExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAMaxExpression(AMaxExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inASuccessorExpression(ASuccessorExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAPredecessorExpression(APredecessorExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAPow1SubsetExpression(APow1SubsetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAFinSubsetExpression(AFinSubsetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAFin1SubsetExpression(AFin1SubsetExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inANotSubsetPredicate(ANotSubsetPredicate node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inANotSubsetStrictPredicate(ANotSubsetStrictPredicate node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAGeneralIntersectionExpression(
AGeneralIntersectionExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAQuantifiedIntersectionExpression(
AQuantifiedIntersectionExpression node) {
- usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
public void inAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
@@ -354,9 +398,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void setOfFunctions(Node node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.Functions);
+ extendedStandardModules.add(STANDARD_MODULES.Functions);
} else {
- usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
}
}
@@ -405,7 +449,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
BType type = typechecker.getType(node.getIdentifier());
if (type instanceof SetType) {
- usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
}
}
@@ -413,7 +457,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inATotalFunctionExpression(ATotalFunctionExpression node) {
SetType type = (SetType) typechecker.getType(node);
if (type.getSubtype() instanceof SetType) {
- usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
}
}
@@ -424,27 +468,27 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void evalFunctionOrRelation(Node node) {
BType t = typechecker.getType(node);
if (t instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.Functions);
+ extendedStandardModules.add(STANDARD_MODULES.Functions);
} else {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
}
public void inARelationsExpression(ARelationsExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inADomainExpression(ADomainExpression node) {
BType t = typechecker.getType(node.getExpression());
if (!(t instanceof FunctionType)) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
}
public void inASetExtensionExpression(ASetExtensionExpression node) {
BType t = typechecker.getType(node);
if (t instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.TLC);
+ extendedStandardModules.add(STANDARD_MODULES.TLC);
}
}
@@ -492,52 +536,52 @@ public class UsedStandardModules extends DepthFirstAdapter {
BType type = typechecker.getType(((AFunctionExpression) e)
.getIdentifier());
if (type instanceof SetType) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
} else {
- usedStandardModules.add(STANDARD_MODULES.Functions);
+ extendedStandardModules.add(STANDARD_MODULES.Functions);
}
}
}
}
public void inADirectProductExpression(ADirectProductExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inAParallelProductExpression(AParallelProductExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inACompositionExpression(ACompositionExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inAFirstProjectionExpression(AFirstProjectionExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inASecondProjectionExpression(ASecondProjectionExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inAIterationExpression(AIterationExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inAClosureExpression(AClosureExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inAReflexiveClosureExpression(AReflexiveClosureExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inATransFunctionExpression(ATransFunctionExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
public void inATransRelationExpression(ATransRelationExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ extendedStandardModules.add(STANDARD_MODULES.Relations);
}
/**
@@ -547,9 +591,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inASeqExpression(ASeqExpression node) {
SetType type = (SetType) typechecker.getType(node);
if (type.getSubtype() instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.Sequences);
+ extendedStandardModules.add(STANDARD_MODULES.Sequences);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
}
}
@@ -564,9 +608,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void evalSequenceOrRelation(Node node) {
BType type = typechecker.getType(node);
if (type instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.Sequences);
+ extendedStandardModules.add(STANDARD_MODULES.Sequences);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
}
}
@@ -585,36 +629,36 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void evalSequenceExtendedOrRelation(Node node) {
BType type = typechecker.getType(node);
if (type instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
}
}
public void inAIseqExpression(AIseqExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
}
}
public void inASeq1Expression(ASeq1Expression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
}
}
public void inAIseq1Expression(AIseq1Expression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
}
}
@@ -633,9 +677,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inAPermExpression(APermExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
- usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
} else {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
}
}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index fbcea22edf06a061ac8f043720bad06b3d954187..1068dedef3fa339587e16ab32d064e5ba8c099ae 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -20,14 +20,15 @@ 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.Start;
+import de.tlc4b.analysis.StandardMadules;
/**
* This class eliminates all definition calls in the MACHINE. A definition call
* will be replaced by the right-hand side of the definition and all parameter
* on the RHS are replaced by the arguments of the call.
*
- * Note: All parameters of a definition are replaced before calls of
- * sub-definitions are resolved. This behavior is similar to what ProB does by
+ * Note: All parameters of a definition are replaced before a call of a
+ * sub-definition is resolved. This behavior is similar to what ProB does when
* eliminating all definitions.
*
*/
@@ -77,13 +78,18 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
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_")
+ || StandardMadules
+ .isKeywordInModuleExternalFunctions(name))
continue;
} else if (e instanceof APredicateDefinitionDefinition) {
String name = ((APredicateDefinitionDefinition) e).getName()
.getText().toString();
- if (name.equals("GOAL"))
+ if (name.equals("GOAL")
+ || StandardMadules
+ .isKeywordInModuleExternalFunctions(name))
continue;
}
e.replaceBy(null);
@@ -117,14 +123,22 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
@Override
public void caseADefinitionExpression(ADefinitionExpression node) {
+
String name = node.getDefLiteral().getText();
- PDefinition def = definitionsTable.get(name);
+ ArrayList<PExpression> arguments = new ArrayList<PExpression>(
+ node.getParameters());
+ if (StandardMadules.isKeywordInModuleExternalFunctions(name)) {
+ for (PExpression arg : arguments) {
+ arg.apply(this);
+ }
+ return;
+ }
+ PDefinition def = definitionsTable.get(name);
AExpressionDefinitionDefinition clone = (AExpressionDefinitionDefinition) def
.clone();
Hashtable<String, PExpression> context = new Hashtable<String, PExpression>();
- ArrayList<PExpression> arguments = new ArrayList<PExpression>(
- node.getParameters());
+
for (int i = 0; i < clone.getParameters().size(); i++) {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
@@ -144,11 +158,19 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
String name = node.getDefLiteral().getText();
PDefinition def = definitionsTable.get(name);
+ ArrayList<PExpression> arguments = new ArrayList<PExpression>(
+ node.getParameters());
+ if (StandardMadules.isKeywordInModuleExternalFunctions(name)) {
+ for (PExpression arg : arguments) {
+ arg.apply(this);
+ }
+ return;
+ }
+
APredicateDefinitionDefinition clone = (APredicateDefinitionDefinition) def
.clone();
Hashtable<String, PExpression> context = new Hashtable<String, PExpression>();
- ArrayList<PExpression> arguments = new ArrayList<PExpression>(
- node.getParameters());
+
for (int i = 0; i < clone.getParameters().size(); i++) {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
diff --git a/src/main/java/de/tlc4b/exceptions/TranslationException.java b/src/main/java/de/tlc4b/exceptions/TranslationException.java
new file mode 100644
index 0000000000000000000000000000000000000000..fa71eccb25ba427f582ea82b6b6b293122ea3b85
--- /dev/null
+++ b/src/main/java/de/tlc4b/exceptions/TranslationException.java
@@ -0,0 +1,15 @@
+package de.tlc4b.exceptions;
+
+@SuppressWarnings("serial")
+public class TranslationException extends TLC4BException{
+
+ public TranslationException(String e) {
+ super(e);
+ }
+
+ @Override
+ public String getError() {
+ return "TranslationError";
+ }
+
+}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 85fdd34f03459e21b2b583e0b28136bfe2548779..8276701550722999f06042be7a4ed60ef37cdc7b 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -15,6 +15,7 @@ import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.PrecedenceCollector;
import de.tlc4b.analysis.PrimedNodesMarker;
import de.tlc4b.analysis.Renamer;
+import de.tlc4b.analysis.StandardMadules;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.analysis.UsedStandardModules;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
@@ -241,10 +242,10 @@ public class TLAPrinter extends DepthFirstAdapter {
this.configFileString.append("INVARIANT NotGoal\n");
}
- if (TLC4BGlobals.isAssertion()) {
+ if (TLC4BGlobals.isAssertion() && tlaModule.hasInitPredicate()) {
for (int i = 0; i < configFile.getAssertionSize(); i++) {
- this.configFileString.append("INVARIANT Assertion" + (i + 1)
- + "\n");
+ this.configFileString.append("INVARIANT Assertion")
+ .append(i + 1).append("\n");
}
}
@@ -278,8 +279,9 @@ public class TLAPrinter extends DepthFirstAdapter {
for (int i = 0; i < operations.size(); i++) {
AOperation node = (AOperation) operations.get(i);
String name = renamer.getNameOfRef(node);
- configFileString.append(name + "_action = ");
- configFileString.append(name + "_action");
+ String actionName = name + "actions";
+ configFileString.append(actionName).append(" = ")
+ .append(actionName);
configFileString.append("\n");
}
configFileString.append("\n");
@@ -302,13 +304,13 @@ public class TLAPrinter extends DepthFirstAdapter {
}
private void printExtendedModules() {
- if (usedStandardModules.getUsedModules().size() > 0) {
+ if (usedStandardModules.getExtendedModules().size() > 0) {
moduleStringAppend("EXTENDS ");
- for (int i = 0; i < usedStandardModules.getUsedModules().size(); i++) {
+ for (int i = 0; i < usedStandardModules.getExtendedModules().size(); i++) {
if (i > 0) {
moduleStringAppend(", ");
}
- moduleStringAppend(usedStandardModules.getUsedModules().get(i)
+ moduleStringAppend(usedStandardModules.getExtendedModules().get(i)
.toString());
}
moduleStringAppend("\n");
@@ -323,6 +325,7 @@ public class TLAPrinter extends DepthFirstAdapter {
def.getDefName().apply(this);
continue;
}
+
def.getDefName().apply(this);
moduleStringAppend(" == ");
Node e = def.getDefinition();
@@ -449,7 +452,11 @@ public class TLAPrinter extends DepthFirstAdapter {
if (assertions.size() == 0)
return;
for (int i = 0; i < assertions.size(); i++) {
- moduleStringAppend("Assertion" + (i + 1) + " == ");
+ if (tlaModule.hasInitPredicate()) {
+ moduleStringAppend("Assertion" + (i + 1) + " == ");
+ } else {
+ moduleStringAppend("ASSUME Assertion" + (i + 1) + " == ");
+ }
assertions.get(i).apply(this);
moduleStringAppend("\n");
}
@@ -1108,6 +1115,10 @@ public class TLAPrinter extends DepthFirstAdapter {
if (name == null) {
name = Utils.getIdentifierAsString(node.getIdentifier());
}
+ if(name.equals(SORT_SET)){
+ moduleStringAppend("{}");
+ return;
+ }
moduleStringAppend(name);
if (primedNodesMarker.isPrimed(node)) {
moduleStringAppend("'");
@@ -1313,12 +1324,15 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAExpressionDefinitionDefinition(
AExpressionDefinitionDefinition node) {
+ String oldName = node.getName().getText().trim();
+ if(StandardMadules.isKeywordInModuleExternalFunctions(oldName)){
+ return;
+ }
String name = renamer.getName(node);
if (null == name) {
name = node.getName().getText().trim();
}
moduleStringAppend(name);
-
List<PExpression> args = node.getParameters();
if (args.size() > 0) {
moduleStringAppend("(");
@@ -1354,6 +1368,9 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printBDefinition(String name, List<PExpression> args,
Node rightSide) {
+ if(StandardMadules.isKeywordInModuleExternalFunctions(name)){
+ return;
+ }
moduleStringAppend(name);
if (args.size() > 0) {
moduleStringAppend("(");
@@ -1760,7 +1777,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();
+ String name = Utils.getIdentifierAsString(id.getIdentifier());
+ if(name.equals(SORT_SET)){
+ moduleStringAppend(SORT_SET);
+ //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);
@@ -1777,11 +1813,11 @@ public class TLAPrinter extends DepthFirstAdapter {
} else {
if (TLC4BGlobals.checkWelldefinedness()) {
- moduleStringAppend(REL_CALL + "(");
+ moduleStringAppend(REL_CALL);
} else {
- moduleStringAppend(REL_CALL_WITHOUT_WD_CHECK + "(");
+ moduleStringAppend(REL_CALL_WITHOUT_WD_CHECK);
}
-
+ moduleStringAppend("(");
node.getIdentifier().apply(this);
moduleStringAppend(", ");
List<PExpression> copy = new ArrayList<PExpression>(
diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
index 4eb277c4f2f5b33c12ca25bd55ee29a0636c6e0a..d56ff85ae7ade3b4bfcd79b2b95e08f60eab0fa2 100644
--- a/src/main/java/de/tlc4b/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -20,7 +20,7 @@ public class TLAModule {
protected final ArrayList<POperation> operations;
private ArrayList<PDefinition> bDefinitions;
private final ArrayList<Node> assertions;
-
+
private ArrayList<PDefinition> allDefinitions;
public TLAModule() {
@@ -33,46 +33,47 @@ public class TLAModule {
this.bDefinitions = new ArrayList<PDefinition>();
this.assertions = new ArrayList<Node>();
this.invariants = new ArrayList<Node>();
-
+
this.allDefinitions = new ArrayList<PDefinition>();
}
- public void sortAllDefinitions(MachineContext machineContext){
- DefinitionsOrder defOrder = new DefinitionsOrder(machineContext, this.allDefinitions);
+ public void sortAllDefinitions(MachineContext machineContext) {
+ DefinitionsOrder defOrder = new DefinitionsOrder(machineContext,
+ this.allDefinitions);
this.allDefinitions = defOrder.getAllDefinitions();
}
-
- public void addToAllDefinitions(PDefinition def){
+
+ public void addToAllDefinitions(PDefinition def) {
this.allDefinitions.add(def);
}
-
- public ArrayList<PDefinition> getAllDefinitions(){
+
+ public ArrayList<PDefinition> getAllDefinitions() {
return allDefinitions;
}
-
- public ArrayList<Node> getAssertions(){
+
+ public ArrayList<Node> getAssertions() {
return assertions;
}
-
- public void addAssertion(Node node){
+
+ public void addAssertion(Node node) {
assertions.add(node);
}
-
+
public void addAssume(Node node) {
if (!assumes.contains(node))
assumes.add(node);
}
- public void addInit(Node node){
- if(!initPredicates.contains(node))
+ public void addInit(Node node) {
+ if (!initPredicates.contains(node))
initPredicates.add(node);
}
-
- public boolean isInitPredicate(Node node){
+
+ public boolean isInitPredicate(Node node) {
return initPredicates.contains(node);
}
-
+
public String getModuleName() {
return moduleName;
}
@@ -105,12 +106,16 @@ public class TLAModule {
return invariants;
}
- public void setBDefinitions(ArrayList<PDefinition> defs){
+ public void setBDefinitions(ArrayList<PDefinition> defs) {
this.bDefinitions = defs;
}
-
+
public ArrayList<PDefinition> getBDefinitions() {
return bDefinitions;
}
+ public boolean hasInitPredicate() {
+ return this.initPredicates.size() > 0;
+ }
+
}
diff --git a/src/main/resources/standardModules/ExternalFunctions.tla b/src/main/resources/standardModules/ExternalFunctions.tla
new file mode 100644
index 0000000000000000000000000000000000000000..ec85b011567c1575278ce597a5a9431da3b9a8d0
--- /dev/null
+++ b/src/main/resources/standardModules/ExternalFunctions.tla
@@ -0,0 +1,51 @@
+------------------------------ MODULE ExternalFunctions ------------------------------
+EXTENDS Sequences, Integers, TLC, FiniteSets
+
+RECURSIVE SPLIT1(_,_,_,_)
+LOCAL SPLIT1(s,c,start,i) ==
+ 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))
+ [] OTHER -> SPLIT1(s,c,start,i+1)
+
+STRING_SPLIT(s, c) == SPLIT1(s,c,1,1)
+
+
+LOCAL DIGIT_TO_STRING(x) ==
+ CASE x = 0 -> "0"
+ [] x = 1 -> "1"
+ [] x= 2 -> "2"
+ [] x = 3 -> "3"
+ [] x = 4 -> "4"
+ [] x= 5 -> "5"
+ [] x= 6 -> "6"
+ [] x= 7 -> "7"
+ [] x=8 -> "8"
+ [] x=9 -> "9"
+
+RECURSIVE INT_TO_STRING1(_)
+LOCAL INT_TO_STRING1(i) ==
+ IF i < 10
+ THEN DIGIT_TO_STRING(i)
+ ELSE INT_TO_STRING1(i\div10) \o DIGIT_TO_STRING(i%10)
+
+INT_TO_STRING(i) ==
+ IF i < 0
+ THEN "-" \o INT_TO_STRING1(-i)
+ ELSE INT_TO_STRING1(i)
+
+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>>}
+
+printf(s,v) == PrintT(s) /\ PrintT(v)
+
+=============================================================================
\ No newline at end of file
diff --git a/src/test/java/de/tlc4b/prettyprint/ClausesTest.java b/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
index a4a78c37e1f9a1cb92d72a483a5b04b2031df9e7..895d7a6e964cb591a9108e653cfb53bd2612cf29 100644
--- a/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
@@ -7,13 +7,13 @@ import org.junit.Test;
public class ClausesTest {
- @Test //TODO include config
+ @Test
public void testAssertion() throws Exception {
String machine = "MACHINE test\n"
+ "ASSERTIONS 1 = 1\n"
+ "END";
String expected = "---- MODULE test ----\n"
- + "Assertions == \\/ 1 = 1\n"
+ + "ASSUME Assertion1 == 1 = 1\n"
+ "======";
compare(expected, machine);
}
@@ -24,7 +24,8 @@ public class ClausesTest {
+ "ASSERTIONS 1 = 1; 2 = 2\n"
+ "END";
String expected = "---- MODULE test ----\n"
- + "Assertions == \\/ 1 = 1 \\/ 2 = 2\n"
+ + "ASSUME Assertion1 == 1 = 1\n"
+ + "ASSUME Assertion2 == 2 = 2\n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/resources/basics/ExternalFunctionsTest.mch b/src/test/resources/basics/ExternalFunctionsTest.mch
new file mode 100644
index 0000000000000000000000000000000000000000..01daf94cdb2a8cc8ed455d86a8d4e7fd2ffd92fc
--- /dev/null
+++ b/src/test/resources/basics/ExternalFunctionsTest.mch
@@ -0,0 +1,25 @@
+MACHINE ExternalFunctionsTest
+DEFINITIONS
+printf(format_string,value) == TRUE=TRUE;
+EXTERNAL_PREDICATE_printf(T) == STRING*T;
+INT_TO_STRING(S) == "0";
+EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);
+STRING_SPLIT(x,y) == ["foo"];
+EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));
+EXTERNAL_FUNCTION_REC(A,B) == (STRING * A)-->B;
+REC(F,A) == {};
+EXTERNAL_FUNCTION_REC_LET(A) == (STRING * A)-->A;
+REC_LET(F,A) == {};
+ABSTRACT_CONSTANTS SORT_SET
+PROPERTIES
+SORT_SET: POW(INTEGER) <-> POW(INTEGER*INTEGER) &
+SORT_SET = REC_LET("SORT_SET",%x.(x={}|<>) \/ %x.(x:POW1(INTEGER)|REC("SORT_SET",x-{max(x)})<-max(x)))
+ASSERTIONS
+ printf("result", 2);
+ INT_TO_STRING(123) = "123";
+ INT_TO_STRING(-123) = "-123";
+ STRING_SPLIT("foo bar", " ") = ["foo", "bar"];
+ STRING_SPLIT(" foo", " ") = ["foo"];
+ STRING_SPLIT("foo||bar", "||") = ["foo", "bar"];
+ SORT_SET({4,2,3,1}) = [1,2,3,4]
+END