%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=<N, combination(L,N2,N,C)).

% Finds N, N-1, ..., 0 combinations of a list, where N is the number of
% elements in the list
allcomb(L, C) :- count(L, N), !, combination(L, 1, N, C).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% dotsub : T x T x T
%
%    The dot-subtraction (or conditional subtraction) of Chen.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dotsub(X, Y, RES) :- X < Y, RES is 0.
dotsub(X, Y, RES) :- X >= 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=<U, ontime(L1, U, T).

%
% Transition rules for an agent constructed by prefix combinator
%
arrow(P, A, T, Q) :- 
    (prefix(P, A, L, U, Q);dprefix(P, A, L, U, Q)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR), 
    \+ dres(P, A), \+ dres(P, ABAR), ontime(L, U, T).

%
% Transition rules for an agent constructed by summation combinator
%
arrow(P, A, T, Q) :- 
    (sum(P, P1, _);dsum(P, P1, _)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR),
    \+ dres(P, A), \+ dres(P, ABAR), arrow(P1, A, T, Q).
arrow(P, A, T, Q) :- 
    (sum(P, _, P2);dsum(P, _, P2)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR),
    \+ dres(P, A), \+ dres(P, ABAR), arrow(P2, A, T, Q).
%
% Transition rules for an agent constructed by parallel composition
% combinator
% Here we may need new agent definitions for the agent that our original
% agent evolves into. First an identical definition in the database is
% seeked. If one can be found, then it is used. Otherwise a new agent
% definition is inserted into the database with composition combinator,
% and predicate 'dcom' is used for this purpose.
%
arrow(P, tau, T, Q) :-
    (com(P, P1, P2);dcom(P, P1, P2)),
    arrow(P1, A, T, P1P), complement(A, ABAR), arrow(P2, ABAR, T, P2P),
    (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)).
arrow(P, tau, T, Q) :-
    (com(P, P1, P2);dcom(P, P1, P2)),
    arrow(P1, A, T, P1P), complement(A, ABAR), arrow(P2, ABAR, T, P2P),
    \+ (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)),
    current(NEW), NEW1 is NEW+1, retract(current(NEW)), assert(current(NEW1)),
    assert(dcom(NEW, P1P, P2P)), Q is NEW, \+ setrest(P, Q).
arrow(P, A, T, Q) :-
    (com(P, P1, P2);dcom(P, P1, P2)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR), \+ dres(P, A),
    \+ dres(P, ABAR), arrow(P1, A, T, P1P), simdelay(P2, T, P2P), 
    (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)).
arrow(P, A, T, Q) :-
    (com(P, P1, P2);dcom(P, P1, P2)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR), \+ dres(P, A), 
    \+ dres(P, ABAR), arrow(P1, A, T, P1P), simdelay(P2, T, P2P), 
    \+ (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)),
    current(NEW), NEW1 is NEW+1, retract(current(NEW)), assert(current(NEW1)),
    assert(dcom(NEW, P1P, P2P)), Q is NEW, \+ setrest(P, Q).
arrow(P, A, T, Q) :-
    (com(P, P1, P2);dcom(P, P1, P2)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR), \+ dres(P, A), 
    \+ dres(P, ABAR), arrow(P2, A, T, P2P), simdelay(P1, T, P1P), 
    (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)).
arrow(P, A, T, Q) :-
    (com(P, P1, P2);dcom(P, P1, P2)),
    complement(A, ABAR), \+ res(P, A), \+ res(P, ABAR), \+ dres(P, A),
    \+ dres(P, ABAR), arrow(P2, A, T, P2P), simdelay(P1, T, P1P), 
    \+ (com(Q, P1P, P2P);com(Q, P2P, P1P);dcom(Q, P1P, P2P);dcom(Q, P2P, P1P)),
    current(NEW), NEW1 is NEW+1, retract(current(NEW)), assert(current(NEW1)),
    assert(dcom(NEW, P1P, P2P)), Q is NEW, \+ setrest(P, Q).


%
% sort1 finds immediate actions that an agent may perform and returns a set of
% (P, T, Q), where P is the agent under interest, T is the time when
% the action is (or may be) performed, and Q is the agent P evolves into.
% Like sortd it computes this set just once, and then saves a copy in the 
% database, and returns this copy when it is called with the same arguments
% again.
%
findacts(P, L, SORT1) :- 
    arrow(P, A, T, Q), \+ member((A,T,Q), L),
    insert((A,T,Q), L, LP), !, findacts(P, LP, SORT1).
findacts(_, L, SORT1) :- 
    insert(void, L, SORT1), !.

sort1(P, SORT1) :- arrowsof(P, SORT1), !.
sort1(P, SORT1) :- findacts(P, [], SORT1),
                   assert(arrowsof(P, SORT1)), !.

simarrow(P, A, T, Q) :- 
    sort1(P, S1), !, member((A,T,Q), S1). 



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% darrow : K x Act x T x K
%
%    Defines the new labelled transition relation.
%
%    darrow(p, a, u, q) means; 
%          a
%       P ===> 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(_)).


