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
