On Fri, May 09, 2025 at 04:50:29PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-05-09 at 10:12 +0200, Nam Cao wrote:
> > + def negate(self):
> > + # ![]F == <>(!F)
> > + return EventuallyOp(self.left,
> > self.right.negate()).normalize()
>
> Shouldn't this be:
> + return EventuallyOp(self.child.negate()).normalize()
Yes, remnant of the old version :(
> > +def p_unop(p):
> > + '''
> > + unop : ALWAYS ltl
> > + | EVENTUALLY ltl
> > + | NOT ltl
> > + '''
> > + if p[1] == "always":
> > + op = AlwaysOp(p[2])
> > + if p[1] == "eventually":
> > + op = EventuallyOp(p[2])
> > + if p[1] == "not":
> > + op = NotOp(p[2])
>
> Pylint is complaining about this one, wouldn't it be better changing it to an
> if/elif chain and addding:
>
> else:
> raise ValueError("Invalid unary operator: %s" % p[1])
lex should have failed due to unknown token before getting here. But yes,
this would be a good change.
> > +def parse_ltl(s: str) -> ASTNode:
> > + spec = parser.parse(s)
> > +
> > + subexpr = dict()
> > +
> > + for assign in spec:
> > + if assign[0] == "RULE":
> > + rule = assign[1]
> > + else:
> > + subexpr[assign[0]] = assign[1]
>
> rule may be undefined here (but I guess python will just say variable rule is
> undefined and it would be quite clear the ltl didn't start with a rule.
We could make the error verbose.
> I'm still getting a few more errors but my model may be to blame, still need
> to
> play a bit.
Feel free to send me the model. Maybe it is a bug in the script. But I
would be happy to help debugging your model as well.
Thanks for the feedback,
Nam
