Hi!

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

Maybe add subsection titles to better mark separation between different
examples?

+The 'wip' (wakeup in preemptive) example introduced as a deterministic automaton
+can also be described as:
+
+- *X* = { ``any_thread_running`` }
+- *E* = { ``sched_waking`` }
+- *V* = { ``preemptive`` }
+- x\ :subscript:`0` = ``any_thread_running``
+- X\ :subscript:`m` = {``any_thread_running``}
+- *f* =
+   - *f*\ (``any_thread_running``, ``sched_waking``, ``preemptive==0``) = ``any_thread_running``
+- *i* =
+   - *i*\ (``any_thread_running``) = ``true``
+
+Which can be represented graphically as::
+
+     |
+     |
+     v
+   #====================#   sched_waking;preemptive==0
+   H                    H ------------------------------+
+   H any_thread_running H                               |
+   H                    H <-----------------------------+
+   #====================#
+
+In this example, by using the preemptive state of the system as an environment
+variable, we can assert this constraint on ``sched_waking`` without requiring
+preemption events (as we would in a deterministic automaton), which can be
+useful in case those events are not available or not reliable on the system.
+
+Since all the invariants in *i* are true, we can omit them from the representation.
+
+As a sample timed automaton we can define 'stall' as:

Maybe indicate this first one is a not properly correct example (correct
version follows)?

+
+- *X* = { ``dequeued``, ``enqueued``, ``running``}
+- *E* = { ``enqueue``, ``dequeue``, ``switch_in``}
+- *V* = { ``clk`` }
+- x\ :subscript:`0` = ``dequeue``
+- X\ :subscript:`m` = {``dequeue``}
+- *f* =
+   - *f*\ (``enqueued``, ``switch_in``, ``clk < threshold``) = ``running``
+   - *f*\ (``running``, ``dequeue``) = ``dequeued``
+   - *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued``
+- *i* = *omitted as all true*
+
+Graphically represented as::
+
+       |
+       |
+       v
+     #============================#
+     H          dequeued          H <+
+     #============================#  |
+       |                             |
+       | enqueue; reset(clk)         |
+       v                             |
+     +----------------------------+  |
+     |          enqueued          |  | dequeue
+     +----------------------------+  |
+       |                             |
+       | switch_in; clk < threshold  |
+       v                             |
+     +----------------------------+  |
+     |          running           | -+
+     +----------------------------+
+
+This model imposes that the time between when a task is enqueued (it becomes
+runnable) and when the task gets to run must be lower than a certain threshold.
+A failure in this model means that the task is starving.
+One problem in using guards on the edges in this case is that the model will
+not report a failure until the ``switch_in`` event occurs. This means that,
+according to the model, it is valid for the task never to run.
+As this is not exactly what is intended, we can change the model as:
+
+- *X* = { ``dequeued``, ``enqueued``, ``running``}
+- *E* = { ``enqueue``, ``dequeue``, ``switch_in``}
+- *V* = { ``clk`` }
+- x\ :subscript:`0` = ``dequeue``
+- X\ :subscript:`m` = {``dequeue``}
+- *f* =
+   - *f*\ (``enqueued``, ``switch_in``) = ``running``
+   - *f*\ (``running``, ``dequeue``) = ``dequeued``
+   - *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued``
+- *i* =
+   - *i*\ (``enqueued``) = ``clk < threshold``
+
+Graphically::
+
+    |
+    |
+    v
+  #=========================#
+  H        dequeued         H <+
+  #=========================#  |
+    |                          |
+    | enqueue; reset(clk)      |
+    v                          |
+  +-------------------------+  |
+  |        enqueued         |  |
+  |    clk < threshold      |  | dequeue
+  +-------------------------+  |
+    |                          |
+    | switch_in                |
+    v                          |
+  +-------------------------+  |
+  |         running         | -+
+  +-------------------------+
+
+In this case, we moved the guard as an invariant to the ``enqueued`` state,
+this means we not only forbid the occurrence of ``switch_in`` when ``clk`` is
+past the threshold but also mark as invalid in case we are *still* in
+``enqueued`` after the threshold. This model is effectively in an invalid state
+as soon as a task is starving, rather than when the starving task finally runs.
+
+Hybrid Automaton in C
+---------------------
+
+The definition of hybrid automata in C is heavily based on the deterministic
+automata one. Specifically, we add the set of environment variables and the
+constraints (both guards on transitions and invariants on states) as follows::
+
+  /* enum representation of X (set of states) to be used as index */
+  enum states {
+	dequeued = 0,
+	enqueued,
+	running,
+	state_max
+  };
+
+  #define INVALID_STATE state_max
+
+  /* enum representation of E (set of events) to be used as index */
+  enum events {
+	dequeue = 0,
+	enqueue,
+	switch_in,
+	event_max
+  };
+
+  /* enum representation of V (set of environment variables) to be used as index */
+  enum envs {
+	clk = 0,
+	env_max,
+	env_max_stored = env_max
+  };
+
+  struct automaton {
+	char *state_names[state_max];                  // X: the set of states
+	char *event_names[event_max];                  // E: the finite set of events
+	char *env_names[env_max];                      // V: the finite set of env vars
+	unsigned char function[state_max][event_max];  // f: transition function
+	unsigned char initial_state;                   // x_0: the initial state
+	bool final_states[state_max];                  // X_m: the set of marked states
+  };
+
+  struct automaton aut = {
+	.state_names = {
+		"dequeued",
+		"enqueued",
+		"running"
+	},
+	.event_names = {
+		"dequeue",
+		"enqueue",
+		"switch_in"
+	},
+	.env_names = {
+		"clk"
+	},
+	.function = {
+		{ INVALID_STATE,      enqueued, INVALID_STATE },
+		{ INVALID_STATE, INVALID_STATE,       running },
+		{      dequeued, INVALID_STATE, INVALID_STATE },
+	},
+	.initial_state = dequeued,
+	.final_states = { 1, 0, 0 },
+  };
+
+  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?

+	else
+		cancel_timer();
+	return res;
+  }
+
+The function ``verify_constraint``, here reported as simplified, checks guards,
+performs resets and starts timers to validate invariants according to
+specification.
+Due to the complex nature of environment variables, the user needs to provide
+functions to get and reset environment variables, although we provide some
+helpers for common types (e.g. clocks with ns or jiffy granularity).
+Invariants defined in this way only make sense as clock expirations (e.g. *clk
+< threshold*).

Thanks,
Juri