Re: [RFC PATCH 11/17] Documentation/rv: Add documentation about hybrid automata

[Gabriele Monaco <gmonaco@redhat.com>]

On Tue, 2025-08-19 at 11:14 +0200, Juri Lelli wrote:
> 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?

Yeah indeed. That isn't even the 'standard' one as it isn't explicitly
configurable, but yes, at the expiration the invariant is already false
(I currently don't support AND/OR conditions in there).

I should make all this process clear, especially that those state
constraints are the only ones arming a timer and leaving the state
after that expiration (if the callback didn't run) or going through the
expiration itself implies a failure.

Thanks for pointing it out!
Gabriele