Add some tests

grahamrhay · Jan 18, 2024 · e0aeaea · e0aeaea
1 parent 033bb28
commit e0aeaea
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 0 deletions.
diff --git a/syn_tests.cfg b/syn_tests.cfg
@@ -0,0 +1,6 @@
+INIT I
+NEXT N
+
+CONSTANTS
+Nodes = {}
+MaxDisconnections = 0
diff --git a/syn_tests.tla b/syn_tests.tla
@@ -0,0 +1,20 @@
+---- MODULE syn_tests ----
+EXTENDS syn
+
+VARIABLE x
+
+I == FALSE /\ x = 0
+N == FALSE /\ x' = x
+
+\* AllRegisteredForNode
+
+ASSUME LET l == ("n1" :> <<>> @@ "n2" :> [a |-> 0, b |-> 2] @@ "n3" :> [c |-> 1])
+       res == AllRegisteredForNode(l)
+       IN res = {"a", "b", "c"}
+
+\* Duplicates
+
+ASSUME LET l == ("n1" :> <<>> @@ "n2" :> [a |-> 0] @@ "n3" :> [a |-> 1])
+       res == Duplicates(DOMAIN l, l, {})
+       IN res = {"a"}
+====