PAT Forum
Would you like to react to this message? Create an account in a few clicks or log in to continue.

Parse error in LTL formulas with Until operator

Go down

Parse error in LTL formulas with Until operator Empty Parse error in LTL formulas with Until operator

Post  Guest 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

Parse error in LTL formulas with Until operator Empty Thanks for reporting this

Post  pat team 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

http://www.comp.nus.edu.sg/~pat/

Back to top Go down

Back to top

- Similar topics

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