iT邦幫忙

2021 iThome 鐵人賽

DAY 17
1
自我挑戰組

後端工程師與圖的修練系列 第 17

有限狀態過程 Finite State Process

有限狀態過程 (FSP, Finite State Process) 是有限狀態機的一種表達方式,本篇文章提及關於 Concurrency 透過 FSP 建模的介紹。

在前面幾個章節雖然有介紹過有限狀態機,但希望再繼續介紹關於有限狀態機的內容。

首先要先介紹本篇文章使用 LTSA - Labelled Transition System Analyser (https://www.doc.ic.ac.uk/ltsa/) 來進行有限狀態機圖形的建模,這套工具也有簡易操作和動畫效果。

https://ithelp.ithome.com.tw/upload/images/20210927/20092753bxrnvMeGxx.png

將寫完的 code 做驗證,可以透過下述步驟看見結果:

https://ithelp.ithome.com.tw/upload/images/20210927/20092753jpYXuJpEiJ.png

以上範例來自於 [1],經過中文解釋後,現在要描述一個可以給多個學生共用印表機的 Concurrent Process,其中參數是印表機紙閘最大數量有三張,不管幾個學生在一個補紙週期之前,最多可以印三份文件; 如果紙張數量為零,就需要重新填充。

以上狀態看起來可以用狀態描述:

const MIN_SHEET_COUNT	=	1 // 最小紙閘數量
const MAX_SHEET_COUNT	=	3 // 最大閘數量
range DOC_COUNT		=	MIN_SHEET_COUNT .. MAX_SHEET_COUNT // 文件 = 1~3 (A, B, C 三種不同的文件)
range SHEET_STACK	=	0 .. MAX_SHEET_COUNT // 剩餘數量堆疊

// 印表機    剩餘紙閘數量      最大紙閘數量           開始        剩餘[最大紙閘數量]狀態的印表機
PRINTER(SHEETS_AVAILABLE = MAX_SHEET_COUNT) =  ( start -> PRINTER_AVAILABLE[MAX_SHEET_COUNT]),
  // 剩餘 [目前剩餘數量: 剩餘數量堆疊] 狀態的印表機
  PRINTER_AVAILABLE[sheets_available: SHEET_STACK] =
    //         剩餘數量    > 0 
    if   (sheets_available > 0)
           // 獲得   指定要印出[DOC_COUNT 1~3]哪一份文件  ->  釋放文件   -> 剩餘[目前剩餘數量 - 1]狀態的印表機
      then (acquire -> print[DOC_COUNT] -> release -> PRINTER_AVAILABLE[sheets_available - 1])
           // 印不出文件  請填充紙閘      釋放文件         剩餘[最大紙閘數量]狀態的印表機
      else (empty -> refill_printer -> release -> PRINTER_AVAILABLE[MAX_SHEET_COUNT]).

https://ithelp.ithome.com.tw/upload/images/20210927/20092753pmHut6wNXq.png

編譯後可以得到圖形,也可以播放動畫:

https://ithelp.ithome.com.tw/upload/images/20210927/200927534QvJ80Q2rD.png

可以看見一開始狀態按下已經打勾的 start 後,會跳到 acquire ,再按一次會出現 printer 1, 2, 3,並且這三個文件的狀態可以任意切換,這個印紙的步驟重複三次,就會進入到 empty 階段,沒有紙,此時做 refill 重新填紙,狀態就會回到 1:

https://ithelp.ithome.com.tw/upload/images/20210927/20092753aVbu4VqLSg.png

這是一整個印表機的狀態流,如果細看學生的狀態流,也可以讓印表機跟學生狀態同時進行動畫:

https://ithelp.ithome.com.tw/upload/images/20210927/200927537nShFw1VyW.png

每次狀態一變化,就可以切換學生跟印表機的 Draw 去看目前的狀態在哪邊,只要 Edit 的取名兩邊都一致就好。

const MIN_SHEET_COUNT	=	1 // 最小紙閘數量
const MAX_SHEET_COUNT	=	3 // 最大閘數量
range DOC_COUNT		=	MIN_SHEET_COUNT .. MAX_SHEET_COUNT // 文件 = 1~3 (A, B, C 三種不同的文件)
range SHEET_STACK	=	0 .. MAX_SHEET_COUNT // 剩餘數量堆疊

// 印表機    剩餘紙閘數量      最大紙閘數量           開始        剩餘[最大紙閘數量]狀態的印表機
PRINTER(SHEETS_AVAILABLE = MAX_SHEET_COUNT) =  ( start -> PRINTER_AVAILABLE[MAX_SHEET_COUNT]),
  // 剩餘 [目前剩餘數量: 剩餘數量堆疊] 狀態的印表機
  PRINTER_AVAILABLE[sheets_available: SHEET_STACK] =
    //         剩餘數量    > 0 
    if   (sheets_available > 0)
           // 獲得   指定要印出[DOC_COUNT 1~3]哪一份文件  ->  釋放文件   -> 剩餘[目前剩餘數量 - 1]狀態的印表機
      then (acquire -> print[DOC_COUNT] -> release -> PRINTER_AVAILABLE[sheets_available - 1])
           // 印不出文件  請填充紙閘      釋放文件         剩餘[最大紙閘數量]狀態的印表機
      else (empty -> refill_printer -> release -> PRINTER_AVAILABLE[MAX_SHEET_COUNT]).


// 學生    要印的文件   3 個       先印第 1 份
STUDENT(DOCS_TO_PRINT = 3) =  PRINT[0],
//  印 第幾份文件 1 ~ 要印的文件數量
PRINT[doc_count: 0 .. DOCS_TO_PRINT] = (
// 如果   文件數量 小於  要印的文件數量
  when (doc_count < DOCS_TO_PRINT) 
   // 獲得印出的文件      釋放       下一個要列印的文件數量是目前第幾張 + 1
    acquire -> print -> release -> PRINT[doc_count + 1] |
// 如果  第幾分文件數量 = 要印的文件數量
  when (doc_count == DOCS_TO_PRINT)
  // 結束 
    terminate -> END ).

文章補充至此,LTS Analyzer 是一個很酷的工具,可以幫你檢視或驗證目前的併發模型,還可以逐一檢查每一個相同狀態的模型上在做什麼。

References:
[1] https://betterprogramming.pub/building-better-concurrency-finite-state-processes-and-modeling-processes-ea0a06b8d529
[2] https://zh.wikipedia.org/wiki/%E6%9C%89%E9%99%90%E7%8A%B6%E6%80%81%E6%9C%BA
[3] https://www.doc.ic.ac.uk/ltsa/


上一篇
UML 圖摘要
下一篇
EPC 事件驅動圖
系列文
後端工程師與圖的修練31

尚未有邦友留言

立即登入留言