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

Bug 72 - Engine crash when negating deadlock
Summary: Engine crash when negating deadlock
Status: CLOSED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.4.2
Hardware: All All
: P1 major
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2003-12-08 10:48 CET by Ulrik Nyman
Modified: 2005-02-18 11:02 CET (History)
0 users

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
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.