确定性自动机¶
形式上，一个确定性自动机，用 G 表示，定义为一个五元组
G = { X, E, f, x0, Xm }
其中
X 是状态的集合；
E 是事件的有限集合；
x0 是初始状态；
Xm （X 的子集）是标记（或最终）状态的集合。
f : X x E -> X 是转换函数。它定义了在状态 X 中发生来自 E 的事件时的状态转换。在确定性自动机的特殊情况下，在 X 的状态中发生 E 中的事件，其下一个状态是确定的来自 X 的状态。
例如，一个名为 ‘wip’（抢占式唤醒）的给定自动机可以定义为
X = {
preemptive,non_preemptive}E = {
preempt_enable,preempt_disable,sched_waking}x0 =
preemptiveXm = {
preemptive}- f =
f(
preemptive,preempt_disable) =non_preemptivef(
non_preemptive,sched_waking) =non_preemptivef(
non_preemptive,preempt_enable) =preemptive
这种形式化定义的好处之一是，它可以以多种格式呈现。例如，使用顶点（节点）和边的图形表示，这对于操作系统从业者来说非常直观，没有任何损失。
前面的 ‘wip’ 自动机也可以表示为
preempt_enable
+---------------------------------+
v |
#============# preempt_disable +------------------+
--> H preemptive H -----------------> | non_preemptive |
#============# +------------------+
^ |
| sched_waking |
+--------------+
C 语言中的确定性自动机¶
在论文 “Linux 内核的高效形式化验证” 中，作者提出了一种在 C 语言中表示自动机的简单方法，该方法可以用作 Linux 内核中的常规代码。
例如，’wip’ 自动机可以表示为（带有注释）
/* enum representation of X (set of states) to be used as index */
enum states {
preemptive = 0,
non_preemptive,
state_max
};
#define INVALID_STATE state_max
/* enum representation of E (set of events) to be used as index */
enum events {
preempt_disable = 0,
preempt_enable,
sched_waking,
event_max
};
struct automaton {
char *state_names[state_max]; // X: the set of states
char *event_names[event_max]; // E: the finite set of events
unsigned char function[state_max][event_max]; // f: transition function
unsigned char initial_state; // x_0: the initial state
bool final_states[state_max]; // X_m: the set of marked states
};
struct automaton aut = {
.state_names = {
"preemptive",
"non_preemptive"
},
.event_names = {
"preempt_disable",
"preempt_enable",
"sched_waking"
},
.function = {
{ non_preemptive, INVALID_STATE, INVALID_STATE },
{ INVALID_STATE, preemptive, non_preemptive },
},
.initial_state = preemptive,
.final_states = { 1, 0 },
};
转换函数表示为状态（行）和事件（列）的矩阵，因此函数 f : X x E -> X 可以在 O(1) 中求解。例如
next_state = automaton_wip.function[curr_state][event];
Graphviz .dot 格式¶
Graphviz 开源工具可以使用 (文本) DOT 语言作为源代码生成自动机的图形表示。DOT 格式被广泛使用，可以转换为许多其他格式。
例如，这是 DOT 中的 ‘wip’ 模型
digraph state_automaton {
{node [shape = circle] "non_preemptive"};
{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
{node [shape = doublecircle] "preemptive"};
{node [shape = circle] "preemptive"};
"__init_preemptive" -> "preemptive";
"non_preemptive" [label = "non_preemptive"];
"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
"preemptive" [label = "preemptive"];
"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
{ rank = min ;
"__init_preemptive";
"preemptive";
}
}
可以使用 dot 实用程序将此 DOT 格式转换为位图或矢量图像，或者使用 graph-easy 转换为 ASCII 艺术。 例如
$ dot -Tsvg -o wip.svg wip.dot
$ graph-easy wip.dot > wip.txt
dot2c¶
dot2c 是一个实用程序，它可以解析包含自动机的 .dot 文件（如上例所示），并自动将其转换为 [3] 中提出的 C 表示形式。
例如，将前面的 ‘wip’ 模型放入名为 ‘wip.dot’ 的文件中，以下命令会将 .dot 文件转换为 ‘wip.h’ 文件中 C 表示形式（先前显示）
$ dot2c wip.dot > wip.h
‘wip.h’ 的内容是 ‘C 语言中的确定性自动机’ 部分中的代码示例。
备注¶
自动机形式允许以多种格式对离散事件系统 (DES) 进行建模，适用于不同的应用程序/用户。
例如，使用集合论的形式描述更适合于自动机运算，而图形格式更适合于人工解释；以及用于机器执行的计算机语言。
参考资料¶
许多教科书都涵盖了自动机形式。有关简要介绍，请参阅
O'Regan, Gerard. Concise guide to software engineering. Springer,
Cham, 2017.
有关详细描述，包括离散事件系统 (DES) 上的操作和应用，请参阅
Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
event systems. Boston, MA: Springer US, 2008.
有关内核中的 C 表示形式，请参阅
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods.
Springer, Cham, 2019. p. 315-332.