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)
Reassigning to Martijn.
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.
Remaining things have now been checked into CVS. Closing the bug.