search

UPPAALModelChecker / docs.uppaal.org

This repo contains the official UPPAAL documentation published on https://docs.uppaal.org
https://docs.uppaal.org
1 stars 13 forks source link

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

Open yrke opened 3 years ago

yrke commented 3 years ago

[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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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.