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

Bug 673

Summary: symbolic queries on hybrid models should fail with an error
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: minor    
Priority: P5    
Version: 4.1.23   
Hardware: All   
OS: All   
Architecture:
Attachments: hybrid model breaking symbolic analysis

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.