From 7b416cba02a764396840942d58908e9ec7035357 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 15 Dec 2015 10:44:28 +0100
Subject: [PATCH] Fixed function assignment translation
---
.../resources/standardModules/Functions.tla | 5 ++--
.../de/tlc4b/tlc/integration/FixedBugs.java | 23 +++++++++++++++++++
2 files changed, 26 insertions(+), 2 deletions(-)
create mode 100644 src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
diff --git a/src/main/resources/standardModules/Functions.tla b/src/main/resources/standardModules/Functions.tla
index 7e9d2bb..6cffb41 100644
--- a/src/main/resources/standardModules/Functions.tla
+++ b/src/main/resources/standardModules/Functions.tla
@@ -1,5 +1,5 @@
----------------------------- 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]:
diff --git a/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
new file mode 100644
index 0000000..90a8309
--- /dev/null
+++ b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
@@ -0,0 +1,23 @@
+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));
+ }
+}
--
GitLab