On Tue, 2025-08-19 at 11:14 +0200, Juri Lelli wrote:

On 19/08/25 10:53, Juri Lelli wrote:

quoted

Hi!

On 14/08/25 17:08, Gabriele Monaco wrote:

...

quoted

quoted

+  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