| Summary: | Add quantifiers to the expression language | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Gerd Behrmann <behrmann> |
| Component: | Engine | Assignee: | Gerd Behrmann <behrmann> |
| Status: | RESOLVED FIXED | ||
| Severity: | enhancement | CC: | martijnh |
| Priority: | P2 | ||
| Version: | unspecified | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
| Bug Depends on: | |||
| Bug Blocks: | 196 | ||
Reassigning to Martijn. Basic support for the forall quantifier has been checked into CVS. Missing: - 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. |
Intent ------ To extent the expression language with a forall quantifier. Motivation ---------- 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. Syntax ------ Syntactically, we propose adding a keyword 'forall' and a production like: 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 later. Implementation -------------- 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;