remove: add simple remove model

2019-01-14 16:17:07 +01:00
parent 7e0edb007c
commit 31fbbc4d95
1 changed files with 12 additions and 0 deletions
--- a/Remove.tla
+++ b/Remove.tla
@@ -0,0 +1,12 @@
+------------------------------- MODULE Remove -------------------------------
+
+EXTENDS Integers, Sequences
+
+Remove(i, seq) == 
+  [j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j] 
+                                      ELSE seq[j+1]]
+
+=============================================================================
+\* Modification History
+\* Last modified Mon Jan 14 16:12:46 CET 2019 by veitheller
+\* Created Mon Jan 14 16:12:39 CET 2019 by veitheller