|Summary:||Segfault when using clock expressions in liveness properties|
|Product:||UPPAAL||Reporter:||Ferdy Hanssen <hanssen>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
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 3 Gerd Behrmann 2005-07-13 17:22:22 CEST
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.