specification feature_interaction_system[u, n, a]:noexit

  
   (* written by Bernard Stepien, October 1993 *)

   (* Note: this is an automatic translation of the 
      standard data type version, you may copy the ADTs
      in the former specification for better readability 
    *)

   library Set, NaturalNumber, Boolean endlib 

(* *** translating the following enumerated type **************************
 enumtype phone_number is 
   { num1, num2, num3, num4, num5}
 endtype 
 ******* in ACT ONE **************** *)
 type phone_number is NaturalNumber
    sorts phone_number
    opns 
      num1:  -> phone_number
      num2:  -> phone_number
      num3:  -> phone_number
      num4:  -> phone_number
      num5:  -> phone_number
      next: phone_number -> phone_number
      min_phone_number:  -> phone_number
      max_phone_number:  -> phone_number
      is_num1: phone_number -> Bool
      is_num2: phone_number -> Bool
      is_num3: phone_number -> Bool
      is_num4: phone_number -> Bool
      is_num5: phone_number -> Bool
      h: phone_number -> Nat
      _eq_: phone_number, phone_number -> Bool
      _ne_: phone_number, phone_number -> Bool
      _lt_: phone_number, phone_number -> Bool
      _le_: phone_number, phone_number -> Bool
      _gt_: phone_number, phone_number -> Bool
      _ge_: phone_number, phone_number -> Bool
    eqns 
          forall x, y:phone_number

        ofsort phone_number

         min_phone_number = num1; 

         max_phone_number = num5; 

         next(num1) = num2; 

         next(num2) = num3; 

         next(num3) = num4; 

         next(num4) = num5 ;

        ofsort Nat

         h(num1) = 0; 

         h(num2) = Succ(0); 

         h(num3) = Succ(Succ(0)); 

         h(num4) = Succ(Succ(Succ(0))); 

         h(num5) = Succ(Succ(Succ(Succ(0)))) ;

        ofsort Bool

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

         x ne y = h(x) ne h(y); 

         x lt y = h(x) lt h(y); 

         x le y = h(x) le h(y); 

         x gt y = h(x) gt h(y); 

         x ge y = h(x) ge h(y); 

         x eq num1 = true => 
         is_num1(x) = true; 

         x eq num2 = true => 
         is_num2(x) = true; 

         x eq num3 = true => 
         is_num3(x) = true; 

         x eq num4 = true => 
         is_num4(x) = true; 

         x eq num5 = true => 
         is_num5(x) = true; 

         x ne num1 = true => 
         is_num1(x) = false; 

         x ne num2 = true => 
         is_num2(x) = false; 

         x ne num3 = true => 
         is_num3(x) = false; 

         x ne num4 = true => 
         is_num4(x) = false; 

         x ne num5 = true => 
         is_num5(x) = false ;
 endtype 

(* *** translating the following enumerated type **************************
 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 { activate_call_forward, hang_up, flash_hook, pound, star, dial, pwd, talk, answer, offhook } 
      network_actions { unconditional_refusal, detect_forward, busy, connect, ring, conreq, tone } 
      voice_mail_actions { good_bye, play_announce_new_number, play_announce_management, play_announce_star_pound, deliver_messages, play_announce_pwd, voice_mail_answer } 
 endtype 
 ******* in ACT ONE **************** *)
 type primitives is NaturalNumber
    sorts primitives
    opns 
      offhook:  -> primitives
      conreq:  -> primitives
      ring:  -> primitives
      answer:  -> primitives
      connect:  -> primitives
      talk:  -> primitives
      pwd:  -> primitives
      dial:  -> primitives
      tone:  -> primitives
      star:  -> primitives
      pound:  -> primitives
      voice_mail_answer:  -> primitives
      busy:  -> primitives
      flash_hook:  -> primitives
      conreq_calling_card:  -> primitives
      hang_up:  -> primitives
      discon_req:  -> primitives
      activate_call_forward:  -> primitives
      play_announce_pwd:  -> primitives
      deliver_messages:  -> primitives
      play_announce_star_pound:  -> primitives
      play_announce_management:  -> primitives
      play_announce_new_number:  -> primitives
      good_bye:  -> primitives
      detect_forward:  -> primitives
      unconditional_refusal:  -> primitives
      next: primitives -> primitives
      min_primitives:  -> primitives
      max_primitives:  -> primitives
      is_offhook: primitives -> Bool
      is_conreq: primitives -> Bool
      is_ring: primitives -> Bool
      is_answer: primitives -> Bool
      is_connect: primitives -> Bool
      is_talk: primitives -> Bool
      is_pwd: primitives -> Bool
      is_dial: primitives -> Bool
      is_tone: primitives -> Bool
      is_star: primitives -> Bool
      is_pound: primitives -> Bool
      is_voice_mail_answer: primitives -> Bool
      is_busy: primitives -> Bool
      is_flash_hook: primitives -> Bool
      is_conreq_calling_card: primitives -> Bool
      is_hang_up: primitives -> Bool
      is_discon_req: primitives -> Bool
      is_activate_call_forward: primitives -> Bool
      is_play_announce_pwd: primitives -> Bool
      is_deliver_messages: primitives -> Bool
      is_play_announce_star_pound: primitives -> Bool
      is_play_announce_management: primitives -> Bool
      is_play_announce_new_number: primitives -> Bool
      is_good_bye: primitives -> Bool
      is_detect_forward: primitives -> Bool
      is_unconditional_refusal: primitives -> Bool
      is_user_actions: primitives -> Bool
      is_network_actions: primitives -> Bool
      is_voice_mail_actions: primitives -> Bool
      h: primitives -> Nat
      _eq_: primitives, primitives -> Bool
      _ne_: primitives, primitives -> Bool
      _lt_: primitives, primitives -> Bool
      _le_: primitives, primitives -> Bool
      _gt_: primitives, primitives -> Bool
      _ge_: primitives, primitives -> Bool
    eqns 
          forall x, y:primitives

        ofsort primitives

         min_primitives = offhook; 

         max_primitives = unconditional_refusal; 

         next(offhook) = conreq; 

         next(conreq) = ring; 

         next(ring) = answer; 

         next(answer) = connect; 

         next(connect) = talk; 

         next(talk) = pwd; 

         next(pwd) = dial; 

         next(dial) = tone; 

         next(tone) = star; 

         next(star) = pound; 

         next(pound) = voice_mail_answer; 

         next(voice_mail_answer) = busy; 

         next(busy) = flash_hook; 

         next(flash_hook) = conreq_calling_card; 

         next(conreq_calling_card) = hang_up; 

         next(hang_up) = discon_req; 

         next(discon_req) = activate_call_forward; 

         next(activate_call_forward) = play_announce_pwd; 

         next(play_announce_pwd) = deliver_messages; 

         next(deliver_messages) = play_announce_star_pound; 

         next(play_announce_star_pound) = play_announce_management; 

         next(play_announce_management) = play_announce_new_number; 

         next(play_announce_new_number) = good_bye; 

         next(good_bye) = detect_forward; 

         next(detect_forward) = unconditional_refusal ;

        ofsort Nat

         h(offhook) = 0; 

         h(conreq) = Succ(0); 

         h(ring) = Succ(Succ(0)); 

         h(answer) = Succ(Succ(Succ(0))); 

         h(connect) = Succ(Succ(Succ(Succ(0)))); 

         h(talk) = Succ(Succ(Succ(Succ(Succ(0))))); 

         h(pwd) = Succ(Succ(Succ(Succ(Succ(Succ(0)))))); 

         h(dial) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))); 

         h(tone) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))); 

         h(star) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))); 

         h(pound) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))); 

         h(voice_mail_answer) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))); 

         h(busy) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))); 

         h(flash_hook) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))); 

         h(conreq_calling_card) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))))); 

         h(hang_up) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))))); 

         h(discon_req) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))))))); 

         h(activate_call_forward) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))))))); 

         h(play_announce_pwd) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))))))))); 

         h(deliver_messages) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))))))))); 

         h(play_announce_star_pound) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))))))))))); 

         h(play_announce_management) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))))))))))); 

         h(play_announce_new_number) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))))))))))))); 

         h(good_bye) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))))))))))))); 

         h(detect_forward) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0)))))))))))))))))))))))); 

         h(unconditional_refusal) = Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(0))))))))))))))))))))))))) ;

        ofsort Bool

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

         x ne y = h(x) ne h(y); 

         x lt y = h(x) lt h(y); 

         x le y = h(x) le h(y); 

         x gt y = h(x) gt h(y); 

         x ge y = h(x) ge h(y); 

         x eq offhook = true => 
         is_offhook(x) = true; 

         x eq conreq = true => 
         is_conreq(x) = true; 

         x eq ring = true => 
         is_ring(x) = true; 

         x eq answer = true => 
         is_answer(x) = true; 

         x eq connect = true => 
         is_connect(x) = true; 

         x eq talk = true => 
         is_talk(x) = true; 

         x eq pwd = true => 
         is_pwd(x) = true; 

         x eq dial = true => 
         is_dial(x) = true; 

         x eq tone = true => 
         is_tone(x) = true; 

         x eq star = true => 
         is_star(x) = true; 

         x eq pound = true => 
         is_pound(x) = true; 

         x eq voice_mail_answer = true => 
         is_voice_mail_answer(x) = true; 

         x eq busy = true => 
         is_busy(x) = true; 

         x eq flash_hook = true => 
         is_flash_hook(x) = true; 

         x eq conreq_calling_card = true => 
         is_conreq_calling_card(x) = true; 

         x eq hang_up = true => 
         is_hang_up(x) = true; 

         x eq discon_req = true => 
         is_discon_req(x) = true; 

         x eq activate_call_forward = true => 
         is_activate_call_forward(x) = true; 

         x eq play_announce_pwd = true => 
         is_play_announce_pwd(x) = true; 

         x eq deliver_messages = true => 
         is_deliver_messages(x) = true; 

         x eq play_announce_star_pound = true => 
         is_play_announce_star_pound(x) = true; 

         x eq play_announce_management = true => 
         is_play_announce_management(x) = true; 

         x eq play_announce_new_number = true => 
         is_play_announce_new_number(x) = true; 

         x eq good_bye = true => 
         is_good_bye(x) = true; 

         x eq detect_forward = true => 
         is_detect_forward(x) = true; 

         x eq unconditional_refusal = true => 
         is_unconditional_refusal(x) = true; 

         x ne offhook = true => 
         is_offhook(x) = false; 

         x ne conreq = true => 
         is_conreq(x) = false; 

         x ne ring = true => 
         is_ring(x) = false; 

         x ne answer = true => 
         is_answer(x) = false; 

         x ne connect = true => 
         is_connect(x) = false; 

         x ne talk = true => 
         is_talk(x) = false; 

         x ne pwd = true => 
         is_pwd(x) = false; 

         x ne dial = true => 
         is_dial(x) = false; 

         x ne tone = true => 
         is_tone(x) = false; 

         x ne star = true => 
         is_star(x) = false; 

         x ne pound = true => 
         is_pound(x) = false; 

         x ne voice_mail_answer = true => 
         is_voice_mail_answer(x) = false; 

         x ne busy = true => 
         is_busy(x) = false; 

         x ne flash_hook = true => 
         is_flash_hook(x) = false; 

         x ne conreq_calling_card = true => 
         is_conreq_calling_card(x) = false; 

         x ne hang_up = true => 
         is_hang_up(x) = false; 

         x ne discon_req = true => 
         is_discon_req(x) = false; 

         x ne activate_call_forward = true => 
         is_activate_call_forward(x) = false; 

         x ne play_announce_pwd = true => 
         is_play_announce_pwd(x) = false; 

         x ne deliver_messages = true => 
         is_deliver_messages(x) = false; 

         x ne play_announce_star_pound = true => 
         is_play_announce_star_pound(x) = false; 

         x ne play_announce_management = true => 
         is_play_announce_management(x) = false; 

         x ne play_announce_new_number = true => 
         is_play_announce_new_number(x) = false; 

         x ne good_bye = true => 
         is_good_bye(x) = false; 

         x ne detect_forward = true => 
         is_detect_forward(x) = false; 

         x ne unconditional_refusal = true => 
         is_unconditional_refusal(x) = false; 

         is_user_actions(x) = is_activate_call_forward(x) or is_hang_up(x) or is_flash_hook(x) or is_pound(x) or is_star(x) or is_dial(x) or is_pwd(x) or is_talk(x) or is_answer(x) or is_offhook(x); 

         is_network_actions(x) = is_unconditional_refusal(x) or is_detect_forward(x) or is_busy(x) or is_connect(x) or is_ring(x) or is_conreq(x) or is_tone(x); 

         is_voice_mail_actions(x) = is_good_bye(x) or is_play_announce_new_number(x) or is_play_announce_management(x) or is_play_announce_star_pound(x) or is_deliver_messages(x) or is_play_announce_pwd(x) or is_voice_mail_answer(x) ;
 endtype 

(* *** translating the following enumerated type **************************
 enumtype service is 
   { three_way_calling, call_waiting, call_forward, originate_screening}
 endtype 
 ******* in ACT ONE **************** *)
 type service is NaturalNumber
    sorts service
    opns 
      three_way_calling:  -> service
      call_waiting:  -> service
      call_forward:  -> service
      originate_screening:  -> service
      next: service -> service
      min_service:  -> service
      max_service:  -> service
      is_three_way_calling: service -> Bool
      is_call_waiting: service -> Bool
      is_call_forward: service -> Bool
      is_originate_screening: service -> Bool
      h: service -> Nat
      _eq_: service, service -> Bool
      _ne_: service, service -> Bool
      _lt_: service, service -> Bool
      _le_: service, service -> Bool
      _gt_: service, service -> Bool
      _ge_: service, service -> Bool
    eqns 
          forall x, y:service

        ofsort service

         min_service = three_way_calling; 

         max_service = originate_screening; 

         next(three_way_calling) = call_waiting; 

         next(call_waiting) = call_forward; 

         next(call_forward) = originate_screening ;

        ofsort Nat

         h(three_way_calling) = 0; 

         h(call_waiting) = Succ(0); 

         h(call_forward) = Succ(Succ(0)); 

         h(originate_screening) = Succ(Succ(Succ(0))) ;

        ofsort Bool

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

         x ne y = h(x) ne h(y); 

         x lt y = h(x) lt h(y); 

         x le y = h(x) le h(y); 

         x gt y = h(x) gt h(y); 

         x ge y = h(x) ge h(y); 

         x eq three_way_calling = true => 
         is_three_way_calling(x) = true; 

         x eq call_waiting = true => 
         is_call_waiting(x) = true; 

         x eq call_forward = true => 
         is_call_forward(x) = true; 

         x eq originate_screening = true => 
         is_originate_screening(x) = true; 

         x ne three_way_calling = true => 
         is_three_way_calling(x) = false; 

         x ne call_waiting = true => 
         is_call_waiting(x) = false; 

         x ne call_forward = true => 
         is_call_forward(x) = false; 

         x ne originate_screening = true => 
         is_originate_screening(x) = false ;
 endtype 

(* *** translating the following enumerated type **************************
 enumtype active_service is 
   { no_active_service, forward_calls}
 endtype 
 ******* in ACT ONE **************** *)
 type active_service is NaturalNumber
    sorts active_service
    opns 
      no_active_service:  -> active_service
      forward_calls:  -> active_service
      next: active_service -> active_service
      min_active_service:  -> active_service
      max_active_service:  -> active_service
      is_no_active_service: active_service -> Bool
      is_forward_calls: active_service -> Bool
      h: active_service -> Nat
      _eq_: active_service, active_service -> Bool
      _ne_: active_service, active_service -> Bool
      _lt_: active_service, active_service -> Bool
      _le_: active_service, active_service -> Bool
      _gt_: active_service, active_service -> Bool
      _ge_: active_service, active_service -> Bool
    eqns 
          forall x, y:active_service

        ofsort active_service

         min_active_service = no_active_service; 

         max_active_service = forward_calls; 

         next(no_active_service) = forward_calls ;

        ofsort Nat

         h(no_active_service) = 0; 

         h(forward_calls) = Succ(0) ;

        ofsort Bool

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

         x ne y = h(x) ne h(y); 

         x lt y = h(x) lt h(y); 

         x le y = h(x) le h(y); 

         x gt y = h(x) gt h(y); 

         x ge y = h(x) ge h(y); 

         x eq no_active_service = true => 
         is_no_active_service(x) = true; 

         x eq forward_calls = true => 
         is_forward_calls(x) = true; 

         x ne no_active_service = true => 
         is_no_active_service(x) = false; 

         x ne forward_calls = true => 
         is_forward_calls(x) = false ;
 endtype 


(* The following set type has been translated 

 settype subscrib_services is service 
   elements service
   values 
      no_services = {  }
 endtype
*)
 type subscrib_services00 is Set 
     renamedby 
    sortnames 
         subscrib_services for Set
 endtype 

 type subscrib_services0 is subscrib_services00 
     actualizedby service 
     using 
    sortnames 
         Bool for FBool
         service for Element
 endtype 

 type subscrib_services is subscrib_services0
    opns 
      no_services:  -> subscrib_services
    eqns 

        ofsort subscrib_services

         no_services = {} ;
 endtype 


(* The following set type has been translated 

 settype screen_list is phone_number 
   elements phone_number
   values 
      no_screen_list = {  }
 endtype
*)
 type screen_list00 is Set 
     renamedby 
    sortnames 
         screen_list for Set
 endtype 

 type screen_list0 is screen_list00 
     actualizedby phone_number 
     using 
    sortnames 
         Bool for FBool
         phone_number for Element
 endtype 

 type screen_list is screen_list0
    opns 
      no_screen_list:  -> screen_list
    eqns 

        ofsort screen_list

         no_screen_list = {} ;
 endtype 


    behavior 


 ( 
 
 phone[u, n](num1, Insert(three_way_calling, Insert(call_waiting, Insert(originate_screening, {}))), no_active_service, num1, Insert(num4, {}))
|||

 phone[u, n](num2, Insert(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)
|||

 call_waiting[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)
 [] 
   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)
|||

 three_way_calling[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