Skip to content

P Program (Outline)

P Language Manual

We recommend starting with the Tutorials to get familiar with the P language and its tool chain.

P Top Level Declarations Grammar 
topDecl:                # Top-level P Program Declarations
| typeDecl              # UserDefinedTypeDeclaration
| enumTypeDecl          # EnumTypeDeclaration
| eventDecl             # EventDeclaration
| machineDecl           # MachineDeclaration
| specDecl              # SpecDeclaration
| funDecl               # GlobalFunctionDeclaration
| moduleDecl            # ModuleDeclaration
| testDecl              # TestCaseDeclaration
;

A P program consists of a collection of the following top-level declarations:

Declaration Description
User Defined Types User-defined types as well as foreign types (defined in external languages)
Enums Enum values that can be used as int constants
Events Events used by state machines to communicate with each other
State Machines State machines that model or implement the behavior of the system
Specification Monitors Safety and liveness specifications the system must satisfy
Global Functions Functions shared across state machines and spec monitors
Module System Modular system design by dividing into separate components
Test Cases Finite scenarios for checking system correctness
Models, Specifications, and Model Checking Scenarios

A quick primer:

  • Specification — says what the system should do (correctness properties)
  • Model — captures the details of how the system does it
  • Model checking scenario — provides the finite non-deterministic test-harness under which the model checker verifies that the model satisfies its specifications