diff --git a/syn_tests.cfg b/syn_tests.cfg new file mode 100644 index 0000000..e7181db --- /dev/null +++ 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 new file mode 100644 index 0000000..e8e31d6 --- /dev/null +++ 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"} +====