Skip to content

Commit

Permalink
Merge a note on nested quantifiers (pr #57)
Browse files Browse the repository at this point in the history
Added a note on nested quantifiers
  • Loading branch information
mikucionisaau committed May 22, 2024
2 parents 46c7230 + 1fdbf74 commit d3524ee
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion content/language-reference/query-semantics/symb_queries.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ An _eventually_ property `A<> p` can be expressed as the _potentially_ property

The syntax `p --> q` denotes a leads to property meaning that whenever `p` holds eventually `q` will hold as well. Since UPPAAL uses timed automata as the input model, this has to be interpreted not only over action transitions but also over delay transitions.

A _leads to_ property `p --> q` can be expressed as the property `A[] (p imply A<> q)`.
A _leads to_ property `p --> q` can be expressed as the property `A[] (p imply A<> q)` (note that the leads-to property is a special case and in general nested quantifiers are not supported).



Expand Down

0 comments on commit d3524ee

Please sign in to comment.