Bug 66

For some models, this might be very nice. Uppaal only uses the control structure
of the automata to identify active clocks. This is most certainly an over
approximation of the real set of active clocks, since we do not take
synchronisations and guards on integers into account.

As you mention, giving users control over active clocks is dangerous since users
make mistakes. So we should try to extend the automatic active clock reduction
analysis. For instance the techniques described in the "To Store or Not To
Store" paper could easily be applied to active clock reduction aswell.

That said, I don't think that we will ever be able to exactly identify the set
of active clocks (or the set of active integer variables for that matter). So
being able to specify the active clocks (or active variables in general) is a
good thing.

I suggest that instead of doing it "per location", we should make it possible to
add some kind of expression to each clock/variable, indicating whether it is
active or not. This should be combined with the automatic analysis, e.g. if the
expression evaluates to false, then the clock is inactive, if it evaluates to
true, then we use the automatic analysis. Using an expression instead tying it
to a location would make it possible to take e.g. the values of integer
variables into account when computing whether a clock is active. And for active
variable reduction: If you take the train-gate demo model, then you could
formulate an expression stating that only the len first elements are active in
the array holding the queue. Of course, we could allow the expression to refer
to locations (like in the property language).

Finally, we can add runtime checks ensuring that the user didn't make any
mistakes. I.e. we could check that whenever we have found a clock/variable to be
inactive (due to the user specified expression) then no expression accesses the
value of this clock/integer variable. This would be one of the generic checks to
run on any model.

Here is my proposal how to add "user specified inactive clocks".

Structure
---------

There are a number of alternatives how this hinting could be
implemented. One possibility is to use the special
function mechanism of bug 115. Whenever a clock is defined, the user can
optionally create a spcecial function *in the same scope* defining the
activeness of the clock. E.g.


clock x;

bool $active_x()
{
   return expr;
}

Alternatively we could name it $is_active_x() or $is_x_active()
(although the latter is more correctly from an grammatical point, I do
not like the fact that is uses a prefix and a suffix). 

The interpretation of the function would be that if it returns true,
then x *might* at some later point. If it returns false, then the user
guarantees that it will not be. The default would be simply to return
true. On top of this we would of course do our normal active clock
reduction analysis. I.e. if $active_x() returns true, but we find x to
be inactive, then we know x is inactive and can remove it.

To rules must be obeyed:

- $active_x() must never go from false to true without a reset of x.

- x must never be used (e.g. in a guard or invariant) if it is
  inactive.

The nice thing is that violations of either rule can be detected at
runtime, and an error messages can be provided.




Alternative structure
---------------------

An alternativ is to add special properties to clocks such that we can
refer to x.active and set it to false, e.g. in an $on_after_update()
special function. This means instead of:

bool $active_x()
{
   return expr;
}

we write

void $on_after_update()
{
   x.active = expr;
}


This is harder to implement, since it requires modifications to the
parser and type checker (since now clocks have an 'inner name space').

Possible advantages would be that the model can become a little
smaller since all update expressions are collected in one function; it
could even be slightly faster. 

The real difference between the two approaches is what we do with
clocks in arrays and records.

Arrays and records
------------------

Arrays are easy to handle in both cases:

clock x[5];

bool $active_x(int index)
{
   return expr;
}

or

void $on_after_update()
{
   x[i].active = expr;  /* This would require some loop */
}


Here I find the first solution more elegant. Both approaches can
handle multi-dimensional arrays in the same way. Notice that the
second approach again has the potential of being faster. Imagine a
stack of clocks encoded in an array:

clock x[SIZE];
int length = 0;

The first approach would call the following function SIZE times:

bool $active_x(int index)
{
   return index < length;
} 

The second approach would look like this:

void $on_after_update()
{
   int i;
   for (i = length; i < SIZE; i++)
   {
	x[i].active = false;
   }
}

This is less elegant, but the loop is smaller. Even better, we can put
the x[i].active = false update on the edge popping an element of the
stack, thus avoiding the loop altogether.




The real problem comes when we have records:

struct { int a; clock x[5]; } A[3];

bool $active_A_x(int index_of_A, int index_of_A_x)
{
  return expr;
}

void $on_after_update()
{
  A[i].x[j].active = expr;   /* This again requires a loop */
}

Here the use of .active suddenly becomes nicer, since the approach
using special functions must use some sort of name mangling. Although
it is straightforward to generate the proper name of the special
function and the required parameters, I do fear that users might
become confused.


Summary
-------

Now I need some input: Except for the case with records, I clearly
find the first approach more elegant. It also has the advantage of
providing a clear mapping from states to whether a clock is active or
not; the second approach can update the active field on an edge, hence
we could end up with two identical states where the clock is active in
one state, but not in the other. The second approach has the potential
of being faster and has a simpler naming scheme when using records.

What should we use?

From an implementation point of view, the second approach does require
a modification to the parser, to the code generator (the one that
generates the byte code), to the filter structure and to the variable
mapping. The first approach only requires a modification the filter
structure.


Epilog: Instead of adding functions telling whether a clock is active
or not, one could add functions returning the maximum (lower and
upper) bound of a clock. This could potentially provide an even better
speedup - in particular when comparing clocks with integer expressions
-  but I'm pretty sure the user would become very confused.