% % epath.pl: create and manipulate epistemic path terms. % % Copyright 2008, Ryan Kelly % % Syntax for epistemic paths is: % % A - primitive agent name % E1 ; E2 - sequence % E1 | E2 - choice % ?(C) - test % E* - iteration % !(X:T) - nondet variable rebind with given type % -[X:V|..] - variable assignment % % % epath_not_refuted_values(E,VVIn,VVOut) - determine possible var values % % If path E is entered with variable bindings from the set VVIn, then % it will terminate with bindings from the set VVOut. % Each of these is a list mapping vars to a list of possible values, e.g. % [X:[a,b,c], Y:[f,g]]. Vars not in the mapping are allowed to take on % any value. % % Since this is a propositional domain, we can handle the star operator % as a simple fixpoint calculation and be sure it will eventually terminate. % epath_not_refuted_values(A,VV,VV) :- agent(A). epath_not_refuted_values(?(P),VVIn,VVOut) :- epath_not_refuted_values_test(VVIn,[],P,VVOut), vv_valid(VVOut). epath_not_refuted_values(!(X:T),VVIn,VVOut) :- bagof(Val,call(T,Val),Vals), vv_update(VVIn,X,Vals,VVOut). epath_not_refuted_values(-[],VVIn,VVIn). epath_not_refuted_values(-[X:V|Xs],VVIn,VVOut) :- vv_update(VVIn,X,[V],VV2), epath_not_refuted_values(-Xs,VV2,VVOut). epath_not_refuted_values(E1 ; E2,VVIn,VVOut) :- epath_not_refuted_values(E1,VVIn,VV2), epath_not_refuted_values(E2,VV2,VVOut). epath_not_refuted_values(E1 | E2,VVIn,VVOut) :- ( epath_not_refuted_values(E1,VVIn,VV1) -> ( epath_not_refuted_values(E2,VVIn,VV2) -> vv_merge(VV1,VV2,VVOut) ; VVOut = VV1 ) ; epath_not_refuted_values(E2,VVIn,VVOut) ). epath_not_refuted_values(E*,VVIn,VVOut) :- epath_not_refuted_values(E,VVIn,VV2), ( VV2 = VVIn -> VVOut = VV2 ; epath_not_refuted_values(E*,VV2,VVOut) ). epath_not_refuted_values_test([],_,_,[]). epath_not_refuted_values_test([X:Vs|Xs],Sofar,P,VVOut) :- partition(epath_not_refuted_values_allowed(P,X,Xs,Sofar),Vs,Vs1,_), VVOut = [X:Vs1|VVOut2], Sofar2 = [X:Vs1|Sofar], epath_not_refuted_values_test(Xs,Sofar2,P,VVOut2). epath_not_refuted_values_allowed(P,X,Others1,Others2,V) :- epath_not_refuted_values_allowed_sub1(P,Others1,P1), epath_not_refuted_values_allowed_sub1(P1,Others2,P2), subs(X,V,P2,P3), simplify(P3,P4), P4 \= false. epath_not_refuted_values_allowed_sub1(P,[],P). epath_not_refuted_values_allowed_sub1(P,[X:Vs|Xs],P2) :- member(Val,Vs), subs(X,Val,P,P1), epath_not_refuted_values_allowed_sub1(P1,Xs,P2). vv_valid([]). vv_valid([_:Vs|Xs]) :- Vs \= [], vv_valid(Xs). vv_update([],X,Vs,[X:Vs]). vv_update([X1:Vs1|Xs],X2,Vs2,Res) :- ( X1 == X2 -> Res = [X1:Vs2|Xs] ; Res = [X1:Vs1|Res2], vv_update(Xs,X2,Vs2,Res2) ). vv_merge([],VV2,VV2). vv_merge([X:Vs|Xs],VV1,Res) :- vv_merge1(VV1,X,Vs,VV2), vv_merge(Xs,VV2,Res). vv_merge1([],X,Vs,[X:Vs]). vv_merge1([X1:Vs1|Xs],X2,Vs2,Res) :- ( X1 == X2 -> union(Vs1,Vs2,VsU), Res = [X1:VsU|Xs] ; Res = [X1:Vs1|Res2], vv_merge1(Xs,X2,Vs2,Res2) ). % % epath_enum_vars(E,En) - enumerate all possible values of each path % variable in the epath, reducing it from FODL % to VPDL and hence making it decidable % % We expand any unions produced during enumeration over sequence operators, % in the hope that each branch will simplify given the new variable bindings. % We try to push var assignments as far to the right as possible, doing subs % into tests and simplifying. % epath_enum_vars(E1 ; E2,En) :- epath_enum_vars(E1,En1), flatten_op('|',[En1],Ens1), epath_enum_vars(E2,En2), flatten_op('|',[En2],Ens2), epath_enum_vars_branches(Ens1,Ens2,Ens), epath_build('|',Ens,En). epath_enum_vars(E1 | E2,En) :- flatten_op('|',[E1,E2],Es), maplist(epath_enum_vars,Es,Ens), epath_build('|',Ens,En). epath_enum_vars(E*,En) :- epath_enum_vars(E,EnS), epath_build('*',EnS,En). epath_enum_vars(?(P),?(P)). epath_enum_vars(-VA,-VA). epath_enum_vars(!(X:T),En) :- bagof(VA,V^(call(T,V),VA=(-[X:V])),VAs), epath_build('|',VAs,En). epath_enum_vars(A,A) :- agent(A). epath_enum_vars_branches([],_,[]). epath_enum_vars_branches([B|Bs],Es,[R|Rs]) :- ( epath_ends_with_assign(B,VA,Head) -> epath_enum_vars_branches_assign(Es,VA,Head,[],R) ; epath_enum_vars_branches_noassign(Es,B,[],R) ), epath_enum_vars_branches(Bs,Es,Rs). epath_enum_vars_branches_assign([],_,_,Acc,R) :- joinlist('|',Acc,R). epath_enum_vars_branches_assign([E|Es],VA,B,Acc,R) :- epath_push_assign(E,VA,Ea), epath_build(';',[B,Ea],R1), epath_enum_vars_branches_assign(Es,VA,B,[R1|Acc],R). epath_enum_vars_branches_noassign([],_,Acc,R) :- joinlist('|',Acc,R). epath_enum_vars_branches_noassign([E|Es],B,Acc,R) :- epath_build(';',[B,E],R1), epath_enum_vars_branches_noassign(Es,B,[R1|Acc],R). % % epath_ends_with_assign(E,VA,Head) - epath ends with a variable assignment % % This predicate is true when E ends with a unique variable assignment % operator. VA is bound to the assignment and Head is the remainder % of the path. % epath_ends_with_assign(E1 ; E2,VA,Head) :- epath_ends_with_assign(E2,VA2,Head2), ( Head2 = (?true) -> ( epath_ends_with_assign(E1,VA1,Head1) -> Head = Head1, vassign_merge(VA1,VA2,VA) ; Head = E1, VA=VA2 ) ; Head = (E1 ; Head2), VA=VA2 ). epath_ends_with_assign(E1 | E2,VA,Head) :- epath_ends_with_assign(E1,VA,Head1), epath_ends_with_assign(E2,VA2,Head2), VA == VA2, Head = (Head1 | Head2). epath_ends_with_assign(-(VA),VA,?true). % % epath_push_assign(E,VA,Ep) - push a variable assignment as far to the % right as possible. % % This may involve, for example, pushing it over a test operator and % substituting the assigned values into the test formula. % epath_push_assign(E1 ; E2,VA,Ep) :- epath_push_assign(E1,VA,Ep1), ( epath_ends_with_assign(Ep1,VA2,Head) -> epath_push_assign(E2,VA2,Ep2), epath_build(';',[Head,Ep2],Ep) ; epath_build(';',[Ep1,E2],Ep) ). epath_push_assign(E1 | E2,VA,Ep) :- epath_push_assign(E1,VA,Ep1), epath_push_assign(E2,VA,Ep2), epath_build('|',[Ep1,Ep2],Ep). epath_push_assign(E*,VA,(-VA) ; (E*)). epath_push_assign(!(X:T),VA,Ep) :- ( vassign_contains(VA,X) -> Ep = (-VA ; !(X:T)) ; Ep = (!(X:T) ; -VA) ). epath_push_assign(-VA2,VA,-VAm) :- vassign_merge(VA2,VA,VAm). epath_push_assign(?(P),VA,?(Q) ; -VA) :- vassign_subs(VA,P,Q1), simplify(Q1,Q). epath_push_assign(A,VA,A ; -VA) :- agent(A). % % Predicates for manipulating a variable assignment list % vassign_merge([],VA,VA). vassign_merge([(X:V)|Xs],VA2,VA) :- vassign_insert(X,V,VA2,VAt), vassign_merge(Xs,VAt,VA). vassign_insert(X,V,[],[X:V]). vassign_insert(X,V,[(X2:V2)|Xs],VA) :- ( X == X2 -> VA = [(X2:V2)|Xs] ; vassign_insert(X,V,Xs,VAs), VA = [(X2:V2)|VAs] ). vassign_contains([(X:_)|Xs],Y) :- X == Y ; vassign_contains(Xs,Y). vassign_subs([],P,P). vassign_subs([(X:V)|Xs],P,Q) :- subs(X,V,P,P2), vassign_subs(Xs,P2,Q). % % epath_vars(E,Vars) - find all path variables (as opposed to formula-level % variables) in the given epistemic path. % epath_vars(E1 ; E2,Vars) :- epath_vars(E1,Vars1), epath_vars(E2,Vars2), epath_vars_union(Vars1,Vars2,Vars), !. epath_vars(E1 | E2,Vars) :- epath_vars(E1,Vars1), epath_vars(E2,Vars2), epath_vars_union(Vars1,Vars2,Vars), !. epath_vars(E*,Vars) :- epath_vars(E,Vars), !. epath_vars(!(X:T),[X:T]) :- !. epath_vars(?(_),[]) :- !. epath_vars(-VA,VA) :- !. epath_vars(A,[]) :- agent(A). epath_vars_union([],Vars,Vars). epath_vars_union([X:T|Vars1],Vars2,Vars) :- (ismember(X:T,Vars2) -> epath_vars_union(Vars1,Vars2,Vars) ; Vars = [X:T|VarsT], epath_vars_union(Vars1,Vars2,VarsT) ). % % epath_build(Op,Args,EPath) - build an epath, with simplification % % This predicate builds an epath, applying simplifications appropriate % to the top-level operator but assuming all argument paths are already % simplified. % epath_build('|',Es,E) :- flatten_op('|',Es,Es0), partition('='(?false),Es0,_,Es1), simplify_epath_choice_subsumes(Es1,Es2), simplify_epath_choice_union(Es2,Es3), ( Es3 = [] -> E = (?false) ; joinlist('|',Es3,E) ). epath_build(';',Es,E) :- flatten_op(';',Es,Es0), ( member(?false,Es0) -> E = (?false) ; partition('='(?true),Es0,_,Es1), ( Es1 = [] -> E = (?true) ; simplify_epath_seq_combine(Es1,Ss), ( member(?false,Ss) -> E = (?false) ; joinlist(';',Ss,E) ) ) ). epath_build('*',E,Eb) :- simplify_star_contents(E,E1), ( E1 = (?(P)) -> Eb = (?(P)) ; Eb = (E1*) ). % % simplify_epath - simplify an epistemic path % % we can do this by recursively stripping off the outermost operator, % simplifying the argument paths, then apply epath_build. % simplify_epath(X,_) :- var(X), !, throw(cant_simplify_a_free_epath). simplify_epath(A,A) :- agent(A). simplify_epath(E1 ; E2,Es) :- flatten_op(';',[E1,E2],Eseq), maplist(simplify_epath,Eseq,Esimp), epath_build(';',Esimp,Es). simplify_epath(E1 | E2,Es) :- flatten_op('|',[E1,E2],Eseq), maplist(simplify_epath,Eseq,Esimp), epath_build('|',Esimp,Es). simplify_epath(E*,Es) :- simplify_epath(E,E1s), epath_build('*',E1s,Es). simplify_epath(?(P),?(S)) :- simplify(P,S). simplify_epath(!(X:T),!(X:T)). epath_elim_impossible_branches(A,_,A) :- agent(A). epath_elim_impossible_branches(?(P),VVPoss,?(P1)) :- ( epath_not_refuted_values(?(P),VVPoss,_) -> P1 = P ; P1 = false ). epath_elim_impossible_branches(!(X:T),_,!(X:T)). epath_elim_impossible_branches(-VA,_,-VA). epath_elim_impossible_branches(E1 ; E2,VVPoss,Er) :- ( epath_not_refuted_values(E1,VVPoss,VV2) -> epath_elim_impossible_branches(E1,VVPoss,Er1), epath_elim_impossible_branches(E2,VV2,Er2), (Er1 = ?false -> Er = ?false ; Er2 = ?false -> Er = ?false ; Er = (Er1 ; Er2) ) ; Er = (?false) ). epath_elim_impossible_branches(E1 | E2,VVPoss,Er) :- epath_elim_impossible_branches(E1,VVPoss,Er1), epath_elim_impossible_branches(E2,VVPoss,Er2), (Er1 = ?false -> Er = Er2 ; Er2 = ?false -> Er = Er1 ; Er = (Er1 | Er2) ). epath_elim_impossible_branches(E*,VVPoss,Er) :- ( epath_not_refuted_values(E*,VVPoss,VV2) -> epath_elim_impossible_branches(E,VV2,E2), (E2 = ?false -> Er = ?false ; Er = (E2*) ) ; Er = (?false) ). % % Simplification for operations within a star. % simplify_star_contents(E1,E2) :- ( simplify_star_contents1(E1,Es) -> simplify_star_contents(Es,E2) ; E2 = E1 ). simplify_star_contents1(E*,E). % Any choices within a star that are simply ?true can be removed, % as we always have the option of staying in current state. simplify_star_contents1(E1 | E2,Ep) :- flatten_op('|',[E1,E2],Es), partition('='(?true),Es,Ts,Es2), length(Ts,N), N > 0, joinlist('|',Es2,Ep). % % Flatten stars in (B1* | (B2* | B3*)*)* simplify_star_contents1(E,Ep) :- ( E = ((B1*) | (((B2*) | (B3*))*)) ; E = ((((B1*) | (B2*))*) | (B3*)) ) -> Ep = ((B1*) | (B2*) | (B3*)). % % Remove choices that are subsumed by repetition of another branch simplify_star_contents1(E1 | E2,Ep) :- flatten_op('|',[E1,E2],Es), simplify_epath_star_subsumes(Es,Ss), joinlist('|',Ss,Ep). simplify_epath_star_subsumes(Es,Ss) :- simplify_epath_star_subsumes(Es,[],0,Ss). simplify_epath_star_subsumes([],Acc,1,Acc). simplify_epath_star_subsumes([E|Es],Acc,HaveSimpd,Ss) :- ( member(E2,Acc), epath_subsumes(E2*,E) -> simplify_epath_star_subsumes(Es,Acc,1,Ss) ; partition(epath_subsumes(E*),Acc,Rem,Acc2), ( Rem = [] -> NewHaveSimpd = HaveSimpd ; NewHaveSimpd = 1 ), simplify_epath_star_subsumes(Es,[E|Acc2],NewHaveSimpd,Ss) ). % % simplify branches in a choice by removing any subsumed by another branch % simplify_epath_choice_subsumes(Es,Ss) :- simplify_epath_choice_subsumes(Es,[],Ss). simplify_epath_choice_subsumes([],Acc,Acc). simplify_epath_choice_subsumes([E|Es],Acc,Ss) :- ( member(E2,Acc), epath_subsumes(E2,E) -> simplify_epath_choice_subsumes(Es,Acc,Ss) ; partition(epath_subsumes(E),Acc,_,Acc2), simplify_epath_choice_subsumes(Es,[E|Acc2],Ss) ). % % simplify branches in a choice by combining two branches into a single, % simpler branch giving their union. % simplify_epath_choice_union(Es,Ss) :- simplify_epath_choice_union(Es,[],Ss). simplify_epath_choice_union([],Acc,Acc). simplify_epath_choice_union([E|Es],Acc,Ss) :- ( (select(E1,Acc,Rest), simplify_epath_union(E,E1,Eu)) -> simplify_epath_choice_union([Eu|Es],Rest,Ss) ; simplify_epath_choice_union(Es,[E|Acc],Ss) ). % % simplify_epath_seq_combine(Es,Ss) - simplify sequence of paths by % combining adjacent ones. % simplify_epath_seq_combine(Es,Ss) :- simplify_epath_seq_combine(Es,[],Ss). simplify_epath_seq_combine([E],Acc,Ss) :- reverse([E|Acc],Ss). simplify_epath_seq_combine([E|Es],Acc,Ss) :- ( simplify_epath_combine([E|Es],Es2) -> simplify_epath_seq_combine_recheck(Es2,Acc,Ss) ; simplify_epath_seq_combine(Es,[E|Acc],Ss) ). :- index(simplify_eapth_seq_combine_recheck(0,1,0)). simplify_epath_seq_combine_recheck(Es,[],Ss) :- simplify_epath_seq_combine(Es,[],Ss). simplify_epath_seq_combine_recheck(Es,[A|Acc],Ss) :- ( simplify_epath_combine([A|Es],Es2) -> simplify_epath_seq_combine_recheck(Es2,Acc,Ss) ; simplify_epath_seq_combine(Es,[A|Acc],Ss) ). % % epath_subsumes(E1,E2) - detect common cases where one epath completely % subsumes another. That is, all worlds reachable % by path E2 are also reachable by path E1. % % epath_subsumes/2 is det, which we ensure using cuts % epath_subsumes(E,E) :- !. epath_subsumes(E*,E1*) :- epath_subsumes(E*,E1), !. epath_subsumes(E*,E1) :- epath_subsumes(E,E1), !. epath_subsumes(E*,E1) :- epath_seq_split(E1,[P1,P2],[]), epath_subsumes(E*,P1), epath_subsumes(E*,P2), !. epath_subsumes(E,E1 | E2) :- epath_subsumes(E,E1), epath_subsumes(E,E2), !. epath_subsumes(E1 | E2,E) :- (epath_subsumes(E1,E) ; epath_subsumes(E2,E)), !. epath_subsumes(E1 ; E2,E) :- epath_seq_split(E,[P1,P2],[]), epath_subsumes(E1,P1), epath_subsumes(E2,P2), !. % % simplify_epath_union(E1,E2,Eu) - simplify E1 and E2 into their union % (E1 | E2) <=> Eu % % simplify_epath_combine(Es,Esc) - simplify E1;E2;P into Ec;P % % This basically allows us to special-case a number of common forms. % simplify_epath_union(E1,E2,Eu) :- simplify_epath_union1(E1,E2,Eu) ; simplify_epath_union1(E2,E1,Eu). % P1 | (P1 ; P2* ; P2) => P1 ; P2* simplify_epath_union1(E1,E2,Eu) :- P1 = E1, epath_seq_split(E2,[P1,P2*,P2],[]), epath_build('*',P2,P2S), epath_build(';',[P1,P2S],Eu). % P1 | (P2 ; P2* ; P1) => P2* ; P1 simplify_epath_union1(E1,E2,Eu) :- P1 = E1, epath_seq_split(E2,[P2,P2*,P1],[]), epath_build('*',P2,P2S), epath_build(';',[P2S,P1],Eu). % P1 | (P2* ; P2 ; P1) => P2* ; P1 simplify_epath_union1(E1,E2,Eu) :- P1 = E1, epath_seq_split(E2,[P2*,P2,P1],[]), epath_build('*',P2,P2S), epath_build(';',[P2S,P1],Eu). % ?P1 | ?P2 => ?(P1 | P2) simplify_epath_union1(?P1,?P2,?Pu) :- fml2cnf(P1 | P2,Pu1), simplify(Pu1,Pu). % P1* ; (P2 ; (P1*))* => (P1* | P2*)* simplify_epath_combine(E,[Ec|Rest]) :- epath_seq_split(E,[P1*,Pr*],Rest), epath_seq_split(Pr,[P2,P1*],[]), epath_build('|',[P1*,P2*],Ec1), epath_build('*',Ec1,Ec). % (P1* ; P2)* ; P1* => (P1* | P2*)* simplify_epath_combine(E,[Ec|Rest]) :- epath_seq_split(E,[Pr*,P1*],Rest), epath_seq_split(Pr,[P1*,P2],[]), epath_build('|',[P1,P2],Ec1), epath_build('*',Ec1,Ec). % (P1* ; P2)* ; P1 ; P1* => (P1* | P2*)* simplify_epath_combine(E,[Ec|Rest]) :- epath_seq_split(E,[Pr*,P1,P1*],Rest), epath_seq_split(Pr,[P1*,P2],[]), epath_build('|',[P1,P2],Ec1), epath_build('*',Ec1,Ec). % P1* ; P2* => P1* if P1 > P2 simplify_epath_combine(E,[Ec|Rest]) :- epath_seq_split(E,[P1*,P2*],Rest), ( epath_subsumes(P1,P2), Ec = P1 ; epath_subsumes(P2,P1), Ec = P2 ). % ?P1 ; ?P2 => ?(P1 & P2) simplify_epath_combine(E,[?(Pc)|Rest]) :- epath_seq_split(E,[?P1,?P2],Rest), fml2cnf(P1 & P2,Pc1), simplify(Pc1,Pc). % % epath_seq_split(E,Seqs,Rest) - nondeterminstically split sequence of ops % % This predicate nondeterministically splits a series of sequence operators % into patterns that match the elements of the list Seqs. Each free var in % Seqs may be given one or more elements from the sequence, while each % any entries in Seq that are nonvar will be unified with precisely one % element. % :- index(epath_seq_split(1,1,0)). epath_seq_split(E1 ; E2,Seqs,Rest) :- flatten_op(';',[E1,E2],Es), epath_seq_split_prep(Seqs,Preps), epath_seq_split(Es,Preps,Rest), epath_seq_split_unprep(Preps,Seqs). epath_seq_split([E|Es],Seqs,Rest) :- epath_seq_split([E|Es],[],Seqs,Rest). epath_seq_split(Rest,[],[],Rest). epath_seq_split(Rest,[S-Vs|Todo],[],Rest) :- reverse(Vs,VsR), ( var(S) -> S = VsR ; joinlist(';',VsR,S) ), epath_seq_split(Rest,Todo,[],Rest). epath_seq_split([E|Es],Todo,[S|Seqs],Rest) :- ( var(S) -> ((Todo = [S2-Vs|Todo2], S2 == S) -> (epath_seq_split([E|Es],Todo,Seqs,Rest) ; epath_seq_split(Es,[S-[E|Vs]|Todo2],[S|Seqs],Rest)) ; epath_seq_split(Es,[S-[E]|Todo],[S|Seqs],Rest) ) ; epath_seq_split_unify(S,[E|Es],Es2), epath_seq_split(Es2,Todo,Seqs,Rest) ). epath_seq_split([],Todo,[S],Rest) :- var(S), Todo = [S2-_|_], S2 == S, epath_seq_split([],Todo,[],Rest). epath_seq_split_unify(P,[E|Es],Es) :- var(P), P=E, !. epath_seq_split_unify(P1 ; P2,Es,Es2) :- epath_seq_split_unify(P1,Es,Es1), epath_seq_split_unify(P2,Es1,Es2), !. epath_seq_split_unify(E,[E|Es],Es). epath_seq_split_prep([],[]). epath_seq_split_prep([S|Seqs],[P|Preps]) :- (var(S) -> true ; S=P ), epath_seq_split_prep(Seqs,Preps). epath_seq_split_unprep([],[]). epath_seq_split_unprep([P|Preps],[S|Seqs]) :- ( P = [_|_] -> joinlist(';',P,S) ; P=S ), epath_seq_split_unprep(Preps,Seqs). % % copy_epath(EIn,EOut) - copy an epath, renaming path variables % % This produces a copy of EIn with all path variables replaced by % fresh variables. All free formula variables remain unchanged, while % all bound formula variables are also renamed. % copy_epath(E,Ec) :- epath_vars(E,EVarsT), maplist(arg(1),EVarsT,EVars), term_variables(E,TVars), vdelete_list(TVars,EVars,FVars), copy_term(E^FVars,E2^FVars2), FVars2=FVars, copy_epath_fmls(E2,Ec). copy_epath_fmls(E1 ; E2,E1c ; E2c) :- copy_epath_fmls(E1,E1c), copy_epath_fmls(E2,E2c). copy_epath_fmls(E1 | E2,E1c | E2c) :- copy_epath_fmls(E1,E1c), copy_epath_fmls(E2,E2c). copy_epath_fmls(E*,Ec*) :- copy_epath_fmls(E,Ec). copy_epath_fmls(?(P),?(Pc)) :- copy_fml(P,Pc). copy_epath_fmls(!(V:T),!(V:T)). copy_epath_fmls(-VA,-VA). copy_epath_fmls(A,A) :- agent(A). % % pp_epath(E) - pretty-print an epistemic path % pp_epath(E) :- pp_epath(E,0,0). pp_epath_list([E],_,_,O1,D1) :- pp_epath(E,O1,D1). pp_epath_list([E1,E2|Es],Op,D,O1,D1) :- pp_epath(E1,O1,D1), nl, pp_inset(D), write(Op), nl, pp_epath_list([E2|Es],Op,D,D1,D1). pp_epath(E1 ; E2,O,D) :- flatten_op(';',[E1,E2],Es), D1 is D + 1, O1 is O + 1, pp_epath_list(Es,';',D,O1,D1). pp_epath(E1 | E2,O,D) :- flatten_op('|',[E1,E2],Es), D1 is D + 1, O1 is O + 1, pp_epath_list(Es,'|',D,O1,D1). pp_epath(?(P),O,D) :- D1 is D + 1, pp_inset(O), write('? '), pp_fml(P,0,D1). pp_epath(!(V:T),O,_) :- pp_inset(O), write('! '), write(V:T). pp_epath(-VA,O,_) :- pp_inset(O), write('- '), pp_epath_assign(VA). pp_epath(E*,O,D) :- D1 is D + 1, pp_inset(O), write('*'), nl, pp_epath(E,D1,D1). pp_epath(A,O,_) :- agent(A), pp_inset(O), write(A). pp_epath_assign([]). pp_epath_assign([(X:V)|Xs]) :- write(X), write(' <= '), write(V), write(', '), pp_epath_assign(Xs).