ltl p1: ((((ms[2].x[25]==0)) && ((ms[2].x[1]==0))) || (! (isPsystemStep))) U ((((ms[2].x[25]==1)) && ((ms[2].x[1]==0))) && (isPsystemStep))
spin: cannot find trail file