execorder.lp
No OneTemporary
Actions

Subscribers

None

File Metadata

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