Thread Life Cycle

状態遷移のチェックだってできるぜ。
といいたいところだが、まぁ簡単に図を書くくらいなら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 {}