(* Protocole Stop and Wait *)

specification StopWait : noexit

type boolean is 
   sorts bool
   opns
      not : bool->bool
      and : bool,bool->bool
      or  : bool,bool->bool
endtype   

type natural is boolean
   sorts nat
   opns
      +  : nat,nat->nat
      -  : nat,nat->nat
      *  : nat,nat->nat
      <  : nat,nat->bool
      >  : nat,nat->bool
      <= : nat,nat->bool
      >= : nat,nat->bool
endtype

behaviour

  hide send,rec_ack,timeout,receive,snd_ack,yes,no in 

  (
    Sender[send,rec_ack,timeout](false)
    |[send,rec_ack]|
    Medium[send,rec_ack,receive,snd_ack]
  )
  |[receive,snd_ack]|
  Receiver[receive,snd_ack,yes,no]

where

  process Medium[send,rec_ack,receive,snd_ack]:noexit:=

     Slot[send,receive](1,6)
     |||
     Slot[snd_ack,rec_ack](1,6)

  where

    process Slot[in_slot,out_slot](dmin,dmax:time):noexit:=
      in_slot; delay(dmin,dmax) out_slot;
      Slot[in_slot,out_slot](dmin,dmax)
    endproc (* SLot *)

  endproc (* Medium *)


  process Sender[send,rec_ack,timeout](wait:bool):noexit:=
    [not(wait)]-> ( delay(1,3) send; Sender[send,rec_ack,timeout](true) )
    []
    [wait]-> (
      ( rec_ack; Sender[send,rec_ack,timeout](false) )
      []
      ( delay(19) timeout; send; Sender[send,rec_ack,timeout](true) )
    )
  endproc (* Sender *)


  process Receiver[receive,snd_ack,yes,no]:noexit:=
    receive; 
    delay(2,6) (
      ( no; Receiver[receive,snd_ack,yes,no] )
      []
      ( yes; snd_ack; Receiver[receive,snd_ack,yes,no] )
    )
  endproc (* Receiver *)


endspec (* StopWait *)