0

我在 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))}
4

1 回答 1

0

这是一个警告,而不是错误。这是因为这部分(cashDispensed && !continueTransaction)可能永远不会成为真的。所以,这个公式是微不足道的。

您可以通过取消选中iSpin 中的“报告无法访问的代码”复选框来禁用警告。

于 2015-08-05T11:59:49.937 回答