From 0a4f120cfac7c5e610ef1d858e025287e8a293c6 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 9 May 2014 12:53:40 +0200
Subject: [PATCH] Refactored the specanalyser
---
.../de/tla2b/analysis/AbstractASTVisitor.java | 62 ++-
.../java/de/tla2b/analysis/BOperation.java | 8 +-
.../java/de/tla2b/analysis/SpecAnalyser.java | 424 ++----------------
.../de/tla2b/global/TranslationGlobals.java | 2 +
.../java/de/tla2b/pprint/BMachinePrinter.java | 1 -
.../tla2b/translation/BDefinitionsFinder.java | 67 +++
.../de/tla2b/translation/BMacroHandler.java | 1 -
.../tla2b/translation/OperationsFinder.java | 161 +++++++
src/main/java/de/tla2b/translation/TLA2B.java | 1 -
.../de/tla2b/translation/Tla2BTranslator.java | 1 -
.../translation/UsedDefinitionsFinder.java | 31 +-
src/main/java/de/tla2bAst/BAstCreator.java | 2 +-
src/test/java/de/tla2b/examples/MCTest.java | 45 +-
.../RegressionTests.java | 5 +-
src/test/java/de/tla2b/main/MainTest.java | 2 +-
.../tla2b/prettyprintb/ExampleFilesTest.java | 75 ++++
.../MCTests/CarTalkPuzzle/CarTalkPuzzle.tla | 158 +++++++
.../resources/MCTests/CarTalkPuzzle/MC.cfg | 7 +
.../resources/MCTests/CarTalkPuzzle/MC.out | 53 +++
.../resources/MCTests/CarTalkPuzzle/MC.tla | 27 ++
.../resources/MCTests/CarTalkPuzzle/MC_TE.out | 53 +++
.../CarTalkPuzzle/Model2/CarTalkPuzzle.tla | 158 +++++++
.../MCTests/CarTalkPuzzle/Model2/MC.cfg | 7 +
.../MCTests/CarTalkPuzzle/Model2/MC.out | 64 +++
.../MCTests/CarTalkPuzzle/Model2/MC.tla | 25 ++
.../MCTests/CarTalkPuzzle/Model2/MC_TE.out | 64 +++
.../resources/MCTests/Invariant/Invariant.tla | 11 +
src/test/resources/MCTests/Invariant/MC.cfg | 10 +
src/test/resources/MCTests/Invariant/MC.tla | 18 +
.../RecursiveFunctions/RecursiveFunction1.tla | 5 +
.../RecursiveFunctionGlobalVariable.tla | 7 +
.../AsynchInterface/AsynchInterface.cfg | 0
.../AsynchInterface/AsynchInterface.mch | 0
.../AsynchInterface/AsynchInterface.tla | 0
.../Channel/Channel.cfg | 0
.../Channel/Channel.mch | 0
.../Channel/Channel.tla | 0
.../{examples => regression}/Club/Club.cfg | 0
.../{examples => regression}/Club/Club.mch | 0
.../{examples => regression}/Club/Club.tla | 0
.../resources/regression/Club/Club_tla.mch | 18 +
.../Counter/Counter.cfg | 0
.../Counter/Counter.mch | 0
.../Counter/Counter.tla | 0
.../DefCapture/DefCapture.mch | 0
.../DefCapture/DefCapture.tla | 0
.../DieHard/DieHard.cfg | 0
.../DieHard/DieHard.mch | 0
.../DieHard/DieHard.tla | 0
.../DieHard/DieHarder.cfg | 0
.../DieHard/DieHarder.mch | 0
.../DieHard/DieHarder.tla | 0
.../{examples => regression}/Doors/Doors.cfg | 0
.../{examples => regression}/Doors/Doors.mch | 0
.../{examples => regression}/Doors/Doors.tla | 0
.../GraphIso/GraphIso.cfg | 0
.../GraphIso/GraphIso.mch | 0
.../GraphIso/GraphIso.tla | 0
.../HourClock/HourClock.cfg | 0
.../HourClock/HourClock.mch | 0
.../HourClock/HourClock.tla | 0
.../Jukebox/Jukebox.cfg | 0
.../Jukebox/Jukebox.mch | 0
.../Jukebox/Jukebox.tla | 0
.../regression/MySequence/MySequence.cfg | 1 +
.../MySequence/MySequence.tla | 0
.../Queens/Queens.cfg | 0
.../Queens/Queens.mch | 0
.../Queens/Queens.tla | 0
.../Queens/Queens2.cfg | 0
.../Queens/Queens2.mch | 0
.../Queens/Queens2.tla | 0
.../RecursiveFunction/RecursiveFunction.mch | 0
.../RecursiveFunction/RecursiveFunction.tla | 0
.../Scheduler/Scheduler.cfg | 0
.../Scheduler/Scheduler.mch | 0
.../Scheduler/Scheduler.tla | 0
.../SimpleSATProblem/SimpleSATProblem.mch | 0
.../SimpleSATProblem/SimpleSATProblem.tla | 0
.../SumAndProduct/SumAndProductConstraint.tla | 0
.../SumAndProduct/SumAndProductTransition.tla | 0
.../uf50_02/uf50_02.tla | 0
82 files changed, 1078 insertions(+), 496 deletions(-)
create mode 100644 src/main/java/de/tla2b/translation/BDefinitionsFinder.java
create mode 100644 src/main/java/de/tla2b/translation/OperationsFinder.java
rename src/test/java/de/tla2b/{regression => examples}/RegressionTests.java (88%)
create mode 100644 src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/CarTalkPuzzle.tla
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/MC.cfg
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/MC.out
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/MC.tla
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/MC_TE.out
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/Model2/CarTalkPuzzle.tla
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.cfg
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.out
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.tla
create mode 100644 src/test/resources/MCTests/CarTalkPuzzle/Model2/MC_TE.out
create mode 100644 src/test/resources/MCTests/Invariant/Invariant.tla
create mode 100644 src/test/resources/MCTests/Invariant/MC.cfg
create mode 100644 src/test/resources/MCTests/Invariant/MC.tla
create mode 100644 src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunction1.tla
create mode 100644 src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunctionGlobalVariable.tla
rename src/test/resources/{examples => regression}/AsynchInterface/AsynchInterface.cfg (100%)
rename src/test/resources/{examples => regression}/AsynchInterface/AsynchInterface.mch (100%)
rename src/test/resources/{examples => regression}/AsynchInterface/AsynchInterface.tla (100%)
rename src/test/resources/{examples => regression}/Channel/Channel.cfg (100%)
rename src/test/resources/{examples => regression}/Channel/Channel.mch (100%)
rename src/test/resources/{examples => regression}/Channel/Channel.tla (100%)
rename src/test/resources/{examples => regression}/Club/Club.cfg (100%)
rename src/test/resources/{examples => regression}/Club/Club.mch (100%)
rename src/test/resources/{examples => regression}/Club/Club.tla (100%)
create mode 100644 src/test/resources/regression/Club/Club_tla.mch
rename src/test/resources/{examples => regression}/Counter/Counter.cfg (100%)
rename src/test/resources/{examples => regression}/Counter/Counter.mch (100%)
rename src/test/resources/{examples => regression}/Counter/Counter.tla (100%)
rename src/test/resources/{examples => regression}/DefCapture/DefCapture.mch (100%)
rename src/test/resources/{examples => regression}/DefCapture/DefCapture.tla (100%)
rename src/test/resources/{examples => regression}/DieHard/DieHard.cfg (100%)
rename src/test/resources/{examples => regression}/DieHard/DieHard.mch (100%)
rename src/test/resources/{examples => regression}/DieHard/DieHard.tla (100%)
rename src/test/resources/{examples => regression}/DieHard/DieHarder.cfg (100%)
rename src/test/resources/{examples => regression}/DieHard/DieHarder.mch (100%)
rename src/test/resources/{examples => regression}/DieHard/DieHarder.tla (100%)
rename src/test/resources/{examples => regression}/Doors/Doors.cfg (100%)
rename src/test/resources/{examples => regression}/Doors/Doors.mch (100%)
rename src/test/resources/{examples => regression}/Doors/Doors.tla (100%)
rename src/test/resources/{examples => regression}/GraphIso/GraphIso.cfg (100%)
rename src/test/resources/{examples => regression}/GraphIso/GraphIso.mch (100%)
rename src/test/resources/{examples => regression}/GraphIso/GraphIso.tla (100%)
rename src/test/resources/{examples => regression}/HourClock/HourClock.cfg (100%)
rename src/test/resources/{examples => regression}/HourClock/HourClock.mch (100%)
rename src/test/resources/{examples => regression}/HourClock/HourClock.tla (100%)
rename src/test/resources/{examples => regression}/Jukebox/Jukebox.cfg (100%)
rename src/test/resources/{examples => regression}/Jukebox/Jukebox.mch (100%)
rename src/test/resources/{examples => regression}/Jukebox/Jukebox.tla (100%)
create mode 100644 src/test/resources/regression/MySequence/MySequence.cfg
rename src/test/resources/{examples => regression}/MySequence/MySequence.tla (100%)
rename src/test/resources/{examples => regression}/Queens/Queens.cfg (100%)
rename src/test/resources/{examples => regression}/Queens/Queens.mch (100%)
rename src/test/resources/{examples => regression}/Queens/Queens.tla (100%)
rename src/test/resources/{examples => regression}/Queens/Queens2.cfg (100%)
rename src/test/resources/{examples => regression}/Queens/Queens2.mch (100%)
rename src/test/resources/{examples => regression}/Queens/Queens2.tla (100%)
rename src/test/resources/{examples => regression}/RecursiveFunction/RecursiveFunction.mch (100%)
rename src/test/resources/{examples => regression}/RecursiveFunction/RecursiveFunction.tla (100%)
rename src/test/resources/{examples => regression}/Scheduler/Scheduler.cfg (100%)
rename src/test/resources/{examples => regression}/Scheduler/Scheduler.mch (100%)
rename src/test/resources/{examples => regression}/Scheduler/Scheduler.tla (100%)
rename src/test/resources/{examples => regression}/SimpleSATProblem/SimpleSATProblem.mch (100%)
rename src/test/resources/{examples => regression}/SimpleSATProblem/SimpleSATProblem.tla (100%)
rename src/test/resources/{examples => regression}/SumAndProduct/SumAndProductConstraint.tla (100%)
rename src/test/resources/{examples => regression}/SumAndProduct/SumAndProductTransition.tla (100%)
rename src/test/resources/{examples => regression}/uf50_02/uf50_02.tla (100%)
diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index b49e64a..c606330 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -53,72 +53,64 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
}
- public void visitExprNode(ExprNode n) {
-
- switch (n.getKind()) {
+ public void visitExprNode(ExprNode node) {
+ switch (node.getKind()) {
case OpApplKind: {
- visitOpApplNode((OpApplNode) n);
+ visitOpApplNode((OpApplNode) node);
return;
}
-
case NumeralKind: {
- visitNumeralNode((NumeralNode) n);
+ visitNumeralNode((NumeralNode) node);
return;
}
-
case StringKind: {
- visitStringNode((StringNode) n);
+ visitStringNode((StringNode) node);
return;
}
-
case SubstInKind: {
- visitStubstInNode((SubstInNode) n);
+ visitStubstInNode((SubstInNode) node);
return;
}
case AtNodeKind: { // @
- visitAtNode((AtNode) n);
+ visitAtNode((AtNode) node);
return;
}
-
case LetInKind: {
- visitLetInNode((LetInNode) n);
+ visitLetInNode((LetInNode) node);
return;
}
-
}
}
- public void visitOpApplNode(OpApplNode n) {
- switch (n.getOperator().getKind()) {
+ public void visitOpApplNode(OpApplNode node) {
+ switch (node.getOperator().getKind()) {
case VariableDeclKind: {
- visitVariableNode(n);
+ visitVariableNode(node);
return;
}
case ConstantDeclKind: {
- visitConstantNode(n);
+ visitConstantNode(node);
return;
}
case FormalParamKind: {
- visitFormalParamNode(n);
+ visitFormalParamNode(node);
return;
}
case BuiltInKind: {
- visitBuiltInNode(n);
+ visitBuiltInNode(node);
return;
}
case UserDefinedOpKind: {
-
- if(BBuiltInOPs.contains(n.getOperator().getName())){
- visitBBuiltinsNode(n);
+ if (BBuiltInOPs.contains(node.getOperator().getName())) {
+ visitBBuiltinsNode(node);
return;
- }else{
- visitUserDefinedNode(n);
+ } else {
+ visitUserDefinedNode(node);
return;
}
-
}
}
@@ -130,7 +122,7 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
for (ExprNode exprNode : in) {
visitExprNode(exprNode);
}
-
+
ExprOrOpArgNode[] arguments = n.getArgs();
for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
visitExprOrOpArgNode(exprOrOpArgNode);
@@ -142,23 +134,23 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
for (ExprNode exprNode : in) {
visitExprNode(exprNode);
}
-
+
ExprOrOpArgNode[] arguments = n.getArgs();
for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
- // exprOrOpArgNode == null in case the OTHER construct
- if(exprOrOpArgNode != null){
+ // exprOrOpArgNode == null in case the OTHER construct
+ if (exprOrOpArgNode != null) {
visitExprOrOpArgNode(exprOrOpArgNode);
}
-
+
}
}
- public void visitLetInNode(LetInNode n) {
- OpDefNode[] lets = n.getLets();
+ public void visitLetInNode(LetInNode node) {
+ OpDefNode[] lets = node.getLets();
for (OpDefNode opDefNode : lets) {
visitLocalDefinition(opDefNode);
}
- visitExprNode(n.getBody());
+ visitExprNode(node.getBody());
}
public void visitLocalDefinition(OpDefNode opDefNode) {
@@ -174,8 +166,6 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
}
public void visitUserDefinedNode(OpApplNode n) {
-
-
for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
visitExprOrOpArgNode(exprOrOpArgNode);
}
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index d849ded..8ffcf1b 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -55,8 +55,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private List<OpDeclNode> anyVariables;
private final SpecAnalyser specAnalyser;
- final int SUBSTITUTE_PARAM = 29;
-
public BOperation(String name, ExprNode n,
ArrayList<OpApplNode> existQuans, SpecAnalyser specAnalyser) {
this.name = name;
@@ -220,9 +218,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
anyVariables.add(var);
}
-// for (SymbolNode symbol : primedVariablesFinder.getAllVariables()) {
-// anyVariables.add((OpDeclNode) symbol);
-// }
+ // for (SymbolNode symbol : primedVariablesFinder.getAllVariables()) {
+ // anyVariables.add((OpDeclNode) symbol);
+ // }
anyVariables.removeAll(assignments.keySet());
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index d42406e..c7fec44 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -17,22 +17,19 @@ import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.SemanticErrorException;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
+import de.tla2b.translation.BDefinitionsFinder;
+import de.tla2b.translation.OperationsFinder;
import de.tla2b.translation.UsedDefinitionsFinder;
import de.tla2b.types.IType;
import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.NumeralNode;
import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpArgNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
@@ -42,24 +39,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private OpDefNode spec;
private OpDefNode init;
private OpDefNode next;
- private ArrayList<OpDefNode> invariants;
+ private ArrayList<OpDefNode> invariants = new ArrayList<OpDefNode>();
private final ModuleNode moduleNode;
private ExprNode nextExpr;
- private String nextName;
private ArrayList<OpDeclNode> bConstants;
// used to check if a b constant has arguments and is not overriden in the
// configfile
- private final ArrayList<BOperation> bOperations = new ArrayList<BOperation>();
- private ArrayList<ExprNode> inits;
- private ArrayList<LetInNode> globalLets = new ArrayList<LetInNode>();
- // these local definitions occur in assume nodes or in BOperations and will
- // be added in the front part of the definitions clause of the resulting B
- // Machine
-
- private ArrayList<OpApplNode> ifThenElseNodes = new ArrayList<OpApplNode>();
+ private ArrayList<BOperation> bOperations = new ArrayList<BOperation>();
+ private ArrayList<ExprNode> inits = new ArrayList<ExprNode>();
private Set<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
// set of OpDefNodes which will appear in the resulting B Machine
@@ -120,13 +110,30 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
evalInit();
evalNext();
}
- findOperations();
- findDefinitions();
+ for (OpDefNode inv : new ArrayList<OpDefNode>(invariants)) {
+ try {
+ OpApplNode opApplNode = (OpApplNode) inv.getBody();
+
+ OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
+
+ if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())){
+ int i = invariants.indexOf(inv);
+ invariants.set(i, opDefNode);
+ }
+ } catch (ClassCastException e) {
+ }
+ }
+
+
+ OperationsFinder operationsFinder = new OperationsFinder(this);
+ bOperations = operationsFinder.getBOperations();
UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
+ this.usedDefinitions = definitionFinder.getUsedDefinitions();
- usedDefinitions = definitionFinder.getUsedDefinitions();
+ BDefinitionsFinder bDefinitionFinder = new BDefinitionsFinder(this);
+ this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
//usedDefinitions.addAll(bDefinitionsSet);
// test whether there is a init predicate if there is a variable
@@ -144,13 +151,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
con.getName()));
}
}
- evalRecursiveFunctions();
+ findRecursiveConstructs();
}
private void evalInit() {
if (init != null) {
- inits = new ArrayList<ExprNode>();
- inits = new ArrayList<ExprNode>();
inits.add(init.getBody());
}
}
@@ -158,13 +163,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private void evalNext() throws FrontEndException {
if (next != null) {
this.nextExpr = next.getBody();
- this.nextName = next.getName().toString();
}
}
public void evalSpec() throws SemanticErrorException, FrontEndException {
if (spec != null) {
- inits = new ArrayList<ExprNode>();
processConfigSpec(spec.getBody());
}
@@ -208,7 +211,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
.getOperator().getName()) == OPCODE_sa) {
ExprNode next = (ExprNode) ((OpApplNode) boxArg).getArgs()[0];
this.nextExpr = next;
- this.nextName = "Next";
return;
}
}
@@ -226,366 +228,14 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
- /**
- * Searches for BOperations in a ExprNode. BOperations are seperated with
- * the aid of the disjunction (\/) operator.
- *
- * @param exprNode
- * @param opName
- * the name of the definition where exprNode occur
- * @throws FrontEndException
- * @throws ConfigFileErrorException
- */
- private void findOperations() throws FrontEndException,
- ConfigFileErrorException {
- if (nextExpr == null)
- return;
- findOperationsInSemanticNode(nextExpr, nextName,
- new ArrayList<OpApplNode>());
- }
-
- /**
- *
- * @param node
- * @param opName
- * @param existQuans
- * a list containing all existential quantifier which will be
- * parameters in the resulting B Maschine
- * @throws FrontEndException
- * @throws ConfigFileErrorException
- */
- private void findOperationsInSemanticNode(SemanticNode node, String opName,
- ArrayList<OpApplNode> existQuans) throws FrontEndException,
- ConfigFileErrorException {
- switch (node.getKind()) {
- case OpApplKind: {
- findOperationsInOpApplNode((OpApplNode) node, opName, existQuans);
- return;
- }
- case LetInKind: {
- LetInNode letInNode = (LetInNode) node;
- globalLets.add(letInNode);
-
- findOperationsInSemanticNode(letInNode.getBody(), opName,
- existQuans);
- return;
- }
- case NumeralKind: {
- int val = ((NumeralNode) node).val();
- throw new FrontEndException(String.format(
- "Expected an action at '%s'.\n%s", val, node.getLocation()
- .toString()));
- }
-
- case StringKind: {
- StringNode s = (StringNode) node;
- throw new FrontEndException(String.format(
- "Expected an action at '\"%s\"'.\n%s", s.getRep(), node
- .getLocation().toString()));
- }
-
- default:
- throw new FrontEndException(String.format(
- "Expected an action.\n%s", node.getLocation().toString()));
- }
-
- }
-
- private void findOperationsInOpApplNode(OpApplNode n, String name,
- ArrayList<OpApplNode> existQuans) throws FrontEndException,
- ConfigFileErrorException {
- int kind = n.getOperator().getKind();
- if (kind == UserDefinedOpKind
- && !BBuiltInOPs.contains(n.getOperator().getName())) {
- OpDefNode def = (OpDefNode) n.getOperator();
- usedDefinitions.add(def);
- if (def.getParams().length > 0) {
- BOperation op = new BOperation(def.getName().toString(), n,
- existQuans, this);
- bOperations.add(op);
- return;
- } else {
- findOperationsInSemanticNode(def.getBody(), def.getName()
- .toString(), existQuans);
- return;
- }
-
- } else if (kind == BuiltInKind) {
- int opcode = BuiltInOPs.getOpCode(n.getOperator().getName());
- switch (opcode) {
- case OPCODE_dl: // DisjList
- {
- if (n.getArgs().length == 1) {
- findOperationsInSemanticNode(n.getArgs()[0], name,
- existQuans);
- return;
- }
- for (int i = 0; i < n.getArgs().length; i++) {
- findOperationsInSemanticNode(n.getArgs()[i],
- name + (i + 1), existQuans);
- }
- return;
- }
- case OPCODE_lor: {
- for (int i = 0; i < n.getArgs().length; i++) {
- findOperationsInSemanticNode(n.getArgs()[i],
- name + (i + 1), existQuans);
- }
- return;
- }
- case OPCODE_be: { // BoundedExists
- ArrayList<OpApplNode> clone = new ArrayList<OpApplNode>(
- existQuans);
- clone.add(n);
- findOperationsInSemanticNode(n.getArgs()[0], name, clone);
- return;
- }
-
- case OPCODE_unchanged:
- case OPCODE_eq: // =
- case OPCODE_noteq: // /=, #
- case OPCODE_neg: // Negation
- case OPCODE_lnot: // Negation
- case OPCODE_cl: // $ConjList
- case OPCODE_land: // \land
- case OPCODE_equiv: // \equiv
- case OPCODE_implies: // =>
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_in: // \in
- case OPCODE_notin: // \notin
- case OPCODE_subseteq: // \subseteq - subset or equal
- case OPCODE_fa: // $FcnApply f[1]
- case OPCODE_ite: // IF THEN ELSE
- case OPCODE_case: {
- BOperation op = new BOperation(name, n, existQuans, this);
- bOperations.add(op);
- return;
- }
- }
- }
- throw new FrontEndException(String.format(
- "Expected an action at '%s' :\n%s", n.getOperator().getName()
- .toString(), n.getLocation().toString()));
-
- }
-
- /**
- *
- * @throws ConfigFileErrorException
- */
-
- private void findDefinitions() throws ConfigFileErrorException {
- if (configFileEvaluator != null) {
- bDefinitionsSet.addAll(configFileEvaluator.getConstantOverrideTable().values());
- }
-
- AssumeNode[] assumes = moduleNode.getAssumptions();
- for (int i = 0; i < assumes.length; i++) {
- findDefintionInExprNode(assumes[i].getAssume(), null);
- }
-
- if (inits != null) {
- for (int i = 0; i < inits.size(); i++) {
- findDefintionInExprNode(inits.get(i), null);
- }
- }
-
-
-// if(nextExpr != null){
-// findDefintionInExprNode(nextExpr, null);
-// }
- if (bOperations != null) {
- for (int i = 0; i < bOperations.size(); i++) {
- ExprNode node = bOperations.get(i).getNode();
-
- if (node instanceof OpApplNode) {
- OpApplNode opApplNode = (OpApplNode) node;
- if (opApplNode.getOperator().getKind() == UserDefinedOpKind
- && !BBuiltInOPs.contains(opApplNode.getOperator()
- .getName())) {
- OpDefNode def = (OpDefNode) opApplNode.getOperator();
- node = def.getBody();
- }
- }
- findDefintionInExprNode(node, null);
- }
- }
-
- if (invariants != null) {
- for (int i = 0; i < invariants.size(); i++) {
- OpDefNode def = invariants.get(i);
- bDefinitionsSet.add(def);
- findDefintionInExprNode(def.getBody(), null);
- }
- }
-
- for (int i = 0; i < globalLets.size(); i++) {
- LetInNode letInNode = globalLets.get(i);
- for (int j = 0; j < letInNode.getLets().length; j++) {
- findDefintionInExprNode(letInNode.getLets()[j].getBody(), null);
- }
- }
-
- HashSet<OpDefNode> defSet = new HashSet<OpDefNode>(bDefinitionsSet);
- for (OpDefNode def : defSet) {
- findDefintionInExprNode(def.getBody(), null);
- }
-
- //bDefinitionsSet.remove(next);
- }
-
- /**
- * @param exprOrOpArgNode
- */
- private void findDefintionInExprOrOpArgNode(ExprOrOpArgNode n,
- FormalParamNode[] parameters) {
- if (n instanceof ExprNode) {
- findDefintionInExprNode((ExprNode) n, parameters);
- } else if (n instanceof OpArgNode) {
-
- }
- }
-
- private void findDefintionInExprNode(ExprNode node,
- FormalParamNode[] parameters) {
- switch (node.getKind()) {
- case OpApplKind: {
- findDefinitionInOpApplNode((OpApplNode) node, parameters);
- return;
- }
- case LetInKind: {
- LetInNode l = (LetInNode) node;
- for (int i = 0; i < l.getLets().length; i++) {
- OpDefNode letDef = l.getLets()[i];
-
- if (parameters != null)
- letParams.put(letDef, parameters);
-
- findDefintionInExprNode(letDef.getBody(), letDef.getParams());
- }
- findDefintionInExprNode(l.getBody(), parameters);
- return;
- }
-
- }
- }
-
- /**
- * @param node
- * @throws ConfigFileErrorException
- */
- private void findDefinitionInOpApplNode(OpApplNode node,
- FormalParamNode[] parameters) {
- switch (node.getOperator().getKind()) {
- case ConstantDeclKind: {
- for (int i = 0; i < node.getArgs().length; i++) {
- findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
- }
- return;
- }
-
- case VariableDeclKind: {
- for (int i = 0; i < node.getArgs().length; i++) {
- findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
- }
- return;
- }
-
- case BuiltInKind: {
- findDefinitionInBuiltInKind(node, parameters);
- return;
- }
-
- case UserDefinedOpKind: {
- OpDefNode def = (OpDefNode) node.getOperator();
- // TODO
- ModuleNode moduleNode = def.getSource()
- .getOriginallyDefinedInModuleNode();
- if (moduleNode.getName().toString().equals("TLA2B")) {
- return;
- }
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName()
- .toString())) {
-
- for (int i = 0; i < node.getArgs().length; i++) {
- findDefintionInExprOrOpArgNode(node.getArgs()[i],
- parameters);
- }
- return;
- }
- if (bDefinitionsSet.add(def)) {
- findDefintionInExprNode(def.getBody(), def.getParams());
- }
-
- for (int i = 0; i < node.getArgs().length; i++) {
- findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
- }
- return;
- }
-
- }
-
- }
-
- /**
- * @param node
- */
- private void findDefinitionInBuiltInKind(OpApplNode node,
- FormalParamNode[] parameters) {
- switch (BuiltInOPs.getOpCode(node.getOperator().getName())) {
-
- case OPCODE_be:
- case OPCODE_bf:
- case OPCODE_soa:
- case OPCODE_sso:
- case OPCODE_nrfs:
- case OPCODE_fc: {
- ExprNode[] in = node.getBdedQuantBounds();
- for (int i = 0; i < in.length; i++) {
- findDefintionInExprNode(in[i], parameters);
- }
- break;
- }
- case OPCODE_ite: {
- ifThenElseNodes.add(node);
- // if(!definitionMacro.contains(IF_THEN_ELSE)){
- // definitionMacro.add(IF_THEN_ELSE);
- // }
- break;
- }
-
- case OPCODE_bc: {
- if (!definitionMacros.contains(CHOOSE)) {
- definitionMacros.add(CHOOSE);
- }
- break;
- }
- case OPCODE_unchanged: {
- return;
- }
- }
- for (int i = 0; i < node.getArgs().length; i++) {
- findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
- }
- }
-
- /**
- * @throws NotImplementedException
- *
- */
- private void evalRecursiveFunctions() throws NotImplementedException {
+ private void findRecursiveConstructs() throws NotImplementedException {
Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
for (OpDefNode def : set) {
if (def.getInRecursive()) {
bDefinitionsSet.remove(def);
- // System.out.println(def.toString(7));
RecursiveDefinition rd = new RecursiveDefinition(def);
recursiveDefinitions.add(rd);
} else
-
- // System.out.println(def.toString(4));
if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
switch (getOpCode(o.getOperator().getName())) {
@@ -598,22 +248,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
- // public void evalIfThenElse() {
- // boolean b = false;
- // for (int i = 0; i < ifThenElseNodes.size() && !b; i++) {
- // OpApplNode node = ifThenElseNodes.get(i);
- // TLAType t = (TLAType) node.getToolObject(TYPE_ID);
- // if (t.getKind() != BOOL)
- // b = true;
- // }
- // if (b)
- // definitionMacros.add(IF_THEN_ELSE);
- // }
-
- public ArrayList<LetInNode> getGlobalLets() {
- return this.globalLets;
- }
-
public ArrayList<BOperation> getBOperations() {
return this.bOperations;
}
@@ -662,4 +296,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return invariants;
}
+ public OpDefNode getInitDef(){
+ return init;
+ }
+
}
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 3fcfb30..692bdd5 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -22,6 +22,8 @@ public interface TranslationGlobals {
final int TYPE_ID = 5;
final int LET_PARAMS_ID = 13;
final int NEW_NAME = 20;
+
+ final int SUBSTITUTE_PARAM = 29;
final String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
final String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
diff --git a/src/main/java/de/tla2b/pprint/BMachinePrinter.java b/src/main/java/de/tla2b/pprint/BMachinePrinter.java
index f9499be..147ec15 100644
--- a/src/main/java/de/tla2b/pprint/BMachinePrinter.java
+++ b/src/main/java/de/tla2b/pprint/BMachinePrinter.java
@@ -73,7 +73,6 @@ public class BMachinePrinter extends AbstractExpressionPrinter implements
this.inits = specAnalyser.getInits();
this.bOperations = specAnalyser.getBOperations();
- this.globalLets = specAnalyser.getGlobalLets();
this.definitionMacro = specAnalyser.getDefinitionMacros();
this.bDefinitions = specAnalyser.getBDefinitions();
this.letParams = specAnalyser.getLetParams();
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
new file mode 100644
index 0000000..5272dc7
--- /dev/null
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -0,0 +1,67 @@
+package de.tla2b.translation;
+
+import java.util.HashSet;
+
+import tla2sany.semantic.ASTConstants;
+import tla2sany.semantic.AssumeNode;
+import tla2sany.semantic.ExprOrOpArgNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tlc2.tool.ToolGlobals;
+import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.BOperation;
+import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.global.TranslationGlobals;
+import de.tla2b.types.IType;
+
+public class BDefinitionsFinder extends AbstractASTVisitor implements
+ ASTConstants, ToolGlobals, IType, TranslationGlobals {
+ private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
+
+ public BDefinitionsFinder(SpecAnalyser specAnalyser) {
+ if (specAnalyser.getConfigFileEvaluator() != null) {
+ bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
+ .getConstantOverrideTable().values());
+ bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
+ .getOperatorOverrideTable().values());
+ }
+
+ for (BOperation op : specAnalyser.getBOperations()) {
+ visitExprNode(op.getNode());
+ }
+
+ if (specAnalyser.getInits() != null) {
+ for (int i = 0; i < specAnalyser.getInits().size(); i++) {
+ visitExprNode(specAnalyser.getInits().get(i));
+ }
+ }
+
+ for (AssumeNode assume : specAnalyser.getModuleNode().getAssumptions()) {
+ visitAssumeNode(assume);
+ }
+
+ for (OpDefNode def : specAnalyser.getInvariants()) {
+ bDefinitionsSet.add(def);
+ }
+
+
+ HashSet<OpDefNode> temp = new HashSet<OpDefNode>(bDefinitionsSet);
+ for (OpDefNode opDefNode : temp) {
+ visitExprNode(opDefNode.getBody());
+ }
+ }
+
+ public void visitUserDefinedNode(OpApplNode n) {
+ OpDefNode def = (OpDefNode) n.getOperator();
+ bDefinitionsSet.add(def);
+ visitExprNode(def.getBody());
+ for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ }
+
+ public HashSet<OpDefNode> getBDefinitionsSet() {
+ return bDefinitionsSet;
+ }
+
+}
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index 6ef40fa..04237df 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -15,7 +15,6 @@ import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SymbolNode;
import de.tla2b.analysis.AbstractASTVisitor;
-import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.config.ConfigfileEvaluator;
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
new file mode 100644
index 0000000..3051cd2
--- /dev/null
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -0,0 +1,161 @@
+package de.tla2b.translation;
+
+import java.util.ArrayList;
+
+import tla2sany.semantic.ASTConstants;
+import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.FormalParamNode;
+import tla2sany.semantic.LetInNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tlc2.tool.BuiltInOPs;
+import tlc2.tool.ToolGlobals;
+import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.BOperation;
+import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.global.BBuiltInOPs;
+import de.tla2b.global.TranslationGlobals;
+import de.tla2b.types.IType;
+
+public class OperationsFinder extends AbstractASTVisitor implements
+ ASTConstants, ToolGlobals, IType, TranslationGlobals {
+ private final SpecAnalyser specAnalyser;
+
+ private String currentName;
+ private ArrayList<OpApplNode> exists;
+ // a list containing all existential quantifier which will be parameters in
+ // the resulting B Maschine
+
+ private final ArrayList<BOperation> bOperations;
+
+ public OperationsFinder(SpecAnalyser specAnalyser) {
+ this.specAnalyser = specAnalyser;
+ this.bOperations = new ArrayList<BOperation>();
+ if (specAnalyser.getNext() != null) {
+
+ currentName = "Next";
+ exists = new ArrayList<OpApplNode>();
+ visitExprNode(specAnalyser.getNext());
+ }
+ }
+
+
+ public void visitExprNode(ExprNode n) {
+ switch (n.getKind()) {
+ case OpApplKind: {
+ visitOpApplNode((OpApplNode) n);
+ return;
+ }
+ case NumeralKind: {
+ throw new RuntimeException(String.format(
+ "Expected an action.\n%s", n.getLocation().toString()));
+ }
+ case StringKind: {
+ throw new RuntimeException(String.format(
+ "Expected an action.\n%s", n.getLocation().toString()));
+ }
+ case SubstInKind: {
+ throw new RuntimeException(String.format(
+ "Expected an action.\n%s", n.getLocation().toString()));
+ }
+ case AtNodeKind: { // @
+ throw new RuntimeException(String.format(
+ "Expected an action.\n%s", n.getLocation().toString()));
+ }
+ case LetInKind: {
+ // we do not visit the local definitions
+ visitExprNode(((LetInNode) n).getBody());
+ return;
+ }
+ }
+ }
+
+ public void visitUserDefinedNode(OpApplNode n) {
+ OpDefNode def = (OpDefNode) n.getOperator();
+ if (BBuiltInOPs.contains(def.getName())) {
+ BOperation op = new BOperation(def.getName().toString(), n, exists,
+ specAnalyser);
+ bOperations.add(op);
+ return;
+ }
+
+ for (int i = 0; i < def.getParams().length; i++) {
+ FormalParamNode param = def.getParams()[i];
+ param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
+ }
+ currentName = def.getName().toString();
+ visitExprNode(def.getBody());
+ }
+
+ @Override
+ public void visitBuiltInNode(OpApplNode n) {
+ int opcode = BuiltInOPs.getOpCode(n.getOperator().getName());
+ switch (opcode) {
+ case OPCODE_dl: // DisjList
+ {
+ if (n.getArgs().length == 1) {
+ visitExprOrOpArgNode(n.getArgs()[0]);
+ return;
+ } else {
+ String oldName = currentName;
+ ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(
+ exists);
+
+ for (int i = 0; i < n.getArgs().length; i++) {
+ exists = new ArrayList<OpApplNode>(oldExists);
+ currentName = oldName;
+ visitExprOrOpArgNode(n.getArgs()[i]);
+ }
+ return;
+ }
+ }
+ case OPCODE_lor: {
+ String oldName = currentName;
+ ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(exists);
+
+ for (int i = 0; i < n.getArgs().length; i++) {
+ exists = new ArrayList<OpApplNode>(oldExists);
+ currentName = oldName;
+ visitExprOrOpArgNode(n.getArgs()[i]);
+ }
+ return;
+ }
+ case OPCODE_be: { // BoundedExists
+ exists.add(n);
+ visitExprOrOpArgNode(n.getArgs()[0]);
+ return;
+ }
+
+ case OPCODE_unchanged:
+ case OPCODE_eq: // =
+ case OPCODE_noteq: // /=, #
+ case OPCODE_neg: // Negation
+ case OPCODE_lnot: // Negation
+ case OPCODE_cl: // $ConjList
+ case OPCODE_land: // \land
+ case OPCODE_equiv: // \equiv
+ case OPCODE_implies: // =>
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_in: // \in
+ case OPCODE_notin: // \notin
+ case OPCODE_subseteq: // \subseteq - subset or equal
+ case OPCODE_fa: // $FcnApply f[1]
+ case OPCODE_ite: // IF THEN ELSE
+ case OPCODE_case: {
+ BOperation op = new BOperation(currentName, n, exists, specAnalyser);
+ bOperations.add(op);
+ return;
+ }
+
+ }
+ throw new RuntimeException(String.format(
+ "Expected an action at '%s' :\n%s", n.getOperator().getName()
+ .toString(), n.getLocation().toString()));
+
+ }
+
+ public ArrayList<BOperation> getBOperations() {
+ return bOperations;
+ }
+
+}
diff --git a/src/main/java/de/tla2b/translation/TLA2B.java b/src/main/java/de/tla2b/translation/TLA2B.java
index 9c01419..0875681 100644
--- a/src/main/java/de/tla2b/translation/TLA2B.java
+++ b/src/main/java/de/tla2b/translation/TLA2B.java
@@ -16,7 +16,6 @@ import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.util.FileUtils;
import util.FileUtil;
import util.ToolIO;
diff --git a/src/main/java/de/tla2b/translation/Tla2BTranslator.java b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
index 64c0659..92c97f2 100644
--- a/src/main/java/de/tla2b/translation/Tla2BTranslator.java
+++ b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
@@ -13,7 +13,6 @@ import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.util.FileUtils;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 8fd0f23..679a7f9 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -19,34 +19,40 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
private final HashSet<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
+
public UsedDefinitionsFinder(SpecAnalyser specAnalyser) {
-
- if(specAnalyser.getConfigFileEvaluator() != null){
- Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values();
+
+ if (specAnalyser.getConfigFileEvaluator() != null) {
+ Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator()
+ .getConstantOverrideTable().values();
for (OpDefNode def : cons) {
visitExprNode(def.getBody());
}
- Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values();
+ Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator()
+ .getOperatorOverrideTable().values();
for (OpDefNode def : cons) {
visitExprNode(def.getBody());
}
usedDefinitions.addAll(cons);
usedDefinitions.addAll(ops);
}
-
+
visitAssumptions(specAnalyser.getModuleNode().getAssumptions());
-
-
- if(specAnalyser.getNext() != null){
+
+ if (specAnalyser.getNext() != null) {
visitExprNode(specAnalyser.getNext());
}
+ if (specAnalyser.getInitDef() != null) {
+ usedDefinitions.add(specAnalyser.getInitDef());
+ }
+
if (specAnalyser.getInits() != null) {
for (int i = 0; i < specAnalyser.getInits().size(); i++) {
visitExprNode(specAnalyser.getInits().get(i));
}
}
-
+
if (specAnalyser.getInvariants() != null) {
for (int i = 0; i < specAnalyser.getInvariants().size(); i++) {
OpDefNode def = specAnalyser.getInvariants().get(i);
@@ -56,14 +62,14 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
}
}
- public HashSet<OpDefNode> getUsedDefinitions(){
+ public HashSet<OpDefNode> getUsedDefinitions() {
return usedDefinitions;
}
-
+
@Override
public void visitUserDefinedNode(OpApplNode n) {
super.visitUserDefinedNode(n);
-
+
OpDefNode def = (OpDefNode) n.getOperator();
ModuleNode moduleNode = def.getSource()
.getOriginallyDefinedInModuleNode();
@@ -80,6 +86,5 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
visitExprNode(def.getBody());
}
-
}
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index d4da3ff..730c6d3 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -159,7 +159,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private final BMacroHandler bMacroHandler;
private final RecursiveFunctionHandler recursiveFunctionHandler;
- final int SUBSTITUTE_PARAM = 29;
+
final HashSet<OpDefNode> allTLADefinitions;
List<OpDeclNode> bConstants;
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index ee9ee41..2526a1f 100644
--- a/src/test/java/de/tla2b/examples/MCTest.java
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -8,14 +8,14 @@ import static de.tla2b.util.TestUtil.runModule;
public class MCTest {
@Test
- public void testClub() throws Exception {
- String file = "src/test/resources/examples/Club/Club.tla";
+ public void testSimpleMC() throws Exception {
+ String file = "src/test/resources/MCTests/simple/MC.tla";
runModule(file);
}
-
+
@Test
- public void testSimpleMC() throws Exception {
- String file = "src/test/resources/MCTests/simple/MC.tla";
+ public void testInvariantMC() throws Exception {
+ String file = "src/test/resources/MCTests/Invariant/MC.tla";
runModule(file);
}
@@ -56,12 +56,6 @@ public class MCTest {
}
- @Test
- public void testChannel() throws Exception {
- String file = "src/test/resources/examples/Channel/Channel.tla";
- runModule(file);
- }
-
@Ignore
@Test
public void testCarTalkPuzzle() throws Exception {
@@ -76,12 +70,6 @@ public class MCTest {
runModule(file);
}
- @Test
- public void testSequences() throws Exception {
- String file = "src/test/resources/examples/MySequence/MySequence.tla";
- runModule(file);
- }
-
@Ignore
@Test
public void testRecursiveFunciton() throws Exception {
@@ -95,33 +83,10 @@ public class MCTest {
runModule(file);
}
- @Test
- public void testSumAndProduct() throws Exception {
- String file = "src/test/resources/examples/SumAndProduct/SumAndProductTransition.tla";
- runModule(file);
- }
-
@Test
public void testMacroTest() throws Exception {
String file = "src/test/resources/renamer/MacroTest/MacroTest.tla";
runModule(file);
}
- @Test
- public void testSumAndProductConstraint() throws Exception {
- String file = "src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla";
- runModule(file);
- }
-
- @Test
- public void testuf50_02() throws Exception {
- String file = "src/test/resources/examples/uf50_02/uf50_02.tla";
- runModule(file);
- }
-
- @Test
- public void testRecursiveFunction() throws Exception {
- String file = "src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla";
- runModule(file);
- }
}
diff --git a/src/test/java/de/tla2b/regression/RegressionTests.java b/src/test/java/de/tla2b/examples/RegressionTests.java
similarity index 88%
rename from src/test/java/de/tla2b/regression/RegressionTests.java
rename to src/test/java/de/tla2b/examples/RegressionTests.java
index 36e9651..d5b0220 100644
--- a/src/test/java/de/tla2b/regression/RegressionTests.java
+++ b/src/test/java/de/tla2b/examples/RegressionTests.java
@@ -1,4 +1,4 @@
-package de.tla2b.regression;
+package de.tla2b.examples;
import static de.tla2b.util.TestUtil.runModule;
@@ -33,8 +33,7 @@ public class RegressionTests extends AbstractParseModuleTest{
final ArrayList<String> list = new ArrayList<String>();
final ArrayList<String> ignoreList = new ArrayList<String>();
- list.add("./src/test/resources/examples");
- ignoreList.add("./src/test/resources/testing/");
+ list.add("./src/test/resources/regression");
return getConfiguration2(list, ignoreList);
}
}
diff --git a/src/test/java/de/tla2b/main/MainTest.java b/src/test/java/de/tla2b/main/MainTest.java
index 08a6200..a8e832b 100644
--- a/src/test/java/de/tla2b/main/MainTest.java
+++ b/src/test/java/de/tla2b/main/MainTest.java
@@ -8,7 +8,7 @@ public class MainTest {
@Test
public void testClub() throws Exception {
- String file = "src/test/resources/examples/Club/Club.tla";
+ String file = "src/test/resources/regression/Club/Club.tla";
TLA2B.main(new String[] { file });
}
diff --git a/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java b/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java
new file mode 100644
index 0000000..efbb272
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java
@@ -0,0 +1,75 @@
+package de.tla2b.prettyprintb;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.node.Start;
+import de.tla2b.output.ASTPrettyPrinter;
+import de.tla2b.util.AbstractParseModuleTest;
+import de.tla2b.util.FileUtils;
+import de.tla2b.util.PolySuite;
+import de.tla2b.util.TestUtil;
+import de.tla2b.util.PolySuite.Config;
+import de.tla2b.util.PolySuite.Configuration;
+import de.tla2bAst.Translator;
+import static org.junit.Assert.assertEquals;
+
+@RunWith(PolySuite.class)
+public class ExampleFilesTest extends AbstractParseModuleTest {
+
+ private final File moduleFile;
+
+ public ExampleFilesTest(File machine, Object result) {
+ this.moduleFile = machine;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ // String[] a = new String[] { moduleFile.getPath() };
+ System.out.println(moduleFile.getPath());
+ // runModule(moduleFile.getPath());
+ Translator t = new Translator(moduleFile.getPath());
+ Start start = t.translate();
+ String resultTree = TestUtil.getTreeAsString(start);
+
+ ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ start.apply(aP);
+ System.out.println(aP.getResultString());
+
+ // parse pretty print result
+ final BParser parser = new BParser("testcase");
+ final Start ppStart = parser.parse(aP.getResultString(), false);
+ String ppTree = TestUtil.getTreeAsString(ppStart);
+
+ // comparing result with pretty print
+ assertEquals(resultTree, ppTree);
+
+
+ // machine file
+ String machinePath = FileUtils.removeExtention(moduleFile.getPath())
+ + ".mch";
+ File expectedMachine = new File(machinePath);
+
+ final BParser expectedParser = new BParser("testcase");
+ final Start expectedStart = expectedParser.parseFile(expectedMachine,
+ false);
+
+ String expectedTree = TestUtil.getTreeAsString(expectedStart);
+
+ assertEquals(expectedTree, resultTree);
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<String> list = new ArrayList<String>();
+ final ArrayList<String> ignoreList = new ArrayList<String>();
+
+ list.add("./src/test/resources/prettyprint/OperationsTest/");
+ // ignoreList.add("./src/test/resources/testing/");
+ return getConfiguration2(list, ignoreList);
+ }
+}
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/CarTalkPuzzle.tla b/src/test/resources/MCTests/CarTalkPuzzle/CarTalkPuzzle.tla
new file mode 100644
index 0000000..38fed75
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/CarTalkPuzzle.tla
@@ -0,0 +1,158 @@
+---------------------------- MODULE CarTalkPuzzle ---------------------------
+(***************************************************************************)
+(* Car Talk is a U.S. radio program about car repair. Each show includes *)
+(* a puzzle, which is often a little mathematical problem. Usually, those *)
+(* problems are easy for a mathematically sophisticated listener to solve. *)
+(* However, I was not able immediately to see how to solve the puzzle from *)
+(* the 22 October 2011 program. I decided to specify the problem in TLA+ *)
+(* and let TLC (the TLA+ model checker) compute the solution. This is the *)
+(* specification I wrote. (I have tried to explain in comments all TLA+ *)
+(* notation that is not standard mathematical notation.) Once TLC had *)
+(* found the solution, it was not hard to understand why it worked. *)
+(* *)
+(* Here is the problem. A farmer has a 40 pound stone and a balance *)
+(* scale. How can he break the stone into 4 pieces so that, using those *)
+(* pieces and the balance scale, he can weigh out any integral number of *)
+(* pounds of corn from 1 pound through 40 pounds. *)
+(***************************************************************************)
+
+(***************************************************************************)
+(* The following statement imports the standard operators of arithmetic *)
+(* such as + and =< (less than or equals). It also defines the operator *)
+(* .. so that i..j is the set of all integers k with i =< k =< j. *)
+(***************************************************************************)
+EXTENDS Integers
+
+(***************************************************************************)
+(* For generality, I solve the problem of breaking an N pound stone into P *)
+(* pieces. The following statement declares N and P to be unspecified *)
+(* constant values. *)
+(***************************************************************************)
+CONSTANTS N, P
+
+(***************************************************************************)
+(* I define the operator Sum so that if f is any integer-valued function, *)
+(* and S any finite subset of its domain, then Sum(f, S) is the sum of *)
+(* f[x] for all x in S. (In TLA+, function application is indicated by *)
+(* square brackets instead of parentheses, as it is in ordinary math.) *)
+(* *)
+(* A RECURSIVE declaration must precede a recursively defined operator. *)
+(* The operator CHOOSE is known to logicians as Hilbert's Epsilon. It is *)
+(* defined so that CHOOSE x \in S : P(x) equals some unspecified value v *)
+(* such that P(v) is true, if such a value exists. *)
+(***************************************************************************)
+RECURSIVE Sum(_,_)
+Sum(f,S) == IF S = {} THEN 0
+ ELSE LET x == CHOOSE x \in S : TRUE
+ IN f[x] + Sum(f, S \ {x})
+
+(***************************************************************************)
+(* I now define the set Break of all "breaks", where a break represents a *)
+(* method of breaking the stone into P (integer-weight) pieces. The *)
+(* obvious definition of a break would be a set of weights. However, that *)
+(* doesn't work because it doesn't handle the situation in which two of *)
+(* pieces have the same weight. Instead, I define a break of the N pound *)
+(* stone into P pieces to be a function B from 1..P (the integers from 1 *)
+(* through P) into 1..N such that B[i] is the weight of piece number i. *)
+(* To avoid solutions that differ only by how the pieces are numbered, I *)
+(* consider only breaks in which the pieces are numbered in non-decreasing *)
+(* order of their weight. This leads to the following definition of the *)
+(* set Break of all breaks. *)
+(* *)
+(* In TLA+, [S -> T] is the set of all functions with domain S and range a *)
+(* subset of T. \A and \E are the universal and existential quantifiers. *)
+(***************************************************************************)
+Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
+ /\ \A i \in 1..P : \A j \in (i+1)..P : B[i] =< B[j]}
+
+(***************************************************************************)
+(* To weigh a quantity of corn, we can put some of the weights on the same *)
+(* side of the balance scale as the corn and other weights on the other *)
+(* side of the balance. The following operator is true for a weight w, a *)
+(* break B, and sets S and T of pieces if w plus the weight of the pieces *)
+(* in S equals the weight of the pieces in T. The elements of S and T are *)
+(* piece numbers (numbers in 1..P), so Sum(B, S) is the weight of the *)
+(* pieces in S. *)
+(***************************************************************************)
+IsRepresentation(w, B, S, T) == S \cap T = {}
+ /\ w + Sum(B,S) = Sum(B,T)
+(***************************************************************************)
+(* I now define IsSolution(B) to be true iff break B solves the problem, *)
+(* meaning that it can be used to balance any weight in 1..N. *)
+(* *)
+(* SUBSET S is the set of all subsets of S (the power set of S). *)
+(***************************************************************************)
+IsSolution(B) == \A w \in 1..N :
+ \E S, T \in SUBSET (1..P) : IsRepresentation(w, B, S, T)
+==========
+(***************************************************************************)
+(* I define AllSolutions to be the set of all breaks B that solve the *)
+(* problem. *)
+(***************************************************************************)
+AllSolutions == { B \in Break : IsSolution(B) }
+
+(***************************************************************************)
+(* We can now have TLC compute the solution to the problem as follows. We *)
+(* open this module in the TLA+ Toolbox (an Integrated Development *)
+(* Environment for the TLA+ tools). We then create a new TLC model in *)
+(* which we assign the values 40 to N and 4 to P. We specify in the model *)
+(* that TLC should compute the value of AllSolutions and run TLC on the *)
+(* model. After running for 22 seconds on my 3 year old 2.5 GHz laptop, *)
+(* it prints the result *)
+(* *)
+(* { <<1, 3, 9, 27>> } *)
+(* *)
+(* In TLA+, a k-tuple is represented as a function f with domain 1..k . *)
+(* Therefore, TLC prints a break B, which with P = 4 is a function with *)
+(* domain 1..4, as the tuple <<B[1], B[2], B[3], B[4]>>. Its output *)
+(* therefore indicates that there is a single break that solves the Car *)
+(* Talk puzzle, and it breaks the stone into pieces of weights 1, 3, 9, *)
+(* and 27 pounds. *)
+(* *)
+(* You have undoubtedly observed that the weights of the four pieces are *)
+(* 3^0, 3^1, 3^2, and 3^3. You may also have observed that 40 equals 1111 *)
+(* base 3. These facts should give you enough of a hint to be able to *)
+(* answer this: *)
+(* *)
+(* For what values of N and P is the problem solvable, and what *)
+(* is a solution for those values? *)
+(***************************************************************************)
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* It's a good idea to check that the definition of AllSolutions really *)
+(* generates solutions. The following operator defines ExpandSolutions to *)
+(* be a set of sequences, one for each solution in AllSolutions. Each of *)
+(* those sequences is of length N, where the element i shows how to weight *)
+(* i pounds of corn. For example, for the single solution with N = 40 and *)
+(* P = 4, element 7 of the sequence is *)
+(* *)
+(* <<7, {3}, {1, 9}>> *)
+(* *)
+(* indicating that to weight 7 pounds of corn, we can put the 3 pound *)
+(* weight on the same side of the balance as the corn and the 1 and 9 *)
+(* pound weights on the other side. For simplicity, I have made the *)
+(* definition work only only when the solution breaks the stone into *)
+(* pieces with unequal weights. As an exercise, modify the definition so *)
+(* it prints the elements using sequences instead of sets, as in *)
+(* *)
+(* << 7, <<3>>, <<1, 9>> >> *)
+(* *)
+(* so it works if the weights of the pieces are not all distinct. *)
+(* *)
+(* The definition below uses the following notation: *)
+(* *)
+(* \X is the Cartesian product of sets. *)
+(* *)
+(* [w \in 1..N |-> F(w)] is the N tuple with F(i) as element i. *)
+(* *)
+(***************************************************************************)
+ExpandSolutions ==
+ LET PiecesFor(w, B) == CHOOSE ST \in (SUBSET (1..P)) \X (SUBSET (1..P)) :
+ IsRepresentation(w, B, ST[1], ST[2])
+ Image(S, B) == {B[x] : x \in S}
+ SolutionFor(w, B) == << w,
+ Image(PiecesFor(w, B)[1], B),
+ Image(PiecesFor(w, B)[2], B) >>
+ IN { [w \in 1..N |-> SolutionFor(w, B)] : B \in AllSolutions }
+===============================================================================
+Created by Leslie Lamport on 26 October 2011
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/MC.cfg b/src/test/resources/MCTests/CarTalkPuzzle/MC.cfg
new file mode 100644
index 0000000..df9b1c4
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/MC.cfg
@@ -0,0 +1,7 @@
+\* CONSTANT definitions
+CONSTANT
+N <- const_131986752160123000
+\* CONSTANT definitions
+CONSTANT
+P <- const_131986752161624000
+\* Generated on Fri Oct 28 22:52:01 PDT 2011
\ No newline at end of file
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/MC.out b/src/test/resources/MCTests/CarTalkPuzzle/MC.out
new file mode 100644
index 0000000..17d5dd7
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/MC.out
@@ -0,0 +1,53 @@
+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.03 of 20 July 2011
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running in Model-Checking mode.
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file MC.tla
+Parsing file CarTalkPuzzle.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\TLC.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Integers.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Naturals.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Sequences.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module CarTalkPuzzle
+Semantic processing of module Sequences
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2011-10-28 22:52:02)
+@!@!@ENDMSG 2185 @!@!@
+<<"$!@$!@$!@$!@$!", <<242, 121>>>>
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 0 distinct states generated.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+ Estimates of the probability that TLC did not check all reachable states
+ because two distinct states had the same fingerprint:
+ calculated (optimistic): val = 0
+ based on the actual fingerprints: val = 1.1E-19
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(0) at 2011-10-28 22:52:02: 0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 0.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished. (2011-10-28 22:52:02)
+@!@!@ENDMSG 2186 @!@!@
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/MC.tla b/src/test/resources/MCTests/CarTalkPuzzle/MC.tla
new file mode 100644
index 0000000..5aa206b
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/MC.tla
@@ -0,0 +1,27 @@
+---- MODULE MC ----
+EXTENDS CarTalkPuzzle, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_131986752160123000 ==
+40
+----
+
+\* CONSTANT definitions @modelParameterConstants:1P
+const_131986752161624000 ==
+4
+----
+
+\* Constant expression definition @modelExpressionEval
+const_expr_131986752163225000 ==
+\* ExpandSolutions
+\* CHOOSE B \in Break : IsSolution(B)
+<<3^5 - 1, 40 + 3^4>>
+----
+
+\* Constant expression ASSUME statement @modelExpressionEval
+ASSUME PrintT(<<"$!@$!@$!@$!@$!",const_expr_131986752163225000>>)
+----
+
+=============================================================================
+\* Modification History
+\* Created Fri Oct 28 22:52:01 PDT 2011 by lamport
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/MC_TE.out b/src/test/resources/MCTests/CarTalkPuzzle/MC_TE.out
new file mode 100644
index 0000000..17d5dd7
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/MC_TE.out
@@ -0,0 +1,53 @@
+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.03 of 20 July 2011
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running in Model-Checking mode.
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file MC.tla
+Parsing file CarTalkPuzzle.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\TLC.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Integers.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Naturals.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Sequences.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module CarTalkPuzzle
+Semantic processing of module Sequences
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2011-10-28 22:52:02)
+@!@!@ENDMSG 2185 @!@!@
+<<"$!@$!@$!@$!@$!", <<242, 121>>>>
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 0 distinct states generated.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+ Estimates of the probability that TLC did not check all reachable states
+ because two distinct states had the same fingerprint:
+ calculated (optimistic): val = 0
+ based on the actual fingerprints: val = 1.1E-19
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(0) at 2011-10-28 22:52:02: 0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 0.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished. (2011-10-28 22:52:02)
+@!@!@ENDMSG 2186 @!@!@
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/Model2/CarTalkPuzzle.tla b/src/test/resources/MCTests/CarTalkPuzzle/Model2/CarTalkPuzzle.tla
new file mode 100644
index 0000000..1ef24e4
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/Model2/CarTalkPuzzle.tla
@@ -0,0 +1,158 @@
+---------------------------- MODULE CarTalkPuzzle ---------------------------
+(***************************************************************************)
+(* Car Talk is a U.S. radio program about car repair. Each show includes *)
+(* a puzzle, which is often a little mathematical problem. Usually, those *)
+(* problems are easy for a mathematically sophisticated listener to solve. *)
+(* However, I was not able immediately to see how to solve the puzzle from *)
+(* the 22 October 2011 program. I decided to specify the problem in TLA+ *)
+(* and let TLC (the TLA+ model checker) compute the solution. This is the *)
+(* specification I wrote. (I have tried to explain in comments all TLA+ *)
+(* notation that is not standard mathematical notation.) Once TLC had *)
+(* found the solution, it was not hard to understand why it worked. *)
+(* *)
+(* Here is the problem. A farmer has a 40 pound stone and a balance *)
+(* scale. How can he break the stone into 4 pieces so that, using those *)
+(* pieces and the balance scale, he can weigh out any integral number of *)
+(* pounds of corn from 1 pound through 40 pounds. *)
+(***************************************************************************)
+
+(***************************************************************************)
+(* The following statement imports the standard operators of arithmetic *)
+(* such as + and =< (less than or equals). It also defines the operator *)
+(* .. so that i..j is the set of all integers k with i =< k =< j. *)
+(***************************************************************************)
+EXTENDS Integers
+
+(***************************************************************************)
+(* For generality, I solve the problem of breaking an N pound stone into P *)
+(* pieces. The following statement declares N and P to be unspecified *)
+(* constant values. *)
+(***************************************************************************)
+CONSTANTS N, P
+
+(***************************************************************************)
+(* I define the operator Sum so that if f is any integer-valued function, *)
+(* and S any finite subset of its domain, then Sum(f, S) is the sum of *)
+(* f[x] for all x in S. (In TLA+, function application is indicated by *)
+(* square brackets instead of parentheses, as it is in ordinary math.) *)
+(* *)
+(* A RECURSIVE declaration must precede a recursively defined operator. *)
+(* The operator CHOOSE is known to logicians as Hilbert's Epsilon. It is *)
+(* defined so that CHOOSE x \in S : P(x) equals some unspecified value v *)
+(* such that P(v) is true, if such a value exists. *)
+(***************************************************************************)
+RECURSIVE Sum(_,_)
+Sum(f,S) == IF S = {} THEN 0
+ ELSE LET x == CHOOSE x \in S : TRUE
+ IN f[x] + Sum(f, S \ {x})
+
+(***************************************************************************)
+(* I now define the set Break of all "breaks", where a break represents a *)
+(* method of breaking the stone into P (integer-weight) pieces. The *)
+(* obvious definition of a break would be a set of weights. However, that *)
+(* doesn't work because it doesn't handle the situation in which two of *)
+(* pieces have the same weight. Instead, I define a break of the N pound *)
+(* stone into P pieces to be a function B from 1..P (the integers from 1 *)
+(* through P) into 1..N such that B[i] is the weight of piece number i. *)
+(* To avoid solutions that differ only by how the pieces are numbered, I *)
+(* consider only breaks in which the pieces are numbered in non-decreasing *)
+(* order of their weight. This leads to the following definition of the *)
+(* set Break of all breaks. *)
+(* *)
+(* In TLA+, [S -> T] is the set of all functions with domain S and range a *)
+(* subset of T. \A and \E are the universal and existential quantifiers. *)
+(***************************************************************************)
+Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
+ /\ \A i \in 1..P : \A j \in (i+1)..P : B[i] =< B[j]}
+
+(***************************************************************************)
+(* To weigh a quantity of corn, we can put some of the weights on the same *)
+(* side of the balance scale as the corn and other weights on the other *)
+(* side of the balance. The following operator is true for a weight w, a *)
+(* break B, and sets S and T of pieces if w plus the weight of the pieces *)
+(* in S equals the weight of the pieces in T. The elements of S and T are *)
+(* piece numbers (numbers in 1..P), so Sum(B, S) is the weight of the *)
+(* pieces in S. *)
+(***************************************************************************)
+IsRepresentation(w, B, S, T) == S \cap T = {}
+ /\ w + Sum(B,S) = Sum(B,T)
+(***************************************************************************)
+(* I now define IsSolution(B) to be true iff break B solves the problem, *)
+(* meaning that it can be used to balance any weight in 1..N. *)
+(* *)
+(* SUBSET S is the set of all subsets of S (the power set of S). *)
+(***************************************************************************)
+IsSolution(B) == \A w \in 1..N :
+ \E S, T \in SUBSET (1..P) : IsRepresentation(w, B, S, T)
+
+(***************************************************************************)
+(* I define AllSolutions to be the set of all breaks B that solve the *)
+(* problem. *)
+(***************************************************************************)
+AllSolutions == { B \in Break : IsSolution(B) }
+
+(***************************************************************************)
+(* We can now have TLC compute the solution to the problem as follows. We *)
+(* open this module in the TLA+ Toolbox (an Integrated Development *)
+(* Environment for the TLA+ tools). We then create a new TLC model in *)
+(* which we assign the values 40 to N and 4 to P. We specify in the model *)
+(* that TLC should compute the value of AllSolutions and run TLC on the *)
+(* model. After running for 22 seconds on my 3 year old 2.5 GHz laptop, *)
+(* it prints the result *)
+(* *)
+(* { <<1, 3, 9, 27>> } *)
+(* *)
+(* In TLA+, a k-tuple is represented as a function f with domain 1..k . *)
+(* Therefore, TLC prints a break B, which with P = 4 is a function with *)
+(* domain 1..4, as the tuple <<B[1], B[2], B[3], B[4]>>. Its output *)
+(* therefore indicates that there is a single break that solves the Car *)
+(* Talk puzzle, and it breaks the stone into pieces of weights 1, 3, 9, *)
+(* and 27 pounds. *)
+(* *)
+(* You have undoubtedly observed that the weights of the four pieces are *)
+(* 3^0, 3^1, 3^2, and 3^3. You may also have observed that 40 equals 1111 *)
+(* base 3. These facts should give you enough of a hint to be able to *)
+(* answer this: *)
+(* *)
+(* For what values of N and P is the problem solvable, and what *)
+(* is a solution for those values? *)
+(***************************************************************************)
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* It's a good idea to check that the definition of AllSolutions really *)
+(* generates solutions. The following operator defines ExpandSolutions to *)
+(* be a set of sequences, one for each solution in AllSolutions. Each of *)
+(* those sequences is of length N, where the element i shows how to weight *)
+(* i pounds of corn. For example, for the single solution with N = 40 and *)
+(* P = 4, element 7 of the sequence is *)
+(* *)
+(* <<7, {3}, {1, 9}>> *)
+(* *)
+(* indicating that to weight 7 pounds of corn, we can put the 3 pound *)
+(* weight on the same side of the balance as the corn and the 1 and 9 *)
+(* pound weights on the other side. For simplicity, I have made the *)
+(* definition work only only when the solution breaks the stone into *)
+(* pieces with unequal weights. As an exercise, modify the definition so *)
+(* it prints the elements using sequences instead of sets, as in *)
+(* *)
+(* << 7, <<3>>, <<1, 9>> >> *)
+(* *)
+(* so it works if the weights of the pieces are not all distinct. *)
+(* *)
+(* The definition below uses the following notation: *)
+(* *)
+(* \X is the Cartesian product of sets. *)
+(* *)
+(* [w \in 1..N |-> F(w)] is the N tuple with F(i) as element i. *)
+(* *)
+(***************************************************************************)
+ExpandSolutions ==
+ LET PiecesFor(w, B) == CHOOSE ST \in (SUBSET (1..P)) \X (SUBSET (1..P)) :
+ IsRepresentation(w, B, ST[1], ST[2])
+ Image(S, B) == {B[x] : x \in S}
+ SolutionFor(w, B) == << w,
+ Image(PiecesFor(w, B)[1], B),
+ Image(PiecesFor(w, B)[2], B) >>
+ IN { [w \in 1..N |-> SolutionFor(w, B)] : B \in AllSolutions }
+===============================================================================
+Created by Leslie Lamport on 26 October 2011
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.cfg b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.cfg
new file mode 100644
index 0000000..5bb0e31
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.cfg
@@ -0,0 +1,7 @@
+\* CONSTANT definitions
+CONSTANT
+N <- const_131965207585635000
+\* CONSTANT definitions
+CONSTANT
+P <- const_131965207587136000
+\* Generated on Wed Oct 26 11:01:15 PDT 2011
\ No newline at end of file
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.out b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.out
new file mode 100644
index 0000000..40ef268
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.out
@@ -0,0 +1,64 @@
+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.03 of 20 July 2011
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running in Model-Checking mode.
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file MC.tla
+Parsing file CarTalkPuzzle.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\TLC.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Integers.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Naturals.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Sequences.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module CarTalkPuzzle
+Semantic processing of module Sequences
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2011-10-26 11:01:16)
+@!@!@ENDMSG 2185 @!@!@
+<< "$!@$!@$!@$!@$!",
+ { <<1, 1, 3, 10>>,
+ <<1, 1, 4, 9>>,
+ <<1, 1, 5, 8>>,
+ <<1, 2, 2, 10>>,
+ <<1, 2, 3, 9>>,
+ <<1, 2, 4, 8>>,
+ <<1, 2, 5, 7>>,
+ <<1, 2, 6, 6>>,
+ <<1, 3, 3, 8>>,
+ <<1, 3, 4, 7>>,
+ <<1, 3, 5, 6>> } >>
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 0 distinct states generated.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+ Estimates of the probability that TLC did not check all reachable states
+ because two distinct states had the same fingerprint:
+ calculated (optimistic): val = 0
+ based on the actual fingerprints: val = 1.1E-19
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(0) at 2011-10-26 11:01:18: 0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 0.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished. (2011-10-26 11:01:18)
+@!@!@ENDMSG 2186 @!@!@
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.tla b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.tla
new file mode 100644
index 0000000..f1e49a1
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.tla
@@ -0,0 +1,25 @@
+---- MODULE MC ----
+EXTENDS CarTalkPuzzle, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_131965207585635000 ==
+15
+----
+
+\* CONSTANT definitions @modelParameterConstants:1P
+const_131965207587136000 ==
+4
+----
+
+\* Constant expression definition @modelExpressionEval
+const_expr_131965207588737000 ==
+AllSolutions
+----
+
+\* Constant expression ASSUME statement @modelExpressionEval
+ASSUME PrintT(<<"$!@$!@$!@$!@$!",const_expr_131965207588737000>>)
+----
+
+=============================================================================
+\* Modification History
+\* Created Wed Oct 26 11:01:15 PDT 2011 by lamport
diff --git a/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC_TE.out b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC_TE.out
new file mode 100644
index 0000000..40ef268
--- /dev/null
+++ b/src/test/resources/MCTests/CarTalkPuzzle/Model2/MC_TE.out
@@ -0,0 +1,64 @@
+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.03 of 20 July 2011
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running in Model-Checking mode.
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file MC.tla
+Parsing file CarTalkPuzzle.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\TLC.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Integers.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Naturals.tla
+Parsing file C:\lamport\tla\newtools\tla2-inria-workspace\tla2-inria\tlatools\class\tla2sany\StandardModules\Sequences.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module CarTalkPuzzle
+Semantic processing of module Sequences
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2011-10-26 11:01:16)
+@!@!@ENDMSG 2185 @!@!@
+<< "$!@$!@$!@$!@$!",
+ { <<1, 1, 3, 10>>,
+ <<1, 1, 4, 9>>,
+ <<1, 1, 5, 8>>,
+ <<1, 2, 2, 10>>,
+ <<1, 2, 3, 9>>,
+ <<1, 2, 4, 8>>,
+ <<1, 2, 5, 7>>,
+ <<1, 2, 6, 6>>,
+ <<1, 3, 3, 8>>,
+ <<1, 3, 4, 7>>,
+ <<1, 3, 5, 6>> } >>
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 0 distinct states generated.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+ Estimates of the probability that TLC did not check all reachable states
+ because two distinct states had the same fingerprint:
+ calculated (optimistic): val = 0
+ based on the actual fingerprints: val = 1.1E-19
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(0) at 2011-10-26 11:01:18: 0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+0 states generated, 0 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 0.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished. (2011-10-26 11:01:18)
+@!@!@ENDMSG 2186 @!@!@
diff --git a/src/test/resources/MCTests/Invariant/Invariant.tla b/src/test/resources/MCTests/Invariant/Invariant.tla
new file mode 100644
index 0000000..dc36ab7
--- /dev/null
+++ b/src/test/resources/MCTests/Invariant/Invariant.tla
@@ -0,0 +1,11 @@
+----------------------------- MODULE Invariant -----------------------------
+EXTENDS Naturals
+VARIABLES x
+Init == x = 1
+Next == x' = 2
+Inv == x \in 1..3
+
+=============================================================================
+\* Modification History
+\* Last modified Fri May 09 12:27:40 CEST 2014 by hansen
+\* Created Fri May 09 12:26:48 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/Invariant/MC.cfg b/src/test/resources/MCTests/Invariant/MC.cfg
new file mode 100644
index 0000000..4ffafa6
--- /dev/null
+++ b/src/test/resources/MCTests/Invariant/MC.cfg
@@ -0,0 +1,10 @@
+\* INIT definition
+INIT
+init_13996312783457000
+\* NEXT definition
+NEXT
+next_13996312783578000
+\* INVARIANT definition
+INVARIANT
+inv_13996312783689000
+\* Generated on Fri May 09 12:27:58 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/Invariant/MC.tla b/src/test/resources/MCTests/Invariant/MC.tla
new file mode 100644
index 0000000..7c32471
--- /dev/null
+++ b/src/test/resources/MCTests/Invariant/MC.tla
@@ -0,0 +1,18 @@
+---- MODULE MC ----
+EXTENDS Invariant, TLC
+
+\* INIT definition @modelBehaviorInit:0
+init_13996312783457000 ==
+Init
+----
+\* NEXT definition @modelBehaviorNext:0
+next_13996312783578000 ==
+Next
+----
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_13996312783689000 ==
+Inv
+----
+=============================================================================
+\* Modification History
+\* Created Fri May 09 12:27:58 CEST 2014 by hansen
diff --git a/src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunction1.tla b/src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunction1.tla
new file mode 100644
index 0000000..80d00b4
--- /dev/null
+++ b/src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunction1.tla
@@ -0,0 +1,5 @@
+-------------- MODULE RecursiveFunction1 ----------------
+EXTENDS Integers, FiniteSets
+foo(a) == LET Sum[x \in Nat] == IF x = 0 THEN a ELSE x + Sum[x-1] IN Sum[3]
+ASSUME 11 = foo(5)
+=================================
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunctionGlobalVariable.tla b/src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunctionGlobalVariable.tla
new file mode 100644
index 0000000..c7e55e8
--- /dev/null
+++ b/src/test/resources/prettyprint/RecursiveFunctions/RecursiveFunctionGlobalVariable.tla
@@ -0,0 +1,7 @@
+-------------- MODULE RecursiveFunctionGlobalVariable ----------------
+EXTENDS Integers, FiniteSets
+VARIABLES x
+Sum[a \in Nat] == IF a = 0 THEN x ELSE a + Sum[a-1]
+Init == x = 1
+Next == x'= Sum[x]
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/AsynchInterface/AsynchInterface.cfg b/src/test/resources/regression/AsynchInterface/AsynchInterface.cfg
similarity index 100%
rename from src/test/resources/examples/AsynchInterface/AsynchInterface.cfg
rename to src/test/resources/regression/AsynchInterface/AsynchInterface.cfg
diff --git a/src/test/resources/examples/AsynchInterface/AsynchInterface.mch b/src/test/resources/regression/AsynchInterface/AsynchInterface.mch
similarity index 100%
rename from src/test/resources/examples/AsynchInterface/AsynchInterface.mch
rename to src/test/resources/regression/AsynchInterface/AsynchInterface.mch
diff --git a/src/test/resources/examples/AsynchInterface/AsynchInterface.tla b/src/test/resources/regression/AsynchInterface/AsynchInterface.tla
similarity index 100%
rename from src/test/resources/examples/AsynchInterface/AsynchInterface.tla
rename to src/test/resources/regression/AsynchInterface/AsynchInterface.tla
diff --git a/src/test/resources/examples/Channel/Channel.cfg b/src/test/resources/regression/Channel/Channel.cfg
similarity index 100%
rename from src/test/resources/examples/Channel/Channel.cfg
rename to src/test/resources/regression/Channel/Channel.cfg
diff --git a/src/test/resources/examples/Channel/Channel.mch b/src/test/resources/regression/Channel/Channel.mch
similarity index 100%
rename from src/test/resources/examples/Channel/Channel.mch
rename to src/test/resources/regression/Channel/Channel.mch
diff --git a/src/test/resources/examples/Channel/Channel.tla b/src/test/resources/regression/Channel/Channel.tla
similarity index 100%
rename from src/test/resources/examples/Channel/Channel.tla
rename to src/test/resources/regression/Channel/Channel.tla
diff --git a/src/test/resources/examples/Club/Club.cfg b/src/test/resources/regression/Club/Club.cfg
similarity index 100%
rename from src/test/resources/examples/Club/Club.cfg
rename to src/test/resources/regression/Club/Club.cfg
diff --git a/src/test/resources/examples/Club/Club.mch b/src/test/resources/regression/Club/Club.mch
similarity index 100%
rename from src/test/resources/examples/Club/Club.mch
rename to src/test/resources/regression/Club/Club.mch
diff --git a/src/test/resources/examples/Club/Club.tla b/src/test/resources/regression/Club/Club.tla
similarity index 100%
rename from src/test/resources/examples/Club/Club.tla
rename to src/test/resources/regression/Club/Club.tla
diff --git a/src/test/resources/regression/Club/Club_tla.mch b/src/test/resources/regression/Club/Club_tla.mch
new file mode 100644
index 0000000..91c6f69
--- /dev/null
+++ b/src/test/resources/regression/Club/Club_tla.mch
@@ -0,0 +1,18 @@
+/*@ generated by TLA2B 1.0.7 Fri May 09 12:45:00 CEST 2014 */
+MACHINE Club
+SETS ENUM1 = {n1, n2, n3}
+ABSTRACT_CONSTANTS capacity, NAME, total
+PROPERTIES
+((((capacity : INTEGER & NAME = ENUM1) & total : INTEGER) & (capacity : NATURAL & capacity = 2)) & card(NAME) > capacity) & (total : NATURAL & total > 2)
+VARIABLES member, waiting
+INVARIANT
+member : POW(ENUM1) & waiting : POW(ENUM1)
+INITIALISATION
+member, waiting:(member = {} & waiting = {})
+OPERATIONS
+ join_queue(nn) = ANY member_n WHERE ((((nn : NAME & nn /: member) & nn /: waiting) & member_n : POW(ENUM1)) & card(waiting) < total) & member_n = member THEN waiting,member := waiting \/ {nn},member_n END;
+
+ join(nn) = SELECT ((nn : NAME & nn : waiting) & card(member) < capacity) & card(member) < capacity THEN member,waiting := member \/ {nn},waiting - {nn} END;
+
+ remove(nn) = ANY waiting_n WHERE ((nn : NAME & nn : member) & waiting_n : POW(ENUM1)) & waiting_n = waiting THEN member,waiting := member - {nn},waiting_n END
+END
\ No newline at end of file
diff --git a/src/test/resources/examples/Counter/Counter.cfg b/src/test/resources/regression/Counter/Counter.cfg
similarity index 100%
rename from src/test/resources/examples/Counter/Counter.cfg
rename to src/test/resources/regression/Counter/Counter.cfg
diff --git a/src/test/resources/examples/Counter/Counter.mch b/src/test/resources/regression/Counter/Counter.mch
similarity index 100%
rename from src/test/resources/examples/Counter/Counter.mch
rename to src/test/resources/regression/Counter/Counter.mch
diff --git a/src/test/resources/examples/Counter/Counter.tla b/src/test/resources/regression/Counter/Counter.tla
similarity index 100%
rename from src/test/resources/examples/Counter/Counter.tla
rename to src/test/resources/regression/Counter/Counter.tla
diff --git a/src/test/resources/examples/DefCapture/DefCapture.mch b/src/test/resources/regression/DefCapture/DefCapture.mch
similarity index 100%
rename from src/test/resources/examples/DefCapture/DefCapture.mch
rename to src/test/resources/regression/DefCapture/DefCapture.mch
diff --git a/src/test/resources/examples/DefCapture/DefCapture.tla b/src/test/resources/regression/DefCapture/DefCapture.tla
similarity index 100%
rename from src/test/resources/examples/DefCapture/DefCapture.tla
rename to src/test/resources/regression/DefCapture/DefCapture.tla
diff --git a/src/test/resources/examples/DieHard/DieHard.cfg b/src/test/resources/regression/DieHard/DieHard.cfg
similarity index 100%
rename from src/test/resources/examples/DieHard/DieHard.cfg
rename to src/test/resources/regression/DieHard/DieHard.cfg
diff --git a/src/test/resources/examples/DieHard/DieHard.mch b/src/test/resources/regression/DieHard/DieHard.mch
similarity index 100%
rename from src/test/resources/examples/DieHard/DieHard.mch
rename to src/test/resources/regression/DieHard/DieHard.mch
diff --git a/src/test/resources/examples/DieHard/DieHard.tla b/src/test/resources/regression/DieHard/DieHard.tla
similarity index 100%
rename from src/test/resources/examples/DieHard/DieHard.tla
rename to src/test/resources/regression/DieHard/DieHard.tla
diff --git a/src/test/resources/examples/DieHard/DieHarder.cfg b/src/test/resources/regression/DieHard/DieHarder.cfg
similarity index 100%
rename from src/test/resources/examples/DieHard/DieHarder.cfg
rename to src/test/resources/regression/DieHard/DieHarder.cfg
diff --git a/src/test/resources/examples/DieHard/DieHarder.mch b/src/test/resources/regression/DieHard/DieHarder.mch
similarity index 100%
rename from src/test/resources/examples/DieHard/DieHarder.mch
rename to src/test/resources/regression/DieHard/DieHarder.mch
diff --git a/src/test/resources/examples/DieHard/DieHarder.tla b/src/test/resources/regression/DieHard/DieHarder.tla
similarity index 100%
rename from src/test/resources/examples/DieHard/DieHarder.tla
rename to src/test/resources/regression/DieHard/DieHarder.tla
diff --git a/src/test/resources/examples/Doors/Doors.cfg b/src/test/resources/regression/Doors/Doors.cfg
similarity index 100%
rename from src/test/resources/examples/Doors/Doors.cfg
rename to src/test/resources/regression/Doors/Doors.cfg
diff --git a/src/test/resources/examples/Doors/Doors.mch b/src/test/resources/regression/Doors/Doors.mch
similarity index 100%
rename from src/test/resources/examples/Doors/Doors.mch
rename to src/test/resources/regression/Doors/Doors.mch
diff --git a/src/test/resources/examples/Doors/Doors.tla b/src/test/resources/regression/Doors/Doors.tla
similarity index 100%
rename from src/test/resources/examples/Doors/Doors.tla
rename to src/test/resources/regression/Doors/Doors.tla
diff --git a/src/test/resources/examples/GraphIso/GraphIso.cfg b/src/test/resources/regression/GraphIso/GraphIso.cfg
similarity index 100%
rename from src/test/resources/examples/GraphIso/GraphIso.cfg
rename to src/test/resources/regression/GraphIso/GraphIso.cfg
diff --git a/src/test/resources/examples/GraphIso/GraphIso.mch b/src/test/resources/regression/GraphIso/GraphIso.mch
similarity index 100%
rename from src/test/resources/examples/GraphIso/GraphIso.mch
rename to src/test/resources/regression/GraphIso/GraphIso.mch
diff --git a/src/test/resources/examples/GraphIso/GraphIso.tla b/src/test/resources/regression/GraphIso/GraphIso.tla
similarity index 100%
rename from src/test/resources/examples/GraphIso/GraphIso.tla
rename to src/test/resources/regression/GraphIso/GraphIso.tla
diff --git a/src/test/resources/examples/HourClock/HourClock.cfg b/src/test/resources/regression/HourClock/HourClock.cfg
similarity index 100%
rename from src/test/resources/examples/HourClock/HourClock.cfg
rename to src/test/resources/regression/HourClock/HourClock.cfg
diff --git a/src/test/resources/examples/HourClock/HourClock.mch b/src/test/resources/regression/HourClock/HourClock.mch
similarity index 100%
rename from src/test/resources/examples/HourClock/HourClock.mch
rename to src/test/resources/regression/HourClock/HourClock.mch
diff --git a/src/test/resources/examples/HourClock/HourClock.tla b/src/test/resources/regression/HourClock/HourClock.tla
similarity index 100%
rename from src/test/resources/examples/HourClock/HourClock.tla
rename to src/test/resources/regression/HourClock/HourClock.tla
diff --git a/src/test/resources/examples/Jukebox/Jukebox.cfg b/src/test/resources/regression/Jukebox/Jukebox.cfg
similarity index 100%
rename from src/test/resources/examples/Jukebox/Jukebox.cfg
rename to src/test/resources/regression/Jukebox/Jukebox.cfg
diff --git a/src/test/resources/examples/Jukebox/Jukebox.mch b/src/test/resources/regression/Jukebox/Jukebox.mch
similarity index 100%
rename from src/test/resources/examples/Jukebox/Jukebox.mch
rename to src/test/resources/regression/Jukebox/Jukebox.mch
diff --git a/src/test/resources/examples/Jukebox/Jukebox.tla b/src/test/resources/regression/Jukebox/Jukebox.tla
similarity index 100%
rename from src/test/resources/examples/Jukebox/Jukebox.tla
rename to src/test/resources/regression/Jukebox/Jukebox.tla
diff --git a/src/test/resources/regression/MySequence/MySequence.cfg b/src/test/resources/regression/MySequence/MySequence.cfg
new file mode 100644
index 0000000..81bbfad
--- /dev/null
+++ b/src/test/resources/regression/MySequence/MySequence.cfg
@@ -0,0 +1 @@
+SPECIFICATION Spec
\ No newline at end of file
diff --git a/src/test/resources/examples/MySequence/MySequence.tla b/src/test/resources/regression/MySequence/MySequence.tla
similarity index 100%
rename from src/test/resources/examples/MySequence/MySequence.tla
rename to src/test/resources/regression/MySequence/MySequence.tla
diff --git a/src/test/resources/examples/Queens/Queens.cfg b/src/test/resources/regression/Queens/Queens.cfg
similarity index 100%
rename from src/test/resources/examples/Queens/Queens.cfg
rename to src/test/resources/regression/Queens/Queens.cfg
diff --git a/src/test/resources/examples/Queens/Queens.mch b/src/test/resources/regression/Queens/Queens.mch
similarity index 100%
rename from src/test/resources/examples/Queens/Queens.mch
rename to src/test/resources/regression/Queens/Queens.mch
diff --git a/src/test/resources/examples/Queens/Queens.tla b/src/test/resources/regression/Queens/Queens.tla
similarity index 100%
rename from src/test/resources/examples/Queens/Queens.tla
rename to src/test/resources/regression/Queens/Queens.tla
diff --git a/src/test/resources/examples/Queens/Queens2.cfg b/src/test/resources/regression/Queens/Queens2.cfg
similarity index 100%
rename from src/test/resources/examples/Queens/Queens2.cfg
rename to src/test/resources/regression/Queens/Queens2.cfg
diff --git a/src/test/resources/examples/Queens/Queens2.mch b/src/test/resources/regression/Queens/Queens2.mch
similarity index 100%
rename from src/test/resources/examples/Queens/Queens2.mch
rename to src/test/resources/regression/Queens/Queens2.mch
diff --git a/src/test/resources/examples/Queens/Queens2.tla b/src/test/resources/regression/Queens/Queens2.tla
similarity index 100%
rename from src/test/resources/examples/Queens/Queens2.tla
rename to src/test/resources/regression/Queens/Queens2.tla
diff --git a/src/test/resources/examples/RecursiveFunction/RecursiveFunction.mch b/src/test/resources/regression/RecursiveFunction/RecursiveFunction.mch
similarity index 100%
rename from src/test/resources/examples/RecursiveFunction/RecursiveFunction.mch
rename to src/test/resources/regression/RecursiveFunction/RecursiveFunction.mch
diff --git a/src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla b/src/test/resources/regression/RecursiveFunction/RecursiveFunction.tla
similarity index 100%
rename from src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla
rename to src/test/resources/regression/RecursiveFunction/RecursiveFunction.tla
diff --git a/src/test/resources/examples/Scheduler/Scheduler.cfg b/src/test/resources/regression/Scheduler/Scheduler.cfg
similarity index 100%
rename from src/test/resources/examples/Scheduler/Scheduler.cfg
rename to src/test/resources/regression/Scheduler/Scheduler.cfg
diff --git a/src/test/resources/examples/Scheduler/Scheduler.mch b/src/test/resources/regression/Scheduler/Scheduler.mch
similarity index 100%
rename from src/test/resources/examples/Scheduler/Scheduler.mch
rename to src/test/resources/regression/Scheduler/Scheduler.mch
diff --git a/src/test/resources/examples/Scheduler/Scheduler.tla b/src/test/resources/regression/Scheduler/Scheduler.tla
similarity index 100%
rename from src/test/resources/examples/Scheduler/Scheduler.tla
rename to src/test/resources/regression/Scheduler/Scheduler.tla
diff --git a/src/test/resources/examples/SimpleSATProblem/SimpleSATProblem.mch b/src/test/resources/regression/SimpleSATProblem/SimpleSATProblem.mch
similarity index 100%
rename from src/test/resources/examples/SimpleSATProblem/SimpleSATProblem.mch
rename to src/test/resources/regression/SimpleSATProblem/SimpleSATProblem.mch
diff --git a/src/test/resources/examples/SimpleSATProblem/SimpleSATProblem.tla b/src/test/resources/regression/SimpleSATProblem/SimpleSATProblem.tla
similarity index 100%
rename from src/test/resources/examples/SimpleSATProblem/SimpleSATProblem.tla
rename to src/test/resources/regression/SimpleSATProblem/SimpleSATProblem.tla
diff --git a/src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla b/src/test/resources/regression/SumAndProduct/SumAndProductConstraint.tla
similarity index 100%
rename from src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla
rename to src/test/resources/regression/SumAndProduct/SumAndProductConstraint.tla
diff --git a/src/test/resources/examples/SumAndProduct/SumAndProductTransition.tla b/src/test/resources/regression/SumAndProduct/SumAndProductTransition.tla
similarity index 100%
rename from src/test/resources/examples/SumAndProduct/SumAndProductTransition.tla
rename to src/test/resources/regression/SumAndProduct/SumAndProductTransition.tla
diff --git a/src/test/resources/examples/uf50_02/uf50_02.tla b/src/test/resources/regression/uf50_02/uf50_02.tla
similarity index 100%
rename from src/test/resources/examples/uf50_02/uf50_02.tla
rename to src/test/resources/regression/uf50_02/uf50_02.tla
--
GitLab