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

ispin help (unreachable states in LTL formula)