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

Update query BNF #21

Closed magoorden closed 2 years ago

magoorden commented 2 years ago

The BNFs of the different types of queries (https://docs.uppaal.org/language-reference/requirements-specification/) were not reflecting accurately what is and is not accepted by the parser.

Using parser.y I have updated the BNFs to reflect what is possible.

Two points are open that need to be resolved before we can actually merge it:

  1. The syntax of partially observable TIGA-based queries is unclear. In the parser it is defined as '{' ExpressionList '}' 'control:' Goal Subjection, but when I try to run this query I get an error message stating "Clock lower bound must be weak and upper bound strict.", so not any ExpressionList is accepted. It would be useful to state these additional restrictions here in the documentation, but I don't know what they are.
  2. Almost all queries can be subjected to a strategy except a TimeEfficientGameQuery query. Therefore, individual queries have Subjection instead of query categories in general. This leads to a lot of Subjections scattered around. Any suggestion for a better way to notate this is welcome.
magoorden commented 2 years ago

@mikucionisaau I asked Kim whether he could remember how for the above point 1 the expression list should look like. He was not sure. Do you know it?

magoorden commented 2 years ago

The syntax of the simulation query has changed in Uppaal Stratego 10 beta 2. The parser.y in utap does not reflect this (and maybe other changes) yet.

mikucionisaau commented 2 years ago

@yrke I am not authorized to merge :-(