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

Bug 640 - SMC reports Lookup of a state outside the strategy when run under a tiga strategy
Summary: SMC reports Lookup of a state outside the strategy when run under a tiga stra...
Status: ASSIGNED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Linux
: P5 normal
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2017-08-19 16:27 CEST by Jakob Haahr Taankvist
Modified: 2019-01-25 12:05 CET (History)
0 users

See Also:
Architecture:

Attachments
The model originally submitted by Jin Hyun Kim <jhkim07@gmail.com> (6.25 KB, text/xml)
2017-08-19 16:27 CEST, Jakob Haahr Taankvist 		Details
A very simple model which also shows the problem (1.89 KB, text/xml)
2017-08-19 16:28 CEST, Jakob Haahr Taankvist 		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 Jakob Haahr Taankvist 2017-08-19 16:27:04 CEST 
Created attachment 316 [details]
The model originally submitted by Jin Hyun Kim <jhkim07@gmail.com>

In the two models attached the second query reports Lookup of a state outside the strategy. 

A workaround is to change the first query to the equivalent: 

strategy TonyBound = control: A[] (isUpdated[1] > 0 && isUpdated[2] > 0 && isUpdated[3] > 0 ) || time <= 20
Comment 1 Jakob Haahr Taankvist 2017-08-19 16:28:54 CEST 
Created attachment 317 [details]
A very simple model which also shows the problem