-
Notifications
You must be signed in to change notification settings - Fork 16
Open
Description
As seasoned Uppaal users, we know that queries can be edited in the Query box. For new users (for example students), this is not trivial, especially when you have a model without any queries at all.
The documentation is not crystal clear on where to insert/edit the queries. Currently, editing queries is mentioned in a parenthetical clause in the paragraph on selecting queries:
Queries are selected and de-selected using the mouse alone, or in combination with the Shift or the Control key of the keyboard (use the Shift key to (de-)select a range of entries and the Control key to (de-)select single entries).
The first selected requirement and its comment is always shown in the two editor fields named Query and Comment, where they may be edited.
New users can easily miss this crucial piece of information.
Metadata
Metadata
Assignees
Labels
No labels