Bug 115

Motivation
----------

The newest development version has a nice litle feature in which one
can define global update expressions, that are either executed before
or after the update on the edges. This feature was originally
introduced in UPPAAL CORA, but since it has a number of very
interesting applications I moved it to mainline UPPAAL a long time
ago. In short, one can write:

before_update
{
   expr1
}

after_update
{
   expr2
}

This means that expr1 is executed before updates on edges and expr2
after.  Notice that they are only executed once per transition - no
matter how many edges are involved in defining the
transition. Interesting applications include:

- Annotating the model with a remaining cost estimate (UPPAAL CORA).

- Annotating the model with a heuristic function for guiding
  the search (UPPAAL CORA).

- Defining default values, i.e., when no value is assigned to a
  variable on any edges of the transition, then a default value is
  assigned (implemented by setting the variable to the default value
  in before_update) (UPPAAL).

- Implementing VHDL like value passing between components in which a
  write to an output variable is not seen in the input variable until
  the next 'tick'. Very nice when translating VHDL code to UPPAAL
  models. Involves both before_update and after_update (UPPAAL).

I'm sure there are many more uses. Now, there are other such
interesting expression one might want to define, i.e., expressions
that are called automatically by UPPAAL is certain situations. Instead
of keeping adding keywords like above to the language, I would rather
introduce a generic mechanism for doing this.

Structure
---------

My proposal is to use the newly introduced feature making it possible
to define functions. The idea would be that UPPAAL recognises certain
names and knows what to with them. E.g. the before_update section
above could easily be replaced by a function:

void on_before_update()
{
   expr1;
}

which would even make it possibly to use statements (this was also
possible before, but required the before_update expression to call
another function containing the statements).

The only problem is the risk that the user might define a function
with this name for other purposes, not realising that UPPAAL treats it
in a special way. I propose to introduce a special prefix for such
special functions. Possible prefixes are $ and @. The former looks
very shell-like and the latter very Ruby-like. I propose using the $
symbol, e.g.:

void $on_before_update()
{
   expr1;
}

Implementing this in UTAP should be rather easy.


There are a number of interesting special functions, some of them
global, some of the local:

void $on_before_update()
------------------------

Global: Is called before any edge updates. 

void $on_after_update()
-----------------------

Global: Is called after any edge updates. 

void $on_before_update()
------------------------

Local: Is called before any edge updates and before the global
on_before_update(). Is called even when the process is not involved in
the transition.

void $on_after_update()
-----------------------

Local: Is called after any edge updates, but before the global
on_after_update(). Is called even when the process is not involved in
the transition.

void $on_before_local_update()
------------------------------

Local: Called before the local edge update, hence only when the local
process is involved in the transition.

void $on_after_local_update()
------------------------------

Local: Called after the local edge update, hence only when the local
process is involved in the transition.

bool $enabled()
---------------

Local: Must be side-effect free. When false is returned, all edges are
disabled.




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

Due to the byte-code interpreter in UPPAAL, the addition of this
feature can be achieved with zero overhead for the case where none of
the functions are defined:

If defined, calls to $on_before_local_update() and
$on_after_local_update() are integrated into the byte-code generated
for the update expression on edges.

If defined, calls to local and global $on_before_update() are compiled
into a single byte-code block, which is called before the other
updates. Similarly for the $on_after_update() functions. In case the
block it empty, the execution overhead is identical to the current
before_update and after_update expressions.

If defined, calls to $enabled() are integrated into the byte-code
generated for the guard expressions.


In all cases, there is no overhead if the functions are not defined.


Summary
-------

This is a low risk modification (low risk in the sense that it
requires few modifications and does not incur any overhead for old
models). The existing before_update and after_update expressions have
shown to be very useful, but introduce new keywords. The proposed
modification avoids this problem and is extensible (i.e., we might
come up with many more special functions in the future). 

I propose that this is implemented ASAP - I volunteer for doing the
implementation.