形式化说明技术课件

n教学目标教学目标 了解形式化说明技术，了解有穷状态机的概念，了解形式化说明技术，了解有穷状态机的概念，了解了解PetriPetri网的概念。网的概念。n教学重点教学重点 形式化说明技术的积极意义。形式化说明技术的积极意义。n教学难点教学难点 有穷状态机、有穷状态机、PetriPetri网的概念。网的概念。第第4章章 形式化说明技术形式化说明技术教学目标第4章 形式化说明技术第第4章章 形式化说明技术形式化说明技术n4.1 概述概述n4.2 有穷状态机有穷状态机n4.3 Petri网网n4.4 Z语言语言第4章 形式化说明技术4.1 概述4.1 概述概述n按按照照形形式式化化的的程程度度，可可以以把把软软件件工工程程使使用用的的方方法划分成法划分成3 3类类：非形式化：非形式化 、半形式化半形式化、形式化、形式化n用用自自然然语语言言描描述述需需求求规规格格说说明明，是是典典型型的的非非形形式化方法。式化方法。n用用数数据据流流图图或或实实体体-联联系系图图建建立立模模型型，是是典典型型的的半形式化方法。半形式化方法。n所所谓谓形形式式化化方方法法，是是描描述述系系统统性性质质的的基基于于数数学学的的技技术术，也也就就是是说说，如如果果一一种种方方法法有有坚坚实实的的数数学基础，那么它就是形式化的。学基础，那么它就是形式化的。4.1 概述按照形式化的程度，可以把软件工程使用的方法划分n用用自自然然语语言言书书写写的的系系统统规规格格说说明明书书，可可能能存存在在矛矛盾盾、二二义义性性、含含糊糊性性、不不完完整整性性及及抽抽象象层层次次混混乱乱等问题。等问题。n所谓矛盾是指一组相互冲突的陈述。所谓矛盾是指一组相互冲突的陈述。n二义性是指读者可以用不同方式理解的陈述。二义性是指读者可以用不同方式理解的陈述。4.1.1 非形式化方法的缺点非形式化方法的缺点用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性n为为了了克克服服非非形形式式化化方方法法的的缺缺点点，人人们们把把数数学学引引入入软件开发过程，创造了基于数学的形式化方法。软件开发过程，创造了基于数学的形式化方法。n在在开开发发大大型型软软件件系系统统的的过过程程中中应应用用数数学学，能能够够带带来下述的几个优点：来下述的几个优点：n能能够够简简洁洁准准确确地地描描述述物物理理现现象象、对对象象或或动动作作的的结结果，因此是理想的建模工具。果，因此是理想的建模工具。n数数学学特特别别适适合合于于表表示示状状态态，也也就就是是表表示示“做做什什么么”，数学比自然语言更适于描述详细的需求。，数学比自然语言更适于描述详细的需求。4.1.2 形式化方法的优点形式化方法的优点为了克服非形式化方法的缺点，人们把数学引入软件开发过程，创造n在在软软件件开开发发过过程程中中使使用用数数学学的的另另一一个个优优点点是是，可可以在不同的软件工程活动之间平滑地过渡。以在不同的软件工程活动之间平滑地过渡。n不不仅仅功功能能规规格格说说明明，而而且且系系统统设设计计也也可可以以用用数数学学表表达达，当当然然，程程序序代代码码也也是是一一种种数数学学符符号号(虽虽然然是一种相当繁琐、冗长的数学符号是一种相当繁琐、冗长的数学符号)。n数数学学作作为为软软件件开开发发工工具具的的最最后后一一个个优优点点是是，它它提提供供了了高高层层确确认认的的手手段段。可可以以使使用用数数学学方方法法证证明明，设设计计符符合合规规格格说说明明，程程序序代代码码正正确确地地实实现现了了设设计计结果结果。4.1.2 形式化方法的优点形式化方法的优点在软件开发过程中使用数学的另一个优点是，可以在不同的软件工程n是否广泛应用？是否广泛应用？n由由于于软软件件系系统统的的复复杂杂性性，用用少少数数几几个个数数学学公公式式来来描述它，是根本不可能的。描述它，是根本不可能的。n另另外外，由由于于沟沟通通不不够够的的问问题题、开开发发者者的的随随意意性性问问题题，要要设设想想出出使使用用一一个个大大型型复复杂杂系系统统的的每每一一个个可可能的情景，通常是做不到的。能的情景，通常是做不到的。4.1.2 形式化方法的优点形式化方法的优点是否广泛应用？4.1.2 形式化方法的优点n对对形形式式化化方方法法应应该该“一一分分为为二二”，既既不不要要过过分分夸夸大它的优点也不要一概排斥。大它的优点也不要一概排斥。n下面给出应用形式化方法的几条准则：下面给出应用形式化方法的几条准则：(1)(1)应该选用适当的表示方法应该选用适当的表示方法 通通常常，一一种种规规格格说说明明技技术术只只能能用用自自然然的的方方式式说说明明某某一一类类概概念念，如如果果用用这这种种技技术术描描述述其其不不适适于于描描述述的的概概念念，则则不不仅仅工工作作量量大大而而且且描描述述方方式式也也很很复复杂杂。因因此此，应应该该仔仔细细选选择择一一种种适适用用于于当当前前项项目目的的形形式式化说明技术。化说明技术。4.1.3 应用形式化方法的准则应用形式化方法的准则对形式化方法应该“一分为二”，既不要过分夸大它的优点也不要一(2)应该形式化，但不要过分形式化应该形式化，但不要过分形式化目前的形式化技术还不适于描述系统的每个方面。目前的形式化技术还不适于描述系统的每个方面。带使用之，有助于防止含糊和误解。带使用之，有助于防止含糊和误解。(3)应该估算成本应该估算成本为了使用形式化方法，通常需要事先进行大量的为了使用形式化方法，通常需要事先进行大量的培训。最好预先估算所需的成本并编入预算。培训。最好预先估算所需的成本并编入预算。(4)应该有形式化方法顾问随时提供咨询应该有形式化方法顾问随时提供咨询绝大多数软件工程师对形式化方法中使用的数学绝大多数软件工程师对形式化方法中使用的数学和逻辑并不很熟悉，而且没受过使用形式化方法的和逻辑并不很熟悉，而且没受过使用形式化方法的专业训练，因此，需要专家指导和培训。专业训练，因此，需要专家指导和培训。4.1.3 应用形式化方法的准则应用形式化方法的准则(2)应该形式化，但不要过分形式化4.1.3 应用形式(5)不应该放弃传统的开发方法不应该放弃传统的开发方法把形式化方法和结构化方法或面向对象方法集成把形式化方法和结构化方法或面向对象方法集成起来是可能的，而且由于取长补短往往能获得很好起来是可能的，而且由于取长补短往往能获得很好的效果。的效果。(6)应该建立详尽的文档应该建立详尽的文档建议使用自然语言注释形式化的规格说明书，以建议使用自然语言注释形式化的规格说明书，以帮助用户和维护人员理解系统。帮助用户和维护人员理解系统。4.1.3 应用形式化方法的准则应用形式化方法的准则(5)不应该放弃传统的开发方法4.1.3 应用形式化方法(7)不应该放弃质量标准不应该放弃质量标准(8)不应该盲目依赖形式化方法不应该盲目依赖形式化方法(9)应该测试、测试再测试应该测试、测试再测试(10)应该重用应该重用即使采用了形式化方法，软件重用仍然是降低软即使采用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的惟一合理的方法。而且用件成本和提高软件质量的惟一合理的方法。而且用形式化方法说明的软件构件具有清晰定义的功能和形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们有更好的可重用性。接口，使得它们有更好的可重用性。4.1.3 应用形式化方法的准则应用形式化方法的准则 不应该放弃质量标准4.1.3 应用形式化方法的准则第第4章章 形式化说明技术形式化说明技术n4.1 概述概述n4.2 有穷状态机有穷状态机n4.3 Petri网网n4.4 Z语言语言第4章 形式化说明技术4.1 概述4.2 有穷状态机有穷状态机4.2.1 概念 有穷状态机可以准确描述一个系统，是表达规有穷状态机可以准确描述一个系统，是表达规格说明的一种形式化方法格说明的一种形式化方法。例子：例子：一一个个保保险险箱箱上上装装了了一一个个复复合合锁锁，锁锁有有三三个个位位置置，分分别别标标记记为为 1 1、2 2、3 3，转转盘盘可可向向左左(L L)或或向向右右(R R)转转动动。这这样样，在在任任意意时时刻刻转转盘盘都都有有 6 6种种可可能能的的运运动动，即即1 1L L、1 1 R R、2 2L L、2 2 R R、3 3L L和和3 3 R R。保保险险箱箱的的组组合合密密码码是是1 1L L、3 3R R、2 2L L，转转盘盘的的任任何何其其他他运运动动都都将将引引起起报报警警。如如 图图 描描 绘绘 了了 保保 险险 箱箱 的的 状状 态态 转转 换换 情情 况况。4.2 有穷状态机4.2.1 概念形式化说明技术课件4.2.1 概念概念 状状态态转转换换并并不不一一定定要要用用图图形形方方式式描描述述，表表格形式也可以表达同样的信息。格形式也可以表达同样的信息。4.2.1 概念 状态转换并不一定要用图形方式描述，表一个有穷状态机包括下述一个有穷状态机包括下述5 5个部分：个部分：4.2.1 概念概念状状态态集集J J：输入集输入集K K：转换函数转换函数T:T:初始态初始态S:S:终态集终态集F:F:保险箱锁定保险箱锁定 保险箱解锁，报警保险箱解锁，报警 保险箱锁定，保险箱锁定，A A，B B，保险箱解锁，报警，保险箱解锁，报警 1L1L，1R1R，2L2L，2R2R，3L3L，3R3R如表如表4.14.1所示所示一个有穷状态机包括下述5个部分：4.2.1 概念状态集J：一有穷状态机可表示为一个一有穷状态机可表示为一个5 5元组元组(J,K,T,S,F):(J,K,T,S,F):J J是一个有穷的非空状态集；是一个有穷的非空状态集；K K是一个有穷的非空输入集；是一个有穷的非空输入集；T T是一个从是一个从(J-F)K(J-F)K到到J J的转换函数；（非的转换函数；（非F F到到J J）SJSJ，是一个初始状态；，是一个初始状态；4.2.1 概念概念F F J J，是终态集。，是终态集。一有穷状态机可表示为一个5元组(J,K,T,S,F):4.2 有有穷穷状状态态机机的的概概念念在在计计算算机机系系统统中中应应用用得得非常广泛。例如非常广泛。例如:菜单驱动的用户界面。菜单驱动的用户界面。一一个个菜菜单单的的显显示示和和一一个个状状态态相相对对应应，键键盘盘输输入入或或用用鼠鼠标标选选择择一一个个图图标标是是使使系系统统进进入入其其他他状状态态的的一一个个事事件件。状状态态的的每每个个转转换换都都具具有有下下面面的形式：的形式：当前状态当前状态 菜单菜单+事件事件 所选择的项所选择的项下个状态下个状态。4.2.1 概念概念 有穷状态机的概念在计算机系统中应用得非常广泛。例如:菜单 对对一一个个系系统统进进行行规规格格说说明明，通通常常都都需需要要对对有有穷穷状状态机做一个很有用的扩展态机做一个很有用的扩展:即即在在前前述述的的5 5元元组组中中加加入入第第6 6个个组组件件谓谓词词集集P P，从从而而把把有有穷穷状状态态机机扩扩展展为为一一个个6 6元元组组，其其中中每每个个谓谓词词都都是是系系统统全全局局状状态态Y Y的的函函数数。转转换换函函数数T T现现在在是是一一个个从从(J-F)KP(J-F)KP到到J J的函数。现在的转换规则形式如下：的函数。现在的转换规则形式如下：当前状态当前状态 菜单菜单+事件事件 所选择的项所选择的项+谓词谓词下个状态。下个状态。4.2.1 概念概念 对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用自然语言描述的电梯系统的需求：用自然语言描述的电梯系统的需求：在在一一幢幢m m层层的的大大厦厦中中需需要要一一套套控控制制n n部部电电梯梯的的产产品品，要要求求这这n n部部电电梯梯按按照照约约束束条条件件C1C1，C2C2和和C3C3在楼层间移动。在楼层间移动。4.2.2 例子例子用自然语言描述的电梯系统的需求：4.2.2 例子C1C1：每每部部电电梯梯内内有有m m个个按按钮钮，每每个个按按钮钮代代表表一一个个楼楼层层。当当按按下下一一个个按按钮钮时时该该按按钮钮指指示示灯灯亮亮，同同时时电电梯梯驶驶向向相应的楼层，到达按钮指定的楼层时指示灯熄灭。相应的楼层，到达按钮指定的楼层时指示灯熄灭。C2C2：除除了了大大厦厦的的最最低低层层和和最最高高层层之之外外，每每层层楼楼都都有有两两个个按按钮钮分分别别请请求求电电梯梯上上行行和和下下行行。这这两两个个按按钮钮之之一一被被按按下下时时相相应应的的指指示示灯灯亮亮，当当电电梯梯到到达达此此楼楼层层时时灯熄灭，电梯向要求的方向移动。灯熄灭，电梯向要求的方向移动。C3C3：当对电梯没有请求时，它关门并停在当前楼层。：当对电梯没有请求时，它关门并停在当前楼层。4.2.2 例子例子C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个 这个问题中有两个按钮集。这个问题中有两个按钮集。n n部部电电梯梯中中的的每每一一部部都都有有m m个个按按钮钮，一一个个按按钮对应一个楼层，称它们为钮对应一个楼层，称它们为电梯按钮电梯按钮。每每层层楼楼有有两两个个按按钮钮，一一个个请请求求向向上上，另另一一个请求向下，这些按钮称为个请求向下，这些按钮称为楼层按钮楼层按钮。4.2.2 例子例子 这个问题中有两个按钮集。4.2.2 例子令令EB(e,f)EB(e,f)表表示示按按下下电电梯梯e e内内的的按按钮钮并并请请求求到到f f层层去。去。EB(e,f)EB(e,f)有有两个状态两个状态：EBON(e,f)EBON(e,f)：电梯按钮：电梯按钮(e,f)(e,f)打开打开(亮亮)EBOFF(e,f)EBOFF(e,f)：电梯按钮：电梯按钮(e,f)(e,f)关闭关闭(灭灭)EBP(e,f)EBP(e,f)：电梯按钮：电梯按钮(e,f)(e,f)被按下被按下EAF(e,f)EAF(e,f)：电梯：电梯e e到达到达f f层层4.2.2 例子例子 电梯按钮的状态转换图电梯按钮的状态转换图C1C1：每每部部电电梯梯内内有有m m个个按按钮钮，每每个个按按钮钮代代表表一一个个楼楼层层。当当按按下下一一个个按按钮钮时时该该按按钮钮指指示示灯灯亮亮，同同时时电电梯梯驶驶向向相相应应的的楼楼层层，到到达达按按钮钮指指定的楼层时指示灯熄灭。定的楼层时指示灯熄灭。令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(为为了了定定义义与与这这些些事事件件和和状状态态相相联联系系的的状状态态转转换换规则，需要一个谓词规则，需要一个谓词V(e,f)V(e,f)：V(e,f)V(e,f)：电梯：电梯e e停在停在f f层层则状态转换规则的形式化描述如下：则状态转换规则的形式化描述如下：EBOFF(e,f)+EBP(e,f)+not V(e,f)EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f)EBON(e,f)反之：反之：EBON(e,f)+EAF(e,f)EBON(e,f)+EAF(e,f)EBOFF(e,f)EBOFF(e,f)4.2.2 例子例子为了定义与这些事件和状态相联系的状态转换规则，需要一个谓词V令令FB(d,f)FB(d,f)表表示示f f层层请请求求电电梯梯向向d d方方向向运运动动的的按按钮钮，楼层按钮的也有楼层按钮的也有两个状态两个状态：FBON(d,f)FBON(d,f)：楼层按钮：楼层按钮(d,f)(d,f)打开打开(亮亮)FBOFF(d,f)FBOFF(d,f)：楼层按钮：楼层按钮(d,f)(d,f)关闭关闭(灭灭)FBP(d,f)FBP(d,f)：楼层按钮：楼层按钮(d,f)(d,f)被按下被按下EAF(1n,f)EAF(1n,f)：电梯：电梯1 1或或或或n n到达到达f f层层其中其中1n1n表示或为表示或为1 1或为或为22或为或为n n。4.2.2 例子例子C2C2：除除了了大大厦厦的的最最低低层层和和最最高高层层之之外外，每每层层楼楼都都有有两两个个按按钮钮分分别别请请求求电电梯梯上上行行和和下下行行。这这两两个个按按钮钮之之一一被被按按下下时时相相应应的的指指示示灯灯亮亮，当当电电梯梯到到达达此此楼楼层层时时灯灯熄熄灭灭，电电梯梯向向要要求求的的方向移动。方向移动。楼层按钮的状态转换图楼层按钮的状态转换图令FB(d,f)表示f层请求电梯向d方向运动的按钮，楼层按钮为为了了定定义义与与这这些些事事件件和和状状态态相相联联系系的的状状态态转转换换规规则则，同同样样也也需需要要一一个个谓谓词词，它它是是S(d,e,f)S(d,e,f)，它的定义如下它的定义如下:S(d,e,f)S(d,e,f)：电电梯梯e e停停在在f f层层并并且且移移动动方方向向由由d d确确定定为向上为向上(d=U)(d=U)或向下或向下(d=D)(d=D)或待定或待定(d=N)(d=N)。4.2.2 例子例子为了定义与这些事件和状态相联系的状态转换规则，同样也需要一个使用谓词使用谓词S(d,e,f)S(d,e,f)，形式化转换规则为：，形式化转换规则为：FBOFF(d,f)+FBP(d,f)+notS(d,1n,f)FBOFF(d,f)+FBP(d,f)+notS(d,1n,f)FBON(d,f)FBON(d,f)反之反之FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f)FBOFF(d,f)其中，其中，d=Ud=U oror D D。4.2.2 例子例子使用谓词S(d,e,f)，形式化转换规则为：4.2.2 例在在讨讨论论电电梯梯按按钮钮状状态态转转换换规规则则时时定定义义的的谓谓词词V(e,f)V(e,f)，可可以用谓词以用谓词S(d,e,f)S(d,e,f)重新定义如下：重新定义如下：V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)电梯的状态及其转换规则电梯的状态及其转换规则:一一个个电电梯梯状状态态实实质质上上包包含含许许多多子子状状态态,下下面面定定义义电电梯梯的的3 3个状态：个状态：M(d,e,f)M(d,e,f)：电梯：电梯e e正沿正沿d d方向移动，即将到达的是第方向移动，即将到达的是第f f层层S(d,e,f)S(d,e,f)：电梯：电梯e e停在停在f f层，将朝层，将朝d d方向移动方向移动(尚未关门尚未关门)W(e,f)W(e,f)：电梯：电梯e e在在f f层等待层等待(已关门已关门)4.2.2 例子例子在讨论电梯按钮状态转换规则时定义的谓词V(e,f)，可以用谓4.2.2 例子例子图4.4 电梯的状态转换图4.2.2 例子图图4.44.4中包含了下述中包含了下述3 3个可触发状态发生改变的事件。个可触发状态发生改变的事件。DC(e,f)DC(e,f)：电梯：电梯e e在楼层在楼层f f关上门关上门ST(e,f)ST(e,f)：电电梯梯e e靠靠近近f f层层时时触触发发传传感感器器，电电梯梯控控制制器器决定在当前楼层电梯是否停下决定在当前楼层电梯是否停下RLRL：电电梯梯按按钮钮或或楼楼层层按按钮钮被被按按下下进进入入打打开开状状态态，登登录需求录需求4.2.2 例子例子图4.4中包含了下述3个可触发状态发生改变的事件。4.2.2最最后后，给给出出电电梯梯的的状状态态转转换换规规则则。为为简简单单起起见见，这这里给出的规则仅发生在关门之时。里给出的规则仅发生在关门之时。S(U,e,f)+DC(e,f)S(U,e,f)+DC(e,f)M(U,e,f+1)M(U,e,f+1)S(D,e,f)+DC(e,f)S(D,e,f)+DC(e,f)M(D,e,f-1)M(D,e,f-1)S(N,e,f)+DC(e,f)S(N,e,f)+DC(e,f)W(e,f)W(e,f)4.2.2 例子例子最后，给出电梯的状态转换规则。为简单起见，这里给出的规则仅发4.2.3 评价评价有穷状态机方法描述规格说明：有穷状态机方法描述规格说明：当前状态当前状态+事件事件+谓词谓词下个状态下个状态优点：优点：规规格格说说明明易易于于书书写写、易易于于验验证证，而而且且可可以以比比较较容容易易地地把把它它转转变变成成设设计计或或程程序序代代码码。有有穷穷状状态态机机方方法比数据流图技术更精确，而且和它一样易于理解。法比数据流图技术更精确，而且和它一样易于理解。缺点：缺点：在在开开发发一一个个大大系系统统时时三三元元组组(即即状状态态、事事件件、谓谓词词)的的数数量量会会迅迅速速增增长长。此此外外，和和数数据据流流图图方方法法一一样，形式化的有穷状态机方法也没有处理定时需求。样，形式化的有穷状态机方法也没有处理定时需求。4.2.3 评价有穷状态机方法描述规格说明：第第4章章 形式化说明技术形式化说明技术n4.1 概述概述n4.2 有穷状态机有穷状态机n4.3 Petri网网n4.4 Z语言语言第4章 形式化说明技术4.1 概述4.3 Petri网网4.3.1 概念并发系统中需要解决的主要问题是定时问题：包括同步问题、竞争条件以及死锁问题。定时问题常常是因不好的设计或有错误的实现引起的，归根到底又是由不好的规格说明造成的.Petri网技术可用于确定系统中隐含的定时问题。网技术可用于确定系统中隐含的定时问题。Petri网技术在计算机领域应用较多，网技术在计算机领域应用较多，已经证明，用Petri网可以有效地描述并发活动。4.3 Petri网4.3.1 概念PetriPetri网包含网包含4 4种元素：种元素：一组位置一组位置P P一组转换一组转换T T输入函数输入函数I I输出函数输出函数O O4.3.1 概念位置位置转换转换输入输入输出输出Petri网包含4种元素：4.3.1 概念位置转换输入输出如图举例说明了如图举例说明了PetriPetri网的组成：网的组成：一组位置一组位置P为为P1，P2，P3，P4：用圆圈代表；：用圆圈代表；一一组组转转换换T为为t1，t2：图图中中用用短短直直线线表表示示转转换换；两两个个用用于于转转换换的的输输入入函函数数，用用由由位位置置指指向向转转换换的的箭头表示，它们是：箭头表示，它们是：I(t1)=P2，P4 I(t2)=P2两两个个用用于于转转换换的的输输出出函函数数，用用由由转转换换指指向向位位置置的的箭头表示，它们是：箭头表示，它们是：O(t1)=P1 O(t2)=P3，P3如图举例说明了Petri网的组成：PetriPetri网是一个四元组网是一个四元组C=(PC=(P，T T，I I，O)O)，其中：，其中：P=PP=P1 1,P,P2 2,P,Pn n 是一个有穷位置集，是一个有穷位置集，n0n0；T=(tT=(t1 1,t,tm m)是是一一个个有有穷穷转转换换集集，m0,m0,且且T T和和不相交；不相交；I:TPI:TP为为输输入入函函数数，是是由由转转换换到到位位置置无无序序单单位组的映射；位组的映射；O:TPTP为为输输出出函函数数，是是由由转转换换到到位位置置无无序序单单位组的映射。位组的映射。4.3.1 概念Petri网是一个四元组C=(P，T，I，O)，其中：4.3带标记的带标记的PetriPetri网：网：权标权标(token)(token)的分配。如图中有的分配。如图中有4 4个权标个权标上述标记可以用向量上述标记可以用向量(1(1，2 2，0 0，1)1)表示。表示。由于由于P P2 2和和P P4 4中有权标，因此中有权标，因此t t1 1启动启动(即被激发即被激发)。通通常常，当当每每个个输输入入位位置置所所拥拥有有的的权权标标数数大大于于等等于于从从该该位位置置到到转转换换的的线线数数时时，就就允允许许转转换换。当当t t1 1被被激激发发时时，P P2 2和和P P4 4上上各各有有一一个个权权标标被被移移出出，而而P P1 1上上则则增加一个权标（增加一个权标（2 2，1 1，0 0，0 0）。）。PetriPetri网网中中权权标标总总数数不不是是固固定定的的，在在这这个个例例子子中中两个权标被移出，而两个权标被移出，而P P1 1上只能增加一个权标。上只能增加一个权标。4.3.1 概念权标数权标数带标记的Petri网：4.3.1 概念权标数如如图图，P P2 2上上有有权权标标，因因此此t t2 2也也可可以以被被激激发发。当当t t2 2被被激激发发时时，P P2 2上上将将移移走走一一个个权权标标，而而P P3 3上上新新增增加加两两个个权标（权标（1 1，1 1，2 2，1 1）。）。4.3.1 概念如图，P2上有权标，因此t2也可以被激发。当t2被激发时，PPetriPetri网网具具有有非非确确定定性性，如如果果数数个个转转换换都都达达到到了了激激发发条条件件，则则其其中中任任意意一一个个都都可可以以被被激激发发。图图4.64.6所所示示PetriPetri网网的的标标记记为为(1(1，2 2，0 0，1)1)，t t1 1和和t t2 2都都可可以以被激发。被激发。4.3.1 概念假设假设t t1 1被激发了，标记为被激发了，标记为(2(2，1 1，0 0，0)0)。此时，只有。此时，只有t t2 2可以被激发。可以被激发。如果如果t t2 2也被激发了，则权标从也被激发了，则权标从P P2 2中移出，两个新权标被放在中移出，两个新权标被放在P P3 3上，上，标记为标记为(2(2，0 0，2 2，0)0)。Petri网具有非确定性，如果数个转换都达到了激发条件，则其带带有有标标记记的的PetriPetri网网成成为为一一个个五五元元组组(P(P，T T，I I，O O，M),M),其其中中标标记记M M，是是由由一一组组位位置置P P到到一一组组非非负负整整数数的映射：的映射：M M：PP0 0，1 1，2 2，对对PetriPetri网的一个重要扩充是加入禁止线网的一个重要扩充是加入禁止线禁禁止止线线是是用用一一个个小小圆圆圈圈而而不不是是用用箭箭头头标标记记的的输输入线，如图所示。入线，如图所示。4.3.1 概念禁止线禁止线带有标记的Petri网成为一个五元组(P，T，I，O，M),通通常常，当当每每个个输输入入线线上上至至少少有有一一个个权权标标，而而禁禁止止线线上上没没有有权权标标的的时时候候，相相应应的的转转换换才才是是允允许许的的。图图中中P P3 3上上有有一一个个权权标标而而P P2 2上上没没有有权权标标，因因此转换此转换t t1 1可以被激发。可以被激发。4.3.1 概念禁止线禁止线输入线输入线通常，当每个输入线上至少有一个权标，而禁止线上没有权标的时候把把Petri网应用于电梯问题。网应用于电梯问题。当当用用Petri网网表表示示电电梯梯系系统统的的规规格格说说明明时时，每每个个楼楼层层用用一一个个位位置置Ff代代表表(1fm)，在在Petri网网中中电电梯梯是是用用一一个个权权标标代代表表的的。在在位位置置Ff上上有有权权标标，表表示示在在楼层楼层f上有电梯。上有电梯。1.电梯按钮第一个约束条件描述了电梯按钮的行为。第一个约束条件描述了电梯按钮的行为。C1：每每部部电电梯梯有有m个个按按钮钮，每每层层对对应应一一个个按按钮钮。当当按按下下一一个个按按钮钮时时该该按按钮钮指指示示灯灯亮亮，指指示示电电梯梯移移往往相相应应的的楼楼层层。当当电电梯梯到到达达指指定定的的楼楼层层时时，按按钮钮将熄灭。将熄灭。4.3.2 例子把Petri网应用于电梯问题。4.3.2 例子为了了用用Petri网网表表达达电梯梯按按钮的的规格格说明明，需需要要设置置其其它它位位置置。电梯梯中中楼楼层f的的按按钮，在在Petri网网中中用位置用位置EBf表示表示(1fm)。在在EBf上上有有一一个个权标，就就表表示示电梯梯内内楼楼层f的的按按钮被按下了。被按下了。4.3.2 例子为了用Petri网表达电梯按钮的规格说明，需要设置其它位置。用用Petri网可准确地电梯按钮的行为规律。网可准确地电梯按钮的行为规律。首首先先，假假设设按按钮钮没没有有发发亮亮，显显然然在在位位置置EBf上上没没有有权权标标，从从而而在在存存在在禁禁止止线线的的情情况况下下，转转换换“EBf被按下被按下”是允许发生的。是允许发生的。假假设设现现在在按按下下按按钮钮，则则转转换换被被激激发发并并在在EBf上上放放置置了了一一个个权权标标，如如图图所所示示。以以后后不不论论再再按按下下多多少少次次按按钮钮，禁禁止止线线与与现现有有权权标标的的组组合合都都决决定定了了转转换换“EBf被被按按下下”不不能能再再被被激激发发了了，因因此此，位位置置EBf上上的权标数不会多于的权标数不会多于1。4.3.2 例子用Petri网可准确地电梯按钮的行为规律。4.3.2 例子假假设设电电梯梯由由g层层驶驶向向f层层，因因为为电电梯梯在在g层层，如如图图所所示示，位位置置Fg上上有有一一个个权权标标。由由于于每每条条输输入入线线上上各各有一个权标，转换有一个权标，转换“电梯在运行电梯在运行”被激发。被激发。EBf和和Fg上上的的权权标标被被移移走走，按按钮钮EBf被被关关闭闭，在在位位置置Ff上上出出现现一一个个新新权权标标，即即转转换换的的激激发发使使电电梯梯由由g层驶到层驶到f层。层。实实际际上上转转换换需需要要时时间间，在在标标准准Petri网网中中转转换换假假设设瞬瞬时时完完成成的的，而而在在现现实实情情况况下下就就需需要要时时间间控控制制Petri网，以使转换与非零时间相联系。网，以使转换与非零时间相联系。4.3.2 例子假设电梯由g层驶向f层，因为电梯在g层，如图所示，位置Fg上2.楼层按钮第第二二条条约约束束C2：除除了了第第一一层层与与顶顶层层之之外外，每每个个楼楼层层都都有有两两个个按按钮钮，上上行行和和下下行行。这这些些按按钮钮在在按按下下时时发发亮亮，当当电电梯梯到到达达该该层层并并将将向向指指定定方方向向移移动动时，相应的按钮才会熄灭。时，相应的按钮才会熄灭。在在Petri网网中中楼楼层层按按钮钮用用位位置置 和和 表表示示，代代表表f层层请请求求电电梯梯上上行行和和下下行行的的按按钮钮。底底层层的的按按钮钮为为 ，最最高层的按钮为高层的按钮为 。4.3.2 例子2.楼层按钮4.3.2 例子如图所示的情况为电梯由如图所示的情况为电梯由g g层驶向层驶向f f层。层。某某一一个个楼楼层层按按钮钮亮亮或或两两个个楼楼层层按按钮钮都都亮亮。如如果果两个按钮都亮了，则只有一个按钮熄灭。两个按钮都亮了，则只有一个按钮熄灭。最后，考虑第三条约束。最后，考虑第三条约束。第第三三条条约约束束C3C3：当当电电梯梯没没有有收收到到请请求求时时，它它将将停留在当前楼层并关门。停留在当前楼层并关门。这这条条约约束束很很容容易易实实现现，如如图图所所示示，当当没没有有请请求求(和和 上上无无权权标标）时时，任任何何一一个个转转换换“电电梯梯在在运运行行”都不能被激发。都不能被激发。4.3.2 例子如图所示的情况为电梯由g层驶向f层。4.3.2 例子小结及作业小结及作业小结：小结：本章为了解内容，重点是有穷状态机和本章为了解内容，重点是有穷状态机和Petri。小结及作业小结：