第2章-有限状态机及其扩展

1Chapter2有限状态机及其扩展有限状态机有限状态机是有限计算的基本模型，也是许多形式化规格、验证方法的基础模型。StatechartsStatecharts是通过定义递阶状态、状态的AND或OR分解等高级特性的有限状态机的一种扩展形式。2（一）有限状态机（1）基本概念有限状态机（finitestatemachine）或有限自动机（finiteautomata）是有限计算的基本模型，是许多形式化规格、验证方法的基础模型。超级商场的自动门控制器自动门的前、后分别有两个缓冲区。自动门的前缓冲区用来检测是否有人接近。自动门的后缓冲区，使得控制器把门打开足够长的时间让人走进去，并且不让门在打开的时候碰到站在它附近的人。自动门控制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合的动作指令。自动门的动作控制应满足如下要求（规格）：①当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭合状态；②当后缓冲区有顾客出现，则自动门维持其原有状态；③当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。前缓冲区后缓冲区（1）基本概念状态集合Q={closed,open}；初始状态q0=closed；输入集合={front,rear,both,neither}状态转移关系集合(closed,rear)=closed；(closed,both)=closed；(closed,neither)=closed；(closed,front)=open(open,rear)=pen；(open,both)=open；(open,front)=open；(open,neither)=closedclosed：闭合状态；open：打开状态；front：前缓冲区有顾客；rear：后缓冲区有顾客；both=frontrear：前、后缓冲区都有顾客；neither=frontrear：前、后缓冲区都无顾客closedopenfrontneitherboth,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)=101dec2incincincdecdecinc：增加1dec：减少15（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)=1ABCACAAABCABA12A3B,CB,CCBA4A6（1）基本概念有限状态机是一个五元组M=(Q,,,q0,F)，其中①Q={q0,q1,…,qn}是有限状态集合。在任一确定的时刻，有限状态机只能处于一个确定的状态qi；②={1,2,…,m}是有限输入字符集合。在任一确定的时刻，有限状态机只能接收一个确定的输入j；③：QQ是状态转移函数。如果在某一确定的时刻，有限状态机处于某一状态qiQ，并接收一个输入字符j，那么下一时刻将处于一个确定的状态q=(qi，j)Q。在这里规定q=(q，)；④q0Q是初始状态，有限状态机由此状态开始接收输入；⑤FQ是终结状态集合，有限状态机在达到终结态后不再接收输入。7（1）基本概念一个有限状态机包括：一个有限状态集，用于描述系统中的不同状态；一个输入符号集，用于表征系统所接收的不同输入信息；一个状态转移函数，用于表述系统在接收不同输入下,从一个状态转移到另外一个状态的规则。状态转移函数:刻画其行为的最关键部分,一个从Q到Q的二元函数。状态转移函数通常可以用关系矩阵、状态转移表或状态转移图的形式来表示。有限状态机可用四元组M=(Q,,,q0)或三元组M=(Q,,)来表示。8（1）基本概念状态转移矩阵用行表示状态机所处的当前状态，列表示将要到达的下一个状态，行列交叉处表示输入字符。称该矩阵为转移函数的关系矩阵，或者有限状态机M的状态转移矩阵。模3计数器0120incdec2incdec1decinc状态转移矩阵9状态转移表用表格的行表示状态机所处的当前状态，列表示当前的输入字符，行列交叉处表示要到达的下一个状态。称该表格为M的状态转换表。模3计数器输入字符状态incdec120120012状态转移表10状态转移图用圆圈（结点）表示状态；将存在转移关系的状态用有向弧连接，并标注相应的输入字符在有向弧旁；用标有箭头的结点表示初始状态；属于终结状态集中的状态用双圈表示。01dec2incincincdecdec状态转移图模3计数器11（1）基本概念前面讨论的有限状态机，可以看作仅接受输入符号并发生状态改变，但无任何输出的自动机器。现实生活中的许多有限状态系统,对于不同的输入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。将有限状态机进行推广，引出具有输出机制的自动机器模型。带输出的自动机器模型，按照输出的不同分成两类：输出与状态有关—Moore机；输出与状态和输入有关—Mealy机。12（1）基本概念Moore机形式定义为六元组M=(Q,,,,,q0)，其中①Q={q0,q1,…,qn}是有限状态集合；②={1,2,…,m}是有限输入字符集合；③={a1,a2,…,ar}是有限输出字符集合；④：QQ是状态转移函数；⑤：Q是输出函数；⑥q0Q是初始状态。1/10/01/20/11/00/2q0q2q1例：模3余数Q={q0，q1，q2}={0，1}(qj)=j,j=0,1,2在输入010100下，输出为01221213（1）基本概念Mealy机形式定义为六元组M=(Q,,,,,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下，输出为nnyny1/y0/n1/n0/y0/n1/nq0q2q114（1）基本概念身份认证系统（具有条件和变量机制的有限状态机）(最大允许错误次数为3)（err：报警状态；ctr：计数变量）X[con]/Y[exec]含义在于：所标注的状态转移关系在输入x且条件con成立下，转移至下一状态，并输出y且执行exec。标注中的各项x、[con]、y或[exec]可以缺省。12A3B,C[ctr3]/[ctr:=ctr+1]BA4errC[ctr3]/[ctr:=ctr+1]B,C[ctr=3]/[ctr:=ctr+1]B,C[ctr=3]/[ctr:=ctr+1]A,C[ctr=3]/[ctr:=ctr+1]B,C[ctr3]/[ctr:=ctr+1]A[ctr3]/[ctr:=ctr+1]/ctr:=015（1）基本概念身份认证系统err12A3BA4ctr=2ctr=2ctr=2ctr=212A3BA4ctr=3ctr=3ctr=3ctr=312A3BA4ctr=1ctr=1ctr=1ctr=112A3BA4ctr=0ctr=0ctr=0ctr=0ctr=4B,CB,CB,CB,CB,CB,CB,CB,CA,CCCCAAA16（2）有限状态机的复合通常，软件系统是以模块或子系统的形式出现整个软件系统的有限状态机规格,需要对各个模块的有限状态机进行复合。有限状态机复合的最简单方式是笛卡尔积有限状态机的笛卡尔积复合,规格了多个有限状态机相互独立运行的行为。软件系统之间存在交互问题，有限状态机的复合也必然涉及交互问题。17（2）有限状态机的复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,q20)的笛卡尔积为M=M1M2=(Q,,,q0)，其中，Q=Q1Q2；=(1{})(2{})；q0=(q10,q20)Q1Q2；((q1,q2),(a1,a2))=(q1,q2)1(q1,a1)=q1，a2=，a11(q1,q2)2(q2,a2)=q2，a1=，a22(q1,q2)1(q1,a1)=q1，2(q2,a2)=q2，a11，a22无定义其余18（2）有限状态机的复合01dec2incincincdecdec模3计数器模4计数器01dec2incincdec3incincdecdecdec模3和模4计数器的笛卡尔积复合有3×4=12个状态每个状态下，两个模计数器均可相互独立地进行加数、减数或保持不变19（2）有限状态机的复合每个状态有3×3=9种状态转移选择，但其中一种为无任何状态转移发生，故只有8种状态转移。其笛卡尔积复合具有12×8=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,,,q0)，其中，Q=Q1Q2；=12；q0=(q10,q20)Q1Q2；((q1,q2),a)=(q1,q2)1(q1,a)=q1，2(q2,a)=q2，a12(q1,q2)2(q2,a)=q2，a1，a2(q1,q2)1(q1,a)=q1，a1，a2无定义其余21♣有限状态机的同步积复合模计数器的同步积复合2,02,12,32,21,01,11,31,20,00,10,30,2decinc模3和模4计数器，可以进行耦合运行，阻止各自的独立运行行为。只有inc、inc和dec、dec两种共24个状态转移22♣有限状态机的异步积复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,q20)的异步积复合为M=M1M2=(Q,,,q0)，其中，Q=Q1Q2；=12；q0=(q10,q20)Q1Q2；((q1,q2),a)=(q1,q2)2(q2,a)=q2，a2(q1,q2)1(q1,a)=q1，a1无定义其余23♣有限状态机的异步积复合模计数器的异步积复合2,02,12,32,21,01,11,31,20,00,10,30,2incdecincdec模3和模4计数器，可以进行耦合运行，但在任何状态下仅有其中一个模计数器运行。分别有inc和dec两种共48个状态转移（3）生产者-消费者问题生产者－消费者系统包含一个生产者和一个消费者。生产者进程产生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，并把消息从缓存器中取走。消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。如果缓存器是满的，那么生产者进程必须等待，直到消费者进程从缓存器中取出一个消息，使缓存器产生一个消息空位。同样，如果缓存器是空的，那么消费者进程就必须等待，直到生产者进程产生一个消