% Abstract reachability
%

:- use_module(library(clpq)).
:- use_module(library(lists)).

%*******************************************************************************
% The program

start(pc(l1)).
error(pc(l5)).

r(
  p(pc(l1), data(X, Y, Z)), 	% from point
  p(pc(l2), data(Xp, Yp, Zp)), 	% to point
  (Y>=Z, Xp=X, Yp=Y, Zp=Z),	% relation
  t1				% label
 ).

r(
  p(pc(l2), data(X, Y, Z)), 	% from point
  p(pc(l2), data(Xp, Yp, Zp)), 	% to point
  (X+1=<Y, Xp=X+1, Yp=Y, Zp=Z),	% relation
  t2				% label
 ).

r(
  p(pc(l2), data(X, Y, Z)), 	% from point
  p(pc(l3), data(Xp, Yp, Zp)), 	% to point
  (X>=Y, Xp=X, Yp=Y, Zp=Z),	% relation
  t3				% label
 ).

r(
  p(pc(l3), data(X, Y, Z)), 	% from point
  p(pc(l4), data(Xp, Yp, Zp)), 	% to point
  (X>=Z, Xp=X, Yp=Y, Zp=Z),	% relation
  t4				% label
 ).

r(
  p(pc(l3), data(X, Y, Z)), 	% from point
  p(pc(l5), data(Xp, Yp, Zp)), 	% to point
  (X+1=<Z, Xp=X, Yp=Y, Zp=Z),	% relation
  t5				% label
 ).
%*******************************************************************************

preds(data(X, Y, Z), [X>=0, X>=Z, Y>=Z]).

check(L) :-
	start(PC),
	retractall(abst_state(_, _)),
	assert(abst_state(PC, [])),
	assert(worklist(abst_state(PC, []))),
	abst_reach_loop,
	findall((A,B),abst_state(A,B),L).

abst_reach_loop :-
	( findall(_, abst_reach_step, [_|_]) ->
	    abst_reach_loop
	;
	    true
	).

abst_reach_step :-
	retract(worklist(abst_state(PC, Cube))),
	concretize(Cube, Data),
	r(p(PC, Data), p(PCp, DataP), TransRel, _TId),
	{TransRel},
	abstract(DataP, CubeP),
	\+ abst_state(PCp, CubeP),
	assert(abst_state(PCp, CubeP)),
	assert(worklist(abst_state(PCp, CubeP))).

% posts all the predicates entailed so far
concretize(Cube, Data) :-
	preds(Data, Preds),
	concretize1(Cube, Preds, 1).
concretize1([C|Cs], [Pred|Preds], N) :-
	N1 is N+1,
	( N =:= C ->
	    {Pred},
	    concretize1(Cs, Preds, N1)
	;
	    concretize1([C|Cs], Preds, N1)
	).
concretize1([], _, _).


% filters the predicates that are entailed
abstract(Data, Cube) :-
	preds(Data, Preds),
	abstract1(Preds, 1, [], Cube).
abstract1([Pred|Preds], N, Acc, Cube) :-
	N1 is N+1,
	( entailed(Pred) ->
	    abstract1(Preds, N1, [N|Acc], Cube)
	;
	    abstract1(Preds, N1, Acc, Cube)
	).
abstract1([], _, RevCube, Cube) :- rev(RevCube, Cube).