Bug 666 - Erroneous time-lock
Summary: Erroneous time-lock
Status: NEW
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-09-13 13:48 CEST (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.