---------------------------- MODULE ShiftRegister ---------------------------
EXTENDS PCCallReturn, Naturals
-----------------------------------------------------------------------------
CONSTANT N
ASSUME (N \in Nat) /\ (N > 0)

Empty  ==  CHOOSE v : v \notin Input
-----------------------------------------------------------------------------
VARIABLE sr

SRInit  ==  /\ CRInit 
            /\ sr = [i \in 1..N |-> Empty]

SRTypeOK  ==  /\ CRTypeOK
              /\ sr \in [1..N -> Input \cup {Empty}]
-----------------------------------------------------------------------------
SRCall(v)  ==  /\ sr[1] = Empty
               /\ Call(v)
               /\ sr' = [sr EXCEPT ![1] = v]

SRReturn  ==  /\ sr[N] # Empty
              /\ Return(sr[N])
              /\ sr' = [sr EXCEPT ![N] = Empty]

SRShift(i)  ==  /\ sr[i]   # Empty
                /\ sr[i+1] = Empty
                /\ sr'= [sr EXCEPT ![i] = Empty, ![i+1] = sr[i]]
                /\ UNCHANGED iFace

SRNext  ==  \/ \E v \in Input : SRCall(v)
            \/ \E i \in 1..(N-1) : SRShift(i)
            \/ SRReturn
-----------------------------------------------------------------------------
SRSpec  ==  SRInit  /\  [][SRNext]_<<sr, iFace>>

THEOREM SRSpec => []SRTypeOK
=============================================================================