specification simple_phone_system[offhook, tone, conreq, connect_caller, talk, ring, answer, connect_called, busy]:noexit

  (* written by Bernard Stepien 21/09/90 *)

    type phone_number is

      sorts  phone_number
      opns   num1, num2, num3 :-> phone_number
    endtype

  behavior

   
    ( phone[offhook, tone, conreq, connect_caller, talk, ring,
             answer, connect_called, busy](num1) 
     ||| 
      phone[offhook, tone, conreq, connect_caller, talk, ring, 
             answer, connect_called, busy](num2) 
     |||
      phone[offhook, tone, conreq, connect_caller, talk, ring,
             answer, connect_called, busy](num3)
    )

    |[ conreq, connect_caller, ring, connect_called, busy]|

     network[conreq, ring, connect_called, connect_caller, busy]
   
  


  where

    process phone[offhook, tone, conreq, connect_caller, talk, ring, answer, connect_called , busy]
                                                           (NUMBER:phone_number):noexit:=
                             
        offhook  ! NUMBER    (* call initiator role *)
        ; tone ! NUMBER
        ;
        (
         conreq   ! NUMBER ? CALLED_NUMBER:phone_number ;
         connect_caller  ! NUMBER ;
         talk     ! NUMBER ;
         stop
        |||
         busy ! NUMBER ; stop
        )
     []
                          
        ring ! NUMBER    (* call responder role *)
        ;
        (
         answer ! NUMBER ;
         connect_called ! NUMBER ;
         talk ! NUMBER ;
         stop
        |||
         busy ! NUMBER ; stop
        )

    endproc

    process network[conreq, ring, connect_called, connect_caller,busy]:noexit:=

      conreq ? CALLER:phone_number ? CALLED:phone_number 
      ;
      (
      (
       ring    ! CALLED ; 
       connect_called ! CALLED ; 
       connect_caller ! CALLER ;
       stop
       []
       busy   ! CALLED ; stop
      )
      |||
       network[conreq, ring, connect_called, connect_caller, busy]
      )

    endproc

    process tester[offhook, conreq, connect_caller, talk, ring, answer, connect_called]:noexit:=

       offhook ! num1 ;        (* a good test sequence *)
       conreq  ! num1 ! num2 ;
       ring    ! num2 ;
       answer  ! num2 ;
       connect_called ! num2 ;
       connect_caller ! num1 ;
       talk    ! num1 ;
       talk    ! num2 ;
       stop

      []

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

endspec