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

Bug 118

Summary: Add iterators to the language
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: 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    

Description Gerd Behrmann 2004-12-02 12:05:17 CET
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.
Comment 1 Gerd Behrmann 2005-02-01 13:52:54 CET
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.
Comment 2 Gerd Behrmann 2005-02-01 13:53:40 CET
Except for the type checker, the code implementing the language extension has
been checked into CVS.
Comment 3 Gerd Behrmann 2005-09-04 17:09:56 CEST
Type checking of iterators has been in CVS for some time now. Closing the bug.