model-checking - デッドロック チェックと範囲外配列ルックアップの比較 Uppaal

Question

A[] not deadlockモデルの検証ツールでクエリを実行すると、検証がエラーで停止します。

エラーのため、検証は中止されました。ほとんどの場合、これは範囲外の割り当てまたは範囲外の配列ルックアップが原因です。

これは、「範囲外の割り当てまたは範囲外の配列ルックアップ」が発生するまで、私のモデルがデッドロックフリーであることを暗黙のうちに意味しますか?

Answer 1

クエリに応答できる場合、UPPAAL が状態空間を検索し続けることは意味がありません。したがって、UPPAAL が検索できた状態空間の部分にはデッドロックがないと考えてよいと思います。

複数のトレースを介してエラー状態に到達する可能性がありますが、それはモデルに依存することを覚えておいてください。

このエラーが発生する理由はすでにわかっているようです。このエラー状態に陥らないようにするガード!willCauseError()をモデルに追加することで、修正を試みることができます。ただし、それ自体がデッドロックを引き起こす可能性があります。それを避けるために、反対のガードを使用して、関連する場所からそれ自体への遷移を追加できますwillCauseError()。これにより、プログラムはデッドロックではなく強制的にライブロックになります。