From e0aeaea733e3ca93ffe8029376d6453e965378e1 Mon Sep 17 00:00:00 2001
From: Graham Hay <grahamrhay@gmail.com>
Date: Thu, 18 Jan 2024 12:28:34 +0000
Subject: [PATCH] Add some tests

---
 syn_tests.cfg |  6 ++++++
 syn_tests.tla | 20 ++++++++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 syn_tests.cfg
 create mode 100644 syn_tests.tla

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"}
+====