ispin help (unreachable states in LTL formula)

0
votes

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))}
1
javamodel-checkingspinformal-methods
You can use formatting to make the examples readable. – Felix

1 Answers

0
votes

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.