Using the "until" operator

[abadithela]

Hi,

I'm trying to use the until operator (U) in one of my specifications but I get a KeyError. Isn't U the right way to denote this operator? I have been able to use the Next (X) operator without a problem. I haven't found this operator used in any of the examples provided. Can you please point me to any examples in which this operator has been used?

Thanks!
Apurva

[necozay]

"Until" is not part of GR(1). That is why it is not used in the examples. There is a conservative conversion to GR(1) implemented here. I think it should be handled automatically but I don't remember that part of the implementation. One temporary workaround is to use the encoding in the above link and manually write down the corresponding GR(1) spec for your problem.