/* A Tvp program for reverse

*/

#define COMPLETE
// #define ID_PRED

// **********************************************************************
// **********************************************************************
// SETS and PREDICATE DECLARATIONS
// **********************************************************************
// **********************************************************************
// ======================================================================

// ====================================================================== 
// Program variables and fields
// ====================================================================== 

%s ReverseVarAll	{x,y,z }

%s MainVarAll		{ list, res}

%s VarAll		ReverseVarAll + MainVarAll

%s Fields { n }
%s Bools { }

%s FP { fp1 }
%s FR { fr1 }

// ====================================================================== 
// Standard predicates
// ====================================================================== 

#include "predicate.tvp" 

// ======================================================================
// specific instrumentation predicates
// ======================================================================

%s CrossInstrum1 CrossInstrum1 + { reverse_n_succ }

#ifdef ID_PRED
%s CrossInstrum1 CrossInstrum1 + { reverse_n_pred }
#endif

foreach (m1 in Mode){
  foreach (m2 in Mode - { m1 }){
#ifdef ID_PRED
    %i reverse_n_pred[m1,m2](v) = A(v_1) ( n[m1](v_1,v) -> n[m2](v,v_1) ) nonabs
#endif
    %i reverse_n_succ[m1,m2](v) = A(v_1) ( n[m1](v,v_1) -> n[m2](v_1,v) ) nonabs
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode - {m1}){
    foreach (m3 in Mode - {m1,m2}){
      %r id_succ[n,m1,m2](v) & reverse_n_succ[m2,m3](v) ==> reverse_n_succ[m1,m3](v)
#ifdef ID_PRED
      %r reverse_n_succ[m1,m2](v) & id_pred[n,m2,m3](v) ==> reverse_n_succ[m1,m3](v)

      %r id_pred[n,m1,m2](v) & reverse_n_pred[m2,m3](v) ==> reverse_n_pred[m1,m3](v)
      %r reverse_n_pred[m1,m2](v) & id_succ[n,m2,m3](v) ==> reverse_n_pred[m1,m3](v)

      %r reverse_n_pred[m1,m2](v) & reverse_n_succ[m2,m3](v) ==> id_pred[n,m1,m3](v)
      %r reverse_n_succ[m1,m2](v) & reverse_n_pred[m2,m3](v) ==> id_succ[n,m1,m3](v)
#endif
    }
  }
}

%%

// **********************************************************************
// FUNCTION DEFINITIONS
// **********************************************************************

#include "function.tvp" 

%%

// **********************************************************************
// EQUATIONS
// **********************************************************************

/* The program we want to analyze:

procedure main(list) is
var res;
begin
main1:	res := reverse(list);
main2:
end

function reverse(x) : y is
var z;
begin
reverse_entry:	z := x->n;
reverse1:       x->n := null;
reverse2:	if (z != 0) then begin
reverse3:	   y := reverse(z);
reverse4:	   z->n = x;
		end
		else begin
reverse5:	  y := x;
		end
reverse_end:
reverse_summary:
end
*/

// Main
main_entry	= Setup_1[list]			(main_begin)
main_end	= ret_1_1[res, reverse, list]	(main_entry, reverse_summary)
// Reverse
reverse_entry	= call_X_1[reverse, list,x]	(main_entry)
reverse_entry	= call_X_1[reverse, z,x]	(reverse3)
reverse1	= AssignVarNext[z,x,n]		(reverse_entry)
reverse2	= AssignNextNull[x,n]		(reverse1)
reverse3	= IsVarNotNull[z]		(reverse2)
reverse4	= ret_1_1[y, reverse, z]	(reverse3,reverse_summary)
reverse_end	= AssignNextVar[z,n,x]		(reverse4)
reverse5	= IsVarNull[z]			(reverse2)
reverse_end	= AssignVarVar[y,x]		(reverse5)
reverse_summary	= summary_1_1[reverse,x,y]	(reverse_end)

%%

main_begin
main_entry
reverse_entry
reverse1
reverse2
reverse3
reverse4
reverse5
reverse_end
reverse_summary
main_end