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

Bug 632 - resulting strategy does not depend on the timing
Summary: resulting strategy does not depend on the timing
Status: ASSIGNED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.20-3
Hardware: All All
: P5 critical
Assignee: Peter Gjøl Jensen
URL:
Depends on:
Blocks:
 
Reported: 2017-04-07 10:44 CEST by Marius Mikučionis
Modified: 2017-04-07 10:45 CEST (History)
0 users

See Also:
Architecture:

Attachments
model showing the issue (3.28 KB, text/xml)
2017-04-07 10:44 CEST, Marius Mikučionis 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2017-04-07 10:44:46 CEST 
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.
Comment 1 Marius Mikučionis 2017-04-07 10:45:18 CEST 
I delegate this to Peter.