need for more static semantics
The following property features a static semantics problem: param0=='NS' should be r.param0=='NS'
prop03_NoDoubleGreenAfterLastRedonNS :
(after last Red_ENT r where param0=='NS', after first Green_Ent g where g.param0==r.param0, absence_of Green_ENT g2 where g.param0 != g2.param0);
The IDE does not detect this problem and the property is vacuously true