#define BB 1 #define QSZ 2 mtype = { close, aclose, dial, adial, talk, htalk, numb, numbis, answer, trans, transok, atalk, nak, hangup, sysclose, opent, opend, ioattn, call, cnak }; chan h_envirn = [QSZ] of { byte }; chan h_normal = [QSZ] of { byte }; chan h_extern = [QSZ] of { byte }; chan c_normal = [QSZ] of { byte }; chan c_extern = [QSZ] of { byte }; chan c_envirn = [QSZ] of { byte }; active proctype host() { xr h_normal; xr h_extern; xs c_normal; xs h_envirn; end: closed: do :: h_normal?close -> c_normal!aclose :: h_normal?aclose :: h_normal?adial :: h_normal?talk -> c_normal!close; goto lclosed :: h_normal?atalk :: h_normal?nak -> c_normal!close :: h_extern?opent -> c_normal!talk; goto watalk :: h_extern?opend -> c_normal!dial; goto wadial od; dialing: do :: h_normal?close -> c_normal!aclose; goto rclosed :: h_normal?adial :: h_normal?talk -> c_normal!atalk; h_envirn!htalk; goto talking :: h_normal?atalk :: h_extern?sysclose -> c_normal!close; goto lclosed od; talking: do :: h_normal?close -> c_normal!aclose; goto rclosed :: h_normal?adial :: h_normal?talk -> c_normal!atalk :: h_normal?atalk :: h_extern?sysclose -> c_normal!close; goto lclosed :: h_extern?ioattn -> c_normal!dial; goto wattn od; rclosed: do :: h_normal?close -> c_normal!aclose :: h_extern?sysclose -> c_normal!close; goto lclosed od; watalk: do :: h_normal?close -> c_normal!aclose :: h_normal?aclose :: h_normal?atalk -> goto wtalk :: h_normal?nak :: h_extern?sysclose -> c_normal!close; goto lclosed :: timeout -> c_normal!talk od; wadial: do :: h_normal?close -> c_normal!aclose :: h_normal?aclose :: h_normal?adial -> goto dialing :: h_normal?atalk :: h_normal?nak :: h_extern?sysclose -> c_normal!close; goto lclosed :: timeout -> c_normal!dial od; lclosed: do :: h_normal?close -> c_normal!aclose :: h_normal?aclose -> goto closed :: h_normal?adial :: h_normal?talk -> c_normal!atalk; c_normal!close :: h_normal?atalk :: h_normal?nak :: h_extern?sysclose :: timeout -> c_normal!close od; wtalk: do :: h_normal?close -> c_normal!aclose; goto rclosed :: h_normal?talk -> c_normal!atalk; goto talking :: h_normal?atalk :: h_normal?nak -> goto closed :: h_extern?sysclose -> c_normal!close od; wattn: do :: h_normal?close -> c_normal!aclose; goto rclosed :: h_normal?adial -> goto dialing :: h_normal?talk -> c_normal!atalk :: h_normal?atalk :: h_extern?sysclose -> c_normal!aclose; goto lclosed :: timeout -> c_normal!dial od; endfail: do :: h_normal?nak :: h_extern?sysclose od } active proctype cont() { xr c_normal; xr c_extern; xs h_normal; xs c_envirn; end: idle: do :: c_normal?close -> h_normal!aclose :: c_normal?aclose :: c_normal?dial -> h_normal!adial; c_envirn!trans; goto dialing :: c_normal?adial :: c_normal?talk -> goto wproc :: c_normal?atalk :: c_normal?nak -> h_normal!close :: c_extern?call -> c_envirn!cnak od; dialing: do :: c_normal?close -> h_normal!aclose; goto idle :: c_normal?dial -> h_normal!adial :: c_extern?call -> c_envirn!cnak :: c_extern?cnak -> h_normal!nak; goto wclose :: c_extern?transok -> c_envirn!call; goto wproc od; talking: do :: c_normal?close -> h_normal!aclose; c_envirn!hangup; goto idle :: c_normal?dial -> h_normal!adial; goto dialing :: c_normal?talk -> h_normal!atalk :: c_normal?atalk :: c_extern?call -> c_envirn!cnak :: c_extern?hangup -> h_normal!close; goto lclosed od; wcall: do :: c_normal?close -> h_normal!aclose; goto idle :: c_normal?talk -> h_normal!atalk :: c_extern?call -> c_envirn!numb; goto wnumb od; wnumb: do :: c_normal?close -> h_normal!aclose; c_envirn!hangup; goto idle :: c_normal?talk -> h_normal!atalk :: c_extern?call -> c_envirn!cnak :: c_extern?cnak -> h_normal!nak; goto wclose :: c_extern?numbis -> h_normal!talk; c_envirn!answer; goto watalk od; watalk: do :: c_normal?close -> h_normal!aclose; c_envirn!hangup; goto idle :: c_normal?dial -> h_normal!adial :: c_normal?talk -> h_normal!atalk :: c_normal?atalk -> goto talking :: c_extern?call -> c_envirn!cnak :: c_extern?hangup -> h_normal!close; goto lclosed :: timeout -> h_normal!talk od; wclose: do :: c_normal?close -> h_normal!aclose; goto idle :: c_normal?dial -> h_normal!adial :: c_normal?adial :: c_normal?talk -> h_normal!atalk :: c_normal?atalk :: c_extern?call -> c_envirn!cnak od; lclosed: do :: c_normal?close -> h_normal!aclose; goto idle :: c_normal?aclose -> goto idle :: c_normal?dial -> h_normal!adial; h_normal!close :: c_normal?adial :: c_normal?talk -> h_normal!atalk; h_normal!close :: c_normal?atalk :: c_normal?nak -> h_normal!close :: c_extern?call -> c_envirn!cnak :: timeout -> h_normal!close od; wproc: do :: c_normal?close -> h_normal!aclose; c_envirn!hangup; goto idle :: c_normal?dial -> h_normal!adial :: c_normal?talk -> h_normal!atalk :: c_extern?call -> c_envirn!cnak :: c_extern?answer -> h_normal!talk; goto watalk :: c_extern?cnak -> h_normal!nak; goto wclose :: c_extern?numb -> c_envirn!numbis od; endfail: do :: c_normal?nak :: c_extern?call -> c_envirn!cnak od } active proctype cenvir() { xr c_envirn; xs c_extern; end: do :: c_envirn?numbis -> if :: c_extern!answer :: c_extern!hangup fi :: c_envirn?trans -> if :: c_extern!transok :: c_extern!cnak fi :: c_envirn?answer -> c_extern!hangup :: c_envirn?cnak :: c_envirn?hangup :: c_envirn?numb -> if :: c_extern!numbis :: c_extern!hangup fi :: c_envirn?call -> if :: c_extern!numb :: c_extern!cnak fi od } active proctype henvir() { xs h_extern; xr h_envirn; end: idle: if :: h_extern!opent; goto open :: h_extern!opend; goto open fi; open: if :: h_extern!sysclose; goto idle :: h_envirn?htalk; goto talking fi; talking: if :: h_extern!sysclose :: h_extern!ioattn; goto open fi }