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 0000000000000000000000000000000000000000..868ab5e1b4ca4b65c8f1c4d86a057d60496aaa2a
--- /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 0000000000000000000000000000000000000000..2041965fdab3788ec6be40d1e9526c2f5fbcd85d
--- /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 0000000000000000000000000000000000000000..addaef7e755a413ee720c9a43733071d439679c9
--- /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 0000000000000000000000000000000000000000..688146d036fac93fdd9ed749cca16db291bd37a4
--- /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 0000000000000000000000000000000000000000..303d8b59e063b0550108b125949b6943ec2d4f4b
--- /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 0000000000000000000000000000000000000000..ad110dca9e20e37494cfdf54fe03a6569d974b29
--- /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 0000000000000000000000000000000000000000..b2e5e4d0d3b1562d88e5b9e5cf43f7d857126f64
--- /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 0000000000000000000000000000000000000000..e4eda93e3f0fcbb23080a8e7dc29081ce42ffe76
--- /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 0000000000000000000000000000000000000000..73115303fa5b849795a8bf7d78e4962e013a7776
--- /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 0000000000000000000000000000000000000000..59009a98f2468d1364464f2a9f8f85efe41b7f43
--- /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 0000000000000000000000000000000000000000..0a7a02dad5d328d1f245e4bdd03d6b7f3264577c
--- /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 0000000000000000000000000000000000000000..69cca02f78c9a06ca1990a479ae13df5a6a11b43
--- /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 0000000000000000000000000000000000000000..d23db8b678843cd223a8bac4cceb4fe0d07c3fb8
--- /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 0000000000000000000000000000000000000000..5939e9dcb2ab565f85bc6844159d0a6a7414ded8
--- /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 0000000000000000000000000000000000000000..d23db8b678843cd223a8bac4cceb4fe0d07c3fb8
--- /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 0000000000000000000000000000000000000000..5939e9dcb2ab565f85bc6844159d0a6a7414ded8
--- /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 0000000000000000000000000000000000000000..60a318106bbc6e701b724430bdb0a27c879d2035
--- /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 0000000000000000000000000000000000000000..a9e7cf31d3ead0f7a3936d849ad61bd5310d9150
--- /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 0000000000000000000000000000000000000000..07e36d098a26749032f3c488f1daabf76e3eab9e
--- /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 0000000000000000000000000000000000000000..addaef7e755a413ee720c9a43733071d439679c9
--- /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 0000000000000000000000000000000000000000..3471675f8ebd5b9b1474da75830d4a8fe9c3a5bc
--- /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 0000000000000000000000000000000000000000..5b0c40aab287f28cbea784919bd1b0e12479680a
--- /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 0000000000000000000000000000000000000000..de92f0f504ca2bdaf151bcc0ae87dd43f01dcf7c
--- /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 0000000000000000000000000000000000000000..efebca9fc0b6e5d9309a96fc72fd7a0695c0c2f7
--- /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 0000000000000000000000000000000000000000..268aa31239fdcc8d64990010afda015c70795a52
--- /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 0000000000000000000000000000000000000000..ff2050f0405ec0c0440ed7fc8ee2ac72d4c8ff1e
--- /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 0000000000000000000000000000000000000000..52ffeda8a2e77e841a1ac85e538fcb3e47b980cb
--- /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 0000000000000000000000000000000000000000..74d8d2c25c59d1c9b9d1c732ccbd2ae9980075b8
--- /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 0000000000000000000000000000000000000000..72a3bb64df1b6e79622182987c51c3f11e23209c
--- /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 0000000000000000000000000000000000000000..016dd9c9c87a0fb70651f40e8af1d3e3da0bc30d
--- /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 0000000000000000000000000000000000000000..7b37512bf2d05d014722c0b7dc9db29b0f51ceb1
--- /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 0000000000000000000000000000000000000000..0d79faacfda771f54fd5385e3a7415b914b9594c
--- /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 0000000000000000000000000000000000000000..1b29c5f56f7706acc5b3a362389689431dae235c
--- /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 0000000000000000000000000000000000000000..a6e649e164c07842e2d71c67dc25d838f4ac823b
--- /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 0000000000000000000000000000000000000000..d129ef51a7e4112c0c1d9165f48d3416b9b6882c
--- /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 0000000000000000000000000000000000000000..366f450e641cc29eb1f8b52fb6033aa8c6a007c8
--- /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 0000000000000000000000000000000000000000..39f7baa86628f762aa896dc57e8d51e5e12aee8e
--- /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 0000000000000000000000000000000000000000..91f6f079b2169857c61d0a0321ecefe927eb2c59
--- /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 0000000000000000000000000000000000000000..e715e11af7b1ae46c0fbcff449d9e923ca0f812b
--- /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 0000000000000000000000000000000000000000..3a03509da1cd4b153600b0dd37de4a89a9a39b72
--- /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 0000000000000000000000000000000000000000..d41e27a04046fe739ec5bbee89ee0be663fbafca
--- /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 0000000000000000000000000000000000000000..c6682a4b1407f05a893d29612c9987506384acf2
--- /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 0000000000000000000000000000000000000000..272b73df1685367431957d6151a5039dc0a12988
--- /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 0000000000000000000000000000000000000000..e531ebfc34faed7f90410746947b3ca07ed5a934
--- /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)])))])])).