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