java - ispin ヘルプ (LTL 式の到達不能状態)

Question

ispin でシステムをモデル化しましたが、LTL 式を使用してシステムを検証しようとすると、次のような到達不能エラーが見つかりました

unreached in claim l0
    _spin_nvr.tmp:8, state 9, "(!((getReciept&&getCard)))"
    _spin_nvr.tmp:10, state 11, "-end-"
    (2 of 11 states)

私のLTL式は

ltl0{[]((cardeject && getCash)  ->   <>(getReciept && getCard))}

Answer 1

エラーではなく警告です。これは、パーツ(cashDispensed && !continueTransaction)が真にならない可能性があるためです。したがって、式は自明です。

iSpin で「到達不能コードを報告する」チェックボックスをオフにすることで、警告を無効にすることができます。