第4章形式語言剖析

1、西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 1 第4章形式語言剖析 第第4 4章章 形式化說明技術(shù)形式化說明技術(shù) 4.1 概述概述 4.2 有窮狀態(tài)機有窮狀態(tài)機 4.3 Petri網(wǎng)網(wǎng) 4.4 Z語言語言 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 2 第4章形式語言剖析 按形式化的程度，按形式化的程度，可把軟件工程使用的可把軟件工程使用的 方法分成：非

2、形式化、半形式化和形式化方法分成：非形式化、半形式化和形式化 非形式化方法非形式化方法：用自然語言描述需求規(guī)：用自然語言描述需求規(guī) 格說明，是典型的格說明，是典型的非形式化方法非形式化方法 。 半形式化方法：用數(shù)據(jù)流圖或?qū)嶓w半形式化方法：用數(shù)據(jù)流圖或?qū)嶓w- -聯(lián)系聯(lián)系 圖建立模型，是典型的半形式化方法。圖建立模型，是典型的半形式化方法。 形式化方法形式化方法： 描述系統(tǒng)性質(zhì)的是基于數(shù)描述系統(tǒng)性質(zhì)的是基于數(shù) 學(xué)的技術(shù)，也就是說，如果一種方法有堅學(xué)的技術(shù)，也就是說，如果一種方法有堅 實的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。實的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。 西安電子科技大學(xué)計算機學(xué)院 - School

3、of Computer Science & Engineering, Xidian University, China 3 第4章形式語言剖析 4.1 4.1 概述概述 4.1.1 4.1.1 非形式化方法的缺點非形式化方法的缺點 用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義 性、含糊性、不完整性及抽象層次混亂等問題。性、含糊性、不完整性及抽象層次混亂等問題。 矛盾是指一組相互沖突的陳述。矛盾是指一組相互沖突的陳述。 二義性是指讀者可以用不同方式理解的陳述。二義性是指讀者可以用不同方式理解的陳述。 含糊性含糊性: :系統(tǒng)規(guī)格說明書是很龐大

4、的文檔，因此，幾乎不可系統(tǒng)規(guī)格說明書是很龐大的文檔，因此，幾乎不可 避免地會出現(xiàn)含糊性。實際上，這樣籠統(tǒng)的陳述并沒有給出任避免地會出現(xiàn)含糊性。實際上，這樣籠統(tǒng)的陳述并沒有給出任 何有用的信息。何有用的信息。 不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。 抽象層次混亂是指在非常抽象的陳述中混進(jìn)了一些關(guān)于細(xì)抽象層次混亂是指在非常抽象的陳述中混進(jìn)了一些關(guān)于細(xì) 節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀者很難了解系統(tǒng)的節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀者很難了解系統(tǒng)的 整體功能結(jié)構(gòu)。整體功能結(jié)構(gòu)。 西安電子科技大學(xué)計算機學(xué)院 - School o

5、f Computer Science & Engineering, Xidian University, China 4 第4章形式語言剖析 把數(shù)學(xué)引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學(xué)的形式化方法。把數(shù)學(xué)引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學(xué)的形式化方法。 在開發(fā)大型軟件系統(tǒng)的過程中應(yīng)用數(shù)學(xué)，能夠帶來下述的幾個在開發(fā)大型軟件系統(tǒng)的過程中應(yīng)用數(shù)學(xué)，能夠帶來下述的幾個 優(yōu)點：優(yōu)點： 1. 1.數(shù)學(xué)最有用的一個性質(zhì)是，它能夠簡潔準(zhǔn)確地描述物理現(xiàn)象、數(shù)學(xué)最有用的一個性質(zhì)是，它能夠簡潔準(zhǔn)確地描述物理現(xiàn)象、 對象或動作的結(jié)果，因此是理想的建模工具。對象或動作的結(jié)果，因此是理想的建模工具。 數(shù)學(xué)特別適合于表示狀態(tài)，也

6、就是表示數(shù)學(xué)特別適合于表示狀態(tài)，也就是表示“做什么做什么”。 需求規(guī)格說明書主要描述應(yīng)用系統(tǒng)在運行前和運行后的狀需求規(guī)格說明書主要描述應(yīng)用系統(tǒng)在運行前和運行后的狀 態(tài)，因此，數(shù)學(xué)比自然語言更適于描述詳細(xì)的需求。態(tài)，因此，數(shù)學(xué)比自然語言更適于描述詳細(xì)的需求。 2. 2. 可以在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī)可以在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī) 格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學(xué)表達(dá)，當(dāng)然，程序代碼也格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學(xué)表達(dá)，當(dāng)然，程序代碼也 是一種數(shù)學(xué)符號是一種數(shù)學(xué)符號( (雖然是一種相當(dāng)繁瑣、冗長的數(shù)學(xué)符號雖然是一種相當(dāng)繁瑣、冗長的數(shù)學(xué)符號) )。 3.

7、3. 它提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法證明，它提供了高層確認(rèn)的手段。可以使用數(shù)學(xué)方法證明， 設(shè)計符合規(guī)格說明，程序代碼正確地實現(xiàn)了設(shè)計結(jié)果。設(shè)計符合規(guī)格說明，程序代碼正確地實現(xiàn)了設(shè)計結(jié)果。 4.1.2 4.1.2 形式化方法的優(yōu)點形式化方法的優(yōu)點 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 5 第4章形式語言剖析 人們對形式化方法的看法并不一致。人們對形式化方法的看法并不一致。 擁護(hù)者甚至宣稱這種方法可以引發(fā)軟件開發(fā)方法的革命；擁護(hù)者甚至宣稱這種方法可以引發(fā)軟件開發(fā)

8、方法的革命； 也有人對把數(shù)學(xué)引入軟件開發(fā)過程持懷疑甚至反對的態(tài)度。也有人對把數(shù)學(xué)引入軟件開發(fā)過程持懷疑甚至反對的態(tài)度。 對形式化方法也應(yīng)該對形式化方法也應(yīng)該“一分為二一分為二”，既不要過分夸大它的優(yōu)，既不要過分夸大它的優(yōu) 點也不要一概排斥。點也不要一概排斥。 應(yīng)用形式化方法的應(yīng)用形式化方法的1010條準(zhǔn)則：條準(zhǔn)則： (1) (1) 應(yīng)該選用適當(dāng)?shù)谋硎痉椒☉?yīng)該選用適當(dāng)?shù)谋硎痉椒?應(yīng)該仔細(xì)選擇一種適用于當(dāng)前項目的形式化說明技術(shù)。應(yīng)該仔細(xì)選擇一種適用于當(dāng)前項目的形式化說明技術(shù)。 (2) (2) 應(yīng)該形式化，但不要過分形式化。應(yīng)該形式化，但不要過分形式化。 目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面。

9、但是，也目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面。但是，也 不能因此就認(rèn)為完全沒必要采用形式化方法。形式化規(guī)格說明技不能因此就認(rèn)為完全沒必要采用形式化方法。形式化規(guī)格說明技 術(shù)要求我們非常準(zhǔn)確地描述事物，因此有助于防止含糊和誤解。術(shù)要求我們非常準(zhǔn)確地描述事物，因此有助于防止含糊和誤解。 4.1.3 4.1.3 應(yīng)用形式化方法的準(zhǔn)則應(yīng)用形式化方法的準(zhǔn)則 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 6 第4章形式語言剖析 (3) (3) 應(yīng)該估算成本。應(yīng)該估算成本。 為了使用

10、形式化方法，通常需要事先進(jìn)行大量的培訓(xùn)。最為了使用形式化方法，通常需要事先進(jìn)行大量的培訓(xùn)。最 好預(yù)先估算所需的成本并編入預(yù)算。好預(yù)先估算所需的成本并編入預(yù)算。 (4)(4) 應(yīng)該有形式化方法顧問隨時提供咨詢。絕大多數(shù)軟件工程應(yīng)該有形式化方法顧問隨時提供咨詢。絕大多數(shù)軟件工程 師對形式化方法中使用的數(shù)學(xué)和邏輯并不很熟悉，而且沒受過師對形式化方法中使用的數(shù)學(xué)和邏輯并不很熟悉，而且沒受過 使用形式化方法的專業(yè)訓(xùn)練，因此，需要專家指導(dǎo)和培訓(xùn)。使用形式化方法的專業(yè)訓(xùn)練，因此，需要專家指導(dǎo)和培訓(xùn)。 (5)(5) 不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和結(jié)構(gòu)化方法不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和結(jié)構(gòu)

11、化方法 或面向?qū)ο蠓椒善饋硎强赡艿?，而且由于取長補短往往能或面向?qū)ο蠓椒善饋硎强赡艿?，而且由于取長補短往往能 獲得很好的效果。獲得很好的效果。 (6)(6) 應(yīng)該建立詳盡的文檔。建議使用自然語言注釋形式化的規(guī)應(yīng)該建立詳盡的文檔。建議使用自然語言注釋形式化的規(guī) 格說明書，以幫助用戶和維護(hù)人員理解系統(tǒng)。格說明書，以幫助用戶和維護(hù)人員理解系統(tǒng)。 (7)(7) 不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。 形式化方法并不能保證軟件的正確性，只不過是有助于開形式化方法并不能保證軟件的正確性，只不過是有助于開 發(fā)出高質(zhì)量軟件的一種手段。除使用形式化說明技術(shù)外，在系發(fā)出高質(zhì)量軟件的一種手段。除使用形式化

12、說明技術(shù)外，在系 統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量保證活動。統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量保證活動。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 7 第4章形式語言剖析 (8)(8) 不應(yīng)該盲目依賴形式化方法。不應(yīng)該盲目依賴形式化方法。 只不過是眾多工具中的一種。形式化方法并不能保證開發(fā)只不過是眾多工具中的一種。形式化方法并不能保證開發(fā) 出的軟件絕對正確，例如，無法用形式化方法證明從非形式化出的軟件絕對正確，例如，無法用形式化方法證明從非形式化 需求到

13、形式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其他方需求到形式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其他方 法法(例如，評審、測試?yán)?，評審、測試)來驗證軟件正確性。來驗證軟件正確性。 (9)(9) 應(yīng)該測試、測試再測試。應(yīng)該測試、測試再測試。 形式化方法不僅不能保證軟件系統(tǒng)絕對正確，也不能證明形式化方法不僅不能保證軟件系統(tǒng)絕對正確，也不能證明 系統(tǒng)性能或其他質(zhì)量指標(biāo)符合需要，因此，軟件測試的重要性系統(tǒng)性能或其他質(zhì)量指標(biāo)符合需要，因此，軟件測試的重要性 并沒有降低。并沒有降低。 (10) 應(yīng)該重用。應(yīng)該重用。 即使采用了形式化方法，軟件重用仍然是降低軟件成本和即使采用了形式化方法，軟件重用仍然是降

14、低軟件成本和 提高軟件質(zhì)量的惟一合理的方法。而且用形式化方法說明的軟提高軟件質(zhì)量的惟一合理的方法。而且用形式化方法說明的軟 件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用 性。性。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 8 第4章形式語言剖析 4.2 有窮狀態(tài)機有窮狀態(tài)機 4.2.1 概念概念 實例：介紹有窮狀態(tài)機的基本概念。實例：介紹有窮狀態(tài)機的基本概念。 一個保險箱上裝了一個復(fù)合鎖，鎖有三個位置，一個保

15、險箱上裝了一個復(fù)合鎖，鎖有三個位置， 分別標(biāo)記為分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左，轉(zhuǎn)盤可向左(L)或向右或向右(R)轉(zhuǎn)動。轉(zhuǎn)動。 這樣，在任意時刻轉(zhuǎn)盤都有這樣，在任意時刻轉(zhuǎn)盤都有6種可能的運動，即種可能的運動，即： 1L、1R、2L、2R、3L和和3R。 保險箱的組合密碼是保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其，轉(zhuǎn)盤的任何其 他運動都將引起報警。他運動都將引起報警。 圖圖4.1描繪了保險箱的狀態(tài)轉(zhuǎn)換情況。描繪了保險箱的狀態(tài)轉(zhuǎn)換情況。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University,

16、 China 9 第4章形式語言剖析 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 10 第4章形式語言剖析 狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述， 表格形式也可以表達(dá)同樣的信息。表格形式也可以表達(dá)同樣的信息。 從上例可以看出，一個有窮狀態(tài)機包括下述從上例可以看出，一個有窮狀態(tài)機包括下述5個部分：個部分： 狀態(tài)集狀態(tài)集J、輸入集、輸入集K、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個狀、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個狀 態(tài)態(tài)(次態(tài)次態(tài))的轉(zhuǎn)換函數(shù)的轉(zhuǎn)換函數(shù)T、

17、初始態(tài)、初始態(tài)S和終態(tài)集和終態(tài)集F。 對于對于上例，相應(yīng)的有窮狀態(tài)機各部分如下：上例，相應(yīng)的有窮狀態(tài)機各部分如下： 狀態(tài)集狀態(tài)集J：保險箱鎖定，保險箱鎖定，A，B，保險箱解鎖，報警，保險箱解鎖，報警 輸入集輸入集K：1L，1R，2L，2R，3L，3R 轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T：如表：如表4.1所示。所示。 初始態(tài)初始態(tài)S： 保險箱鎖定。保險箱鎖定。 終態(tài)集終態(tài)集F：保險箱解鎖，報警保險箱解鎖，報警。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 11 第4章形式語言剖析 如果使用更

18、形式化的術(shù)語，一個有窮狀態(tài)機可以如果使用更形式化的術(shù)語，一個有窮狀態(tài)機可以 表示為一個表示為一個5 5元組元組(J (J，K K，T T，S S，F(xiàn))F)，其中：，其中： J J是一個有窮的非空狀態(tài)集；是一個有窮的非空狀態(tài)集； K K是一個有窮的非空輸入集；是一個有窮的非空輸入集； T T是一個從是一個從(J-F)(J-F)K K到到J J的轉(zhuǎn)換函數(shù)；的轉(zhuǎn)換函數(shù)； SJ SJ，是一個初始狀態(tài)；，是一個初始狀態(tài)； F FJ J，是終態(tài)集。，是終態(tài)集。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian Universi

19、ty, China 12 第4章形式語言剖析 有窮狀態(tài)機概念在計算機系統(tǒng)中應(yīng)用得非常廣泛。有窮狀態(tài)機概念在計算機系統(tǒng)中應(yīng)用得非常廣泛。 例如：例如： 每個菜單驅(qū)動的用戶界面都是一個有窮狀態(tài)機的實每個菜單驅(qū)動的用戶界面都是一個有窮狀態(tài)機的實 現(xiàn)。一個菜單的顯示和一個狀態(tài)相對應(yīng)，現(xiàn)。一個菜單的顯示和一個狀態(tài)相對應(yīng)， 鍵盤輸入或用鼠標(biāo)選擇一個圖標(biāo)是使系統(tǒng)進(jìn)入鍵盤輸入或用鼠標(biāo)選擇一個圖標(biāo)是使系統(tǒng)進(jìn)入 其他狀態(tài)的一個事件。其他狀態(tài)的一個事件。 狀態(tài)的每個轉(zhuǎn)換都具有下面的形式：狀態(tài)的每個轉(zhuǎn)換都具有下面的形式： 當(dāng)前狀態(tài)當(dāng)前狀態(tài)菜單菜單+ +事件事件所選擇的項所選擇的項下個狀態(tài)下個狀態(tài) 西安電子科技大學(xué)計算

20、機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 13 第4章形式語言剖析 進(jìn)行規(guī)格說明進(jìn)行規(guī)格說明時，通常對有窮狀態(tài)機做一個擴展，即時，通常對有窮狀態(tài)機做一個擴展，即 在前述的在前述的5 5元組中加入元組中加入 第第6 6個組件個組件謂詞集謂詞集P P； 把有窮狀態(tài)機擴展為一個把有窮狀態(tài)機擴展為一個6 6元組，其中每個謂詞都是元組，其中每個謂詞都是 系統(tǒng)全局狀態(tài)系統(tǒng)全局狀態(tài)Y Y的函數(shù)。的函數(shù)。 轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T T現(xiàn)在是一個從現(xiàn)在是一個從(J-F)(J-F)K KP P到到J J的函數(shù)。的函數(shù)

21、。 現(xiàn)在的轉(zhuǎn)換規(guī)則形式如下：現(xiàn)在的轉(zhuǎn)換規(guī)則形式如下： 當(dāng)前狀態(tài)當(dāng)前狀態(tài) 菜單菜單+事件事件 所選擇的項所選擇的項+謂詞謂詞 下個狀態(tài)下個狀態(tài) 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 14 第4章形式語言剖析 4.2.2 4.2.2 例子例子 用有窮狀態(tài)機技術(shù)表達(dá)電梯系統(tǒng)的規(guī)格說明。用有窮狀態(tài)機技術(shù)表達(dá)電梯系統(tǒng)的規(guī)格說明。 首先給出用自然語言描述的對電梯系統(tǒng)的需求：首先給出用自然語言描述的對電梯系統(tǒng)的需求： 在一幢在一幢mm層大廈中需要一套控制層大廈中需要一套控制n n部

22、電梯的產(chǎn)品，要部電梯的產(chǎn)品，要 求這求這n n部電梯按照約束條件部電梯按照約束條件C1C1，C2C2和和C3C3在樓層間移動。在樓層間移動。 C1 C1：每部電梯內(nèi)有：每部電梯內(nèi)有mm個按鈕，每個按鈕代表一個按鈕，每個按鈕代表一 個樓層。個樓層。 當(dāng)按下一個按鈕時該按鈕指示燈亮，同時當(dāng)按下一個按鈕時該按鈕指示燈亮，同時 電梯駛向相應(yīng)的樓層電梯駛向相應(yīng)的樓層； 到達(dá)按鈕指定的樓層時指示燈熄滅。到達(dá)按鈕指定的樓層時指示燈熄滅。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 15

23、第4章形式語言剖析 C2：除了大廈的最低層和最高層之外，每層樓都：除了大廈的最低層和最高層之外，每層樓都 有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之 一被按下時相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時燈一被按下時相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時燈 熄滅，電梯向要求的方向移動。熄滅，電梯向要求的方向移動。 C3：對電梯沒有請求時，關(guān)門并停在當(dāng)前樓層。：對電梯沒有請求時，關(guān)門并停在當(dāng)前樓層。 使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進(jìn)行規(guī)格說使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進(jìn)行規(guī)格說 明。題中有兩個按鈕集。明。題中有兩個按鈕集。 電梯按鈕電梯按鈕： n部電梯中

24、的每一部都有部電梯中的每一部都有m個按鈕，個按鈕， 一個按鈕對應(yīng)一個樓層。一個按鈕對應(yīng)一個樓層。mn個按鈕都在電梯中。個按鈕都在電梯中。 樓層按鈕：每層樓有兩個按鈕，一個請求向上，樓層按鈕：每層樓有兩個按鈕，一個請求向上， 另一個請求向下。另一個請求向下。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 16 第4章形式語言剖析 電梯按鈕電梯按鈕：狀態(tài)轉(zhuǎn)換圖如圖所示。：狀態(tài)轉(zhuǎn)換圖如圖所示。 令令EB(e,f)表示按下電梯表示按下電梯e內(nèi)的按鈕并請求到內(nèi)的按鈕并請求到f層去。層去

25、。 EB(e,f)有兩個狀態(tài)：有兩個狀態(tài)： EBON(e,f)：電梯按鈕：電梯按鈕(e,f)打開打開 EBOFF(e,f)：電梯按鈕：電梯按鈕(e,f)關(guān)閉關(guān)閉 如果電梯按鈕如果電梯按鈕(e,f)(e,f)發(fā)光且電梯到達(dá)發(fā)光且電梯到達(dá)f f層，該按鈕將熄滅。相層，該按鈕將熄滅。相 反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。 上述描述中包含了兩個事件，它們分別是上述描述中包含了兩個事件，它們分別是： EBP(e,f)：電梯按鈕：電梯按鈕(e,f)被按下被按下 EAF(e,f)：電梯：電梯e到達(dá)到達(dá)f層層 西安電子科技大學(xué)計算機學(xué)院 - School of C

26、omputer Science & Engineering, Xidian University, China 17 第4章形式語言剖析 為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則， 需要一個謂詞需要一個謂詞V(e,f)V(e,f)，它的含義如下：，它的含義如下： V(e,f) V(e,f)：電梯：電梯e e停在停在f f層層 如果電梯按鈕如果電梯按鈕(e,f)(e,f)處于關(guān)閉狀態(tài)處于關(guān)閉狀態(tài)當(dāng)前狀態(tài)當(dāng)前狀態(tài)， 且電梯按鈕且電梯按鈕(e,f)(e,f)被按下被按下事件事件，而且電梯，而且電梯e e不在不在f f 層層謂詞謂詞，則該電梯按鈕打開發(fā)

27、光，則該電梯按鈕打開發(fā)光下個狀態(tài)下個狀態(tài)。 狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下： 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) 反之，如果電梯到達(dá)反之，如果電梯到達(dá)f f層，且電梯按鈕是打開的，層，且電梯按鈕是打開的， 于是它就會熄滅。于是它就會熄滅。 這條轉(zhuǎn)換規(guī)則可以形式化地表示為：這條轉(zhuǎn)換規(guī)則可以形式化地表示為： EAF(e,f)+EBON(e,f) EAF(e,f)+EBON(e,f) EBOFF(e,f)EBOFF(e,f) 西安電子科技大學(xué)計算機學(xué)院

28、 - School of Computer Science & Engineering, Xidian University, China 18 第4章形式語言剖析 樓層按鈕：令樓層按鈕：令FB(d,f)表示表示f層請求電梯向?qū)诱埱箅娞菹騞方向運動的按鈕，方向運動的按鈕， 樓層按鈕樓層按鈕FB(d,f)的狀態(tài)轉(zhuǎn)換圖如圖：的狀態(tài)轉(zhuǎn)換圖如圖： 樓層按鈕的狀態(tài)如下：樓層按鈕的狀態(tài)如下： FBON(d,f)：樓層按鈕：樓層按鈕(d,f)打開打開 FBOFF(d,f)：樓層按鈕：樓層按鈕(d,f)關(guān)閉關(guān)閉 如果樓層按鈕已經(jīng)打開，而且一部電梯到達(dá)如果樓層按鈕已經(jīng)打開，而且一部電梯到達(dá)f f層，則按鈕層，則

29、按鈕 關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打 開。這段敘述中包含了以下兩個事件。開。這段敘述中包含了以下兩個事件。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 19 第4章形式語言剖析 FBP(d,f) FBP(d,f)：樓層按鈕：樓層按鈕(d,f)(d,f)被按下被按下 EAF(1 EAF(1n,f)n,f)：電梯：電梯1 1或或或或n n到達(dá)到達(dá)f f層層 其中：其中：1 1n n 表示表示 或為

30、或為1 1或為或為2 2或為或為n n。 為定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也為定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也 需要一個謂詞，需要一個謂詞，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)。 這個謂詞實際上是一個狀態(tài)，形式化方法允許把事件和狀這個謂詞實際上是一個狀態(tài)，形式化方法允許把事件和狀 態(tài)作為謂詞對待。態(tài)作為謂詞對待。 西安電子科技大學(xué)計算機

31、學(xué)院 - School of Computer Science & Engineering, Xidian University, China 20 第4章形式語言剖析 使用謂詞使用謂詞S(d,e,f)S(d,e,f)，形式化轉(zhuǎn)換規(guī)則為：，形式化轉(zhuǎn)換規(guī)則為： FBOFF(d,f)+FBP(d,f)+not S(d,1FBOFF(d,f)+FBP(d,f)+not S(d,1n,f)n,f)FBON(d,f)FBON(d,f) FBON(d,f)+EAF(1FBON(d,f)+EAF(1n,f)+S(d,1n,f)+S(d,1n,f)n,f)FBOFF(d,f)FBOFF(d,f) 其中，其中，

32、d=U or Dd=U or D。 如果在如果在f f層請求電梯向?qū)诱埱箅娞菹騞 d方向運動的樓層按鈕處于關(guān)閉狀態(tài)，方向運動的樓層按鈕處于關(guān)閉狀態(tài)， 現(xiàn)在該按鈕被按下，并且當(dāng)時沒有正停在現(xiàn)在該按鈕被按下，并且當(dāng)時沒有正停在f f層準(zhǔn)備向?qū)訙?zhǔn)備向d d方向移動方向移動 的電梯，則該樓層按鈕打開。的電梯，則該樓層按鈕打開。 反之，如果樓層按鈕已經(jīng)打開，且至少有一部電梯到達(dá)反之，如果樓層按鈕已經(jīng)打開，且至少有一部電梯到達(dá)f f層，層， 該部電梯將朝該部電梯將朝d d方向運動，則按鈕將關(guān)閉。方向運動，則按鈕將關(guān)閉。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science

33、& Engineering, Xidian University, China 21 第4章形式語言剖析 討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞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) 定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀的事情。定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀的事情。 現(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則，就會出現(xiàn)一些復(fù)雜

34、的情現(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則，就會出現(xiàn)一些復(fù)雜的情 況。一個電梯狀態(tài)實質(zhì)上包含許多子狀態(tài)。況。一個電梯狀態(tài)實質(zhì)上包含許多子狀態(tài)。 定義電梯的定義電梯的3 3個狀態(tài)：個狀態(tài)： M(d,e,f)M(d,e,f)：電梯：電梯e e正沿正沿d d方向移動，即將到達(dá)的是第方向移動，即將到達(dá)的是第f f層層 S(d,e,f)S(d,e,f)：電梯：電梯e e停在停在f f層，將朝層，將朝d d方向移動方向移動( (尚未關(guān)門尚未關(guān)門) ) W(e,f)W(e,f)：電梯：電梯e e在在f f層等待層等待( (已關(guān)門已關(guān)門) ) 西安電子科技大學(xué)計算機學(xué)院 - School of Computer

35、Science & Engineering, Xidian University, China 22 第4章形式語言剖析 其中其中S(d,e,f)狀態(tài)已在討論樓層按鈕時定義過，但是，現(xiàn)在狀態(tài)已在討論樓層按鈕時定義過，但是，現(xiàn)在 的定義更完備一些。的定義更完備一些。 圖圖4.44.4是電梯的狀態(tài)轉(zhuǎn)換圖。是電梯的狀態(tài)轉(zhuǎn)換圖。3 3個電梯停止?fàn)顟B(tài)個電梯停止?fàn)顟B(tài)S(U,e,f)S(U,e,f)、 S(N,e,f)S(N,e,f)和和S(D,e,f)S(D,e,f)已被組合成一個大的狀態(tài)，這樣做的目的是減已被組合成一個大的狀態(tài)，這樣做的目的是減 少狀態(tài)總數(shù)以簡化流圖。少狀態(tài)總數(shù)以簡化流圖。 圖中包含了下

36、述圖中包含了下述3個可觸發(fā)狀態(tài)發(fā)生改變的事件。個可觸發(fā)狀態(tài)發(fā)生改變的事件。 DC(e,f)：電梯：電梯e在樓層在樓層f關(guān)上門關(guān)上門 ST(e,f)：電梯：電梯e靠近靠近f層時觸發(fā)傳感器，電梯控制器決層時觸發(fā)傳感器，電梯控制器決 定在當(dāng)前樓層電梯是否停下；定在當(dāng)前樓層電梯是否停下； RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開狀態(tài)，登：電梯按鈕或樓層按鈕被按下進(jìn)入打開狀態(tài)，登 錄需求錄需求 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 23 第4章形式語言剖析 圖圖4.4 電梯的狀態(tài)

37、轉(zhuǎn)換圖電梯的狀態(tài)轉(zhuǎn)換圖 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 24 第4章形式語言剖析 最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡單起見，最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡單起見， 這里給出的規(guī)則僅發(fā)生在關(guān)門之時。這里給出的規(guī)則僅發(fā)生在關(guān)門之時。 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)+D

38、C(e,f)S(N,e,f)+DC(e,f)W(e,f)W(e,f) 第一條規(guī)則表明，如果電梯第一條規(guī)則表明，如果電梯e e停在停在f f層準(zhǔn)備向上移層準(zhǔn)備向上移 動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。 第二條和第三條規(guī)則，分別對應(yīng)于電梯即將下降第二條和第三條規(guī)則，分別對應(yīng)于電梯即將下降 或者沒有待處理的請求的情況?；蛘邲]有待處理的請求的情況。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 25 第4章形式語言剖析 有窮狀態(tài)機方法

39、用一種簡單格式描述規(guī)格說明：有窮狀態(tài)機方法用一種簡單格式描述規(guī)格說明： 當(dāng)前狀態(tài)當(dāng)前狀態(tài)+ +事件事件+ +謂詞下個狀態(tài)謂詞下個狀態(tài) 這種形式的規(guī)格說明易于書寫、易于驗證，而這種形式的規(guī)格說明易于書寫、易于驗證，而 且可以比較容易地把它轉(zhuǎn)變成設(shè)計或程序代碼?？梢郧铱梢员容^容易地把它轉(zhuǎn)變成設(shè)計或程序代碼。可以 開發(fā)一個開發(fā)一個CASECASE工具把一個有窮狀態(tài)機規(guī)格說明直接工具把一個有窮狀態(tài)機規(guī)格說明直接 轉(zhuǎn)變?yōu)樵创a。轉(zhuǎn)變?yōu)樵创a。 維護(hù)可以通過重新轉(zhuǎn)變來實現(xiàn)，如果需要一個維護(hù)可以通過重新轉(zhuǎn)變來實現(xiàn)，如果需要一個 新的狀態(tài)或事件，首先修改規(guī)格說明，然后直接由新新的狀態(tài)或事件，首先修改規(guī)格說明，

40、然后直接由新 的規(guī)格說明生成新版本的產(chǎn)品。的規(guī)格說明生成新版本的產(chǎn)品。 4.2.3 評價評價 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 26 第4章形式語言剖析 有窮狀態(tài)機方法比數(shù)據(jù)流圖技術(shù)更精確，而且和它有窮狀態(tài)機方法比數(shù)據(jù)流圖技術(shù)更精確，而且和它 一樣易于理解。一樣易于理解。 缺點：在開發(fā)一個大系統(tǒng)時三元組缺點：在開發(fā)一個大系統(tǒng)時三元組( (即狀態(tài)、事件、即狀態(tài)、事件、 謂詞謂詞) )的數(shù)量會迅速增長。的數(shù)量會迅速增長。 此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機此

41、外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機 方法也沒有處理定時需求。方法也沒有處理定時需求。 Petri Petri網(wǎng)技術(shù)，是一種可處理定時問題的形式化方法。網(wǎng)技術(shù)，是一種可處理定時問題的形式化方法。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 27 第4章形式語言剖析 并發(fā)系統(tǒng)中遇到的一個主要問題是并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題定時問題。它。它 可以表現(xiàn)為多種形式，如同步問題、競爭條件以及死可以表現(xiàn)為多種形式，如同步問題、競爭條件以及死 鎖問題。鎖問題。 定時問題

42、通常是由不好的設(shè)計或有錯誤的實現(xiàn)引定時問題通常是由不好的設(shè)計或有錯誤的實現(xiàn)引 起的，而這樣的設(shè)計或?qū)崿F(xiàn)通常又是由不好的規(guī)格說起的，而這樣的設(shè)計或?qū)崿F(xiàn)通常又是由不好的規(guī)格說 明造成的。如果規(guī)格說明不恰當(dāng)，則有導(dǎo)致不完善的明造成的。如果規(guī)格說明不恰當(dāng)，則有導(dǎo)致不完善的 設(shè)計或?qū)崿F(xiàn)的危險。設(shè)計或?qū)崿F(xiàn)的危險。 Petri Petri網(wǎng)是一種有效的用于確定系統(tǒng)中隱含定時問網(wǎng)是一種有效的用于確定系統(tǒng)中隱含定時問 題的技術(shù)，其優(yōu)點是它也可以用于設(shè)計中。題的技術(shù)，其優(yōu)點是它也可以用于設(shè)計中。 4.3 Petri網(wǎng)網(wǎng) 4.3.1 概念概念 西安電子科技大學(xué)計算機學(xué)院 - School of Computer S

43、cience & Engineering, Xidian University, China 28 第4章形式語言剖析 Petri Petri網(wǎng)是由網(wǎng)是由Carl Adam PetriCarl Adam Petri發(fā)明的。最初只有自發(fā)明的。最初只有自 動化專家對動化專家對PetriPetri網(wǎng)感興趣，后來網(wǎng)感興趣，后來PetriPetri網(wǎng)在計算機科學(xué)網(wǎng)在計算機科學(xué) 中也得到廣泛的應(yīng)用，例如：在性能評價、操作系統(tǒng)中也得到廣泛的應(yīng)用，例如：在性能評價、操作系統(tǒng) 和軟件工程等領(lǐng)域，和軟件工程等領(lǐng)域，PetriPetri網(wǎng)應(yīng)用得都比較廣泛。網(wǎng)應(yīng)用得都比較廣泛。 已經(jīng)證明，用已經(jīng)證明，用PetriPe

44、tri網(wǎng)可以有效地描述并發(fā)活動。網(wǎng)可以有效地描述并發(fā)活動。 Petri Petri網(wǎng)包含網(wǎng)包含4 4種元素：一組位置種元素：一組位置P P、一組轉(zhuǎn)換、一組轉(zhuǎn)換T T、 輸入函數(shù)輸入函數(shù)I I、輸出函數(shù)、輸出函數(shù)OO。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 29 第4章形式語言剖析 一組位置一組位置PP1PP1，P2P2，P3P3，P4P4，圖中圓圈代表位置。，圖中圓圈代表位置。 一組轉(zhuǎn)換一組轉(zhuǎn)換Tt1Tt1，t2t2， 圖中用短直線表示轉(zhuǎn)換。圖中用短直線表示轉(zhuǎn)換。 兩

45、個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭 表示，它們是：表示，它們是： I(t1)= I(t1)= P2P2，P4P4 I(t2)= I(t2)=P2P2 兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭 表示，它們是：表示，它們是： O(t1)= O(t1)=P1P1 O(t2)= O(t2)=P3P3，P3P3 注意：輸出函數(shù)注意：輸出函數(shù)O(t2)O(t2)中有兩個中有兩個P3P3，是因為有兩個，是因為有兩個 箭頭由箭頭由t2t2指向指向P3P3。 西安電子科技大學(xué)計算機學(xué)院 - School

46、of Computer Science & Engineering, Xidian University, China 30 第4章形式語言剖析 更形式化的更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個四元組網(wǎng)結(jié)構(gòu)，是一個四元組C=(P,T,I,O)。 其中：其中： P=P1，Pn是一個有窮位置集，是一個有窮位置集，n0。 T=t1，tm是一個有窮轉(zhuǎn)換集，是一個有窮轉(zhuǎn)換集，m0，且，且T和和P不相交。不相交。 I： TP為輸入函數(shù)，為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組是由轉(zhuǎn)換到位置無序單位組(bags)的映射。的映射。 O：TP為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位

47、組的映射。 一個無序單位組或多重組是允許一個元素有多個實例的廣一個無序單位組或多重組是允許一個元素有多個實例的廣 義集。義集。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 31 第4章形式語言剖析 Petri網(wǎng)的標(biāo)記是在網(wǎng)的標(biāo)記是在Petri網(wǎng)中權(quán)標(biāo)網(wǎng)中權(quán)標(biāo)(token)的分配。如下圖中的分配。如下圖中 有有4個權(quán)標(biāo)，其中：個權(quán)標(biāo)，其中： 一個在一個在P1和和 P4中，兩個在中，兩個在P2中，中，P3中沒有。中沒有。 上述標(biāo)記可以用向量上述標(biāo)記可以用向量(1，2，0，1)表

48、示。由于表示。由于P2和和P4中有中有 權(quán)標(biāo)，因此權(quán)標(biāo)，因此t1啟動啟動(即被激發(fā)即被激發(fā))。 通常，當(dāng)每個輸入位置所擁有的權(quán)標(biāo)數(shù)大于等于從該位置通常，當(dāng)每個輸入位置所擁有的權(quán)標(biāo)數(shù)大于等于從該位置 到轉(zhuǎn)換的線數(shù)時，就允許轉(zhuǎn)換。到轉(zhuǎn)換的線數(shù)時，就允許轉(zhuǎn)換。 當(dāng)當(dāng)t1被激發(fā)時，被激發(fā)時，P2和和P4上各有一個權(quán)標(biāo)被移出，而上各有一個權(quán)標(biāo)被移出，而P1上則上則 增加一個權(quán)標(biāo)。增加一個權(quán)標(biāo)。Petri網(wǎng)中權(quán)標(biāo)總數(shù)不是固定的，在這個例子中網(wǎng)中權(quán)標(biāo)總數(shù)不是固定的，在這個例子中 兩個權(quán)標(biāo)被移出，而兩個權(quán)標(biāo)被移出，而P1上只能增加一個權(quán)標(biāo)。上只能增加一個權(quán)標(biāo)。 西安電子科技大學(xué)計算機學(xué)院 - School o

49、f Computer Science & Engineering, Xidian University, China 32 第4章形式語言剖析 上圖中上圖中P2上有權(quán)標(biāo)，因此上有權(quán)標(biāo)，因此t2也可以被激發(fā)。當(dāng)也可以被激發(fā)。當(dāng)t2 被激發(fā)時，被激發(fā)時，P2上將移走一個權(quán)標(biāo)，而上將移走一個權(quán)標(biāo)，而P3上新增加兩個上新增加兩個 權(quán)標(biāo)。權(quán)標(biāo)。 Petri網(wǎng)具有非確定性，如果數(shù)個轉(zhuǎn)換都達(dá)到了激網(wǎng)具有非確定性，如果數(shù)個轉(zhuǎn)換都達(dá)到了激 發(fā)條件，則其中任意一個都可以被激發(fā)。發(fā)條件，則其中任意一個都可以被激發(fā)。 假設(shè)假設(shè)t1被激發(fā)了，結(jié)果如圖，標(biāo)記為被激發(fā)了，結(jié)果如圖，標(biāo)記為(2，1，0，0)。 西安電子科技大

50、學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 33 第4章形式語言剖析 如果如果t2也被激發(fā)了，則權(quán)標(biāo)從也被激發(fā)了，則權(quán)標(biāo)從P2中移出，兩個新中移出，兩個新 權(quán)標(biāo)被放在權(quán)標(biāo)被放在P3上，結(jié)果如圖，標(biāo)記為上，結(jié)果如圖，標(biāo)記為(2，0，2，0)。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 34 第4章形式語言剖析 更形式化地說，更形式化地說，Petri網(wǎng)網(wǎng)C=(P，T，I

51、，O)中的標(biāo)記中的標(biāo)記M，是由，是由 一組位置一組位置P到一組非負(fù)整數(shù)的映射：到一組非負(fù)整數(shù)的映射： M：P0，1，2， 這樣，這樣，帶標(biāo)記的帶標(biāo)記的PetriPetri網(wǎng)成為一個五元組網(wǎng)成為一個五元組(P(P，T T，I I，OO，M)M)。 對對Petri網(wǎng)的一個重要擴充是加入禁止線。如圖，禁止線是用網(wǎng)的一個重要擴充是加入禁止線。如圖，禁止線是用 一個小圓圈而不是用箭頭標(biāo)記的輸入線。一個小圓圈而不是用箭頭標(biāo)記的輸入線。 通常，當(dāng)每個輸入線上至少有一個權(quán)標(biāo)，而禁止線上沒有通常，當(dāng)每個輸入線上至少有一個權(quán)標(biāo)，而禁止線上沒有 權(quán)標(biāo)的時候，相應(yīng)的轉(zhuǎn)換才是允許的。圖中，權(quán)標(biāo)的時候，相應(yīng)的轉(zhuǎn)換才是允許

52、的。圖中，P3P3上有一個權(quán)標(biāo)而上有一個權(quán)標(biāo)而 P2P2上沒有權(quán)標(biāo)，因此轉(zhuǎn)換上沒有權(quán)標(biāo)，因此轉(zhuǎn)換t1t1可以被激發(fā)?？梢员患ぐl(fā)。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 35 第4章形式語言剖析 應(yīng)用應(yīng)用Petri網(wǎng)討論電梯問題。網(wǎng)討論電梯問題。 當(dāng)用當(dāng)用Petri網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時，每個樓網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時，每個樓 層用一個位置層用一個位置Ff代表代表(1fm)，在，在Petri網(wǎng)中電梯是用網(wǎng)中電梯是用 一個權(quán)標(biāo)代表的。在位置一個權(quán)標(biāo)代表的。在位置Ff

53、上有權(quán)標(biāo)，表示在樓層上有權(quán)標(biāo)，表示在樓層f上上 有電梯。有電梯。 1. 電梯按鈕電梯按鈕 電梯問題的第一個約束條件描述了電梯按鈕的行電梯問題的第一個約束條件描述了電梯按鈕的行 為，現(xiàn)在復(fù)述一下這個約束條件。為，現(xiàn)在復(fù)述一下這個約束條件。 4.3.2 例子例子 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 36 第4章形式語言剖析 第一條約束第一條約束C1C1：每部電梯有：每部電梯有mm個按鈕，每層對應(yīng)一個按鈕，每層對應(yīng)一 個按鈕。當(dāng)按下一個按鈕時該按鈕個按鈕。當(dāng)按下一個按鈕時

54、該按鈕 指示燈亮，指示電梯移往相應(yīng)的樓指示燈亮，指示電梯移往相應(yīng)的樓 層。當(dāng)電梯到達(dá)指定的樓層時，按層。當(dāng)電梯到達(dá)指定的樓層時，按 鈕將熄滅。鈕將熄滅。 用用PetriPetri網(wǎng)表達(dá)電梯按鈕的規(guī)格說明時，在網(wǎng)表達(dá)電梯按鈕的規(guī)格說明時，在PetriPetri網(wǎng)網(wǎng) 中還必須設(shè)置其他的位置。電梯中樓層中還必須設(shè)置其他的位置。電梯中樓層f f的按鈕，在的按鈕，在 PetriPetri網(wǎng)中用位置網(wǎng)中用位置EBfEBf表示表示(1fm)(1fm)。在。在EBfEBf上有一個權(quán)上有一個權(quán) 標(biāo)，就表示電梯內(nèi)樓層標(biāo)，就表示電梯內(nèi)樓層f f的按鈕被按下了。的按鈕被按下了。 西安電子科技大學(xué)計算機學(xué)院 - Sch

55、ool of Computer Science & Engineering, Xidian University, China 37 第4章形式語言剖析 電梯按鈕只有在第一次被按下時才會由暗變亮，電梯按鈕只有在第一次被按下時才會由暗變亮， 以后再按它則只會被忽略。以后再按它則只會被忽略。 下圖的下圖的PetriPetri網(wǎng)準(zhǔn)確描述了電梯按鈕的行為規(guī)律。網(wǎng)準(zhǔn)確描述了電梯按鈕的行為規(guī)律。 首先：假設(shè)按鈕沒有發(fā)亮，顯然在位置首先：假設(shè)按鈕沒有發(fā)亮，顯然在位置EBEBf f上沒有上沒有 權(quán)標(biāo)，從而在存在禁止線的情況下，轉(zhuǎn)換權(quán)標(biāo)，從而在存在禁止線的情況下，轉(zhuǎn)換“EBEBf f被按下被按下” 是允許發(fā)生的

56、。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并是允許發(fā)生的。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并 在在EBEBf f上放置了一個權(quán)標(biāo)，如圖所示。以后不論再按下上放置了一個權(quán)標(biāo)，如圖所示。以后不論再按下 多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換 “EBEBf f被按下被按下”不能再被激發(fā)了，因此，位置不能再被激發(fā)了，因此，位置EBEBf f上的權(quán)上的權(quán) 標(biāo)數(shù)不會多于標(biāo)數(shù)不會多于1 1。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 38 第4

57、章形式語言剖析 假設(shè)電梯由假設(shè)電梯由g g層駛向?qū)玉傁騠 f層，因為電梯在層，因為電梯在g g層，如圖所層，如圖所 示，位置示，位置FgFg上有一個權(quán)標(biāo)。由于每條輸入線上各有一個上有一個權(quán)標(biāo)。由于每條輸入線上各有一個 權(quán)標(biāo)，轉(zhuǎn)換權(quán)標(biāo)，轉(zhuǎn)換“電梯在運行電梯在運行”被激發(fā)，從而被激發(fā)，從而EBEBf f和和FgFg上的上的 權(quán)標(biāo)被移走，按鈕權(quán)標(biāo)被移走，按鈕EBEBf f被關(guān)閉，在位置被關(guān)閉，在位置F Ff f上出現(xiàn)一個新權(quán)上出現(xiàn)一個新權(quán) 標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由g g層駛到層駛到f f層。層。 事實上，電梯由事實上，電梯由g g層移到層移到f f層是需要時間的，為處理層是需

58、要時間的，為處理 這個情況及其他類似的問題這個情況及其他類似的問題( (例如，由于物理上的原因例如，由于物理上的原因 按鈕被按下后不能馬上發(fā)亮按鈕被按下后不能馬上發(fā)亮) )，PetriPetri網(wǎng)模型中必須加入網(wǎng)模型中必須加入 時限。時限。 也就是說，在標(biāo)準(zhǔn)也就是說，在標(biāo)準(zhǔn)PetriPetri網(wǎng)中轉(zhuǎn)換是瞬時完成的，而網(wǎng)中轉(zhuǎn)換是瞬時完成的，而 在現(xiàn)實情況下就需要時間控制在現(xiàn)實情況下就需要時間控制PetriPetri網(wǎng)，以使轉(zhuǎn)換與非零網(wǎng)，以使轉(zhuǎn)換與非零 時間相聯(lián)系。時間相聯(lián)系。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xi

59、dian University, China 39 第4章形式語言剖析 2. 2. 樓層按鈕樓層按鈕 在第二個約束條件中描述了樓層按鈕的行為。在第二個約束條件中描述了樓層按鈕的行為。 第二條約束第二條約束C2C2：除第一層與頂層之外，每個樓層都有：除第一層與頂層之外，每個樓層都有 兩個按鈕，一個要求電梯上行，另一兩個按鈕，一個要求電梯上行，另一 個要求電梯下行。個要求電梯下行。 這些按鈕在按下時發(fā)亮，當(dāng)電梯這些按鈕在按下時發(fā)亮，當(dāng)電梯 到達(dá)該層并將向指定方向移動時，相到達(dá)該層并將向指定方向移動時，相 應(yīng)的按鈕才會熄滅。應(yīng)的按鈕才會熄滅。 在在PetriPetri網(wǎng)中樓層按鈕用位置網(wǎng)中樓層按鈕用

60、位置FBfFBfu u和和FBfFBfd d表示，分表示，分 別代表別代表f f樓層請求電梯上行和下行的按鈕。樓層請求電梯上行和下行的按鈕。 底層的按鈕為底層的按鈕為FB1FB1u u，最高層的按鈕為，最高層的按鈕為FBmFBmd d，中間，中間 每一層有兩個按鈕每一層有兩個按鈕FBfFBfu u和和FBfFBfd d(1 (1f fm)m)。 西安電子科技大學(xué)計算機學(xué)院 - School of Computer Science & Engineering, Xidian University, China 40 第4章形式語言剖析 圖圖4.11 Petri網(wǎng)表示樓層按鈕網(wǎng)表示樓層按鈕 西安電