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

Bug 620 - optimization query breaks with time-lock where there isn't one
Summary: optimization query breaks with time-lock where there isn't one
Status: ASSIGNED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.20-3
Hardware: All All
: P5 blocker
Assignee: Peter Gjøl Jensen
URL:
: 678 (view as bug list)
Depends on:
Blocks:
 
Reported: 2016-09-29 10:03 CEST by Marius Mikučionis
Modified: 2020-10-13 13:53 CEST (History)
3 users (show)

See Also:
Architecture:


Attachments
stratego model demonstrating the problem (see the 1st query) (11.87 KB, text/xml)
2016-09-29 10:03 CEST, Marius Mikučionis
Details
Initial state sometimes fails for optimising query with time-locked error (27.73 KB, text/xml)
2018-02-05 13:10 CET, Martin Kristjansen
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2016-09-29 10:03:11 CEST
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.
Comment 1 Martin Kristjansen 2018-02-05 13:10:38 CET
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.
Comment 2 Peter Gjøl Jensen 2018-03-09 18:32:53 CET
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.
Comment 3 Fatima 2020-04-29 10:02:57 CEST
*** Bug 678 has been marked as a duplicate of this bug. ***
Comment 4 Marius Mikučionis 2020-10-13 13:42:13 CEST
@pgj the fix seems to have been applied, but the issue is still there.
Comment 5 Marius Mikučionis 2020-10-13 13:53:46 CEST
stratego-5 does not show this issue.
stratego-6 and stratego-7 complains