Skip to content

Commit e144d47

Browse files
ankushdesaiankushdesai
committed
Update documentation structure and content
1 parent acc5581 commit e144d47

File tree

9 files changed

+1451
-34
lines changed

9 files changed

+1451
-34
lines changed

‎Docs/README.md

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# P Language Documentation
2+
3+
This directory contains the documentation for the P programming language, a state machine-based language for formally modeling and specifying complex distributed systems.
4+
5+
## Documentation Structure
6+
7+
The documentation is built using [MkDocs](https://www.mkdocs.org/) with the [Material for MkDocs](https://squidfunk.github.io/mkdocs-material/) theme. The documentation is organized as follows:
8+
9+
- `docs/`: Contains the markdown files for the documentation
10+
- `mkdocs.yml`: Configuration file for MkDocs
11+
- `site/`: Generated static site (after building the documentation)
12+
- `images/`: Images used in the documentation
13+
14+
## Building the Documentation
15+
16+
To build the documentation locally:
17+
18+
1. Make sure you have Python installed
19+
2. Install MkDocs and the Material theme:
20+
```
21+
pip install mkdocs mkdocs-material
22+
```
23+
3. Build the documentation:
24+
```
25+
mkdocs build
26+
```
27+
4. Serve the documentation locally:
28+
```
29+
mkdocs serve
30+
```
31+
5. Open your browser and navigate to `http://localhost:8000`
32+
33+
## Documentation Website
34+
35+
The official documentation is available at: [http://p-org.github.io/P/](http://p-org.github.io/P/)
36+
37+
## Contributing to the Documentation
38+
39+
We welcome contributions to improve the documentation. Please feel free to submit pull requests with improvements, corrections, or additions.

‎Docs/docs/faq.md

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
# Frequently Asked Questions
2+
3+
This page answers common questions about the P language and its toolchain.
4+
5+
## General Questions
6+
7+
### What is P?
8+
9+
P is a state machine-based programming language for formally modeling and specifying complex distributed systems. It allows programmers to model their system design as a collection of communicating state machines and provides tools to check that the system satisfies desired correctness specifications.
10+
11+
### How is P different from other formal methods tools?
12+
13+
P distinguishes itself by:
14+
- Being a programming language rather than just a specification language
15+
- Focusing on practical distributed systems verification
16+
- Providing a balance between expressiveness and analyzability
17+
- Supporting both safety and liveness properties
18+
- Generating executable code from models
19+
20+
### Is P open source?
21+
22+
Yes, P is open source and available on [GitHub](https://github.com/p-org/P) under the MIT license.
23+
24+
### Who uses P?
25+
26+
P is used extensively inside Amazon (AWS) for analysis of complex distributed systems. It was also used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. Additionally, it's being used for programming safe robotics systems in academia.
27+
28+
## Technical Questions
29+
30+
### What kind of systems can I model with P?
31+
32+
P is particularly well-suited for modeling:
33+
- Distributed protocols and systems
34+
- Concurrent software
35+
- Event-driven systems
36+
- Reactive systems
37+
- State-based controllers
38+
39+
### What properties can P verify?
40+
41+
P can verify:
42+
- Safety properties (bad things never happen)
43+
- Liveness properties (good things eventually happen)
44+
- Invariants (properties that must always hold)
45+
- Temporal properties (ordering of events)
46+
47+
### How does P handle state space explosion?
48+
49+
P employs several techniques to manage state space explosion:
50+
- Search prioritization heuristics
51+
- Compositional verification
52+
- Abstraction techniques
53+
- Bounded model checking
54+
55+
### Can P generate executable code?
56+
57+
Yes, P can generate C# and C code from your models. The generated code can be deployed on various platforms when combined with the P runtime.
58+
59+
### How does P compare to TLA+?
60+
61+
While both P and TLA+ are used for formal specification and verification:
62+
- P is more programming-language-like, while TLA+ is more mathematical
63+
- P generates executable code, TLA+ is primarily for specification
64+
- P focuses on state machine models, TLA+ on temporal logic
65+
- P has built-in support for distributed systems concepts
66+
67+
## Usage Questions
68+
69+
### How do I get started with P?
70+
71+
Follow these steps:
72+
1. Install P following the [installation instructions](getstarted/install.md)
73+
2. Go through the [Quick Start Guide](getstarted/quickstart.md)
74+
3. Follow the [Learning Path](learning-path.md)
75+
76+
### How do I debug a P program?
77+
78+
You can debug P programs by:
79+
- Adding print statements to trace execution
80+
- Using assertions to check conditions
81+
- Examining error traces from the model checker
82+
- Using the [debugging techniques](advanced/debuggingerror.md) for counterexamples
83+
84+
### How do I model check a P program?
85+
86+
Use the `p check` command followed by the test case name:
87+
```bash
88+
p check TestCaseName
89+
```
90+
91+
For more options, see [Using P Compiler and Checker](getstarted/usingP.md).
92+
93+
### How do I integrate P with my existing codebase?
94+
95+
P provides a foreign interface that allows you to:
96+
- Call external functions from P code
97+
- Use external types in P code
98+
- Generate code that integrates with your existing system
99+
100+
See [P Foreign Interface](manual/foriegntypesfunctions.md) for details.
101+
102+
## Performance Questions
103+
104+
### How large a system can P verify?
105+
106+
The size of systems P can verify depends on:
107+
- The complexity of the state machines
108+
- The number of concurrent components
109+
- The properties being verified
110+
- Available computing resources
111+
112+
P has been used to verify industrial-scale distributed systems at AWS.
113+
114+
### How long does model checking typically take?
115+
116+
Model checking time varies widely based on:
117+
- System complexity
118+
- State space size
119+
- Property complexity
120+
- Search strategy
121+
122+
Simple examples may check in seconds, while complex systems might take hours.
123+
124+
### Can P use multiple cores for verification?
125+
126+
The current version of P primarily uses a single core for verification. However, work is ongoing to support parallel verification strategies.
127+
128+
## Community Questions
129+
130+
### How do I contribute to P?
131+
132+
You can contribute to P by:
133+
- Reporting bugs on [GitHub Issues](https://github.com/p-org/P/issues)
134+
- Submitting pull requests with improvements
135+
- Adding examples or case studies
136+
- Improving documentation
137+
- Participating in [discussions](https://github.com/p-org/P/discussions)
138+
139+
See [Building from Source](getstarted/build.md) for information on building P from source code.
140+
141+
### Where can I get help with P?
142+
143+
You can get help with P through:
144+
- [GitHub Discussions](https://github.com/p-org/P/discussions)
145+
- [GitHub Issues](https://github.com/p-org/P/issues)
146+
- Contacting the P team at [[email protected]](mailto:[email protected])
147+
148+
### Are there any books or courses on P?
149+
150+
While there are no dedicated books on P yet, you can learn from:
151+
- The [documentation](https://p-org.github.io/P/)
152+
- [Academic papers](publications.md) about P
153+
- [Video presentations](videos.md) about P
154+
- [Case studies](casestudies.md) showing P in action

‎Docs/docs/getstarted/quickstart.md

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
# Quick Start Guide
2+
3+
This guide will help you quickly get started with P by walking you through creating, compiling, and checking a simple P program. By the end of this guide, you'll have a basic understanding of how to use P for modeling and verifying distributed systems.
4+
5+
## Prerequisites
6+
7+
Before starting, make sure you have:
8+
9+
1. Installed P following the [installation instructions](install.md)
10+
2. Set up your preferred IDE (we recommend [Peasy](PeasyIDE.md))
11+
12+
## Your First P Program: Hello World
13+
14+
Let's create a simple "Hello World" example in P that demonstrates basic state machine communication.
15+
16+
### Step 1: Create a new directory for your project
17+
18+
```bash
19+
mkdir HelloWorldP
20+
cd HelloWorldP
21+
```
22+
23+
### Step 2: Create a P file
24+
25+
Create a file named `HelloWorld.p` with the following content:
26+
27+
```
28+
// Define events for communication
29+
event eHello;
30+
event eWorld;
31+
event eStartMachine;
32+
33+
// Main machine that coordinates the example
34+
machine Main {
35+
var helloMachine: machine;
36+
var worldMachine: machine;
37+
38+
start state Init {
39+
entry {
40+
// Create the Hello and World machines
41+
helloMachine = new HelloMachine();
42+
worldMachine = new WorldMachine();
43+
44+
// Start the Hello machine
45+
send helloMachine, eStartMachine, worldMachine;
46+
}
47+
}
48+
}
49+
50+
// Machine that sends "Hello"
51+
machine HelloMachine {
52+
var worldMachine: machine;
53+
54+
start state WaitForStart {
55+
on eStartMachine do (payload: machine) {
56+
worldMachine = payload;
57+
goto SendHello;
58+
}
59+
}
60+
61+
state SendHello {
62+
entry {
63+
print "Hello";
64+
send worldMachine, eHello;
65+
}
66+
}
67+
}
68+
69+
// Machine that responds with "World"
70+
machine WorldMachine {
71+
start state WaitForHello {
72+
on eHello do {
73+
print "World!";
74+
raise eWorld;
75+
}
76+
77+
on eWorld do {
78+
print "Hello World example completed.";
79+
}
80+
}
81+
}
82+
83+
// Test case to run the example
84+
test testHelloWorld {
85+
// Create the Main machine which will orchestrate the example
86+
new Main();
87+
}
88+
```
89+
90+
### Step 3: Compile the P program
91+
92+
Run the following command to compile your P program:
93+
94+
```bash
95+
p compile HelloWorld.p
96+
```
97+
98+
This will generate C# code in the `POutput` directory.
99+
100+
### Step 4: Run the test case
101+
102+
Run the test case to see the output:
103+
104+
```bash
105+
p run testHelloWorld
106+
```
107+
108+
You should see output similar to:
109+
110+
```
111+
Hello
112+
World!
113+
Hello World example completed.
114+
```
115+
116+
### Step 5: Check the program for correctness
117+
118+
P can also check your program for correctness. Let's add a simple safety specification:
119+
120+
Add the following to your `HelloWorld.p` file:
121+
122+
```
123+
// Safety monitor to ensure World always follows Hello
124+
spec SafetyMonitor observes eHello, eWorld {
125+
var sawHello: bool;
126+
127+
start state Init {
128+
entry {
129+
sawHello = false;
130+
}
131+
132+
on eHello do {
133+
sawHello = true;
134+
}
135+
136+
on eWorld do {
137+
assert sawHello, "World was printed before Hello!";
138+
}
139+
}
140+
}
141+
```
142+
143+
Now check your program:
144+
145+
```bash
146+
p check testHelloWorld
147+
```
148+
149+
If everything is correct, you should see that the check passes without any errors.
150+
151+
## Next Steps
152+
153+
Now that you've created your first P program, you can:
154+
155+
1. Learn more about P state machines in the [State Machines](../manual/statemachines.md) section
156+
2. Explore the [Client-Server tutorial](../tutorial/clientserver.md) for a more complex example
157+
3. Read about [P Monitors](../manual/monitors.md) to understand how to specify and verify properties
158+
159+
## Common Commands Reference
160+
161+
Here's a quick reference of common P commands:
162+
163+
| Command | Description |
164+
|---------|-------------|
165+
| `p compile <file.p>` | Compile a P program |
166+
| `p run <test-name>` | Run a specific test case |
167+
| `p check <test-name>` | Check a test case for correctness |
168+
| `p help` | Display help information |
169+
170+
For more detailed information on using the P compiler and checker, see [Using P Compiler and Checker](usingP.md).

0 commit comments

Comments
 (0)