4-形式化說明技術(shù)課件

教學(xué)目標(biāo)

了解形式化說明技術(shù)，了解有窮狀態(tài)機(jī)的概念，了解Petri網(wǎng)的概念。教學(xué)重點(diǎn)

形式化說明技術(shù)的積極意義。教學(xué)難點(diǎn)

有窮狀態(tài)機(jī)、Petri網(wǎng)的概念。第4章形式化說明技術(shù)教學(xué)目標(biāo)第4章形式化說明技術(shù)第4章形式化說明技術(shù)4.1概述4.2有窮狀態(tài)機(jī)4.3

Petri網(wǎng)4.4

Z語言第4章形式化說明技術(shù)4.1概述4.1概述按照形式化的程度，可以把軟件工程使用的方法劃分成3類：非形式化、半形式化、形式化用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數(shù)據(jù)流圖或?qū)嶓w-聯(lián)系圖建立模型，是典型的半形式化方法。所謂形式化方法，是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，也就是說，如果一種方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。4.1概述按照形式化的程度，可以把軟件工程使用的方法劃分用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。所謂矛盾是指一組相互沖突的陳述。二義性是指讀者可以用不同方式理解的陳述。4.1.1非形式化方法的缺點(diǎn)用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性為了克服非形式化方法的缺點(diǎn)，人們把數(shù)學(xué)引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學(xué)的形式化方法。在開發(fā)大型軟件系統(tǒng)的過程中應(yīng)用數(shù)學(xué)，能夠帶來下述的幾個(gè)優(yōu)點(diǎn)：能夠簡(jiǎn)潔準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng)作的結(jié)果，因此是理想的建模工具。數(shù)學(xué)特別適合于表示狀態(tài)，也就是表示“做什么”，數(shù)學(xué)比自然語言更適于描述詳細(xì)的需求。4.1.2形式化方法的優(yōu)點(diǎn)為了克服非形式化方法的缺點(diǎn)，人們把數(shù)學(xué)引入軟件開發(fā)過程，創(chuàng)造在軟件開發(fā)過程中使用數(shù)學(xué)的另一個(gè)優(yōu)點(diǎn)是，可以在不同的軟件工程活動(dòng)之間平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計(jì)也可以用數(shù)學(xué)表達(dá)，當(dāng)然，程序代碼也是一種數(shù)學(xué)符號(hào)(雖然是一種相當(dāng)繁瑣、冗長(zhǎng)的數(shù)學(xué)符號(hào))。數(shù)學(xué)作為軟件開發(fā)工具的最后一個(gè)優(yōu)點(diǎn)是，它提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說明，程序代碼正確地實(shí)現(xiàn)了設(shè)計(jì)結(jié)果。4.1.2形式化方法的優(yōu)點(diǎn)在軟件開發(fā)過程中使用數(shù)學(xué)的另一個(gè)優(yōu)點(diǎn)是，可以在不同的軟件工程是否廣泛應(yīng)用？由于軟件系統(tǒng)的復(fù)雜性，用少數(shù)幾個(gè)數(shù)學(xué)公式來描述它，是根本不可能的。另外，由于溝通不夠的問題、開發(fā)者的隨意性問題，要設(shè)想出使用一個(gè)大型復(fù)雜系統(tǒng)的每一個(gè)可能的情景，通常是做不到的。4.1.2形式化方法的優(yōu)點(diǎn)是否廣泛應(yīng)用？4.1.2形式化方法的優(yōu)點(diǎn)對(duì)形式化方法應(yīng)該“一分為二”，既不要過分夸大它的優(yōu)點(diǎn)也不要一概排斥。下面給出應(yīng)用形式化方法的幾條準(zhǔn)則：(1)應(yīng)該選用適當(dāng)?shù)谋硎痉椒?/p>

通常，一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念，如果用這種技術(shù)描述其不適于描述的概念，則不僅工作量大而且描述方式也很復(fù)雜。因此，應(yīng)該仔細(xì)選擇一種適用于當(dāng)前項(xiàng)目的形式化說明技術(shù)。4.1.3應(yīng)用形式化方法的準(zhǔn)則對(duì)形式化方法應(yīng)該“一分為二”，既不要過分夸大它的優(yōu)點(diǎn)也不要一(2)應(yīng)該形式化，但不要過分形式化目前的形式化技術(shù)還不適于描述系統(tǒng)的每個(gè)方面。帶使用之，有助于防止含糊和誤解。(3)應(yīng)該估算成本為了使用形式化方法，通常需要事先進(jìn)行大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入預(yù)算。(4)應(yīng)該有形式化方法顧問隨時(shí)提供咨詢絕大多數(shù)軟件工程師對(duì)形式化方法中使用的數(shù)學(xué)和邏輯并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓(xùn)練，因此，需要專家指導(dǎo)和培訓(xùn)。4.1.3應(yīng)用形式化方法的準(zhǔn)則(2)應(yīng)該形式化，但不要過分形式化4.1.3應(yīng)用形式(5)不應(yīng)該放棄傳統(tǒng)的開發(fā)方法把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿模矣捎谌￠L(zhǎng)補(bǔ)短往往能獲得很好的效果。(6)應(yīng)該建立詳盡的文檔建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維護(hù)人員理解系統(tǒng)。4.1.3應(yīng)用形式化方法的準(zhǔn)則(5)不應(yīng)該放棄傳統(tǒng)的開發(fā)方法4.1.3應(yīng)用形式化方法不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)不應(yīng)該盲目依賴形式化方法

應(yīng)該測(cè)試、測(cè)試再測(cè)試應(yīng)該重用即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法。而且用形式化方法說明的軟件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用性。4.1.3應(yīng)用形式化方法的準(zhǔn)則不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)4.1.3應(yīng)用形式化方法的準(zhǔn)則第4章形式化說明技術(shù)4.1概述4.2有窮狀態(tài)機(jī)4.3

Petri網(wǎng)4.4

Z語言第4章形式化說明技術(shù)4.1概述4.2有窮狀態(tài)機(jī)4.2.1概念有窮狀態(tài)機(jī)可以準(zhǔn)確描述一個(gè)系統(tǒng)，是表達(dá)規(guī)格說明的一種形式化方法。例子：一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左(L)或向右(R)轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤都有6種可能的運(yùn)動(dòng)，即1L、1R、2L、2R、3L和3R。保險(xiǎn)箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其他運(yùn)動(dòng)都將引起報(bào)警。如圖描繪了保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換情況。4.2有窮狀態(tài)機(jī)4.2.1概念4_形式化說明技術(shù)課件4.2.1概念狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，表格形式也可以表達(dá)同樣的信息。4.2.1概念狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，表一個(gè)有窮狀態(tài)機(jī)包括下述5個(gè)部分：4.2.1概念狀態(tài)集J：輸入集K：轉(zhuǎn)換函數(shù)T:初始態(tài)S:終態(tài)集F:保險(xiǎn)箱鎖定{保險(xiǎn)箱解鎖，報(bào)警}{保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖，報(bào)警}{1L，1R，2L，2R，3L，3R}如表4.1所示一個(gè)有窮狀態(tài)機(jī)包括下述5個(gè)部分：4.2.1概念狀態(tài)集J：一有窮狀態(tài)機(jī)可表示為一個(gè)5元組(J,K,T,S,F):J是一個(gè)有窮的非空狀態(tài)集；K是一個(gè)有窮的非空輸入集；T是一個(gè)從(J-F)×K到J的轉(zhuǎn)換函數(shù)；（非F到J）S∈J，是一個(gè)初始狀態(tài)；4.2.1概念F

J，是終態(tài)集。一有窮狀態(tài)機(jī)可表示為一個(gè)5元組(J,K,T,S,F):4.2有窮狀態(tài)機(jī)的概念在計(jì)算機(jī)系統(tǒng)中應(yīng)用得非常廣泛。例如:菜單驅(qū)動(dòng)的用戶界面。一個(gè)菜單的顯示和一個(gè)狀態(tài)相對(duì)應(yīng)，鍵盤輸入或用鼠標(biāo)選擇一個(gè)圖標(biāo)是使系統(tǒng)進(jìn)入其他狀態(tài)的一個(gè)事件。狀態(tài)的每個(gè)轉(zhuǎn)換都具有下面的形式：當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]→下個(gè)狀態(tài)。4.2.1概念有窮狀態(tài)機(jī)的概念在計(jì)算機(jī)系統(tǒng)中應(yīng)用得非常廣泛。例如:菜單對(duì)一個(gè)系統(tǒng)進(jìn)行規(guī)格說明，通常都需要對(duì)有窮狀態(tài)機(jī)做一個(gè)很有用的擴(kuò)展:即在前述的5元組中加入第6個(gè)組件——謂詞集P，從而把有窮狀態(tài)機(jī)擴(kuò)展為一個(gè)6元組，其中每個(gè)謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉(zhuǎn)換函數(shù)T現(xiàn)在是一個(gè)從(J-F)×K×P到J的函數(shù)。現(xiàn)在的轉(zhuǎn)換規(guī)則形式如下：當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]+謂詞→下個(gè)狀態(tài)。4.2.1概念對(duì)一個(gè)系統(tǒng)進(jìn)行規(guī)格說明，通常都需要對(duì)有窮狀態(tài)機(jī)做一個(gè)很有用自然語言描述的電梯系統(tǒng)的需求：在一幢m層的大廈中需要一套控制n部電梯的產(chǎn)品，要求這n部電梯按照約束條件C1，C2和C3在樓層間移動(dòng)。4.2.2例子用自然語言描述的電梯系統(tǒng)的需求：4.2.2例子C1：每部電梯內(nèi)有m個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈熄滅。C2：除了大廈的最低層和最高層之外，每層樓都有兩個(gè)按鈕分別請(qǐng)求電梯上行和下行。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移動(dòng)。C3：當(dāng)對(duì)電梯沒有請(qǐng)求時(shí)，它關(guān)門并停在當(dāng)前樓層。4.2.2例子C1：每部電梯內(nèi)有m個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)這個(gè)問題中有兩個(gè)按鈕集。n部電梯中的每一部都有m個(gè)按鈕，一個(gè)按鈕對(duì)應(yīng)一個(gè)樓層，稱它們?yōu)殡娞莅粹o。每層樓有兩個(gè)按鈕，一個(gè)請(qǐng)求向上，另一個(gè)請(qǐng)求向下，這些按鈕稱為樓層按鈕。4.2.2例子這個(gè)問題中有兩個(gè)按鈕集。4.2.2例子令EB(e,f)表示按下電梯e內(nèi)的按鈕并請(qǐng)求到f層去。EB(e,f)有兩個(gè)狀態(tài)：EBON(e,f)：電梯按鈕(e,f)打開(亮)EBOFF(e,f)：電梯按鈕(e,f)關(guān)閉(滅)EBP(e,f)：電梯按鈕(e,f)被按下EAF(e,f)：電梯e到達(dá)f層4.2.2例子

電梯按鈕的狀態(tài)轉(zhuǎn)換圖C1：每部電梯內(nèi)有m個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈熄滅。令EB(e,f)表示按下電梯e內(nèi)的按鈕并請(qǐng)求到f層去。EB(為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，需要一個(gè)謂詞V(e,f)：V(e,f)：電梯e停在f層則狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：EBOFF(e,f)+EBP(e,f)+notV(e,f)

EBON(e,f)反之：EBON(e,f)+EAF(e,f)

EBOFF(e,f)4.2.2例子為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，需要一個(gè)謂詞V令FB(d,f)表示f層請(qǐng)求電梯向d方向運(yùn)動(dòng)的按鈕，樓層按鈕的也有兩個(gè)狀態(tài)：FBON(d,f)：樓層按鈕(d,f)打開(亮)FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉(滅)FBP(d,f)：樓層按鈕(d,f)被按下EAF(1…n,f)：電梯1或…或n到達(dá)f層其中1…n表示或?yàn)?或?yàn)?…或?yàn)閚。4.2.2例子C2：除了大廈的最低層和最高層之外，每層樓都有兩個(gè)按鈕分別請(qǐng)求電梯上行和下行。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移動(dòng)。

樓層按鈕的狀態(tài)轉(zhuǎn)換圖令FB(d,f)表示f層請(qǐng)求電梯向d方向運(yùn)動(dòng)的按鈕，樓層按鈕為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個(gè)謂詞，它是S(d,e,f)，它的定義如下:S(d,e,f)：電梯e停在f層并且移動(dòng)方向由d確定為向上(d=U)或向下(d=D)或待定(d=N)。4.2.2例子為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個(gè)使用謂詞S(d,e,f)，形式化轉(zhuǎn)換規(guī)則為：FBOFF(d,f)+FBP(d,f)+notS(d,1…n,f)

FBON(d,f)反之FBON(d,f)+EAF(1…n,f)+S(d,1…n,f)

FBOFF(d,f)其中，d=U

or

D。4.2.2例子使用謂詞S(d,e,f)，形式化轉(zhuǎn)換規(guī)則為：4.2.2例在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時(shí)定義的謂詞V(e,f)，可以用謂詞S(d,e,f)重新定義如下：V(e,f)=S(U,e,f)orS(D,e,f)orS(N,e,f)電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則:一個(gè)電梯狀態(tài)實(shí)質(zhì)上包含許多子狀態(tài),下面定義電梯的3個(gè)狀態(tài)：M(d,e,f)：電梯e正沿d方向移動(dòng)，即將到達(dá)的是第f層S(d,e,f)：電梯e停在f層，將朝d方向移動(dòng)(尚未關(guān)門)W(e,f)：電梯e在f層等待(已關(guān)門)4.2.2例子在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時(shí)定義的謂詞V(e,f)，可以用謂4.2.2例子圖4.4電梯的狀態(tài)轉(zhuǎn)換圖4.2.2例子圖4.4中包含了下述3個(gè)可觸發(fā)狀態(tài)發(fā)生改變的事件。DC(e,f)：電梯e在樓層f關(guān)上門ST(e,f)：電梯e靠近f層時(shí)觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開狀態(tài)，登錄需求4.2.2例子圖4.4中包含了下述3個(gè)可觸發(fā)狀態(tài)發(fā)生改變的事件。4.2.2最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡(jiǎn)單起見，這里給出的規(guī)則僅發(fā)生在關(guān)門之時(shí)。S(U,e,f)+DC(e,f)

M(U,e,f+1)S(D,e,f)+DC(e,f)

M(D,e,f-1)S(N,e,f)+DC(e,f)

W(e,f)4.2.2例子最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡(jiǎn)單起見，這里給出的規(guī)則僅發(fā)4.2.3

評(píng)價(jià)有窮狀態(tài)機(jī)方法描述規(guī)格說明：當(dāng)前狀態(tài)+事件+謂詞

下個(gè)狀態(tài)優(yōu)點(diǎn)：規(guī)格說明易于書寫、易于驗(yàn)證，而且可以比較容易地把它轉(zhuǎn)變成設(shè)計(jì)或程序代碼。有窮狀態(tài)機(jī)方法比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理解。缺點(diǎn)：在開發(fā)一個(gè)大系統(tǒng)時(shí)三元組(即狀態(tài)、事件、謂詞)的數(shù)量會(huì)迅速增長(zhǎng)。此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機(jī)方法也沒有處理定時(shí)需求。4.2.3評(píng)價(jià)有窮狀態(tài)機(jī)方法描述規(guī)格說明：第4章形式化說明技術(shù)4.1概述4.2有窮狀態(tài)機(jī)4.3

Petri網(wǎng)4.4

Z語言第4章形式化說明技術(shù)4.1概述4.3Petri網(wǎng)4.3.1概念并發(fā)系統(tǒng)中需要解決的主要問題是定時(shí)問題：包括同步問題、競(jìng)爭(zhēng)條件以及死鎖問題。定時(shí)問題常常是因不好的設(shè)計(jì)或有錯(cuò)誤的實(shí)現(xiàn)引起的，歸根到底又是由不好的規(guī)格說明造成的.Petri網(wǎng)技術(shù)可用于確定系統(tǒng)中隱含的定時(shí)問題。Petri網(wǎng)技術(shù)在計(jì)算機(jī)領(lǐng)域應(yīng)用較多，已經(jīng)證明，用Petri網(wǎng)可以有效地描述并發(fā)活動(dòng)。4.3Petri網(wǎng)4.3.1概念Petri網(wǎng)包含4種元素：一組位置P一組轉(zhuǎn)換T輸入函數(shù)I輸出函數(shù)O4.3.1概念位置轉(zhuǎn)換輸入輸出Petri網(wǎng)包含4種元素：4.3.1概念位置轉(zhuǎn)換輸入輸出如圖舉例說明了Petri網(wǎng)的組成：一組位置P為｛P1，P2，P3，P4｝：用圓圈代表；一組轉(zhuǎn)換T為｛t1，t2｝：圖中用短直線表示轉(zhuǎn)換；兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是：I(t1)=｛P2，P4｝

I(t2)=｛P2｝兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是：O(t1)=｛P1｝

O(t2)=｛P3，P3｝如圖舉例說明了Petri網(wǎng)的組成：Petri網(wǎng)是一個(gè)四元組C=(P，T，I，O)，其中：P={P1,P2,…Pn}是一個(gè)有窮位置集，n≥0；T=(t1,…,tm)是一個(gè)有窮轉(zhuǎn)換集，m≥0,且T和不相交；I:T→P∞為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射；O:T→P∞為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。4.3.1概念Petri網(wǎng)是一個(gè)四元組C=(P，T，I，O)，其中：4.3帶標(biāo)記的Petri網(wǎng)：權(quán)標(biāo)(token)的分配。如圖中有4個(gè)權(quán)標(biāo)上述標(biāo)記可以用向量(1，2，0，1)表示。由于P2和P4中有權(quán)標(biāo)，因此t1啟動(dòng)(即被激發(fā))。通常，當(dāng)每個(gè)輸入位置所擁有的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù)時(shí)，就允許轉(zhuǎn)換。當(dāng)t1被激發(fā)時(shí)，P2和P4上各有一個(gè)權(quán)標(biāo)被移出，而P1上則增加一個(gè)權(quán)標(biāo)（2，1，0，0）。Petri網(wǎng)中權(quán)標(biāo)總數(shù)不是固定的，在這個(gè)例子中兩個(gè)權(quán)標(biāo)被移出，而P1上只能增加一個(gè)權(quán)標(biāo)。4.3.1概念權(quán)標(biāo)數(shù)帶標(biāo)記的Petri網(wǎng)：4.3.1概念權(quán)標(biāo)數(shù)如圖，P2上有權(quán)標(biāo)，因此t2也可以被激發(fā)。當(dāng)t2被激發(fā)時(shí)，P2上將移走一個(gè)權(quán)標(biāo)，而P3上新增加兩個(gè)權(quán)標(biāo)（1，1，2，1）。4.3.1概念如圖，P2上有權(quán)標(biāo)，因此t2也可以被激發(fā)。當(dāng)t2被激發(fā)時(shí)，PPetri網(wǎng)具有非確定性，如果數(shù)個(gè)轉(zhuǎn)換都達(dá)到了激發(fā)條件，則其中任意一個(gè)都可以被激發(fā)。圖4.6所示Petri網(wǎng)的標(biāo)記為(1，2，0，1)，t1和t2都可以被激發(fā)。4.3.1概念假設(shè)t1被激發(fā)了，標(biāo)記為(2，1，0，0)。此時(shí)，只有t2可以被激發(fā)。如果t2也被激發(fā)了，則權(quán)標(biāo)從P2中移出，兩個(gè)新權(quán)標(biāo)被放在P3上，標(biāo)記為(2，0，2，0)。Petri網(wǎng)具有非確定性，如果數(shù)個(gè)轉(zhuǎn)換都達(dá)到了激發(fā)條件，則其帶有標(biāo)記的Petri網(wǎng)成為一個(gè)五元組(P，T，I，O，M),其中標(biāo)記M，是由一組位置P到一組非負(fù)整數(shù)的映射：M：P→｛0，1，2，…｝對(duì)Petri網(wǎng)的一個(gè)重要擴(kuò)充是加入禁止線禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記的輸入線，如圖所示。4.3.1概念禁止線帶有標(biāo)記的Petri網(wǎng)成為一個(gè)五元組(P，T，I，O，M),通常，當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)換才是允許的。圖中P3上有一個(gè)權(quán)標(biāo)而P2上沒有權(quán)標(biāo)，因此轉(zhuǎn)換t1可以被激發(fā)。4.3.1概念禁止線輸入線通常，當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時(shí)候把Petri網(wǎng)應(yīng)用于電梯問題。當(dāng)用Petri網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時(shí)，每個(gè)樓層用一個(gè)位置Ff代表(1≤f≤m)，在Petri網(wǎng)中電梯是用一個(gè)權(quán)標(biāo)代表的。在位置Ff上有權(quán)標(biāo)，表示在樓層f上有電梯。1.電梯按鈕第一個(gè)約束條件描述了電梯按鈕的行為。C1：每部電梯有m個(gè)按鈕，每層對(duì)應(yīng)一個(gè)按鈕。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時(shí)，按鈕將熄滅。4.3.2例子把Petri網(wǎng)應(yīng)用于電梯問題。4.3.2例子為了用Petri網(wǎng)表達(dá)電梯按鈕的規(guī)格說明，需要設(shè)置其它位置。電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個(gè)權(quán)標(biāo)，就表示電梯內(nèi)樓層f的按鈕被按下了。4.3.2例子為了用Petri網(wǎng)表達(dá)電梯按鈕的規(guī)格說明，需要設(shè)置其它位置。用Petri網(wǎng)可準(zhǔn)確地電梯按鈕的行為規(guī)律。首先，假設(shè)按鈕沒有發(fā)亮，顯然在位置E