system bitalt;

type data = range 0 .. 1;

signal get(data);
signal put(data);
signal ack(boolean);
signal sdt(data, boolean);

/*
 * Connections
 *
 */

signalroute et(1)
  from env to transmitter
  with put;

signalroute tr(1) #unicast #lossy
  from transmitter to receiver
  with sdt;

signalroute rt(1) #unicast #lossy
  from receiver to transmitter 
  with ack;

signalroute re(1)
  from receiver to env
  with get;

/*
 * Transmitter
 *
 */

process transmitter(1);

var t clock;
var b boolean;
var c boolean;
var m data;

state start #start ;
    task b := false;
      nextstate idle;
endstate;
state idle;
  input put(m);
    output sdt(m, b) via {tr}0;
    set t := 0;
      nextstate busy;
endstate;
state busy;
  input ack(c);
      nextstate q8;
  when t = 1;
    output sdt(m, b) via {tr}0;
    set t := 0;
      nextstate busy;
endstate;
state q8 #unstable ;
  provided c = b;
    task b := not b;
    reset t;
      nextstate idle;
  provided c <> b;
      nextstate busy;
endstate;
endprocess;

/*
 * Receiver
 *
 */

process receiver(1);

var b boolean;
var c boolean;
var m data;

state start #start ;
    task b := false;
      nextstate idle;
endstate;
state idle;
  input sdt(m, c);
    if b = c then
      output ack(b) via {rt}0;
      output get(m);
      task b := not b;
    else
      output ack(not b) via {rt}0;
    endif 
    nextstate idle;
endstate;
endprocess;
endsystem;