状態遷移のチェックだってできるぜ。
といいたいところだが、まぁ簡単に図を書くくらいならLTSAと同じだなぁ、
というところをやってみる。
/* LTSAのマネ.Thread Life Cycle THREAD = CREATED, CREATED = (start -> RUNNABLE |stop -> TERMINATED), RUNNING = ({suspend,sleep} ->NON_RUNNABLE |yield ->RUNNABLE |{stop, end} ->TERMINATED |run ->RUNNING), RUNNABLE = (suspend ->NON_RUNNABLE |dispatch ->RUNNING |stop ->TERMINATED), NON_RUNNABLE = (resume ->RUNNABLE |stop ->TERMINATED), TERMINATED = STOP. */ one sig CREATED { start: RUNNABLE, stop: TERMINATED } one sig RUNNING { suspend,sleep: NON_RUNNABLE, yield: RUNNABLE, stop,end: TERMINATED, run_: RUNNING } one sig RUNNABLE { suspend: NON_RUNNABLE, dispatch: RUNNING, stop: TERMINATED } one sig NON_RUNNABLE { resume: RUNNABLE, stop: TERMINATED } one sig TERMINATED {} run {}