■

Uppaalを使い続ける。良い所は次の動作の選択肢が明示的に示されるところ。SPINにはそういう概念は特になかったはず…あんまり覚えていないけど。悪いところはGuardの中で他のプロセスの状態を参照できないところ。これは本当に意味がわからない。オートマトンを図示出来ても、他のプロセスからその状態がわからないのであれば、同等の効果を得るために変数に状態を代入しなければなりません。結局変数に状態を代入するのであれば、図には一体何の意味があるのでしょうか。