Introduction to PSF

Modules

PSF 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.