有限状态机及其扩展

1、1 Chapter 2 有限状态机及其扩展有限状态机及其扩展 o有限状态机有限状态机 n 有限状态机是有限计算的基本模型，也 是许多形式化规格、验证方法的基础模 型。 o Statecharts n Statecharts是通过定义递阶状态、状 态的AND或OR分解等高级特性的有限 状态机的一种扩展形式。 2 （一）（一） 有限状态机有限状态机 （1） 基本概念基本概念 有限状态机（有限状态机（finite state machine）或有限自动机）或有限自动机 （finite automata）是有限计算的基本模型，是许多形式化）是有限计算的基本模型，是许多形式化 规格、验证方法的基础模型。

2、规格、验证方法的基础模型。 超级商场的自动门控制器超级商场的自动门控制器 自动门的前、后分别有两个缓冲自动门的前、后分别有两个缓冲 区。自动门的前缓冲区用来检测是否有人接近。自动门的区。自动门的前缓冲区用来检测是否有人接近。自动门的 后缓冲区，使得控制器把门打开足够长的时间让人走进去，后缓冲区，使得控制器把门打开足够长的时间让人走进去， 并且不让门在打开的时候碰到站在它附近的人。自动门控并且不让门在打开的时候碰到站在它附近的人。自动门控 制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合 的动作指令。的动作指令。 自动门的动作控制应满足如下要求

3、（规格）：自动门的动作控制应满足如下要求（规格）： 当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭 合状态；合状态； 当后缓冲区有顾客出现，则自动门维持其原有状态；当后缓冲区有顾客出现，则自动门维持其原有状态； 当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。 前 缓 冲 区 后 缓 冲 区 （1） 基本概念基本概念 状态集合状态集合Q = closed, open；初始状态初始状态 q0 = closed； 输入集合输入集合 = front, rear, both, neither 状态转移关系

4、集合状态转移关系集合 (closed, rear) =closed；(closed,both)=closed； (closed, neither)=closed；(closed,front)=open； (open, rear) = open； (open,both) =open； (open, front) = open；(open, neither) = closed closed：闭合状态； open：打开状态；front：前缓冲区有顾客；rear：后缓冲区有顾客； both = front rear：前、后缓冲区都有顾客； neither = front rear：前、后缓冲区都无顾客

5、 closed open front neither both,rear,neitherboth,rear,front 前 缓 冲 区 后 缓 冲 区 4 （1） 基本概念基本概念 模模3计数器计数器 状态集合状态集合Q = 0, 1, 2 ； 初始状态初始状态 q0 = 0； 输入集合输入集合 = inc, dec 状态转移关系集合状态转移关系集合 (0,inc)=1；(0,dec)=2；(1,inc)=2；(1,dec)=0；(2,inc)=0；(2,dec)=1 0 1 dec 2 inc inc inc decdec inc：增加1 dec：减少1 5 （1） 基本概念基本概念 身份认

6、证系统身份认证系统 （合法身份：（合法身份：ABAABA） 状态集合状态集合Q = 1, 2, 3, 4 ； 初始状态初始状态 q0 = 1； 终结状态集合终结状态集合 F = 4； 输入集合输入集合 = A, B, C 状态转移关系集合状态转移关系集合 (1,A)=2；(1,B)=1；(1,C) =1；(2,A)=2；(2,B)=3； (2,C) =1；(3,A) =4；(3,B)=1；(3,C) =1 ABCACA AABCABA (1,AB)=3 1 2 A 3 B,C B,C C B A 4 A 终结状态 accepting state 6 （1） 基本概念基本概念 有限状态机是一个五

7、元组 M = (Q, , , q0, F)，其中 Q = q0, q1, qn是有限状态集合。在任一确定的时 刻，有限状态机只能处于一个确定的状态qi； = 1,2, m是有限输入字符集合。在任一确定 的时刻，有限状态机只能接收一个确定的输入j； ：Q Q是状态转移函数。如果在某一确定的时 刻，有限状态机处于某一状态qiQ，并接收一个输入字 符j，那么下一时刻将处于一个确定的状态q = (qi， j)Q。在这里规定q = (q，) ； q0 Q是初始状态，有限状态机由此状态开始接收输入； F Q是终结状态集合，有限状态机在达到终结态后不 再接收输入。 7 （1） 基本概念基本概念 ：字母表 字

8、符串：字母表上的字符组成的有限序列（为空串） 语言：字母表上的字符串的集合 当=a,b，aabb,ab,abab,bba,等都是上的语言 有限状态机接受的语言：L(M)=x|(q0,x) F 有限状态机可用四元组 M = (Q, , , q0)或三元组 M = (Q, , )来表示。 状态转移函数:刻画其行为的最关键部分, 一个从Q到Q 的二元函数。状态转移函数通常可以用关系矩阵、状 态转移表或状态转移图的形式来表示。 8 （1） 基本概念基本概念 o 状态转移矩阵 用行表示状态机所处的当前状 态，列表示将要到达的下一个状态，行列交叉 处表示输入字符。称该矩阵为转移函数的关 系矩阵，或者有限状

9、态机M的状态转移矩阵。 模3计数器 0 1 2 0 inc dec 2 inc dec 1 dec inc 状态转移矩阵 0 1 dec 2 inc inc inc decdec 9 o 状态转移表 用表格的行表示状态机所处的当 前状态，列表示当前的输入字符，行列交叉处 表示要到达的下一个状态。 模3计数器 输入字符 状态 inc dec 1 2 0 1 2 0 0 1 2 状态转移表 0 1 dec 2 inc inc inc decdec 10 o 状态转移图 用圆圈（结点）表示状态；将存 在转移关系的状态用有向弧连接，并标注相应 的输入字符在有向弧旁；用标有箭头的结点表 示初始状态；属于

10、终结状态集中的状态用双圈 表示。 0 1 dec 2 inc inc inc dec dec 状态转移图 模3计数器 11 （1） 基本概念基本概念 p 前面讨论的有限状态机，可以看作仅接受输入符 号并发生状态改变，但无任何输出的自动机器。 p 现实生活中的许多有限状态系统,对于不同的输入 信号，除内部状态不断改变外，还不断向系统外 部输出各种信号。 p 将有限状态机进行推广，引出具有输出机制的自 动机器模型。 p 带输出的自动机器模型，按照输出的不同分成两 类：输出与状态有关Moore机机；输出与状态和 输入有关Mealy机机。 12 （2） Moore机机 Moore机形式定义为六元组M

11、= (Q, , , , , q0)，其中 Q = q0,q1,qn是有限状态集合； = 1,2,m是有限输入字符集合； = a1,a2,ar是有限输出字符集合； ：Q Q是状态转移函数； ：Q 是输出函数； q0 Q是初始状态。 1 0 1 01 0 q0 q2 q1 例例：二进制数的：二进制数的 模模3余数余数 Q = q0，q1，q2 S= 0，1 = 0,1,2 (qj) = j, j = 0,1,2 在输入010100 下，输出为012212 13 （2） Mealy机机 Mealy机形式定义为六元组M = (Q, , , , , q0)，其中 Q = q0,q1,qn是有限状态集合；

12、 = 1,2,m是有限输入字符集合； = a1,a2,ar是有限输出字符集合； ：Q Q是状态转移函数； ：Q 是输出函数； q0 Q 是初始状态。 状态转移函数为： (q0,0) = q1, (q0,1) = q2, (q1,1) = q2, (q1,0) = q1, (q2,1) = q2, (q2,0) = q1 输出函数为： (q0,0) = n, (q0,1) = n, (q1,1) = n, (q1,0) = y, (q2,1) = y, (q2,0) = n。 在输入01100 下，输出为nnyny 1/y0/n 1/n 0/y 0/n 1/n q0 q2 q1 14 （2） M

13、ealy机机 身份认证系统（具有条件和变量机制的有限状态机） (最大允许错误次数为3)（err：报警状态； ctr：计数变量） Xcon/Yexec含义在于：所标注的状态转移关系在输入x且条件con成立下，转移至下一状态， 并输出y且执行exec。标注中的各项x、con、y或exec可以缺省。 12 A 3 B,Cctr3/ctr:=ctr+1 B A 4 err Cctr3/ctr:=ctr+1 B,Cctr=3/ctr:=ctr+1 B,Cctr=3/ctr:=ctr+1 A,Cctr=3/ctr:=ctr+1 B,Cctr3/ctr:=ctr+1 Actr3/ctr:=ctr+1 /ct

14、r:= 0 15 （2） Mealy机机 身份认证系统身份认证系统 err 1 2 A3BA 4 ctr= 2 ctr= 2 ctr= 2 ctr= 2 1 2 A3BA 4 ctr= 3 ctr= 3 ctr= 3 ctr= 3 1 2 A3BA 4 ctr= 1 ctr= 1 ctr= 1 ctr= 1 1 2 A 3BA 4 ctr= 0 ctr= 0 ctr= 0 ctr= 0 ctr= 4 B,C B,C B,C B,C B,CB,C B,C B,C A,C C C C A A A 16 （3） 有限状态机的复合有限状态机的复合 o 通常，软件系统是以模块或子系统的形式出 现 o 整

15、个软件系统的有限状态机规格,需要对各 个模块的有限状态机进行复合。 o 有限状态机复合的最简单方式是笛卡尔积 o 有限状态机的笛卡尔积复合,规格了多个有 限状态机相互独立运行的行为。 o 软件系统之间存在交互问题，有限状态机的 复合也必然涉及交互问题。 17 （3） 有限状态机的复合有限状态机的复合 有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的笛卡尔积 为M = M1 M2 = (Q, , , q0)，其中， Q = Q1Q2； = (1 )(2 )； q0 = (q10, q20) Q1Q2； (q1, q2), (a1, a2) = (q

16、1, q2) 1(q1, a1)=q1，a2 = ，a11 (q1, q2) 2(q2, a2)=q2，a1 = ，a22 (q1, q2) 1(q1, a1)=q1，2(q2, a2)=q2，a11， a22 无定义无定义 其余其余 18 （3） 有限状态机的复合有限状态机的复合 0 1 dec 2 inc inc inc decdec 模模3计数器计数器 模模4计数器计数器 0 1 dec 2 inc inc dec 3 inc inc dec dec dec o 模3和模4计数器的笛卡尔积复合有34=12 个状态 o 每个状态下，两个模计数器均可相互独立地进 行加数、减数或保持不变 19

17、 （3） 有限状态机的复合有限状态机的复合 o 每个状态有33=9种状态转移选择，但其中一种 为无任何状态转移发生，故只有8种状态转移。 o 其笛卡尔积复合具有128=96个状态转移 2,0 2,1 2,32,2 1,0 1,1 1,31,2 0,0 0,1 0,30,2 dec,dec inc, inc,dec inc,inc dec,incdec, ,inc ,dec 模计数器的笛卡尔积模计数器的笛卡尔积复合复合 20 有限状态机的同步积复合有限状态机的同步积复合 有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的同 步积复合为M = M1 M

18、2 = (Q, , , q0)，其中， Q = Q1Q2； = 1 2 ； q0 = (q10, q20) Q1Q2； (q1, q2), a) = (q1, q2) 1(q1, a)=q1， 2(q2, a)=q2，a1 2 (q1, q2) 2(q2, a)=q2，a1，a2 (q1, q2) 1(q1, a)=q1，a1，a2 无定义 其余 21 有限状态机的同步积复合有限状态机的同步积复合 模计数器的同步积模计数器的同步积复合复合 2,0 2,1 2,32,2 1,0 1,1 1,31,2 0,0 0,1 0,30,2 dec inc p模模3 3和模和模4 4计数器，可以进行耦合运行

19、，阻止各自的独计数器，可以进行耦合运行，阻止各自的独 立运行行为。立运行行为。 只有只有incinc、incinc和和decdec、decdec两种共两种共2424个状态转移个状态转移 22 有限状态机的异步积复合有限状态机的异步积复合 有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的异步积复 合为M = M1 M2 = (Q, , , q0)，其中， Q = Q1Q2； = 1 2 ； q0 = (q10, q20) Q1Q2； (q1, q2), a) = (q1, q2) 2(q2, a)=q2，a2 (q1, q2) 1(q1, a)=q

20、1，a1 无定义 其余 23 有限状态机的异步积复合有限状态机的异步积复合 模计数器的异步积模计数器的异步积复合复合 2,0 2,1 2,32,2 1,0 1,1 1,31,2 0,0 0,1 0,30,2 inc dec inc dec p模模3 3和模和模4 4计数器，可以进行耦合运行，但在任何状态计数器，可以进行耦合运行，但在任何状态 下仅有其中一个模计数器运行。下仅有其中一个模计数器运行。 分别有分别有incinc和和decdec两种共两种共4848个状态转移个状态转移 （4 4） 生产者生产者- -消费者问题消费者问题 生产者消费者系统生产者消费者系统包含一个生产者和一个消费者。生产

21、者进程产包含一个生产者和一个消费者。生产者进程产 生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。 生产者在进行“生产”动作后，状态由P1转变为P2；而 在“写”动作后，状态由P2恢复为P1。消费者进程能读 取消息，并把消息从缓存器中取走。消费者在“读”动 作后，状态由C1转变为C2；而在进行“消费”动作后， 状态由C2恢复为C1。如果缓存器是满的，那么生产者进如果缓存器是满的，那么生产者进 程必须等待，直到消费者进程从缓存器中取出一个消息，程必须等待，直到消费者进程从缓存器中取出一个消息， 使缓存器产生一个消息空位。同样，如果缓

22、存器是空的，使缓存器产生一个消息空位。同样，如果缓存器是空的， 那么消费者进程就必须等待，直到生产者进程产生一个那么消费者进程就必须等待，直到生产者进程产生一个 消息并把所产生的消息写入缓存器中。消息并把所产生的消息写入缓存器中。缓存器在进行 “读”动作后，缓存器大小减“1”，而在“写”动作后， 缓存器大小加“1”。 生产者生产者 P1 生产 P2 写 C1 读 C2 消费读 20 读 1 写 写 缓存器缓存器消费者消费者 25 （4 4） 生产者生产者- -消费者问题消费者问题 三个有限状态机 M1 = (P1, P2, 写, 生产, 1, P1) 、M2 = (C1, C2, 读, 消费,

23、 2, C1) 、 M3 = (0, 1, 2, 读, 写, 3, 0)，显然，1 3 读，2 3 写。 三个有限状态机的同步积复合M = M1 M2 M3，其中， Q = Q1Q2Q3； = 1 23； q0 = (q10, q20, q30) Q1Q2Q3； (q1, q2, q3), a) = (q1, q2, q3) 1(q1, a,)=q1，2(q2, a,)=q2，3(q3, a,)=q3，a 1 23 (q1, q2, q3) 1(q1, a,)=q1，2(q2, a,)=q2，a 1 2，a 3 (q1, q2, q3) 1(q1, a,)=q1，3(q3, a,)=q3，a

24、1 3，a 2 (q1, q2, q3) 2(q2, a,)=q2，3(q3, a,)=q3，a 2 3，a 1 (q1, q2, q3 ) 1(q1, a,)=q1，a 1，a 2，a 3 (q1, q2, q3 ) 2(q2, a,)=q2，a 2，a 1，a 3 (q1, q2, q3 ) 3(q3, a,)=q3，a 3，a 1，a 2 无定义 其余 （4 4） 生产者生产者- -消费者问题消费者问题 写 生产 读 0, P1,C1 消费 1, P1,C1 0, P1,C2 2, P1,C1 2, P1,C2 1, P1,C2 消费 消费读 读 0, P2,C1 消费 1, P2,C1

25、 0, P2,C2 2, P2,C1 2, P2,C2 1, P2,C2 消费 消费读 生产 生产生产 生产生产 写 写 写 生产者生产者 P1 生产 P2 写 C1 读 C2 消费读 20 读 1 写写 缓存器缓存器消费者消费者 27 有限状态机的缺陷 u 在多有限状态机系统中，系统的状态为所有状态机的状态的 笛卡儿（同步、异步）积，因此系统的状态数具有状态组合 复杂性问题。即使对于非常简单的情况，复合后系统的状态 图的规模也会变得非常庞大，甚至无法进行； u 有限状态机模型实质上存在一个限制性假定：在系统所处的 每一个状态上，在任何时刻，最多执行一个操作。因此，有 限状态机主要描述顺序系统

26、，并发描述能力很弱； u 有限状态机不能描述无限状态系统，同时，缺乏描述时间特 性的机制。有限状态机也不适合于描述系统的功能和结构特 性。 28 （二）（二） Statecharts （1） StatechartsStatecharts中的状态中的状态 Statecharts是由以色列的Harel于1987年建立的传统有限状态机的一 种扩展形式。Statecharts中通过引入状态的递阶（层次化）、状态 的“与（AND）”分解和“或（OR）”分解等高级特性，从而具有了 更强的描述能力。Statecharts中状态用圆角方框图示，状态名标注 在圆角方框内的上方 。 S S2 S22S21S1 S

27、1 F F S3 S2 T1 T S U T2 29 状态的层次化状态的层次化 有限状态机在输入F下均可从状态S或T转移到状态U。这里可将 状态S和T合并成一个新的状态，记为状态V，并将两个状态转移 弧用一个弧来代替。状态的层次化通过框图的嵌套来图示。 具有子状态的状态称为递阶状态，没有子状态的状态称为简单 状态或者原子状态。 高级状态或超状态、父状态、先辈状态、子状态、后代状态 （任意深度多层次描述） S F F U T S V F U T S S2 S22S21S1 30 或（或（OR）状态、与（）状态、与（AND）状态）状态 u状态的层次化可以通过自顶向下的状态分解，或自底向上的状态合并

28、来实现。状态的层次化可以通过自顶向下的状态分解，或自底向上的状态合并来实现。 u或（或（OROR）状态状态：当且仅当位于该状态就是位于其中的一个子状态，即，位于一 个或状态不能同时位于该状态的两个以上的子状态。或状态表示了子状态之间 的一种异或关系。状态的或状态表示，称为状态的或分解。 u与（与（ANDAND）状态状态：当且仅当位于该状态就是同时位于其所有的子状态。与状态表 示了子状态之间的一种与关系。状态的与状态表示，称为状态的正交分解；与 状态的子状态，又称为状态的正交分量。图形表示中，用虚线将与状态的正交 分量或子状态进行隔离，与状态的标识符（即，状态名）标注在和状态边框连与状态的标识符

29、（即，状态名）标注在和状态边框连 在一体的小方框内在一体的小方框内。 S1 F F S3 S2 T1 T S U T2 S S2 S22S21S1 31 （2 2） StatechartsStatecharts中的迁移中的迁移 o 迁移上的条件、事件和动作 迁移的输入迁移的输入称为触发触发（trigger），触发可以是事件或者（和）条件。 迁移的输出迁移的输出称为动作动作（action），动作可以是产生新的事件或执行 一个过程或函数等。 输入是状态之间迁移发生的原因，只有当一个迁移的输入事件出现 或者（和）迁移的输入中条件满足时，该迁移所联系的状态才可发 生转移。动作的执行被认为是瞬时的。触发

30、和动作以触发和动作以“事件事件 条条 件件/动作动作”的形式标注在迁移弧旁。的形式标注在迁移弧旁。 S1 Ein(S1)/R t=2/F S3 S2 T1 T S R T2 RF /E F/R 32 迁移上的条件、事件和动作迁移上的条件、事件和动作 预定义的与状态、数据项、时间有关的条件、事件和动作 （P36） 条件：in(S) 表示是否处于状态S中，如是则为真，否则为假； ac(A) 表示活动A是否处于活动状态，如是则为真，否则为假； hg(A) 表示活动A是否处于挂起状态，如是则为真，否则为假； 事件：en(S) 表示进入状态S；ex(S) 表示退出状态S； ns表示正在进入当前状态； x

31、s表示正在退出当前状态； st(A)表示活动A被启动；st表示当前活动被启动；sp(A)表示活动A被停止； tr(C)表示条件C变为真；fs(C)表示条件C变为假； rd(X)表示X被动作rd!读；wr(X)表示X被动作wr!写；ch(X)表示数据项X的值发生改变； tm(E，N)表示事件E发生后，已过了N个时间单位。 动作：tr!(C) 表示对条件C赋值真；fs!(C) 表示对条件C赋值假； st!(A)表示启动活动A；sp!(A)表示停止活动A；sd!(A)表示挂起活动A； rs!(A)表示重新开始活动A； rd!(X) 表示读数据或条件X；wr!(X) 表示写数据或条件X； 事件、条件和

32、动作可进行逻辑and ,or ,not等运算。 如：E1 and E2表示事件E1与E2同时发生；C1 or C2表示C1和C2的或逻辑运算。 迁移与状态的连接迁移与状态的连接 迁移描述了简单状态和简单状态、简单状态和递阶状态、递阶状态和递 阶状态之间的状态转移关系。 迁移用有向弧图示，有向弧可以从一个状态的边界引出，终止于另一状 态的边界，也可以穿过先辈状态的边界。 当一个迁移没有指明其源状态时，则称之为缺省迁移。其所指向的状态， 称为缺省状态。缺省迁移用圆点箭线弧表示。 缺省迁移可以指向一个状态，也可以穿过先辈状态的边框直接指向某一 子状态。 当迁移指向一个与状态时当迁移指向一个与状态时，

33、则相当于指向其所有的子状态；，则相当于指向其所有的子状态；当迁移指向当迁移指向 一个或状态时一个或状态时，则相当于指向其缺省的子状态。当退出一个状态时，则相当于指向其缺省的子状态。当退出一个状态时， 则相当退出其所有的子状态则相当退出其所有的子状态。 R F S2 S22S21 S1 R F S2 S22S21 S1 U R F S S22S21 S1 T T2T1 U 34 复合迁移复合迁移 o为了简化图形中迁移的有向弧线，Statecharts中引 入了一些辅助符号，从而得到状态之间转移关系的复 合迁移。 o条件连接符 也称为C-连接符，用于条件的连接。 Statecharts规定始于C-

34、连接符的条件分支可以多个， 但是这些条件分支必须是异或的。 S1 S3 S2 C1 E C C2 S1 S3 S2 EC1 EC2 35 复合迁移复合迁移 -开关连接符 开关连接符，也称为S-连接符，用于事件的连接。 S1 S3 S2 E1 A S E2 E3 S1 S3 S2 AE1 AE2 AE3 36 复合迁移复合迁移-分叉（汇合）连接符 迁移的触发和（或）动作的相同部分，可以通过分叉 （汇合）连接符形成一个单一的弧线进入（离开） 连接符。 分叉（汇合）连接符适用于条件连接符和开关连接符 所不能描述的情形。 S1 S3 S2 R /A S S1 S3 S2 C1 E F S1 S3 S2

35、 SET S1 S3 S2 /A C1 E 37 复合迁移复合迁移 -分叉（汇合）结构 o分叉（汇合）结构是进入（离开）与状态的子状态迁 移的一种描述方式。 o此类结构下复合迁移所联系的状态转移，要求迁移上 所有的触发同时满足，且动作也都同时执行。 U S1 S3 S S2 S4 A E1/A1 c2/A2 U S1 S3 S S2 S4 A c1/A1 E2/A2 38 复合迁移复合迁移 -图形连接符 o图形连接符可以实现迁移的异地连接图形连接符可以实现迁移的异地连接。用椭圆符号并标 注相同的名称来图示。 oStatecharts规定每个图形连接符出现与所连接的迁移必须 具有相同方向的弧线（

36、离开或者进入）。 S1INT S S2 S3 A E1/A1 INT R INT 39 复合迁移复合迁移 -历史连接符 o历史连接符规定系统进入一个状态组中的一个最近访问历史连接符规定系统进入一个状态组中的一个最近访问 历史状态历史状态,用标注H的圆圈图示。 o历史连接符可以理解为一个特殊的状态。进入历史连接 符就表示进入该连接符所在状态组中最近访问的那个状 态，若历史状态为空，则进入历史连接符所指向的状态。 S1 H S2 T S 从状态从状态T进入状态进入状态S时，首先进入其历史时，首先进入其历史 状态状态H，即进入最近访问的那个状态。，即进入最近访问的那个状态。 若上次访问的状态为若上次

37、访问的状态为S2，则进入状态，则进入状态S2。 如果如果H为空，则进入为空，则进入S1状态。状态。 交通灯控制系统交通灯控制系统 40 41 电梯运动系统 o 某个楼层 j 所能观察到的电梯运动有如下可 能的几种情形： o电梯一直向上移动； o电梯一直向下移动； o电梯从下面往上逐渐靠近，停止，然后继续向上运动； o电梯从上面往下逐渐靠近，停止，然后继续向下运动； o电梯从下面往上逐渐靠近，停止，然后反向向下运动； o电梯从上面往下逐渐靠近，停止，然后反向向上运动； o电梯从下面往上逐渐靠近，停止，然后在空闲状态等待； o电梯从上面往下逐渐靠近，停止，然后在空闲状态等待； o从空闲状态起动，然

38、后向下运动； 从空闲状态起动，然后向上运动。 电梯运动系统 对于某楼层j的观察者，电梯可能会处于如下状态之一： o等待(w:wait)：在该层等待，并且门未打开； o停止-空闲(s-i:stop-idle)：停在该层，并且门打开； o停止-向上(s-u:stop-up)：电梯在向上运动过程中在该楼层暂停； o停止-向下(s-d:stop-down)：电梯在向下运动过程中在该楼层暂停； o靠近-向上(a-u:approach-up)：电梯在向上运动过程中逐渐靠近该楼层； o靠近-向下(a-d:approach-down)：电梯在向下运动过程中逐渐靠近该楼层； o退出-向上(e-u:exit-up

39、)：电梯离开该楼层，继续向上运动； 退出-向下(e-d:exit-down)：电梯离开该楼层，继续向下运动。 e-u e-u e-d e-d a-u s-u e-u e-d s-d a-d e-ua-d s-us-d a-u s-u e-d s-d a-u s-u w s-i a-d s-d w s-i e-u s-u w e-d s-d w 电梯运动系统电梯运动系统StatechartsStatecharts规格规格 exit exit-downexit-up stop stop-upstop-down stop-idle call close-door close-door reduce-speedwait approach approach-up approach-down 状态s-u、s-d和s-i可以合并为 一个超状态超状态stop；状态a-u和a-d 合并为超状态超状态approach；状态 e-u和e-d合并为超状态超状态exit。 电梯经过在某楼层的暂停后， 将合上门然后离开该楼层，这 一过程规格为状态状态stop在触发在触发 事件事件close-door下转移到状态下转移到状态 exit。 当存在某楼层