Missing language reference for queries such as "simulate" "strategy" and "control"

[yrke]

[11/13 5:54 PM] Martijn Goorden - In the paper 'Uppaal Stratego' from David et al. in TACAS.2015 (DOI: 10.1007/978-3-662-46681-0_16) has an overview of different queries in Table 4. I have no idea whether this overview is complete.

[magoorden]

The requirement specification page contains now much more information on the queries that are possible. When I was reading the Uppaal TIGA manual, I noticed that the query E<> control : phi was mentioned (Section 3.3). This query is possible in Uppaal Stratego, but I don't think the current documentation 'allows' for this query.

[magoorden]

Another issue is that once you have synthesized a strategy, for example with strategy Save = A[] !system.unsafe, you can use the strategy in regular symbolic model checking queries, like A[] !system.unsafe under Save. The current requirement specification page states that this under keyword can only be used if the query starts with strategy <name> = . No symbolic query SymbQuery has the option under.

[magoorden]

The BNF for loadStrategy did not allow it to be names, i.e., the query strategy name = loadStrategy... is not allowed according to the documentation.