1Deterministic Automata
  2======================
  3
  4Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
  5
  6        *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
  7
  8where:
  9
 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
 15  transition in the occurrence of an event from *E* in the state *X*. In the
 16  special case of deterministic automata, the occurrence of the event in *E*
 17  in a state in *X* has a deterministic next state from *X*.
 18
 19For example, a given automaton named 'wip' (wakeup in preemptive) can
 20be defined as:
 21
 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``
 30
 31One of the benefits of this formal definition is that it can be presented
 32in multiple formats. For example, using a *graphical representation*, using
 33vertices (nodes) and edges, which is very intuitive for *operating system*
 34practitioners, without any loss.
 35
 36The previous 'wip' automaton can also be represented as::
 37
 38                       preempt_enable
 39          +---------------------------------+
 40          v                                 |
 41        #============#  preempt_disable   +------------------+
 42    --> H preemptive H -----------------> |  non_preemptive  |
 43        #============#                    +------------------+
 44                                            ^              |
 45                                            | sched_waking |
 46                                            +--------------+
 47
 48Deterministic Automaton in C
 49----------------------------
 50
 51In the paper "Efficient formal verification for the Linux kernel",
 52the authors present a simple way to represent an automaton in C that can
 53be used as regular code in the Linux kernel.
 54
 55For example, the 'wip' automata can be presented as (augmented with comments)::
 56
 57  /* enum representation of X (set of states) to be used as index */
 58  enum states {
 59	preemptive = 0,
 60	non_preemptive,
 61	state_max
 62  };
 63
 64  #define INVALID_STATE state_max
 65
 66  /* enum representation of E (set of events) to be used as index */
 67  enum events {
 68	preempt_disable = 0,
 69	preempt_enable,
 70	sched_waking,
 71	event_max
 72  };
 73
 74  struct automaton {
 75	char *state_names[state_max];                   // X: the set of states
 76	char *event_names[event_max];                   // E: the finite set of events
 77	unsigned char function[state_max][event_max];   // f: transition function
 78	unsigned char initial_state;                    // x_0: the initial state
 79	bool final_states[state_max];                   // X_m: the set of marked states
 80  };
 81
 82  struct automaton aut = {
 83	.state_names = {
 84		"preemptive",
 85		"non_preemptive"
 86	},
 87	.event_names = {
 88		"preempt_disable",
 89		"preempt_enable",
 90		"sched_waking"
 91	},
 92	.function = {
 93		{ non_preemptive,  INVALID_STATE,  INVALID_STATE },
 94		{  INVALID_STATE,     preemptive, non_preemptive },
 95	},
 96	.initial_state = preemptive,
 97	.final_states = { 1, 0 },
 98  };
 99
100The *transition function* is represented as a matrix of states (lines) and
101events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
102in O(1). For example::
103
104  next_state = automaton_wip.function[curr_state][event];
105
106Graphviz .dot format
107--------------------
108
109The Graphviz open-source tool can produce the graphical representation
110of an automaton using the (textual) DOT language as the source code.
111The DOT format is widely used and can be converted to many other formats.
112
113For example, this is the 'wip' model in DOT::
114
115  digraph state_automaton {
116        {node [shape = circle] "non_preemptive"};
117        {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
118        {node [shape = doublecircle] "preemptive"};
119        {node [shape = circle] "preemptive"};
120        "__init_preemptive" -> "preemptive";
121        "non_preemptive" [label = "non_preemptive"];
122        "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
123        "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
124        "preemptive" [label = "preemptive"];
125        "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
126        { rank = min ;
127                "__init_preemptive";
128                "preemptive";
129        }
130  }
131
132This DOT format can be transformed into a bitmap or vectorial image
133using the dot utility, or into an ASCII art using graph-easy. For
134instance::
135
136  $ dot -Tsvg -o wip.svg wip.dot
137  $ graph-easy wip.dot > wip.txt
138
139dot2c
140-----
141
142dot2c is a utility that can parse a .dot file containing an automaton as
143in the example above and automatically convert it to the C representation
144presented in [3].
145
146For example, having the previous 'wip' model into a file named 'wip.dot',
147the following command will transform the .dot file into the C
148representation (previously shown) in the 'wip.h' file::
149
150  $ dot2c wip.dot > wip.h
151
152The 'wip.h' content is the code sample in section 'Deterministic Automaton
153in C'.
154
155Remarks
156-------
157
158The automata formalism allows modeling discrete event systems (DES) in
159multiple formats, suitable for different applications/users.
160
161For example, the formal description using set theory is better suitable
162for automata operations, while the graphical format for human interpretation;
163and computer languages for machine execution.
164
165References
166----------
167
168Many textbooks cover automata formalism. For a brief introduction see::
169
170  O'Regan, Gerard. Concise guide to software engineering. Springer,
171  Cham, 2017.
172
173For a detailed description, including operations, and application on Discrete
174Event Systems (DES), see::
175
176  Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
177  event systems. Boston, MA: Springer US, 2008.
178
179For the C representation in kernel, see::
180
181  De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
182  Silva. Efficient formal verification for the Linux kernel. In:
183  International Conference on Software Engineering and Formal Methods.
184  Springer, Cham, 2019. p. 315-332.