Bug 666 - Erroneous time-lock
Summary: Erroneous time-lock
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.20-5
Hardware: PC Linux
: P5 normal
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2019-09-13 13:48 CEST by Danny Bøgsted Poulsen
Modified: 2019-12-18 14:44 CET (History)
0 users

See Also:
Architecture:


Attachments
Model (1.56 KB, text/xml)
2019-09-13 13:48 CEST, Danny Bøgsted Poulsen
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Danny Bøgsted Poulsen 2019-09-13 13:48:46 CEST
Created attachment 335 [details]
Model

Runnig the query
 strategy opt = minE (Process.timer) [<=50]: <> Process.STOP on the attached model results in the message 
"
State
( Process._id0 )
[ Process.timer=3.18742806482673 Process.c=3.18742806482673 ]
Process.loc=0 
is time-locked."


There shouldn't be a time-lock in the model in that particular state. There is no time-invariant on the location.
Comment 1 Marius Mikučionis 2019-09-30 12:17:34 CEST
This seems to be fixed on the working branch, so the fix is going to be released soon with stratego-6
Comment 2 Marius Mikučionis 2019-12-18 14:44:02 CET
The issue does not occur on this model using stratego-7, so I am closing.