(* Example from Nicolas Berthier *)

node transceiver(enter_tx,
		 enter_rx,
		 exit_rx,
		 calibrate,
		 sleep,
		 wake_up,
		 irq_tx_done,
		 irq_on_packet,
		 irq_end_of_packet,
		 irq_end_of_calibration,
		 irq_fifo_threshold,
		 ok:bool) returns (red:bool)
let
  automaton
    state Idle
      do
	red = false;
      until enter_tx & ok then Tx
          | calibrate & ok then Calibrate
          | sleep & ok then Sleep
          | enter_rx & ok then Rx
    state Tx
      do
	red = true;
      until irq_tx_done then Idle
    state Calibrate
      do
	red = false;
      until irq_end_of_calibration then Idle
    state Sleep
      do
	red = false;
      until wake_up & ok then Idle
    state Rx
      do
	red = true;
      until irq_on_packet then Rx_Packet
          | exit_rx & ok then Idle
    state Rx_Packet
      do
	red = true;
      until irq_end_of_packet then Idle
  end
tel

node adc(adc_on,adc_off,ok:bool) returns (o:bool)
let
  automaton
    state Off
      do
	o = false;
      until adc_on & ok then On
    state On
      do
	o = true;
      until adc_off & ok then Off
  end
tel

node main(enter_tx,
	  enter_rx,
	  exit_rx,
	  calibrate,
	  sleep,
	  wake_up,
	  irq_tx_done,
	  irq_on_packet,
	  irq_end_of_packet,
	  irq_end_of_calibration,
	  irq_fifo_threshold,adc_on,adc_off:bool)
    returns (a_on,red:bool)

contract
    enforce (not (a_on & red)) with (ok_r,ok_a:bool)

let
  a_on = inlined adc(adc_on,adc_off,ok_a);
  red = inlined transceiver(enter_tx,
			    enter_rx,
			    exit_rx,
			    calibrate,
			    sleep,
			    wake_up,
			    irq_tx_done,
			    irq_on_packet,
			    irq_end_of_packet,
			    irq_end_of_calibration,
			    irq_fifo_threshold,ok_r);
tel