Peasy

Peasy: An easy-to-use development environment for P

P is a state machine based programming language for formal modeling and analysis of distributed systems. P is being used by developers in industry and academia to reason about the correctness of their distributed system. We developed Peasy is to make the process of creating, checking, and debugging P models easy.

📣 Peasy is a step towards making application of P in practice, easy-peasy! 📣

Peasy is a VS Code language extension for P. Peasy supports syntax highlighting, compilation, error reporting, and unit testing of P formal models within the VS Code environment.

Peasy provides state machine visualization that developers can use to visualize their formal design (P state machines) and share in their design documentation.

Peasy provides trace visualization to aid debugging counter examples provided by the P checker. Error traces for complex distributed systems are hard to debug as they involve nontrivial interleaving of messages. Peasy helps visualize traces as message sequence charts, perform filtering, and do motif based analysis.

Navigate through the user guide for an in depth description and demo videos of all the cool features in the Peasy extension. Checkout the demo video for a complete step-by-step guide.

Built with ❤️ from the P Team @ Amazon Web Services (AWS).

Peasy Features

my img

Syntax Highlighting

my img

Automatic Compilation

my img

Snippets

my img

Error Reporting

my img

Testing Framework

my img

Trace Visualization

my img

State Machine Visualization