:-dynamic f/3. :-dynamic f/6. :-dynamic app/2. :-dynamic edge/2. :- prolog_flag(redefine_warnings,_,off). :- use_module(library(terms)). :- use_module(library(lists)). :- use_module(library(clpr)). :- use_module(library(ugraphs)). time(Goal,T,M,P,C):- statistics(runtime,[T1,_]), Goal, statistics(runtime,[T2,_]), statistics(memory,[M,_]), statistics(program,[P,_]), statistics(choice,[C,_]), T is ((T2-T1)//100)/10. % T is T2-T1. % printtime(G) G is a goal % ptime(G):- time(G,T,_,_,_), nl, write('Execution time '), write(T). notallowed(M,C,Invariants):- member(inv(NM,NC),Invariants), msubsumes(M,C,NM,NC). allowedN(M,C,Invariants):- \+(notallowed(M,C,Invariants)). get_constraints([],{}):-!. get_constraints([[_]-{C}],{C}):-!. get_constraints([[_]-{C}|R],{C,N}):- get_constraints(R,{N}),!. % entails(C,D): C entails D % - C,D are constraints of the form {c1,...,cn} % entails(C,D):- C,entailed(D). % subsumed({},{}). subsumed({C},{D}):- call_residue(entails({C},(D)),_). subsumed({C},{}):- call_residue({C},_). % % factsubsumed(H,D,H1,D1): (H1,D1) subsumes (H,D) % - H,H1 are atoms % - D,D1 are constraints factsubsumed_with_copy(Atom,Cnst,Atom1,Cnst1):- copy_term((Atom,Cnst),(H,D)), copy_term((Atom1,Cnst1),(H1,D1)), subsumes_chk(H1,H), unify_with_occurs_check(H,H1), simplify(D,DS), simplify(D1,DS1), subsumed(DS,DS1). factsubsumed(H,D,H1,C):- subsumes_chk(H1,H), unify_with_occurs_check(H,H1), simplify(D,D1), simplify(C,C1), subsumed(D1,C1). % unify(C,D,R): R is equivalent to (C and D) % unify({},{},{}):-!. unify({},C,R):- % pay attention call_residue({},L) fails call_residue(C,S), get_constraints(S,R),!. unify({D},{},R):- call_residue({D},S), get_constraints(S,R),!. unify({D},{C},R):- call_residue({C,D},S), get_constraints(S,R),!. % % project(C,T,PC): PC is the projection of C over the variables of T % project({}, _, {}) :- !. project(Cons, Term, PCons) :- !, retractall(projection_temporary(_)), assert((projection_temporary(Term) :- Cons)), call_residue(projection_temporary(Term), TmpPCons), get_constraints(TmpPCons, PCons). % atom_cons_unify(H,B,B1,C,C1,D2) % atom_cons_unify(H,B,B1,C,C1,D2):- unify_with_occurs_check(B1,B), unify(C,C1,D), project(D,H,D1), simplify(D1,D2). % satisfiable(C,D): C and D is satisfiable % satisfiable({},{}). satisfiable({},{D}):- call_residue({D},_). satisfiable({D},{}):- call_residue({D},_). satisfiable({D},{C}):- call_residue({D},_), call_residue({C},_). % simplify(C,D). % simplify({},{}):-!. simplify(C,D):- call_residue(C,R), get_constraints(R,D). combine({},{},{}). combine({},{C},{C}). combine({C},{},{C}). combine({C},{D},{C,D}). mysublist([],[],[]). mysublist([X|L],[X|M],N):- mysublist(L,M,N). mysublist([X|L],M,[X|N]):- mysublist(L,M,N). munify(M1,C1,M2,C2,D):- unify_with_occurs_check(M1,M2), unify(C1,C2,D). sel(SubM,SupM,SubSupM,Rest):- length(SubM,LSubM), 1 =< LSubM, length(SupM,LSupM), LSubM =< LSupM, sel(SubM,SupM,[],SubSupM,Rest). sel([A|SubM],[B|RestM],SupM,[B|L],R):- functor(A,F,N), functor(B,F,N), append(SupM,RestM,AuxM), sel(SubM,AuxM,[],L,R). sel([A|SubM],[B|RestM],SupM,L,R):- sel([A|SubM],RestM,[B|SupM],L,R). sel([],Rest,_,[],Rest). % % msubsumes(N,C,M,D) = den(N,C) =< den(M,D) % msubsumes(N,C,M,D):- sel(M,N,SN,_), subsumes_chk(M,SN), copy_term((SN,C),(CSN,CC)), copy_term((M, D),(CM, CD)), project(CC,CSN,PCC), unify_with_occurs_check(CSN,CM), simplify(PCC,SPCC), simplify(CD,SCD), subsumed(SPCC,SCD). apply_rule(M,Cm,A,B,Cab,H,Ch):- mysublist(M,SM,RM), sel(SM,B,SB,_), munify(SB,Cab,SM,Cm,Cu), append(A,RM,H), project(Cu,H,Cpu), simplify(Cpu,Ch). addedge(Of,Nf):- edge(Of,Nf),!. addedge(Of,Nf):- assert(edge(Of,Nf)). apply_msubsumes(NM,NC,Nf):- f(_,M,C,Of,_,_), msubsumes(NM,NC,M,C), addedge(Of,Nf), !. check_asserta(f(Step,NM,NC,Nf,Pref,Clause)):- asserta(f(Step,NM,NC,Nf,Pref,Clause)). removeAllF(NM,NC):- setof(_,removeF(NM,NC),_),!. removeAllF(_,_):-!. removeF(NM,NC):- clause(f(S,M,C,Nf,Pref,Clause),true,Ref), msubsumes(M,C,NM,NC), erase(Ref), asserta(delf(S,M,C,Nf,Pref,Clause)). apply_widen(_,NM,NC,NM,NC). % :-widen(NM,NC,WM,WC). selfloop(NM,NC,CM,CCm,Nf):- msubsumes(NM,NC,CM,CCm), addedge(Nf,Nf). select_and_apply(CS,NS):- invariants(Invariants), f(CS,M,Cm,Nf,_,_), copy_term((M,Cm),(CM,CCm)), rule(A,B,Cab,RuleNo), apply_rule(M,Cm,A,B,Cab,NM,NC), allowedN(NM,NC,Invariants), \+(selfloop(NM,NC,CM,CCm,Nf)), \+(apply_msubsumes(NM,NC,Nf)), apply_widen(NS,NM,NC,WM,WC), % removeAllF(WM,WC), retract(countF(CountF)), CountF1 is CountF+1, assert(countF(CountF1)), asserta(f(NS,WM,WC,CountF,Nf,RuleNo)), addedge(CountF,Nf), write('.'), flush_output. loop(N):- N1 is N+1, nl, write('Step'), write(N1), nl, flush_output, setof(_,select_and_apply(N,N1),_), !, loop(N1). loop(_):- nl, write('--------------------------------------------------------'),nl, write('The fixpoint has been reached!'),nl, write('Search for the initial configuration using :-ls.'). go:- unsafe(L), clearF(L), clearApp, loop(0). clearF(L):- retractall(f(_,_,_,_,_,_)), retractall(countF(_)), assert(countF(1)), assertList(L). clearApp:- retractall(app(_,_)), retractall(edge(_,_)). assertList([unsafe(Unsafe,C)|Rest]):- !, retract(countF(CountF)), CountF1 is CountF+1, assert(countF(CountF1)), assert(f(0,Unsafe,C,CountF,0,0)), assertList(Rest). assertList([]). safe:- \+ f(_,[init],_,_,_,_). listF:-listing(f). listR:-listing(rule). listU:-listing(unsafe). attack:- f(Step, [init], _, K, _, _), tracer(Step,K). tracer(Step,K):- Step>0,!, f(Step, State, Cstr, K, Prev, Rule), %; % delf(Step, State, Cstr, K, Prev, Rule) % ), write('Constrained configuration: '), nl, portray_clause((State:Cstr)), nl,nl, rule(H,B,C,Rule), nl, nl, write('Rule: '),write(Rule),nl, portray_clause(rule(H,B,C)), nl, nl, Step1 is Step-1, tracer(Step1,Prev). tracer(0,K):- f(Step, State, Cstr, K, Prev, Rule), write('Unsafe state: '), nl, portray_clause((State:Cstr)), nl, write('****** End of trace *****'), nl. backtrace(Step,K,L):- Step1 is Step+1, f(Step1, State, Cstr, N, K, Rule), %write('Constrained configuration/Step: '), %write(N),write(' '),write(Step), nl, %portray_clause((State:Cstr)), nl,nl, nl, nl, append(L,[s(Step1,N,(State:Cstr))],L1), backtrace(Step1,Prev,L1). backtrace(Step,K,L):- nl,write('Trace'), write(L), fail. ls:-listing(f/6). le:-listing(edge/2). lr:-listing(rule/4). lz:-listing(z/2). lc:-listing(count/1). lf:-listing(info/4). allpaths(I):- buildgraph(G), showpath(I,G). showpath(I,G):- path(I,G,P), write(P),nl, fail. showpath(_,_):-!. selpaths(I,K):- buildgraph(G), showselpath(I,K,G). showselpath(I,K,G):- path(I,G,P), \+(member(K,P)), write(P),nl, fail. showselpath(_,_,_):-!. buildgraph(G):- setof(U-V,(edge(U,V),\+(U==V)),Edges), vertices_edges_to_ugraph([],Edges,G).