UPPAAL を使用してモデルをセットアップし、ベリファイアを使用してデッドロックをチェックしました。答えは: プロパティが満たされていない. したがって、デッドロックが存在します。
特定の状況におけるすべての変数の状態や現在の値など、デッドロックに関するより詳細な情報を UPPAAL で報告する方法はありますか?
質問する
1758 次
1 に答える
1
はい。UPPAAL でデッドロックを追跡できます。つまり、デッドロックを引き起こしている状態またはパスを見つけることができます。オプション --> 診断トレース --> 最速に移動します。診断トレースでは、これらのオプション some/fastest/shortest のいずれかを選択できます。最速を選択した後。ベリファイアに移動し、デッドロック ロック プロパティを確認します。シミュレーターに移動した後、「はい」を選択して新しいトレースをシミュレーションに保存します。プロパティを満足できないものにしている新しいストア トレースが表示されます。それが役立つことを願っています
于 2016-11-29T07:34:55.190 に答える