# 状态机
本章定义了用于描述时钟状态机的语言元素。这类状态机具有与状态图(Harel 1987)相似的建模能力,其重要特性在于每个时钟周期内对每个变量仅执行一次赋值(例如,若多个状态机并行执行并在同一时钟周期内对同一变量进行赋值,则属于错误行为;此类错误将在翻译阶段被检测出来)。此外,时钟方程和模块可在时钟周期内被激活或停用。高效实现方案仅需在当前时钟周期内评估处于激活状态的方程和模块。这一重要特性无法通过其他 Modelica 语言元素实现。
本章定义的状态机语义受模式自动机启发,基本沿用了 Lucid Synchrone 3.0(Pouzet 2006)的框架。需注意的是,飞行器安全关键控制软件常采用此类状态机进行定义。相较于 Lucid Synchrone 3.0 版本,其差异主要体现在以下特性:
- Lucid Synchrone 具有两种状态转换:强转换和弱转换。强转换会在评估状态动作前执行,而弱转换则在评估状态动作后执行。这种机制可能导致出人意料的行为——当一个状态被弱转换激活却又被真值强转换退出时,该状态的所有动作都将被跳过。
因此,本章中的状态机采用了即时(等同于强)转换与延迟转换。延迟转换是指那些条件被自动推迟、隐含了先前状态的即时转换。 - 并行状态机可通过语言元素显式同步(类似于顺序功能图中的并行分支)。这种常见操作也可在状态图或 Lucid Synchrone 状态机中定义,但只能通过转换条件间接实现。
- Modelica 模块可用作状态变量。这些模块可能包含时钟驱动或时钟离散化的连续时间方程(在后一种情况下,若对应状态处于活跃状态,方程将在上一个时钟周期与下一个时钟周期之间进行积分)。
# 过渡
任何不包含连续时间方程或连续时间算法的 Modelica 模块实例都可能成为状态机的一个状态。由转移语句耦合的一组实例构成一个状态机。状态机的所有部分必须具有相同的时钟。从一个状态出发的所有转移必须具有不同的优先级。每个状态机中有且仅有一个实例必须通过在 initialState 语句中出现来标记为初始状态。
下列特殊类型的类连接方程用于定义状态机。
| Expression | Description | Details |
|---|---|---|
transition(from, to, condition, ...) | State machine transition between states | Operator 17.1 |
initialState(state) | State machine initial state | Operator 17.2 |
过渡方程和初始状态方程仅能在方程式中使用,不可用于条件非参数表达式的 if 方程内部,也不可在 when 方程中使用。
以下列出的运算符用于查询状态机的运行状态。
| Expression | Description | Details |
|---|---|---|
activeState(state) | Predicate for active state | Operator 17.3 |
ticksInState() | Ticks since activation | Operator 17.4 |
timeInState() | Time since activation | Operator 17.5 |
Operator 17.1 transition
transition (from , to , condition ,
immediate =imm , reset =reset , synchronize =synch , priority =prio)
参数 from 和 to 是块实例,condition 是布尔参数。可选参数 immediate、reset 和同步属于布尔类型,具有参数变异性,默认值分别为 true、true、false。可选参数 priority 为整数类型,具有参数变异性,默认值为 1。
该运算符定义了从实例 "from" 到实例 "to" 的状态转换。这两个实例将转变为状态机的状态。当条件为真且 imm 参数为 true 时(称为立即转换),或当 imm 为 false 且 previous(condition) 为真时(称为延迟转换),该转换将被触发。参数 priority 定义了多个转换同时满足触发条件时的优先级,此时优先级数值最小的转换将优先触发。要求 prio≥1,且同一状态发出的所有转换必须具有不同的优先级值。若 reset 参数为 true,则靶区状态将被重新初始化——即状态机将重启至初始状态,所有状态变量恢复为起始值。当 synch 参数为 true 时,任何转换都将被禁用,直到 from 状态对应的所有状态机都达到最终状态(即没有输出转换的状态)。
Operator 17.2 initialState
initialState (state)
参数状态(Argument state)是指被定义为状态机初始状态的块实例。在状态机的第一个时钟周期,该状态将被激活。
Operator 17.3 activeState
activeState (state)
参数 state 是一个块实例。如果该实例是状态机的一个状态且在当前时钟周期处于活跃状态,则操作符返回 true;若非活跃状态,则操作符返回 false。
如果实例不是状态机的状态,则属于错误
Operator 17.4 ticksInState
ticksInState ()
返回状态机时钟的滴答次数,该数值表示当前活动状态保持其活动状态而未被中断(即未发生从此状态出发的局部或层次转移)的持续时间。若发生向当前活动状态或其外围活动状态的自身转移,则该数值重置为一。
此功能仅限于在状态机中使用。
Operator 17.5 timeInState
timeInState ()
返回当前活跃状态保持其持续活跃状态(即未发生从此状态出发的本地或层级转换)的时限(以秒为单位的实数)。若发生向当前活跃状态或其外围活跃状态的自我转换,该时限将重置为零。
此功能仅能在状态机中使用。
示例:若存在一个从状态 A1 到 A2 的即时性为 false 的转换,其条件为 ticksInState() >= 5,且 A1 在 10 毫秒时激活,时钟周期为 1 毫秒,那么 A1 将在 10 毫秒、11 毫秒、12 毫秒、13 毫秒、14 毫秒期间保持激活状态,到 15 毫秒时将不再激活:
block State end State;
State A0;
State A1; // Becomes active at 10ms
State A2;
equation
initialState(A0);
transition(A0, A1, sample(time, Clock(1, 1000)) > 0.0095);
transition(A1, A2, ticksInState() >= 5, immediate = false);
# 状态机图形
下图展示了状态机的推荐布局结构:
简易状态机的推荐布局。针对5个转移条件,其设置从左至右依次为:immediate = 真、假、真、假、真;reset = 真、真、假、假、真;同步 = 假、假、假、假、真;priority = 1、2、3、4、5。
示例:
transition(state2, state1, x < 10,
immediate = true, reset = true, synchronize = false, priority = 1)
annotation(
Line(
points = {{-40,-16},{-36,-4},{-32,8},{-40,26},{-40,32},{-46,50}},
color = {175, 175, 175},
thickness = 0.25,
smooth = Smooth.Bezier),
Text(
string = "%condition",
extent = {{4, -4}, {4, -10}},
fontSize = 10,
textStyle = {TextStyle.Bold},
textColor = {95, 95, 95},
horizontalAlignment = TextAlignment.Left),
);
表示转移条件的 Text 注释可以使用 %condition 标记来引用条件表达式。
Text 的范围(extent)的解读方式取决于 Line 的第一个点:若 immediate = false,则相对于 Line 的第一个点;若 immediate = true,则相对于 Line 的最后一个点。
除了由 Line 注释的点所定义的线条外,还会用一条垂直线来表示转移。若 immediate = false,这条垂直线更靠近第一个点;若为 true,则更靠近最后一个点。
如果条件文本与垂直线距离较远,会用一条淡化的直线连接转移文本和垂直线(见上方最右侧的转移示例)。
若 reset = true,会使用实心箭头头;否则使用空心箭头头。若 synchronize = true,会在箭头起始处使用反向的“分叉”符号(见上方最右侧的转移示例)。
priority 属性的值会在条件文本前添加前缀,若 priority > 1,前缀后会跟一个冒号。
initialState 线条有一个实心箭头头,且在初始状态的另一端有一个圆点(如上方所示)。
# 状态机语义
为了定义状态机的语义,假设所有转移的数据都存储在一个记录数组中:
record Transition
Integer from;
Integer to;
Boolean immediate = true;
Boolean reset = true;
Boolean synchronize = false;
Integer priority = 1;
end Transition;
转移按优先级编号升序排序,数组中优先级编号最小的转移排在最后;并且对于每个 from 值,优先级必须唯一。状态从 1 开始枚举编号。转移条件因随时间变化,存储在单独的数组 c[:] 中。
语义模型是一个离散时间系统,输入为 {c[:], active, reset}(其中 t 对应转移操作符的输入),输出为 {activeState, activeReset, activeResetStates[:]} ,状态为 {nextState, nextReset, nextResetStates[:]}。对于顶级状态机,active 始终为 true;对于子状态机,仅当父状态激活时,active 才为 true。对于顶级状态机,reset 仅在首次激活时为 true;对于子状态机,reset 由更高层级的状态机传递而来。
# 状态激活
状态更新从 nextState 开始,即上一时刻确定的下一状态。selectedState 会考虑是否要对状态机执行重置操作。
output Integer selectedState = if reset then 1 else previous(nextState);
整数 fired 的计算方式是,通过检查 selectedState 是否为源状态,以及对于立即转移,条件是否为真;对于延迟转移,previous(condition) 是否为真,以此确定要触发的转移的索引。max 函数会返回优先级最高的转移的索引,若没有符合条件的转移则返回 0。
Integer fired =
max(
if t[i].from == selectedState and
(if t[i].immediate then c[i] else previous(c[i]))
then i
else 0
for i in 1 : size(t, 1));
c 的起始值为 false 。这种定义方式需要记录所有转移条件的上一时刻值。以下描述一种等效语义,只需记录一个整数变量 delayed 的值即可。
整数 immediate 的计算方式是,检查 selectedState 是否为源状态且条件为真,以此确定可能触发的立即转移的索引。max 函数返回具有真条件和最高优先级的转移索引,若没有则返回 0。
Integer immediate =
max(
if t[i].immediate and t[i].from == selectedState and c[i] then i else 0
for i in 1 : size(t, 1));
类似地,整数 delayed 计算的是潜在延迟转移(即在下一个时钟滴答发生的转移)的索引。此时,源状态需等于 nextState:
Integer delayed =
max(
if not t[i].immediate and t[i].from == nextState and c[i] then i else 0
for i in 1 : size(t, 1));
要触发的转移按如下方式确定,需考虑延迟转移优先级可能高于立即转移的情况:
Integer fired = max(previous(delayed), immediate);
nextState 被设置为找到的转移的目标状态:
Integer nextState =
if active then
(if fired > 0 then t[fired].to else selectedState)
else
previous(nextState);
为了定义同步转移,每个状态机必须确定哪些是最终状态(即没有从该状态出发的转移的状态),并确定当前状态机是否处于最终状态:
Boolean finalStates[nStates] =
{min(t[j].from <> i for j in 1 : size(t, 1)) for i in 1 : nStates};
Boolean stateMachineInFinalState = finalStates[activeState];
要使同步转移生效,元状态内所有状态机的 stateMachineInFinalState 条件都必须为真。语义示例模型中给出了一个示例。
# 重置处理
一个状态可能因以下两个原因被重置:
- 整个状态机从其上下文被重置。在这种情况下,所有状态都必须被重置,且初始状态变为激活状态。
- 一个重置转移被触发。此时,其目标状态被重置,但其他状态不会。
第一种重置机制由 activeResetStates 和 nextResetStates 向量处理。
状态机重置标志被传播并单独维护到每个状态:
output Boolean activeResetStates[nStates] =
{reset or previous(nextResetStates[i]) for i in 1 : nStates};
直到一个状态最终被执行,然后其对应的重置条件被设置为 false:
Boolean nextResetStates[nStates] =
if active then
{activeState <> i and activeResetStates[i] for i in 1 : nStates}
else
previous(nextResetStates)
第二种重置机制通过 selectedReset 和 nextReset 变量实现。如果没有重置转移被触发,nextReset 会在下一个周期被设置为 false。
# 激活处理
当一个状态被挂起时,其方程不应被执行,且其变量应保持它们的值,包括时钟离散化的连续时间方程中的状态变量。
当子状态机的封闭状态不活跃时,子状态机的执行必须被挂起。这个激活标志作为布尔输入 active 提供。当该标志为 true 时,子状态机通过保护状态变量(nextState、nextReset 和 nextResetStates)的方程来维持其之前的状态。
# 语义摘要
整个语义模型如下所示:
model StateMachineSemantics "Semantics of state machines"
parameter Integer nStates;
parameter Transition t[:] "Array of transition data sorted in priority";
input Boolean c[size(t, 1)] "Transition conditions sorted in priority";
input Boolean active "true if the state machine is active";
input Boolean reset "true when the state machine should be reset";
Integer selectedState = if reset then 1 else previous(nextState);
Boolean selectedReset = reset or previous(nextReset);
// For strong (immediate) and weak (delayed) transitions
Integer immediate =
max(
if (t[i].immediate and t[i].from == selectedState and c[i]) then i else 0
for i in 1 : size(t, 1));
Integer delayed =
max(
if (not t[i].immediate and t[i].from == nextState and c[i]) then i else 0
for i in 1 : size(t, 1));
Integer fired = max(previous(delayed), immediate);
output Integer activeState =
if reset then 1 elseif fired > 0 then t[fired].to else selectedState;
output Boolean activeReset =
reset or (if fired > 0 then t[fired].reset else selectedReset);
// Update states
Integer nextState = if active then activeState else previous(nextState);
Boolean nextReset = not active and previous(nextReset);
// Delayed resetting of individual states
output Boolean activeResetStates[nStates] =
{reset or previous(nextResetStates[i]) for i in 1 : nStates};
Boolean nextResetStates[nStates] =
if active then
{activeState <> i and activeResetStates[i] for i in 1 : nStates}
else
previous(nextResetStates);
Boolean finalStates[nStates] =
{min(t[j].from <> i for j in 1 : size(t, 1)) for i in 1 : nStates};
Boolean stateMachineInFinalState = finalStates[activeState];
end StateMachineSemantics;
# 合并变量定义
当一个状态类使用外部输出声明时,其方程可以访问对应的内部声明变量。此时需要特殊规则来维护单一赋值原则,因为这类外部变量在不同互斥状态中的多重定义需要进行合并。
在每个状态中,求解外部输出变量,并且为每个这样的变量形成一个单一的定义:
v :=
if activeState(state₁) then
expr₁
elseif activeState(state₂) then
expr₂
elseif …
else
last(v)
last 是返回其输入的特殊内部语义运算符。它仅用于为排序做标记,即其参数的关联(关系)应被忽略。如果变量在初始状态中未被赋值,则必须为该变量提供一个起始值。
会形成一个新的赋值方程,该方程在嵌套状态机的更高层级中可能会被合并。
# 合并到输出的连接
Modelica 针对非状态机的因果连接语义被推广到状态机的状态,利用了同一时间仅有一个状态处于激活状态这一事实。
可以将来自状态机不同状态的输出连接在一起,也可以将其与其他因果连接器连接。这些输出被合并视为信号的单一来源,并给出以下约束方程:
u₁ = u₂ = … = y₁ = y₂ = …
其中,yᵢ 是来自状态机不同状态的输出,uᵢ 是其他因果变量。其语义定义:
v = if activeState(state₁) then
y₁
elseif activeState(state₂) then
y₂
elseif …
else
last(v);
u₁ = v
u₂ = v
…
# 案例
下图为层次状态机示例:内部整型变量 v(初始值 = 0):
示例:考虑上图中的分层状态机。该模型展示了以下特性:
- state1 是一个元状态,其中包含两个并行状态机。
- stateA 将 v 声明为外部输出(outer output)。state1 处于中间层级,将 v 声明为内部 - 外部输出(inner outer output),即,通过作为内部(inner) 来匹配更低层级的 外部 v(outer v),同时通过作为外部(outer) 来匹配更高层级的内部 v(inner v)。最顶层将 v 声明为内部(inner)并提供起始值。
- count 在 state1 中定义了一个起始值。当向 state1 进行重置转移(v >= 20)时,它会被重置。
- stateX 将局部变量 w 声明为等同于被声明为内部输入的 v。
- stateY 声明了一个局部计数器 j。它在开始时会重置,并且作为到 state1 的重置转移(v >= 20)的结果也会重置:当重置转移(v >= 20)触发时,活跃状态的变量会立即重置(即 state1 中的 count 以及 stateX 中的 i )。其他状态的变量仅在这些状态变为活跃的时刻才会重置。因此,当转移 stateX.i > 20 触发时(在 state1 再次变为活跃之后,也就是在重置转移 v >= 20 之后 ),stateY 中的 j 会被重置为 0。
- 对 state1 的两个并行状态机的退出进行同步,是通过使用 activeState 函数检查 stateX 和 stateY 是否处于活跃状态来实现的。
以下是无注释的 Modelica 代码:
block HierarchicalAndParallelStateMachine
inner Integer v(start = 0);
State1 state1;
State2 state2;
equation
initialState(state1);
transition(state1, state2,
activeState(state1.stateD) and activeState(state1.stateY),
immediate = false);
transition(state2, state1, v >= 20, immediate = false);
public
block State1
inner Integer count(start = 0);
inner outer output Integer v;
block StateA
outer output Integer v;
equation
v = previous(v) + 2;
end StateA;
StateA stateA;
block StateB
outer output Integer v;
equation
v = previous(v) - 1;
end StateB;
StateB stateB;
block StateC
outer output Integer count;
equation
count = previous(count) + 1;
end StateC;
StateC stateC;
block StateD
end StateD;
StateD stateD;
equation
initialState(stateA);
transition(stateA, stateB, v >= 6, immediate = false);
transition(stateB, stateC, v == 0, immediate = false);
transition(stateC, stateA, true, immediate = false, priority = 2);
transition(stateC, stateD, count >= 2, immediate = false);
public
block StateX
outer input Integer v;
Integer i(start = 0);
Integer w; // = v;
equation
i = previous(i) + 1;
w = v;
end StateX;
StateX stateX;
block StateY
Integer j(start = 0);
equation
j = previous(j) + 1;
end StateY;
StateY stateY;
equation
initialState(stateX);
transition(stateX, stateY, stateX.i > 20,
immediate = false, reset = false);
end State1;
block State2
outer output Integer v;
equation
v = previous(v) + 5;
end State2;
end HierarchicalAndParallelStateMachine;
下图展示了状态机的行为,变量 v 所反映的那样:
从状态 1 到状态 2 的转换本可以通过条件为 true 的同步转换来完成。语义等效模型如下所示:
block HierarchicalandParallelStateMachine
extends StateMachineSemantics(
nStates = 2,
t = {Transition(from = 1, to = 2, immediate = false, synchronize = true),
Transition(from = 2, to = 1, immediate = false)},
c = {true, v >= 20});
Boolean init(start = true) = sample(false);
block State1
Boolean active;
Boolean reset;
outer input Integer v_previous;
inner output Integer v;
inner Integer count(start = 0);
inner Integer count_previous = if reset then 0 else previous(count);
block StateMachineOf_stateA
extends StateMachineSemantics(
nStates = 4,
t = {Transition(from = 1, to = 2, immediate = false),
Transition(from = 2, to = 3, immediate = false),
Transition(from = 3, to = 1, immediate = false),
Transition(from = 3, to = 4, immediate = false)},
c = {v >= 6, v == 0, true, count >= 2});
outer input Integer v_previous;
outer output Integer v;
outer input Integer count_previous;
outer output Integer count;
equation
inFinalState = true; // no macro states
if activeState == 1 then
// equations for stateA
v = v_previous + 2;
count = count_previous;
elseif activeState == 2 then
// equations for stateB
v = v_previous - 1;
count = count_previous;
elseif activeState == 3 then
// equations for stateC
v = v_previous;
count = count_previous + 1;
else // if activeState == 4 then
// equations for stateD
v = v_previous;
count = count_previous;
end if;
end StateMachineOf_stateA;
StateMachineOf_stateA stateMachineOf_stateA(
active = active, reset = reset);
block StateMachineOf_stateX
extends StateMachineSemantics(
nStates = 2,
t = {Transition(from = 1, to = 2, immediate = false, reset = false)},
c = {i > 25});
outer input Integer v;
Integer i(start = 0);
Integer i_previous;
Integer j(start = 0);
Integer j_previous;
Integer w;
equation
inFinalState = true; // no macro states
if activeState == 1 then
// equations for stateX
i_previous =
if activeReset or activeResetStates[1] then 0 else previous(i);
j_previous = previous(j);
i = i_previous + 1;
w = v;
j = j_previous + 1;
else // if activeState == 2 then
// equations for stateY
i_previous = previous(i);
j_previous =
if activeReset or activeResetStates[2] then 0 else previous(j);
i = i_previous;
w = previous(w);
j = j_previous + 1;
end if;
end StateMachineOf_stateX;
StateMachineOf_stateX stateMachineOf_stateX(
active = active, reset = reset);
Boolean inFinalState =
stateMachineOf_stateA.stateMachineInFinalState and
stateMachineOf_stateX.stateMachineInFinalState;
end State1;
State1 state1;
Integer v(start = 0);
inner Integer v_previous = if reset then 0 else previous(v);
equation
active = true;
reset = previous(init);
if activeState == 1 then
// equations for state1
inFinalState = state1.inFinalState;
state1.active = true;
state1.reset = activeReset or activeResetStates[1];
v = state1.v;
else // if activeState == 2 then
// equations for state2
inFinalState = true; // not macro state
state1.active = false;
state1.reset = false;
v = previous(v) + 5;
end if;
end HierarchcialAndParallelStateMachine;