共有変数やイベント同期を基本相互作用とするデッドロック発見器（並行合成器）を作ってきましたが，第3の選択肢としてアクターモデルを考えたいと思います．アクターモデルは非同期通信なので，仮にバグがあってもメッセージプールが無限に膨れ上がるだけでデッドロックしないことがあります．そこでデッドロック発見器を目指すのはやめて，状態の同一性判定もやめて，単なる並行合成器にしてみました．可視化はいつものとおりです．
プログラムは github.com に置きました．
例として分散システムにおける合意アルゴリズムを記述してみました．私は分散システムについてはほとんど何も知りません．下記リファレンスを参考にしました．Isabelle のモデルを一部改変して並行合成器にかけてみただけです．