From 41b4f1f594530a809171b22d850f989b51a36696 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 16 May 2014 16:39:45 +0200
Subject: [PATCH] added missing files
---
.../java/de/tla2b/types/TupleOrFunction.java | 207 ++++++++++++++++++
.../java/de/tla2b/examples/InstanceTest.java | 23 ++
.../examples/instance/Counter/Counter.tla | 9 +
.../instance/Counter/InstanceDefinition.mch | 13 ++
.../instance/Counter/InstanceDefinition.tla | 5 +
.../instance/Counter/InstanceNoName.mch | 18 ++
.../instance/Counter/InstanceNoName.tla | 6 +
.../Counter/ModConstantAssignment.cfg | 3 +
.../Counter/ModConstantAssignment.mch | 13 ++
.../Counter/ModConstantAssignment.tla | 4 +
.../instance/Counter/OneInstanced.mch | 19 ++
.../instance/Counter/OneInstanced.tla | 8 +
.../examples/instance/Counter/TwoInstance.mch | 32 +++
.../examples/instance/Counter/TwoInstance.tla | 9 +
.../instance/Counter/TwoInstanced.mch | 32 +++
.../instance/Counter/TwoInstanced.tla | 9 +
.../examples/instance/OpArg/OpArg.tla | 7 +
.../instance/OpArg/OpArgInstanced.mch | 14 ++
.../instance/OpArg/OpArgInstanced.tla | 6 +
.../instance/configOverride/Counter.tla | 9 +
.../configOverride/InstanceCounter.cfg | 4 +
.../configOverride/InstanceCounter.mch | 16 ++
.../configOverride/InstanceCounter.tla | 5 +
.../InstanceCounterException.cfg | 4 +
.../InstanceCounterException.tla | 6 +
.../InstanceInstanceOpArg.cfg | 1 +
.../InstanceInstanceOpArg.tla | 7 +
.../constantSubstitution/InstanceOpArg.tla | 5 +
.../constantSubstitution/InstanceOpArg2.tla | 7 +
.../constantSubstitution/InstanceOpArg3.cfg | 1 +
.../constantSubstitution/InstanceOpArg3.tla | 7 +
.../InstanceOpArgException.tla | 6 +
.../constantSubstitution/InstanceValue.tla | 6 +
.../constantSubstitution/InstanceValue2.tla | 6 +
.../instance/constantSubstitution/OpArg.tla | 5 +
.../instance/constantSubstitution/Value.tla | 6 +
.../examples/instance/let/InstanceLet.mch | 26 +++
.../examples/instance/let/InstanceLet.tla | 7 +
.../resources/examples/instance/let/Let.tla | 14 ++
.../examples/instance/twoInstanced/first.tla | 5 +
.../examples/instance/twoInstanced/second.tla | 6 +
.../prettyprint/backtranslation/TlaTypes.cfg | 2 +
.../prettyprint/backtranslation/TlaTypes.tla | 20 ++
src/test/resources/regression/Club/Club.prob | 3 +
44 files changed, 621 insertions(+)
create mode 100644 src/main/java/de/tla2b/types/TupleOrFunction.java
create mode 100644 src/test/java/de/tla2b/examples/InstanceTest.java
create mode 100644 src/test/resources/examples/instance/Counter/Counter.tla
create mode 100644 src/test/resources/examples/instance/Counter/InstanceDefinition.mch
create mode 100644 src/test/resources/examples/instance/Counter/InstanceDefinition.tla
create mode 100644 src/test/resources/examples/instance/Counter/InstanceNoName.mch
create mode 100644 src/test/resources/examples/instance/Counter/InstanceNoName.tla
create mode 100644 src/test/resources/examples/instance/Counter/ModConstantAssignment.cfg
create mode 100644 src/test/resources/examples/instance/Counter/ModConstantAssignment.mch
create mode 100644 src/test/resources/examples/instance/Counter/ModConstantAssignment.tla
create mode 100644 src/test/resources/examples/instance/Counter/OneInstanced.mch
create mode 100644 src/test/resources/examples/instance/Counter/OneInstanced.tla
create mode 100644 src/test/resources/examples/instance/Counter/TwoInstance.mch
create mode 100644 src/test/resources/examples/instance/Counter/TwoInstance.tla
create mode 100644 src/test/resources/examples/instance/Counter/TwoInstanced.mch
create mode 100644 src/test/resources/examples/instance/Counter/TwoInstanced.tla
create mode 100644 src/test/resources/examples/instance/OpArg/OpArg.tla
create mode 100644 src/test/resources/examples/instance/OpArg/OpArgInstanced.mch
create mode 100644 src/test/resources/examples/instance/OpArg/OpArgInstanced.tla
create mode 100644 src/test/resources/examples/instance/configOverride/Counter.tla
create mode 100644 src/test/resources/examples/instance/configOverride/InstanceCounter.cfg
create mode 100644 src/test/resources/examples/instance/configOverride/InstanceCounter.mch
create mode 100644 src/test/resources/examples/instance/configOverride/InstanceCounter.tla
create mode 100644 src/test/resources/examples/instance/configOverride/InstanceCounterException.cfg
create mode 100644 src/test/resources/examples/instance/configOverride/InstanceCounterException.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.cfg
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceOpArg.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceOpArg2.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.cfg
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceOpArgException.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceValue.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/InstanceValue2.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/OpArg.tla
create mode 100644 src/test/resources/examples/instance/constantSubstitution/Value.tla
create mode 100644 src/test/resources/examples/instance/let/InstanceLet.mch
create mode 100644 src/test/resources/examples/instance/let/InstanceLet.tla
create mode 100644 src/test/resources/examples/instance/let/Let.tla
create mode 100644 src/test/resources/examples/instance/twoInstanced/first.tla
create mode 100644 src/test/resources/examples/instance/twoInstanced/second.tla
create mode 100644 src/test/resources/prettyprint/backtranslation/TlaTypes.cfg
create mode 100644 src/test/resources/prettyprint/backtranslation/TlaTypes.tla
create mode 100644 src/test/resources/regression/Club/Club.prob
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
new file mode 100644
index 0000000..868ab5e
--- /dev/null
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -0,0 +1,207 @@
+package de.tla2b.types;
+
+import java.util.Collections;
+import java.util.Iterator;
+import java.util.LinkedHashMap;
+import java.util.Map.Entry;
+
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.tla2b.exceptions.TypeErrorException;
+import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
+
+public class TupleOrFunction extends AbstractHasFollowers {
+ private final LinkedHashMap<Integer, TLAType> types = new LinkedHashMap<Integer, TLAType>();
+
+ public TupleOrFunction(Integer index, TLAType type) {
+ super(TUPLE_OR_FUNCTION);
+ types.put(index, type);
+ if (type instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) type).addFollower(this);
+ }
+ }
+
+ public TupleOrFunction() {
+ super(TUPLE_OR_FUNCTION);
+ }
+
+ public void apply(TypeVisitorInterface visitor) {
+ throw new RuntimeException("Type " + this + " is not a complete type.");
+ }
+
+ @Override
+ public String toString() {
+ FunctionType func = new FunctionType();
+ func.setDomain(IntType.getInstance());
+ func.setRange(new UntypedType());
+ FunctionType res;
+ try {
+ res = func.unify(this);
+ } catch (UnificationException e) {
+ StringBuilder sb = new StringBuilder();
+ sb.append("TupleOrFunction(");
+ for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext();) {
+ Integer key = keys.next();
+ sb.append(key);
+ sb.append(" : ").append(types.get(key));
+ if (keys.hasNext())
+ sb.append(", ");
+ }
+ sb.append(")");
+ throw new RuntimeException("Type "+ sb + "is incomplete");
+ }
+
+ return res.toString();
+
+
+ }
+
+ @Override
+ public PExpression getBNode() {
+ return null;
+ }
+
+ @Override
+ public boolean compare(TLAType o) {
+ if (this.contains(o) || o.contains(this))
+ return false;
+ if (o.getKind() == UNTYPED)
+ return true;
+ if (o instanceof TupleOrFunction) {
+ TupleOrFunction t = (TupleOrFunction) o;
+ for (Entry<Integer, TLAType> entry : types.entrySet()) {
+ if (t.types.containsKey(entry.getKey())
+ && entry.getValue()
+ .compare(t.types.get(entry.getKey()))) {
+ return false;
+ }
+ }
+ }
+ if (o instanceof FunctionType) {
+ FunctionType t = (FunctionType) o;
+ if (!t.getDomain().compare(IntType.getInstance())) {
+ return false;
+ }
+ for (TLAType type : this.types.values()) {
+ if (!type.compare(t.getRange())) {
+ return false;
+ }
+ }
+ return true;
+ }
+ if (o instanceof TupleType) {
+ TupleType t = (TupleType) o;
+ for (int i = 0; i < t.getTypes().size(); i++) {
+ if (this.types.containsKey(i + 1)) {
+ if (!t.getTypes().get(i).compare(this.types.get(i + 1))) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+ // this type is not comparable with all other types
+ return false;
+ }
+
+ @Override
+ public boolean contains(TLAType o) {
+ for (TLAType type : this.types.values()) {
+ if (type.equals(o) || type.contains(o)) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ @Override
+ public boolean isUntyped() {
+ for (TLAType type : types.values()) {
+ if (type.isUntyped())
+ return true;
+ }
+ FunctionType func = new FunctionType();
+ func.setDomain(IntType.getInstance());
+ func.setRange(new UntypedType());
+ if (func.compare(this)) {
+ return false;
+ } else {
+ return true;
+ }
+ }
+
+ @Override
+ public TLAType cloneTLAType() {
+ TupleOrFunction res = new TupleOrFunction();
+ for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
+ res.types.put(new Integer(entry.getKey().intValue()), entry
+ .getValue().cloneTLAType());
+ }
+ return res;
+ }
+
+ @Override
+ public TLAType unify(TLAType o) throws UnificationException {
+ if (!this.compare(o))
+ throw new UnificationException();
+ if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
+ return this;
+ }
+ if (o instanceof FunctionType) {
+ FunctionType funcType = (FunctionType) o;
+ TLAType res = funcType.getRange();
+ for (TLAType type : types.values()) {
+ if (type instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) type).removeFollower(this);
+ }
+ res = res.unify(type);
+ }
+ return funcType;
+ }
+ if (o instanceof TupleType) {
+ TupleType tupleType = (TupleType) o;
+ int max = Collections.max(types.keySet());
+ if (max <= tupleType.getTypes().size()) {
+ for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
+ int index = entry.getKey();
+ TLAType type = entry.getValue();
+ if (type instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) type).removeFollower(this);
+ }
+ TLAType elementOfTuple = tupleType.getTypes()
+ .get(index - 1);
+ elementOfTuple.unify(type);
+ }
+ return tupleType;
+ } else {
+ TLAType range = new UntypedType();
+ for (TLAType type : types.values()) {
+ if (type instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) type).removeFollower(this);
+ }
+ range = range.unify(type);
+ }
+ FunctionType funcType = new FunctionType(IntType.getInstance(),
+ range);
+ return funcType.unify(tupleType);
+ }
+ }
+ throw new RuntimeException();
+ }
+
+ public void setNewType(AbstractHasFollowers oldType,
+ TLAType newType) {
+ LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<Integer, TLAType>(types);
+ for (Entry<Integer, TLAType> entry : temp.entrySet()) {
+ if(entry.getValue().equals(oldType)){
+ types.put(entry.getKey(), newType);
+ if (newType instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) newType).addFollower(this);;
+ }
+ }
+ }
+
+ }
+
+}
diff --git a/src/test/java/de/tla2b/examples/InstanceTest.java b/src/test/java/de/tla2b/examples/InstanceTest.java
new file mode 100644
index 0000000..2041965
--- /dev/null
+++ b/src/test/java/de/tla2b/examples/InstanceTest.java
@@ -0,0 +1,23 @@
+package de.tla2b.examples;
+
+import static de.tla2b.util.TestUtil.runModule;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+public class InstanceTest {
+
+
+ @Test
+ public void testInstanceNoName() throws Exception {
+ String file = "src/test/resources/examples/instance/Counter/InstanceNoName.tla";
+ runModule(file);
+ }
+
+ @Ignore
+ @Test
+ public void testInstance() throws Exception {
+ String file = "src/test/resources/examples/instance/Counter/OneInstanced.tla";
+ runModule(file);
+ }
+}
diff --git a/src/test/resources/examples/instance/Counter/Counter.tla b/src/test/resources/examples/instance/Counter/Counter.tla
new file mode 100644
index 0000000..addaef7
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/Counter.tla
@@ -0,0 +1,9 @@
+-------------------------- MODULE Counter -----------------------------
+EXTENDS Naturals
+CONSTANTS start
+VARIABLE x
+-----------------------------------------------------------------------
+Init == x = start
+val == 1
+Next == x' = x + val
+=======================================================================
diff --git a/src/test/resources/examples/instance/Counter/InstanceDefinition.mch b/src/test/resources/examples/instance/Counter/InstanceDefinition.mch
new file mode 100644
index 0000000..688146d
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/InstanceDefinition.mch
@@ -0,0 +1,13 @@
+MACHINE InstanceDefinition
+DEFINITIONS
+ val == 5
+VARIABLES c
+INVARIANT
+ c : INTEGER
+INITIALISATION
+ c:(c = 0)
+OPERATIONS
+ Next_Op = ANY c_n
+ WHERE c_n : INTEGER & c_n = c + val
+ THEN c := c_n END
+END
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/InstanceDefinition.tla b/src/test/resources/examples/instance/Counter/InstanceDefinition.tla
new file mode 100644
index 0000000..303d8b5
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/InstanceDefinition.tla
@@ -0,0 +1,5 @@
+-------------- MODULE InstanceDefinition ----------------
+VARIABLES c
+val == 5 (* the val definition of the Counter module will be automatically overriden by SANY *)
+INSTANCE Counter WITH x <- c, start <- 0
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/InstanceNoName.mch b/src/test/resources/examples/instance/Counter/InstanceNoName.mch
new file mode 100644
index 0000000..ad110dc
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/InstanceNoName.mch
@@ -0,0 +1,18 @@
+MACHINE InstanceNoName
+ABSTRACT_CONSTANTS start
+PROPERTIES
+ start : INTEGER
+DEFINITIONS
+ Init == c = start;
+
+ val == 1
+VARIABLES c
+INVARIANT
+ c : INTEGER
+INITIALISATION
+ c:(Init)
+OPERATIONS
+ Next_Op = ANY c_n
+ WHERE c_n : INTEGER & c_n = c + val
+ THEN c := c_n END
+END
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/InstanceNoName.tla b/src/test/resources/examples/instance/Counter/InstanceNoName.tla
new file mode 100644
index 0000000..b2e5e4d
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/InstanceNoName.tla
@@ -0,0 +1,6 @@
+-------------- MODULE InstanceNoName ----------------
+CONSTANTS start
+VARIABLES c
+INSTANCE Counter WITH x <- c
+Spec == Init /\ [][Next]_c
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/ModConstantAssignment.cfg b/src/test/resources/examples/instance/Counter/ModConstantAssignment.cfg
new file mode 100644
index 0000000..e4eda93
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/ModConstantAssignment.cfg
@@ -0,0 +1,3 @@
+INIT Init
+NEXT Next
+CONSTANTS val = [Counter] 7
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/ModConstantAssignment.mch b/src/test/resources/examples/instance/Counter/ModConstantAssignment.mch
new file mode 100644
index 0000000..7311530
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/ModConstantAssignment.mch
@@ -0,0 +1,13 @@
+MACHINE ModConstantAssignment
+DEFINITIONS
+ val == 7
+VARIABLES c
+INVARIANT
+ c : INTEGER
+INITIALISATION
+ c:(c = 0)
+OPERATIONS
+ Next_Op = ANY c_n
+ WHERE c_n : INTEGER & c_n = c + val
+ THEN c := c_n END
+END
diff --git a/src/test/resources/examples/instance/Counter/ModConstantAssignment.tla b/src/test/resources/examples/instance/Counter/ModConstantAssignment.tla
new file mode 100644
index 0000000..59009a9
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/ModConstantAssignment.tla
@@ -0,0 +1,4 @@
+-------------- MODULE ModConstantAssignment ----------------
+VARIABLES c
+INSTANCE Counter WITH x <- c, start <- 0
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/OneInstanced.mch b/src/test/resources/examples/instance/Counter/OneInstanced.mch
new file mode 100644
index 0000000..0a7a02d
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/OneInstanced.mch
@@ -0,0 +1,19 @@
+MACHINE OneInstanced
+ABSTRACT_CONSTANTS start
+PROPERTIES
+ start : INTEGER
+DEFINITIONS
+ count_Init == c = start;
+
+ count_val == 1;
+
+VARIABLES c
+INVARIANT
+ c : INTEGER
+INITIALISATION
+ c:(count_Init)
+OPERATIONS
+ count_Next_Op = ANY c_n
+ WHERE c_n : INTEGER & c_n = c + count_val
+ THEN c := c_n END
+END
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/OneInstanced.tla b/src/test/resources/examples/instance/Counter/OneInstanced.tla
new file mode 100644
index 0000000..69cca02
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/OneInstanced.tla
@@ -0,0 +1,8 @@
+-------------- MODULE OneInstanced ----------------
+CONSTANTS start
+VARIABLES c
+count == INSTANCE Counter WITH x <- c
+Init == count!Init
+Next == count!Next
+=================================
+
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/TwoInstance.mch b/src/test/resources/examples/instance/Counter/TwoInstance.mch
new file mode 100644
index 0000000..d23db8b
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/TwoInstance.mch
@@ -0,0 +1,32 @@
+MACHINE TwoInstanced
+ABSTRACT_CONSTANTS start
+PROPERTIES
+ start : INTEGER
+DEFINITIONS
+ count_Init == c = start;
+
+ count_val == 1;
+
+ count_Next == c_n = c + count_val;
+
+ count2_Init == c2 = 0;
+
+ count2_val == 1;
+
+ count2_Next == c2_n = c2 + count2_val;
+
+VARIABLES c, c2
+INVARIANT
+ c : INTEGER
+ & c2 : INTEGER
+INITIALISATION
+ c, c2:(count_Init & count2_Init)
+OPERATIONS
+ Next1_Op = ANY c_n
+ WHERE c_n : INTEGER & count_Next & TRUE = TRUE
+ THEN c := c_n END;
+
+ Next2_Op = ANY c2_n
+ WHERE c2_n : INTEGER & count2_Next & TRUE = TRUE
+ THEN c2 := c2_n END
+END
diff --git a/src/test/resources/examples/instance/Counter/TwoInstance.tla b/src/test/resources/examples/instance/Counter/TwoInstance.tla
new file mode 100644
index 0000000..5939e9d
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/TwoInstance.tla
@@ -0,0 +1,9 @@
+-------------- MODULE TwoInstanced --------------
+CONSTANTS start
+VARIABLES c, c2
+count == INSTANCE Counter WITH x <- c
+count2 == INSTANCE Counter WITH x <- c2, start <- 0
+Init == count!Init /\ count2!Init
+Next == \/ (count!Next /\ UNCHANGED c2)
+ \/ (count2!Next /\ UNCHANGED c)
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/Counter/TwoInstanced.mch b/src/test/resources/examples/instance/Counter/TwoInstanced.mch
new file mode 100644
index 0000000..d23db8b
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/TwoInstanced.mch
@@ -0,0 +1,32 @@
+MACHINE TwoInstanced
+ABSTRACT_CONSTANTS start
+PROPERTIES
+ start : INTEGER
+DEFINITIONS
+ count_Init == c = start;
+
+ count_val == 1;
+
+ count_Next == c_n = c + count_val;
+
+ count2_Init == c2 = 0;
+
+ count2_val == 1;
+
+ count2_Next == c2_n = c2 + count2_val;
+
+VARIABLES c, c2
+INVARIANT
+ c : INTEGER
+ & c2 : INTEGER
+INITIALISATION
+ c, c2:(count_Init & count2_Init)
+OPERATIONS
+ Next1_Op = ANY c_n
+ WHERE c_n : INTEGER & count_Next & TRUE = TRUE
+ THEN c := c_n END;
+
+ Next2_Op = ANY c2_n
+ WHERE c2_n : INTEGER & count2_Next & TRUE = TRUE
+ THEN c2 := c2_n END
+END
diff --git a/src/test/resources/examples/instance/Counter/TwoInstanced.tla b/src/test/resources/examples/instance/Counter/TwoInstanced.tla
new file mode 100644
index 0000000..5939e9d
--- /dev/null
+++ b/src/test/resources/examples/instance/Counter/TwoInstanced.tla
@@ -0,0 +1,9 @@
+-------------- MODULE TwoInstanced --------------
+CONSTANTS start
+VARIABLES c, c2
+count == INSTANCE Counter WITH x <- c
+count2 == INSTANCE Counter WITH x <- c2, start <- 0
+Init == count!Init /\ count2!Init
+Next == \/ (count!Next /\ UNCHANGED c2)
+ \/ (count2!Next /\ UNCHANGED c)
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/OpArg/OpArg.tla b/src/test/resources/examples/instance/OpArg/OpArg.tla
new file mode 100644
index 0000000..60a3181
--- /dev/null
+++ b/src/test/resources/examples/instance/OpArg/OpArg.tla
@@ -0,0 +1,7 @@
+-------------- MODULE OpArg ----------------
+EXTENDS Naturals
+CONSTANTS k(_,_)
+VARIABLES c
+Init == c = 1
+Next == c' = c + k(1, 2)
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/OpArg/OpArgInstanced.mch b/src/test/resources/examples/instance/OpArg/OpArgInstanced.mch
new file mode 100644
index 0000000..a9e7cf3
--- /dev/null
+++ b/src/test/resources/examples/instance/OpArg/OpArgInstanced.mch
@@ -0,0 +1,14 @@
+MACHINE OpArgInstanced
+DEFINITIONS
+ foo(a,b) == a + b;
+
+VARIABLES c
+INVARIANT
+ c : INTEGER
+INITIALISATION
+ c:(c = 1)
+OPERATIONS
+ Next_Op = ANY c_n
+ WHERE c_n : INTEGER & c_n = c + foo(1,2)
+ THEN c := c_n END
+END
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/OpArg/OpArgInstanced.tla b/src/test/resources/examples/instance/OpArg/OpArgInstanced.tla
new file mode 100644
index 0000000..07e36d0
--- /dev/null
+++ b/src/test/resources/examples/instance/OpArg/OpArgInstanced.tla
@@ -0,0 +1,6 @@
+-------------- MODULE OpArgInstanced --------------
+EXTENDS Naturals
+VARIABLES c
+foo(a,b) == a + b
+INSTANCE OpArg WITH k <- foo
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/configOverride/Counter.tla b/src/test/resources/examples/instance/configOverride/Counter.tla
new file mode 100644
index 0000000..addaef7
--- /dev/null
+++ b/src/test/resources/examples/instance/configOverride/Counter.tla
@@ -0,0 +1,9 @@
+-------------------------- MODULE Counter -----------------------------
+EXTENDS Naturals
+CONSTANTS start
+VARIABLE x
+-----------------------------------------------------------------------
+Init == x = start
+val == 1
+Next == x' = x + val
+=======================================================================
diff --git a/src/test/resources/examples/instance/configOverride/InstanceCounter.cfg b/src/test/resources/examples/instance/configOverride/InstanceCounter.cfg
new file mode 100644
index 0000000..3471675
--- /dev/null
+++ b/src/test/resources/examples/instance/configOverride/InstanceCounter.cfg
@@ -0,0 +1,4 @@
+INIT Init
+NEXT Next
+CONSTANTS
+val =[Counter] 4
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/configOverride/InstanceCounter.mch b/src/test/resources/examples/instance/configOverride/InstanceCounter.mch
new file mode 100644
index 0000000..5b0c40a
--- /dev/null
+++ b/src/test/resources/examples/instance/configOverride/InstanceCounter.mch
@@ -0,0 +1,16 @@
+MACHINE InstanceCounter
+ABSTRACT_CONSTANTS start
+PROPERTIES
+ start : INTEGER
+DEFINITIONS
+ val == 4
+VARIABLES x
+INVARIANT
+ x : INTEGER
+INITIALISATION
+ x:(x = start)
+OPERATIONS
+ Next_Op = ANY x_n
+ WHERE x_n : INTEGER & x_n = x + val
+ THEN x := x_n END
+END
diff --git a/src/test/resources/examples/instance/configOverride/InstanceCounter.tla b/src/test/resources/examples/instance/configOverride/InstanceCounter.tla
new file mode 100644
index 0000000..de92f0f
--- /dev/null
+++ b/src/test/resources/examples/instance/configOverride/InstanceCounter.tla
@@ -0,0 +1,5 @@
+-------------- MODULE InstanceCounter ----------------
+CONSTANTS start
+VARIABLES x
+INSTANCE Counter
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/configOverride/InstanceCounterException.cfg b/src/test/resources/examples/instance/configOverride/InstanceCounterException.cfg
new file mode 100644
index 0000000..efebca9
--- /dev/null
+++ b/src/test/resources/examples/instance/configOverride/InstanceCounterException.cfg
@@ -0,0 +1,4 @@
+INIT Init
+NEXT Next
+CONSTANTS
+start <-[Counter] foo
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/configOverride/InstanceCounterException.tla b/src/test/resources/examples/instance/configOverride/InstanceCounterException.tla
new file mode 100644
index 0000000..268aa31
--- /dev/null
+++ b/src/test/resources/examples/instance/configOverride/InstanceCounterException.tla
@@ -0,0 +1,6 @@
+-------------- MODULE InstanceCounterException ----------------
+CONSTANTS start
+VARIABLES x
+INSTANCE Counter
+foo == 11
+==========================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.cfg b/src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.cfg
new file mode 100644
index 0000000..ff2050f
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.cfg
@@ -0,0 +1 @@
+CONSTANTS foo3 <- bazz
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.tla
new file mode 100644
index 0000000..52ffeda
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceInstanceOpArg.tla
@@ -0,0 +1,7 @@
+-------------- MODULE InstanceInstanceOpArg ----------------
+EXTENDS Naturals
+CONSTANTS c3, foo3(_,_)
+bazz(a,b) == a + b
+INSTANCE InstanceOpArg WITH c2 <- c3, foo2 <- foo3
+ASSUME def /\ c3 = 3
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg.tla
new file mode 100644
index 0000000..74d8d2c
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg.tla
@@ -0,0 +1,5 @@
+-------------------------- MODULE InstanceOpArg -----------------------------
+CONSTANTS c2, foo2(_,_)
+INSTANCE OpArg WITH c <- c2, foo <- foo2
+
+=======================================================================
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg2.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg2.tla
new file mode 100644
index 0000000..72a3bb6
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg2.tla
@@ -0,0 +1,7 @@
+-------------- MODULE InstanceOpArg2 ----------------
+EXTENDS Naturals
+CONSTANTS c2
+bar(a,b) == a + b
+INSTANCE OpArg WITH c <- c2, foo <- bar
+ASSUME def /\ c2 = 3
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.cfg b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.cfg
new file mode 100644
index 0000000..016dd9c
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.cfg
@@ -0,0 +1 @@
+CONSTANTS bar <- bazz
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.tla
new file mode 100644
index 0000000..7b37512
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.tla
@@ -0,0 +1,7 @@
+-------------- MODULE InstanceOpArg3 ----------------
+EXTENDS Naturals
+CONSTANTS c2, bar(_,_)
+bazz(a,b) == a + b
+INSTANCE OpArg WITH c <- c2, foo <- bar
+ASSUME def /\ c2 = 3
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceOpArgException.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArgException.tla
new file mode 100644
index 0000000..0d79faa
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceOpArgException.tla
@@ -0,0 +1,6 @@
+-------------- MODULE InstanceOpArgException ----------------
+EXTENDS Naturals
+CONSTANTS c2, bar(_,_)
+INSTANCE OpArg WITH c <- c2, foo <- bar
+ASSUME def /\ c2 = 3
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceValue.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceValue.tla
new file mode 100644
index 0000000..1b29c5f
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceValue.tla
@@ -0,0 +1,6 @@
+-------------- MODULE InstanceValue ----------------
+EXTENDS Naturals
+CONSTANTS c
+INSTANCE Value WITH val <- 1+1
+ASSUME def
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/InstanceValue2.tla b/src/test/resources/examples/instance/constantSubstitution/InstanceValue2.tla
new file mode 100644
index 0000000..a6e649e
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/InstanceValue2.tla
@@ -0,0 +1,6 @@
+-------------- MODULE InstanceValue2 ----------------
+EXTENDS Naturals
+CONSTANTS c, val2
+INSTANCE Value WITH val <- val2
+ASSUME def /\ val2 = 1
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/constantSubstitution/OpArg.tla b/src/test/resources/examples/instance/constantSubstitution/OpArg.tla
new file mode 100644
index 0000000..d129ef5
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/OpArg.tla
@@ -0,0 +1,5 @@
+-------------------------- MODULE OpArg -----------------------------
+CONSTANTS c, foo(_,_)
+def == c = foo(1,2)
+
+=======================================================================
diff --git a/src/test/resources/examples/instance/constantSubstitution/Value.tla b/src/test/resources/examples/instance/constantSubstitution/Value.tla
new file mode 100644
index 0000000..366f450
--- /dev/null
+++ b/src/test/resources/examples/instance/constantSubstitution/Value.tla
@@ -0,0 +1,6 @@
+-------------------------- MODULE Value -----------------------------
+EXTENDS Naturals
+CONSTANTS c, val
+def == c = val
+
+=======================================================================
diff --git a/src/test/resources/examples/instance/let/InstanceLet.mch b/src/test/resources/examples/instance/let/InstanceLet.mch
new file mode 100644
index 0000000..39f7baa
--- /dev/null
+++ b/src/test/resources/examples/instance/let/InstanceLet.mch
@@ -0,0 +1,26 @@
+MACHINE InstanceLet
+DEFINITIONS
+ inst_Init == c = 1;
+
+ inst_val == 4;
+
+ inst_foo(p) == 1 + e + p;
+ inst_Next == #e.(e : {1, 2} & c_n = c + inst_foo(3) + inst_val);
+
+ inst2_Init == c2 = 1;
+
+ inst2_val == 4;
+
+ inst2_foo(p) == 1 + e + p;
+ inst2_Next == #e.(e : {1, 2} & c2_n = c2 + inst2_foo(3) + inst2_val)
+VARIABLES c, c2
+INVARIANT
+ c : INTEGER
+ & c2 : INTEGER
+INITIALISATION
+ c, c2:(inst_Init & inst2_Init)
+OPERATIONS
+ Next_Op = ANY c_n, c2_n
+ WHERE c_n : INTEGER & c2_n : INTEGER & inst_Next & inst2_Next
+ THEN c, c2 := c_n, c2_n END
+END
diff --git a/src/test/resources/examples/instance/let/InstanceLet.tla b/src/test/resources/examples/instance/let/InstanceLet.tla
new file mode 100644
index 0000000..91f6f07
--- /dev/null
+++ b/src/test/resources/examples/instance/let/InstanceLet.tla
@@ -0,0 +1,7 @@
+-------------- MODULE InstanceLet ----------------
+VARIABLES c, c2
+inst == INSTANCE Let WITH x <- c
+inst2 == INSTANCE Let WITH x <- c2
+Init == inst!Init /\ inst2!Init
+Next == inst!Next /\ inst2!Next
+=================================
\ No newline at end of file
diff --git a/src/test/resources/examples/instance/let/Let.tla b/src/test/resources/examples/instance/let/Let.tla
new file mode 100644
index 0000000..e715e11
--- /dev/null
+++ b/src/test/resources/examples/instance/let/Let.tla
@@ -0,0 +1,14 @@
+---------------------------- MODULE Let -------------------------------
+EXTENDS Naturals
+VARIABLES x
+-----------------------------------------------------------------------------
+Init == x = 1
+val == 4
+Next ==
+ \E e \in {1,2}:
+ LET
+ foo(p) == 1 + e + p
+ IN
+ x' = x + foo(3) + val
+=============================================================================
+
diff --git a/src/test/resources/examples/instance/twoInstanced/first.tla b/src/test/resources/examples/instance/twoInstanced/first.tla
new file mode 100644
index 0000000..3a03509
--- /dev/null
+++ b/src/test/resources/examples/instance/twoInstanced/first.tla
@@ -0,0 +1,5 @@
+-------------------------- MODULE first -----------------------------
+EXTENDS Naturals
+CONSTANTS c2
+INSTANCE second WITH c1 <- c2
+=======================================================================
diff --git a/src/test/resources/examples/instance/twoInstanced/second.tla b/src/test/resources/examples/instance/twoInstanced/second.tla
new file mode 100644
index 0000000..d41e27a
--- /dev/null
+++ b/src/test/resources/examples/instance/twoInstanced/second.tla
@@ -0,0 +1,6 @@
+-------------------------- MODULE first -----------------------------
+EXTENDS Naturals
+CONSTANTS c1
+
+val == c1 + 1
+=======================================================================
diff --git a/src/test/resources/prettyprint/backtranslation/TlaTypes.cfg b/src/test/resources/prettyprint/backtranslation/TlaTypes.cfg
new file mode 100644
index 0000000..c6682a4
--- /dev/null
+++ b/src/test/resources/prettyprint/backtranslation/TlaTypes.cfg
@@ -0,0 +1,2 @@
+CONSTANTS
+m = m
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/backtranslation/TlaTypes.tla b/src/test/resources/prettyprint/backtranslation/TlaTypes.tla
new file mode 100644
index 0000000..272b73d
--- /dev/null
+++ b/src/test/resources/prettyprint/backtranslation/TlaTypes.tla
@@ -0,0 +1,20 @@
+------------------------- MODULE TlaTypes ---------------------
+
+EXTENDS Naturals, TLC
+CONSTANTS a, b, c, d, e, f, g, h, i, j, k, l
+ ,m
+ASSUME a = 1
+ASSUME b = TRUE
+ASSUME c = "abc"
+ASSUME d = m
+
+ASSUME e = <<1,2>>
+ASSUME f = <<1,2,3>>
+ASSUME g = << <<1,2>>,3>>
+ASSUME h = <<>> /\ h \in UNION{[x -> Nat] :x \in SUBSET Nat}
+ASSUME i = <<1>>
+ASSUME j = (1 :> 2)
+
+ASSUME k = [a|-> 1, b|-> TRUE]
+ASSUME l = [a|-> 1] /\ l # [b|-> TRUE]
+========
\ No newline at end of file
diff --git a/src/test/resources/regression/Club/Club.prob b/src/test/resources/regression/Club/Club.prob
new file mode 100644
index 0000000..e531ebf
--- /dev/null
+++ b/src/test/resources/regression/Club/Club.prob
@@ -0,0 +1,3 @@
+parser_version('2014-03-12 22:57:52.564').
+classical_b('Club',['/Users/hansen/git/tla2bAST/src/test/resources/regression/Club/Club.tla']).
+machine(abstract_machine(1,machine(2),machine_header(3,'Club',[]),[sets(4,[enumerated_set(5,'ENUM1',[identifier(6,n1),identifier(7,n2),identifier(8,n3)])]),constants(9,[identifier(info(10,tla_type(integer)),capacity),identifier(info(11,tla_type(set(modelvalue))),'NAME'),identifier(info(12,tla_type(integer)),total)]),properties(13,conjunct(14,conjunct(15,conjunct(16,conjunct(17,conjunct(18,member(19,identifier(20,capacity),integer_set(21)),equal(22,identifier(23,'NAME'),identifier(24,'ENUM1'))),member(25,identifier(26,total),integer_set(27))),conjunct(28,member(29,identifier(30,capacity),natural_set(31)),equal(32,identifier(33,capacity),integer(34,2)))),greater(35,card(36,identifier(37,'NAME')),identifier(38,capacity))),conjunct(39,member(40,identifier(41,total),natural_set(42)),greater(43,identifier(44,total),integer(45,2))))),variables(46,[identifier(info(47,tla_type(set(modelvalue))),member),identifier(info(48,tla_type(set(modelvalue))),waiting)]),invariant(49,conjunct(50,member(51,identifier(52,member),pow_subset(53,identifier(54,'ENUM1'))),member(55,identifier(56,waiting),pow_subset(57,identifier(58,'ENUM1'))))),initialisation(59,becomes_such(60,[identifier(61,member),identifier(62,waiting)],conjunct(63,equal(64,identifier(65,member),empty_set(66)),equal(67,identifier(68,waiting),empty_set(69))))),operations(70,[operation(71,identifier(71,join_queue),[],[identifier(72,nn)],any(73,[identifier(74,member_n)],conjunct(75,conjunct(76,conjunct(77,conjunct(78,conjunct(79,member(80,identifier(81,nn),identifier(82,'NAME')),not_member(83,identifier(84,nn),identifier(85,member))),not_member(86,identifier(87,nn),identifier(88,waiting))),member(89,identifier(90,member_n),pow_subset(91,identifier(92,'ENUM1')))),less(93,card(94,identifier(95,waiting)),identifier(96,total))),equal(97,identifier(98,member_n),identifier(99,member))),assign(100,[identifier(101,waiting),identifier(102,member)],[union(103,identifier(104,waiting),set_extension(105,[identifier(106,nn)])),identifier(107,member_n)]))),operation(108,identifier(108,join),[],[identifier(109,nn)],select(110,conjunct(111,conjunct(112,conjunct(113,member(114,identifier(115,nn),identifier(116,'NAME')),member(117,identifier(118,nn),identifier(119,waiting))),less(120,card(121,identifier(122,member)),identifier(123,capacity))),less(124,card(125,identifier(126,member)),identifier(127,capacity))),assign(128,[identifier(129,member),identifier(130,waiting)],[union(131,identifier(132,member),set_extension(133,[identifier(134,nn)])),minus_or_set_subtract(135,identifier(136,waiting),set_extension(137,[identifier(138,nn)]))]),[])),operation(139,identifier(139,remove),[],[identifier(140,nn)],any(141,[identifier(142,waiting_n)],conjunct(143,conjunct(144,conjunct(145,member(146,identifier(147,nn),identifier(148,'NAME')),member(149,identifier(150,nn),identifier(151,member))),member(152,identifier(153,waiting_n),pow_subset(154,identifier(155,'ENUM1')))),equal(156,identifier(157,waiting_n),identifier(158,waiting))),assign(159,[identifier(160,member),identifier(161,waiting)],[minus_or_set_subtract(162,identifier(163,member),set_extension(164,[identifier(165,nn)])),identifier(166,waiting_n)])))])])).
--
GitLab