This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 117

Summary: Add template-sets to the language
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: enhancement CC: martijnh
Priority: P1    
Version: unspecified   
Hardware: All   
OS: All   
Architecture:
Bug Depends on:    
Bug Blocks: 196    

Description Gerd Behrmann 2004-12-02 11:58:18 CET
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.
Comment 1 Gerd Behrmann 2005-02-01 13:56:03 CET
Reassigning to Martijn.
Comment 2 Gerd Behrmann 2005-08-25 15:52:22 CEST
Reassigning to Gerd.
Comment 3 Gerd Behrmann 2005-08-25 15:54:59 CEST
Support for template sets has been committed to CVS. 

At the moment template sets can be declared over integer types starting with a range starting at 0. This 
looks rather ugly and I suggest that once scalarsets are introduced, support for declaring template sets 
over integers is removed.
Comment 4 Gerd Behrmann 2005-08-25 16:00:09 CEST
Things that are missing:

- Extending the XML format
- Extending the GUI
- Lots of testing :-)
Comment 5 Gerd Behrmann 2005-11-06 17:48:07 CET
Increasing priority. The engine has been updated, but there is some GUI work left to be done. We should 
target this for 3.6 alpha 2.
Comment 6 Gerd Behrmann 2006-01-17 17:24:22 CET
The syntax for template sets has changed. Rather than

process P[i : int[0,4](int j) { ... }

we now use

process P(int[0, 4] +i, int j) { ... }

The first argument (or more generally, the arguments for parameters prefixed
with a + sign) is implicitly given and should not be specified when
instantiating the template. E.g. the above template is instantiated as

Ps = P(k);

for k being an integer variable.

Template set parameters must always be listed first. Otherwise the syntax is
unchanged.

This change has the benefit that we do not need to change the DTD of the XML
format and we do not need to make any changes in the GUI to support template
sets. This change has alrady been implemented on the trunk.
Comment 7 Gerd Behrmann 2006-01-19 13:19:26 CET
I am resolving this bug as FIXED. Any further problems with template sets should be registered as new 
bugs.