diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 45d56b841f849b552bf35f54859546760d1851a6..e46b6c7f004c09e76d9556e10909f27d4d498733 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -222,6 +222,7 @@ public class TLC4B {
tlc4b.tlcOutputInfo = tlc4b.translator.getTLCOutputInfo();
StopWatch.stop(TRANSLATION_TIME);
printlnSilent("(" + StopWatch.getRunTimeAsString(TRANSLATION_TIME) + "ms)");
+ printlnSilent("Translated TLA:\n" + tlc4b.tlaModule);
tlc4b.createFiles();
if (TLC4BGlobals.isRunTLC()) {
diff --git a/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
index 69a295555b8936b1b5bcde9441b68ec6c0f98f76..1dd121bc4262eda31bb2b13548ae538d3bc82eef 100644
--- a/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
+++ b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
@@ -9,12 +9,15 @@ import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
+import de.be4.classicalb.core.parser.node.AFunctionExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.APrimedIdentifierExpression;
+import de.be4.classicalb.core.parser.node.ARecordFieldExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.POperation;
import de.be4.classicalb.core.parser.util.Utils;
+import de.tlc4b.exceptions.NotSupportedException;
import de.tlc4b.exceptions.ScopeException;
public class PrimedNodesMarker extends DepthFirstAdapter {
@@ -40,14 +43,30 @@ public class PrimedNodesMarker extends DepthFirstAdapter {
}
}
+ private void primeIfVariable(Node node) {
+ Node ref = machineContext.getReferences().get(node);
+ if (machineContext.getVariables().containsValue(ref)) {
+ primedNodes.add(node);
+ }
+ }
+
@Override
public void caseAAssignSubstitution(AAssignSubstitution node) {
List<PExpression> copy = new ArrayList<>(node.getLhsExpression());
for (PExpression e : copy) {
- Node ref = machineContext.getReferences().get(e);
- if (machineContext.getVariables().containsValue(ref)) {
- primedNodes.add(e);
- }
+ primeWrittenVariable(e);
+ }
+ }
+
+ private void primeWrittenVariable(PExpression e) {
+ if (e instanceof AIdentifierExpression) {
+ primeIfVariable(e);
+ } else if (e instanceof AFunctionExpression) {
+ primeWrittenVariable(((AFunctionExpression) e).getIdentifier());
+ } else if (e instanceof ARecordFieldExpression) {
+ primeWrittenVariable(((ARecordFieldExpression) e).getRecord());
+ } else {
+ throw new NotSupportedException("Unsupported assignment lhs: " + e);
}
}
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index f39d45299e0a109351f1df0e33e0141330203eb0..d707ac23334a671ba2d3d8002223be18d167286d 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -434,20 +434,13 @@ public class UsedStandardModules extends DepthFirstAdapter {
// Function call
public void inAFunctionExpression(AFunctionExpression node) {
- // System.out.println(node.parent().getClass());
- if (node.parent() instanceof AAssignSubstitution) {
- AAssignSubstitution parent = (AAssignSubstitution) node.parent();
- if (parent.getLhsExpression().contains(node)) {
- // function assignment (function call on the left side), e.g.
- // f(x) := 1
- return;
- }
- }
BType type = typechecker.getType(node.getIdentifier());
- if (type instanceof SetType) {
+ if (type instanceof FunctionType) {
+ extendedStandardModules.add(StandardModule.Functions);
+ } else {
extendedStandardModules.add(StandardModule.FunctionsAsRelations);
+ extendedStandardModules.add(StandardModule.Relations);
}
-
}
public void inATotalFunctionExpression(ATotalFunctionExpression node) {
@@ -525,18 +518,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
public void inAAssignSubstitution(AAssignSubstitution node) {
- List<PExpression> copy = new ArrayList<>(node.getLhsExpression());
- for (PExpression e : copy) {
- if (e instanceof AFunctionExpression) {
- BType type = typechecker.getType(((AFunctionExpression) e)
- .getIdentifier());
- if (type instanceof SetType) {
- extendedStandardModules.add(StandardModule.Relations);
- } else {
- extendedStandardModules.add(StandardModule.Functions);
- }
- }
- }
+ // function assignments are handled in "inAFunctionExpression"
}
public void inADirectProductExpression(ADirectProductExpression node) {
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
index efde0eec729cb1c8b34848e83526c92efc7fee52..075ec52423e6a16e83f5b4f2d1c8f9e61356cc74 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
@@ -21,6 +21,7 @@ import de.be4.classicalb.core.parser.node.AIfSubstitution;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AParallelSubstitution;
+import de.be4.classicalb.core.parser.node.ARecordFieldExpression;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.ASelectWhenSubstitution;
import de.be4.classicalb.core.parser.node.ASkipSubstitution;
@@ -29,6 +30,7 @@ import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PSubstitution;
import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.exceptions.NotSupportedException;
import de.tlc4b.exceptions.SubstitutionException;
/**
@@ -131,19 +133,26 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<>(node.getLhsExpression());
HashSet<Node> list = new HashSet<>();
for (PExpression e : copy) {
- if (e instanceof AIdentifierExpression) {
- Node identifier = machineContext.getReferenceNode(e);
- list.add(identifier);
- } else {
- AFunctionExpression func = (AFunctionExpression) e;
- Node identifier = machineContext.getReferenceNode(func.getIdentifier());
- list.add(identifier);
- }
+ Node assigned = getAssignedVariable(e);
+ Node identifier = machineContext.getReferenceNode(assigned);
+ list.add(identifier);
}
assignedVariablesTable.put(node, list);
defaultOut(node);
}
+ private PExpression getAssignedVariable(PExpression e) {
+ if (e instanceof AIdentifierExpression) {
+ return e;
+ } else if (e instanceof AFunctionExpression) {
+ return getAssignedVariable(((AFunctionExpression) e).getIdentifier());
+ } else if (e instanceof ARecordFieldExpression) {
+ return getAssignedVariable(((ARecordFieldExpression) e).getRecord());
+ } else {
+ throw new NotSupportedException("Unknown assignment lhs: " + e);
+ }
+ }
+
@Override
public void caseABecomesElementOfSubstitution(ABecomesElementOfSubstitution node) {
List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 9474ba326984a31d5db08e5b5c7860ebe205ee3f..1d6bcd957a888170c46d1448a12c069f6e32569d 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -17,7 +17,6 @@ import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.PrecedenceCollector;
import de.tlc4b.analysis.PrimedNodesMarker;
import de.tlc4b.analysis.Renamer;
-import de.tlc4b.analysis.StandardModules;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.analysis.UsedStandardModules;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
@@ -30,6 +29,7 @@ import de.tlc4b.btypes.PairType;
import de.tlc4b.btypes.SetType;
import de.tlc4b.btypes.StructType;
import de.tlc4b.btypes.UntypedType;
+import de.tlc4b.exceptions.NotSupportedException;
import de.tlc4b.exceptions.TranslationException;
import de.tlc4b.ltl.LTLFormulaVisitor;
import de.tlc4b.tla.ConfigFile;
@@ -63,6 +63,8 @@ public class TLAPrinter extends DepthFirstAdapter {
private final Renamer renamer;
private final InvariantPreservationAnalysis invariantPreservationAnalysis;
+ private boolean disablePrimedNodes = false;
+
public TLAPrinter(MachineContext machineContext, Typechecker typechecker,
UnchangedVariablesFinder unchangedVariablesFinder,
PrecedenceCollector precedenceCollector,
@@ -629,30 +631,6 @@ public class TLAPrinter extends DepthFirstAdapter {
printUnchangedVariables(node, true);
}
- @Override
- public void caseAAssignSubstitution(AAssignSubstitution node) {
- List<PExpression> copy = new ArrayList<>(node.getLhsExpression());
- List<PExpression> copy2 = new ArrayList<>(node.getRhsExpressions());
-
- for (int i = 0; i < copy.size(); i++) {
- PExpression left = copy.get(i);
- PExpression right = copy2.get(i);
-
- if (left instanceof AFunctionExpression) {
- printFunctionAssignment(left, right);
-
- } else {
- printNormalAssignment(left, right);
- }
-
- if (i < copy.size() - 1) {
- moduleStringAppend(" /\\ ");
- }
- }
-
- printUnchangedVariables(node, true);
- }
-
@Override
public void caseABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
inABecomesSuchSubstitution(node);
@@ -681,53 +659,63 @@ public class TLAPrinter extends DepthFirstAdapter {
outABecomesSuchSubstitution(node);
}
- private void printNormalAssignment(PExpression left, PExpression right) {
- AIdentifierExpression id = (AIdentifierExpression) left;
- String name = Utils.getTIdentifierListAsString(id.getIdentifier());
- if (!machineContext.getVariables().containsKey(name)) {
- moduleStringAppend("TRUE");
- } else {
- left.apply(this);
+ @Override
+ public void caseAAssignSubstitution(AAssignSubstitution node) {
+ List<PExpression> copy = new ArrayList<>(node.getLhsExpression());
+ List<PExpression> copy2 = new ArrayList<>(node.getRhsExpressions());
+
+ for (int i = 0; i < copy.size(); i++) {
+ PExpression left = copy.get(i);
+ PExpression right = copy2.get(i);
+
+ AIdentifierExpression assigned = getAssignedIdentifier(left);
+ assigned.apply(this);
moduleStringAppend(" = ");
- right.apply(this);
+ printAssignmentRhs(assigned, right);
+
+ if (i < copy.size() - 1) {
+ moduleStringAppend(" /\\ ");
+ }
}
+
+ printUnchangedVariables(node, true);
}
- private void printFunctionAssignment(PExpression left, PExpression right) {
- PExpression var = ((AFunctionExpression) left).getIdentifier();
- LinkedList<PExpression> params = ((AFunctionExpression) left).getParameters();
- BType type = typechecker.getType(var);
- var.apply(this);
- moduleStringAppend("' = ");
- if (type instanceof FunctionType) {
- moduleStringAppend(FUNC_ASSIGN);
- moduleStringAppend("(");
- var.apply(this);
- moduleStringAppend(", ");
- if (params.size() > 1) {
- moduleStringAppend("<<");
- }
- for (Iterator<PExpression> iterator = params.iterator(); iterator
- .hasNext();) {
- PExpression pExpression = iterator.next();
- pExpression.apply(this);
- if (iterator.hasNext()) {
- moduleStringAppend(", ");
- }
- }
- if (params.size() > 1) {
- moduleStringAppend(">>");
- }
- moduleStringAppend(", ");
- right.apply(this);
- moduleStringAppend(")");
+ private AIdentifierExpression getAssignedIdentifier(PExpression left) {
+ if (left instanceof AIdentifierExpression) {
+ return (AIdentifierExpression) left;
+ } else if (left instanceof AFunctionExpression) {
+ return getAssignedIdentifier(((AFunctionExpression) left).getIdentifier());
+ } else if (left instanceof ARecordFieldExpression) {
+ return getAssignedIdentifier(((ARecordFieldExpression) left).getRecord());
} else {
- moduleStringAppend(REL_OVERRIDING + "(");
- var.apply(this);
- moduleStringAppend(", {<<");
+ throw new NotSupportedException("Unsupported assignment lhs: " + left);
+ }
+ }
- if (params.size() > 1) {
- moduleStringAppend("<<");
+ private void printAssignmentRhs(Node left, PExpression right) {
+ if (left instanceof AAssignSubstitution) {
+ right.apply(this);
+ return;
+ }
+
+ Node parent = left.parent();
+ if (left instanceof AIdentifierExpression) {
+ printAssignmentRhs(parent, right);
+ } else if (left instanceof AFunctionExpression) {
+ AFunctionExpression func = (AFunctionExpression) left;
+ PExpression ident = func.getIdentifier();
+ List<PExpression> params = func.getParameters();
+
+ BType type = typechecker.getType(ident);
+ if (type instanceof FunctionType) {
+ moduleStringAppend(FUNC_ASSIGN);
+ moduleStringAppend("(");
+ printAssignmentFunctionalOverrideBase(ident);
+ moduleStringAppend(", ");
+ if (params.size() > 1) {
+ moduleStringAppend("<<");
+ }
for (Iterator<PExpression> iterator = params.iterator(); iterator.hasNext();) {
PExpression pExpression = iterator.next();
pExpression.apply(this);
@@ -735,13 +723,136 @@ public class TLAPrinter extends DepthFirstAdapter {
moduleStringAppend(", ");
}
}
- moduleStringAppend(">>");
+ if (params.size() > 1) {
+ moduleStringAppend(">>");
+ }
+ moduleStringAppend(", ");
+ printAssignmentRhs(parent, right);
+ moduleStringAppend(")");
} else {
- params.get(0).apply(this);
+ moduleStringAppend(REL_OVERRIDING + "(");
+ printAssignmentFunctionalOverrideBase(ident);
+ moduleStringAppend(", {<<");
+ if (params.size() > 1) {
+ moduleStringAppend("<<");
+ for (Iterator<PExpression> iterator = params.iterator(); iterator.hasNext();) {
+ PExpression pExpression = iterator.next();
+ pExpression.apply(this);
+ if (iterator.hasNext()) {
+ moduleStringAppend(", ");
+ }
+ }
+ moduleStringAppend(">>");
+ } else {
+ params.get(0).apply(this);
+ }
+ moduleStringAppend(", ");
+ printAssignmentRhs(parent, right);
+ moduleStringAppend(">>})");
}
- moduleStringAppend(", ");
- right.apply(this);
- moduleStringAppend(">>})");
+ } else {
+ throw new NotSupportedException("Unsupported assignment lhs: " + left);
+ }
+ }
+
+ private void printAssignmentFunctionalOverrideBase(PExpression e) {
+ // TODO: optimize for nesting levels > 2
+ if (e instanceof AIdentifierExpression) {
+ // print without primed identifiers
+ disablePrimedNodes = true;
+ e.apply(this);
+ disablePrimedNodes = false;
+ } else if (e instanceof AFunctionExpression) {
+ AFunctionExpression func = (AFunctionExpression) e;
+ PExpression ident = func.getIdentifier();
+ LinkedList<PExpression> params = func.getParameters();
+ moduleStringAppend("(IF ");
+ BType identType = typechecker.getType(ident);
+ BType valueType = typechecker.getType(e);
+ if (identType instanceof FunctionType) {
+ if (params.size() > 1) {
+ moduleStringAppend("<<");
+ }
+ for (Iterator<PExpression> it = params.iterator(); it.hasNext();) {
+ it.next().apply(this);
+ if (it.hasNext()) {
+ moduleStringAppend(", ");
+ }
+ }
+ if (params.size() > 1) {
+ moduleStringAppend(">>");
+ }
+ moduleStringAppend( " \\in ");
+ moduleStringAppend("DOMAIN ");
+ printAssignmentFunctionalOverrideBase(ident);
+ } else {
+ if (params.size() > 1) {
+ moduleStringAppend("<<");
+ for (Iterator<PExpression> it = params.iterator(); it.hasNext();) {
+ it.next().apply(this);
+ if (it.hasNext()) {
+ moduleStringAppend(", ");
+ }
+ }
+ moduleStringAppend(">>");
+ } else {
+ params.get(0).apply(this);
+ }
+ moduleStringAppend(" \\in ");
+ moduleStringAppend(REL_DOMAIN);
+ moduleStringAppend("(");
+ printAssignmentFunctionalOverrideBase(ident);
+ moduleStringAppend(")");
+ }
+ moduleStringAppend(" THEN ");
+ if (identType instanceof FunctionType) {
+ printAssignmentFunctionalOverrideBase(ident);
+ moduleStringAppend("[");
+ if (params.size() > 1) {
+ moduleStringAppend("<<");
+ }
+ for (Iterator<PExpression> it = params.iterator(); it.hasNext();) {
+ it.next().apply(this);
+ if (it.hasNext()) {
+ moduleStringAppend(", ");
+ }
+ }
+ if (params.size() > 1) {
+ moduleStringAppend(">>");
+ }
+ moduleStringAppend("]");
+ } else {
+ if (TLC4BGlobals.checkWelldefinedness()) {
+ moduleStringAppend(REL_CALL);
+ } else {
+ moduleStringAppend(REL_CALL_WITHOUT_WD_CHECK);
+ }
+ moduleStringAppend("(");
+ printAssignmentFunctionalOverrideBase(ident);
+ moduleStringAppend(", ");
+ if (params.size() > 1) {
+ moduleStringAppend("<<");
+ for (Iterator<PExpression> it = params.iterator(); it.hasNext();) {
+ it.next().apply(this);
+ if (it.hasNext()) {
+ moduleStringAppend(", ");
+ }
+ }
+ moduleStringAppend(">>");
+ } else {
+ params.get(0).apply(this);
+ }
+ moduleStringAppend(")");
+ }
+ moduleStringAppend(" ELSE ");
+ if (valueType instanceof FunctionType) {
+ moduleStringAppend("<<>>");
+ } else {
+ moduleStringAppend("{}");
+ }
+ moduleStringAppend(")");
+ } else {
+ throw new NotSupportedException("Unsupported assignment lhs: " + e);
}
}
@@ -1169,13 +1280,13 @@ public class TLAPrinter extends DepthFirstAdapter {
if (name == null) {
name = Utils.getTIdentifierListAsString(node.getIdentifier());
}
- if (StandardModules.isAbstractConstant(name)) {
+ if (isAbstractConstant(name)) {
// in order to pass the member check
moduleStringAppend("{}");
return;
}
moduleStringAppend(name);
- if (primedNodesMarker.isPrimed(node)) {
+ if (!disablePrimedNodes && primedNodesMarker.isPrimed(node)) {
moduleStringAppend("'");
}
outAIdentifierExpression(node);
@@ -1462,7 +1573,7 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAExpressionDefinitionDefinition(AExpressionDefinitionDefinition node) {
String oldName = node.getName().getText().trim();
- if (StandardModules.isKeywordInModuleExternalFunctions(oldName)) {
+ if (isKeywordInModuleExternalFunctions(oldName)) {
return;
}
String name = renamer.getName(node);
@@ -1503,7 +1614,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
private void printBDefinition(String name, List<PExpression> args, Node rightSide) {
- if (StandardModules.isKeywordInModuleExternalFunctions(name)) {
+ if (isKeywordInModuleExternalFunctions(name)) {
return;
}
moduleStringAppend(name);
@@ -1918,7 +2029,7 @@ public class TLAPrinter extends DepthFirstAdapter {
AIdentifierExpression id = (AIdentifierExpression) node
.getIdentifier();
String name = Utils.getTIdentifierListAsString(id.getIdentifier());
- if (StandardModules.isAbstractConstant(name)) {
+ if (isAbstractConstant(name)) {
moduleStringAppend(name);
// node.getIdentifier().apply(this);
diff --git a/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
deleted file mode 100644
index 0874873923ad3e3744b84c9d7807728ffcb8299a..0000000000000000000000000000000000000000
--- a/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
+++ /dev/null
@@ -1,32 +0,0 @@
-package de.tlc4b.tlc.integration;
-
-import static de.tlc4b.tlc.TLCResults.TLCResult.*;
-import static de.tlc4b.util.TestUtil.testString;
-import static org.junit.Assert.assertEquals;
-
-import org.junit.Test;
-
-public class FixedBugs {
-
- @Test
- public void testFunctionAssignment() throws Exception {
- String machine =
- "MACHINE Test\n"
- + "VARIABLES x \n"
- + "INVARIANT x : 1..3 +-> 1..2 \n"
- + "INITIALISATION x := {} \n"
- + "OPERATIONS foo = PRE x = {} THEN x(1) := 2 END \n"
- + "END";
- assertEquals(Deadlock, testString(machine));
- }
-
- @Test
- public void testActionIdentifier() throws Exception {
- String machine =
- "MACHINE Test\n"
- + "CONSTANTS ACTION\n"
- + "PROPERTIES ACTION={1, 2, 3} \n"
- + "END";
- assertEquals(NoError, testString(machine));
- }
-}
diff --git a/src/test/java/de/tlc4b/tlc/integration/FixedBugsTest.java b/src/test/java/de/tlc4b/tlc/integration/FixedBugsTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..4ff6fb050d784d65a118717b3adc67f6e40719b9
--- /dev/null
+++ b/src/test/java/de/tlc4b/tlc/integration/FixedBugsTest.java
@@ -0,0 +1,53 @@
+package de.tlc4b.tlc.integration;
+
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.testString;
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+public class FixedBugsTest {
+
+ @Test
+ public void testActionIdentifier() throws Exception {
+ String machine =
+ "MACHINE Test\n"
+ + "CONSTANTS ACTION\n"
+ + "PROPERTIES ACTION={1, 2, 3} \n"
+ + "END";
+ assertEquals(NoError, testString(machine));
+ }
+
+ @Test
+ public void testFunctionAssignment() throws Exception {
+ String machine = "MACHINE Test\n" +
+ "VARIABLES x\n" +
+ "INVARIANT x : 1..3 +-> 1..3\n" +
+ "INITIALISATION x := {}\n" +
+ "OPERATIONS foo = SELECT x = {} THEN x(1) := 1 END\n" +
+ "END";
+ assertEquals(Deadlock, testString(machine));
+ }
+
+ @Test
+ public void testNestedFunctionAssignment2() throws Exception {
+ String machine = "MACHINE Test\n" +
+ "VARIABLES x\n" +
+ "INVARIANT x : 1..3 +-> (1..3 +-> 1..3)\n" +
+ "INITIALISATION x := {}\n" +
+ "OPERATIONS foo = SELECT x = {} THEN x(1)(2) := 1 END\n" +
+ "END";
+ assertEquals(Deadlock, testString(machine));
+ }
+
+ @Test
+ public void testNestedFunctionAssignment3() throws Exception {
+ String machine = "MACHINE Test\n" +
+ "VARIABLES x\n" +
+ "INVARIANT x : 1..3 +-> (1..3 +-> (1..3 +-> 1..3))\n" +
+ "INITIALISATION x := {}\n" +
+ "OPERATIONS foo = SELECT x = {} THEN x(1)(2)(3) := 1 END\n" +
+ "END";
+ assertEquals(Deadlock, testString(machine));
+ }
+}
diff --git a/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java b/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
index a59e2217320786428d618bcaa75d8398c86113b0..9118180df41125b5323e67cbdaa369a60a7335db 100644
--- a/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
+++ b/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
@@ -3,6 +3,7 @@ package de.tlc4b.util;
import java.io.File;
import de.tlc4b.TLC4B;
+import de.tlc4b.TLC4BGlobals;
import tlc2.TLCGlobals;
@@ -16,6 +17,7 @@ public class TLC4BRunnerTestString {
// leading to name conflicts when two tests are started within the same second.
// This line works around the issue by instead using a millisecond timestamp as the name.
TLCGlobals.metaDir = TLCGlobals.metaRoot + File.separator + System.currentTimeMillis() + File.separator;
+ TLC4BGlobals.setVerbose(true);
TLC4B.testString(args[0],true);
}