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 中的“报告无法访问的代码”复选框来禁用警告。