| Summary: | symbolic queries on hybrid models should fail with an error | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | 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 | ||
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.