%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: comm_path(Smth, X), v(Smth)}0.
comm_path(X, begin):- v(X); #sum{1: 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).    

    
%       ISSUES    
%==============================================================    
comm_spot_lost_end(Source) :- scan(_, source(Source), report(end)).
comm_spot_lost(Source, Spot) :- scan(Spot, source(Source), report(write)).
comm_spot_outofreach(X, Spot) :- scan(Spot, source(X), length(horizon)).
comm_spot_outofreach(X, Spot) :- scan(Spot, sink(X), length(horizon)).

comm_spot_corrupt_null(Sink) :- scan(_, sink(Sink), report(begin_)).
comm_spot_dup(Sink, Spot) :- scan(Spot, sink(Sink), report(read)).

comm_spot(Source):-comm_spot_lost_end(Source).
comm_spot(Source):-comm_spot_lost(Source, Spot).
comm_spot(X):-comm_spot_outofreach(X, Spot).
comm_spot(Sink):-comm_spot_corrupt_null(Sink).
comm_spot(Sink):-comm_spot_dup(Sink, Spot).


%       IMPLEMENTATION
%=============================================================
comm_impl(Source, commDirect):- comm_bind(Source, write); not comm_spot(Source).
bind(Source, callguard(commDirect)):- comm_impl(Source, commDirect).