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

Bug 640

Summary:	SMC reports Lookup of a state outside the strategy when run under a tiga strategy
Product:	UPPAAL Stratego	Reporter:	Jakob Haahr Taankvist <jht>
Component:	Engine	Assignee:	Marius Mikučionis <marius>
Status:	ASSIGNED ---
Severity:	normal
Priority:	P5
Version:	unspecified
Hardware:	PC
OS:	Linux
Architecture:
Attachments:	The model originally submitted by Jin Hyun Kim <jhkim07@gmail.com> A very simple model which also shows the problem

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