SPINモデルチェッカーでは最大探索深度を小さくするには小さすぎますか？考えられる理由は何でしょうか？

Question

私のモデル検証をしながら私は、コンパイル文字列が

tesTdma.pml

-aスピン

最大検索深さが小さすぎる、 奥行= 9999の状態

で、このエラーを取得していますこのエラーの原因を理解していない。誰かが1.1.4とSPIN 6.4.7

Answer 1

のverこの使用IsPinを出くわしたのは、検索深さが制限されていることが表示されます、そしてあなたは、生成、検証panに適切なオプションを渡すことで、拘束を増やす必要があります。

-b

有界検索モードは、トリガおよびエラー証跡、検索の深さを超えてそれをエラーになり

-mN Nステップ（デフォルトN = 10000）に

セット最大探索深

man page of pan、 またman page of spin参照：

-run

はpan.cで検証ソースコードを生成（-aのように）、すぐに検証者をコンパイルして実行します。 -run引数はオプションが-[ODUE]またはランタイムフラグ（他のすべてのオプション）として検証者に開始（コンパイラに渡されます。自分自身をスピンするオプションが-run引数を先行すべき。

-runオプションがある従うオプションあなたが代わりに個別の、spinへの呼び出しを介してpanにオプションを渡したい場合に便利

また、スライド1からthese slidesで27ページ：

SPINは深さの境界が完全な状態空間を検索できないことを知らせるために“error: max search depth too small”を表示します。