Bug 117

Intent
------

To allow the user to declare templates that are always instantiated
into a set of processes.

Motivation
----------

The main motivation comes from the need to easily specify symmetric
systems for symmetry reduction. We need a syntactic construction, that
guarantees that a certain template is always instatiated over a
scalarset, e.g., a set of process identifiers.

The suggested syntactic extension is not limited to scalarsets and
symmetry reduction and is therefore proposed separately from symmetry
reduction. Still, the main motivation comes from symmetry reduction.

Also Paul has previously expressed a desire for a feature that allows
the user to instantiate a template into a set of processes. 

Initially we considered changing the instantiation mechanism. Finally,
we decided against this and instead modified the template declaration
mechanism. The reason for this is again based on the desire for adding
symmetry reduction: In order to guarantee symmetry, it is really a
requirement that the template is instantiated over a scalarset. 

Take Fischer's protocol for mutual exclusion as an example: Here we
have a template for a process taking the process identifier as an
argument. Initially, we thought of keeping the declaration of a
template, e.g, process P(pid_t pid) {...}. Then, in the instantiation
one would need to instantiate P for every element in pid_t - maybe as
an array of processes, e.g., P p[pid_t] = { P(0), P(1), P(2), P(3) };
The problem is that this suggests a degree of freedom in the
instantiation that is not really there: Since the template was
declared over a scalarset, there is no longer a choice in how it can
be instantiated - it must be instantiated for each element. We feel
that the number of side conditions required for this syntax is too big
and therefore suggest the following alternative.


Syntax
------

The suggestion is to introduce a mechanism to declare a template over
a set. This is in some sense similar to the RuleSet construction of
Murphi. In UPPAAL this becomes a template set. Lets start with the XTA
syntax. There are a number of possible variations over the same idea:

process (pid: pid_t, ... ) P() {...}
process [pid: pid_t][...] P() {...}
process P[pid: pid_t][...]() {...}


PSet1 = P();
PSet2 = P();

Where PSet1 and PSet2 are sets of processes over pid_t. Notice that it
is still possible to provide other parameters for the template set,
but the syntax enforces that for a single process set, all processes
have the same arguments (which is very important for symmetry
reduction).

In the property language, one can refer to specific processes in the
set using an array indexing like notation, e.g. (although this can
simplified by the proposed extension with quantifiers in bug 116):

A[] PSet1[0].cs + PSet1[1].cs + PSet1[2].cs + PSet1[3].cs <= 1

This is a reason for choosing the third of the proposed template
declaration notations (which is most similar to an array
declaration). However, the first notation is similar to the proposed
iterator and quantifier extensions.

The abstract syntax (for the third notation) would be something like:

template-decl ::= 'process' <id> ( '[' <id> ':' <type> ']' )* '('
                  parameter-list ')' '{' template-body '}'




In the GUI this is best achieved by introducing another field between
the name and the parameters of the template declaration.


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

Besides the obvious changes to the parser and type checker, this only
requires changes in the CommonBuilder class which takes care of
template instantiation.