specification feature_intentions[f,u,n]:noexit (* Written by Bernard Stepien - December 1994 *) library Boolean, NaturalNumber, Set endlib type operations is Boolean, NaturalNumber sorts operations opns off_hook, tone, dial, conreq, ring,answer, connect, talk, detect_forward, connect_refused:-> operations _ne_: operations, operations -> Bool h: operations ->nat eqns forall S1, S2:operations ofsort nat h(off_hook) = 0; h(tone) = Succ(h(off_hook)); h(dial) = Succ(h(tone)); h(conreq) = Succ(h(dial)); h(ring) = Succ(h(conreq)); h(connect) = Succ(h(ring)); h(talk) = Succ(h(connect)); h(detect_forward) = Succ(h(talk)); h(answer) = Succ(h(detect_forward)); h(connect_refused) = Succ(h(answer)); ofsort Bool S1 ne S1 = false; S1 ne S2 = h(S1) ne h(S2); endtype type number is Boolean, NaturalNumber sorts number opns num1, num2, num3, num4, none :-> number _eq_, _ne_: number, number -> Bool h: number -> nat eqns forall N1, N2:number ofsort Bool N1 eq N2 = h(N1) eq h(N2); N1 ne N2 = h(N1) ne h(N2); ofsort nat h(num1) = 0; h(num2) = Succ(0); h(num3) = Succ(Succ(0)); h(num4) = Succ(Succ(Succ(0))); h(none) = Succ(Succ(Succ(Succ(0)))); endtype type number_set00 is Set renamedby sortnames number_set for Set endtype type number_set0 is number_set00 actualizedby number using sortnames Bool for FBool number for Element endtype type number_set is number_set0 endtype type features is sorts feature opns call_forward, OCS:-> feature endtype type feature_data is number, features, number_set sorts feature_data opns fwd: number -> feature_data ocs: number_set -> feature_data extract_fwd: feature_data -> number extract_ocs: feature_data -> number_set extract_feature: feature_data -> feature update_data: feature, number, number_set -> number_set eqns forall N:number, L:number_set ofsort number extract_fwd(fwd(N)) = N; ofsort number_set extract_ocs(ocs(L)) = L; update_data(OCS,N,L) = L; update_data(call_forward,N,L) = Insert(N,L); ofsort feature extract_feature(fwd(N)) = call_forward; extract_feature(ocs(L)) = OCS; endtype type locations is sorts location opns origin, dest:-> location endtype type roles is number, locations sorts role opns caller, called: number -> role determine_role: location,number -> role eqns forall N:number ofsort role determine_role(origin,N) = caller(N); determine_role(dest,N) = called(N); endtype type ConnectionIdentifier is sorts ConIdent opns conn1, conn2, conn3: -> ConIdent endtype type intentions is Boolean, features, operations, roles, number_set sorts intention opns violates: feature, role, operations, number_set -> Bool eqns forall N:number, S: operations, L:number_set ofsort Bool violates(OCS,called(N),connect,L) = N IsIn L; violates(OCS,called(N),off_hook,L) = false; violates(OCS,called(N),tone,L) = false; violates(OCS,called(N),dial,L) = false; violates(OCS,called(N),conreq,L) = false; violates(OCS,called(N),detect_forward,L) = false; violates(OCS,called(N),connect_refused,L) = false; violates(OCS,called(N),ring,L) = N IsIn L; violates(OCS,called(N),answer,L) = N IsIn L; violates(OCS,called(N),talk,L) = N IsIn L; violates(OCS,caller(N),S,L) = false; (* call forward rules *) violates(call_forward,caller(N),S,L) = false; (* same rules as OCS apply *) violates(call_forward,called(N),S,L) = violates(OCS,called(N),S,L) ; endtype type error_msg is sorts error_msg opns violation:-> error_msg endtype behavior ( ( phone[u,n,f](num1,fwd(none),ocs(Insert(num3,{})) ) ||| phone[u,n,f](num2,fwd(num3),ocs({})) ||| phone[u,n,f](num3,fwd(none),ocs({})) ) |[n]| network[n] ) || verify_intentions[f,u,n] where process phone[u,n,f](N:number,FWD:feature_data,OCS:feature_data):noexit:= u ! N ! off_hook ! origin ? ConId: ConIdent ; f ! ConId ! extract_feature(OCS) ! extract_ocs(OCS) ; n ! N ! tone ! origin ! ConId ; u ! N ! dial ? C:number ! origin ! ConId ; ( [ extract_ocs(OCS) eq {} ]-> n ! N ! conreq ! C ! origin ! ConId ; n ! N ! connect ! origin ! ConId ; u ! N ! talk ! origin ! ConId ; stop [] [ extract_ocs(OCS) ne {} ]-> n ! N ! conreq ! C ! origin ! OCS ! ConId ; ( n ! N ! connect ! origin ! ConId ; u ! N ! talk ! origin ! ConId ; stop [] n ! N ! connect_refused ! origin ! ConId ; stop ) ) [] n ! N ! ring ! dest ? ConId: ConIdent ; ( [ extract_fwd(FWD) eq none ]-> u ! N ! answer ! dest ! ConId ; n ! N ! connect ! dest ! ConId ; u ! N ! talk ! dest ! ConId ; stop [] [ extract_fwd(FWD) ne none ]-> f ! ConId ! extract_feature(FWD) ! Insert(extract_fwd(FWD), {}) ; n ! N ! detect_forward ! extract_fwd(FWD) ! dest ! ConId ; phone[u,n,f](N,FWD,OCS) ) endproc process network[n]:noexit:= n ? O:number ! tone ? L:location ? ConId: ConIdent ; ( ( n ! O ! conreq ? D:number ? L:location ! ConId ; network_connect[n](O,D,ConId) [] n ! O ! conreq ? D:number ? L:location ? OCS:feature_data ! ConId ; ( [ D NotIn extract_ocs(OCS)]-> network_connect[n](O,D,ConId) [] [ D IsIn extract_ocs(OCS)]-> n ! O ! connect_refused ? L:location ! ConId ; stop ) ) ||| network[n] ) endproc process network_connect[n](O,D:number,ConId:ConIdent):noexit:= n ! D ! ring ? L:location ! ConId ; ( n ! D ! connect ? L:location ! ConId ; n ! O ! connect ? L:location ! ConId ; stop [] n ! D ! detect_forward ? FWD:number ? L:location ! ConId ; network_connect[n](O,FWD,ConId) ) endproc process verify_intentions[f,u,n]:noexit:= u ? N:number ! off_hook ? L:location ? ConId: ConIdent ; ( intentions_monitor[f,u,n](ConId) ||| verify_intentions[f,u,n] ) endproc process intentions_monitor[f,u,n](ConId:ConIdent):noexit:= normal_operation[u,n](ConId) [> activate_intention[f,u,n](ConId) endproc process normal_operation[u,n](ConId:ConIdent):noexit:= n ? N:number ! tone ? L:location ! ConId ; normal_operation[u,n](ConId) [] u ? N:number ! dial ? C:number ? L:location ! ConId ; normal_operation[u,n](ConId) [] n ? N:number ! conreq ? D:number ? L:location ! ConId ; normal_operation[u,n](ConId) [] n ? N:number ! conreq ? D:number ? L:location ? FD:feature_data ! ConId ; normal_operation[u,n](ConId) [] n ? N:number ! connect ? L:location ! ConId ; normal_operation[u,n](ConId) [] u ? N:number ! talk ? L:location ! ConId ; normal_operation[u,n](ConId) [] n ? N:number ! ring ? L:location ! ConId ; normal_operation[u,n](ConId) [] u ? N:number ! answer ? L:location ! ConId ; normal_operation[u,n](ConId) [] n ? N:number ! detect_forward ? D:number ? L:location ! ConId ; normal_operation[u,n](ConId) [] n ? N:number ! connect_refused ! ConId ; normal_operation[u,n](ConId) endproc process activate_intention[f,u,n](ConId:ConIdent):noexit:= f ! ConId ? Feature: feature ? SL: number_set ; monitor_one_intention[f,u,n](Feature,SL,ConId) endproc process monitor_one_intention[f,u,n](F:feature,SL:number_set,ConId:ConIdent):noexit:= hide v in n ? N:number ? S:operations ? C:number ? L:location ! ConId ; ( [ violates(F,determine_role(L,N),S,SL) ] -> v ! violation ! F ! S ! ConId ! N ; stop [] [ not(violates(F,determine_role(L,N),S,SL)) ] -> monitor_one_intention[f,u,n](F,SL,ConId) ) [] n ? N:number ? S:operations ? C:number ? L:location ? FD:feature_data ! ConId ; ( [ violates(F,determine_role(L,N),S,SL) ] -> v ! violation ! F ! S ! ConId ! N ; stop [] [ not(violates(F,determine_role(L,N),S,SL)) ] -> monitor_one_intention[f,u,n](F,SL,ConId) ) [] n ? N:number ? S:operations ? L:location ! ConId ; ( [ violates(F,determine_role(L,N),S,SL) ] -> v ! violation ! F ! S ! ConId ! N ; stop [] [ not(violates(F,determine_role(L,N),S,SL)) ] -> monitor_one_intention[f,u,n](F,SL,ConId) ) [] u ? N:number ? S:operations ? C:number ? L:location ! ConId ; ( [ violates(F,determine_role(L,N),S,SL) ] -> v ! violation ! F ! S ! ConId ! N ; stop [] [ not(violates(F,determine_role(L,N),S,SL)) ] -> monitor_one_intention[f,u,n](F,SL,ConID) ) [] u ? N:number ? S:operations ? L:location ! ConID [ S ne off_hook ] ; ( [ violates(F,determine_role(L,N),S,SL) ] -> v ! violation ! F ! S ! ConId ! N ; stop [] [ not(violates(F,determine_role(L,N),S,SL)) ] -> monitor_one_intention[f,u,n](F,SL,ConID) ) [] f ! ConId ? NF: feature ? NSL: number_set ; monitor_one_intention[f,u,n](F,SL,ConId) endproc endspec