【文章內(nèi)容簡介】 rt Start Ringing T1 Starting/Stopping of the Timers is not visible on STD. 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 36 Finite State Machines (FSMs) 四、 Moore 機(jī) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 37 Moore FSM ?前面討論的 FSM和非確定 FSM，可以看成僅接收輸入并發(fā)生狀態(tài)改變，但無任何輸出的自動機(jī)器。 ?實際上生活中的許多有限狀態(tài)系統(tǒng)對于不同的輸入信號，除內(nèi)部狀態(tài)不斷改變外，還不斷向系統(tǒng)外部輸出各種信號。 ?具有輸出的自動機(jī)器模型按照輸出的不同分成兩類： ?Moore 機(jī)：輸出與狀態(tài)有關(guān) ?Mealy機(jī)：輸出與狀態(tài)和輸入有關(guān) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 38 Moore FSM: Formal Definition ?Moore FSM is 6tuple: FSM = (S, s0, I, O, ?, ?), where ?S = {s0, s1, …, s n}: 有限狀態(tài)集合。在任一確定時刻，F(xiàn)SM只能處于一個確定的狀態(tài) si。 ?I = {a0, a1, …, a m}: 有限 輸入字符 集合。在任一確定的時刻， FSM只能接收一個確定的輸入 aj。 ?O = {b0, b1, …, b n}: 有限 輸出字符 集合。 ?? ： S ? I ? 2S是狀態(tài)轉(zhuǎn)換函數(shù)，如果在某一確定的時刻， FSM處于某一狀態(tài) si ? S, 并接收一個輸入字符 aj? I，那么下一時刻將處于一個確定的狀態(tài) s180。 = ?(si , aj) ? S。在這里規(guī)定， s = ?(s , ?)， 即對任何狀態(tài) s，當(dāng)讀入空字符 ?時，有很狀態(tài)機(jī)不發(fā)生任何狀態(tài)轉(zhuǎn)移。 ?s0 ? S是初始狀態(tài)， FSM由此狀態(tài)開始接收輸入 ??： S ? O是輸出函數(shù) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 39 Moore 機(jī)： Formal Definition ?Moore機(jī)只是在接收輸入串的過程中不斷改變狀態(tài)，并且在每個狀態(tài)上有字符輸出。例如： ?對于輸入串 {a0, a1, …, a n1}，設(shè)： ? ?(s0 , a0) = s1, ? ?(s1 , a1) = s2, …. ? ?(sn1 , an1) = sn ?這時輸出序列為： ?(s0) ?(s1) … ?(sn1) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 40 Moore 機(jī) vs. 有限狀態(tài)機(jī) ?有限狀態(tài)機(jī)可看做是 Moore機(jī)的一個特例， Why? ?對于任何一個有限狀態(tài)機(jī) M = (S, s0, I, ?, F): ?引入輸出字符集合 O = {0, 1}，并定義 S到 O的映射 ? 為： ?對于 s ? F, ?(s) = 1；對于 s ? F, ?(s) = 0 ?這樣得到一個 Moore機(jī) M?= (S, s0, I, O, ?, ?)，在該 Moore機(jī)中，輸出為 1的狀態(tài)為終結(jié)狀態(tài)，輸出為 0的狀態(tài)即為非終結(jié)狀態(tài)。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 41 Finite State Machines (FSMs) 五、 Mealy 機(jī) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 42 Mealy FSM: Formal Definition ?Mealy FSM is 6tuple: FSM = (S, s0, I, O, ?, ?), where ?S = {s0, s1, …, s n}: 有限狀態(tài)集合。在任一確定時刻，F(xiàn)SM只能處于一個確定的狀態(tài) si。 ?I = {a0, a1, …, a m}: 有限 輸入字符 集合。在任一確定的時刻， FSM只能接收一個確定的輸入 aj。 ?O = {b0, b1, …, b n}: 有限 輸出字符 集合。 ?? ： S ? I ? 2S是狀態(tài)轉(zhuǎn)換函數(shù)，如果在某一確定的時刻， FSM處于某一狀態(tài) si ? S, 并接收一個輸入字符 aj? I，那么下一時刻將處于一個確定的狀態(tài) s180。 = ?(si , aj) ? S。在這里規(guī)定， s = ?(s , ?)， 即對任何狀態(tài) s，當(dāng)讀入空字符 ?時，有很狀態(tài)機(jī)不發(fā)生任何狀態(tài)轉(zhuǎn)移。 ?s0 ? S是初始狀態(tài)， FSM由此狀態(tài)開始接收輸入 ??： S ? I ? O是輸出函數(shù) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 43 Moore 機(jī)： Formal Definition ?Mealy機(jī)只是在接收輸入串的過程中不斷改變狀態(tài)，并且字符輸出與當(dāng)前狀態(tài)有關(guān)。例如： ?對于輸入串 {a0, a1, …, a n1}，設(shè)： ? ?(s0 , a1) = s1, ? ?(s1 , a2) = s2, …. ? ?(sn1 , an1) = sn ?這時輸出序列為： ?(s0, a0) ?(s1 , a1) … ?(sn1 , an1) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 44 Mealy 機(jī) vs. Moore機(jī) ? Moore機(jī)可看做是 Mealy機(jī)的一個特例， Why? ?對于任何一個 Moore機(jī) M = (S, s0, I, O, ?, ?) : ?設(shè)當(dāng)輸入串為 {a0, a1, …, a n1}時，其輸出序列為： ?(s0) ?(s1) … ?(sn)，其中 si 和 ai1 滿足： ?(si1, ai1) = si， 1? i ?n ?引入： S ? I 到 O的映射 ??： ? ??(si1, ai1) = ?{?(si1, ai1)} = ? (si), 1? i ?n ?這樣得到一個 Mealy機(jī) M?= (S, s0, I, O, ?, ??)，對于輸入串 {a0, a1, …, a n1}， Mealy機(jī) M?的輸出為 ??為： ??(s0, a0) ??(s1, a1)… ??(sn1, an1) = ?(s0) ?(s1) … ?(sn1) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 45 Mealy機(jī)： Example ?停止等待協(xié)議： ?設(shè)甲、乙雙方進(jìn)行半雙工通信，甲發(fā)信息幀，乙回送確認(rèn)幀。雙方約定采用停止等待協(xié)議，因此甲方僅需用 1比特來編號。 ?將 0號幀和 1號幀分別記為 [0]和 [1]。 ?當(dāng)收到有差錯的幀時，則丟棄此幀，同時不發(fā)任何應(yīng)答幀。 ?當(dāng)收到無差錯的幀但序號不正確時，要發(fā)確認(rèn)幀，同時要丟棄此幀，不送主機(jī)。 ?我們還假定收方在準(zhǔn)備發(fā)送確認(rèn)幀 ACK時，暫不接收外面發(fā)來的幀。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 46 停止等待協(xié)議：狀態(tài)變遷表 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 47 停止等待協(xié)議：狀態(tài)變遷圖 1 2 3 4 1 2 3 4 等待 準(zhǔn)備發(fā) ACK 準(zhǔn)備發(fā) ACK 準(zhǔn)備發(fā) [0] 準(zhǔn)備發(fā) [1] 期望收 [1] 期望收 [0] 等待 發(fā) [0] 發(fā) [1] 收 [1] 收 [0] 發(fā) ACK 發(fā) ACK 收 ACK 收 ACK 發(fā) ACK 收 [1] 發(fā) ACK 收 [0] 甲方 乙方 超 時 超 時 狀態(tài)符號 狀態(tài)編號 狀態(tài)含義 狀態(tài)變遷 輸入事件 對某些狀態(tài)進(jìn)行了簡化。例如，當(dāng)乙方處于 “ 期望收 [0]”的狀態(tài)時，若收到無差錯的[1]幀，仍然應(yīng)當(dāng)先進(jìn)入 “ 準(zhǔn)備發(fā) ACK”狀態(tài)，然后才發(fā)出 ACK。但這里就將 “ 收 [1]”與“ 發(fā) ACK”合并成為一個事件。 再例如，當(dāng)乙方處于“ 期望收 [1]”的狀態(tài)時，若收到無差錯的 [0]幀，仍然應(yīng)當(dāng)先進(jìn)入 “ 準(zhǔn)備發(fā) ACK”狀態(tài)，然后才發(fā)出 ACK。但這里就將 “ 收 [0]”與 “ 發(fā)ACK”合并成為一個事件。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 48 停止等待協(xié)議：狀態(tài)變遷圖合并 ?前面描述的甲、乙兩方各自的有限狀態(tài)機(jī)實際上并非獨立地工作而是協(xié)調(diào)在一起工作的。如合在一起用一個有限狀態(tài)機(jī)來描述整個系統(tǒng)，將會更加清楚。但這將導(dǎo)致狀態(tài)數(shù)目將大大增加。 Why? ?甲方和乙方的狀態(tài)各有 4個， ?而信道上的狀態(tài)也有 4個 (即：信道上傳送 [0]，傳送 [1]，傳送 ACK，以及出現(xiàn)差錯或幀的丟失 )。 ?這樣將總共有 43=64種狀態(tài)，用狀態(tài)圖很難清楚地表示出來。 ?解決辦法：合并一些狀態(tài) ,即考慮一些次要的細(xì)節(jié) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 49 停止等待協(xié)議：狀態(tài)變遷圖合并 ?狀態(tài)合并： ?甲方的狀態(tài) 1和狀態(tài) 2，狀態(tài) 3和狀態(tài) 4都可以合并， ?乙的狀態(tài) 1和狀態(tài) 4，狀態(tài) 2和狀態(tài) 3也可進(jìn)行合并。 ?信道的狀態(tài)是由其內(nèi)容決定的，例如，如果幀 [0]正在信道上 (即，幀已被分地發(fā)送出去，部分地被接收，但在目的主機(jī)上還未進(jìn)行處理 )，則信道的狀態(tài)為幀[0]。 ?整個系統(tǒng)的狀態(tài)是通信雙方兩個協(xié)議機(jī)和信道的所有狀態(tài)的組合。 用 3個字符 XYZ 表示整個系統(tǒng)的狀態(tài)，其中 ? X = 0或 1，對應(yīng)于甲方準(zhǔn)備發(fā) [0]或 [1](包括發(fā)完后等待ACK的狀態(tài) )； ? Y = 0或 1，對應(yīng)于乙方期望收到 [0]或 [1]； ? Z = 0, 1, A或 ?，對應(yīng)于信道上傳送的是 [0]， [1]， ACK 或出現(xiàn)了差錯 (包括丟失 )。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 50 停止等待協(xié)議：合并后的狀態(tài)變遷圖 變遷 意義 0 幀丟失或幀出錯 1 收 [0]，發(fā) ACK，送主機(jī) 2 收 ACK，發(fā) [1] 3 收 [1]，發(fā) ACK，送主機(jī) 4 收 ACK，發(fā) [0] 5 收 [0]，發(fā) ACK，不送主機(jī) 6 收 [1]，發(fā) ACK，不送主機(jī) 7 超時，發(fā) [0] 8 超時，發(fā) [1] 0 0 0 0 0 0 1 2 3 4 5 6 7 8 8 7 0 0 0 0 1 0 1 1 1 1 0 1 1 0 ? 1 1 ? 0 1 ? 0 0 ? 1 0 A 0 1 A 假設(shè)系統(tǒng)一開始處在 (000)狀態(tài)。這表示甲發(fā)完 [0]，乙期望收到 [0]，而信道上傳送的也是[0]。在無差錯的情況下，系統(tǒng)的狀態(tài)僅在 4個狀態(tài)中循環(huán)：(000)→ (01A)→ (111)→ (10A)→ (000)→ … 。如果信道丟失了幀 [0]，則進(jìn)行從狀態(tài) (000)到狀態(tài)(00)的轉(zhuǎn)換。最終，發(fā)送過程超時 (轉(zhuǎn)換 7)，且系統(tǒng)回到狀態(tài) (000)。確認(rèn)幀的丟失更為復(fù)雜，需要兩種轉(zhuǎn)換： 7和 5，或 8和 6，直到修復(fù)損壞。從理論上講，應(yīng)當(dāng)共有 2?2?4 = 16種不同的狀態(tài)。去掉沒有意義的組合后，還剩下 10種狀態(tài)，而導(dǎo)致狀態(tài)變遷的輸入事件共有 9種 (標(biāo)號 0?8)。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 51 停止等待協(xié)議： Summary ?當(dāng)描述比較復(fù)雜的協(xié)議時，狀態(tài)的數(shù)目將急劇增加，以致很難用它來清晰地描述協(xié)議。 ?例如，如果我們將前面描述的半雙工通信的停止等待協(xié)議改為全雙工通信的停止等待協(xié)議，則其狀態(tài)圖就要復(fù)雜多了 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 52 全雙工通信的停止等待協(xié)議狀態(tài)變遷圖 000 A000 A00 0 0 0 100 A101 A0 A0 010 A01 A01 0 1 0 1 1 1 11 11 A111 A3 + 41 + 208068024 + 60700 73242 + 50800807