%%%%%%%%%%%%%%%%%%%%%%%%%              dp_check program                  %%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% checks compliance of an architecture model with dp1, dp2, dp3, dp4 and dp5 design patterns.
%% 
%% This program is an implementation of the design patterns checker presented in:
%%  
%% Paper: "Specification of Schedulability Assumptions to Leverage Multicore Analysis" 
%% Authors: S Rubini, VA Nicolas, F Singhoff, A Plantec, HN Tran, P Dissaux. 
%%          Univ Brest, Lab-STICC, CNRS, UMR 6285, F-29200 Brest, France.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- lib(lists).

:- dynamic sw_archi/1,
   tasks/1,
   processing_elements/1,
   resources/1,
   am_PE_use/2, 
   am_R_use/2, 
   dm_PE_allowed/2,
   dm_PE_actual/2,  
   dm_R_allowed/2,
   dm_R_actual/2,  
   dm_PE_scheduling/3,
   ha_independent/1,
   ha_dependent/1,
   am_time/3,
   a_type/2,  
   a_proc_type/2, 
   a_proc_isa/2,  
   a_proc_speed/2,
   a_mem_type/2,
   a_mem_cache_associativity/2,
   a_mem_cache_level/2,
   a_mem_cache_size/2,
   a_mem_cache_line_size/2,
   a_mem_cache_miss_time/2,
   a_conn_type/2,
   end_with_success/0.
   

% Main predicate: dp_check(AMN)
% AMN = Architecture Model file Name (without the .ecl extension) 
dp_check(AMN) :-    
        atom_string(AMN,N2),
        getcwd(N1),  
        append_strings(N1,N2,N),
        os_file_name(F,N),
        compile(F), 
        archi_model_build(N2), !,
	writeln(""),
	writeln("---------------------------- valid design patterns (among dp1, dp2, dp3, dp4, dp5)"), writeln(""),
        dp(N2).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   
archi_model_build(A) :-
        retract_archi,
        archi_model_base(Lb),
        (foreach(X,Lb) do assert(X)),
        archi_model_spec(A,Ls),
        (foreach(X,Ls) do assert(X)).


archi_model_base(L) :-  
        L = [ am_PE_use(error,[]),  
              dm_R_actual(error,error),  
              dm_PE_actual(error,error),  
              dm_PE_scheduling(error,error,error),  
              a_proc_isa(error,error), 
              a_proc_speed(error,error)].

     
retract_archi :-
        retract_all(sw_archi(_)),
        retract_all(tasks(_)),
        retract_all(processing_elements(_)),
        retract_all(resources(_)),
        retract_all(dm_R_actual(_,_)),  
        retract_all(dm_R_allowed(_,_)),  
        retract_all(am_PE_use(_,_)), 
        retract_all(am_R_use(_,_)),  
        retract_all(dm_PE_allowed(_,_)),
        retract_all(dm_PE_actual(_,_)),  
        retract_all(dm_PE_scheduling(_,_,_)),
        retract_all(ha_independent(_)),
        retract_all(ha_dependent(_)),
        retract_all(am_time(_,_,_)),
        retract_all(a_proc_type(_,_)), 
        retract_all(a_proc_isa(_,_)),  
        retract_all(a_proc_speed(_,_)),
        retract_all(a_type(_,_)),     
        retract_all(a_mem_type(_,_)),
        retract_all(a_mem_cache_associativity(_,_)),
        retract_all(a_mem_cache_level(_,_)),
        retract_all(a_mem_cache_size(_,_)),
        retract_all(a_mem_cache_line_size(_,_)),
        retract_all(a_mem_cache_miss_time(_,_)),
        retract_all(a_conn_type(_,_)),
	retract_all(end_with_success).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dp(AMN) :- dp1, write(AMN), writeln(" is DP1 compliant"), fail.
dp(AMN) :- dp2, write(AMN), writeln(" is DP2 compliant"), fail.
dp(AMN) :- dp3, write(AMN), writeln(" is DP3 compliant"), fail.
dp(AMN) :- dp4, write(AMN), writeln(" is DP4 compliant"), fail.
dp(AMN) :- dp5, write(AMN), writeln(" is DP5 compliant"), fail.
dp(_).


% dp1
dp1 :- sw_archi(A), member(A,[log_upg,log_sync]),
       tasks(LTasks),
       processing_elements(LPE), !,
       dep_comp(LTasks,LPE), !,
       exe_inde(LTasks,LPE), !,
       fea_id(LTasks),!.


% dp2 
dp2 :- sw_archi(A), member(A,[log_upg,log_rav,log_sync]),
       tasks(LTasks),
       processing_elements(LPE), !,
       dep_part(LTasks,LPE), !,
       exe_inde(LTasks,LPE), !,
       fea_id(LTasks),!.


% dp3 
dp3 :- sw_archi(A), member(A,[log_upg,log_rav,log_sync]),
       tasks(LTasks),
       processing_elements(LPE), !,
       dep_glob(LTasks,LPE), !,
       exe_inde(LTasks,LPE), !,
       fea_id(LTasks), !.


% dp4
dp4 :- sw_archi(A), member(A,[log_upg,log_sync]),
       tasks(LTasks),
       processing_elements(LPE), !,
       dep_part(LTasks,LPE), !,
       exe_inde(LTasks,LPE), !,
       fea_id(LTasks), !,
       fea_ic(LTasks),!.


% dp5 
dp5 :- sw_archi(A), member(A,[log_upg,log_sync]),
       tasks(LTasks),
       processing_elements(LPE), !,
       dep_part(LTasks,LPE), !,
       exe_dep(LTasks,LPE), !,
       fea_id(LTasks), !,
       resources(LR), !,
       fea_dram(LTasks,LR),!.    


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dep_comp([],_).
dep_comp([T],LPE):- 
        dm_PE_allowed(T,[C|LC]), !,
        (foreach(P,[C|LC]), param(LPE) do
            member(P,LPE), !
        ), !.
dep_comp([T1|LT],LPE) :-
	dm_PE_allowed(T1,LP1), !,
        LP1 = [_|_],
        (foreach(P,LP1), param(LPE) do 
                member(P,LPE), !
        ), !,
  	(foreach(T2,LT), param(LP1) do 	 
           	dm_PE_allowed(T2,LP2), !,
            	(subtract(LP1,LP2,[]), 
                 subtract(LP2,LP1,[])  
             	;  
            	intersection(LP1,LP2,[])), !
      	), !,
	dep_comp(LT,LPE).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dep_part([],_).
dep_part([T],LPE):- 
        dm_PE_actual(T,P),
        member(P,LPE), !, 
        dm_PE_scheduling(P,T,_), !.
dep_part([T1|LT],LPE) :- 
        dm_PE_actual(T1,P),
        member(P,LPE), !,
        dm_PE_scheduling(P,T1,S), !,
        (foreach(T2,LT), param(P,S) do                
            (dm_PE_actual(T2,P) -> 
                dm_PE_scheduling(P,T2,S)
            ;
                true)
        ), !,
        dep_part(LT,LPE).
            

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dep_glob([],_).
dep_glob([T],LPE):- 
        dm_PE_allowed(T,[C|LC]),
        dm_PE_scheduling(C,T,S),
        (foreach(P,[C|LC]), param(LPE,T,S) do
            member(P,LPE), !,
            dm_PE_scheduling(P,T,S), !
        ), !.
dep_glob([T1|LT],LPE) :- 
        dm_PE_allowed(T1,LP1), !,
        LP1 = [P1|_],
        dm_PE_scheduling(P1,T1,S1), !,
        (foreach(P,LP1), param(LPE,T1,S1) do 
                member(P,LPE), !,
                dm_PE_scheduling(P,T1,S1), !
        ), !,
        (foreach(T2,LT), param(LP1,P1,S1) do 
            dm_PE_allowed(T2,LP2), 
            (subtract(LP1,LP2,[]), 
             subtract(LP2,LP1,[]), 
             dm_PE_scheduling(P1,T2,S1)
            ;  
             intersection(LP1,LP2,[]))
        ), !,
        dep_glob(LT,LPE).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% see below explanations for not using the 2nd parameter
exe_inde(LT,_) :- 
        (foreach(T,LT) do 
            dm_PE_allowed(T,LP), !,
            LP = [_|_],
            %% exe_inde is always called after dep_comp, dep_part or dep_glob.
            %% dep_comp, dep_part or dep_glob check member(P,List of PEs) for all P in LP
            %% so no need to check it once again here.
            (foreach(P,LP) do ha_independent(P)), !,
            (dm_PE_actual(T,P) -> ha_independent(P)
            ; 
             true), !
        ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% see below explanations for not using the 2nd parameter
      %% exe_dep is always called after dep_part.
      %% dep_part checks member(P,List of PEs) for all P in LP
      %% so no need to check it once again here.
exe_dep([T],_) :- 
        dm_PE_allowed(T,LP),
        LP = [_|_],
        member(P,LP), 
        ha_dependent(P), !.
exe_dep([T],LP) :- 
        dm_PE_actual(T,P),
        member(P,LP),
        ha_dependent(P), !.
exe_dep([T|_],_) :- 
        dm_PE_allowed(T,LP),
        LP = [_|_],
        member(P,LP), 
        ha_dependent(P), !.
exe_dep([T|_],LP) :- 
        dm_PE_actual(T,P),
        member(P,LP),
        ha_dependent(P), !.
exe_dep([_|LT],LP) :- 
        exe_dep(LT,LP).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

fea_id(LT) :-
        build_set_DM_PE_allowed_actual(LT,LP_allowed_actual), !,     
        (find_a_proc_speed(_,S,LP_allowed_actual) ->
            (foreach(P,LP_allowed_actual), param(S) do 
                (a_proc_speed(P,S2) -> S=S2
                ;
                                     true)
            )
        ;
            true
        ), !, 
        (find_a_proc_isa(_,I,LP_allowed_actual) ->
            (foreach(P,LP_allowed_actual), param(I) do 
                (a_proc_isa(P,I2) -> I=I2
                ;
                                     true)
            )
        ;
            true
        ), !. 
        
find_a_proc_speed(P,V,L) :- 
        a_proc_speed(P,V),
        member(P,L), !.

find_a_proc_isa(P,V,L) :- 
        a_proc_isa(P,V),
        member(P,L), !.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

fea_ic(LT) :-
        build_set_DM_PE_allowed_actual(LT,LP_allowed_actual), !,
        (foreach(P,LP_allowed_actual) do 
            am_PE_use(P,[R]),
            a_mem_type(R,instruction_cache_type),
            a_mem_cache_associativity(R,1),
            a_mem_cache_miss_time(R,_), !      
        ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

fea_dram(LT,LR) :-  
        build_set_DM_PE_allowed_actual(LT,LP_allowed_actual), !,
        build_set_DM_R_allowed_actual(LT,LR_allowed_actual), !,
        (foreach(R,LR_allowed_actual) do a_mem_type(R,bank)), !,
        LP_allowed_actual = [P1|LP_allowed_actual2],
        am_PE_use(P1,[R]), !,
        member(R,LR), !,       
        a_mem_type(R,idCache), !,
        (foreach(P,LP_allowed_actual2), param(R) do am_PE_use(P,[R])), !,
        am_R_use(R,B), !,
        (foreach(R,LR_allowed_actual), param(B) do member(R,B)), !.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

build_set_DM_PE_allowed_actual(LT,LP_allowed_actual) :-
        (foreach(T,LT), fromto([],In,Out,Out2) do
            (dm_PE_allowed(T,LP) ->          
                append(In,LP,In2)
            ; 
                In2 = In),
            (dm_PE_actual(T,P) -> 
                Out = [P|In2]
            ; 
                Out = In2), !
        ), !,
        del_duplicates(Out2,LP_allowed_actual).

build_set_DM_R_allowed_actual(LT,LR_allowed_actual) :-
        (foreach(T,LT), fromto([],In,Out,Out2) do
            (dm_R_allowed(T,LR) ->           
                append(In,LR,In2)
            ; 
                In2 = In),
            (dm_R_actual(T,LRa) -> 
                append(In2,LRa,Out)
            ; 
                Out = In2), !
        ), !,
        del_duplicates(Out2,LR_allowed_actual).

del_duplicates([X],[X]) :- !.
del_duplicates([X|L],L2) :-
        member(X,L), !,
        del_duplicates(L,L2).
del_duplicates([X|L],[X|L2]) :-
        del_duplicates(L,L2).