Adding Barrier synchronization and Auxiliary Variable examples (#177)

Signed-off-by: JarodDif <jarod.differdange@gmail.com>

Author: JarodDif

.ciignore

@@ -11,3 +11,6 @@ specifications/CCF
 specifications/azure-cosmos-tla
 specifications/microwave
 
+# Basic contribution only
+specifications/barriers
+specifications/locks_auxiliary_vars

specifications/barriers/Barrier.cfg

@@ -0,0 +1,4 @@
+CONSTANT N = 6
+SPECIFICATION Spec
+INVARIANT TypeOK 
+PROPERTY BarrierProperty

specifications/barriers/Barrier.tla

@@ -0,0 +1,40 @@
+------------------------------- MODULE Barrier --------------------------------
+EXTENDS Integers
+
+CONSTANTS 
+  N
+
+VARIABLES pc
+
+vars == << pc >>
+
+ProcSet == (1..N)
+
+Init == 
+  /\ pc = [p \in ProcSet |-> "b0"]
+
+b0(self) ==
+  /\ pc[self] = "b0"
+  /\ pc' = [pc EXCEPT ![self] = "b1"]
+
+b1 ==
+  /\ \A p \in ProcSet : pc[p] = "b1"
+  /\ pc' = [p \in ProcSet |-> "b0"]
+
+Next == 
+  \/ \E p \in ProcSet : b0(p)
+  \/ b1
+
+Spec == Init /\ [][Next]_vars
+
+-------------------------------------------------------------------------------
+
+TypeOK ==
+  /\ pc \in [ProcSet -> {"b0", "b1"}]
+
+\* A process cannot leave the barrier if there are still other processes
+\* that need to enter it
+BarrierProperty ==
+  /\ [][\A p,q \in ProcSet : pc[p] = "b0" /\ pc[q] = "b1" => pc'[q] = "b1"]_vars
+
+===============================================================================

specifications/barriers/Barriers.cfg

@@ -0,0 +1,4 @@
+CONSTANT N = 6
+SPECIFICATION Spec
+INVARIANTS TypeOK LockInv Inv FlushInv
+PROPERTY BSpec