This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 116

Summary: Add quantifiers to the expression language
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Severity: enhancement CC: martijnh
Priority: P2    
Version: unspecified   
Hardware: All   
OS: All   
Bug Depends on:    
Bug Blocks: 196    

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.