| Summary: | Add iterators to the 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 | ||
Implementation guide
--------------------
Modification to UTAP:
1. The existing parsing of for-loops needed to be changed to avoid
conflicts when adding another use of the keyword. The behaviour of
forBegin() in the ParserBuilder interface was changed.
Previously forBegin() was called right after 'for (' was parsed.
This was changed so that is not called until 'for (expr;expr;expr)'
has been parsed (otherwise a larger lookahead would be required to
distinguish the two types of for loops).
- The parser (parser.y) was changed so that forBegin() is called
after the closing parantheses is parsed, but before the
statement.
2. Extending the ParserBuilder interface (build.h)
The methods iterationBegin(const char *name) and iterationEnd(const
char *name) were added. The name argument is the name of the
identifier used for the iterator.
3. Extending the parser (parser.y)
We need to be able to parse the statement 'for ( Id : Type )
Statement'. ParserBuilder::iterationBegin(const char *name) is
called after the closing parantheses has been parsed and
iterationEnd(const char *name) is called after the statement has
been parsed.
4. Adding a Statement implementation for new loop
A new Statement derivative called IterationStatement was added. It
needs a new frame to contain the iterator variable (a symbol).
5. Extending the SystemBuilder class.
iterationBegin(const char *) and iterationEnd(const char *) were
implemented. A new frame is created to hold the iterator. Notice
that the statement instance is already created in iterationBegin()
so that we have a place to put the reference to the new frame
(otherwise it might be lost if the inner statement requires
creating new frames).
6. Extending the type checker (typechecker.cpp)
This has not been implemented yet.
For the old-verifyta module only the Compiler class needs
modification. The Compiler::visitIterationStatement() method was
implemented. Only integers are supported at the moment.
Except for the type checker, the code implementing the language extension has been checked into CVS. Type checking of iterators has been in CVS for some time now. Closing the bug. |
Intent ------ To extend the language with a Java 5 like iterator construct. Motivation ---------- The main motivation comes from the need to iterate over arrays indexed by scalars (for symmetry reduction). In particular we need to be able to do something like this: typedef scalarset[4] pid_t; int a[pid_t]; ... for (i : pid_t) a[i] = 0; ... Of course, such an extension should not be specific to symmetry reduction. Hence a proposal for introduction a generic iterator construction to the imperative language extensions. I want to stress that although this construction is syntactic sugar for the current language, it is required for scalarsets (since there is no other way to iterate over the elements of a scalarset). Notice though that in case of symmetry reduction the body must be restricted to be independent of the enumeration order (since elements of a scalarset are not ordered). Syntax ------ Syntactically, we propose the following variation of the normal for-loop construction: for-statement ::= 'for' '(' <id> ':' <type> ')' <statement> Of course, the old for-loop construct should be maintained. Notice the similarity with the proposed forall quantifier. The difference is that 'for' is a loop control structure whereas forall is used to form expressions. The scope of the identifier used in the for loop is limitted to the statement of the for-loop. It is not necessary to explicitly declare the identifier. Also, the type of the iterator is inferred. In Java, iterators are over collection objects. We could also allow iterators over array types, e.g. int a[4]; int sum = 0; for (v : a) sum += v; I propose to delay this variation until a latter point. Implementation -------------- Apart from updates to the parser and type checker, this extension can be dealt with by modifying the compiler in a rather straightforward manner. Extensions to the interpreter or other parts of Uppaal are not required.