2.3 数据有限状态机

2.2节的电梯控制系统自动机图有点复杂。本节引入其他场景，如汽车超速自动提醒系统，超速提醒依赖于汽车行驶的速度，再如自动加温空调的开和关依赖于房间的温度变化而转移。因此需要介绍一种能简单处理依赖于系统数据变化的有限状态机模型：数据有限状态机。

2.3.1 数据流图

数据流图DFG（Dataflow Graph）是最普遍的描述计算密集系统的方法。数学公式可以自然地由一个有向图表示，其中节点代表计算或函数，边代表节点执行的顺序。

计算的数据流图是基于异步和功能性原则的的。异步原则是所有计算仅当待执行的计算来源于可计算状态时才执行，功能性原则是所有计算行为均是函数式的，没有其他作用。这样就得到所有可执行的计算串行或者并行地执行。

定义2.3（数据流图 ^[12] ） 数据流图形式化地定义为4元组< N , A ， V ， v ⁰ >，其中 N ={ n ₁ , n ₂ ,…, n _M }是节点集， A ={ a ₁ , a ₂ ,…, a _L }⊆ N × N 是两节点间的边集， V ={< v ₁ , v ₂ ,…, v _L >|v _i ∈ V _i , i =1,…, L }⊆ V ₁ × V ₂ ×…× V _L 是由每个边值与特殊元素⊥组成的 L 元向量 v 的集合，其中 V _i 是边 a _i 的值与特殊符号⊥组成的集合， v _i 是 V _i 中元素，特殊符号⊥表示这个位置的边值还没有计算出来。 表示初始时刻的边向量。

数据流图的节点实现计算功能，边实现数据输入和输出。由于计算需要时间，因而边上的数据存在延迟，就形成了与时间相关的数据流。用符号 v ^t 表示 t 时刻的 L 元向量 v 。

例2.8 ^[12] 使用数据流图表示 的计算过程。

解 ：这个计算涉及7个节点：2个输入、2个平方、1个加法、1个开方和1个输出。

节点集 N ={ a , b ，平方1，平方2，加法，开方， c }

边集 A ={( a ,平方1)，( b ,平方2)，（平方1，加法），（平方2，加法），（加法，开方），（开方， c ）}，这样向量 v 是6元向量

图2-13是它的数据流图。

初始时刻是 t ₀ ，给 a 和 b 赋值3和4，此时仅有这两个值是可用的，它们是两个平方节点的输入，因而有 v ⁰ =<3,4，⊥，⊥，⊥，⊥>。在 t ₁ 时刻，两个平方节点的计算结果分别为9和16，因而有 v ¹ =<3,4,9,16，⊥，⊥>。在 t ₂ 时刻，加法节点计算结果为25，因而有 v ² =<3,4,9,16,25，⊥>。开方节点计算结果为5，因而有 v ³ =<3,4,9,16,25,5>。开方节点的值赋给 c ，所有的值都计算出来了，计算结束，输出结果为5。

2.3.2 数据有限状态机的基本概念

大多数实时系统具有控制和计算相结合的特征。这样必须把有限状态自动机和数据流图结合在一起。一种方法是把时间划分成相等的时间区间，这个时间区间称为状态，把一个或多个状态布置到数据流图的每个节点上。因为数据流图的计算是在数据流上执行的，所以我们称这个组合模型为带有数据流的有限状态机模型FSMD（a finite-state machine with dataflow），简称为数据有限状态机或数据有限自动机。

扩展有限状态机使得其能处理数据。具体做法是引入数据变量、数据输入和数据输出。

数据变量集合用 X 表示，其元素使用 x 表示，该集合定义了数据状态，该数据状态定义了每个节点上的所有变量值。因此，使用算术表达式来规范数据变量的值。Expr( X )是数据变量集合 X 上的算术表达式集合， e 或 e _i 或 e _j 表示其元素，使用巴克斯-诺尔范尔BNF（Backus-Naür form）定义 e 为：

e ::= k|x|e ^* e ( ^* ∈{+,-,×})

其中 k 是常值， x ∈ X 是变量，都是原子算术表达式，而 e ₁ + e ₂ 、 e ₁ -e ₂ 和 e ₁ × e ₂ 是复合算术表达式。使用数据算术表达式可以定义状态转移条件以及数据输出情况。

定义一个算术逻辑公式 AL （Arithmetic Logic Formula）为：

其中 e ₁ , e ₂ ∈Expr( X )是 X 上的算术表达式，△∈{=<，<，=，>，>=}是算术表达式间的关系，其中=<表示小于等于，>=表示大于等于，其余是自明的。□∈{∧，∨，→}是逻辑运算符（合取、析取、蕴涵）， 是逻辑运算符“非”。因而 e _i △ e _j 是原子算术逻辑公式， AL ₁ □ AL ₂ 与 AL 是复合算术逻辑公式。如Data=0以及( a-b )>( x + y )是原子算术逻辑公式，（counter=0）∧( x >10)是复合算术逻辑公式。注意Data≠0定义为 （Data=0），它是复合算术逻辑公式。

再如cfloor=rfloor是原子算术逻辑公式，表示电梯所在楼层cfloor等于请求的楼层rfloor，结果是电梯保持在原楼层。而cfloor≠rfloor是复合算术逻辑公式，表示电梯所在楼层cfloor不等于请求的楼层rfloor，结果是电梯上升或者下降到请求的楼层rfloor。

定义2.4（数据有限状态机） 数据有限状态机含有状态集 S ，数据集 X ，输入集 I ，输出集 O ，转移函数 f 和输出函数 h 。

转移函数 f 定义了需要的状态转移条件（Transition Condition），为此增加转移条件集 TC ，转移条件由算术逻辑公式 AL 定义，如（counter=0）∧( x >10)、cfloor≠rfloor。

把数据有限状态机的输入集 I 定义为由数据输入集 I _D 和控制输入集 I _C 组成的二元组，即 I 是 I _D 和 I _C 的笛卡儿积：

I = I _D × I _C

这样输入集的元素变成了二元组( d , c )，或直接写成 d ; c ，其中 d 是数据输入值， c 是控制输入值。

同样，把数据有限状态机的输出集 O 定义为由数据输出集 O _D 和控制输出集 O _C 的笛卡儿积：

O = O _D × O _C

集合 O _D 的元素是数据输出值的赋值语句，赋值符号为“:=”，如cfloor:=rfloor； O _C 的元素是控制输出值的赋值语句，赋值符号为“<=”，如output<=rfloor-cfloor。这样电梯控制系统的输出为：

cfloor:=rfloor；output<=rfloor-cfloor

其中cfloor:=rfloor定义了数据输出值：cfloor=rfloor，即电梯要到的楼层是rfloor；output<=rfloor-cfloor定义了控制输出值：output=rfloor-cfloor，即电梯要上升或下降rfloor-floor层（当rfloor-cfloor>0时电梯上升rfloor-floor层，当rfloor-cfloor<0时电梯下降cfloor-rfloor层，当rfloor-cfloor=0时电梯保持不动）。

数据有限状态机的转移函数 f 是状态集与输入集的笛卡儿积到状态集的一个映射，反映了状态转移既依赖于当前的状态又依赖于当前的输入值。但带有数据流的数据有限状态机除了系统的状态外，还有状态上的数据值。因此把状态集 S 和数据集 X 的笛卡儿积 S × X 作为数据有限状态机转移函数的基础，其转移实质上是把 S × X 中的元素转移为 S × X 中的元素，这种转移还要依赖于当前的数据输入值。只有当前的数据输入值符合一定条件时这种转移才能成功，因此为了成功实现转移，还需要往转移函数中增加数据输入应该满足的条件，即转移条件。依据这些分析，我们给出数据有限状态机的转移函数的形式化定义：

转移函数 f ：( S × X )× I × TC → S × X

同样地，给出Mealy型输出函数的形式化定义：

Mealy型输出函数 h ：( S × X )× I × TC → O

这里以在两个状态之间转移的数据有限状态机模型为例，说明转移函数与输出之间的关系。假设只含有2个状态( s _i , x )和( s _j , y )，以及2个转移( s _i , x )→( s _j , y )和( s _j , y )→( s _i , x )。每个转移都包含1个转移条件和1个输出，输出动作可以并行执行。表2-1和图2-14是数据有限状态机的两种表达方式。

由于输入集 I 和输出集 O 的元素都是2元组，即 I = I _D × I _C 和 O = O _D × O _C ，因此把转移函数 f 和输出函数 h 定义为2个函数的积： f = f _D × f _C , h = h _D × h _C 。其中：

f _C : S × I × TC → S , f _D : S × X × I _D → X ,

f _C 是状态控制转移函数，定义了下一个状态，这种转移依赖于当前状态 s 、当前输入 i =( d , c )和转移条件 AL ，转移条件 AL 依赖于当前数据值 d 。 f _D 定义了下一个状态的数据值，依赖于当前状态 s 、当前数据输入 x 和数据输入值 d ，换句话说，对每一个状态 s _i ∈ S ，计算每一个变量 x _j ∈ X 的值，这个值是通过表达式 e _j ∈Expr( X )获得的，即 x _j := e _j 。

把输出函数 h 定义为 h _D 和 h _C 两个函数：

h _D :（S × X） × I _D × TC → O _D ，h _C :（S × X） × I _C × TC → O _C

其中 h _D 定义了数据输出，而 h _C 定义了控制输出，相同于有限状态机的控制输出。

数据有限状态机通常使用Mealy型自动机表示，边上权值表现形式为： AL / x := e ; o <= e′ 。其中 AL 是逻辑公式，表示转移条件； x := e 和 o <= e′ 都是输出， x := e 表示 x 的值通过计算算术表达式 e 获得， o <= e′ 表示 o 的值是 e′ 的值。若使用Moore型自动机形式表示，则边上权值表现形式为 AL ，而状态机上显示输出为 x := e ; o <= e′ 。

2.3.3 数据有限状态机的建模例子

例2.9 电梯控制系统的Mealy型数据有限状态机

假设有一座 N 层高的楼，装有电梯1部，每层楼都能到达，要求建立该电梯的Mealy型数据有限状态机。

解 ：定义全局变量cfloor以存储电梯楼层的当前状态值1,2,3,…, N 和全局变量rfloor以存储请求要到达的楼层值1,2,3,…, N 。在数据有限状态机模型中，可以只使用一个状态 s ₁ ，有3个转移都是从 s ₁ 到 s ₁ 的，但它们的转移条件和输出（动作）是不同的。

形式化建模：状态集 S ={ s ₁ }，数据变量集 X ={cfloor，rfloor}，控制输入集 I _C ={}，数据输入集 I _D ={rfloor}，数据输入值集={1,2,3,…, N }，数据输出集 O _D ={cfloor}，控制输出集 O _C ={ d , u , n }，转移条件集 TC ={cfloor>rfloor，cfloor<rfloor，cfloor=rfloor}。状态转移函数 f 和输出函数 h 见表2-2。建模结果示意图如图2-15所示。

数据输出的结果是把rfloor的值赋给cfloor，记住当前电梯所要到达的楼层。控制输出的结果是：当cfloor>rfloor时，把cfloor-rfloor的值赋给控制输出 d ，电梯下降cfloor-rfloor层，到达指定的楼层rfloor；当cfloor<rfloor时，把rfloor-cfloor的值赋给控制输出 u ，电梯上升rfloor-cfloor层，到达指定的楼层rfloor；当cfloor=rfloor时，表示请求变量rfloor的值就是当前楼层，此时变量cfloor保持不变，而控制输出 n 的值为'0'，表示电梯保持不动状态。

例2.10 餐巾纸售货机的数据有限状态机 （系统功能同之前一样）

解 ：数据输入集 I _D ={ J , Y }，数据输入值集为{0,1}， J =1表示 J 已接收5角， Y =1表示 Y 已接收10角。状态集{ s ₀ , s ₅ , s ₁₀ , s ₁₅ , s ₂₀ }，其中 s ₀ 表示0角（是起始状态）， s ₅ 表示5角， s ₁₀ 表示10角， s ₁₅ 表示15角， s ₂₀ 表示20角。转移条件集 TC ={ J =1， Y =1}。控制输出集 O _C ={Open}，控制输出值集为{0,1}，数据输出集 O _D ={m}，数据输出值集为{5}（表示5角）。在此基础上建立Moore型自动机模型（如图2-16所示）和Mealy型自动机模型（如图2-17所示）。

例2.11 升级版餐巾纸售货机的数据有限状态机

此餐巾纸售货机在之前系统功能的基础上增加可以使用非现金支付以及现金找零的功能，请设计这款餐巾纸售货机的数据有限状态机。

解：使用Moore型自动机建模。

状态集 S ={ s ₀ , s ₁ }，其中 s ₀ 是开始状态，表示售货机处于待出货状态， s ₁ 表示售货处于机售货状态

数据输入变量集{ x }， x 记录支付钱数

转移条件集 TC ={ x <15, x >=15}

控制输出变量集 O _C ={Out _C }

控制输出变量值集={关闭，打开}

数据输出变量集 O _D ={Out _D , x }

数据输出变量值集={0包，1包}

其示意图如图2-18所示。

使用Mealy型自动机建模。

状态集 S ={ s }，其他与Moore型自动机的相同，见图2-19。

例2.12 超速自动提醒系统

为了安全驾驶，在车子启动后启动超速自动提醒系统并设置提醒车速值为100km/h。当车速超过这个提醒值时，汽车会自动语音提醒“超速”，直到车速低于提醒值为止。

解：形式化建模。

状态集 S ={不提醒，提醒}

数据输入变量集 X ={Carv}，其中Carv表示车速

控制输入集 I _C ={}

数据输入值集 I _D =[10,120]，此为Carv取值范围

数据输出集 O _D ={Outputspeed}

控制输出集 O _C ={Outputsound}

控制输出值集为{超速}

转移条件集 TC ={Carv>=100km/h,Carv<100km/h}

转移函数 f 和输出函数 h 见图2-20

例2.13 加热空调

加热空调是一个智能空调，能依据房间的温度自动地开和关。比如设置房间温度为20℃，空调控制系统会将房间温度控制在20℃左右：当室温大于等于22℃时空调关闭，房间自动降温；当房间温度低于18℃时，空调自动打开，对房间进行加温，这样反复进行。

解：形式化建模 。

空调状态集 S ={关，开}，初始状态为关

数据输入集 X ={ T }，其中 T 是房间温度

数据输入值集 I _D =[0,30]，此为 T 的取值范围

数据输出集 O _D ={Temp}（表示房间温度）

控制输出集 O _C ={Output}

控制输出值集={开，关}

转移条件集 TC ={ T >=22℃, T =<18℃}

状态转移函数 f 和输出函数 h 的定义见图2-21