specification state_phone[g] :exit

  (* written by bernard Stepien 05/02/90 *)

  Library NaturalNumber, Boolean endlib

   type state is NaturalNumber, Boolean

      sorts state

      opns

       ready, ready_user, ready_tone,
       ready_dial, ready_ring, ready_answer,
       ready_called_connect,
       ready_caller_connect,
       ready_voice,
       ready_caller_hang_up,
       ready_called_hang_up,
       ready_exit  : -> state

       h: state -> Nat
        _eq_ : state, state -> Bool

      eqns
         forall x, y: state

         ofsort Nat

           h(ready) = 0;
           h(ready_user) = Succ(h(ready));
           h(ready_tone) = Succ(h(ready_user));
           h(ready_dial) = Succ(h(ready_tone));
           h(ready_ring) = Succ(h(ready_dial));
           h(ready_answer) = Succ(h(ready_ring));
           h(ready_called_connect) = Succ(h(ready_answer));
           h(ready_caller_connect) = Succ(h(ready_called_connect));
           h(ready_voice) = Succ(h(ready_caller_connect)); 
           h(ready_caller_hang_up) = Succ(h(ready_voice)); 
           h(ready_called_hang_up) = Succ(h(ready_caller_hang_up)); 
           h(ready_exit) = Succ(h(ready_called_hang_up)); 

         ofsort Bool

           x eq y = h(x) eq h(y);

   endtype

   type signal is 

      sorts signal

      opns

         answer, voice, ring, connect, 
         dial, tone, hang_up: -> signal

   endtype

   type phone_number is

     sorts
          phone_number
     opns
          empty, one, two :  -> phone_number
   endtype


   behaviour
 
      phoning[g](ready_tone,empty,empty)

     where

      process phoning[g](S:state,Caller,Called:phone_number): exit :=

     
       [S eq ready_tone] -> g ? Caller: phone_number ! tone;
                         phoning[g](ready_dial,Caller,Called)
          []

       [S eq ready_dial] -> g ? Called: phone_number ! dial;
                         phoning[g](ready_ring,Caller,Called)
          []

       [S eq ready_ring] -> g ! Called ! ring;
                         phoning[g](ready_answer,Caller,Called)
          []

       [S eq ready_answer] -> g ! Called ! answer;
                         phoning[g](ready_called_connect,Caller,Called)
          []

       [S eq ready_called_connect] -> g ! Called ! connect;
                         phoning[g](ready_caller_connect,Caller,Called)
          []

       [S eq ready_caller_connect] -> g ! Caller ! connect;
                         phoning[g](ready_voice,Caller,Called)
          []

       [S eq ready_voice] -> g ! Called ! voice;
                         phoning[g](ready_voice,Caller,Called)
          []

       [S eq ready_voice] -> g ! Caller ! voice;
                         phoning[g](ready_called_hang_up,Caller,Called)
          []

       [S eq ready_called_hang_up] -> g ! Called ! hang_up;
                         phoning[g](ready_caller_hang_up,Caller,Called)
          []

       [S eq ready_caller_hang_up] -> g ! Caller ! hang_up;
                         phoning[g](ready_exit,Caller,Called)
          []

       [S eq ready_exit] -> exit

      endproc
     

endspec