On 19/08/25 10:53, Juri Lelli wrote:
> Hi!
>
> On 14/08/25 17:08, Gabriele Monaco wrote:
...
> > + static bool verify_constraint(enum states curr_state, enum events event,
> > + enum states next_state)
> > + {
> > + bool res = true;
> > +
> > + /* Validate guards as part of f */
> > + if (curr_state == enqueued && event == sched_switch_in)
> > + res = get_env(clk) < threshold;
> > + else if (curr_state == dequeued && event == sched_wakeup)
> > + reset_env(clk);
> > +
> > + /* Validate invariants in i */
> > + if (next_state == curr_state)
> > + return res;
> > + if (next_state == enqueued && res)
> > + start_timer(clk, threshold);
>
> So, then the timer callback checks the invariant and possibly reports
> failure?
Ah, OK. The 'standard' ha_monitor_timer_callback just reports failure
(react) in case the timer fires. Which makes sense as at that point the
invariant is broken. Maybe add some wording to highlight this?
