specification status_oriented_memory_phone[c,b,g,n,t,tn] :noexit (* written by Bernard STEPIEN on february 2nd, 1991 *) library Set,Boolean, NaturalNumber endlib type signal is sorts signal opns offhook, answer, voice, ring, connect, disreq, disind, conreq, conatmp, stopring, not_in_service, busy, dial, tone, hangup: -> signal endtype type status is sorts status opns idle, set_up, recvd_req, conctd, sbusy, con_req, dis_card , rung :-> status endtype type phone_number is NaturalNumber sorts phone_number opns none, one, two, three, four : -> phone_number natnum: phone_number -> Nat _eq_, _ne_ : phone_number, phone_number -> Bool eqns forall x,y: phone_number ofsort Nat natnum(none) = 0; natnum(one) = Succ(natnum(none)); natnum(two) = Succ(natnum(one)); natnum(three) = Succ(natnum(two)); natnum(four) = Succ(natnum(three)); ofsort Bool x eq y = natnum(x) eq natnum(y); x ne y = not(x eq y); endtype type phone_set0 is Set actualizedby phone_number, Boolean using sortnames phone_number for Element Bool for FBool endtype type phone_set is phone_set0 renamedby sortnames phone_set for Set endtype behaviour hide n, tn in (* ( decomment the left paren if using the test_sequence *) ( installer[c,b,g,n,t,tn]({} of phone_set) |[b,n,tn]| controller[b,n,tn] ) (* || test_sequence[c,b,g,n,t,tn] ) *) (* if you want to use the test sequence, do not forget to decomment the three above lines *) where process installer[c,b,g,n,t,tn](PIP:phone_set):noexit:= c ? NewNumber: phone_number ; ( station[b,g,n,t,tn](NewNumber) ||| installer[c,b,g,n,t,tn](Insert(NewNumber,PIP)) ) [] not_in_service[c,b,g,n,t,tn](PIP) endproc (* station *) process not_in_service[c,b,g,n,t,tn](PIP:phone_set):noexit:= b ? CRS: phone_number ! not_in_service [CRS NotIn PIP] ; installer[c,b,g,n,t,tn](PIP) endproc process station[b,g,n,t,tn](N:phone_number):noexit:= ( call_initiator_station[b,g,n,t,tn](N) [] call_responder_station[b,g,n,t,tn](N) ) >> station[b,g,n,t,tn](N) endproc (* station *) process call_initiator_station[b,g,n,t,tn](N:phone_number):exit:= g ! N ! offhook ; ( ( ( g ! N ! tone ; g ! N ! dial ? C : phone_number ; n ! N ! conreq ! C ; n ! N ! connect ; talking[g](N) ) ||| continuous_busy_signal[b](N) ) [> station_call_termination[t,tn](N) ) |[b,g,n,t,tn]| station_processor_memory[b,g,n,t,tn](N,idle,none) endproc (* call_initiator_station *) process call_responder_station[b,g,n,t,tn](C:phone_number):exit:= ( n ? N: phone_number ! ring ! C ; ( ( ( g ! C ! answer ; n ! C ! connect ; talking[g](C) ) ||| continuous_busy_signal[b](C) ) [> station_call_termination[t,tn](C) ) ) |[b,g,n,t,tn]| station_processor_memory[b,g,n,t,tn](C,idle,none) endproc (* call_responder_station *) process station_processor_memory[b,g,n,t,tn] (N:phone_number,S:status,PT:phone_number):exit:= station_record_status[b,g,n,t,tn](N,S,PT) [] station_indicate_termination_sequence[t,tn](N,S,PT) endproc process station_record_status[b,g,n,t,tn] (N:phone_number,S:status,PT:phone_number):exit:= is_not_reachable[b,g,n,t,tn](N,PT) [] is_in_set_up[b,g,n,t,tn](N,PT) [] has_rung[b,g,n,t,tn](N,PT) [] is_in_con_req[b,g,n,t,tn](N,PT) [] is_fully_connected[b,g,n,t,tn](N,PT) endproc process is_not_reachable[b,g,n,t,tn](N,PT:phone_number):exit:= b ! N ! busy ; station_processor_memory[b,g,n,t,tn](N,sbusy,PT) [] b ! N ! not_in_service ; station_processor_memory[b,g,n,t,tn](N,sbusy,PT) endproc process is_in_set_up[b,g,n,t,tn](N,PT:phone_number):exit:= g ! N ! offhook ; station_processor_memory[b,g,n,t,tn](N,set_up,PT) [] g ! N ! tone ; station_processor_memory[b,g,n,t,tn](N,set_up,PT) [] g ! N ! dial ? NPT: phone_number ; station_processor_memory[b,g,n,t,tn](N,set_up,NPT) endproc process has_rung[b,g,n,t,tn](N,PT:phone_number):exit:= n ? NPT: phone_number ! ring ! N ; station_processor_memory[b,g,n,t,tn](N,rung,NPT) endproc process is_in_con_req[b,g,n,t,tn](N,PT:phone_number):exit:= g ! N ! answer ; station_processor_memory[b,g,n,t,tn](N,recvd_req,PT) [] g ! N ! voice ; station_processor_memory[b,g,n,t,tn](N,recvd_req,PT) [] n ! N ! conreq ! PT ; station_processor_memory[b,g,n,t,tn](N,recvd_req,PT) endproc process is_fully_connected[b,g,n,t,tn](N,PT:phone_number):exit:= n ! N ! connect ; station_processor_memory[b,g,n,t,tn](N,conctd,PT) endproc process station_indicate_termination_sequence[t,tn] (N:phone_number,S:status,PT:phone_number):exit:= tn ! N ! disind ! S ; t ! N ! hangup ? S: status ; exit [] tn ! N ! stopring ! S ; exit [] t ! N ! hangup ! S ; ( tn ! N ! disreq ! PT ! S ; exit [] exit ) endproc process station_call_termination[t,tn](N:phone_number):exit:= station_terminate_set_up[t](N) [] station_terminate_once_connected[t,tn](N) [] station_terminate_during_con_req[t,tn](N) [] station_terminate_after_rung[tn](N) [] station_disconnect_once_connected[t,tn](N) [] station_disconnect_during_con_req[t,tn](N) endproc (* station_call_termination *) process station_terminate_set_up[t](N:phone_number):exit:= t ! N ! hangup ! set_up ; exit endproc process station_terminate_once_connected[t,tn] (N:phone_number):exit:= t ! N ! hangup ! conctd ; ( tn ! N ! disreq ? PT: phone_number ? S: status ; exit [] tn ! N ! disind ? S: status ; exit ) endproc process station_terminate_during_con_req[t,tn] (N:phone_number):exit:= t ! N ! hangup ! recvd_req ; ( tn ! N ! disreq ? PT: phone_number ? S: status ; exit [] tn ! N ! disind ? S: status ; exit ) endproc process station_terminate_after_rung[tn] (N:phone_number):exit:= tn ! N ! stopring ! rung ; exit endproc process station_disconnect_once_connected[t,tn] (N:phone_number):exit:= tn ! N ! disind ! conctd ; t ! N ! hangup ! conctd ; exit endproc process station_disconnect_during_con_req[t,tn] (N:phone_number):exit:= tn ! N ! disind ! recvd_req ; t ! N ! hangup ! recvd_req ; exit endproc process controller[b,n,tn]: noexit:= n ? N :phone_number ! conreq ? C :phone_number ; connection_control[b,n,tn](N,C) (* ||| controller[b,n,tn] *) endproc process connection_control[b,n,tn](N,C:phone_number): noexit:= (* n ? N :phone_number ! conreq ? C :phone_number ; *) ( ( ( ring_a_free_number[n](N,C) [] detect_busy_signal[b,tn](N,C) [] detect_not_in_service[b,tn](N,C) ) [> control_termination[tn] ) |[b,n,tn]| control_processor_memory[b,n,tn](N,recvd_req,none,idle) ) ||| controller[b,n,tn] endproc (* connection_control *) process ring_a_free_number[n](N,C:phone_number):noexit:= n ! N ! ring ! C ; n ! C ! connect ; n ! N ! connect ; stop endproc process detect_busy_signal[b,tn](N,C:phone_number):noexit:= b ! C ! busy ; ( tn ! N ! disind ? S: status ; stop [] tn ! N ! disreq ? S: status ; stop ) endproc process detect_not_in_service[b,tn](N,C:phone_number):noexit:= b ! C ! not_in_service ; ( tn ! N ! disind ? S: status ; stop [] tn ! N ! disreq ? S: status ; stop ) endproc process control_termination[tn]:noexit:= tn ? N: phone_number ! disreq ? C: phone_number ? S: status ; ( tn ! C ! stopring ! rung ; stop [] tn ! C ! disind ! conctd ; stop [] tn ! C ! disind ! recvd_req ; stop [] tn ! C ! disreq ! N ! conctd ; stop [] stop ) endproc (* control_termination *) process control_processor_memory[b,n,tn] (CIN:phone_number, CIS:status,CRN:phone_number, CRS:status):noexit:= control_record_status[b,n,tn](CIN,CIS,CRN,CRS) [] control_indicate_termination_sequence[b,tn](CIN,CIS,CRN,CRS) endproc process control_record_status[b,n,tn] (CIN:phone_number, CIS:status,CRN:phone_number, CRS:status):noexit:= n ? CIN: phone_number ! conreq ? NCRN: phone_number ; control_processor_memory[b,n,tn](CIN,recvd_req,CRN,CRS) [] n ? CIN: phone_number ! ring ? CRN: phone_number ; control_processor_memory[b,n,tn](CIN,CIS,CRN,rung) [] n ! CIN ! connect ; control_processor_memory[b,n,tn](CIN,conctd,CRN,CRS) [] n ! CRN ! connect ; control_processor_memory[b,n,tn](CIN,CIS,CRN,conctd) endproc process control_indicate_termination_sequence[b,tn] (CIN:phone_number, CIS:status,CRN:phone_number, CRS:status):noexit:= indicate_disreq_initiator_to_responder[tn] (CIN, CIS,CRN, CRS) [] indicate_disreq_responder_to_initiator[tn] (CIN, CIS,CRN, CRS) [] indicate_not_reachable[b,tn] (CIN, CIS,CRN, CRS) endproc (* control_indicate_termination_sequence *) process indicate_disreq_initiator_to_responder[tn] (CIN:phone_number, CIS:status,CRN:phone_number, CRS:status):noexit:= tn ! CIN ! disreq ? NCRN:phone_number ! CIS ; ( tn ! CRN ! stopring ! CRS ; stop [] [CRN ne none]-> ( tn ! CRN ! disind ? CRS: status ; stop [] tn ! CRN ! disreq ! CIN ? CRS: status ; stop ) [] [CRN eq none] -> stop ) endproc process indicate_disreq_responder_to_initiator[tn] (CIN:phone_number, CIS:status,CRN:phone_number, CRS:status):noexit:= tn ! CRN ! disreq ! CIN ? CRS: status ; ( tn ! CIN ! disind ? CIS:status; stop [] tn ! CIN ! disreq ! CRN ? CIS:status ; stop ) endproc process indicate_not_reachable[b,tn] (CIN:phone_number, CIS:status,CRN:phone_number, CRS:status):noexit:= b ? CRN: phone_number ! busy ; ( tn ! CIN ! disind ! CIS; stop [] tn ! CIN ! disreq ! CRN ! CIS ; stop ) [] b ? CRN: phone_number ! not_in_service ; ( tn ! CIN ! disind ! CIS; stop [] tn ! CIN ! disreq ! CRN ! CIS ; stop ) endproc process talking[g](N:phone_number):noexit:= g ! N ! voice ; talking[g](N) endproc (* talking *) process continuous_busy_signal[b](N:phone_number):noexit:= b ! N ! busy ; continuous_busy_signal[b](N) endproc process test_sequence[c,b,g,n,t,tn]:noexit:= c ! one ; (* phone installation phase *) c ! two ; c ! three ; c ! four ; ( test_full_con[c,b,g,n,t,tn] (* [] test_set_up[c,b,g,n,t,tn] [] test_recvd_req[c,b,g,n,t,tn] *) ) where process test_full_con[c,b,g,n,t,tn] :noexit:= g ! one ! offhook ; (* phone one connects with phone two *) g ! one ! tone ; g ! one ! dial ! two ; n ! one ! conreq ! two ; g ! three ! offhook ; (* phone three wants also phone two *) g ! three ! tone ; g ! three ! dial ! two ; n ! three ! conreq ! two ; n ! one ! ring ! two ; g ! two ! answer ; (* and gets it before phone one *) b ! two ! busy ; (* and phone one gets busy on phone two *) tn ! three ! disind ? S1:status ; t ! three ! hangup ? S2:status ; (* and aborts call *) (* i (enable: exit *) (* remainder of three - two connection *) n ! two ! connect ; n ! one ! connect ; (* everybody terminates *) t ! one ! hangup ? S3:status ; tn ! one ! disreq ! two ? S4:status ; (* i (enable: exit) *) tn ! two ! disind ? S5:status ; t ! two ! hangup ? S6:status ; (* i (enable: exit) *) (* return to original state means that the same test sequence should be able to be re-executed *) g ! one ! offhook ; (* phone one is back to idle *) g ! three ! offhook ; (* phone three is back to idle *) g ! two ! offhook ; (* phone two is back to idle *) stop (* explicit end of test sequence *) endproc process test_set_up[c,b,g,n,t,tn]:noexit:= (* hang up after set up state *) g ! one ! offhook ; (* phone one connects with phone two *) g ! one ! tone ; g ! one ! dial ! two ; t ! one ! hangup ? S:status ; g ! one ! offhook ; (* phone one s back to original state *) stop endproc process test_recvd_req[c,b,g,n,t,tn]:noexit:= (* hang up after connection request *) g ! one ! offhook ; (* phone one connects with phone two *) g ! one ! tone ; g ! one ! dial ! two ; n ! one ! conreq ! two ; t ! one ! hangup ? S1:status; tn ! one ! disreq ! two ? S2:status ; g ! one ! offhook ; (* phone one is back to original state *) stop endproc endproc endspec