specification feature_interaction_system[u, n, a]:noexit

  
   (* written by Bernard Stepien, October 1993 *)

   (* NOTE: this specification uses Extended Data types that are
      not part of the LOTOS language. Consequently the pao2ao
      translator is required to translate it into standard LOTOS
   *)

   library Boolean, NaturalNumber , Set endlib 

 enumtype phone_number is 
   { num1, num2, num3, num4, num5 }
 endtype 

 enumtype primitives is 
   { 
     offhook, conreq, ring, answer, connect, talk, pwd, dial, tone,
     star, pound, voice_mail_answer, busy, flash_hook,
     conreq_calling_card, hang_up, discon_req,
     activate_call_forward,
     play_announce_pwd, deliver_messages, 
     play_announce_star_pound, play_announce_management,
     play_announce_new_number, good_bye, detect_forward,
     unconditional_refusal
   }
    subclass

      user_actions  { offhook, answer, talk, pwd, dial, star, pound, flash_hook,
                       hang_up, activate_call_forward }
      network_actions  { tone, conreq, ring, connect, busy, detect_forward, unconditional_refusal }
      voice_mail_actions  { voice_mail_answer, play_announce_pwd, 
                             deliver_messages, play_announce_star_pound,
                             play_announce_management,
                             play_announce_new_number,
                             good_bye
                           }
 endtype 

 enumtype service is
   {
     three_way_calling, call_waiting, call_forward, originate_screening }
 endtype

 enumtype active_service is
   { no_active_service, forward_calls }
 endtype

 settype subscrib_services is service
    elements service
    values
      no_services = { }
 endtype

 settype screen_list is phone_number
   elements phone_number
   values
    no_screen_list = { }
 endtype

 behavior 


 ( 
     phone[u, n](num1, { three_way_calling, call_waiting,originate_screening }, no_active_service , num1, { num4 } )
   |||
     phone[u, n](num2, { call_forward }, no_active_service ,num4, no_screen_list)
   |||
     voice_mail[u, n](num3)
   |||
     phone[u, n](num4,no_services, no_active_service,num4, no_screen_list)
   |||
     phone[u, n](num5,no_services, no_active_service,num5, no_screen_list)
 ) 

|[n]|

 network[n,a]

 where 
 

 process phone[u, n](NUMBER:phone_number,SUBS_SERV:subscrib_services,ACTIV_SERV:active_service,FWD_NUMBER:phone_number, SCR_LIST:screen_list):noexit:=

    call_initiator_phone[u, n](NUMBER,SUBS_SERV,ACTIV_SERV,FWD_NUMBER, SCR_LIST)

    []

    call_responder_phone[u, n](NUMBER,SUBS_SERV,ACTIV_SERV,FWD_NUMBER, SCR_LIST)

 endproc

 process call_initiator_phone[u, n]
         (NUMBER:phone_number,SUBS_SERV:subscrib_services,ACTIV_SERV:active_service,FWD_NUMBER:phone_number, SCR_LIST:screen_list):noexit:=

   u ! NUMBER ! offhook
   ; n ! NUMBER ! tone
   ;
   (
   (
    (
          n ! NUMBER ? CALLED_NUMBER:phone_number ! conreq ! SCR_LIST
     ;    
        (
          complete_connection[u,n](NUMBER,SUBS_SERV)
          []
          n ! NUMBER ! CALLED_NUMBER ! unconditional_refusal 
          ; phone[u,n](NUMBER,SUBS_SERV,forward_calls,FWD_NUMBER,SCR_LIST)
        )

    []
          calling_card_call[u,n](NUMBER, SUBS_SERV)
    )
   []
    (
       u ! NUMBER ! activate_call_forward ? FWD_NUMBER: phone_number
     ; phone[u,n](NUMBER,SUBS_SERV,forward_calls,FWD_NUMBER,SCR_LIST)
    )
    )
    |||
     busy_ring[u,n](NUMBER,SUBS_SERV)
   )

  endproc

   process call_responder_phone[u, n]
         (NUMBER:phone_number,SUBS_SERV:subscrib_services,ACTIV_SERV:active_service,FWD_NUMBER:phone_number, SCR_LIST:screen_list):noexit:=
  
   n ! NUMBER ! ring
   ;
   (
     (
       (
         [ ACTIV_SERV ne forward_calls ]->
              u ! NUMBER ! answer
         ;    n ! NUMBER ! connect
         ;    u ! NUMBER ! talk
         ;    stop
       )

      []

       call_forward[u,n](NUMBER,SUBS_SERV,FWD_NUMBER,SCR_LIST)
     )
    |||
     busy_ring[u,n](NUMBER,SUBS_SERV)
   )

 endproc

 process user_events[u,n](NUMBER:phone_number, SUBS_SERV:subscrib_services):noexit:=

       u ! NUMBER ! talk 
     ; user_events[u,n](NUMBER, SUBS_SERV)

    []

       u ! NUMBER ! star  
     ; n ! NUMBER ! star  
     ; user_events[u,n](NUMBER, SUBS_SERV)

    []

       u ! NUMBER ! pound  
     ; n ! NUMBER ! pound  
     ; user_events[u,n](NUMBER, SUBS_SERV)

    []

       u ! NUMBER ! pwd  
     ; n ! NUMBER ! pwd  
     ; user_events[u,n](NUMBER, SUBS_SERV)

    []

      (* after the network played a dial a new number announcement *)
       n ! NUMBER ? NEW_NUMBER:phone_number ! conreq  
     ; complete_connection[u,n](NUMBER, SUBS_SERV)

    []

       u ! NUMBER ! hang_up 
     ; n ! NUMBER ! discon_req 
     ; stop

 endproc
 
 process calling_card_call[u,n](NUMBER:phone_number, SUBS_SERV:subscrib_services):noexit:=

     n  ! NUMBER ? CALLED_NUMBER:phone_number ! conreq_calling_card ? CHARGE_NUMBER:phone_number
   ; complete_connection[u,n](NUMBER, SUBS_SERV)

 endproc

  process complete_connection[u,n](NUMBER:phone_number,SUBS_SERV:subscrib_services):noexit:=

       n ! NUMBER ! connect
     ;
     (
	   user_events[u,n](NUMBER,SUBS_SERV)
   	|||
   	   features[u,n](NUMBER,SUBS_SERV)    
     )

  endproc

  process features[u, n](NUMBER:phone_number,SUBS_SERV:subscrib_services):noexit:=

      call_waiting[u,n](NUMBER,SUBS_SERV)

     |||

      three_way_calling[u,n](NUMBER,SUBS_SERV)

  endproc

  process call_waiting[u,n](NUMBER:phone_number,SUBS_SERV:subscrib_services):noexit:=

    [ call_waiting IsIn SUBS_SERV] ->
         n ! NUMBER ! ring
       ; u ! NUMBER ! flash_hook
       ; n ! NUMBER ! connect
       ;
        ( user_events[u,n](NUMBER,SUBS_SERV)
          [>
            (   n ! discon_req
	      ; stop
            )
	)

  endproc

  process three_way_calling[u,n](NUMBER:phone_number,SUBS_SERV:subscrib_services):noexit:=

    [ three_way_calling IsIn SUBS_SERV] ->
        u ! NUMBER ! flash_hook
      ; u ! NUMBER ! dial ? C:phone_number
      ; n ! NUMBER ! conreq ! C
      ; n ! NUMBER ! connect
      ;
	( user_events[u,n](NUMBER,SUBS_SERV)
          [>
            (   n ! discon_req
	      ; stop
            )
	)

  endproc

  process call_forward[u,n](NUMBER:phone_number,SUBS_SERV:subscrib_services,FWD_NUMBER:phone_number,SCR_LIST:screen_list):noexit:=

    [ call_forward IsIn SUBS_SERV] ->
	 n ! NUMBER ! detect_forward ! FWD_NUMBER
       ; phone[u,n](NUMBER,SUBS_SERV,forward_calls,FWD_NUMBER,SCR_LIST)

  endproc

  process busy_ring[u,n](NUMBER:phone_number,SUBS_SERV:subscrib_services):noexit:=

    [ call_waiting NotIn SUBS_SERV] ->
	 n ! NUMBER ! busy
       ; u ! NUMBER ! hang_up
       ; n ! NUMBER ! discon_req
       ; stop

  endproc

  process voice_mail[v, n](NUMBER:phone_number):noexit:=

        n ! NUMBER ! ring
   ;    v ! NUMBER ! voice_mail_answer
   ;    n ! NUMBER ! connect
   ;    v ! NUMBER ! play_announce_pwd
   ;    n ! NUMBER ! pwd
   ;    v ! NUMBER ! deliver_messages
   ;    v ! NUMBER ! play_announce_star_pound
   ;
   (
        n ! NUMBER ! star
     ;  v ! Number ! good_bye
     ;  stop
    []
        n ! NUMBER ! pound
     ;  v ! NUMBER ! play_announce_management
     ;  stop
   )

 endproc


 process network[n,a]:noexit:= 

   n ? CALLER:phone_number ! tone
   ;  
   (
     connection_handler[n,a](CALLER)
     |||
     network[n,a]
   )

 endproc

 process connection_handler[n,a](CALLER:phone_number):noexit:=
  
   n ! CALLER ? CALLED:phone_number ! conreq ? SCR_LIST:screen_list
   ;  
   (
     [ CALLED NotIn SCR_LIST ] ->
     n ! CALLED ! ring
     ;
     (
         n ! CALLED ! connect
       ; n ! CALLER ! connect
       ; relay_user_events[n](CALLER,CALLED)

      []

	 n ! CALLED ! detect_forward ? FWD_NUMBER: phone_number
       ; n ! FWD_NUMBER ! ring
       ; n ! FWD_NUMBER ! connect
       ; n ! CALLER ! connect
       ; relay_user_events[n](CALLER,FWD_NUMBER)
     )   	 
   []
    [ CALLED IsIn SCR_LIST ] ->
      n ! CALLER ! CALLED ! unconditional_refusal
      ; stop
   []
      n ! CALLED ! busy
      ; stop
   )

 []

   n ! CALLER ? CALLED_NUMBER:phone_number ! conreq_calling_card ? CHARGE_NUMBER:phone_number
   ; network_complete_connection[n,a](CALLER, CALLED_NUMBER)
 
 endproc

 process relay_user_events[n](CALLER,CALLED:phone_number):noexit:=

   n ! CALLER ? EVENT:primitives [ is_user_actions(EVENT) ]
   ; n ! CALLED ! EVENT 
   ; relay_user_events[n](CALLER,CALLED)

  []

   n ! CALLER ! discon_req ; stop

 endproc

  process network_complete_connection[n,a](CALLER,CALLED:phone_number):noexit:=

          n ! CALLED ! ring
     ;    n ! CALLED ! connect
     ;    n ! CALLER ! connect
     ;
     (
            relay_user_events[n](CALLER,CALLED)
       ||| 
            calling_card_intercept[n,a](CALLER)
     )

  endproc

  process calling_card_intercept[n,a](CALLER:phone_number):noexit:=

           n ! CALLER ! pound
        ;  a ! CALLER ! play_announce_new_number 
        ;  n ! CALLER ? NEW_NUMBER:phone_number ! conreq
        ;  network_complete_connection[n,a](CALLER,NEW_NUMBER)

  endproc

 process tester[u, n]:noexit:= 

        u ! num1 ! offhook
   ;    n ! num2 ! num1 ! conreq
   ;    n ! num2 ! ring
   ;    u ! num2 ! answer
   ;    n ! num2 ! connect
   ;    n ! num1 ! connect
   ;    u ! num1 ! talk
   ;    u ! num2 ! talk
   ;    stop
 [] 
        u ! num1 ! offhook
   ;    n ! num2 ! num1 ! conreq
   ;    n ! num2 ! ring
   ;    n ! num2 ! connect
   ;    n ! num1 ! connect
   ;    u ! num1 ! talk
   ;    u ! num2 ! talk
   ;    stop

 endproc

 endspec