P Program (Outline)

We recommend that you start 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 following top-level declarations:

Top Level Declarations Description
User Defined Types P supports users defined types as well as foreign types (types that are defined in external language)
Enums P supports declaring enum values that can be used as int constants (update the link)
Events Events are used by state machines to communicate with each other
State Machines P state machines are used to model or implement the behavior of the system
Specification Monitors P specification monitors are used to write the safety and liveness specifications the system must satisfy for correctness
Global Functions P supports declaring global functions that can be shared across state machines and spec monitors
Module System P supports a module system for implementing and testing the system modularly by dividing it into separate components
Test Cases P test cases help programmers to write different finite scenarios under which they would like to check the correctness of their system

Models, Specifications, Model Checking Scenario

A quick primer on what a model is, versus a specification, and model checking scenarios: (1) A specification says what the system should do (correctness properties). (2) A model captures the details of how the system does it. (3) A model checking scenario provides the finite non-deterministc test-harness or environment under which the model checker should check that the system model satisfies its specifications.