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.
Change of plans: In some cases type inference would make certain construction impossible. For instance: process P() {...} Ps(int[0,4] i) = P() system Ps; would be a natural way of creating 5 instances of P() without requiring it to have any parameters. However if we cannot explicitly provide a type for i, then this would be impossible. Therefore I suggest dropping type inference.
The basic functionallity has been implemented. Things missing: - Check if symmetry can be broken by the new feature - Check what happens if non-const int without explicitly specified range is used as free process parameter. My guess is that it will use the default range, thus creating 64k intances....not good.
This has now been implemented on the trunk.