On Mon, 2025-07-14 at 14:48 +0200, Nam Cao wrote:
> On Mon, Jul 14, 2025 at 02:42:10PM +0200, Nam Cao wrote:
> > On Mon, Jul 14, 2025 at 02:18:05PM +0200, Gabriele Monaco wrote:
> > > Now I can't think of a way to rewrite the model to allow a pulse
> > > in
> > > sched_switch, that is /whenever scheduling turns to true, the
> > > next
> > > event is a switch/ instead of /any time scheduling is true, the
> > > next
> > > event is a switch/.
> > >
> > > I tried something like:
> > > RULE = always ((not SCHEDULING and next SCHEDULING) imply next
> > > SWITCH)
> >
> > Be careful of operator precedence. This rule is also what I would
> > suggest,
> > but you need parentheses:
> >
> > RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> > (next SWITCH))
>
> Actually no, this also does not work. You need double 'next':
>
> RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> (next next SWITCH))
>
Thanks! This one seems to work.
> Not sure what you mean by .init field
I meant in ltl2k there's this condition for variable usage but not for
variable definition. I'm not sure exactly what it stands for.
_fill_start():
...
if not node.init:
continue
But I guess you got what I meant already.
> Btw, I think this "(not X) and (next X)" seems very useful. So we
> could
> define a helper for this, perhaps something like "rising_edge".
Yeah good idea! I see myself mixing up in the future otherwise..
I guess you'd need to define also a falling_edge for its counterpart.
Or perhaps making it more compact as just rising/falling (with good
documentation or references to somewhere defining it).
Also we need to make clear this operator takes 2 instances, so whatever
happens after (next) it needs a double next.
Maybe it gets complicated but in the future we might have also some
nextN (next2, next3, etc. with a sensible limit not to explode the
generated code) or something along the line.
> Thanks for the report, I will post some patches to address these
> problems
> with the scripts.
Great, thanks!
I'd say since those are unrelated and the next works as intended, feel
free to add
Tested-by: Gabriele Monaco <gmon...@redhat.com>
Thanks again,
Gabriele
