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

Bug 175

Summary: Segfault when using clock expressions in liveness properties
Product: UPPAAL Reporter: Ferdy Hanssen <hanssen>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: major    
Priority: P2    
Version: 3.5.7   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: Model
Query

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.