MODULE channel(input)

VAR
  output:       boolean;
  loss:         boolean;

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


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;


MODULE main

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

LTLSPEC
  (sender.produce &
   G F !ack.loss & 
   G F !msg.loss &
   G (!receiver.waiting -> F receiver.consume)) ->
  F receiver.consume

LTLSPEC
  (G F !ack.loss & 
   G F !msg.loss &
   G (!receiver.waiting -> F receiver.consume) &
   G (!sender.sending -> F sender.produce)) ->
  G F receiver.consume