Re: [PATCH v7 13/22] rv: Add support for LTL monitors

[Nam Cao <namcao@linutronix.de>]

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