specification feature_intentions[f,u,n]:noexit (* Written by Bernard Stepien, March 1995 *) library Boolean, NaturalNumber, Set endlib type signals is Boolean, NaturalNumber sorts signals opns off_hook, tone, dial, conreq, ring,answer, connect, talk, detect_forward, connect_refused:-> signals _ne_: signals, signals -> Bool h: signals ->nat eqns forall S1, S2:signals 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 Boolean sorts ConIdent opns conn1, conn2: -> ConIdent _eq_, _ne_: ConIdent, ConIdent -> Bool eqns ofsort Bool forall X,Y:ConIdent X eq X = true; conn1 eq conn2 = false; conn2 eq conn1 = false; X ne Y = not(X eq Y); endtype type intentions is Boolean, features, signals, roles, number_set sorts intention opns violates: feature, role, signals, number_set -> Bool eqns forall N:number, S: signals, 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, exausted_list :-> error_msg endtype type ActFeature is features, number, number_set, ConnectionIdentifier sorts ActFeature opns activatedFeature: feature, ConIdent , number_set -> ActFeature noActFeature:-> ActFeature _eq_, _ne_ : ActFeature, ActFeature -> Bool extract_act_feat: ActFeature -> feature extract_act_con: ActFeature -> ConIdent extract_act_RestList: ActFeature -> number_set eqns forall F:feature, C:ConIdent,RS:number_set ofsort feature extract_act_feat(activatedFeature(F,C,RS)) = F; ofsort ConIdent extract_act_con(activatedFeature(F,C,RS)) = C; ofsort number_set extract_act_RestList(activatedFeature(F,C,RS)) = RS; endtype type ActFeatSet00 is Set renamedby sortnames ActFeatSet for Set endtype type ActFeatSet0 is ActFeatSet00 actualizedby ActFeature using sortnames Bool for FBool ActFeature for Element endtype type ActFeatSet is ActFeatSet0 opns head : ActFeatSet -> ActFeature tail : ActFeatSet -> ActFeatSet IsEmpty: ActFeatSet -> Bool eqns forall H: Actfeature, T:ActFeatSet ofsort Actfeature head(Insert(H,T)) = H; head({}) = noActFeature; ofsort ActFeatSet tail(Insert(H,T)) = T; tail( {} ) = {}; ofsort Bool IsEmpty(Insert(H,T)) = false; IsEmpty({}) = true; endtype behavior ( ( (* let OList1:feature_data = ocs({}) in *) let OList1:feature_data = ocs(Insert(num3,{})) in ( phone[u,n,f](num1,fwd(none), OList1) ||| phone[u,n,f](num2,fwd(num3),ocs({})) ||| phone[u,n,f](num3,fwd(none),ocs({})) ) ) |[n]| network[n] ) || verify_intentions[f,u,n]( {} of ActFeatSet) 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 ; n ! N ! connect ! origin ; u ! N ! talk ! origin ; 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 ! 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(N, {}) ; 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 ; 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](AFS: ActFeatSet):noexit:= f ? ConId:ConIdent ? F: feature ? SL: number_set ; verify_intentions[f,u,n](Insert(activatedFeature(F,ConId,SL),AFS)) [] verify_action[f,u,n](AFS) endproc process verify_action[f,u,n](AFS:ActFeatSet):noexit:= u ? N:number ! off_hook ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,off_hook,L,AFS,AFS) [] n ? N:number ! tone ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,tone,L,AFS,AFS) [] u ? N:number ! dial ? C:number ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,dial,L,AFS,AFS) [] n ? N:number ! conreq ? D:number ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,conreq,L,AFS,AFS) [] n ? N:number ! conreq ? D:number ? L:location ? FD:feature_data ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,conreq,L,AFS,AFS) [] n ? N:number ! connect ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,connect,L,AFS,AFS) [] u ? N:number ! talk ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,talk,L,AFS,AFS) [] n ? N:number ! ring ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,ring,L,AFS,AFS) [] u ? N:number ! answer ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,answer,L,AFS,AFS) [] n ? N:number ! detect_forward ? D:number ? L:location ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,detect_forward,origin,AFS,AFS) [] n ? N:number ! connect_refused ? ConID:ConIdent ; verify_one_intention[f,u,n](ConId,N,connect_refused,origin,AFS,AFS) endproc process verify_one_intention[f,u,n](ConId:ConIdent, N:number,S:signals,L:location,AFS:ActFeatSet,OAFS:ActFeatSet):noexit:= hide v in ( [IsEmpty(AFS)]-> verify_intentions[f,u,n](OAFS) [] ( [ not(IsEmpty(AFS))]-> ( let AF:ActFeature = head(AFS) in [ ConId eq extract_act_con(AF) ]-> ( [ violates(extract_act_feat(AF),determine_role(L,N),S,extract_act_RestList(AF)) ] -> v ! violation ! ConId ! N ! extract_act_feat(AF) ! S ; verify_one_intention[f,u,n](ConId,N,S,L,tail(AFS),OAFS) [] [ not(violates(extract_act_feat(AF),determine_role(L,N),S,extract_act_RestList(AF))) ] -> verify_one_intention[f,u,n](ConId,N,S,L,tail(AFS),OAFS) ) [] [ ConId ne extract_act_con(AF) ]-> verify_one_intention[f,u,n](ConId,N,S,L,tail(AFS),OAFS) ) ) ) endproc endspec