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