From d0faf6ffe1ab920a748e45c8472dc20dcc1939f5 Mon Sep 17 00:00:00 2001
From: Jeremy Wall <jeremy@marzhillstudios.com>
Date: Sat, 26 Nov 2022 18:13:23 -0500
Subject: [PATCH] TLA+ Specification

---
 .gitignore      |  3 +++
 tla/check.cfg   | 12 ++++++++++++
 tla/check.tla   |  4 ++++
 tla/dag.tla     | 40 ++++++++++++++++++++++++++++++++++++++++
 tla/scratch.cfg | 10 ++++++++++
 tla/scratch.tla | 10 ++++++++++
 6 files changed, 79 insertions(+)
 create mode 100644 tla/check.cfg
 create mode 100644 tla/check.tla
 create mode 100644 tla/dag.tla
 create mode 100644 tla/scratch.cfg
 create mode 100644 tla/scratch.tla

diff --git a/.gitignore b/.gitignore
index 0ae2a00..1f4987d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,6 @@
 
 /target
 /Cargo.lock
+tla/*.old
+tla/*.out
+tla/states
\ No newline at end of file
diff --git a/tla/check.cfg b/tla/check.cfg
new file mode 100644
index 0000000..44c8423
--- /dev/null
+++ b/tla/check.cfg
@@ -0,0 +1,12 @@
+CONSTANT
+    Null = Null
+    NumNodes = 2
+
+SPECIFICATION
+    Spec
+
+\* PROPERTY
+\* Uncomment the previous line and add property names
+
+\* INVARIANT
+\* Uncomment the previous line and add invariant names
diff --git a/tla/check.tla b/tla/check.tla
new file mode 100644
index 0000000..4b32627
--- /dev/null
+++ b/tla/check.tla
@@ -0,0 +1,4 @@
+---- MODULE check ----
+EXTENDS TLC, dag
+
+====
\ No newline at end of file
diff --git a/tla/dag.tla b/tla/dag.tla
new file mode 100644
index 0000000..e49350f
--- /dev/null
+++ b/tla/dag.tla
@@ -0,0 +1,40 @@
+---- MODULE dag ----
+EXTENDS TLC, Integers
+CONSTANT
+    NumNodes, Null
+
+Nodes == 1..NumNodes
+
+VARIABLE graph, pc, tmp, edges
+
+vars == << graph, pc, tmp, edges >>
+
+Init == /\ graph = {}
+        /\ pc = "GetEdge"
+        /\ tmp = Null
+        /\ edges = {x \in (Nodes \X Nodes): x[1] # x[2]}
+
+GetEdge == /\ tmp = Null
+           /\ \/ /\ graph = {}
+                 /\  tmp' = Null
+              \/ tmp' = CHOOSE e \in edges: (e \notin graph /\ e[1] # e[2])
+           /\ edges' = edges \ {tmp'}
+           /\ pc' = "AddEdge"
+           /\ UNCHANGED graph
+
+AddEdge == /\ tmp # Null
+           /\ graph' = (graph \union {tmp})
+           /\ pc' = "Done"
+           /\ tmp' = Null
+           /\ UNCHANGED edges
+
+Terminating == /\ pc = "Done"
+               /\ UNCHANGED vars
+
+Next == \/ GetEdge \/ AddEdge
+        \/ Terminating
+
+Termination == <>(pc = "Done")
+
+Spec == Init /\ [][Next]_vars
+====
diff --git a/tla/scratch.cfg b/tla/scratch.cfg
new file mode 100644
index 0000000..754a5ea
--- /dev/null
+++ b/tla/scratch.cfg
@@ -0,0 +1,10 @@
+SPECIFICATION
+    Eval
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+\* PROPERTY
+\* Uncomment the previous line and add property names
+
+\* INVARIANT
+\* Uncomment the previous line and add invariant names
diff --git a/tla/scratch.tla b/tla/scratch.tla
new file mode 100644
index 0000000..0100d48
--- /dev/null
+++ b/tla/scratch.tla
@@ -0,0 +1,10 @@
+---- MODULE scratch ----
+EXTENDS TLC, Integers
+LOCAL INSTANCE Naturals
+LOCAL INSTANCE Sequences
+
+Boolean == {TRUE, FALSE}
+Node == 1..10
+GraphType == [Node \X Node -> Boolean]
+Eval == GraphType
+====
\ No newline at end of file