---------------------- MODULE TwoPhase ---------------------- 
EXTENDS CallReturn, Naturals
VARIABLES c, r
-------------------------------------------------------------
TPInit ==  /\ CRInit 
           /\ c = 0
           /\ r = 0

TPCall == /\ c = r
          /\ Call
          /\ c' = (c + 1) % 2
          /\ r' = r

TPReturn == /\ c # r
            /\ Return
            /\ r' = (r + 1) % 2
            /\ c' = c

TPNext == TPCall \/ TPReturn 
-------------------------------------------------------------
TPSpec == TPInit /\ [][TPNext]_<<iFace, c, r>>

TPInvariant == /\ CRInvariant
               /\ c \in {0,1}
               /\ r \in {0,1}

THEOREM TPSpec => []TPInvariant
-------------------------------------------------------------
Bar == INSTANCE Alternation WITH x <- (c + r) % 2
BarAltSpec == Bar!AltSpec
THEOREM TPSpec => Bar!AltSpec
=============================================================