When checking for deadlock the two following propeties works fine: A[] not deadlock E<> deadlock The following two propeties crashes the engine. A[] deadlock E<> not deadlock They both first report an error stating: CAUGHT EXCEPTION: Negation of the deadlock expression has not been implemented. The real problem is that a "Fatal error: Broken pipe" is reported when trying to check the next propety or when subsequently trying to use the simulator.
As documented in the build-in help system, these alternative uses of the deadlock state property are not supported in version 3.4.2, and thus the server throws an exception indicating that it is not supported. In order to fix this, I have implemented handling of negated deadlock properties. These should now work in both the liveness checker and the reachability checker.