MODULE channel(input)

VAR
  output:       boolean;
  loss:         boolean;

ASSIGN
  init(output) := 1;
  next(output) := case
    loss: output;
    1:    input;
  esac;

JUSTICE
  !loss


MODULE sender(ack)

VAR
  produce:      boolean;
  sending:      boolean;
  msg:          boolean;

ASSIGN
  produce := case
    !sending:   {0, 1};
    1:          0;
  esac;

  init(sending) := 0;
  next(sending) := case
    !sending:   produce;
    msg = ack:  0;
  esac;

  init(msg) := 1;
  next(msg) := case
    produce:    !msg;
    1:          msg;
  esac;


MODULE receiver(msg)

VAR
  consume:      boolean;
  waiting:      boolean;
  ack:          boolean;

ASSIGN
  consume := case
    !waiting:   {0, 1};
    1:          0;
  esac;

  init(waiting) := 1;
  next(waiting) := case
    !waiting:   consume;
    ack != msg: 0;
  esac;

  init(ack) := 1;
  next(ack) := case
    waiting:    msg;
    1:          ack;
  esac;

JUSTICE
  waiting | consume;


MODULE main

VAR
  msg      : channel(sender.msg);
  ack      : channel(receiver.ack);
  sender   : sender(ack.output);
  receiver : receiver(msg.output);

VAR
  produced : boolean;

ASSIGN
  init(produced) := sender.produce;
  next(produced) := produced | sender.produce;

SPEC
  AG (sender.msg = 0 -> AF msg.output = 0)
SPEC
  AG (sender.msg = 1 -> AF msg.output = 1)

SPEC
  AG (sender.produce -> AF receiver.consume)