(* Exemple academique dont on ne *)
(* peut realiser l'accessibilite *)
(* que a la volee.               *)

specification On_The_Fly : 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 a, b in

  P1[a](1)
  |[a]|
  P2[a,b](0)
  
where

  process P1[a](per:time) : noexit :=
    delay(per) a; P1[a](per)
  endproc
  
  process P2[a,b](n:nat) : noexit :=
    ( a; P2[a,b](n+1) )
    []
    [n>0] -> ( b; P2[a,b](n-1) )
  endproc
  
endspec