ModulesPSF specifications consist of one or more modules. There are two types of modules, data and process modules. The structure of data modules is borrowed from ASF, and process modules have a similar structure. A module consist of sections that have a predefined order. Below we give the structure for both types of modules.
data module Module begin sorts ... functions ... variables ... equations ... end Module
process module Module begin atoms .. processes ... sets ... communications ... variables ... definitions ... end Module
The order of the sections is relevant. Each section starts with a keyword followed by the elements of that section. If a section does not have any elements, the associated keyword can be omitted.
In addition to the sections mentioned above a module can also have an imports, an exports, and a parameters section.