communication.lp
No OneTemporary

File Metadata

Created
Mon, Aug 24, 6:12 AM

communication.lp

%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).

Event Timeline