Parse error in LTL formulas with Until operator
PAT Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
Parse error in LTL formulas with Until operator
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.
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
Thanks for reporting this
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
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 Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
Permissions in this forum:
You cannot reply to topics in this forum