------------------------ MODULE ListProducerConsumer ------------------------ 
EXTENDS PCCallReturn
-----------------------------------------------------------------------------
CONSTANT CellAddress

Cell == [val : Input, next : CellAddress]
-----------------------------------------------------------------------------
VARIABLE mem,  freeCells, nxtC,  nxtR

ListPCTypeOK == /\ CRTypeOK
                /\ mem \in [CellAddress -> Cell]
                /\ nxtC \in CellAddress
                /\ nxtR \in CellAddress
                /\ freeCells \subseteq CellAddress

ListPCInit == /\ CRInit
              /\ mem \in [CellAddress -> Cell]
              /\ nxtC \in CellAddress
              /\ nxtR = nxtC 
              /\ freeCells = CellAddress \ {nxtR}

ListPCCall(v) == \E fc \in freeCells :
                   /\ Call(v)
                   /\ nxtC' = fc
                   /\ mem' = [mem EXCEPT ![nxtC] = [val  |-> v,
                                                    next |-> fc]]
                   /\ freeCells' = freeCells \ {fc}
                   /\ UNCHANGED nxtR                      

ListPCReturn == /\ nxtR # nxtC
                /\ Return(RtnVal(mem[nxtR].val))
                /\ nxtR' = mem[nxtR].next
                /\ freeCells' = freeCells \cup {nxtR}
                /\ UNCHANGED <<nxtC, mem>>

ListPCNext == (\E v \in Input : ListPCCall(v)) \/ ListPCReturn
-----------------------------------------------------------------------------
ListPCSpec == ListPCInit /\ [][ListPCNext]_<<mem, freeCells, nxtC, nxtR, iFace>> 

THEOREM ListPCSpec => []ListPCTypeOK
=============================================================================