Search code examples
javamodel-checkingspinformal-methods

ispin help (unreachable states in LTL formula)

I have modeled a system in ispin and when trying to verify the system using LTL formulas I found unreachable error like

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

my ltl formula was 

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

  • It's a warning, not an error. This is because the part (cashDispensed && !continueTransaction) might never become true. So, the formula is trivially true.

    You can disable the warning by unchecking the checkbox "report unreachable code" in iSpin.