Parse error in LTL formulas with Until operator

Go down

Parse error in LTL formulas with Until operator

Post  Guest on Mon Oct 31, 2011 7:57 pm

Hi, I noticed that in assertions for LTL formulas with Until(U) operator, if the second operand of Until(U) is a double-quoted channel event, then PAT gives a parse error telling that the LTL formula is invalid. I think this is a kind of bug.

The following formulas give the same error:

#assert Robot() |= ("aChannel[1].value" U "aChannel[0].value");
#assert Robot() |= ("aChannel[1].value" U "anotherChannel?value");

whereas following don't give any error:

#assert Robot() |= ("aChannel[1].value" U anotherChannel.value);
#assert Robot() |= ("anotherChannel!value" U anEvent);

Thanks.

Guest
Guest


Back to top Go down

Thanks for reporting this

Post  pat team on Tue Nov 01, 2011 10:09 am

You are right. This is a bug in LTL parser, and I have fixed it.
I will release a new version for this bug fixing later.

If you need it now, please email pat@comp.nus.edu.sg

oguzcan wrote:Hi, I noticed that in assertions for LTL formulas with Until(U) operator, if the second operand of Until(U) is a double-quoted channel event, then PAT gives a parse error telling that the LTL formula is invalid. I think this is a kind of bug.

The following formulas give the same error:

#assert Robot() |= ("aChannel[1].value" U "aChannel[0].value");
#assert Robot() |= ("aChannel[1].value" U "anotherChannel?value");

whereas following don't give any error:

#assert Robot() |= ("aChannel[1].value" U anotherChannel.value);
#assert Robot() |= ("anotherChannel!value" U anEvent);

Thanks.

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

Back to top


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