1、1Chapter 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状态转移关系集合状态转移关系集合(closed,rear)=closed；(closed,both)=c
4、losed；(closed,neither)=closed；(closed,front)=open；(open,rear)=open；(open,both)=open；(open,front)=open；(open,neither)=closedclosed：闭合状态；open：打开状态；front：前缓冲区有顾客；rear：后缓冲区有顾客；both=front rear：前、后缓冲区都有顾客；neither=front rear：前、后缓冲区都无顾客closed openfrontneitherboth,rear,neitherboth,rear,front前缓冲区后缓冲区4（1）基本概念基
5、本概念模模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 01dec2incincincdecdecinc：增加1dec：减少15（1）基本概念基本概念身份认证系统身份认证系统 （合法身份：（合法身份：ABAABA）状态集合状态集合Q=1,2,3,4；初始状态初始状态 q0=1；终结状态集合终结状态集合 F=4；输入集合输入集合 =A,B,C 状态转移关系集合状态转移关系集合(1,A
6、)=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)=312A3B,CB,CCBA4A终结状态accepting state6（1）基本概念基本概念有限状态机是一个五元组 M=(Q,q0,F)，其中 Q=q0,q1,qn是有限状态集合。在任一确定的时刻，有限状态机只能处于一个确定的状态qi；=1,2,m是有限输入字符集合。在任一确定的时刻，有限状态机只能接收一个确定的输入j；：Q Q是状态转移函数。如果在某一确定的时刻，有限状态机处于某一状态qiQ，并接收一个输入字符j
7、，那么下一时刻将处于一个确定的状态q=(qi，j)Q。在这里规定q=(q，)；q0 Q是初始状态，有限状态机由此状态开始接收输入；F Q是终结状态集合，有限状态机在达到终结态后不再接收输入。7（1）基本概念基本概念：字母表字符串：字母表上的字符组成的有限序列（为空串）语言：字母表上的字符串的集合当=a,b，aabb,ab,abab,bba,等都是上的语言有限状态机接受的语言：L(M)=x|(q0,x)F有限状态机可用四元组 M=(Q,q0)或三元组 M=(Q,)来表示。状态转移函数:刻画其行为的最关键部分,一个从Q到Q的二元函数。状态转移函数通常可以用关系矩阵、状态转移表或状态转移图的形式来表
8、示。8（1）基本概念基本概念o 状态转移矩阵 用行表示状态机所处的当前状态，列表示将要到达的下一个状态，行列交叉处表示输入字符。称该矩阵为转移函数的关系矩阵，或者有限状态机M的状态转移矩阵。模3计数器 0 1 20 inc dec2 inc dec1 dec inc状态转移矩阵01dec2incincincdecdec9o 状态转移表 用表格的行表示状态机所处的当前状态，列表示当前的输入字符，行列交叉处表示要到达的下一个状态。模3计数器 输入字符状态inc dec1 20 12 0 012状态转移表01dec2incincincdecdec10o 状态转移图 用圆圈（结点）表示状态；将存在转移
9、关系的状态用有向弧连接，并标注相应的输入字符在有向弧旁；用标有箭头的结点表示初始状态；属于终结状态集中的状态用双圈表示。01dec2incincincdecdec状态转移图模3计数器 11（1）基本概念基本概念p 前面讨论的有限状态机，可以看作仅接受输入符号并发生状态改变，但无任何输出的自动机器。p 现实生活中的许多有限状态系统,对于不同的输入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。p 将有限状态机进行推广，引出具有输出机制的自动机器模型。p 带输出的自动机器模型，按照输出的不同分成两类：输出与状态有关Moore机机；输出与状态和输入有关Mealy机机。12（2）Moore机
10、机Moore机形式定义为六元组M=(Q,q0)，其中 Q=q0,q1,qn是有限状态集合；=1,2,m是有限输入字符集合；=a1,a2,ar是有限输出字符集合；：Q Q是状态转移函数；：Q 是输出函数；q0 Q是初始状态。101010q0q2q1例例：二进制数的：二进制数的模模3余数余数Q=q0，q1，q2=0，1=0,1,2(qj)=j,j=0,1,2在输入010100 下，输出为012212 13（2）Mealy机机Mealy机形式定义为六元组M=(Q,q0)，其中 Q=q0,q1,qn是有限状态集合；=1,2,m是有限输入字符集合；=a1,a2,ar是有限输出字符集合；：Q Q是状态转移
11、函数；：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/n1/n0/y0/n1/nq0q2q114（2）Mealy机机身份认证系统（具有条件和变量机制的有限状态机）(最大允许错误次数为3)（err：报警状态；ctr：计数变量）Xcon/Yexec含义在于：所标注的状态转移关系在输入x且条件con成立下，转
12、移至下一状态，并输出y且执行exec。标注中的各项x、con、y或exec可以缺省。12A3B,Cctr3/ctr:=ctr+1 BA4errCctr3/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/ctr:=0 15（2）Mealy机机身份认证系统身份认证系统err12A3BA4ctr=2 ctr=2 ctr=2 ctr=2 12A3BA4ctr=3 ctr=3 ctr=3 ctr=3 12A3BA4ctr=1 ctr=1 c
13、tr=1 ctr=1 12A3BA4ctr=0 ctr=0 ctr=0 ctr=0 ctr=4 B,CB,CB,CB,CB,CB,CB,CB,CA,CCCCAAA16（3）有限状态机的复合有限状态机的复合o 通常，软件系统是以模块或子系统的形式出现o 整个软件系统的有限状态机规格,需要对各个模块的有限状态机进行复合。o 有限状态机复合的最简单方式是笛卡尔积o 有限状态机的笛卡尔积复合,规格了多个有限状态机相互独立运行的行为。o 软件系统之间存在交互问题，有限状态机的复合也必然涉及交互问题。17（3）有限状态机的复合有限状态机的复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,
14、q20)的笛卡尔积为M=M1 M2=(Q,q0)，其中，Q=Q1Q2；=(1)(2)；q0=(q10,q20)Q1Q2；(q1,q2),(a1,a2)=(q1,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）有限状态机的复合有限状态机的复合01dec2incincincdecdec模模3计数器计数器模模4计数器计数器01dec2incincdec3incincdecdecdeco 模3和模4计数器的笛卡尔积复合有34=12个状态o
15、每个状态下，两个模计数器均可相互独立地进行加数、减数或保持不变19（3）有限状态机的复合有限状态机的复合o 每个状态有33=9种状态转移选择，但其中一种为无任何状态转移发生，故只有8种状态转移。o 其笛卡尔积复合具有128=96个状态转移2,02,12,32,21,01,11,31,20,00,10,30,2dec,decinc,inc,decinc,incdec,incdec,inc,dec模计数器的笛卡尔积模计数器的笛卡尔积复合复合 20有限状态机的同步积复合有限状态机的同步积复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,q20)的同步积复合为M=M1 M2=(Q,q
16、0)，其中，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,02,12,32,21,01,11,31,20,00,10,30,2decincp模模3 3和模和模4 4计数器，可以进行耦合运行，阻止各自的独计数器，可以进行耦合运行，阻止各自的独立运行行为。立运行行为。只有只有incinc、inci
17、nc和和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)=q1，a1 无定义 其余23有限状态机的异步积复合有限状态机的异步积复合模计数器的异步积模计数器的异步积复合复合 2,02,12,32,21,01,11,31,20,00,10,30,2incdecinc
18、decp模模3 3和模和模4 4计数器，可以进行耦合运行，但在任何状态计数器，可以进行耦合运行，但在任何状态下仅有其中一个模计数器运行。下仅有其中一个模计数器运行。分别有分别有incinc和和decdec两种共两种共4848个状态转移个状态转移（4 4）生产者生产者-消费者问题消费者问题 生产者消费者系统生产者消费者系统包含一个生产者和一个消费者。生产者进程产包含一个生产者和一个消费者。生产者进程产生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P
19、1。消费者进程能读取消息，并把消息从缓存器中取走。消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。如果缓存器是满的，那么生产者进如果缓存器是满的，那么生产者进程必须等待，直到消费者进程从缓存器中取出一个消息，程必须等待，直到消费者进程从缓存器中取出一个消息，使缓存器产生一个消息空位。同样，如果缓存器是空的，使缓存器产生一个消息空位。同样，如果缓存器是空的，那么消费者进程就必须等待，直到生产者进程产生一个那么消费者进程就必须等待，直到生产者进程产生一个消息并把所产生的消息写入缓存器中。消息并把所产生的消息写入缓存器中。缓存器在进行“读”动作后，缓存器大小
20、减“1”，而在“写”动作后，缓存器大小加“1”。生产者生产者P1生产P2写C1读C2消费读20读1写写缓存器缓存器消费者消费者25（4 4）生产者生产者-消费者问题消费者问题 三个有限状态机 M1=(P1,P2,写,生产,1,P1)、M2=(C1,C2,读,消费,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
21、 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 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
22、,C1 2,P1,C2 1,P1,C2 消费消费读读0,P2,C1 消费1,P2,C1 0,P2,C2 2,P2,C1 2,P2,C2 1,P2,C2 消费消费读生产生产生产生产生产写写写生产者生产者P1生产P2写C1读C2消费读20读1写写缓存器缓存器消费者消费者27有限状态机的缺陷u 在多有限状态机系统中，系统的状态为所有状态机的状态的笛卡儿（同步、异步）积，因此系统的状态数具有状态组合复杂性问题。即使对于非常简单的情况，复合后系统的状态图的规模也会变得非常庞大，甚至无法进行；u 有限状态机模型实质上存在一个限制性假定：在系统所处的每一个状态上，在任何时刻，最多执行一个操作。因此，有限状态
23、机主要描述顺序系统，并发描述能力很弱；u 有限状态机不能描述无限状态系统，同时，缺乏描述时间特性的机制。有限状态机也不适合于描述系统的功能和结构特性。28（二）（二）Statecharts（1）StatechartsStatecharts中的状态中的状态 Statecharts是由以色列的Harel于1987年建立的传统有限状态机的一种扩展形式。Statecharts中通过引入状态的递阶（层次化）、状态的“与（AND）”分解和“或（OR）”分解等高级特性，从而具有了更强的描述能力。Statecharts中状态用圆角方框图示，状态名标注在圆角方框内的上方。SS2S22S21S1S1FFS3S2T
24、1TSUT229 状态的层次化状态的层次化 有限状态机在输入F下均可从状态S或T转移到状态U。这里可将状态S和T合并成一个新的状态，记为状态V，并将两个状态转移弧用一个弧来代替。状态的层次化通过框图的嵌套来图示。具有子状态的状态称为递阶状态，没有子状态的状态称为简单状态或者原子状态。高级状态或超状态、父状态、先辈状态、子状态、后代状态（任意深度多层次描述）SFFUT SVFUTSS2S22S21S130 或（或（OR）状态、与（）状态、与（AND）状态）状态u状态的层次化可以通过自顶向下的状态分解，或自底向上的状态合并来实现。状态的层次化可以通过自顶向下的状态分解，或自底向上的状态合并来实现。
25、u或（或（OROR）状态状态：当且仅当位于该状态就是位于其中的一个子状态，即，位于一个或状态不能同时位于该状态的两个以上的子状态。或状态表示了子状态之间的一种异或关系。状态的或状态表示，称为状态的或分解。u与（与（ANDAND）状态状态：当且仅当位于该状态就是同时位于其所有的子状态。与状态表示了子状态之间的一种与关系。状态的与状态表示，称为状态的正交分解；与状态的子状态，又称为状态的正交分量。图形表示中，用虚线将与状态的正交分量或子状态进行隔离，与状态的标识符（即，状态名）标注在和状态边框连与状态的标识符（即，状态名）标注在和状态边框连在一体的小方框内在一体的小方框内。S1FFS3S2T1TS
26、UT2SS2S22S21S131（2 2）StatechartsStatecharts中的迁移中的迁移 迁移上的条件、事件和动作迁移的输入迁移的输入称为触发触发（trigger），触发可以是事件或者（和）条件。迁移的输出迁移的输出称为动作动作（action），动作可以是产生新的事件或执行一个过程或函数等。输入是状态之间迁移发生的原因，只有当一个迁移的输入事件出现或者（和）迁移的输入中条件满足时，该迁移所联系的状态才可发生转移。动作的执行被认为是瞬时的。触发和动作以触发和动作以“事件事件 条条件件/动作动作”的形式标注在迁移弧旁。的形式标注在迁移弧旁。S1Ein(S1)/Rt=2/FS3S2T1
27、TSRT2RF/EF/R32 迁移上的条件、事件和动作迁移上的条件、事件和动作预定义的与状态、数据项、时间有关的条件、事件和动作（P36）条件：in(S)表示是否处于状态S中，如是则为真，否则为假；ac(A)表示活动A是否处于活动状态，如是则为真，否则为假；hg(A)表示活动A是否处于挂起状态，如是则为真，否则为假；事件：en(S)表示进入状态S；ex(S)表示退出状态S；ns表示正在进入当前状态；xs表示正在退出当前状态；st(A)表示活动A被启动；st表示当前活动被启动；sp(A)表示活动A被停止；tr(C)表示条件C变为真；fs(C)表示条件C变为假；rd(X)表示X被动作rd!读；wr
28、(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；事件、条件和动作可进行逻辑and,or,not等运算。如：E1 and E2表示事件E1与E2同时发生；C1 or C2表示C1和C2的或逻辑运算。迁移与状态的连接迁移与状态的连接 迁移描述了简单状态和简单状态、简单状态和递阶状态、递
29、阶状态和递阶状态之间的状态转移关系。迁移用有向弧图示，有向弧可以从一个状态的边界引出，终止于另一状态的边界，也可以穿过先辈状态的边界。当一个迁移没有指明其源状态时，则称之为缺省迁移。其所指向的状态，称为缺省状态。缺省迁移用圆点箭线弧表示。缺省迁移可以指向一个状态，也可以穿过先辈状态的边框直接指向某一子状态。当迁移指向一个与状态时当迁移指向一个与状态时，则相当于指向其所有的子状态；，则相当于指向其所有的子状态；当迁移指向当迁移指向一个或状态时一个或状态时，则相当于指向其缺省的子状态。当退出一个状态时，则相当于指向其缺省的子状态。当退出一个状态时，则相当退出其所有的子状态则相当退出其所有的子状态。
30、RFS2S22S21S1RFS2S22S21S1URFSS22S21S1TT2T1U34 复合迁移复合迁移 o为了简化图形中迁移的有向弧线，Statecharts中引入了一些辅助符号，从而得到状态之间转移关系的复合迁移。o条件连接符 也称为C-连接符，用于条件的连接。Statecharts规定始于C-连接符的条件分支可以多个，但是这些条件分支必须是异或的。S1S3S2C1ECC2S1S3S2EC1EC235 复合迁移复合迁移 -开关连接符 开关连接符，也称为S-连接符，用于事件的连接。S1S3S2E1ASE2E3S1S3S2AE1AE2AE336 复合迁移复合迁移-分叉（汇合）连接符 迁移的触
31、发和（或）动作的相同部分，可以通过分叉（汇合）连接符形成一个单一的弧线进入（离开）连接符。分叉（汇合）连接符适用于条件连接符和开关连接符所不能描述的情形。S1S3S2R/ASS1S3S2C1EFS1S3S2SETS1S3S2/AC1E37 复合迁移复合迁移 -分叉（汇合）结构 o分叉（汇合）结构是进入（离开）与状态的子状态迁移的一种描述方式。o此类结构下复合迁移所联系的状态转移，要求迁移上所有的触发同时满足，且动作也都同时执行。US1S3SS2S4AE1/A1c2/A2US1S3SS2S4Ac1/A1E2/A238 复合迁移复合迁移 -图形连接符 o图形连接符可以实现迁移的异地连接图形连接符可
32、以实现迁移的异地连接。用椭圆符号并标注相同的名称来图示。oStatecharts规定每个图形连接符出现与所连接的迁移必须具有相同方向的弧线（离开或者进入）。S1INTSS2S3AE1/A1INTRINT39 复合迁移复合迁移 -历史连接符 o历史连接符规定系统进入一个状态组中的一个最近访问历史连接符规定系统进入一个状态组中的一个最近访问历史状态历史状态,用标注H的圆圈图示。o历史连接符可以理解为一个特殊的状态。进入历史连接符就表示进入该连接符所在状态组中最近访问的那个状态，若历史状态为空，则进入历史连接符所指向的状态。S1HS2TS从状态从状态T进入状态进入状态S时，首先进入其历史时，首先进入
33、其历史状态状态H，即进入最近访问的那个状态。，即进入最近访问的那个状态。若上次访问的状态为若上次访问的状态为S2，则进入状态，则进入状态S2。如果如果H为空，则进入为空，则进入S1状态。状态。交通灯控制系统交通灯控制系统4041 电梯运动系统o 某个楼层 j 所能观察到的电梯运动有如下可能的几种情形：电梯一直向上移动；电梯一直向下移动；电梯从下面往上逐渐靠近，停止，然后继续向上运动；电梯从上面往下逐渐靠近，停止，然后继续向下运动；电梯从下面往上逐渐靠近，停止，然后反向向下运动；电梯从上面往下逐渐靠近，停止，然后反向向上运动；电梯从下面往上逐渐靠近，停止，然后在空闲状态等待；电梯从上面往下逐渐靠
34、近，停止，然后在空闲状态等待；从空闲状态起动，然后向下运动；从空闲状态起动，然后向上运动。电梯运动系统对于某楼层j的观察者，电梯可能会处于如下状态之一：等待(w:wait)：在该层等待，并且门未打开；停止-空闲(s-i:stop-idle)：停在该层，并且门打开；停止-向上(s-u:stop-up)：电梯在向上运动过程中在该楼层暂停；停止-向下(s-d:stop-down)：电梯在向下运动过程中在该楼层暂停；靠近-向上(a-u:approach-up)：电梯在向上运动过程中逐渐靠近该楼层；靠近-向下(a-d:approach-down)：电梯在向下运动过程中逐渐靠近该楼层；退出-向上(e-u:
35、exit-up)：电梯离开该楼层，继续向上运动；退出-向下(e-d:exit-down)：电梯离开该楼层，继续向下运动。e-ue-u e-de-d a-us-ue-ue-ds-da-d e-ua-d s-us-d a-us-ue-ds-d a-us-uws-i a-d s-dws-ie-u s-uwe-ds-dw 电梯运动系统电梯运动系统StatechartsStatecharts规格规格 exitexit-downexit-upstopstop-upstop-downstop-idlecallclose-doorclose-doorreduce-speedwaitapproachapproa
36、ch-upapproach-down状态s-u、s-d和s-i可以合并为一个超状态超状态stop；状态a-u和a-d合并为超状态超状态approach；状态e-u和e-d合并为超状态超状态exit。电梯经过在某楼层的暂停后，将合上门然后离开该楼层，这一过程规格为状态状态stop在触发在触发事件事件close-door下转移到状态下转移到状态exit。当存在某楼层对电梯的请求，并且此时的电梯正处于状态wait时，电梯将离开状态wait。这一过程规格为：在触发事件在触发事件call下，状态下，状态 wait转移到状态转移到状态stop.对电梯运动过程进行如下假定：电梯在向上运动过程中，在进入状态电
37、梯在向上运动过程中，在进入状态s-u之前要之前要经过状态经过状态a-u；同理，电梯在向下运动过程中，在进入状态s-d之前要经过状态a-d。这一转换过程，在实际电梯系统运行中需要对电梯进行减速，用reduce-speed来表示所相应的内部事件。楼层观测到的楼层观测到的电梯运动情况完全规格电梯运动情况完全规格 exitexit-downexit-upstopstop-upstop-downstop-idlecall-for-downclose-doorclose-doorreduce-speedwaitapproachapproach-upapproach-downclose-doorno-req
38、uestno-requestreduce-speedcall-for-upchange-directionchange-direction从超状态approach到超状态stop、或者从超状态stop到超状态exit的转换并没有在前图中明确指出。为此，需要对该规格进行细化规格进行细化，标记出与所有子状态相关的迁移。当电梯处于状态stop-idle时，如果发生某个用户对电梯进行请求，则转移到状态stop-up或stop-down；如果没有使用请求，则电梯将进入状态wait。这一过程通过迁移c a l l e d _ f r o m _ u p、called_from_down、change_di
39、rection、和no_request等来描述45 状态状态stop-upstop-up和和stop-downstop-down的细化的细化 exit-upstop-upopenclosedtimeoutclose-doorchange-directionexit-downstop-downopenclosedtimeoutclose-doorchange-direction对状态stop_up和stop-down进行细化，以描述电梯的开关门情况 46 4 4个楼层和个楼层和1 1个电梯的电梯运动系统规格个电梯的电梯运动系统规格a-u:approach-up a-d:approach-down e-u:exit-up e-d:exit-down s-u:stop-up s-d:stop-downs-i:stop-idle w:waitF1stope-uexita-dapproachF2stopa-uapproacha-de-ue-dexitF4stopexite-da-uapproachF3stopa-uapproacha-de-ue-dexitwaitwaitwaitwait
