%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A restricted (without time variables) equivalence (strong, weak) checker % for Timed CCS. % % Ahmet Serkan KARATAS % July 19, 2000 % Version 0.1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Act : The set of actions % K : The set of agent constants % T : Time Domain (Discrete) % tau : The special silent action (tau E Act) % eps : The empty sequence %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % member, insert, subset, union % % Some well-known set operations. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% member(A, [A|_]). member(A, [_|L]) :- member(A, L). insert(void, L, L) :- !. insert(A, L, [A|L]). subset([], _). subset([E|R], L) :- member(E, L), subset(R, L). union([], L, L). union([E|R], L, U) :- member(E, L), !, union(R, L, U). union([E|R], L, [E|U]) :- union(R, L, U). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % allcomb : A-List x A-List % % Takes a list and generates all possible combinations of the elements of % the list. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% del(X, [X|TAIL], TAIL) :- !. del(X, [Y|TAIL], [Y|TAIL1]) :- del(X,TAIL,TAIL1). ins(X, L1, L2) :- del(X, L2, L1). % Finds the N combinations of a list comb(_, 0, []) :- !. comb([], _, _) :- !, fail. comb([X|Y], N, L) :- (N1 is N-1, comb(Y, N1, K), ins(X, K, L)); comb(Y, N, L). % Counts the number of elements in a list count([], 0). count([_|TAIL], N) :- count(TAIL, N1), N is N1+1. combination(L, N, N, L) :- !. combination(L, N1, N, C) :- comb(L, N1, C); (N2 is N1+1, !, N2== Y, RES is X-Y. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % complement : Act x Act % % Defines the complementary action of an action. % % complement(act, act_bar) means, % act_bar is the complement of act. % % Note that this predicate alone does not say that act is the complement % of act_bar! % % ATTENTION: % For ALL the actions that take place in any agent expression the % complementray action should be defined in the database in a % bidirectional way! % Ex: complement(a, abar). % complement(abar, a). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % prefix : K x Act x T x T x K % % Defines an agent constructed by using the prefix combinator ".". % % prefix(p, alpha, lower, upper, q) means, % P = alpha(t)[lower,upper].Q % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sum : K x K x K % % Defines an agent constructed by using the summation combinator "+". % % sum(p, q, r) means; % P = Q + R %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % com : K x K x K % % Defines an agent constructed by using the parallel composition % combinator "|". % % com(p, q, r) means; % P = Q | R %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % res : K x Act % % Adds an action to the restriction set of an agent. % res(p, a) means; % P \a % % Ex: res(ag_p, a). % res(ag_p, b). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % setrest : K x K % % When a new agent definition is added to the database (see below for the % conditions when this occures) all the restrictions of the agent that is % caused a new agent to be added should also be passed to the newly added % agent. setrest performs this task. % % Ex: setrest(P, Q) turns on all the restrictions for P, also for Q %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% setrest(P, Q) :- (res(P, A);dres(P, A)), assert(dres(Q, A)), fail. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % simdelay : K x T x T % % Finds out to which agent an agent evolves to when it makes some % delay, and inserts the resulting agent definition and the delaying % information into the database. % % simdelay(P, DELAY, Q) means, % P -----------> Q % DELAY % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % When an agent makes a delay, it will evolve into a new agent. The definition % of this new agent should be available in the database for further computing. % But most probably there won't be a definition which is identical to the new % agent in the database initially. But as the new agent definitions % corresponding to the delayed agents be added to the database, definitons % that are identical to the delayed agent may become available in the database. % (e.g. assume agent P first delays 2 units and evolves to P2, and again assume % agent P delays 1 unit, evolves to P1, and then P1 delays 1 unit and evolves % to P1'. Obviously P1' is strongly equivalent to P2, so one may be used in % place of the other). % delay first computes what will be the definition for the agent after making % the delay. Then it seeks for an identical definition already inserted to the % database. If it can find one, it returns the found definition as the result. % Otherwise it assigns the new agent a unique agent constant, and then inserts % the definiton of the new agent constant into the database (with the prefix % 'd', e.g. for an agent constructed by prefix combinator a new agent % definition with dprefix will be inserted into the database) % Here we mean pure delay, done without performing any action (observable or % non-observable). % delay(P, 0, P) :- !. delay(P, DELAY, Q) :- (prefix(P, A, L, U, P1);dprefix(P, A, L, U, P1)), DELAY =< U, dotsub(L, DELAY, LP), UP is U-DELAY, (prefix(Q, A, LP, UP, P1);dprefix(Q, A, LP, UP, P1)), !. delay(P, DELAY, Q) :- (prefix(P, A, L, U, P1);dprefix(P, A, L, U, P1)), DELAY =< U, dotsub(L, DELAY, LP), UP is U-DELAY, current(NEW), NEW1 is NEW+1, retract(current(NEW)), assert(current(NEW1)), assert(dprefix(NEW, A, LP, UP, P1)), Q is NEW, \+ setrest(P, Q), !. delay(P, DELAY, Q) :- (sum(P, P1, P2);dsum(P,P1,P2)), delay(P1, DELAY, P1P), delay(P2, DELAY, P2P), (sum(Q, P1P, P2P);sum(Q, P2P, P1P);dsum(Q, P1P, P2P);dsum(Q, P2P, P1P)), !. delay(P, DELAY, Q) :- (sum(P, P1, P2);dsum(P,P1,P2)), delay(P1, DELAY, P1P), delay(P2, DELAY, P2P), current(NEW), NEW1 is NEW+1, retract(current(NEW)), assert(current(NEW1)), assert(dsum(NEW, P1P, P2P)), Q is NEW, \+ setrest(P, Q), !. delay(P, DELAY, Q) :- (sum(P, P1, P2);dsum(P,P1,P2)), delay(P1, DELAY, Q), \+ delay(P2, DELAY, _), !. delay(P, DELAY, Q) :- (sum(P, P1, P2);dsum(P,P1,P2)), \+ delay(P1, DELAY, _), delay(P2, DELAY, Q), !. delay(P, DELAY, Q) :- (com(P, P1, P2);dcom(P, P1, P2)), delay(P1, DELAY, P1P), delay(P2, DELAY, P2P), (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)), !. delay(P, DELAY, Q) :- (com(P, P1, P2);dcom(P, P1, P2)), delay(P1, DELAY, P1P), delay(P2, DELAY, P2P), current(NEW), NEW1 is NEW+1, retract(current(NEW)), assert(current(NEW1)), assert(dcom(NEW, P1P, P2P)), Q is NEW, \+ setrest(P, Q), !. % % sortd finds out which delays an agent can make (without performing any % observable or non-observable action), computes the agent expressions % that the delaying agent evolves into, and returns a set of % (delay, agent constant) pairs, where delay is the amount of delay the % agent under interest makes, and agent constant is the unique agent % constant (member of K) which correspondes to the agent expression the % agent under interest will evolve into after making the delay. % To not to compute this set again and again each time it is called % with the same argument, it inserts a copy of the resulting list into % the database the first time it is called, and then it returns this list % when it is invoked with the same argument. % finddelays(P, N, SD, DSET) :- delay(P, N, Q), insert((N,Q), SD, SD1), N1 is N+1, !, finddelays(P, N1, SD1, DSET). finddelays(_, _, SD, DSET) :- insert(void, SD, DSET), !. sortd(P, SORT) :- delaysof(P, SORT), !. sortd(P, SORT) :- finddelays(P, 0, [], SORT), assert(delaysof(P, SORT)), !. simdelay(P, DELAY, Q) :- sortd(P, SORTP), !, member((DELAY,Q), SORTP). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % simarrow : K x Act x T x K % % Defines the labelled transition relation. % % simarrow(p, a, u, q) means; % a % P ---> Q % u % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Returns a time value between the lower and upper bounds of an action % ontime(L, _, L). ontime(L, U, T) :- L1 is L+1, L1= Q % u % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% silent(tau). empty(eps). % % sort1_s finds the transactions an agent may perform and then seperates them % into two sets, as observanle actions and non-observable (or silent) actions. % sep(E, N, EPS, NONEPS, [(A, T, Q)|REST]) :- silent(A), sep(E, N, [(eps, T, Q)|EPS], NONEPS, REST), !. sep(E, N, EPS, NONEPS, [(A, T, Q)|REST]) :- \+ silent(A), sep(E, N, EPS, [(A, T, Q)|NONEPS], REST), !. sep(E, N, EPS, NONEPS, []) :- insert(void, EPS, E), insert(void, NONEPS, N), !. sort1_s(P, EPS, NONEPS) :- sort1(P, L), sep(EPS, NONEPS, [], [], L), !. % % extend computes into which agents an agent may evolve into by just making % non-observable actions. After each action time values are re-arrenged by % the predicate "addtime" to be able to show how much time has elapsed % since the beginning of the sequence. % addtime([], _, []) :- !. addtime([(A,T1,Q)|TAIL], T, [(A,TNEW,Q)|REST]) :- TNEW is T+T1, addtime(TAIL, T, REST), !. extend([], L, L) :- !. extend([(eps,T,Q)|TAIL], L, ESET) :- sort1_s(Q, EPS, _), addtime(EPS, T, EPSTA), subset(EPSTA, L), !, extend(TAIL, L, ESET), !. extend([(eps,T,Q)|_], L, ESET) :- sort1_s(Q, EPS, _), addtime(EPS, T, EPSTA), union(EPSTA, L, L1), !, extend(L1, L1, ESET), !. % % By the definition of the double arrow for epsilon we must find the delays % that the agent(s) reached after performing 0 or more tau actions can make. % maydelay finds the delays for each of the agents reached after performing % epsilon actions. While doing this the predicate "addtime2" is used to be % able to show the actual time passed since the beginning of the tau actions % till the end of the delay done. % addtime2([], _, []) :- !. addtime2([(D1,Q)|TAIL], T, [(eps,D,Q)|REST]) :- D is T+D1, addtime2(TAIL, T, REST), !. maydelay([], L, L) :- !. maydelay([(eps,T1,Q0)|TAIL], L, DELS) :- sortd(Q0, SD), addtime2(SD, T1, SD1), subset(SD1, L), !, maydelay(TAIL, L, DELS), !. maydelay([(eps,T1,Q0)|_], L, DELS) :- sortd(Q0, SD), addtime2(SD, T1, SD1), union(SD1, L, L1), !, maydelay(L1, L1, DELS), !. % % By the definiton of double arrow we must first find how much time an agent % may spend without performing an observable action (we do this by the above % predicates). And then we must find what kind of observable actions the % agent can perform and then which non-observable actions it can perform % at the same moment. We find the first goal by "mayperform", and the second % goal by samemoment. Union of the two give us the result set. % eps2tau([], []). eps2tau([(eps,T,Q)|TAIL], [(tau,T,Q)|REST]) :- eps2tau(TAIL, REST). mayperform([], L, L) :- !. mayperform([(eps,T1,Q0)|TAIL], L, ACTS) :- sort1_s(Q0, EPS, NONEPS), eps2tau(EPS, TAU), addtime(TAU, T1, TAUTA), addtime(NONEPS, T1, NEPSTA), union(L, NEPSTA, L1), union(L1, TAUTA, L2), mayperform(TAIL, L2, ACTS), !. select([], _, _, []) :- !. select([(eps,T,Q)|TAIL], A, T, [(A,T,Q)|SS]):- select(TAIL, A, T, SS). select([(eps,T1,_)|TAIL], A, T, SS) :- \+ T=T1, select(TAIL, A, T, SS). samemoment([], L, L) :- !. samemoment([(A,T,Q)|TAIL], L, SM) :- extend([(eps,T,Q)], [(eps,T,Q)], ESET), select(ESET, A, T, SSET), union(L, SSET, L1), !, samemoment(TAIL, L1, SM). maydo(EPSET, ACTSET) :- mayperform(EPSET, [], ACTS), samemoment(ACTS, [], EACTS), union(ACTS, EACTS, ACTSET), !. % % The set of actions an agent may perform by double arrow % sort_darr(P, DARRSORT) :- darrowsof(P, DARRSORT), !. sort_darr(P, DARRSORT) :- sort1_s(P, EPS, _), insert((eps,0,P), EPS, EPSP), extend(EPSP, EPSP, EPSE), maydelay(EPSE, EPSE, EPSET), maydo(EPSET, ACTSET), union(EPSET, ACTSET, DARRSORT), assert(darrowsof(P, DARRSORT)), !. darrow(P, A, T, Q) :- sort_darr(P, SD), !, member((A,T,Q), SD). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sbs : S x S where, S = {(P,Q) | P,Q E K} % % sbs checks whether a given set is a strong bisimulation or not. It must % be called with two copies of the set to be investigated, because it uses % one copy to determine the pair to be investigated, and the other copy % to check if the descendants of the pair is in the original set. % % Ex: sbs([(p,q), (p1,q1)], [(p,q), (p1,q1)]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Checks conditions 1,3 of being a strong bisimulation [Chen92, pp66] % scond13(_, _, _, []) :- !. scond13(P, Q, BS, [(A, T, P0)|SORT]) :- simarrow(Q, A, T, Q0), (member((P0,Q0), BS) ; member((Q0,P0), BS)), scond13(P, Q, BS, SORT), !. % % Checks conditions 2,4 of being a strong bisimulation [Chen92, pp66] % scond24(_, _, _, []) :- !. scond24(P, Q, BS, [(D, P0)|SORT]) :- simdelay(Q, D, Q0), (member((P0,Q0), BS) ; member((Q0,P0), BS)), scond24(P, Q, BS, SORT), !. sbs([], _). sbs([(P,Q)|L], BS) :- sort1(P, SORTP), scond13(P, Q, BS, SORTP), sort1(Q, SORTQ), scond13(Q, P, BS, SORTQ), sortd(P, SORTPD), scond24(P, Q, BS, SORTPD), sortd(Q, SORTQD), scond24(Q, P, BS, SORTQD), sbs(L, BS). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % wbs : S x S where, S = {(P,Q) | P,Q E K} % % wbs checks whether a given set is a weak bisimulation or not. It must be % called with two copies of the set to be investigated, because it uses % one copy to determine the pair to be investigated, and the other copy % to check whether the descendants of the pair is in the set or not. % % Ex: wbs([(p,q), (p1,q1)], [(p,q), (p1,q1)]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % filtereps deletes the eps transactions in a set. Because the original % sort_darr of an agent contains both the alpha and alpha-cap actions, % alpha-cap actions should be eliminated for the 1st and 3rd conditions of % being a bisimulation. % filtereps([], []). filtereps([(eps,_,_)|TAIL], REST) :- filtereps(TAIL, REST). filtereps([(A,T,Q)|TAIL], [(A,T,Q)|REST]):- \+ empty(A), filtereps(TAIL, REST). % % Checks conditions 1,3 of being a strong bisimulation [Chen92, pp112] % wcond13(_, _, []) :- !. wcond13(Q, BS, [(tau,U,P0)|REST]) :- darrow(Q, eps, U, Q0), (member((P0,Q0), BS);member((Q0,P0), BS)), wcond13(Q, BS, REST), !. wcond13(Q, BS, [(A,U,P0)|REST]) :- \+ silent(A), darrow(Q, A, U, Q0), (member((P0,Q0), BS);member((Q0,P0), BS)), wcond13(Q, BS, REST), !. % % Checks conditions 2,4 of being a strong bisimulation [Chen92, pp112] % wcond24(_, _, []) :- !. wcond24(Q, BS, [(D,P0)|REST]) :- darrow(Q, eps, D, Q0), (member((P0,Q0), BS);member((Q0,P0), BS)), wcond24(Q, BS, REST), !. wbs([], _). wbs([(P,Q)|REST], BS) :- sort_darr(P, SDP), filtereps(SDP, SDPA), wcond13(Q, BS, SDPA), sortd(P, DELP), wcond24(Q, BS, DELP), sort_darr(Q, SDQ), filtereps(SDQ, SDQA), wcond13(P, BS, SDQA), sortd(Q, DELQ), wcond24(P, BS, DELQ), wbs(REST, BS). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % seq : K x K % % seq checks whether two agents are strongly equivalent or not. It % simply tries ot find a strong bisimulation (P, Q) is a member of. To do % this first it finds all possible derivatives of the agents under % interest (when both performs the same action, or same delay), and then % tries to find a strong bisimulation that is a subset of this derivations % set, and the agents under interest are members of. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % filter selects the members of a set that performs a given action % on the given time, and inserts resulting agents into the resulting set. % filter(_, [], _, _, []) :- !. filter(P, [(A,T,Q)|TAIL], A, T, [(P,Q)|REST]) :- filter(P, TAIL, A, T, REST), !. filter(P, [_|TAIL], A, T, REST) :- filter(P, TAIL, A, T, REST), !. % % sfindpossacts finds the all possible actions an agent may perform depending % on an action of another action. % sfindpossacts([], _, []) :- !. sfindpossacts([(A,T,Q)|TAIL], P, PPOSS) :- sort1(P, SP), filter(Q, SP, A, T, SPF), sfindpossacts(TAIL, P, POSS), union(POSS, SPF, PPOSS), !. % % sfindpossdels finds all possible delays that the agent may make % depending on the delays another agent may do. % sfindpossdels([], _, []) :- !. sfindpossdels([(D,Q0)|TAIL], P, PPOSSD) :- simdelay(P, D, P0), sfindpossdels(TAIL, P, PPOSS), insert((Q0,P0), PPOSS, PPOSSD), !. sfindpossdels([_|TAIL], P, PPOSSD) :- sfindpossdels(TAIL, P, PPOSSD), !. sdset([], EXT, EXT) :- !. sdset([(P,Q)|TAIL], EXT, DSET) :- sort1(P, S1P), sfindpossacts(S1P, Q, QPOSS), sort1(Q, S1Q), sfindpossacts(S1Q, P, PPOSS), sortd(P, SDP), sfindpossdels(SDP, Q, QPOSSD), sortd(Q, SDQ), sfindpossdels(SDQ, P, PPOSSD), subset(QPOSS, EXT), subset(PPOSS, EXT), subset(QPOSSD, EXT), subset(PPOSSD, EXT), sdset(TAIL, EXT, DSET), !. sdset([(P,Q)|_], EXT, DSET) :- sort1(P, S1P), sfindpossacts(S1P, Q, QPOSS), sort1(Q, S1Q), sfindpossacts(S1Q, P, PPOSS), sortd(P, SDP), sfindpossdels(SDP, Q, QPOSSD), sortd(Q, SDQ), sfindpossdels(SDQ, P, PPOSSD), union(EXT, QPOSS, E1), union(E1, PPOSS, E2), union(E2, QPOSSD, E3), union(E3, PPOSSD, ENEW), sdset(ENEW, ENEW, DSET), !. % % As the name implies eliminatedup eliminates the duplicates in a list. % eliminatedup([], []) :- !. eliminatedup([(P,Q)|TAIL], REST) :- member((Q,P), TAIL), eliminatedup(TAIL, REST), !. eliminatedup([(P,Q)|TAIL], [(P,Q)|REST]) :- \+ member((Q,P), TAIL), eliminatedup(TAIL, REST), !. seq(P, Q) :- init, sdset([(P,Q)], [(P,Q)], L), eliminatedup(L, L1), !, allcomb(L1, C), (member((P,Q), C);member((Q,P), C)), sbs(C,C), !, cleardb. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % weq : K x K % % weq checks whether two agents are weakly equivalent or not. It % simply tries ot find a weak bisimulation (P, Q) is a member of. To do % this first it finds the set of all possible derivatives of the agents % under interest, and then tries to find a weak bisimulation that is a subset % of this derivations set, and the agents under interest are members of. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % wfindpossacts finds the all possible actions an agent may perform depending % on an action of another action. % wfindpossacts([], _, []) :- !. wfindpossacts([(tau,T,Q)|TAIL], P, PPOSS) :- sort_darr(P, SP), filter(Q, SP, eps, T, SPF), wfindpossacts(TAIL, P, POSS), union(POSS, SPF, PPOSS), !. wfindpossacts([(A,T,Q)|TAIL], P, PPOSS) :- sort_darr(P, SP), filter(Q, SP, A, T, SPF), wfindpossacts(TAIL, P, POSS), union(POSS, SPF, PPOSS), !. % % wfindpossdels finds all possible transitions that the agent may stay idle % depending on the delays another agent may do. % wfindpossdels([], _, []) :- !. wfindpossdels([(D,Q)|TAIL], P, PPOSSD) :- sort_darr(P, SP), filter(Q, SP, eps, D, SPF), wfindpossdels(TAIL, P, POSS), union(POSS, SPF, PPOSSD), !. % % wdset finds all possible derivation trees of two agents. Then weq tries % to find a bisimulation which is a subset of these derivation trees. % wdset([], EXT, EXT) :- !. wdset([(P,Q)|TAIL], EXT, DSET) :- sort_darr(P, SDP), filtereps(SDP, SDPA), wfindpossacts(SDPA, Q, QPOSS), sort_darr(Q, SDQ), filtereps(SDQ, SDQA), wfindpossacts(SDQA, P, PPOSS), sortd(P, SDELP), wfindpossdels(SDELP, Q, QPOSSD), sortd(Q, SDELQ), wfindpossdels(SDELQ, P, PPOSSD), subset(QPOSS, EXT), subset(PPOSS, EXT), subset(QPOSSD, EXT), subset(PPOSSD, EXT), wdset(TAIL, EXT, DSET), !. wdset([(P,Q)|_], EXT, DSET) :- sort_darr(P, SDP), filtereps(SDP, SDPA), wfindpossacts(SDPA, Q, QPOSS), sort_darr(Q, SDQ), filtereps(SDQ, SDQA), wfindpossacts(SDQA, P, PPOSS), sortd(P, SDELP), wfindpossdels(SDELP, Q, QPOSSD), sortd(Q, SDELQ), wfindpossdels(SDELQ, P, PPOSSD), union(EXT, QPOSS, E1), union(E1, PPOSS, E2), union(E2, QPOSSD, E3), union(E3, PPOSSD, ENEW), wdset(ENEW, ENEW, DSET), !. weq(P, Q) :- init, wdset([(P,Q)], [(P,Q)], L), eliminatedup(L, L1), !, allcomb(L1, C), (member((P,Q), C);member((Q,P), C)), wbs(C,C), !, cleardb. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % init % % Initializes the "memory" by inserting some necessary predicates. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% init :- assert(dprefix(null, null, -1, -1, null2)), assert(dsum(null, null2, null2)), assert(dcom(null, null2, null2)), assert(dres(null, null)), assert(delaysof(null, [])), assert(arrowsof(nil, [])), assert(darrowsof(null, [])), assert(current(1000)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % cleardb % % Clears the "memory" by retracting inserted clauses. % % !ATTENTION! % After seq or weq is called if the predicate is satisfied then the memory % is cleaned automatically. But if the equivalence fails the memory has to % be cleaned manually! %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% cleardb :- retractall(dprefix(_,_,_,_,_)), retractall(dsum(_,_,_)), retractall(dcom(_,_,_)), retractall(dres(_,_)), retractall(delaysof(_,_)), retractall(arrowsof(_,_)), retractall(darrowsof(_,_)), retractall(current(_)).