Lines Matching +full:lines +full:- +full:initial +full:- +full:states
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 ----------------------------
57 /* enum representation of X (set of states) to be used as index */
58 enum states {
75 char *state_names[state_max]; // X: the set of states
78 unsigned char initial_state; // x_0: the initial state
79 bool final_states[state_max]; // X_m: the set of marked states
100 The *transition function* is represented as a matrix of states (lines) and
101 events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
107 --------------------
109 The Graphviz open-source tool can produce the graphical representation
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" ];
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 -----
156 -------
166 ----------
184 Springer, Cham, 2019. p. 315-332.