using past and history function in invariants

[sderrien]

Dear all,

I have been trying to use the history and past function to verify simple invariants, based on the discussion #6 (comment), but I have trouble understanding some Uclid results.

For example, for the example below, I would expect invariants fail0 and fail1 to hold, but I get counter examples, and since it is not possible to print the value of history(cpt,1) in the cex, it is difficult to understand where the problem stems from.

Any advice ?

`
module main {

	var cpt,oldcpt : integer ;
	
	init {
		cpt=0;
	}
  
	next {
		cpt'= cpt+1;
		oldcpt'=cpt;
	}

	invariant inv0 : (cpt>=0);
	invariant pass0 : (cpt>1) ==> (oldcpt==(cpt-1)) ;
	invariant pass1 : (cpt>1) ==> (history(cpt,1)<(cpt)) ;

	invariant fail0 : (cpt>1) ==> (history(cpt,1)==oldcpt) ;
	invariant fail1 : (cpt>1) ==> (history(cpt,1)==(cpt-1)) ;

	control {
		vobj = induction(2);
		check;
		print_results;
 		vobj.print_cex(cpt,oldcpt);
	}
	
}

`

PS: thanks you for Uclid5, this is a really a very nice tool

Regards,

Steven

[polgreen]

Hi,

I think this may be a bug to do with how we are handling history in the SMT query generation (note that the invariants pass if you use induction(1) but fail if you use induction(2). That is certainly surprising).

Let me look into it and get back to you.

[sderrien]

Hello,

Thank you for the fast feedback.

I'll stick to induction(1) for the moment.

Regards.

[polgreen]

Fixed! Thanks for the bug report!