To extend the language with a Java 5 like iterator construct.
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 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).
Syntactically, we propose the following variation of the normal
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
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 sum = 0;
for (v : a) sum += v;
I propose to delay this variation until a latter point.
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
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
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
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.