MODULE main
VAR
   S : process sender(ack_chan.output);
   R : process receiver(msg_chan.output1,msg_chan.output2);
   msg_chan : process two-bit-chan(S.message1,S.message2);
   ack_chan : process one-bit-chan(R.ack);
ASSIGN
   init(S.message2) := 0;
   init(R.expected) := 0;
   init(R.ack)      := 1;
   init(msg_chan.output2) := 1;
   init(ack_chan.output) := 1;

LTLSPEC  G (S.st=sent & S.message1=1 -> msg_chan.output1=1)