Example

As an example of a specification in PSF we specify a system consisting of the processes P and Q that communicate with each other. Process P can either send a 'message' to process Q and then wait for an acknowledgement from Q, or it can send a 'quit' after which the system stops.

We start with specifying a data module containing the definitions for the different data to be send between the processes P and Q.

data module Data
begin
    exports
    begin
        sorts
            DATA
        functions
            message : -> DATA
            ack : -> DATA
            quit : -> DATA
    end
end Data

We continue with a process module that specifies the system consisting of the processes P and Q. This module imports the data module.

process module System
begin
    imports
        Data
    atoms
        snd : DATA
        rec : DATA
        comm : DATA
    processes
        P, Q
        System
    sets
        of atoms
            H = { snd(x), rec(x) | x in DATA }
    communications
        snd(x) | rec(x) = comm(x) for x in DATA
    definitions
        P = snd(message) . rec(ack) . P + snd(quit)
        Q = rec(message) . snd(ack) . Q + rec(quit)
        System = encaps(H, P || Q)
end System

The process System merges the processes P and Q and enforces the communication between them by encapsulating this merge. The encapsulation prevents the execution of the actions in set H, which now can only be executed as part of the communication action.