ltl p5: [] (((! (invariantPrecond)) || (X ((! (isPsystemStep)) U ((invariantPostcond) && (isPsystemStep))))) || (! (isPsystemStep)))
spin: cannot find trail file