《第2章-有限状态机及其扩展幻灯片》由会员分享，可在线阅读，更多相关《第2章-有限状态机及其扩展幻灯片（51页珍藏版）》请在金锄头文库上搜索。
1、1,Chapter 2 有限状态机及其扩展,有限状态机 有限状态机是有限计算的基本模型，也是许多形式化规格、验证方法的基础模型。 Statecharts Statecharts是通过定义递阶状态、状态的AND或OR分解等高级特性的有限状态机的一种扩展形式。,2,（一） 有限状态机,（1） 基本概念 有限状态机（finite state machine）或有限自动机（finite automata）是有限计算的基本模型，是许多形式化规格、验证方法的基础模型。,超级商场的自动门控制器 自动门的前、后分别有两个缓冲区。自动门的前缓冲区用来检测是否有人接近。自动门的后缓冲区，使得控制器把门打开足够长的
2、时间让人走进去，并且不让门在打开的时候碰到站在它附近的人。自动门控制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合的动作指令。 自动门的动作控制应满足如下要求（规格）： 当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭合状态； 当后缓冲区有顾客出现，则自动门维持其原有状态； 当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。,（1） 基本概念,状态集合Q = closed, open；初始状态 q0 = closed； 输入集合 = front, rear, both, neither 状态转移关系集合 (closed, rear) =closed；(closed,both)=closed；(
3、closed, neither)=closed；(closed,front)=open (open, rear) = pen； (open,both) =open； (open, front) = open；(open, neither) = closed closed：闭合状态； open：打开状态；front：前缓冲区有顾客；rear：后缓冲区有顾客； both = front rear：前、后缓冲区都有顾客； neither = front rear：前、后缓冲区都无顾客,4,（1） 基本概念,模3计数器 状态集合Q = 0, 1, 2 ； 初始状态 q0 = 0； 输入集合 = inc
4、, dec 状态转移关系集合 (0,inc)=1；(0,dec)=2；(1,inc)=2；(1,dec)=0；(2,inc)=0；(2,dec)=1,inc：增加1 dec：减少1,5,（1） 基本概念,身份认证系统 （合法身份：ABA） 状态集合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 ,6,（1） 基本概念,有限状态机
5、是一个五元组 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） 基本概念,一个有限状态机包括：一个
6、有限状态集，用于描述系统中的不同状态；一个输入符号集，用于表征系统所接收的不同输入信息；一个状态转移函数，用于表述系统在接收不同输入下,从一个状态转移到另外一个状态的规则。 状态转移函数:刻画其行为的最关键部分, 一个从Q到Q的二元函数。状态转移函数通常可以用关系矩阵、状态转移表或状态转移图的形式来表示。 有限状态机可用四元组 M = (Q, , , q0)或三元组 M = (Q, , )来表示。,8,（1） 基本概念,状态转移矩阵 用行表示状态机所处的当前状态，列表示将要到达的下一个状态，行列交叉处表示输入字符。称该矩阵为转移函数的关系矩阵，或者有限状态机M 的状态转移矩阵。,模3计数器,9
7、,状态转移表 用表格的行表示状态机所处的当前状态，列表示当前的输入字符，行列交叉处表示要到达的下一个状态。称该表格为M的状态转换表。,模3计数器,10,状态转移图 用圆圈（结点）表示状态；将存在转移关系的状态用有向弧连接，并标注相应的输入字符在有向弧旁；用标有箭头的结点表示初始状态；属于终结状态集中的状态用双圈表示。,模3计数器,11,（1） 基本概念,前面讨论的有限状态机，可以看作仅接受输入符号并发生状态改变，但无任何输出的自动机器。 现实生活中的许多有限状态系统,对于不同的输入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。 将有限状态机进行推广，引出具有输出机制的自动机器模型。
8、 带输出的自动机器模型，按照输出的不同分成两类：输出与状态有关Moore机；输出与状态和输入有关Mealy机。,12,（1） 基本概念,Moore机形式定义为六元组M = (Q, , , , , q0)，其中 Q = q0,q1,qn是有限状态集合； = 1,2,m是有限输入字符集合； = a1,a2,ar是有限输出字符集合； ：Q Q是状态转移函数； ：Q 是输出函数； q0 Q是初始状态。,例：模3余数 Q = q0，q1，q2 = 0，1 (qj) = j, j = 0,1,2,在输入010100 下，输出为012212,13,（1） 基本概念,Mealy机形式定义为六元组M = (Q,
9、 , , , , q0)，其中 Q = q0,q1,qn是有限状态集合； = 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,14,（
10、1） 基本概念,身份认证系统（具有条件和变量机制的有限状态机） (最大允许错误次数为3)（err：报警状态； ctr：计数变量） Xcon/Yexec含义在于：所标注的状态转移关系在输入x且条件con成立下，转移至下一状态，并输出y且执行exec。标注中的各项x、con、y或exec可以缺省。,1,2,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,/c
11、tr:= 0,15,（1） 基本概念,身份认证系统,16,（2） 有限状态机的复合,通常，软件系统是以模块或子系统的形式出现 整个软件系统的有限状态机规格,需要对各个模块的有限状态机进行复合。 有限状态机复合的最简单方式是笛卡尔积 有限状态机的笛卡尔积复合,规格了多个有限状态机相互独立运行的行为。 软件系统之间存在交互问题，有限状态机的复合也必然涉及交互问题。,17,（2） 有限状态机的复合,有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的笛卡尔积为M = M1 M2 = (Q, , , q0)，其中， Q = Q1Q2； = (1 )(2 )；
12、 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,（2） 有限状态机的复合,模3计数器,模4计数器,模3和模4计数器的笛卡尔积复合有34=12个状态 每个状态下，两个模计数器均可相互独立地进行加数、减数或保持不变,19,（2） 有限状态机的复合,每个状态有33=9种状态转移选择，但其中一种为无任何状态转移发生，故只有8种状态转
13、移。 其笛卡尔积复合具有128=96个状态转移,模计数器的笛卡尔积复合,20,有限状态机的同步积复合,有限状态机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) 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,有限状态机的同步积
14、复合,模计数器的同步积复合,模3和模4计数器，可以进行耦合运行，阻止各自的独立运行行为。只有inc、inc和dec、dec两种共24个状态转移,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,有限状态机的异步积复合,模计数器的异
15、步积复合,模3和模4计数器，可以进行耦合运行，但在任何状态下仅有其中一个模计数器运行。 分别有inc和dec两种共48个状态转移,（3） 生产者-消费者问题,生产者消费者系统包含一个生产者和一个消费者。生产者进程产生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。 生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，并把消息从缓存器中取走。消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。如果缓存器是满的，那么生产者进程必须等待，直到消费者进程从缓存器中取出一个消息，使缓存器产生一个消息空
16、位。同样，如果缓存器是空的，那么消费者进程就必须等待，直到生产者进程产生一个消息并把所产生的消息写入缓存器中。缓存器在进行“读”动作后，缓存器大小减“1”，而在“写”动作后，缓存器大小加“1”。,25,（3） 生产者-消费者问题,三个有限状态机 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
