Bug 116 - Add quantifiers to the expression language
Summary: Add quantifiers to the expression language
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: All All
: P2 enhancement
Assignee: Gerd Behrmann
Depends on:
Blocks: 196
  Show dependency treegraph
Reported: 2004-12-02 11:57 CET by Gerd Behrmann
Modified: 2005-09-03 21:06 CEST (History)
1 user (show)

See Also:


Note You need to log in before you can comment on or make changes to this bug.
Description Gerd Behrmann 2004-12-02 11:57:35 CET

To extent the expression language with a forall quantifier. 


The main motivation comes from our work on symmetry reduction. Here it
is necessary to be able to make symmetric expressions, in particular
in the queries. As an example take Fischer's protocol for mutual
exclusion. Here you want to express something like:

A[] forall (i: int[1,4]) forall (j: int[1,4]) P[i].cs && P[j].cs implies i == j

The syntax is identical to that of Murphi (and is similar to the new
iterator syntax in Java 5). Paul has previously asked for something
like this. One could also add an exist or forsome operator, but it is
easily expressed using forall and negation.


Syntactically, we propose adding a keyword 'forall' and a production

expr ::= 'forall' '(' <id> ':' <type> ')' <expr>

Here <type> must be an enumerable type (and in the first
implementation even restricted to integer types). For symmetry
reduction, this will be a scalarset, but scalarsets will be added


Besides the obvious update to the parser, we only need to change the
compiler. The evaluation can be done using the existing interpreter
and byte-code language. For the expression above, we need to compile
it to the equivalent of:

for (int i = 1; i <= 4; i++)
   for (int j = 1; j <= 4; j++)
     if (!(P[i].cs && P[j].cs implies i == j)
        return false;
return true;
Comment 1 Gerd Behrmann 2005-02-01 13:55:45 CET
Reassigning to Martijn.
Comment 2 Gerd Behrmann 2005-09-03 16:51:59 CEST
Basic support for the forall quantifier has been checked into CVS. 


- Type check ensuring that the type provided is an integer.
- The interpreter in UTAP needs to be extended to handle these expressions.
- Expression to string conversion in UTAP needs to be extended to handle the new quantifier.
- The static analyser (ExpressionAnalyser) in UPPAAL must be extended to handle the new quantifier.
Comment 3 Gerd Behrmann 2005-09-03 18:36:25 CEST
Remaining things have now been checked into CVS. Closing the bug.