trace/rv/deterministic_automata.rst

10 - *X* is the set of states;
11 - *E* is the finite set of events;
12 - x\ :subscript:`0` is the initial state;
13 - X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
14 - *f* : *X* x *E* -> *X* $ is the transition function. It defines the state
22 - *X* = { ``preemptive``, ``non_preemptive``}
23 - *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
24 - x\ :subscript:`0` = ``preemptive``
25 - X\ :subscript:`m` = {``preemptive``}
26 - *f* =
27    - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
28    - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
29    - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
39           +---------------------------------+
41         #============#  preempt_disable   +------------------+
42     --> H preemptive H -----------------> |  non_preemptive  |
43         #============#                    +------------------+
46                                             +--------------+
49 ----------------------------
101 events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
106 Graphviz .dot format
107 --------------------
109 The Graphviz open-source tool can produce the graphical representation
111 The DOT format is widely used and can be converted to many other formats.
120         "__init_preemptive" -> "preemptive";
122         "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
123         "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
125         "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
132 This DOT format can be transformed into a bitmap or vectorial image
133 using the dot utility, or into an ASCII art using graph-easy. For
136   $ dot -Tsvg -o wip.svg wip.dot
137   $ graph-easy wip.dot > wip.txt
140 -----
143 in the example above and automatically convert it to the C representation
152 The 'wip.h' content is the code sample in section 'Deterministic Automaton
156 -------
162 for automata operations, while the graphical format for human interpretation;
166 ----------
184   Springer, Cham, 2019. p. 315-332.