Assert goal repitively

View previous topic View next topic Go down

Assert goal repitively

Post  r.ben on Fri Oct 07, 2011 7:21 pm

Hi all,

I want to assert a goal like this:

#define goal (x[0] > 0) && (x[1]>0) && ... && (x[30]>0); // this is too long
#assert System |= []<>goal;

Is there an easier way to define the goal instead of above in PAT?

Thanks!
Ben

r.ben

Posts : 1
Join date : 2011-10-07

View user profile

Back to top Go down

Yes. This is possible

Post  pat team on Sun Oct 16, 2011 10:42 pm

PAT has this syntax. See the example below

var x[31];

System = Skip;

#define goal && i:{0..30} @ (x[i] > 0); // this is too long
#assert System |= []<>goal;


r.ben wrote:Hi all,

I want to assert a goal like this:

#define goal (x[0] > 0) && (x[1]>0) && ... && (x[30]>0); // this is too long
#assert System |= []<>goal;

Is there an easier way to define the goal instead of above in PAT?

Thanks!
Ben

pat team
Admin

Posts : 17
Join date : 2010-02-15

View user profile http://www.comp.nus.edu.sg/~pat/

Back to top Go down

View previous topic View next topic Back to top


 
Permissions in this forum:
You cannot reply to topics in this forum