A template DES is a regular DES with one or more parameter variables in its name and in the name of some or all of its state and event labels. This new type of DES allows pairs of percent symbols (%) in the DES name, state names and event names. The variable between two ‘%’ symbols can be assigned values by instantiating the template. Every variable that appears in a state name or event name inside the DES, must also appear in the name of the DES.
A template DES can then be instantiated by specifying whether it is to be a plant or supervisor, and specifying the values the templates' variables can take on. For each distinct value assigned to a variable (or tuple of values assigned to a set of variables), one DES (called an instantiated DES) will be created and added to the project by replacing every instance of the variable (including the enclosing '%') with the specified value. This allows the user to easily specify multiple DES that are identical up to relabelling.
NOTE: Template DES are treated as separate from the project and are ignored by the algorithms. Only the instantiated DES, which are created on the fly from the templates and instantiation information, are visible to the verification algorithms. Also, instantiated DES can be viewed but not edited. Instead, the template must be edited and then the instantiation must be regenerated.
In a flat project, instantiation DES can be created as a plant or supervisor. An instantiation name must be unique to the project.
In an HISC project, a template can be added to any subsystem or interface. The same template DES can appear in more than one subsystem or interface. Instantiation DES can be created as part of a subsystem as a plant or supervisor, or as part of an interface as a supervisor. An instantiation name must be unique within a given subsystem or interface, but is not required to be unique to the entire project.
We can check all the related properties for the instantiations by running existing algorithms. Template DES can be saved and loaded for further work. However, the instantiations cannot be saved separately. DESpot only stores instantiation information in the project file. The instantiations are generated immediately when the project loads.
DESpot provides the following template features: