specification simple_phone_system[u,n]:noexit

    (* written by Bernard Stepien, 05/02/90 *)

    type phone_number is

      sorts  phone_number
      opns   num1, num2 :-> phone_number
    endtype

    type primitives is

      sorts primitive
      opns  offhook, conreq, ring, answer, connect, talk:-> primitive
    endtype

  behavior

   
    ( phone[u,n](num1) ||| phone[u,n](num2) )

    |[n]|

     network[n]
   
  


  where

    process phone[u,n](NUMBER:phone_number):noexit:=
                             
       u ! offhook ! NUMBER ;   (* call initiator role *)
       n ! conreq   ! NUMBER ? CALLED_NUMBER:phone_number ;
       n ! connect  ! NUMBER ;
       u ! talk     ! NUMBER ;
       stop
     []
                          
       n ! ring ! NUMBER ;   (* call responder role *)
       u ! answer ! NUMBER ;
       n ! connect ! NUMBER ;
       u ! talk ! NUMBER ;
       stop

    endproc

    process network[n]:noexit:=

      n ! conreq ? CALLER:phone_number ? CALLED:phone_number ;
      n ! ring    ! CALLED ; 
      n ! connect ! CALLED ; 
      n ! connect ! CALLER ;
      stop

    endproc

    process tester[u,n]:noexit:=

       u ! offhook ! num1 ;        (* a good test sequence *)
       n ! conreq  ! num1 ! num2 ;
       n ! ring    ! num2 ;
       u ! answer  ! num2 ;
       n ! connect ! num2 ;
       n ! connect ! num1 ;
       u ! talk    ! num1 ;
       u ! talk    ! num2 ;
       stop

      []

       u ! offhook ! num1 ;         (* a bad test sequence *)
       n ! conreq  ! num1 ! num2 ;
       n ! ring    ! num2 ;
               (* answer action intentionally missing *)
       n ! connect ! num2 ;
       n ! connect ! num1 ;
       u ! talk    ! num1 ;
       u ! talk    ! num2 ;
       stop
       
    endproc

endspec