Parse error in LTL formulas with Until operator

View previous topic View next topic 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

View previous topic View next topic Back to top

- Similar topics

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