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))
Or if you want to allow some other things to happen inbetween, then:
RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (SCHEDULING
until SWITCH))
Best regards,
Nam
