%
% My mods of Andrey's version from class of 30.05.2011.
%
% Important note: the following class example is provided "as
% is", for reference purposes, and without any claims of correctness.
%

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


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

% This loop, case 2, and original reach check, makes check loop...
% r(
%   p(pc(l2), data(X, Y, Z)), 	% from point
%   p(pc(l2), data(Xp, Yp, Zp)), 	% to point
%   (Xp=X+1, Yp=Y, Zp=Z),		% relation
%   t2prime			% label
%  ).

% % with case 1, this does not get added...
% r(
%   p(pc(l2), data(X, Y, Z)), 	% from point
%   p(pc(l3), data(Xp, Yp, Zp)), 	% to point
%   (Xp=X, Yp=Y, Zp=Z),		% relation
%   t3prime			% 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(p(_,  data(X, Y, Z)), []). 
preds(p(_,  data(X, Y, Z)), [X>=Y]). 
% preds(p(_,  data(X, Y, Z)), [X>=Y, Y>=Z]). 
% preds(p(_,  data(X, Y, Z)), [X>=Y, Y>=Z, X=<Y]).

%*******************************************************************************
% Misc
enumelems(L, Li, Enum) :- enumelems(L, Li, 1, Enum).
enumelems([], _, _, []).
enumelems([H|T], Li, I, Enum) :-
	member(I, Li),
	!,
	Enum = [H|Tsel],
	In is I + 1, 
	enumelems(T, Li, In, Tsel).
enumelems([_|T], Li, I, Enum) :-
	In is I + 1,
	enumelems(T, Li, In, Enum).

sublist(S, L) :- myprefix(S, L).
sublist(S, [_|T]) :- sublist(S, T).
myprefix([], _).
myprefix([H|T1], [H|T2]) :- myprefix(T1, T2).
%*******************************************************************************


check :-
	start(PC),
	retractall(abst_state(_, _)),
	retractall(parent(_,_,_)), % ex 9.6
	assert(abst_state(PC, [])),
	assert(worklist(abst_state(PC, []))),
	abst_reach_loop,
	safe_check,
	print_reached,
	print_parent.

abst_reach_loop :-

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

print_reached :-
	preds(p(_, Data), Preds),
	Data = data(x,y,z),
	print('Reached abstract states...\n'),
	format('~p\n', [Data]),
	findall(_, (
		    abst_state(PCp, Cube),
		    
		    enumelems(Preds, Cube, CubePreds),
		    print((PCp, CubePreds)), nl
		   ),
		_).

print_parent :-
	print('Parent ='),nl,
	findall(_, (
		    parent(F,R,T),
		    format('~p --> ~p --> ~p\n', [F,R,T])
		   ), 
		_).

safe_check :-
	error(PC),
	( abst_state(PC, _) ->
	  print('\nProgram is not safe!!!\n'),
	  makepath(P),
	  format('Counterexample path: ~p\n', [P])
	;
	  print('\nProgram is safe!!!\n')
	).

% ex 9.7
makepath(P) :-
	error(PC),
	abst_state(PC, Cube),
	makepath(abst_state(PC, Cube), Prev),
	rev(Prev, P).
makepath(As, P) :-
	parent(Asp, T, As),
	makepath(Asp, Pp),
	P = [T|Pp].
makepath(_, []).



abst_reach_step :-
	retract(worklist(abst_state(PC, Cube))),
	
	format('Selected state ~p\n', [(pc(PC),Cube)]),
	      
	concretize(Cube, Data),
	r(p(PC, Data), p(PCp, DataP), TransRel, _TId),
	format('Selected transition ~p\n', [_TId]),
	{TransRel},
	abstract(DataP, CubeP),

	format('Discovered state ~p\n', [(pc(PCp),CubeP)]),
	      
	% ex 10.3
	% Case 2:
	% Drop s from reached if s is subsumed by the newly reached abs. state.
	findall(_,
		(
		 abst_state(PCp, CubeReached),
		 \+ CubeReached = CubeP,
		 sublist(CubeReached, CubeP),
		 retract(abst_state(PCp, CubeReached)),
		 format('Retracting state ~p\n', [(pc(PCp), CubeReached)])
		),
		_),


	% Original reachability check
	% \+ abst_state(PCp, CubeP),

	
	% Case 1:
	% Do not add a new state s if s is subsumed by an already reached state.
	\+ (
	    abst_state(PCp, CubeReached),
	    sublist(CubeP, CubeReached)	    
	    ),
	
	assert(abst_state(PCp, CubeP)),
	assert(worklist(abst_state(PCp, CubeP))),
	assert(parent(abst_state(PC, Cube), _TId, abst_state(PCp, CubeP))), % ex 9.6
	format('Reached state ~p\n', [(pc(PCp),CubeP)]).











concretize(Cube, Data) :-
	preds(p(_, 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([], _, _).





abstract(Data, Cube) :-
	preds(p(_, 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).
	    
