Fixed function assignment translation

src/main/resources/standardModules/Functions.tla

 ----------------------------- MODULE Functions -----------------------------
-EXTENDS FiniteSets
+EXTENDS FiniteSets, TLC
 
 Range(f) == {f[x] : x \in DOMAIN f}
  \* The range of the function f
@@ -31,7 +31,8 @@ Inverse(f) == {<<f[x],x>>: x \in DOMAIN f}
 Override(f, g) == [x \in (DOMAIN f) \cup DOMAIN g |-> IF x \in DOMAIN g THEN g[x] ELSE f[x]]
  \* Overwriting of the function f with the function g
 
-FuncAssign(f, d, e) == [f EXCEPT ![d] = e]
+FuncAssign(f, d, e) ==  d :> e @@ f
+ \* [x \in (DOMAIN f) \cup {d} |-> IF x = d THEN e ELSE f[x]]
  \* Overwriting the function f at index d with value e
 
 TotalInjFunc(S, T) == {f \in [S -> T]:

src/test/java/de/tlc4b/tlc/integration/FixedBugs.java

+package de.tlc4b.tlc.integration;
+
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.testString;
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+
+public class FixedBugs {
+
+	@Test
+	public void testFunctionAssignment() throws Exception {
+		String machine = 
+				"MACHINE Test\n"
+				+ "VARIABLES x \n"
+				+ "INVARIANT x : 1..3 +-> 1..2 \n"
+				+ "INITIALISATION x := {} \n"
+				+ "OPERATIONS foo = PRE x = {} THEN x(1) := 2 END \n"
+				+ "END";
+		assertEquals(Deadlock, testString(machine));
+	}
+}