specification simple_phone_system[u,n]:noexit

   (* written by Bernard Stepien 14/11/95 *)

    type phone_number is

      sorts  phone_number
      opns
            num1, num2 :-> phone_number
    endtype

    type operations is
     sorts operation
     opns 
          off_hook, dial, tone, conreq, ring, 
          answer, connect, talk : -> operation
    endtype

    type states is
     sorts state
     opns
        idle, busy:-> state
    endype

  behavior

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

    |[ n ]|

     network[n]
   )
    ||
     constraint[u,n]
  


  where

    process phone[u,n] (NUMBER:phone_number):noexit:=
                             
        u ! off_hook ! 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 constraint[u,n]:noexit:=

        u ? S:operation ? NUMBER:phone_number  (* add predicate on operations *)
        ;   constraint[u,n]
      []
        n ? S:operation ? NUMBER:phone_number  (* add predicate on operations *)
        ;   constraint[u,n]
      []
        n ? S:operation ? NUMBER:phone_number ? CALLED_NUMBER:phone_number 
                          (* add predicate on operations *)
        ; constraint[u,n]

    endproc

endspec