:-dynamic f/5.
:-dynamic trule/5.
:-dynamic crule/6.
:-dynamic srule/6.
:-dynamic ccrule/5.
:-dynamic dcule/5.



:- prolog_flag(redefine_warnings,_,off).
:- use_module(library(terms)).
:- use_module(library(lists)).
:- use_module(library(clpr)).
:- use_module(library(charsio)).
:- use_module(library(system)).

ptime(Goal):-time(Goal,T,_,_,_),nl,write('Time: '),write(T).

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.

 
inclusion([],_).

inclusion([A|R],Q):-
 member(A,Q),!,
 inclusion(R,Q).

 
add(Type,S,Q,[S|Q]):-
 \+ member(S,Q),!.
 
add(Type,_,Q,Q).
 
%%% Example

unsafe:-
 f(Step,graph(_,_,[S,C,Ch]),W1,W2,W3),
 init(IS,IC,_),
 mapcheck(S,IS),
 mapcheck(C,IC),
 nl,
 write('Initial state: '),nl,
 write(f(Step,[S,C,Ch],W1,W2,W3)).

state(node(_,St,_),St).
state(node(_,St),St).
state(edge(_,_,_,St),St).

mapcheck([A|L],Q):-
 state(A,S),
 member(S,Q),
 mapcheck(L,Q).
 
mapcheck([],_). 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% GRAPH SUBSUMPTION
% 
%
% G=graph(SN,SC,[SNodes,CNodes,Edges])
% SNodes list of node(Id,State,Padding) 1...SN
% CNodes list of node(Id,State) 1..SC
% Edges  list of edge(Type,SNode,CNode,State)
% 


sinjection([node(N1,S1,Q1)|SNodes1],SNodes2,[h(N1,N2)|SInjection]):-
 select(node(N2,S2,Q2),SNodes2,RestSNodes2),
 inclusion(Q2,Q1),
 subsumes_chk(S1,S2),
 sinjection(SNodes1,RestSNodes2,SInjection).

sinjection([],_,[]).
 
cinjection([node(N1,S1)|CNodes1],CNodes2,[h(N1,N2)|CInjection]):-
 select(node(N2,S2),CNodes2,RestCNodes2),
 subsumes_chk(S1,S2),
 cinjection(CNodes1,RestCNodes2,CInjection).

cinjection([],_,[]).

 
edge_subsumption(SInjection,CInjection,[edge(Type,S1,C1,State)|E1],E2):-
 member(h(S1,S2),SInjection),
 member(h(C1,C2),CInjection),
 select(edge(Type,S2,C2,State),E2,RestE2),
 edge_subsumption(SInjection,CInjection,E1,RestE2).
  
edge_subsumption(_,_,[],_).

graph_subsumption(graph(SV1,CV1,[SN1,CN1,E1]),graph(SV2,CV2,[SN2,CN2,E2])):-
 SV1 =< SV2,
 CV1 =< CV2, 
 sinjection(SN1,SN2,SInjection),
 cinjection(CN1,CN2,CInjection),
 edge_subsumption(SInjection,CInjection,E1,E2).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

edge_invariant(Type,SN,CN,E):-
  \+ member(edge(Type,SN,CN,_),E).

edge_invariant_cnodes(Type,CN,E):-
 \+ member(edge(Type,_,CN,_),E).


old_edge_invariant(Type,SN,CN,E).

old_edge_invariant_cnodes(Type,CN,E).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% SRULE
%    
% srule(S,Ch,S1,Ch1,rule).
% S -- Ch --  |-->  S1 -- Ch1 
%
% node(Id,S1,Q),edge(Type,Id,Id1,Ch1) ==> 
%   node(Id,S1,Q u Ch),edge(Type,Id,Id1,Ch) (Ch1 is in Q by def.)
%
 
apply_srule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,Ch1,graph(SV,CV,[S1,C,E1])):-
 select(node(SN,St1,Q),S,RestS),
 select(edge(Type,SN,CN,Ch1),E,RestE),
 add(Type,Ch,Q,Q1),
 S1=[node(SN,St,Q1)|RestS],
 E1=[edge(Type,SN,CN,Ch)|RestE].

% node(Id,S1,Q),node(Id1,S2) ==> 
%   node(Id,S1,Q u Ch),edge(Type,Id,Id1,Ch),node(Id1,S2)
% Creation of a new edge
 
apply_srule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,Ch1,graph(SV,CV,[S1,C,E1])):-
 select(node(SN,St1,Q),S,RestS),
 member(node(CN,_),C),
 edge_invariant_cnodes(Type,CN,E),
 edge_invariant(Type,SN,CN,E),
 member(Ch1,Q),
 add(Type,Ch,Q,Q1),
 S1=[node(SN,St,Q1)|RestS],
 E1=[edge(Type,SN,CN,Ch)|E].

% node(Id,S1,Q) ==> node(Id,S1,Q u Ch),edge(Type,Id,NewC,Ch),node(NewC,VarState)
% Creation of a new CNode
 
apply_srule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,Ch1,graph(SV,CV1,[S1,C1,E1])):-
 select(node(SN,St1,Q),S,RestS),
 member(Ch1,Q),
 add(Type,Ch,Q,Q1),
 CV1 is CV+1,
 cnodes(CNs),
 member(K,CNs),
 S1=[node(SN,St,Q1)|RestS],
 C1=[node(CV1,K)|C],
 E1=[edge(Type,SN,CV1,Ch)|E]. 
 
% node(Id1,C1) ==> 
%      node(newS,VarState,Edges),node(Id1,C1),edge(Type,NewS,Id1,Ch)
% Creation of a new SNode
%
% Redundant because CN does not change
% 
 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% CRULES
%    
% C -- Ch --  |-->  C1 -- Ch1 
%
% node(Id,C1),edge(Type,Id,SN,Ch1),node(Id,St2,Q) 
%   ==> node(Id,C),edge(Type,Id,SN,Ch),node(Id,St2,Qu{Ch}) (Ch1 is in Q)
% Modify existing edge
 
apply_crule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,Ch1,graph(SV,CV,[S1,C1,E1])):-
 select(node(CN,St1),C,RestC),
 select(edge(Type,SN,CN,Ch1),E,RestE),
 select(node(SN,St2,Q),S,RestS),
 C1=[node(CN,St)|RestC],
 add(Type,Ch,Q,Q1),
 S1=[node(SN,St2,Q1)|RestS],
 E1=[edge(Type,SN,CN,Ch)|RestE]. 
  
% node(Id,C1),node(Id,St2,Q) 
%   ==> node(Id,C),edge(Type,Id,SN,Ch),node(Id,St2,Qu{Ch}) (Ch1 is in Q)
% Create a new edge
 
apply_crule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,Ch1,graph(SV,CV,[S1,C1,E1])):-
 select(node(CN,St1),C,RestC),
 select(node(SN,St2,Q),S,RestS),
 edge_invariant_cnodes(Type,CN,E),
 edge_invariant(Type,SN,CN,E),
 member(Ch1,Q),
 add(Type,Ch,Q,Q1),
 C1=[node(CN,St)|RestC],
 S1=[node(SN,St2,Q1)|RestS],
 E1=[edge(Type,SN,CN,Ch)|E]. 

%
% node(Id,C1) 
% ==> node(Id,C),edge(Type,Id,SN,Ch),node(Id,St2,Qu{Ch}) (Ch1 is in Q)
% Create a new SNode
 
apply_crule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,_,graph(SV1,CV,[S1,C1,E1])):-
 select(node(CN,St1),C,RestC),
 edge_invariant_cnodes(Type,CN,E),
 edges(Edges),
 SV1 is SV+1,
 snodes(SNs),
 member(K,SNs),
 C1=[node(CN,St)|RestC],
 S1=[node(SV1,K,Edges)|S],
 E1=[edge(Type,SV1,CN,Ch)|E]. 

%
% Create a new CNode
 
apply_crule(graph(SV,CV,[S,C,E]),Type,St,Ch,_,Ch1,graph(SV,CV1,[S1,C1,E1])):-
 select(node(SN,St2,Q),S,RestS),
 CV1 is CV+1,
 member(Ch1,Q),
 add(Type,Ch,Q,Q1),
 C1=[node(CV1,St)|C],
 S1=[node(SN,St2,Q1)|RestS],
 E1=[edge(Type,SN,CV1,Ch)|E].  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% CCRULES
%    
% C   |-->  C1 -- Ch1 
%
% node(Id,C1),edge(Type,Id,SN,Ch1),node(Id,St2,Q) 
%   ==> node(Id,C),node(Id,St2,Q) (Ch1 is in Q)
% Remove existing edge
 
apply_ccrule(graph(SV,CV,[S,C,E]),Type,St,St1,Ch1,graph(SV,CV,[S,C1,RestE])):-
 select(node(CN,St1),C,RestC),
 select(edge(Type,SN,CN,Ch1),E,RestE),
 member(node(SN,_,_),S),
 C1=[node(CN,St)|RestC]. 
  
% Change state of existing CNode
 
apply_ccrule(graph(SV,CV,[S,C,E]),Type,St,St1,Ch1,graph(SV,CV,[S,C1,E])):-
 select(node(CN,St1),C,RestC),
 member(node(SN,_,Q),S),
 edge_invariant(Type,SN,CN,E),
 edge_invariant_cnodes(Type,CN,E),
 member(Ch1,Q),
 C1=[node(CN,St)|RestC].
 
% Create a new SNode
 
apply_ccrule(graph(SV,CV,[S,C,E]),Type,St,St1,_,graph(SV1,CV,[S1,C1,E])):-
 select(node(CN,St1),C,RestC),
 edge_invariant_cnodes(Type,CN,E),
 edges(Edges),
 SV1 is SV+1,
 snodes(SNs),
 member(K,SNs),
 C1=[node(CN,St)|RestC],
 S1=[node(SV1,K,Edges)|S]. 

% Create a new CNode: redundant
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% DCRULES
%    
% C1 -- Ch  |-->  C2 
%
% Add the edge between two existing nodes
 
apply_dcrule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,graph(SV,CV,[S1,C1,E1])):-
 select(node(CN,St1),C,RestC),
 select(node(SN,St2,Q),S,RestS),
 edge_invariant(Type,SN,CN,E),
 edge_invariant_cnodes(Type,CN,E),
 add(Type,Ch,Q,Q1),
 C1=[node(CN,St)|RestC],
 S1=[node(SN,St2,Q1)|RestS],
 E1=[edge(Type,SN,CN,Ch)|E]. 
  
% Create a new SNode and an edge with an existing CNode
 
apply_dcrule(graph(SV,CV,[S,C,E]),Type,St,Ch,St1,graph(SV1,CV,[S1,C1,E1])):-
 select(node(CN,St1),C,RestC),
 edge_invariant_cnodes(Type,CN,E),
 edges(Edges),
 SV1 is SV+1,
 snodes(SNs),
 member(K,SNs),
 C1=[node(CN,St)|RestC],
 S1=[node(SV1,K,Edges)|S],
 E1=[edge(Type,SV1,CN,Ch)|E]. 

%
% Create a new CNode
 
apply_dcrule(graph(SV,CV,[S,C,E]),Type,St,Ch,_,graph(SV,CV1,[S1,C1,E1])):-
 select(node(SN,St2,Q),S,RestS),
 add(Type,Ch,Q,Q1),
 CV1 is CV+1,
 C1=[node(CV1,St)|C],
 S1=[node(SN,St2,Q1)|RestS],
 E1=[edge(Type,SN,CV1,Ch)|E]. 

 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% TRULES
%    
% C |--> C1 IF_FORALL Q
%
 
restrict([],_,[]).
 
restrict([A|Q],L,[A|R]):-
 member(A,L),
 restrict(Q,L,R).
 
restrict([A|Q],L,R):-
 \+ member(A,L),
 restrict(Q,L,R).

myrestrict(Q,L,[A|R]):-
 restrict(Q,L,[A|R]).
 
check(_,_,_,[]).

check(Type,SN,Q,[edge(Type,SN,_,Ch)|E]):-
 member(Ch,Q),
 check(Type,SN,Q,E).

check(Type,SN,Q,[edge(Type,SN1,_,_)|E]):-
 SN \= SN1,
 check(Type,SN,Q,E).

apply_trule(graph(SV,CV,[S,C,E]),Type,St,St1,Ok,graph(SV,CV,[S1,C,E])):-
 select(node(SN,St1,Q),S,RestS),
 restrict(Q,Ok,RestrQ), % RestrQ can be emptyset
 check(Type,SN,RestrQ,E),
 S1=[node(SN,St,RestrQ)|RestS].


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

notallowed(G,Invariants):-
  member(inv(IG),Invariants),
  graph_subsumption(IG,G).

allowedN(G,Invariants):- 
 \+(notallowed(G,Invariants)).
   
apply_msubsumes(G):-
 f(_,SG,_,_,_),
 graph_subsumption(SG,G).

removeAllF(G):-
 setof(_,removeF(G),_),!.

removeAllF(_):-!.

removeF(G):-
 clause(f(_,G1,_,_,_),true,Ref),
 graph_subsumption(G,G1),
 erase(Ref).   
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
select_and_apply(CS,NS):-
 invariants(Invariants),
 f(CS,G,Nf,_,_),
 copy_term((G),(CG)),
 srule(Type,S,C,S1,C1,RuleNo),
 apply_srule(G,Type,S,C,S1,C1,PreG),
 allowedN(PreG,Invariants),
 \+(graph_subsumption(CG,PreG)),
 \+(apply_msubsumes(PreG)),
% removeAllF(PreG),
 retract(countF(CountF)),
 CountF1 is CountF+1,
 assert(countF(CountF1)), 
 asserta(f(NS,PreG,CountF,Nf,RuleNo)).

select_and_apply(CS,NS):-
 invariants(Invariants),
 f(CS,G,Nf,_,_),
 copy_term((G),(CG)),
 crule(Type,S,C,S1,C1,RuleNo),
 apply_crule(G,Type,S,C,S1,C1,PreG),
 allowedN(PreG,Invariants),
 \+(graph_subsumption(CG,PreG)),
 \+(apply_msubsumes(PreG)),
% removeAllF(PreG),
 retract(countF(CountF)),
 CountF1 is CountF+1,
 assert(countF(CountF1)), 
 asserta(f(NS,PreG,CountF,Nf,RuleNo)).


select_and_apply(CS,NS):-
 invariants(Invariants),
 f(CS,G,Nf,_,_),
 copy_term((G),(CG)),
 ccrule(Type,S,S1,C1,RuleNo),
 apply_ccrule(G,Type,S,S1,C1,PreG),
 allowedN(PreG,Invariants),
 \+(graph_subsumption(CG,PreG)),
 \+(apply_msubsumes(PreG)),
% removeAllF(PreG),
 retract(countF(CountF)),
 CountF1 is CountF+1,
 assert(countF(CountF1)), 
 asserta(f(NS,PreG,CountF,Nf,RuleNo)).

select_and_apply(CS,NS):-
 invariants(Invariants),
 f(CS,G,Nf,_,_),
 copy_term((G),(CG)),
 dcrule(Type,S,C,S1,RuleNo),
 apply_dcrule(G,Type,S,C,S1,PreG),
 allowedN(PreG,Invariants),
 \+(graph_subsumption(CG,PreG)),
 \+(apply_msubsumes(PreG)),
% removeAllF(PreG),
 retract(countF(CountF)),
 CountF1 is CountF+1,
 assert(countF(CountF1)), 
 asserta(f(NS,PreG,CountF,Nf,RuleNo)).

select_and_apply(CS,NS):-
 invariants(Invariants),
 f(CS,G,Nf,_,_),
 copy_term((G),(CG)),
 trule(Type,S,S1,Ok,RuleNo),
 apply_trule(G,Type,S,S1,Ok,PreG),
 allowedN(PreG,Invariants),
 \+(graph_subsumption(CG,PreG)),
 \+(apply_msubsumes(PreG)),
% removeAllF(PreG),
 retract(countF(CountF)),
 CountF1 is CountF+1,
 assert(countF(CountF1)), 
 asserta(f(NS,PreG,CountF,Nf,RuleNo)).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

loop(N,OldF):-
 N1 is N+1,
 countF(F),TF is F-1,CF is TF-OldF,
 format('\tTot:~d New:~d',[TF,CF]),
 nl,format('[~d]',[N1]),
 flush_output,
 setof(_,select_and_apply(N,N1),_),
 !,
 loop(N1,TF).

loop(_,_):- 
 nl,
 write('--------------------------------------------------------'),nl,
 write('The fixpoint has been reached!').


go:-
 unsafe(L),
 clearF(L),
 loop(0,0).

pgo:-
 ptime(go).

clearF(L):-
 retractall(f(_,_,_,_,_)),
 retractall(countF(_)),
 assert(countF(1)),
 assertList(L). 
 
assertList([unsafe(UG)|Rest]):-
 !, 
 copy_term(UG,UG1),
 retract(countF(CountF)),
 CountF1 is CountF+1,
 assert(countF(CountF1)),
 assert(f(0,UG1,CountF,0,0)),
 assertList(Rest).
  
assertList([]). 

  
tracer(Step,K):-
 Step>=0,!,
 f(Step, G, K, Prev, Rule),
 write('Step'), write(Step),nl,
 write(G),nl,
% (rule(H,B,C,Rule);grule(H,B,C,G,Rule)), 
 write('Rule: '),write(Rule),nl,
 %read(_),
 Step1 is Step-1,
 tracer(Step1,Prev).

tracer(_,_).

ls:-listing(f).
lr:-listing(srule),listing(crule),listing(ccrule),listing(trule),listing(dcrule).
lc:-listing(count/1).

%%% MODEL 

