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

Hi!

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

...

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?