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

Bug 673 - symbolic queries on hybrid models should fail with an error
Summary: symbolic queries on hybrid models should fail with an error
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.23
Hardware: All All
: P5 minor
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2019-11-06 16:25 CET by Marius Mikučionis
Modified: 2019-11-14 11:56 CET (History)
0 users

See Also:
Architecture:

Attachments
hybrid model breaking symbolic analysis (1.86 KB, text/xml)
2019-11-06 16:25 CET, Marius Mikučionis 		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 Marius Mikučionis 2019-11-06 16:25:04 CET 
Created attachment 338 [details]
hybrid model breaking symbolic analysis

Currently uppaal just goes on to perform symbolic reachability algorithm which almost surely will be incorrect.

The attached example uses "x'==-2" and thus is able to progress beyond the guard "x<-1", but deadlock check concludes that there is a deadlock.