----------------------------- MODULE Channel -----------------------------

EXTENDS Naturals
CONSTANT Data
VARIABLES chan

TypeInvariant == chan \in [val: Data, rdy: {0,1}, ack: {0,1}]

InitChannel == /\ TypeInvariant
        /\ chan.ack = chan.ack

Send(d) == /\ chan.ack = chan.ack
           /\ chan' = [chan EXCEPT !.val = d, !.rdy = 1 - @]

Rcv == /\ chan.rdy # chan.ack
       /\ chan' = [chan EXCEPT !.ack = 1-@]

NextChannel == (\E d \in Data: Send(d)) \/ Rcv

Spec == InitChannel /\ [][NextChannel]_chan

THEOREM Spec => []TypeInvariant
=============================================================================