%---------------------------------------------------------- % "sciff.pl" % % Author: Marco Alberti % Created: Sept. 29, 2003 % % Modified by: Federico Chesani % Modified at: Aug. 30, 2005 % % Modified by: Federico Chesani % Modified at: Dec. 01, 2005 % % % Version: 1.00.01 %---------------------------------------------------------- %:- multifile(fdet/1). %:- dynamic(fdet/1). %---------------------------------------------------------- % CONSULTING THE MODULES %---------------------------------------------------------- :- multifile(user:cell/4). :- dyanmic(user:cell/4). cell(0,0,yellow,arm). cell(0,1,default,empty). cell(0,2,blue,money). cell(0,3,default,empty). cell(0,4,default,empty). cell(0,5,default,empty). cell(0,6,yellow,star). cell(0,7,yellow,book). cell(1,0,red,paper). cell(1,1,blue,money). :- use_module(library(terms)). :- use_module(reified_unif). :- use_module(prolog_version). :- (is_dialect(swi) -> use_module(swi_specific), [my_chr_extensions] % In SWI, my_chr_extensions must be loaded after reified_unif ; is_dialect(sicstus) -> ensure_loaded(my_chr_extensions), use_module(sicstus_specific) ; write('Unrecognized Prolog System'), nl, fail ). :- use_module(library(chr)). :- use_module(proof_util). :- use_module(quantif). :- use_module(ccopy). :- use_module(ics_quant). :- use_module(library(lists)). % [append/3, % delete/3, % nth/4, % member/2]). :- use_module(library(terms), [term_variables/2]). %:- ensure_loaded(solver). :- use_module(solver). %:- use_module(domains). :- use_module(history_parser). :- use_module(sokb_parser). :- use_module(ics_parser). :- use_module(sciff_options). :- use_module(debug). :- use_module(help). :- use_module(graphviz). :- ensure_loaded(defaults). :- use_module(library(clpfd)). % used by invert_constraint in SWI, and in old SCIFF code (e.g., block world) :- [pretty_print]. :- use_module(library(chr)). %---------------------------------------------------------- % DECLARATIONS %---------------------------------------------------------- %handler society_proof. %option(already_in_store,on). :- chr_option(debug,on). % Se lo metto on mi da` un errore %---------------------------------------------------------- % IMPOSING IC/PSIC % % Quantify the variables in an imposed IC, and impose the result as a % PSIC %---------------------------------------------------------- :- chr_constraint(( ic/2, psic/2)). impose_ics @ ic(Body1,Head1) ==> %unfold_nonrecursive(psic(Body1,Head1),PSIC), %impose_psic(PSIC). convert_to_psic(ic(Body1,Head1),PSIC), call(PSIC). %psic(BodyPSIC,HeadPSIC). convert_to_psic(ic(Body1,Head1),PSIC):- unfold_nonrecursive(psic(Body1,Head1),NewPSIC), (NewPSIC = psic(BodyUnf,HeadUnf) -> quantify_variables_in_ics(ics(BodyUnf,HeadUnf), ics(Body2,Head2)), rewrite_body_terms(Body2,Body3), BodyPSIC=Body3, HeadPSIC=Head2, PSIC=psic(BodyPSIC,HeadPSIC) ; PSIC=true). %---------------------------------------------------------- % IMPOSING VARIOUS CONSTRAINTS %---------------------------------------------------------- :- chr_type (functarity ---> [any,int]). :- chr_type (posexp ---> e(functarity,?,int)). :- chr_type (list(T) ---> [] ; [T | list(T)]). :- chr_constraint h/3, en/3, note/2, noten/2, fulf/1, viol/1, pending/1, abd/3, e/3. %e(+functarity,?,?int). %ground_time/0. get_functor(do(_,_,Main,_),[F,A]):- !, functor(Main,F,A). get_functor(do(_,_,_,Main,_),[F,A]):- !, functor(Main,F,A). get_functor(Main,[F,A]):- !, functor(Main,F,A). h(Event,Time):- get_functor(Event,F), h(F,Event,Time). e(Event,Time):- get_functor(Event,F), e(F,Event,Time). en(Event,Time):- get_functor(Event,F), en(F,Event,Time). abd(Event,Time):- get_functor(Event,F), abd(F,Event,Time). % In SICStus 4 there is no remove_constraint, so we remove constraints % with simpagation rules fulf(e(F,EEvent,ETime)) \ pending(e(F,EEvent,ETime)) <=> true. viol(en(F,EEvent,ETime)) \ pending(en(F,EEvent,ETime)) <=> true. viol(e(F,EEvent,ETime)) \ pending(e(F,EEvent,ETime)) <=> true. viol(gt_current_time(e(F,Event,Time), _)) \ pending(e(F,Event,Time)) <=> true. % Adds the [functor,arity] term to expectations & happened events % in the body of ICs. rewrite_body_terms([H,NotH,E,NotE,En,NotEn,Abd,A],[H1,NotH,E1,NotE,En1,NotEn,Abd1,A]):- rewrite_body_atom(H,H1), rewrite_body_atom(E,E1), rewrite_body_atom(Abd,Abd1), rewrite_body_atom(En,En1). rewrite_body_atom([],[]). rewrite_body_atom([h(E,T)|LH],[h(F,E,T)|LH1]):- get_functor(E,F), rewrite_body_atom(LH,LH1). rewrite_body_atom([e(E,T)|LH],[e(F,E,T)|LH1]):- get_functor(E,F), rewrite_body_atom(LH,LH1). rewrite_body_atom([en(E,T)|LH],[en(F,E,T)|LH1]):- get_functor(E,F), rewrite_body_atom(LH,LH1). rewrite_body_atom([abd(E,T)|LH],[abd(F,E,T)|LH1]):- get_functor(E,F), rewrite_body_atom(LH,LH1). %---------------------------------------------------------- % EVENT CALCULUS and FACTORING % % To carefully think about it... %---------------------------------------------------------- % Questo andrebbe messo come IC. % Non posso avere 2 eventi nello stesso tempo sequential_act @ e([act,1],act(E1),T1) \ e([act,1],act(E2),T2) <=> sciff_option(seq_act,on), T2=T1 | E1=E2. % factoring % This factoring is specilised for the abductive event calculus % Questo factoring va legato ad una regola che toglie uno degli abd % se ce ne sono 2 identici. Nel caso dell'EC c'e` gia` (che vieta 2 eventi % nello stesso tempo). %factoring_ec @ % e(act(X1),T1), e(act(X2),T2) % ==> % sciff_option(factoring,on), % nonvar(X1), nonvar(X2) | % reif_unify(e(act(X1),T1),e(act(X2),T2),B), % (B=1 ; B=0). %% Secondo tentativo: fa l'unificazione dei tempi solo se l'azione %% e` gia` ground factoring2 @ e(F,X,T1), e(F,X,T2) ==> sciff_option(factoring,on), ground(X) | (eq(T1,T2) ; neq(T1,T2), when(?=(T1,T2),T1\==T2)). % La seconda serve perche' cosi` se e` la stessa var fallisce % senza dover usare la (poca) propagazione del diverso. %% T1 #= T2 #<=> B, %% (B=1 ; B=0). %---------------------------------------------------------- % ITERATIVE DEEPENING: max number of e(act(...)). %---------------------------------------------------------- :- chr_constraint max_depth/1. max_depth_e_act @ e([act,1],act(_),_), max_depth(DepthMax) ==> %findall_constraints(e(_,act(_),_),L), length(L,N), N>DepthMax | fail. max_constraints(e(_,act(_),_),DepthMax). %%%MARCOM max_depth_e_act @ h([sono,4],sono(_,_,_,_),_), max_depth(DepthMax) ==> findall_constraints(h(_,sono(_,_,_,_),_),L), length(L,N), N>DepthMax | writeln(ciao(N)),fail. %max_constraints(e(_,sono(_,_,_,_),_),DepthMax). %---------------------------------------------------------- % ITERATIVE DEEPENING: max number of violation %---------------------------------------------------------- :- chr_constraint max_viol/1. max_violations @ viol(_), max_viol(MaxViol) ==> findall_constraints(viol(_),L), %write(L), length(L,N), write(N) | lt(MaxViol,1000), leq(N,MaxViol). e_consistency @ e(F,EEvent,ETime), en(F,ENEvent,ENTime) ==> %findall_constraints(gen_phase,[]) | %add_arc_graph('E-consistency',e(EEvent,ETime)\=en(ENEvent,ENTime)), check_unification(p(EEvent,ETime),p(ENEvent,ENTime),0,e,en). % pending_en @ en(F,Event,Time) ==> pending(en(F,Event,Time)). :- chr_constraint nondeterministic/1, phase/1, remove_phase/0. propagation_h @ h(F,Event1,Time1), psic([[h(F,Event2,Time2)|MoreH],NotH,E,NotE,En,NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([[h(Event2,Time2)|MoreH],NotH,E,NotE,En,NotEn,Abd,A],Head), p([[h(Event2a,Time2a)|MoreHa],NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada)), (subsumeschk(p(Event2a,Time2a),p(Event1,Time1)), is_term_quantified(h(Event2a,Time2a),forall) -> %reif_unify(p(Event1,Time1),p(Event2a,Time2a),1), (Event1=Event2a, Time1=Time2a -> psic([MoreHa,NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada) ; true) ; reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), PSIC=psic([MoreHa,NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada), (B==1 -> call(PSIC) ; B==0 -> true ; nondeterministic((B=1, call(PSIC); B=0)) ) ). propagation_e @ e(F,Event1,Time1), psic([[],NotH,[e(F,Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head), p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)), reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), status(S,F), (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)), B=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada) ; draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)), B=0). % End modification % Original version: /* propagation_e @ e(Event1,Time1), psic([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head), p([Ha,NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)), reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), status(S,F), (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)), B#=1, psic([Ha,NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada) ; draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)), B#=0). */ % End Original version % Modified by Federico Chesani % Date 20060404 1230 propagation_note @ note(Event1,Time1), psic([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head), p([[],NotHa,[],[note(Event2a,Time2a)|MoreNotEa],Ena,NotEna,Abda,Aa],Heada)), reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), (B=1, psic([[],NotHa,[],MoreNotEa,Ena,NotEna,Abda,Aa],Heada); B=0). % End Modification % Original Version: /* propagation_note @ note(Event1,Time1), psic([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([H,NotH,E,[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head), p([Ha,NotHa,Ea,[note(Event2a,Time2a)|MoreNotEa],Ena,NotEna,Abda,Aa],Heada)), reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), (B#=1, psic([Ha,NotHa,Ea,MoreNotEa,Ena,NotEna,Abda,Aa],Heada); B#=0). */ /* propagation_e @ e(F,Event1,Time1), psic([[],NotH,[e(F,Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head), p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)), reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), status(S,F), (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)), B#=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada) ; draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)), B#=0). */ propagation_en @ en(F,Event1,Time1), psic([[],NotH,[],[],[en(F,Event2,Time2)|MoreEn],NotEn,Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy(p([[],NotH,[],[],[en(Event2,Time2)|MoreEn],NotEn,Abd,A],Head), p([[],NotHa,[],[],[en(Event2a,Time2a)|MoreEna],NotEna,Abda,Aa],Heada)), ccopy( p( Event1, Time1), p( Event1a, Time1a)), reif_unify(p(Event1a,Time1a),p(Event2a,Time2a),B), (B=1, psic([[],NotHa,[],[],MoreEna,NotEna,Abda,Aa],Heada); B=0). propagation_noten @ noten(Event1,Time1), psic([[],NotH,[],[],[],[noten(Event2,Time2)|MoreNotEn],Abd,A],Head) ==> fn_ok(Event1,Event2) | ccopy( p([[], NotH, [], [], [], [noten(Event2, Time2)| MoreNotEn], Abd,A], Head), p([[],NotHa,[],[],[],[noten(Event2a,Time2a)|MoreNotEna],Abda,Aa],Heada)), ccopy( p( Event1, Time1), p( Event1a, Time1a)), reif_unify(p(Event1a,Time1a),p(Event2a,Time2a),B), ( B=1, psic([[],NotHa,[],[],[],MoreNotEna,Abda,Aa],Heada) ; B=0). propagation_abd @ abd(F,Event1,Time1), psic([[],NotH,[],[],[],[],[abd(F,Event2,Time2)|MoreAbd],A],Head) ==> fn_ok(Event1,Event2) | %ccopy(p([[],NotH,[],[],[],[],[abd(Event2,Time2)|MoreAbd],A],Head), % p([[],NotHa,[],[],[],[],[abd(Event2a,Time2a)|MoreAbda],Aa],Heada)), ccopy(p(NotH, Event2, Time2, MoreAbd, A, Head), p(NotHa,Event2a,Time2a,MoreAbda,Aa,Heada)), (subsumeschk(p(Event2a,Time2a),p(Event1,Time1)), is_term_quantified(abd(Event2a,Time2a),forall) -> (Event2a = Event1, Time2a=Time1 -> psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada) ; true) ; reif_unify(p(Event1,Time1),p(Event2a,Time2a),B), (B=1, psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada); B=0) ). propagation_violated @ viol(Event1), psic([[],NotH,[],[],[],[],[abd([viol,1],viol(Event2),_Time2)|MoreAbd],A],Head) ==> sciff_option(violation_causes_failure,no), fn_ok(Event1,Event2) | ccopy(p([[],NotH,[],[],[],[],[viol(Event2)|MoreAbd],A],Head), p([[],NotHa,[],[],[],[],[viol(Event2a)|MoreAbda],Aa],Heada)), reif_unify(p(Event1),p(Event2a),B), % (B#=1, psic([[],NotHa,[],NotEa,ENa,NotEna,MoreAbda,Aa],Heada); (B=1, psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada); B=0). % Two terms may be unifiable. % Profiled version, nearly twice as fast fn_ok(Term1,Term2):- Term1 == Term2,!. % either if they are identical fn_ok(Term1,Term2):- \+(?=(Term1,Term2)). % or if they are syntactically unifiable /* old version fn_ok(Term1,Term2):- nonvar(Term1), nonvar(Term2), !, Term1=..[H|T1], Term2=..[H|T2], fn_ok_list(T1,T2). fn_ok(_,_). */ fn_ok_list([],[]). fn_ok_list([H1|T1],[H2|T2]):- fn_ok(H1,H2), fn_ok_list(T1,T2). split_list(List,1,[],List):- !. split_list([Head|Tail],N,[Head|Tail1],Rest):- N1 is N-1, split_list(Tail,N1,Tail1,Rest). type_position(h,1). type_position(noth,2). type_position(e,3). type_position(note,4). type_position(en,5). type_position(noten,6). logical_equivalence @ % psic(true,Head) MarcoG: questa mi sembra obsoleta ... psic([[],[],[],[],[],[],[],[]],Head) <=> add_arc_graph(logical_equivalence,(true->Head)), impose_head1(Head). naf(Goal):- commas_to_list(Goal,GoalList), ics_quant:split_body(GoalList,Body), psic(Body,[]). unfold_psic @ psic([[],[],[],[],[],[],[],Atoms],Head) <=> %status(S,F), %draw_graph(S, unfolding_psic, Atoms), unfold([psic(Atoms,Head)]). unfold([]):- !. unfold([psic([],Head)|MorePSICS]):- !, % MarcoG Bug fix: the cut was after the call to psic. % psic is a CHR constraint, that is rewritten to a Prolog predicate % that embeds in its definitions the CHR rules that involve the constraint psic. % So, by adding a cut after this, we are cutting the choice points inside % the rules that involve psic, so sometimes it cuts alternatives in the % head!! %psic([[],[],[],[],[],[],[],[]],Head), impose_head1(Head), unfold(MorePSICS). unfold([psic([naf(Goal)|Body],Head)|PSICS]):- !, commas_to_list(Goal,GoalList), append(Head,[GoalList],NewHead), psic([[],[],[],[],[],[],[],Body],NewHead), unfold(PSICS). unfold([psic([clp_constraint(Constraint)|MoreBodyAtoms],Head)|MorePSICS]):- call(Constraint), unfold([psic(MoreBodyAtoms,Head)|MorePSICS]). unfold([psic([clp_constraint(Constraint)|_MoreBodyAtoms],_Head)|MorePSICS]):- !, % MarcoG: metto una pezza, perche' il vincolo a volte e` una restriction % e non riesce a fare st(C) #<=> 0, pero` si puo` fare st(C) #<=> 0 invert_constraint(Constraint), unfold(MorePSICS). % MarcoG 12 jul 2006: Sometimes the clause generated with % unfolding contains the explicit quantification of a % variable. The quantification is different in PSICs. % I ignore it for the moment, but maybe it should be % considered better ... unfold([psic([quant(_,_)|Body],Head)|MorePSICS]):- !, unfold([psic(Body,Head)|MorePSICS]). % Federico 08 Jun 2007: Managing abducibles introduced by previous unfolding unfold([psic([AnAtom|Body],Head)|PSICS]):- is_SCIFF_RESERVED(AnAtom), !, ic([AnAtom|Body],Head), unfold(PSICS). %%% MARCOM: Aggiunta ad-hoc per trattare la negazione di holds_at in mutua esclusione %%% unfold([psic([not_holdsat(F,T)|Body],Head)|PSICS]):- !, append_naf(Head, holds_at(F, T), ExtHead), append(ExtHead,[[test_holds_at(F, T)]],NewHead), %end modified part psic([[],[],[],[],[],[],[],Body],NewHead), unfold(PSICS). append_naf([],Goal,[]). append_naf([Conjunct|MoreConjuncts], Goal, [[naf(Goal)|Conjunct]|MoreExtConjuncts]):- append_naf(MoreConjuncts, Goal, MoreExtConjuncts). unfold([PSIC|MorePSICS]):- PSIC=psic([BodyAtom|_],_), predicate_property(BodyAtom, dynamic), !, get_candidate_clauses(BodyAtom,Clauses), check_forall(Clauses), get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS), append(UnfoldedPSICS,MorePSICS,NewPSICS), unfold(NewPSICS). unfold([PSIC|MorePSICS]):- PSIC=psic([BodyAtom|_],_), is_sicstus_predicate(BodyAtom),!, findall(clause(BodyAtom,[]),BodyAtom,Clauses), get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS), append(UnfoldedPSICS,MorePSICS,NewPSICS), unfold(NewPSICS). % totally unknown predicate: undefined, not built-in. unfold([PSIC|MorePSICS]):- PSIC=psic([BodyAtom|_],_), \+predicate_property(BodyAtom, _),!,unfold(MorePSICS). % MarcoG: The current atom in the PSIC is not a % defined predicate, nor a built-in. It must have come % out from unfolding, and must be an H, or an abducible. % Let us just re-state the IC, so it will be re-parsed % and quantified by impose_ics. Hope the quantification % is correct (to do: check if the quantification is correct) unfold([psic(_,_)|_]):- writeln('An error occured while applying unfolding transition.'), writeln('Please communicate this error to SCIFF developers as soon as possible!'), writeln('Many Thanks!'), fail. unfold_nonrecursive([],[]):- !. % The PSIC could not have any fact matching it % ie., the PSIC can be removed. We represent this fact with the emptylist % it is used by the recursive call (get_unfolded_nonrecursive can return % the emptylist) unfold_nonrecursive(psic(Body,Head),UnfoldedPSIC):- select(Atom,Body,BodyRest), predicate_property(Atom,dynamic), is_unquantified(Atom), % This way, I am ure it is not invoked by unfolding %copy_term(Atom,Atom1), does not strip constraints functor(Atom,F,Arity), functor(Atom1,F,Arity), %this strips constraints, in case the IC was called not in the beginning, e.g., by unfold. findall((Atom1,BodyClause),clause(Atom1,BodyClause),Clauses), nonrecursive(Clauses),!, get_unfolded_nonrecursive(Atom,BodyRest,Head,Clauses,[UnfoldedPSIC1]), unfold_nonrecursive(UnfoldedPSIC1,UnfoldedPSIC). unfold_nonrecursive(X,X). % Currently unfolds eagerly only predicates consisting of exactly one fact. nonrecursive([(_,true)]). get_unfolded_nonrecursive(Atom,BodyRest,Head,[(Atom1,_BodyClause)],[UnfoldedPSIC1]):- (Atom = Atom1 -> UnfoldedPSIC1 = psic(BodyRest,Head) ; UnfoldedPSIC1 = [] % The atom in the body of PSIC does not unify with % the only fact defining it -> the PSIC is removed ). % We assume that all predicates imported from some module are built-in is_sicstus_predicate(Pred) :- predicate_property(Pred,Prop), % Added also interpreted and compiled, so we can invoke predicates defined in % SCIFF itself memberchk(Prop,[built_in,imported_from(_),interpreted,compiled]). %is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =, memberchk, last_state]). %is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =, memberchk]). % End modification % ORIGINAL VERSION: /* unfold([PSIC|MorePSICS]):- PSIC=psic([BodyAtom|_],_), get_candidate_clauses(BodyAtom,Clauses), write('Unfolding: BodyAtom:'), nl, write(BodyAtom), nl, write('Unfolding: Clauses:'), nl, write(Clauses), nl, check_forall(Clauses), get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS), append(UnfoldedPSICS,MorePSICS,NewPSICS), unfold(NewPSICS). */ % End original version % End Modification %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% invert_constraint(st(reif_unify(X,Y,B))):- !, Bneg in 0..1, Bneg #= 1-B, reif_unify(X,Y,Bneg). invert_constraint(reif_unify(X,Y,B)):- !, Bneg in 0..1, Bneg #= 1-B, reif_unify(X,Y,Bneg). invert_constraint(Constraint):- (Constraint = st(Restriction) -> once(opposite(Restriction,Opp)), st(Opp) ; once(opposite(Constraint,Opp)), call(Opp) ). check_forall(Term):- term_variables(Term,Variables), quantify_unquantified(Variables,forall). quantify_unquantified([],_). quantify_unquantified([Var|MoreVars],Quant):- get_quant(Var,_), !, quantify_unquantified(MoreVars,Quant). quantify_unquantified([Var|MoreVars],Quant):- set_quant(Var,Quant), quantify_unquantified(MoreVars,Quant). get_unfolded_psics([],_,[]). get_unfolded_psics([clause(CHead,CBody)|MoreClauses], PSIC, UnfoldedPSICS):- (MoreClauses = [] -> PSIC=psic([Atom1|MoreAtoms1],Head1) ; ccopy(PSIC,psic([Atom1|MoreAtoms1],Head1)) % MG 16 feb 2008: % Mi sembra che la ccopy sia necessaria solo se % ci sono altre clausole ), (is_term_quantified(Atom1,forall) -> (Atom1=CHead -> append(CBody,MoreAtoms1,NewAtoms), UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS] ; UnfoldedPSICS=MoreUnfoldedPSICS ) ; reif_unify(CHead,Atom1,B), (B==1 -> append(CBody,MoreAtoms1,NewAtoms), UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS] ; B==0 -> UnfoldedPSICS=MoreUnfoldedPSICS ; ( (B=1, append(CBody,MoreAtoms1,NewAtoms), UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS]) ; (B=0, UnfoldedPSICS=MoreUnfoldedPSICS) )) ), get_unfolded_psics(MoreClauses,PSIC,MoreUnfoldedPSICS). get_candidate_clauses(Atom,Clauses):- functor(Atom,F,N), findall(clause(Head,Body), ( functor(Head,F,N), clause(Head,Body1), fn_ok(Atom,Head), (Body1=true-> Body=[]; commas_to_list(Body1,Body)) ), Clauses). impose_head1(Head):- quantify_unquantified(Head), term_variables(Head,Variables), flag_variables(Variables), (Head=[Disj]-> impose_head_disjunct(Disj) ; Head=[] -> fail ; nondeterministic(impose_head(Head))). quantify_unquantified(Head):- ics_scan_head(Head,[],HV1), adjust_variable_list(HV1,HV), % No more repeated variables now (eliminated when SICS were loaded) quantify_unquantified_variables(HV). quantify_unquantified_variables([]). quantify_unquantified_variables([variable(Variable,_)|MoreVariables]):- get_quant(Variable,_), !, quantify_unquantified_variables(MoreVariables). quantify_unquantified_variables([Variable|MoreVariables]):- decide_variable_quantification(Variable,Quantification), attach_variable_quantification(Variable,Quantification), quantify_unquantified_variables(MoreVariables). %impose_head([]):- fail. impose_head([H|_]):- impose_head_disjunct(H). impose_head([_|T]):- impose_head(T). impose_head_disjunct([]). impose_head_disjunct([clp_constraint(C)|Tail]):- !, st(C), impose_head_disjunct(Tail). impose_head_disjunct([Head|Tail]):- %Head=..[Functor|Arguments], %length(Arguments,NofArgs), %functor(Head,Functor,NofArgs), isabducible(Head), !, abduce(Head), impose_head_disjunct(Tail). impose_head_disjunct([Head|Tail]):- call(Head), impose_head_disjunct(Tail). % duplicated both with 2 and 3 arguments, because they might occur in both ways isabducible(h(_,_)). isabducible(h(_,_,_)). isabducible(e(_,_,_)). isabducible(e(_,_)). isabducible(en(_,_,_)). isabducible(en(_,_)). isabducible(note(_,_)). isabducible(noten(_,_)). isabducible(abd(_,_,_)). isabducible(abd(_,_)). is_SCIFF_RESERVED(noth(_,_)) :- !. is_SCIFF_RESERVED(noth(_,_,_)) :- !. is_SCIFF_RESERVED(X) :- isabducible(X). violation @ h(F,HEvent,HTime), pending(en(F,EEvent,ETime)) # _pending ==> fn_ok(HEvent,EEvent) | %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), MA QUESTA CCOPY E` NECESSARIA? case_analysis_violation(F,HEvent,HTime,EEvent,ETime,_pending). /* Old version case_analysis_violation(HEvent,HTime,EEvent,ETime, EEvent1,ETime1,_pending):- reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),1), remove_constraint(_pending), viol(en(EEvent,ETime)). case_analysis_violation(HEvent,HTime,_,_,EEvent1,ETime1,_):- reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0). */ % New version, more efficient case_analysis_violation(F,HEvent,HTime,EEvent1,ETime1,_):- get_option(violation_causes_failure, OptFail), (OptFail = yes -> reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0) ; reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),B), ( B=0 ; B=1, %remove_constraint(_pending), viol(en(F,EEvent1,ETime1)) ) ). load_ics:- findall(ic(Head,Body), ics(Head,Body), ICSs), call_list(ICSs). history:- history_is_empty(yes), !. history:- findall(h(Event,Body), hap(Event,Body), History), set_term_quantification(History, existsf), call_list(History). call_list([]). call_list([IC|MoreICs]):- call(IC), call_list(MoreICs). /* Abduction */ abduce(Abducible):- term_variables(Abducible,Variables), flag_variables(Variables), call(Abducible). flag_variables([]). flag_variables([Var|MoreVars]):- get_quant(Var,Q), ((Q=forallf ; Q=existsf) -> true ; flag_quant(Q,NewQ), set_quant(Var,NewQ) ), flag_variables(MoreVars). flag_quant(exists,existsf). flag_quant(forall,forallf). /* old version, less efficient flag_variables([]). flag_variables([Var|MoreVars]):- get_quant(Var,existsf), !, flag_variables(MoreVars). flag_variables([Var|MoreVars]):- get_quant(Var,forallf), !, flag_variables(MoreVars). flag_variables([Var|MoreVars]):- get_quant(Var,exists), !, quant(Var,existsf), flag_variables(MoreVars). flag_variables([Var|MoreVars]):- get_quant(Var,forall), quant(Var,forallf), flag_variables(MoreVars). */ %MarcoG 9 may 2005 % The 1st clause used to be: %check_unification(T1,T2,B,_,_):- % ccopy(p(T1,T2),p(U1,U2)), % reif_unify(U1,U2,B), % reif_unify(T1,T2,B),!. % but in this case % ?- existsf(U1), U1 #< P, e(un(a),U1), forallf(X), forallf(U2), st(U2,U2#0), en(un(X),U2). % results in X=a!! % I only unify the copies. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Modified by Federico, 30-10-2006 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Old version: /* check_unification(T1,T2,B,_,_):- ccopy(p(T1,T2),p(U1,U2)), reif_unify(U1,U2,B),!. check_unification(T1,T2,_,S1,S2):- T1=..[_|A1], T2=..[_|A2], R1=..[S1|A1], R2=..[S2|A2], inconsistent(R1,R2), ( current_predicate(printConstraints/0) -> printConstraints ; true ), fail. */ % New Version: % DANGER!!! This predicate is defined also in sciff_java_gui.pl % PLEASE DO NOT MODIFY IT UNLESS YOU REALLY KNOW WHAT ARE YOU DOING! % KEEP COHERENT THE TWO VERSIONS OF THIS PREDICATE !!! :- chr_constraint inconsistent/2. check_unification(T1,T2,B,e,note):- !, reif_unify(T1,T2,B). check_unification(T1,T2,B,e,en):- !, ccopy(T2,U2), reif_unify(T1,U2,B). check_unification(T1,T2,B,_,_):- ccopy(p(T1,T2),p(U1,U2)), reif_unify(U1,U2,B). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% not_consistency_e @ e(_,EEvent,ETime), note(NotEEvent,NotETime) ==> check_unification(p(EEvent,ETime),p(NotEEvent,NotETime),0,e,note). not_consistency_en @ en(_,EnEvent,EnTime), noten(NotEnEvent,NotEnTime) ==> check_unification(p(EnEvent,EnTime),p(NotEnEvent,NotEnTime),0,en,noten). :- chr_constraint close_history/0. /* version SICStus 3.9 propagation_noth @ close_history, psic([[],[NotH|MoreNotH],[],[],[],[],[],A],Head) # _psic ==> true & Body=[[],[NotH|MoreNotH],[],[],[],[],[],A], ccopy(p(Body,Head),p(Body1,Head1)), propagate_noth(Body1,Body2) | psic(Body2,Head1). % pragma % passive(_psic). */ % Version for SICStus 4. No more tell guards: Check if it is correct!!! propagation_noth @ close_history, psic([[],[NotH|MoreNotH],[],[],[],[],[],A],Head) ==> Body=[[],[NotH|MoreNotH],[],[],[],[],[],A], ccopy(p(Body,Head),p(Body1,Head1)), propagate_noth(Body1,Body2) | psic(Body2,Head1). propagate_noth([H,NotH,E,NotE,EN,NotEN,Abd,A], [H,NewNotH,E,NotE,EN,NotEN,Abd,A]):- noth_propagation(NotH,NewNotH). noth_propagation([NotH|MoreNotHs],NewNotH):- noth_success(NotH), !, noth_propagation1(MoreNotHs,NewNotH). noth_propagation([NotH|MoreNotHs],[NotH|MoreNewNotHs]):- noth_propagation(MoreNotHs,MoreNewNotHs). noth_propagation1([],[]). noth_propagation1([NotH|MoreNotHs],NewNotH):- noth_success(NotH), !, noth_propagation1(MoreNotHs,NewNotH). noth_propagation1([NotH|MoreNotHs],[NotH|MoreNewNotHs]):- noth_propagation1(MoreNotHs,MoreNewNotHs). noth_success(noth(Event,Time)):- universal_variables_in_term(noth(Event,Time),UnivVariables), (UnivVariables=[] -> \+(has_happened(Event,Time)); universal_variables_happened(Event,Time,TermList), % In realta` il D8 dice che % dovrei rendere universali tutte le variabili, escluse le esistenziali non flagged. PUniv=..[p|UnivVariables], % Qui devo rendere flagged tutte le variabili che sono universali (in teoria tutte escluse le exist non flagged) flag_variables(UnivVariables), impose_noth_not_unif(TermList,PUniv)). impose_noth_not_unif([],_). impose_noth_not_unif([Term|MoreTerms],PUniv):- set_restriction(reified_unif:reif_unify(Term,PUniv,0)), %reif_unify(Term,PUniv,0), impose_noth_not_unif(MoreTerms,PUniv). universal_variables_in_term(Term,UnivVariables):- term_variables(Term,Vars), keep_universals(Vars,UnivVariables). keep_universals([],[]). keep_universals([Var|MoreVars],[Var|MoreUnivVars]):- is_universal(Var), !, keep_universals(MoreVars,MoreUnivVars). keep_universals([_|MoreVars],UnivVars):- keep_universals(MoreVars,UnivVars). universal_variables_happened(Event,Time,TermList):- findall(Term, ( ccopy(p(Event,Time),p(Event1,Time1)), universal_variables_in_term(p(Event1,Time1),UnivVars), has_happened(Event1,Time1), Term=..[p|UnivVars] ), TermList). has_happened(Event,Time):- find_constraint(h(_,Event,Time),_). %% COMPLIANT HISTORY GENERATION: 20 JUL 04 /* versione MarcoA fulfiller1 @ close_history, pending(e(Event,Time)) ==> % write('Inserted '),write(h(Event,Time)),nl, % write_history, h(Event,Time). */ pending_e @ e(F,Event,Time) ==> pending(e(F,Event,Time)). %---------------------------------------------------------- % FULFILLMENT RULES %---------------------------------------------------------- %new fdet version fulfillment @ h(F,HEvent,HTime), pending(e(F,EEvent,ETime)) # _pending ==> fn_ok(HEvent,EEvent) | %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant. case_analysis_fulfillment(F,HEvent,HTime,EEvent,ETime,_pending). case_analysis_fulfillment(F,HEvent,HTime,EEvent,ETime,_):- % HEvent=EEvent, HTime=ETime, % If we use unification, it triggers all the CHR constraints involving the variables % before terminating the execution. With g-SCIFF, it will trigger fulfiller before % removing the pending expectation. Better use reif_unify. % 4 Aug 07: Actually even with reif_unify fulfiller is triggered too early. % Let us anticipate remove_constraint %remove_constraint(_pending), %term_unify(HEvent,EEvent), %eq(HTime,ETime), reif_unify(p(HEvent,HTime),p(EEvent,ETime),1), ( fdet(e(Term,Time)), subsumeschk(e(Term,Time),e(EEvent,ETime)) -> ! ; true ), fulf(e(F,EEvent,ETime)). case_analysis_fulfillment(_,HEvent,HTime,EEvent1,ETime1,_):- reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0). fulfillment_allows @ h(F,do(HX,HRec,HAction,HD),HT), pending(e(F,do(Expecter,EX,ERec,EAction,ED),ET)) # _pending ==> fn_ok(p(do(HX,HRec,HAction,HD),HT),p(do(EX,ERec,EAction,ED),ET)) | %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant. case_analysis_fulfillment(F,do(Expecter,HX,HRec,HAction,HD),HT,do(Expecter,EX,ERec,EAction,ED),ET,_pending). /* fulfillment @ h(HEvent,HTime), pending(e(EEvent,ETime)) # _pending ==> fn_ok(HEvent,EEvent) | %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant. case_analysis_fulfillment(HEvent,HTime,EEvent,ETime,_pending). case_analysis_fulfillment(HEvent,HTime,HEvent,HTime,_pending):- remove_constraint(_pending), %reif_unify(p(HEvent,HTime),p(EEvent,ETime),1), (sciff_option(fdet,on)->!;true), fulf(e(EEvent,ETime)). case_analysis_fulfillment(HEvent,HTime,EEvent1,ETime1,_):- reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0). */ /* versione MarcoG */ fulfiller1 @ (close_history) \ (pending(e(F,Event,Time))) <=> % write('Inserted '),write(h(Event,Time)), sciff_option(fulfiller,on) %findall_constraints(nondeterministic(_),[]) bug fix: fulfilment does not use nondeterinistic | fulf(e(F,Event,Time)), h(F,Event,Time), %%%MARCOM writeln(h(Event,Time)). %Constraints used by AlLoWS :- chr_constraint gen_phase/0, end_gen_phase/0, remove_exp/0. fulfiller_rationality @ (gen_phase) \ pending(e(F,do(X,X,Rec,Action,D),T)) <=> %sciff_option(fulfiller_rationality,on) | fulf(e(F,do(X,X,Rec,Action,D),T)), h(F,do(X,Rec,Action,D),T). fulfiller_chor @ (gen_phase), pending(e(F,do(chor,X,Rec,Action,D),T)) % # _pending ==> %sciff_option(fulfiller_rationality,on) | testing(WS), set_term_quantification(WS,existsf), reif_unify(WS,X,Bool), (Bool=0;Bool=1), (Bool=0 -> %remove_constraint(_pending), fulf(e(F,do(chor,X,Rec,Action,D),T)), h(F,do(X,Rec,Action,D),T) ; true). end_gen_phase @ end_gen_phase \ gen_phase <=> true. write_history:- %findall_constraints(h(send(_,_,_,_),_),L), MarcoG: why only send? findall_constraints(h(_,_,_),L), print_chr_list(L,'\n'). write_normal_abducibles:- findall_constraints(abd(_,_,_),L), print_chr_list(L,'\n'). write_positive_expectations:- findall_constraints(e(_,_,_),L), print_chr_list(L,'\n'). write_violations:- findall_constraints(viol(_,_,_),L), print_chr_list(L,'\n'). write_events_not_expected:- findall_constraints(not_expected(_,_,_),L), print_chr_list(L,'\n'). /* closure_e @ (close_history) \ (pending(e(Event,Time)) # _pending) <=> viol(e(Event,Time)) pragma passive(_pending). */ closure_e @ (close_history), (pending(e(F,Event,Time)) ) %# _pending) ==> true | % this guard has been added to avoid a mis-interpretation of the chr compiler (get_option(violation_causes_failure, yes) -> fail ; (%remove_constraint(_pending), viol(e(F,Event,Time)) ) ). %pragma passive(_pending). Does not work with violation_causes_failure -> no /* closure_e @ (close_history) \ (pending(e(Event,Time)) # _pending) <=> get_option(violation_causes_failure, no) | viol(e(Event,Time)) pragma passive(_pending). */ :- chr_constraint not_expected/1. not_expected_gen @ (h(F,HEvent,HTime)) ==> sciff_option(allow_events_not_expected, no) | not_expected(h(F,HEvent,HTime)). not_expected_remove @ fulf(e(F,Event, Time)) \ not_expected(h(F,Event, Time)) <=> true. % If an event is expected both by the WS and the Chor, % then it is no longer not_expected not_expected_remove_allows1 @ (fulf(e(F,do(chor,EX,ERec,EAction,ED),ET)), fulf(e(F,do(WS,EX,ERec,EAction,ED),ET))) \ not_expected(h(F,do(EX,ERec,EAction,ED),ET)) <=> testing(WS) | true. % If an event is expected only by the choreography, % and it does not involve the WS under test, then % the event is expected not_expected_remove_allows2 @ fulf(e(F,do(chor,EX,ERec,EAction,ED),ET)) \ not_expected(h(F,do(EX,ERec,EAction,ED),ET)) <=> %write('******** TRYING ***************'), testing(WS), nonvar(EX), EX \= WS, nonvar(ERec), ERec \= WS | true. % violation is imposed only if the corresponding flag is set to true protocol_e @ (close_history) \ (not_expected(h(F,Event,Time)) # _not_expected) <=> true %added to avoid a possible chr bug | ( get_option(violation_causes_failure, yes) -> fail ; %remove_constraint(_not_expected), viol(not_expected(h(F,Event,Time))) ) pragma passive(_not_expected). % End Modification %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% closure_en @ (close_history) \ (pending(en(F,Event,Time)) # _pending) <=> fulf(en(F,Event,Time)) pragma passive(_pending). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % MODIFIED BY FEDERICO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Removed because of an optimization introduced by MarcoG % If violation causes failure then failure is imposed immediately % without adding the chr_constraint viol(_). % Otherwise the chr_constraint viol(_) is imposed, and no failment is imposed. % % Violations are generated by the following chr_rules: % - case_analysis_violation (EN with a corresponding H) % - closure_e (close_history, and E without H) % - ct_time_constraint (E and due to the current_time, no H is possible anymore) % - protocol_e (H without E) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* failure_for_violation @ viol(_) ==> ( current_predicate(printConstraints/0) -> printConstraints ; true ), get_option(violation_causes_failure, no). */ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % CURRENT TIME MANAGEMENT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- chr_constraint current_time/1. current_time_update @ (h(_,current_time,CT)) \ (current_time(_OldCT) # _current_time) <=> current_time(CT) pragma passive(_current_time). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Modified by Federico, 20061102 % % Original version: /* ct_time_constraint @ current_time(CT), pending(e(Event,Time)) # _pending ==> impose_time_constraint(Time,CT) pragma passive(_pending). constraints gt_current_time/2. impose_time_constraint(Time,CT):- Time #>= CT, !. impose_time_constraint(Time,CT):- gt_current_time(Time,CT), ( current_predicate(printConstraints/0) -> printConstraints ; true ), fail. */ ct_time_constraint @ current_time(CT), pending(e(F,Event,Time)) # _pending ==> impose_time_constraint(Time,CT, e(F,Event,Time), _pending) pragma passive(_pending). impose_time_constraint(Time,CT, e(F,Event,Time), _):- ( geq(Time,CT) -> true ; ( get_option(violation_causes_failure, yes) -> fail ; %remove_constraint(_pending), viol(gt_current_time(e(F,Event,Time), failed_to_impose_greater_than(Time, CT))) ) ). %end @ phase(deterministic) <=> findall_constraints(nondeterministic(_),[]) | true. switch2nondet @ phase(deterministic) <=> phase(nondeterministic). /*switch2det @ phase(nondeterministic) \ nondeterministic(G) <=> call(G). %phase(deterministic).*/ switch2det @ phase(nondeterministic) , nondeterministic(G) <=> call(G), phase(deterministic). remove_phase \ phase(_) <=> true. remove_phase <=> true. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% build(SOKB,ICS,History):- translate_sokb(SOKB,'./sokb.pl'), translate_ics(ICS,'./ics.pl'), translate_history(History,'./history.pl'). build(ExampleName):- atom_concat(ExampleName,'/',A1), atom_concat(A1,ExampleName,A2), atom_concat(A2,'_sokb.pl',SOKB), atom_concat(A2,'_ics.txt',ICS), atom_concat(A2,'_history.txt',History), build(SOKB,ICS,History). build(ExampleName,SubExample):- atom_concat(ExampleName,'/',A1), atom_concat(A1,ExampleName,A2), atom_concat(A2,'_sokb.pl',SOKB), atom_concat(A2,'_ics.txt',ICS), atom_concat(A2,'_history_',A3), atom_concat(A3,SubExample,A4), atom_concat(A4,'.txt',History), build(SOKB,ICS,History). build1(ExampleName):- atom_concat('../examples/',ExampleName,A0), atom_concat(A0,'/',A1), atom_concat('../protocols/',ExampleName,B0), atom_concat(B0,'/',B1), atom_concat(A1,ExampleName,A2), atom_concat(B1,ExampleName,B2), atom_concat(B2,'_sokb.pl',SOKB), atom_concat(B2,'_ics.txt',ICS), atom_concat(A2,'_history.txt',History), build(SOKB,ICS,History). build1(ExampleName,SubExample):- atom_concat('../examples/',ExampleName,A0), atom_concat(A0,'/',A1), atom_concat('../protocols/',ExampleName,B0), atom_concat(B0,'/',B1), atom_concat(B1,ExampleName,B2), atom_concat(A1,ExampleName,A2), atom_concat(B2,'_sokb.pl',SOKB), atom_concat(B2,'_ics.txt',ICS), atom_concat(A2,'_history_',A3), atom_concat(A3,SubExample,A4), atom_concat(A4,'.txt',History), build(SOKB,ICS,History). build2(ExampleName):- atom_concat('../examples/',ExampleName,A0), atom_concat(A0,'/',A1), atom_concat('../protocols/',ExampleName,B0), atom_concat(B0,'/',B1), atom_concat(A1,ExampleName,_A2), atom_concat(B1,ExampleName,B2), atom_concat(B2,'_sokb.pl',SOKB), atom_concat(B2,'_ics.txt',ICS), build3(SOKB,ICS). build3(SOKB,ICS):- translate_sokb(SOKB,'./sokb.pl'), translate_ics(ICS,'./ics.pl'). /* :- dynamic(numero_soluzioni/1). conta_soluzioni :- retractall(numero_soluzioni(X)), assert(numero_soluzioni(0)), run, numero_soluzioni(N), N1 is N + 1, write('trovata una soluzione ('),write(N1),write(')'),nl, retract(numero_soluzioni(N)), assert(numero_soluzioni(N1)), fail. */ run:- load_ics, current_time(0), society_goal, history, phase(deterministic), close_history. run_no_close:- load_ics, current_time(0), society_goal, history, phase(deterministic). try_number(0). try_number(X):- try_number(Y), X is Y+1, max_bound(B), X < B. iterative_deepening(Goal):- try_number(Depth), write('***************'), writeln(depth(Depth)), max_depth(Depth), call(Goal). iter:- init_graph('proof.dot',_Stream), statistics(runtime,_), load_ics, iterative_deepening( (society_goal, history, phase(deterministic), once(( write('grounding time\n'), ground_time, write('grounding 1\n'), make_choice )) )), statistics(runtime,[_,Time]), writeln(runtime(Time)). iter_gsciff:- init_graph('proof.dot',_Stream), statistics(runtime,_), load_ics, society_goal, N in 0..1000, indomain(N), write('************************* new happen ******************************'), writeln(N), add_history_el(N), phase(deterministic), close_history, write('grounding\n'), make_choice, statistics(runtime,[_,Time]), writeln(runtime(Time)). iter_gsciff_hist:- init_graph('proof.dot',_Stream), statistics(runtime,_), load_ics, society_goal, history, phase(deterministic), N in 0..1000, indomain(N), write('************************* new happen ******************************'), writeln(N), add_history_el_sym(N,_), close_history, statistics(runtime,[_,Time]), writeln(runtime(Time)). % Questo predicato e` per verificare la proprieta` delle aste combinatorie: % "Esiste un insieme di bid t.c. io ottengo uno solo fra i due elementi 1 e 2?" % E` da raffinare, questo e` solo uno sketch di come si potrebbe fare. iter_gsciff_auction:- statistics(runtime,_), load_ics, society_goal, N in 0..1000, indomain(N), write('************************* new happen ******************************'), writeln(N), add_history_el(N), \+(( e(deliver(_Item1)), e(deliver(_Item2)) )), close_history, statistics(runtime,[_,Time]), writeln(runtime(Time)). % Qual e` la bid che devo fare per vincere, sapendo che % 1. voglio minimizzare la cifra che pago % 2. ipotizzo che l'altro faccia una bid di 5 % 3. io voglio pagare al massimo 10 best_bid(Bid):- statistics(runtime,_), load_ics, history, Price in 0..10, existsf(Bid), existsf(Tbid), e(tell(i,auc,bid(i1,Bid),auction1),Tbid), existsf(Price), existsf(Tpay), e(tell(i,auc,pay(Price),auction1),Tpay), add_history_el(2), make_choice, minimize( ( % Metto esplicitamente il society goal, perche' altrimenti % non posso accedere alle variabili indomain(Price), close_history, write(Price), nl ) ,Price), statistics(runtime,[_,Time]), writeln(runtime(Time)). % Explanation in help.pl min_viol_closed(Num,OutList):- max_viol(Num), minimize( ( load_ics, society_goal, history, close_history, indomain(Num), findall_constraints(_,OutList) ),Num). % Explanation in help.pl min_viol_open(Num,OutList):- max_viol(Num), minimize( ( load_ics, society_goal, history, indomain(Num), findall_constraints(_,OutList) ),Num). get_ics_quantified(PSICs):- findall(ic(Head,Body), ics(Head,Body), ICSs), convert_to_psic_list(ICSs,PSICs). convert_to_psic_list([],[]). convert_to_psic_list([IC|ICs],[PSIC|PSICs]):- convert_to_psic(IC,PSIC), convert_to_psic_list(ICs,PSICs). allows(Param):- (var(Param) -> Param = false ; true), % Default behaviour: fail if not conformant % load_ics, I re-write the impose_ics because I don't want to redo it for % each possible history (since it is expensive), so I redo only % the necessary parts get_ics_quantified(PSICs), call_list(PSICs), %current_time(0), gen_phase, % activates rationality history, society_goal, phase(deterministic), end_gen_phase, % deactivates rationality, backtrackable (Param = verbose -> nl, writeln_debug('Trying history'), write_history, write_normal_abducibles, write_positive_expectations, write_violations, write_events_not_expected ; true), (remove_exp, society_goal, % reactivate ics, doing a SCIFF (no g-SCIFF) computation %load_ics, %phase(deterministic), MG: Adding this (together with remove_phase) performs % stronger reasoning. However, in some instances % it can slow down very much the computation. % Better perform stronger reasoning in the early stages (generate) % and faster in other stages. Remember that in the first stages % we look for all solutions (where deterministic checking is % useful), while in the second we look for one solution call_list(PSICs), close_history -> fail % causes backtracking ; writeln_debug('AlLoWS failed: no fulfilment for possible history'),nl, (get_option(sciff_debug, on) -> write_history,write_normal_abducibles ; true), !, Param=true % deep failure ). allows(_):- writeln_debug('AlLoWS succeded: all possible histories compliant'), (get_option(allow_events_not_expected, yes) -> writeln_debug('Feeble conformance proven') ; writeln_debug('Strong conformance proven') ). remove_exp_pending @ remove_exp \ pending(_) <=> true. remove_exp_e @ remove_exp \ e(_,_,_) <=> true. remove_exp_en @ remove_exp \ en(_,_,_) <=> true. remove_exp_fulf @ remove_exp \ fulf(_) <=> true. remove_exp_ic @ remove_exp \ ic(_,_) <=> true. remove_exp_psic @ remove_exp \ psic(_,_) <=> true. %remove_exp_en @ remove_exp \ not_expected(_) <=> true. end_remove_exp @ remove_exp <=> true. %iter_gsciff_vickrey:- % statistics(runtime,_), % load_ics, % society_goal, % N in 0..1000, % indomain(N), write('************************* new happen ******************************'), % writeln(N), % add_history_el(N), % close_history, % statistics(runtime,[_,Time]), % writeln(runtime(Time)). add_history_el:- existsf(X), existsf(T), h(X,T). add_history_el:- existsf(X), existsf(T), h(X,T), writeln('************************* new happen ******************************'), add_history_el. add_history_el(0):- !. add_history_el(N):- existsf(X), existsf(T), h(X,T), N1 is N-1, add_history_el(N1). % generates N happened events ordered in time add_history_el_sym(0,_):- !. add_history_el_sym(N,T1):- existsf(X), existsf(T), h(X,T), T in 0..1000, T #=< T1, N1 is N-1, add_history_el_sym(N1,T). proof:- init_graph('proof.dot',_Stream), statistics(runtime,_), load_ics, society_goal, history, once(( write('grounding time\n'), ground_time, write('grounding 1\n'), make_choice, true )), statistics(runtime,[_,Time]), writeln(runtime(Time)). test(Pred,Mem,Time):- statistics(walltime,[T1,_]), call_always_success(Pred), statistics(walltime,[T2,_]), Time is T2 - T1, statistics(memory,[Mem,_]). call_always_success(Pred):- call(Pred), !. call_always_success(_). clp_constraint(A):- call(A). :- chr_constraint cug/1. cug(X) <=> ground(X)|call(X). /* constraints novis/0. firstfail @ e(X1,T1), e(X2,T2), ground_time ==> fd_var(T1), fd_var(T2), fd_size(T1,S1), fd_size(T2,S2), S1 fd_var(T) | T in -1000..1000, indomain(T). visual @ e(X,T), ground_time ==> fd_var(T) | T in -1000..1000, fd_min(T,Min),fd_max(T,Max), write(T in Min..Max), indomain(T), nl, write(T), novis. */ :- chr_constraint all_e/1, get_list_e/1. e(F,X,T) \ all_e(L) <=> notmember(e(F,X,T),L) | all_e([e(F,X,T)|L]). all_e(L1), get_list_e(L2) <=> L1=L2. findall_e(L):- all_e([]), get_list_e(L), !. notmember(_,[]). notmember(A,[H|_]):- A==H, !, fail. notmember(A,[_|T]):- notmember(A,T). % MG 9 Feb 2008: I don't use the findall_constraints implemented in my_chr_extensions, % because it does not retain the variables (it is due to the implementation of % findall in SICStus) ground_time:- findall_e(L), get_time(L,LT), solver_search(LT). get_time([],[]). get_time([e(_,_,T)|R],[T|RT]):- add_default_domain(T), get_time(R,RT). build_and_run(SOKB, ICS, History, noclose) :- build(SOKB, ICS, History), consult(sokb), use_module(history), use_module(ics), run_no_close. build_and_run(SOKB, ICS, History, close) :- build(SOKB, ICS, History), consult(sokb), use_module(history), use_module(ics), run. project(Project):- default_dir(Dir), atom_concat(Dir,Project,Path), atom_concat(Path,'/',PathSlash), retractall(prjDir(_)), assert(prjDir(PathSlash)), atom_concat(PathSlash,'project.pl',PrjFile), compile(PrjFile), build_prj(PathSlash). append_path(_,[],[]):- !. % If the file is actually a URL, do not change it append_path(Path,[File|Rest],[FullPath|Rest1]):- atom_concat('http://',_,File),!,FullPath=File, append_path(Path,Rest,Rest1). append_path(Path,[File|Rest],[FullPath|Rest1]):- atom_concat(Path,File,FullPath), append_path(Path,Rest,Rest1). convert_sokb([],_). convert_sokb([SOKB|Rest],File):- write_debug('Parsing file '), write_debug(SOKB), translate_sokb(SOKB,File,write), % for the 1st, write, the others are in append writeln_debug(' --> OK'), convert_sokb1(Rest,File). convert_sokb1([],_). convert_sokb1([SOKB|Rest],File):- write_debug('Parsing file '), write_debug(SOKB), translate_sokb(SOKB,File,append), writeln_debug(' --> OK'), convert_sokb1(Rest,File). /* build(SOKB,ICS,History):- translate_sokb(SOKB,'./sokb.pl'), translate_ics(ICS,'./ics.pl'), translate_history(History,'./history.pl'). build(ExampleName):- atom_concat(ExampleName,'/',A1), atom_concat(A1,ExampleName,A2), atom_concat(A2,'_sokb.pl',SOKB), atom_concat(A2,'_ics.txt',ICS), atom_concat(A2,'_history.txt',History), build(SOKB,ICS,History). */