Register/unregister

grahamrhay · Dec 20, 2023 · 9e2a928 · 9e2a928
commit 9e2a928
Show file tree

Hide file tree

Showing 5 changed files with 56 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,2 @@
+states/
+syn_TTrace_*
diff --git a/README.md b/README.md
@@ -0,0 +1,7 @@
+# It's a Syn!
+
+## Run the model
+
+```
+docker run --rm -it -v $PWD:/app -w /app openjdk:14-jdk-alpine java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC -config syn.cfg -workers auto -cleanup syn.tla
+```
diff --git a/syn.cfg b/syn.cfg
@@ -0,0 +1,5 @@
+INIT Init
+NEXT Next
+
+INVARIANTS
+AllRegistered
diff --git a/syn.tla b/syn.tla
@@ -0,0 +1,42 @@
+---- MODULE syn ----
+EXTENDS FiniteSets, Integers
+
+VARIABLES registered, next_val, added, removed
+
+vars == <<registered, next_val, added, removed>>
+
+Init ==
+    /\ registered = {}
+    /\ next_val = 0
+    /\ added = 0
+    /\ removed = 0
+
+Register ==
+    /\ next_val < 5
+    /\ registered' = registered \union {next_val}
+    /\ next_val' = next_val + 1
+    /\ added' = added + 1
+    /\ UNCHANGED <<removed>>
+
+ItemToRemove ==
+    CHOOSE r \in registered: TRUE
+
+Unregister ==
+    /\ Cardinality(registered) > 0
+    /\ registered' = registered \ {ItemToRemove}
+    /\ removed' = removed + 1
+    /\ UNCHANGED <<added, next_val>>
+
+Complete ==
+    /\ next_val = 5
+    /\ UNCHANGED <<added, next_val, registered, removed>>
+
+Next ==
+    \/ Register
+    \/ Unregister
+    \/ Complete
+
+Spec == Init /\ [][Next]_vars
+
+AllRegistered == Cardinality(registered) = (added - removed)
+====
diff --git a/tla2tools.jar b/tla2tools.jar