%
% Forward Symbolic Reachability algorithm
%
% 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, _, _, _], PC=1).
error([PC, _, _, _], PC=5).


r(
  [PC, X, Y, Z],			 % data at from loc
  [PCp, Xp, Yp, Zp],			 % data at to loc
  (PC=1, PCp=2, Y>=Z, Xp=X, Yp=Y, Zp=Z), % relation
  t1					 % label
 ).

r(
  [PC, X, Y, Z],			      % data at from loc
  [PCp, Xp, Yp, Zp],			      % data at to loc
  (PC=2, PCp= 2, X+1=<Y, Xp=X+1, Yp=Y, Zp=Z), % relation
  t2					      % label
 ).

r(
  [PC, X, Y, Z],			 % data at from loc
  [PCp, Xp, Yp, Zp],			 % data at to loc
  (PC=2, PCp=3, X>=Y, Xp=X, Yp=Y, Zp=Z), % relation
  t3					 % label
 ).

r(
  [PC, X, Y, Z],			 % data at from loc
  [PCp, Xp, Yp, Zp],			 % data at to loc
  (PC=3, PCp=4, X>=Z, Xp=X, Yp=Y, Zp=Z), % relation
  t4					 % label
 ).

r(
  [PC, X, Y, Z],			   % data at from loc
  [PCp, Xp, Yp, Zp],			   % data at to loc
  (PC=3, PCp=5, X+1=<Z, Xp=X, Yp=Y, Zp=Z), % relation
  t5					   % label
 ).

% r(
%   [PC, X, Y, Z],			 % data at from loc
%   [PCp, Xp, Yp, Zp],			 % data at to loc
%   (PC=3, PCp=5, Xp=X, Yp=Y, Zp=Z),	 % relation
%   t3prime				 % label
%  ).

% r(
%   [PC, X, Y, Z],			 % data at from loc
%   [PCp, Xp, Yp, Zp],			 % data at to loc
%   (PC=1, PCp=5, Xp=X, Yp=Y, Zp=Z),	 % relation
%   t1prime				 % label
%  ).



fsr :-
	retractall(parent(_,_,_)), % ex 9.7
	retractall(reached(_)),
	start(Svars, Spred),
	print('Start\n'),
	assert(reached(Svars, Spred)),
	fsr_loop,
	fsr_safecheck.

print_reached :-
	findall(_, (
		    reached(Vars, Pred),
		    % format('fsrloop.[PC,X,Y,Z] = ~p\n', [Vars]),
		    Vars = [pc,x,y,z],
		    format('fsrloop.C          = ~p\n', [Pred])
		   ), _).

fsr_loop :-

	print_reached,

	( findall(_, fsr_step, [_|_]) ->
	  print('\nStep\n'),
	  fsr_loop
	;
	  true
	).

fsr_safecheck :-
	error(Evars, Epred),
	( findall(_,
		  (
		   reached(Evars, ReachedState),
		   {ReachedState, Epred}
		  ),
		  [_|_]) ->
	  print('\nProgram is not safe!!!\n'),
	  makepath(P),
	  format('Counterexample path: ~p\n', [P])
	;
	  print('\nProgram is safe!!!\n')
	),
	print_reached.

% ex 9.7
makepath(P) :-
	reached(Vars, Child),
	error(Vars, Error),
	{Child,Error},
	makepath(Vars, Child, Prev),
	rev(Prev, P).
makepath(Vars, Child, P) :-
	parent(p(Pvars, Parent), T, p(Vars, Child)),
	makepath(Pvars, Parent, Pp),
	P = [T|Pp].
makepath(_, _, []).

fsr_step :-
	print('\nfsr_step\n'),

	reached(FromVars, FromState),
	\+ (
	    print('Select reached state...\n'),
	    FromVars = [pc,x,y,z],
	    format('fsrloop.FromState      = ~p\n', [FromState]),
	    fail
	),
	r(FromVars, ToVars, Rho, Tlabel),
	\+ (
	    format('Transition ~p...\n', [Tlabel]),
	    FromVars = [pc,x,y,z],
	    ToVars = [pc_p,x_p,y_p,z_p],
	    format('fsrloop.Rho            = ~p\n', [Rho]),
	    fail
	   ),
	% {FromState, Rho},
	( {FromState, Rho} ->
	  true
	;
	  format('Transition ~p leads nowhere...\n', [Tlabel]),
	  fail
	),
	format('Transition ~p leads somewhere...\n', [Tlabel]),
	\+ (
	    findall(_,
		    (
		     reached(ToVars, ReachedState),
		     entailed(ReachedState),
		     format('New state implies reached state ~p\n', [ReachedState]),
		     format('\twhere [pc,x,y,z] = ~p\n', [ToVars])
		    ), [_|_]),
	    print('New state is already reached!\n')
	),
	
	print('Not yet reached!\n'),
	mydump(FromVars, NewVars, QuantifierFree),
	conjunction(QuantifierFree, NewState),
	[PC|_] = NewVars,
	[Loc|_] = ToVars,
	assert(reached(NewVars, (PC=Loc, NewState))),	
	% ex 9.7
	assert(parent(p(FromVars, FromState),
		      Tlabel,
		      p(NewVars, (PC=Loc, NewState)))),
	\+ (
	    print('New reached state...\n'),
	    format('NewVars                = ~p\n', [NewVars]),
	    % NewVars = [pc,x,y,z],
	    % format('NewVars                = ~p\n', [NewVars]),
	    format('QuantifierFree         = ~p\n', [QuantifierFree]),
	    format('fsrloop.NewState = ~p\n', [(PC=Loc, NewState)]),
	    fail
	   ).

conjunction([], 1=1).
conjunction([H|Tl], F) :- conjunction(Tl, Fp), F = (Fp, H).

recreate_vars([], []).
recreate_vars([M|Ms], Vars) :-
	var(M),
	!,			% only recreate vars once!
	recreate_vars(Ms, _Vars),
	Vars = [M|_Vars].
recreate_vars([_|Ms], Vars) :-
	recreate_vars(Ms, _Vars),
	Vars = [_|_Vars].	
	
mydump(VarsAndNonVars, NewVars, Pred) :-
	recreate_vars(VarsAndNonVars, NewVars),
	dump(NewVars, NewVars, Pred).
	
