1、第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院图4.1 保险箱的状态转换图第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院图4.1是一个有穷状态机的状态转换图。从上面这个简单例子可以看出，一个有穷状态机包括下述5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。对于保险箱的例子，相应的有穷状态机的各部分如下。状态集J：保险箱锁定，A，B，保险箱解锁，报警。输入集K：1L，1R，2L，2R，3L，3R。第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院转换函数T：如表4.1所示。初始态S：保险箱锁定。
2、终态集F：保险箱解锁，报警。一个有穷状态机可以表示为一个5元组(J，K，T，S，F)，其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从(J-F)K到J的转换函数；?SJ，是一个初始状态；FJ，是终态集。 第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警，请画出相应状态转换图。思考题第4章 形式化说明技术上海海洋大学爱恩学院
3、上海海洋大学爱恩学院有穷状态机方法采用了一种简单的格式来描述规格说明：当前状态+事件+(谓词)下个状态这种形式的规格说明易于书写、易于验证，而且可以比较容易地把它转变成设计或程序代码。事实上，可以开发一个CASE工具把一个有穷状态机规格说明直接转变为源代码。4.2.3 评价第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院有限自动机 有限自动机（FA）是更一般化的状态转换图，它分为确定有限自动机DFA和非确定有限自动机NFA两种。 1确定有限自动机（DFA） 一个确定的有限自动机Md（记为DFA Md） 是一个五元组M d=（S, f, s0, Z），其中： (1) S是一个有限状
4、态集，它的每一个元 素称为一个状态； (2) 是一个有穷输入字母表，它的每一 个元素称为一个输入字符； 第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院 (3) f是一个从S到S的单值映射即 f (si , a)=sj且有si、sjS和a； (4) s0S，是惟一的一个初态； (5) Z S，是一个终态集。例如，对下图所给出的状态s1有： f(s1, a)=s2 f(s1, b)=s3 f(s1, c)=s4因此，f是单值映射函数。 第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院图 DFA的状态转换示意 s1s2s3s4cba第4章 形式化说明技术上海海洋大学爱恩
5、学院上海海洋大学爱恩学院DFA 又例：DFA M=（S,U,V,Q, a,b, f, S, Q）其中 f 定义为：f（S，a）=Uf（V，a）=Uf（S，b）=Vf（v，b）=Qf（U，a）=Qf（Q，a）=Qf（U，b）=Vf（Q，b）=Q第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院DFA 的状态图表示f（S，a）=Uf（V，a）=Uf（S，b）=Vf（v，b）=Qf（U，a）=Qf（Q，a）=Qf（U，b）=Vf（Q，b）=QbSUVQaaaba，bb第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院DFA 的矩阵表示f（S，a）=Uf（V，a）=Uf（S，b
6、）=Vf（v，b）=Qf（U，a）=Qf（Q，a）=Qf（U，b）=Vf（Q，b）=QabSUVUQVVUQQQQ字符状态第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院2非确定有限自动机(NFA) 一个非确定有限自动机Mn (记为NFA Mn ) 是一个五元组Mn=(S,f, s0,Z)，其中： (1) S是一个有限状态集，它的每一个元 素称为一个状态； (2) 是一个有穷输入字母表，它的每一 个元素称为一个输入字符； (3) f是一个从S到S的子集映射； (4) s0S，是惟一的一个初态； (5) Z S，是一个终态集。 第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学
7、爱恩学院 NFA和DFA的区别主要是：NFA的状态转换函数f不是单值函数，而是一个多值函数，即f(si，a)=某些状态的集合（siS），它表示不能由当前状态和当前输入字符惟一地确定下一个要转换的状态，也即允许同一个状态对同一个输入字符可以有不同的输出边。第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院图 NFA的状态转换示意 s1s2s3s4caaa第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院例如，对上图所给出的状态s1有： f(s1 , a)=s1 , s2 , s3 即f是一个从S*到S的子集映射；*表示输出边上所标记的不仅是字符，也可以是字。此外，NFA还
8、允许f(s1,)=某些状态的集合，即在NFA的状态转换图中输出边上的标记还可是 (空字)。 第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院3状态转换图与状态转换矩阵 (1)DFA和NFA都可以用状态转换图表示。假定DFA（或NFA）有m个状态、n个输入字符（或字），则这个状态转换图含有m个状态，每个状态最多有n条输出边与其它状态相连接，每一条输出边用（或*）中的一个不同的输入字符（或一个输入字）作标记，整个图含有惟一一个初态和若干个终态。 (2)DFA和NFA也可以用状态转换矩阵表示。状态转换矩阵的行表示状态，列表示输入符号，矩阵元素表示f(si , a)的值。第4章 形式化说
9、明技术上海海洋大学爱恩学院上海海洋大学爱恩学院例例 假定DFA Md=(s0 , s1 , s2 ,a , b , f , s0 ,s2) 且有： f(s0，a)= s1 f(s0，b)= s2 f(s1，a)= s1 f(s1，b)= s2 f(s2，a)= s2 f(s2，b)= s1试给出DFA Md的状态转换图与状态转换矩阵。解答 DFA Md的状态转换图和状态转换矩阵见下一 张幻灯片。第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院 字符 状态abs0s1s2s1s1s2s2s2s1s12 s2s0aabbab DFA Md状态转换矩阵DFA Md状态转换图 第4章 形式化说明技术上海海洋大学爱恩学院上海海洋大学爱恩学院表2.3 状态转换矩阵 字符 状态abs0s2s0，s1s1s2s2s1
