added missing files

src/main/java/de/tla2b/types/TupleOrFunction.java

+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);;
+				}
+			}
+		}
+		
+	}
+
+}

src/test/java/de/tla2b/examples/InstanceTest.java

+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);
+	}
+}

src/test/resources/examples/instance/Counter/Counter.tla

+-------------------------- MODULE Counter -----------------------------
+EXTENDS Naturals
+CONSTANTS start
+VARIABLE x
+-----------------------------------------------------------------------
+Init  ==  x = start
+val == 1
+Next  ==  x' = x + val
+=======================================================================

src/test/resources/examples/instance/Counter/InstanceDefinition.mch

+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

src/test/resources/examples/instance/Counter/InstanceDefinition.tla

+-------------- 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

src/test/resources/examples/instance/Counter/InstanceNoName.mch

+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

src/test/resources/examples/instance/Counter/InstanceNoName.tla

+-------------- MODULE InstanceNoName ----------------
+CONSTANTS start
+VARIABLES c
+INSTANCE Counter WITH x <- c
+Spec == Init /\ [][Next]_c
+=================================
\ No newline at end of file

src/test/resources/examples/instance/Counter/ModConstantAssignment.cfg

+INIT Init
+NEXT Next
+CONSTANTS val = [Counter] 7
\ No newline at end of file

src/test/resources/examples/instance/Counter/ModConstantAssignment.mch

+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

src/test/resources/examples/instance/Counter/ModConstantAssignment.tla

+-------------- MODULE ModConstantAssignment ----------------
+VARIABLES c
+INSTANCE Counter WITH x <- c, start <- 0
+=================================
\ No newline at end of file

src/test/resources/examples/instance/Counter/OneInstanced.mch

+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

src/test/resources/examples/instance/Counter/OneInstanced.tla

+-------------- MODULE OneInstanced ----------------
+CONSTANTS start
+VARIABLES c
+count == INSTANCE Counter WITH x <- c
+Init == count!Init
+Next == count!Next
+=================================
+		
\ No newline at end of file

src/test/resources/examples/instance/Counter/TwoInstance.mch

+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

src/test/resources/examples/instance/Counter/TwoInstance.tla

+-------------- 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

src/test/resources/examples/instance/Counter/TwoInstanced.mch

+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

src/test/resources/examples/instance/Counter/TwoInstanced.tla

+-------------- 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

src/test/resources/examples/instance/OpArg/OpArg.tla

+-------------- MODULE OpArg ----------------
+EXTENDS Naturals
+CONSTANTS k(_,_)
+VARIABLES c
+Init == c = 1 
+Next == c' = c + k(1, 2)
+=================================
\ No newline at end of file

src/test/resources/examples/instance/OpArg/OpArgInstanced.mch

+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

src/test/resources/examples/instance/OpArg/OpArgInstanced.tla

+-------------- MODULE OpArgInstanced --------------
+EXTENDS Naturals
+VARIABLES c
+foo(a,b) == a + b
+INSTANCE OpArg WITH k <- foo
+=================================
\ No newline at end of file

src/test/resources/examples/instance/configOverride/Counter.tla

+-------------------------- MODULE Counter -----------------------------
+EXTENDS Naturals
+CONSTANTS start
+VARIABLE x
+-----------------------------------------------------------------------
+Init  ==  x = start
+val == 1
+Next  ==  x' = x + val
+=======================================================================