| Summary: | resulting strategy does not depend on the timing | ||
|---|---|---|---|
| Product: | UPPAAL Stratego | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Peter Gjøl Jensen <pgj> |
| Status: | ASSIGNED --- | ||
| Severity: | critical | ||
| Priority: | P5 | ||
| Version: | 4.1.20-3 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | model showing the issue | ||
I delegate this to Peter. |
Created attachment 311 [details] model showing the issue The following strategy: strategy Opt = minE (b) [<=1] : <> Proc.END || y>=1 should depend on concrete timing when Proc arrives at the decision and at least sometimes choose A.