TLA+ Specification

.gitignore

@@ -4,3 +4,6 @@
 
 /target
 /Cargo.lock
+tla/*.old
+tla/*.out
+tla/states

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

tla/check.tla

@@ -0,0 +1,4 @@
+---- MODULE check ----
+EXTENDS TLC, dag
+
+====

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

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

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