The following program is not correctly handled by epispin on all lines.
They are accepted by spin.
In the plf-line the complaint is that np_ can only be handled inside a never claim.
Such is of course true according to the book, but as ltl-claims are translated into never claims, np_ should be allowed in ltl-claims too.

ltl p1c {_pid == 1}

ltl pld {_last == 1}

ltl ple {_nr_pr == 1}

ltl plf { np_ == 1}

init{skip;}

Submitted by Kees Pronk on 4 November 2011 at 20:03

Fixed