(****************************************************************) (* Fax Plain and Simple (FPS 2000) Specification in LOTOS *) (* by Patrick Bihan-Faou, *) (* January 1995 *) (****************************************************************) (* This specification is based on the POTS specification *) (* (Plain Old Telephone System) written by Luigi Logrippo, *) (* Mohamed Faci and Bernard Stepien. *) (****************************************************************) Specification FPS_System [User_Actions, Fax_Actions, Network_Actions]: noexit library Set, Boolean, DecDigit, NaturalNumber endlib type DigitPair is DecDigit, Boolean sorts DigitPair opns None: -> DecDigit None: -> Nat Pair: DecDigit,DecDigit -> DigitPair _eq_: DigitPair, DigitPair -> Bool eqns forall f1,f2,l1,l2:DecDigit, f3:Nat ofsort Bool f1 eq None = false; None eq f1 = false; Pair(f1,l1) eq Pair(f2,l2) = (f1 eq f2) and (l1 eq l2); ofsort Bool f3 eq None = false; None eq f3 = false; ofsort Nat NatNum(None) = None endtype type Set_Of_Pairs is DigitPair sorts Set_Of_Pairs opns empty: -> Set_Of_Pairs add: DigitPair,Set_Of_Pairs -> Set_Of_Pairs remove: DigitPair,Set_Of_Pairs -> Set_Of_Pairs isin: DigitPair,Set_Of_Pairs -> Bool Second_Element:DecDigit,Set_Of_Pairs -> DecDigit notin: DigitPair,Set_Of_Pairs -> Bool eqns forall x,y:DigitPair, s:Set_Of_Pairs, f1,f2,l1,l2:DecDigit ofsort Set_Of_Pairs add(x,add(x,s)) = add(x,s); remove(x,add(x,s)) = s; not(x eq y) => remove(x,add(y,s)) = add(y,remove(x,s)); ofsort Bool isin(x,empty) = false; isin(x,add(y,s)) = (x eq y) or (isin(x,s)); isin(x,remove(x,s)) = false; not(x eq y) => isin(x,remove(y,s)) = isin(x,s); notin(x,s) = not(isin(x,s)); ofsort DecDigit Second_Element (f1,empty) = None ; Second_Element (f1,add(Pair(f1,l1),s)) = l1; f1 ne f2 => Second_Element (f1,add(Pair(f2,l2),s)) = Second_Element (f1,s); endtype type DecSet is Set actualizedby DecDigit using sortnames DecDigit for Element Bool for FBool DecSet for Set endtype (*********************************************************) (* These are the messages that a fax machine can display *) (*********************************************************) type network_action is sorts Network_Action opns off_hook, hang_up, ring, say, listen, dial_tone, dial, no_connection_signal, busy_signal :-> Network_Action endtype type fax_display is sorts Fax_Display opns doc_ready, dialing, transmitting_page, transmission_OK, receiving_page, reception_OK, time :-> Fax_Display endtype type ErrorType is Boolean sorts ErrorType opns no_dial_tone, dest_busy, lost_connection, tx_not_OK, rx_not_OK :-> ErrorType endtype type fax_action is sorts Fax_Action opns display, printing, cut_paper, manu_light_on, manu_light_off, bell_sound :-> Fax_Action endtype type user_action is sorts User_Action opns insert_doc, key_in, switch_mode, hit_go :-> User_Action endtype type fax_message is sorts Fax_Message opns user_speech, i_am_here, page_begin, page_data, page_end, page_OK :-> Fax_Message EndType type page_counter is sorts Page_Counter opns none :-> Page_Counter add : Page_Counter -> Page_Counter endtype (*********************************************************) (* Description of the behaviour of the complete system *) (*********************************************************) behaviour ( Actions[User_Actions, Fax_Actions, Network_Actions] |[User_Actions, Network_Actions]| Global_Constraints[User_Actions, Network_Actions](empty, {} of DecSet, {} of DecSet) ) where (******************************************************************************) Process Actions[User_Actions, Fax_Actions, Network_Actions]:noexit:= ( ( Single_Fax_Connection[User_Actions, Fax_Actions, Network_Actions] [] Single_Mode_Switch[User_Actions] ) ||| i; Actions[User_Actions, Fax_Actions, Network_Actions] ) Where (***************************************************************************) Process Single_Mode_Switch[u_action]:noexit:= ( u_action ? me: DecDigit ! switch_mode; stop ) EndProc (* Single_Switch_Mode *) (***************************************************************************) Process Single_Fax_Connection[u_action, f_action, n_action]:noexit:= ( ( (**** The local constraints ****) Fax_Send[u_action, f_action, n_action] ||| Fax_Receive[u_action, f_action, n_action] ) |[n_action]| Network[n_action] (**** The end-to-end constraints ****) ) Where (************************************************************************) Process Fax_Error_Recover[f_action, n_action] (me: DecDigit, etype: ErrorType):noexit:= hide wait_5_sec in ( f_action ! me ! display ! etype; n_action ! me ! hang_up; wait_5_sec ! me; f_action ! me ! display ! time; stop [] stop (* to exit when we don't have any errors *) (* this is to be corrected by a better error-handling *) ) EndProc (* Fax_Error_Recover *) (************************************************************************) Process Fax_Send[u_action, f_action, n_action]:noexit:= ( u_action ? me: DecDigit ! insert_doc ? manu: Bool; ( [ manu ] -> Manu_Send[u_action, f_action, n_action](me) [] [ not(manu) ] -> Auto_Send[u_action, f_action, n_action](me) ) ) Where (*********************************************************************) Process Manu_Send[u_action, f_action, n_action] (me: DecDigit):noexit:= ( Auto_Send[u_action, f_action, n_action](me) ) EndProc (* Manu_Send *) (*********************************************************************) Process Auto_Send[u_action,f_action,n_action] (me: DecDigit):noexit:= ( f_action ! me ! display ! doc_ready; u_action ! me ! key_in ? number : DecDigit; u_action ! me ! hit_go; f_action ! me ! display ! dialing; n_action ! me ! off_hook; ( Fax_Error_Recover[f_action, n_action](me, no_dial_tone) [] n_action ! me ! dial_tone; n_action ! me ! dial ! number; ( n_action ! me ! busy_signal; Fax_Error_Recover[f_action, n_action](me, dest_busy) [] n_action ! me ! listen ! i_am_here; Send_Page[u_action, f_action, n_action](me, add(none)) [> n_action ! me ! no_connection_signal; Fax_Error_Recover[f_action, n_action](me, lost_connection) ) ) ) Where Process Send_Page[u_action, f_action, n_action] (me: DecDigit, counter : Page_Counter):noexit:= hide internal_sync in ( Send_This_Page[f_action, n_action, internal_sync](me, counter) |[internal_sync]| (**) Next_Page_Or_Leave[u_action, f_action, n_action, internal_sync](me, counter) ) Where Process Send_This_Page[f_action, n_action, internal_sync] (me: DecDigit, counter: Page_Counter):noexit:= ( n_action ! me ! say ! page_begin ! counter; f_action ! me ! display ! transmitting_page ! counter; n_action ! me ! say ! page_data ! counter; n_action ! me ! say ! page_end ! counter; n_action ! me ! listen ! page_OK ! counter; internal_sync ! me; stop |[internal_sync]| ( Fax_Error_Recover[f_action, n_action](me, tx_not_OK) [] internal_sync ! me; stop ) ) EndProc (* Send_This_Page *) Process Next_Page_Or_Leave[u_action, f_action, n_action, internal_sync] (me: DecDigit, counter: Page_Counter):noexit:= hide wait_5_sec in ( ( u_action ! me ! insert_doc; internal_sync ! me; Send_Page[u_action, f_action, n_action](me, add(counter)) ) [] ( internal_sync ! me; f_action ! me ! display ! transmission_OK; n_action ! me ! hang_up; wait_5_sec ! me; f_action ! me ! display ! time; stop ) ) EndProc (* Next_Page_Or_Leave *) (* the internal_sync gate is there to make sure that the fax *) (* start to send a new page before the previous one has been *) (* finished *) (* Thus the user must add some paper to transmit *) (* before the acknowledgment message is received from the *) (* other fax machine...*) EndProc (* Send_Page *) EndProc (* Auto_Send *) (*********************************************************************) EndProc (* Fax_Send *) (************************************************************************) Process Fax_Receive[u_action, f_action, n_action]:noexit:= ( n_action ? me: DecDigit ! ring ? manu: Bool; ( [ manu ] -> Auto_Receive[f_action, n_action](me) [] [ not(manu) ] -> Auto_Receive[f_action, n_action](me) ) ) Where Process Auto_Receive[f_action, n_action] (me: DecDigit):noexit:= ( (***** Connection Phase *****) f_action ! me ! bell_sound; n_action ! me ! off_hook; n_action ! me ! say ! i_am_here; Receive_Page[f_action, n_action](me) ) Where Process Receive_Page[f_action, n_action] (me: DecDigit):noexit:= hide internal_sync, wait_5_sec in ( n_action ! me ! listen ! page_begin ? counter : Page_Counter; f_action ! me ! display ! receiving_page ! counter; n_action ! me ! listen ! page_data ! counter; f_action ! me ! printing; n_action ! me ! listen ! page_end ! counter; f_action ! me ! cut_paper; n_action ! me ! say ! page_OK ! counter; internal_sync ! me; stop |[internal_sync]| ( Fax_Error_Recover[f_action, n_action](me, rx_not_OK) [] internal_sync ! me; ( Receive_Page[f_action, n_action](me) [] n_action ! me ! no_connection_signal; n_action ! me ! hang_up; f_action ! me ! display ! reception_OK; wait_5_sec ! me; f_action ! me ! display ! time; stop ) ) ) EndProc (* Receive_Page *) EndProc (* Auto_receive *) EndProc (* Fax_Receive *) (************************************************************************) Process Network[n_action]:noexit:= ( (***** Connection Phase *****) n_action ? caller : DecDigit ! off_hook; n_action ! caller ! dial_tone; n_action ! caller ! dial ? called : DecDigit; ( ( n_action ! called ! ring ? mode: Bool; n_action ! called ! off_hook; Discussion[n_action](caller,called) [> Hang_Up[n_action](caller, called) ) [] n_action ! caller ! busy_signal; n_action ! caller ! hang_up; stop ) (* must still do the hang_up *) ) Where Process Discussion[n_action] (caller, called : DecDigit):noexit:= ( n_action ! caller ! say ? what1: Fax_Message ? what2: Page_Counter; n_action ! called ! listen ! what1 ! what2; Discussion[n_action](caller, called) [] n_action ! called ! say ? what1: Fax_Message ? what2: Page_Counter; n_action ! caller ! listen ! what1 ! what2; Discussion[n_action](caller, called) [] n_action ! caller ! say ? what1: Fax_Message; n_action ! called ! listen ! what1; Discussion[n_action](caller, called) [] n_action ! called ! say ? what1: Fax_Message; n_action ! caller ! listen ! what1; Discussion[n_action](caller, called) ) EndProc (* Discussion *) Process Hang_Up[n_action] (caller, called: DecDigit):noexit:= ( n_action ! caller ! hang_up; n_action ! called ! no_connection_signal; n_action ! called ! hang_up; stop [] n_action ! called ! hang_up; n_action ! caller ! no_connection_signal; n_action ! caller ! hang_up; stop ) EndProc (* Hang_Up *) EndProc (* Network *) (************************************************************************) EndProc (* Single_Fax_Connection *) (***************************************************************************) EndProc (* Actions *) (******************************************************************************) Process Global_Constraints[u_actions, n_actions] (E: Set_Of_Pairs, B: DecSet, M: DecSet):noexit:= ( Users_List_Handler[n_actions](E,B) |[n_actions]| Fax_Mode_Handler[u_actions, n_actions](M) ) Where (***************************************************************************) process Users_List_Handler [S_User] (E : Set_Of_Pairs, B: DecSet ) :noexit:= ( S_User ? User: DecDigit ! off_hook [notin ( Pair(User, Second_Element (User, E)), E)]; Users_List_Handler [S_User]( add( Pair(User, None ), E), B) [] S_User ? Caller: DecDigit ! dial_tone; Users_List_Handler [S_User](E, B) [] S_User ? Caller: DecDigit ! dial ? Called: DecDigit ; Users_List_Handler [S_User] (add( Pair( Caller, Called), remove( Pair(Caller, None), E)), B) [] S_User ? Called: DecDigit ! ring ? mode: Bool [not(isin( Pair(Called, Second_Element (Called, E)), E) or ( Called IsIn B))]; Users_List_Handler [S_User](E, Insert(Called, B)) [] S_User ? User: DecDigit ! hang_up; ( [(User IsIn B)] -> Users_List_Handler [S_User] (remove(Pair (User, None),E), Remove (User, B)) [] [ (User NotIn B)] -> Users_List_Handler [S_User] (remove(Pair (User,Second_Element (User, E)),E), Remove(Second_Element (User, E), B)) ) [] S_User ? Caller: DecDigit ! busy_signal [isin( Pair(Second_Element (Caller, E), Second_Element (Second_Element (Caller, E), E)), E) or ( Second_Element (Caller, E) IsIn B) ]; Users_List_Handler [S_User](E, B) [] S_User ? User: DecDigit ! say ? what1: Fax_Message ? what2: Page_Counter; Users_List_Handler [S_User](E, B) [] S_User ? User: DecDigit ! listen ? what1: Fax_Message ? what2: Page_Counter; Users_List_Handler [S_User](E, B) [] S_User ? User: DecDigit ! say ? what1: Fax_Message; Users_List_Handler [S_User](E, B) [] S_User ? User: DecDigit ! listen ? what1: Fax_Message; Users_List_Handler [S_User](E, B) [] S_User ? User: DecDigit ! no_connection_signal; Users_List_Handler [S_User](E, B) ) EndProc (* Users_List_Handler *) (***************************************************************************) Process Fax_Mode_Handler[u_action, n_action] (M: DecSet):noexit:= (* M is the set of fax-machines that are in manual mode *) (* each fax machine is identified by the phone number of the line *) (* on which it is connected *) ( (* first we describe th global constraint related to the fax-machine *) (* when the user performs an action on it *) u_action ? me:DecDigit ! switch_mode; ( [ me IsIn M ] -> Fax_Mode_Handler[u_action, n_action](Remove(me,M)) [] [ not(me IsIn M) ] -> Fax_Mode_Handler[u_action, n_action](Insert(me,M)) ) [] u_action ? me: DecDigit ! insert_doc ! true [ me IsIn M]; Fax_Mode_Handler[u_action, n_action](M) [] u_action ? me: DecDigit ! insert_doc ! false [ not(me IsIn M) ]; Fax_Mode_Handler[u_action, n_action](M) [] u_action ? me: DecDigit ! key_in ? n: DecDigit; Fax_Mode_Handler[u_action, n_action](M) [] u_action ? me: DecDigit ! hit_go; Fax_Mode_Handler[u_action, n_action](M) [] u_action ? me: DecDigit ! insert_doc; Fax_Mode_Handler[u_action, n_action](M) [] (* now we describe the global constraints on the fax machine *) (* related to events comming from the network *) n_action ? me: DecDigit ! ring ! true [ me IsIn M ]; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! ring ! false [ not(me IsIn M) ]; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! off_hook; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! hang_up; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! dial_tone; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! dial ? n: DecDigit; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! busy_signal; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! say ? w1: Fax_Message ? w2: Page_Counter; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! listen ? w1: Fax_Message ? w2: Page_Counter; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! say ? w1: Fax_Message; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! listen ? w1: Fax_Message; Fax_Mode_Handler[u_action, n_action](M) [] n_action ? me: DecDigit ! no_connection_signal; Fax_Mode_Handler[u_action, n_action](M) ) EndProc (* Fax_Mode_Handler *) (***************************************************************************) EndProc (* Global_Constraints *) (******************************************************************************) EndSpec