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

[Gabriele Monaco <gmonaco@redhat.com>]

On Tue, 2025-08-19 at 10:53 +0200, Juri Lelli wrote:
> Hi!
> 
> On 14/08/25 17:08, Gabriele Monaco wrote:
> > 
> > +
> > +Examples
> > +--------
> 
> Maybe add subsection titles to better mark separation between
> different examples?

Sure, makes sense.

> 
> > +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)?

Yeah I should definitely be clearer about it. As you've guessed, this
example is to show things can be done differently as a tradeoff with
responsiveness, I should make that explicitly.

Thanks for the comments,
Gabriele