graph - TLA+ 状態グラフを視覚化する方法

Question

私は新しいTLA+ユーザーです。TLAツールボックスを使用すると、モデル チェックの完了後に状態グラフを視覚化できると読みました。

そのためには、私が行ったようにドットをインストールする必要があります。しかし、ビジュアライゼーションを起動する方法がわかりませんでした。GUI を使用して購入できますか、それとも専用のコマンド ラインを使用する必要がありますか?

ありがとう

Answer 1

状態グラフを視覚化するには、次のことを行う必要があります。

1. マシンにGraphvizをインストールします (既に行っています)。
2. TLA+ Toolboxローカル マシン上の実行可能ファイルの場所を指すように設定dotします: [設定] → [TLA+ 設定] → [PDF ビューアー] → [ドット コマンドを指定]。(私のマシンでは、自作でgraphvizをインストールしました。私のコマンドは/usr/local/bin/dot.
3. TLC モデル: 追加の TLC オプション → TLC オプション → モデル チェックの完了後に状態グラフを視覚化する (このボックスをオンにします)

モデルを実行するState Graphと、状態グラフの Graphviz 視覚化を含むタブが表示されます。