| Summary: | Guarded, not enabled edge with urgent channel enforces urgency | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Peter Gjøl Jensen <pgj> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | enhancement | CC: | adavid |
| Priority: | P5 | ||
| Version: | 4.1.20 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: | Model provocating the error | ||
Uppaal 4.1.19 implements urgency on all edges. Stratego 4.1.20-4 does not. |
Created attachment 293 [details] Model provocating the error Even though a warning is produced, the engine accepts the attached model, and produces erroneous results. It seems that urgency is enforced on all edges, even though it is only present on one - which is not enabled due to a guard. (Has been fixed in development branch stratego_2016_ndiscrete)