semaphore.tla

----------------------------- MODULE Semaphore -----------------------------
EXTENDS Naturals, Sequences
VARIABLES level, clients, queue
CONSTANT UpperBound, ClientId
----------------------------------------------------------------------------

ClientStatus == {"Acquired", "Released", "Waiting", "Cancelled"}

Init == /\ level = UpperBound
        /\ clients = [fut \in ClientId |-> "Released" ]
        /\ queue = << >>

TypeInvariant == /\ level >= 0
                 /\ clients \in [ClientId -> ClientStatus] 
                 /\ queue \in Seq(ClientId)
                 /\ level =< UpperBound
                 /\ Len(queue) =< UpperBound
-----------------------------------------------------------------------------

Acquire(id) == /\ Len(queue) = 0
               /\ clients[id] = "Released"
               /\ level > 0
               /\ level' = level - 1
               /\ clients' = [clients EXCEPT ![id] = "Acquired"]
               /\ UNCHANGED <<queue>>

Release(id) == /\ level' = level + 1
               /\ clients[id] = "Acquired"
               /\ clients' = [clients EXCEPT ![id] = "Released"]
               /\ UNCHANGED <<queue>>
                 
AddWaiter(id) == /\ level = 0
                 /\ clients[id] = "Released"
                 /\ clients' = [clients EXCEPT ![id] = "Waiting"]
                 /\ queue' = Append(queue, id)
                 /\ UNCHANGED <<level>>

CancelWaiter(id) == /\ clients[id] = "Waiting"
                    /\ clients' = [clients EXCEPT ![id] = "Cancelled"]
                    /\ UNCHANGED <<level, queue>>

AcquireNext == LET id == Head(queue)
                IN /\ Len(queue) > 0
                   /\ level > 0
                   /\ level' = level - 1
                   /\ clients[id] = "Waiting"
                   /\ queue' = Tail(queue)
                   /\ clients' = [clients EXCEPT ![id] = "Acquired"]

RemoveCancelled == LET id == Head(queue)
                   IN /\ Len(queue) > 0
                      /\ clients[id] = "Cancelled"
                      /\ queue' = Tail(queue)
                      /\ clients' = [clients EXCEPT ![id] = "Released"]
                      /\ UNCHANGED <<level>>
                                      
Next == \/ \E id \in ClientId: 
               \/ Acquire(id) 
               \/ AddWaiter(id)          
               \/ Release(id)
               \/ CancelWaiter(id)
        \/ AcquireNext 
        \/ RemoveCancelled 
        
Spec == 
  Init /\ [][Next]_<<level, clients, queue>>
-----------------------------------------------------------------------------
THEOREM Spec => []TypeInvariant
=============================================================================