|
--------------------------- MODULE SharedStorage --------------------------- |
|
EXTENDS Naturals, Sequences |
|
VARIABLES incoming, outgoing, statuses, shared_storage |
|
CONSTANT QLen, Id |
|
ASSUME (QLen \in Nat) /\ (QLen > 0) |
|
-------------------------------------------------------------- |
|
StoredObject == {"Vacant", "Occupied"} |
|
Statuses == {"Vacant", "Waiting", "Processed"} |
|
|
|
Init == /\ shared_storage = [p \in Id |-> "Vacant" ] |
|
/\ statuses = [p \in Id |-> "Vacant" ] |
|
/\ incoming = << >> |
|
/\ outgoing = << >> |
|
|
|
TypeInvariant == /\ incoming \in Seq(Id) |
|
/\ outgoing \in Seq(Id) |
|
/\ shared_storage \in [Id -> StoredObject] |
|
/\ statuses \in [Id -> Statuses] |
|
-------------------------------------------------------------- |
|
|
|
SendIncoming(id) == /\ Len(incoming) < QLen |
|
/\ incoming' = Append(incoming, id) |
|
/\ UNCHANGED <<statuses, outgoing, shared_storage>> |
|
|
|
ReceiveIncoming == LET new == Head(incoming) |
|
IN /\ (incoming # << >>) |
|
/\ incoming' = Tail(incoming) |
|
/\ statuses' = [statuses EXCEPT ![new] = "Waiting"] |
|
/\ shared_storage' = [shared_storage EXCEPT ![new] = "Occupied"] |
|
/\ UNCHANGED outgoing |
|
|
|
ProcessWaiting(id) == /\ statuses[id] = "Waiting" |
|
/\ Len(outgoing) < QLen |
|
/\ shared_storage[id] = "Occupied" |
|
/\ statuses' = [statuses EXCEPT ![id] = "Processed"] |
|
/\ outgoing' = Append(outgoing, id) |
|
/\ UNCHANGED <<incoming, shared_storage>> |
|
|
|
PruneObject(id) == /\ statuses[id] \in {"Waiting", "Processed"} |
|
/\ outgoing = << >> |
|
/\ shared_storage[id] = "Occupied" |
|
/\ shared_storage' = [shared_storage EXCEPT ![id] = "Vacant"] |
|
/\ statuses' = [statuses EXCEPT ![id] = "Vacant"] |
|
/\ UNCHANGED <<incoming, outgoing>> |
|
|
|
ReadOutgoing == /\ outgoing # << >> |
|
/\ shared_storage[Head(outgoing)] = "Occupied" |
|
/\ outgoing' = Tail(outgoing) |
|
/\ UNCHANGED <<incoming, statuses, shared_storage>> |
|
|
|
Next == \/ \E id \in Id : \/ SendIncoming(id) |
|
\/ ProcessWaiting(id) |
|
\/ PruneObject(id) |
|
\/ ReceiveIncoming |
|
\/ ReadOutgoing |
|
|
|
Spec == |
|
Init /\ [][Next]_<<incoming, outgoing, statuses, shared_storage>> |
|
-------------------------------------------------------------- |
|
THEOREM Spec => []TypeInvariant |
|
============================================================================= |
