Bug 119

Intent
------

To make it possible to non-deterministically select a value from a
range of values without using multible edges.

Motivation
----------

People have been asking for a random number generator function for a
long time.

For purposes of symmetry reduction, this is the only way of
selecting a value from a scalarset. So even though this construction
is syntactic sugar for the current language, it is essential for
adding symmetry reduction.

Syntax
------

Essentially, this is the dual construction of the for-iterator
construct. It provides a non-deterministic choice, similar to the case
statement in other modelling languages. In Murphi this was provided as
the box-operator. 

At the moment, we cannot expose such an operation in the imperative
language extensions of Uppaal, since the interpretor cannot generate
multible successors. Therefore we suggest adding this as an extra
field on edges. Essentially there will be a 'select' field just like
we have 'guard', 'synchronisation' and 'update' fields at the
moment. The syntax is something like:

select-list ::= [ <id> ':' <type> ( ',' <id> ':' <type> )+ ]

select-field ::= [ 'select' <id> ':' <type> ( ',' <id> ':' <type> )+ ]

where select-list is what you would write in the GUI and select-field
is what you would write in XTA files.

The semantics would be to non-deterministically select (a) value(s)
for the identifier(s). In the implementation we would obviously need
to enumerate all possible variables.

One comment about names: The name introduced by 'select' is visible
only for the transition, but in all four fields, i.e., the select,
guard, synchronisation and update fields. It must not be an existing
variable, since for instance the guard ranges over the different
values, but we cannot allow that any state variables are modified
while evaluating the guards.

Example
-------

trans
  a->b { select i : int[1,5]; guard i != 3; assign j = i; };

This would select a value between 1 and 5 that is not 3 and assign the
result to j.


Implementation
--------------

This does require a number of changes in UPPAAL. First of all the
parser and type checker need to be extended. Also the GUI needs to be
extended with this additional field.

The XML language is flexible enough to contain this extra field,
though. And the extension of the GUI editor is rather simple and the
same is true for the parser.

For the engine, we have to possible approaches:


We can extend the transition class with extra information and modify
the transition filter to do the enumeration. We probably need to add
the extra iteration 'variables' to the global state as meta variables,
since the successor filter must have access to them (because it
evaluates the update expression).

Other complications come from how we represent traces, since it might
become difficult to replay a trace if we do not store additional
information about the chosen values in the trace store. 

For the simulator, the GUI needs to be extended to allow the
user to select the proper transition (although this might be possible
to do on the server side).



The other possibility is to expand the selection to multible
edges. I.e. we would add an edge for each value (combination) of the
selection. Thus we would not need to modify the transition filter at
all. Potentially we could also statically reduce the guards once the
actual value of the selection is known, although this would be left
for future work. On the downside this requires us to compile the
guard, synchronisation and updates expressions for each of the
generated edges (although they could be reused if they do not depend
on the selection identifier). The problem with the GUI still exists,
since the GUI does not expect the same edge to generate several
transitions.




Initially, I planned to suggest the first implementation, but after
thinking a bit about it, I actually prefer the second
alternative. BUT: There is one situation that the second possibility
cannot handle:


int i;

a->b {select j: int[1,i]; .... };


I.e. the range over which j spans is determined at runtime. This is
quite powerful and cannot be 'unfolded' using the second
implementation approach. Then again, the same thing could be expressed using:


int[0, 20] i;

a->b {select j: int[1,20]; guard j <= i; ... };

which can be unfolded. Obviously, the bound on the declaration of i is
very important in this case (otherwise the unfolded model would become
very big).