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

Bug 175 - Segfault when using clock expressions in liveness properties
Summary: Segfault when using clock expressions in liveness properties
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.5.7
Hardware: PC Linux
: P2 major
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2005-07-13 17:08 CEST by Ferdy Hanssen
Modified: 2005-07-13 18:48 CEST (History)
0 users

See Also:
Architecture:


Attachments
Model (3.73 KB, text/xml)
2005-07-13 17:09 CEST, Ferdy Hanssen
Details
Query (780 bytes, text/plain)
2005-07-13 17:09 CEST, Ferdy Hanssen
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Ferdy Hanssen 2005-07-13 17:08:34 CEST
When you verify the accompanying query on the accompanying model (I have trimmed
the model and query a lot from my original, and this one still segfaults).

If I change the value of mx_lost in the model from 1 to 0 the segfault does not
occur.  If I remove the bit "and rec_time == 0" from the query, the segfault
also does not occur.
Comment 1 Ferdy Hanssen 2005-07-13 17:09:03 CEST
Created attachment 48 [details]
Model
Comment 2 Ferdy Hanssen 2005-07-13 17:09:20 CEST
Created attachment 49 [details]
Query
Comment 3 Gerd Behrmann 2005-07-13 17:22:22 CEST
Confirmed.
Comment 4 Gerd Behrmann 2005-07-13 18:48:34 CEST
A fix has been committed to CVS (it was a missing exclamation mark). 

The problem is triggered by expressions over clocks in liveness or leadsto properties.