example

.gitignore

@@ -1,2 +1,10 @@
 /states
 /temporary.cfg
+
+/examples/bool.tla
+/examples/init.tla
+/examples/int.tla
+/examples/seq.tla
+/examples/set.tla
+/examples/struct.tla
+/examples/temp.tla

Taskfile.yaml

@@ -12,6 +12,7 @@ tasks:
     cmds:
       - python3 -m pip install tlacli
   test:
+    desc: run all tests
     deps:
       - install-tlacli
     cmds:
@@ -20,3 +21,25 @@ tasks:
       - tlacli check simple-tla/set.tla --invariant IsCorrect
       - tlacli check simple-tla/bool.tla --invariant IsCorrect
       - tlacli check simple-tla/int.tla --invariant IsCorrect
+
+  link:
+    desc: create symlinks for simple-tla in examples/
+    silent: true
+    status:
+      - test -e ./examples/init.tla
+    cmds:
+      - ln -s $PWD/simple-tla/bool.tla ./examples/
+      - ln -s $PWD/simple-tla/init.tla ./examples/
+      - ln -s $PWD/simple-tla/int.tla ./examples/
+      - ln -s $PWD/simple-tla/seq.tla ./examples/
+      - ln -s $PWD/simple-tla/set.tla ./examples/
+      - ln -s $PWD/simple-tla/struct.tla ./examples/
+      - ln -s $PWD/simple-tla/temp.tla ./examples/
+
+  run:
+    desc: run an example
+    deps:
+      - install-tlacli
+      - link
+    cmds:
+      - tlacli check {{.CLI_ARGS}}

examples/threads.tla

@@ -0,0 +1,46 @@
+---- MODULE threads ----
+EXTENDS TLC, Sequences, Integers, init
+
+NumThreads == 2
+Threads == seq!range(1, NumThreads)
+
+VARIABLES counter, pc
+
+AllDone ==
+  seq!all(Threads, LAMBDA t: pc[t] = "Done")
+
+Correct ==
+    bool!implies(AllDone, int!eq(counter, NumThreads))
+
+
+vars == << counter, pc >>
+
+ProcSet == (Threads)
+
+Init ==
+    /\ int!is_zero(counter)
+    /\ pc = [self \in ProcSet |-> "IncCounter"]
+
+IncCounter(self) ==
+    /\ pc[self] = "IncCounter"
+    /\ counter' = int!inc(counter)
+    /\ pc' = [pc EXCEPT ![self] = "Done"]
+
+thread(self) == IncCounter(self)
+
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating ==
+    /\ seq!all(ProcSet, LAMBDA self: pc[self] = "Done")
+    /\ UNCHANGED vars
+
+Next ==
+    \/ seq!any(Threads, thread)
+    \/ Terminating
+
+Spec == Init /\ [][Next]_vars
+
+Termination == temp!eventually(
+    seq!all(ProcSet, LAMBDA self: pc[self] = "Done")
+)
+
+====

simple-tla/init.tla

@@ -1,19 +1,19 @@
----- MODULE int ----
+---- MODULE init ----
 
 \* boolean operations
-bool = INSTANCE bool
+bool == INSTANCE bool
 
 \* operations with integer numbers
-int = INSTANCE int
+int == INSTANCE int
 
 \* operations on ordered sequences of values (tuples)
-seq = INSTANCE seq
+seq == INSTANCE seq
 
 \* operations on onordered collections of unique values (sets)
-set = INSTANCE set
+set == INSTANCE set
 
 \* temporal logic operations (checking how values change over time)
-temp = INSTANCE temp
+temp == INSTANCE temp
 
-struct = INSTANCE struct
+struct == INSTANCE struct
 ====

simple-tla/int.tla

@@ -31,12 +31,24 @@ gt(a, b)  == a > b
 \* gte(int, int) -> bool
 gte(a, b) == a \geq b
 
+\* increment tha value
+inc(x) == x + 1
+
 \* check if value is integer (a whole number)
+\*
+\* is_int(any) -> bool
 is_int(x) == x \in Int
 
 \* check if value is a natural number (0, 1, 2, ...)
+\*
+\* is_nat(any) -> bool
 is_nat(x) == x \in Int /\ x > -1
 
+\* check if value is zero
+\*
+\* is_zero(int) -> bool
+is_zero(x) == x = 0
+
 \* check if a is less than b.
 \*
 \* lt(int, int) -> bool

simple-tla/temp.tla

@@ -23,6 +23,6 @@ unchanged(x) == x = x'
 \* Check if the value is not the same as in previous state.
 \*
 \* has_changed(any) -> bool
-has_changed(x) == x # x'
+has_changed(x) == UNCHANGED x
 
 ====