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
Add an attachment (proposed patch, testcase, etc.)

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.