DistributedLockBroken.tla

----------------------- MODULE DistributedLockBroken -----------------------
EXTENDS Naturals, Sequences
VARIABLES clients, lock_checked, data_written
CONSTANT ClientId
----------------------------------------------------------------------------

LockStatus == {"NotAcquired", "Acquired"}

Init == /\ clients = [client \in ClientId |-> "NotAcquired" ]
        /\ lock_checked = [client \in ClientId |-> FALSE ]
        /\ data_written = [client \in ClientId |-> <<>> ]

TypeInvariant == /\ clients \in [ClientId -> LockStatus] 
                 /\ lock_checked = [ClientId -> BOOLEAN]
                 /\ data_written = [ClientId -> Seq(BOOLEAN \X BOOLEAN)]

Coherence == \A c \in ClientId: 
                  data_written[c] #<<>> => 
                      (data_written[c][1] => data_written[c][2])

-----------------------------------------------------------------------------

AcquireLock(id) == /\ \A c \in ClientId: clients[c] = "NotAcquired"
                   /\ clients' = [clients EXCEPT ![id] = "Acquired"]
                   /\ UNCHANGED <<lock_checked, data_written>>

ExpireLock == /\ \E c \in ClientId: /\ clients[c] = "Acquired"
                                    /\ clients' = [clients EXCEPT ![c] = "NotAcquired"]
              /\ UNCHANGED <<lock_checked, data_written>>
                               
CheckLock(id) == /\ clients[id] = "Acquired"
                 /\ lock_checked' = [lock_checked EXCEPT ![id] = TRUE]
                 /\ UNCHANGED <<clients, data_written>>

WriteData(id) == /\ lock_checked[id] = TRUE
                 /\ data_written' = [data_written EXCEPT ![id] = <<TRUE, clients[id] # "NotAcquired">>]        
                 /\ lock_checked' = [lock_checked EXCEPT ![id] = FALSE]
                 /\ UNCHANGED <<clients>>
                 
Next == \/ \E id \in ClientId: \/ AcquireLock(id)
                               \/ CheckLock(id)
                               \/ WriteData(id)
        \/ ExpireLock

Spec == 
  Init /\ [][Next]_<<clients, lock_checked, data_written>>
  
-----------------------------------------------------------------------------
THEOREM Spec => [](TypeInvariant /\ Coherence)

=============================================================================