specification test[u_to_p, p_to_u, p_to_n, n_to_p]:noexit

type Msgs is 
  sorts Msgs
  opns
      offHook, tone, dial, connect, ring, talk, 
	  onHook, answer, conreq:-> Msgs
endtype

type Number is
  sorts number
  opns
     num_one, num_two :-> number
endtype

type User is
  sorts user
  opns
     user_one, user_two :-> user
endtype

type Switch is
  sorts switch
  opns
     switch_one :-> switch
endtype

behavior

	(
	   user[u_to_p, p_to_u](user_one, num_one) 
	  ||| 
           user[u_to_p, p_to_u](user_two, num_two)
        )
     |[u_to_p, p_to_u]|
	(
         phone[u_to_p, p_to_u, p_to_n, n_to_p](num_one, switch_one) 
	  ||| 
	   phone[u_to_p, p_to_u, p_to_n, n_to_p](num_two, switch_one)
        )
     |[p_to_n, n_to_p]|
	switch[p_to_n, n_to_p](switch_one)
where

   process user[u_to_p, p_to_u](U:user, N:number):noexit:=

	u_to_p ! U ! N ! offHook ; user[u_to_p, p_to_u](U, N)
	[]
	u_to_p ! U ! N ! dial ! num_one ; user[u_to_p, p_to_u](U, N)
	[]
	u_to_p ! U ! N ! dial ! num_two ; user[u_to_p, p_to_u](U, N)
	[]
	u_to_p ! U ! N ! onHook ; user[u_to_p, p_to_u](U, N)
	[]
	u_to_p ! U ! N ! talk ; user[u_to_p, p_to_u](U, N)
   endproc

   process phone[u_to_p, p_to_u, p_to_n, n_to_p](N:number, S:switch):noexit:=
	
   	u_to_p ? U:user ! N ! offHook ;
	(
    	  n_to_p ! S ! N ! tone ;
    	  u_to_p ! U ! N ! dial ? CalledNumber:number ;
	  p_to_n ! N ! S ! conreq ! CalledNumber ;
	  n_to_p ! S ! N ! connect ;
	  u_to_p ! U ! N ! talk ;
	  stop     
         [> u_to_p ! U ! N ! onHook ; stop
      )
   []

   	n_to_p ! S ! N ! ring ;
   	u_to_p ? U:user ! N ! offHook ;
      (
	  p_to_n ! N ! S ! answer ;
	  n_to_p ! S ! N ! connect ;
   	  u_to_p ! U ! N ! talk ;
   	  stop
          [> u_to_p ! U ! N ! onHook ; stop
      )
    endproc

    process switch[p_to_n, n_to_p](S:switch):noexit:=

	n_to_p ! S ? N:number ! tone ;
	p_to_n ! N ! S ! conreq ? CalledNumber:number ;
	n_to_p ! S ! CalledNumber ! ring ;
	p_to_n ! CalledNumber ! S ! answer ;
	n_to_p ! S ! CalledNumber ! connect ;
	n_to_p ! S ! N ! connect ;
	stop
    endproc

endspec