| Summary: | optimization query breaks with time-lock where there isn't one | ||
|---|---|---|---|
| Product: | UPPAAL Stratego | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Peter Gjøl Jensen <pgj> |
| Status: | ASSIGNED --- | ||
| Severity: | blocker | CC: | fshsho7, mk09, pgj |
| Priority: | P5 | ||
| Version: | 4.1.20-3 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: |
stratego model demonstrating the problem (see the 1st query)
Initial state sometimes fails for optimising query with time-locked error |
||
Created attachment 319 [details]
Initial state sometimes fails for optimising query with time-locked error
This model sometimes fails optimisation queries, and it fails for all version of stratego (4.1.20-*).
I have tried queries on the form E[] time < 10, so see if I can find live locks, but have not found any.
There seems to be an issue with CSDecorator;
CSDecorator.maxDelay() returns inf even when CSDecorator.zeroDelay() returns true.
The problem can be fixed by replacing the maxDelay() implementation with
double maxDelay() const { return cannotDelay ? 0 : max; }
The method is only called in very few places, so I belive this fix is sound.
*** Bug 678 has been marked as a duplicate of this bug. *** @pgj the fix seems to have been applied, but the issue is still there. stratego-5 does not show this issue. stratego-6 and stratego-7 complains |
Created attachment 299 [details] stratego model demonstrating the problem (see the 1st query) The attached model demonstrates the problem. The problem does not appear in 4.1.20-2 version and it is not manifest for simple simulations. This is specific to optimization query in 4.1.20-3, something is odd with evaluating possible successors when processing optimization query.