%INPUT:
%   const horizon - Max Depth of communication analysis
%   comm_order(Alias)), bind(X, comm_alias(Alias) - to apply additional order constraints
%   dfa_uppy from dfa-propagation


%       INIT
%===========================================================
comm_bind(end, end).
comm_bind(begin, begin).
comm_bind(X, Op):- bind(X, commop(Op)).


%       ORDER
%============================================================
comm_path(X2, X1) :- bind(X2, comm_order(Alias)); bind(X1, comm_alias(Alias)).


%       INHERITS
%============================================================    
comm_path(X, Y) :- dfa_uppy(X, Y).

comm_path(end, X) :- v(X); #sum{1: weak(comm_path(Smth, X)), v(Smth)}0.
comm_path(X, begin):- v(X); #sum{1: weak(comm_path(X, Smth)), v(Smth)}0.


%       SCAN
%============================================================    
%SOURCE    
scan(X, source(X), length(0)) :- comm_bind(X, write).

scan(Z, source(X), length(Length + 1)) :- 
    comm_path(Z, Y);
    scan(Y, source(X), length(Length)); Length < horizon;
    not comm_bind(Z, _).

scan(Z, source(X), report(Op)) :- 
    comm_path(Z, Y);
    scan(Y, source(X), length(Length)); Length < horizon;
    comm_bind(Z, Op).    

%SINK
scan(X, sink(X), length(0)) :- comm_bind(X, read).

scan(Z, sink(X), length(Length + 1)) :- 
    comm_path(Y, Z);
    scan(Y, sink(X), length(Length)); Length < horizon;
    not comm_bind(Z, _).

scan(Z, sink(X), report(Op)) :- 
    comm_path(Y, Z);
    scan(Y, sink(X), length(Length)); Length < horizon;
    comm_bind(Z, Op).    
    

    
%       REPORTS    
%==============================================================    
comm_reports_type(rprtLostEnd; rprtLost; rprtCorruptNull; rprtDup; rprtOutOfReach).

comm_reports(rprtLostEnd    , Source, undef) :- scan(_, source(Source), report(end)).
comm_reports(rprtLost       , Source, Spot) :- scan(Spot, source(Source), report(write)).
comm_reports(rprtCorruptNull, Sink,   undef) :- scan(_, sink(Sink), report(begin)).
comm_reports(rprtDup        , Sink,   Spot) :- scan(Spot, sink(Sink), report(read)).

comm_halt(Source):- comm_reports(rprtLostEnd, Source, undef).
comm_halt(Source):- comm_reports(rprtLost, Source, _).
comm_halt(Sink):-   comm_reports(rprtCorruptNull, Sink, undef).
comm_halt(Sink):-   comm_reports(rprtDup, Sink, Spot).


%       WEAK REPORTS
%=============================================================
weak(comm_reports(rprtLostEnd   , Source)) :-       weak(scan(_, source(Source), report(end))).
weak(comm_reports(rprtLost      , Source, Spot)) :- weak(scan(Spot, source(Source), report(write))).
weak(comm_reports(rprtCorruptNull, Sink)) :-        weak(scan(_, sink(Sink), report(begin))).
weak(comm_reports(rprtDup, Sink, Spot)) :-          weak(scan(Spot, sink(Sink), report(read))).

comm_reports(rprtOutOfReach, X, Spot) :-            weak(scan(Spot, source(X), length(horizon))).
comm_reports(rprtOutOfReach, X, Spot) :-            weak(scan(Spot, sink(X), length(horizon))).


%       SOLUTIONS
%=============================================================
comm_impl(Source, commGuarded):- comm_bind(Source, write);
    not comm_halt(Source);
    1{ weak(comm_reports(Type, Source, _)): comm_reports_type(Type) }.
    
comm_impl(Source, commDirect):- comm_bind(Source, write); 
    not comm_halt(Source);
    not comm_impl(Source, commGuarded).
    
bind(Source, callguard(commDirect)):- comm_impl(Source, commDirect).
bind(Source, callguard(commGuarded)):- comm_impl(Source, commGuarded).


%       WEAK ANALYSIS
%=============================================================
weak(comm_path(X, Y)) :- weak(dfa_uppy(X, Y)).
weak(scan(Arg1, Arg2, Arg3)) :- scan(Arg1, Arg2, Arg3).

weak(scan(Z, sink(X), length(Length + 1))):-
    weak(comm_path(Y, Z));
    weak(scan(Y, sink(X), length(Length))); Length < horizon;
    not comm_bind(Z, _).
    
weak(scan(Z, sink(X), report(Op))):- 
    weak(comm_path(Y, Z));
    weak(scan(Y, sink(X), length(Length))); Length < horizon;
    comm_bind(Z, Op).  
    
    
weak(scan(Z, source(X), length(Length + 1))) :- 
    weak(comm_path(Z, Y));
    weak(scan(Y, source(X), length(Length))); Length < horizon;
    not comm_bind(Z, _).

weak(scan(Z, source(X), report(Op))) :- 
    weak(comm_path(Z, Y));
    weak(scan(Y, source(X), length(Length))); Length < horizon;
    comm_bind(Z, Op).