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

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

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

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

以上範例來自於 [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]).

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

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

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

每次狀態一變化，就可以切換學生跟印表機的 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/