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


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

fsr_loop :-

	findall(_, (
		    reached(Vars, Pred),
		    format('fsrloop.[PC,X,Y,Z] = ~p\n', [Vars]),
		    format('fsrloop.C          = ~p\n', [Pred])
		   ), _),

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

fsr_safecheck :-
	error(Evars, Epred),
	( findall(_,
		  (
		   reached(Evars, ReachedState),
		   {ReachedState, Epred}
		  ),
		  [_|_]) ->
	  print('\nProgram is not safe!!!')
	;
	  print('\nProgram is safe!!!')
	).

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

	reached(FromVars, FromState),
	print('Select reached state...\n'),
	format('fsrloop.[PC,X,Y,Z]     = ~p\n', [FromVars]),
	format('fsrloop.FromState      = ~p\n', [FromState]),
	r(FromVars, ToVars, Rho, Tlabel),
	format('Transition ~p...\n', [Tlabel]),
	format('fsrloop.[PCp,Xp,Yp,Zp] = ~p\n', [ToVars]),
	format('fsrloop.Rho            = ~p\n', [Rho]),
	% {FromState, Rho},
	( {FromState, Rho} ->
	  true
	;
	  format('Transition ~p leads nowhere...\n', [Tlabel]),
	  fail
	),
	format('Transition ~p leads somewhere...\n', [Tlabel]),
	format('fsrloop.[PC,X,Y,Z]     = ~p\n', [FromVars]),
	format('fsrloop.[PCp,Xp,Yp,Zp] = ~p\n', [ToVars]),
	\+ (
	    findall(_,
		    (
		     reached(ToVars, ReachedState),
		     format('fsrloop.ReachedState   = ~p\n', [FromState]),
		     entailed(ReachedState)
		    ), [_|_]),
	    print('Already reached!\n')
	),
	
	print('Not yet reached!\n'),
	mydump(FromVars, NewVars, Dumped),
	conjunction(Dumped, NewState),
	[PC|_] = NewVars,
	[Loc|_] = ToVars,
	assert(reached(NewVars, (PC=Loc, NewState))),
	print('New reached state...\n'),
	format('NewVars                = ~p\n', [NewVars]),
	format('Dumped                 = ~p\n', [Dumped]),
	format('fsrloop.NewState = ~p\n', [(PC=Loc, NewState)]).

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