% INPUT:
%   - POS expected execution order
%     eov_expect(Resource, ScopeBefore, ScopeAfter).
%
% OUTPUT:
%   - does actual execution order match expected one

%cfa_payload(X, Node, Path).

% ---------------------------------
% Find root of the Expectation POS:

cfa_payload(eov_payload(Resource, Pprev), scope(Sprev), ()):-
  eov_expect(Resource, Pprev, _);
  bind(Symprev, eov_checkpoint(Resource, Pprev));
  Symprev = s(_, _, Sprev).
  
eov_results(Resource, fail):-
  eov_expect(Resource, Pprev, Pnext);
  not cfa_payload(eov_payload(Resource, Pprev), scope(Snext), ());
  bind(Symnext, eov_checkpoint(Resource, Pnext));
  Symnext = s(_, _, Snext).
  
eov_results(Resource, success):-
  not eov_results(Resource, fail);
  eov_expect(Resource, _, _).
  
dfa_callguard(Sym, Impl):-  
  bind(Sym, eov_checkpoint(Resource, _));
  eov_results(Resource, Result);
  eov_analysis(Result, Impl).