This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 72

Summary: Engine crash when negating deadlock
Product: UPPAAL Reporter: Ulrik Nyman <ulrik>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: major    
Priority: P1    
Version: 3.4.2   
Hardware: All   
OS: All   
Architecture:

Description Ulrik Nyman 2003-12-08 10:48:58 CET 
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.
Comment 1 Gerd Behrmann 2003-12-08 19:59:01 CET 
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.