Unify TLC models for locks_auxiliary_vars

Author: JarodDif

specifications/locks_auxiliary_vars/LockHS.cfg

@@ -1,3 +1,3 @@
 SPECIFICATION SpecHS
 INVARIANTS TypeOKHS InvHS LockInv
-PROPERTIES Spec
+PROPERTIES Spec PSpec

specifications/locks_auxiliary_vars/LockHS.tla

@@ -26,6 +26,8 @@ NoHistoryChange(A) == A /\ UNCHANGED h_turn
 VARIABLE s
 INSTANCE Stuttering
 
+\* This theorem justifies the validity of the introduced stuttering variable
+\* in definition l1HS
 THEOREM StutterConstantCondition(1..2, 1, LAMBDA j : j-1)
 <1>. DEFINE InvD(S) == {sig \in (1..2) \ S : sig-1 \in S}
             R[n \in Nat] == IF n = 0 THEN {1}
@@ -125,6 +127,7 @@ P == INSTANCE Peterson WITH
       pc <- [p \in ProcSet |-> pc_translation(p, pc[p], s)],
       c <- [p \in ProcSet |-> c_translation(pc_translation(p, pc[p], s))],
       turn <- h_turn
+PSpec == P!Spec
 
 -------------------------------------------------------------------------------
 

specifications/locks_auxiliary_vars/MCLockHS.cfg

@@ -1,2 +1,3 @@
 SPECIFICATION Spec
-INVARIANTS TypeOK Inv
+INVARIANTS TypeOK Inv
+PROPERTY LSpec

specifications/locks_auxiliary_vars/MCLockHS.tla

@@ -106,6 +106,7 @@ lock_translation == IF \E p \in ProcSet : pc[p] \in {"cs", "a4"} THEN 0 ELSE 1
 L == INSTANCE Lock
      WITH pc <- [p \in ProcSet |-> pc_translation(pc[p])], 
      lock <- lock_translation
+LSpec == L!Spec
 
 -------------------------------------------------------------------------------