From 1fdbf74f073f889dbf78ea52b0dd581384b3c1a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= Date: Wed, 22 May 2024 09:42:17 +0200 Subject: [PATCH] Added a note on nested quantifiers --- content/language-reference/query-semantics/symb_queries.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/language-reference/query-semantics/symb_queries.md b/content/language-reference/query-semantics/symb_queries.md index 8bf38814..76012e96 100644 --- a/content/language-reference/query-semantics/symb_queries.md +++ b/content/language-reference/query-semantics/symb_queries.md @@ -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).