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

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: 2020-04-28 15:19 CEST (History)
1 user (show)

See Also:
Architecture:

Attachments
Model (1.56 KB, text/xml)
2019-09-13 13:48 CEST, Danny Bøgsted Poulsen 		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 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.