Bug 278

This bug describes a suggestion for a new feature in the UPPAAL modelling
language. The extension described here replaces and supersedes the templateset
extension described in bug 117. 


I suggest to extend add two new aspects to the template instantiation mechanism:

1. Allow partial instantiation of a template.

2. Allow the use of partially instantiated or uninstantiated templates
   in the system specification.

The intended interpretation of item 2 is to instantiate the template for any
possible value of the parameters not already bound by partial instantiation.
This is as powerful as the template set mechanism currently supported by UPPAAL,
but IMO the new mechanism is cleaner than template sets.

The following exemplifies the extension:

typedef int[0,4] pid_t;

process P(pid_t pid, int &e)
{
...
}

int j;
Ps(i) = P(i, j);
system Ps;


Notice that the identifier i is local to the instantiation line and that its
type is inferred automatically. Templates with unbound parameters are only
allowed in the system line, if all unbound parameters are boolean, integer or
scalar types. For integer types, the bound must be explicitly given (to avoid
risk of accidentally instantiating 64k processes).


This syntax allows powerful new things like (reusing the definition of P above):


int j[5];
Ps(i) = P(i, j[i]);


This is not possible with template set mechanism. It is obviously possible to
instantiate a partially instantiated template further (continuing the previous
example):

Q = Ps(1);
R = Ps(3);
system Q, R;


If a partially instantiated template is given in the system line, this gives
rise to a number of processes. These can be accessed by providing the missing
arguments. E.g. in the first example, we could access individual processes like:

Ps(0).s
Ps(1).s


This is different from the current template set syntax (which exposes an
instantiated template set as an array of processes).




Estimated implementation effort: Implementing the suggested extension requires:


1. Extending the parser. The most problematic aspect is that something
   like Ps(0) looks like a function call. The easiest way to deal with
   this is to let the lexer access the symbol table and generate a
   different token for Ps. 

2. Extending the builder interface with support for partial template
   instantiation and the new expressions for adressing processes.

3. Extending the UTAP system representation to represent a partial
   instantiation (this is a matter of extending the instance_t struct
   with a parameter mapping) and the new kind of expression (the
   existing expression_t class is flexible enough to do this with
   little effort).

4. Extending the type checker with type inference.

5. Extending the Compiler class with code to instantiate a template
   into a set of processes (a minor modification of the existing
   template set code).

6. Remove all template set code.


Item 4 is probably the most tricky part (because of things like 'Ps(i) = P(a[i],
b[i])'). For some cases we would probably need to give up, e.g.

process P(int[1,5] i, int[2,6] j)
{
...
}

Ps(i) = P(i + 1, i + 2);

In this case i clearly has the type int[0,4], but this is not at all easy to
derive and outside the scope of this bug (however, future versions could improve
on the type inference).


Further extensions are possible, e.g. parallel composition and local variables:

p(i) = let { chan e; int j; } in A(i, j, e), B(e, j);

How such extensions should be described in other bugs and are outside the scope
of what can be realistically implemented for 3.6.