有限状态过程 Finite State Process

有限状态过程 (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/