Assert goal repitively

[r.ben]

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]

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;

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