Skip to content

Commit b3ee932

Browse files
mchadalavadamchadalavada
committed
Update documentation with junit example
1 parent fdea4a8 commit b3ee932

26 files changed

+366
-131
lines changed

‎Docs/docs/advanced/pobserve/example/lockserver.md‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
# Lock Server
2+
3+
## Overview
4+
5+
Consider a simple lock server that manages access to shared resources by granting or denying locks. The lock server grants locks if resources are available, denies locks if resources are locked, and releases locks when the client is done using resources.
6+
7+
To ensure the correctness of the lock server, we want to check if the following correctness properties hold in the presence of concurrent client requests:
8+
9+
* *The lock server grants a lock to only one client at a time (Mutual Exclusion)*
10+
* *The lock server responds to a client only when requested (Response Only On Request)*
11+
12+
## Lock Server Package
13+
14+
The [LockServer](https://github.com/p-org/P/tree/main/Src/PObserve/Examples/LockServer) package will be used to demonstrate how to integrate PObserve directly into Java JUnit tests for real-time specification verification during test execution. This package contains:
15+
16+
1. **Lock Server Implementation**: Core lock server functionality with logging integration
17+
2. **JUnit Test Classes**: Various test approaches including PObserve-enabled tests
18+
3. **PObserve Integration**: Real-time specification monitoring during test execution
19+
4. **Logging Configuration**: Log4j2 setup for capturing and analyzing events
20+
21+
## Lock Server PObserve Package
22+
23+
The [LockServerPObserve](https://github.com/p-org/P/tree/dev/pobserve/Src/PObserve/Examples/LockServerPObserve) package will be used to demonstrate how to use different modes of PObserve on the lock server example. This package contains three components:
24+
25+
1. **Parser**: The `LockServerParser` converts the service log lines to PObserve Events
26+
2. **P Specification**: The `LockServerCorrect.p` implements two correctness specifications - `MutualExclusion` and `ResponseOnlyOnRequest`
27+
3. **Logs**: The resources folder contains multiple sample lock server logs for you to play around

Docs/docs/advanced/pobserve/example/lockserverexample.md renamed to Docs/docs/advanced/pobserve/example/lockserverwithpobservecli.md

Lines changed: 3 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,7 @@
1-
# Example: Lock Server
1+
# Running PObserve CLI on Lock Server Example
22

33
This page demonstrates how to use PObserve CLI to verify system correctness using a lock server as an example.
44

5-
## Lock Server Overview
6-
7-
Consider a simple lock server that manages access to shared resources by granting or denying locks. The lock server grants locks if resources are available, denies locks if resources are locked, and releases locks when the client is done using resources.
8-
9-
To ensure the correctness of the lock server, we want to check if the following correctness properties hold in the presence of concurrent client requests:
10-
11-
* *The lock server grants a lock to only one client at a time (Mutual Exclusion)*
12-
* *The lock server responds to a client only when requested (Response Only On Request)*
13-
14-
## Lock Server PObserve Package
15-
16-
The [LockServerPObserve](https://github.com/p-org/P/tree/dev/pobserve/Src/PObserve/Examples/LockServerPObserve) package will be used to demonstrate how to use PObserve CLI on the lock server example. This package contains three components:
17-
18-
1. **Parser**: The `LockServerParser` converts the service log lines to PObserve Events
19-
2. **P Specification**: The `LockServerCorrect.p` implements two correctness specifications - `MutualExclusion` and `ResponseOnlyOnRequest`
20-
3. **Logs**: The resources folder contains multiple lock server logs. Feel free to experiment with PObserve CLI using these logs.
215

226
## Building PObserve and LockServerPObserve JARs
237

@@ -106,4 +90,5 @@ java -jar PObserve-1.0.jar \
10690
0 1 0 0
10791
```
10892

109-
:confetti_ball: Congratulations! You have successfully run your first example with PObserve CLI.
93+
!!! success ""
94+
:confetti_ball: Congratulations! You have successfully run your first example with PObserve CLI.

‎Docs/docs/advanced/pobserve/example/lockserverwithpobservejunit.md‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
# Running PObserve Java Unit Test on Lock Server Example
2+
3+
This page demonstrates how to use PObserve with Java JUnit tests to verify system correctness in real-time during test execution using a lock server as an example.
4+
5+
## Prerequisites: Building and Publishing LockServerPObserve Package
6+
7+
Before running the lock server package that has PObserve integrated JUnit tests, you need to build and publish the `LockServerPObserve` package to your local Maven repository. The JUnit tests depend on this package for the parser and specification classes.
8+
9+
**1. Clone P repository**
10+
```bash
11+
git clone https://github.com/p-org/P.git
12+
```
13+
14+
**2. Navigate to the LockServerPObserve Directory**
15+
16+
```bash
17+
cd P/Src/PObserve/Examples/LockServerPObserve/
18+
```
19+
20+
**3. Build and Publish to Local Maven Repository**
21+
22+
```bash
23+
# Initialize Gradle wrapper if not present
24+
gradle wrapper
25+
26+
# Build the project
27+
./gradlew build
28+
29+
# Publish to local Maven repository
30+
./gradlew publishToMavenLocal
31+
```
32+
33+
??? info "What happens during the build process"
34+
- **P Specification Compilation**: The `compilePSpec` task compiles the P specification files in `src/main/PSpec/` using the P compiler
35+
- **Java Compilation**: Compiles the Java parser and related classes
36+
- **Maven Publication**: Publishes the artifact `io.github.p-org:LockServerPObserve:1.0.0` to your local Maven repository (`~/.m2/repository/`)
37+
- **Dependencies Available**: The lock server package will now be able to resolve the dependency: `implementation("io.github.p-org:LockServerPObserve:1.0.0")`. This provides access to:
38+
39+
* Parser class: `lockserver.pobserve.parser.LockServerParser`
40+
41+
* MutualExclusion specification class: `lockserver.pobserve.spec.PMachines.MutualExclusion.Supplier`
42+
43+
* ResponseOnlyOnRequest specification class: `lockserver.pobserve.spec.PMachines.ResponseOnlyOnRequest.Supplier`
44+
45+
46+
## Running JUnit Tests in Lock Server Package
47+
48+
**1. Navigate to the Lock Server Package**
49+
50+
```bash
51+
cd P/Src/PObserve/Examples/LockServer/
52+
```
53+
54+
**2. Build the Project**
55+
56+
The PObserve integrated JUnit tests are executed during the build process:
57+
```bash
58+
gradle wrapper
59+
./gradlew build
60+
```
61+
62+
**2. Running Unit Tests**
63+
```bash
64+
./gradlew test
65+
```
66+
67+
??? success "Expected Output"
68+
Running `./gradlew test` runs all the pobserve integrated unit tests in the LockServer package. The console output looks as follows:
69+
```
70+
> Task :test
71+
72+
LockServerExtendCustomBaseTest > basicTest() PASSED
73+
74+
LockServerExtendCustomBaseTest > multipleRandomClients() PASSED
75+
76+
LockServerExtendCustomBaseTest > randomClient() PASSED
77+
78+
LockServerExtendCustomBaseTest > expectFail() PASSED
79+
80+
LockServerExtendPObserveBaseTest > basicTest() PASSED
81+
82+
LockServerExtendPObserveBaseTest > multipleRandomClients() PASSED
83+
84+
LockServerExtendPObserveBaseTest > randomClient() PASSED
85+
86+
LockServerExtendPObserveBaseTest > expectFail() PASSED
87+
88+
LockServerTest > testReleaseLockFail() PASSED
89+
90+
LockServerTest > testAcquireLockFail() PASSED
91+
92+
LockServerTest > testAcquireAndReleaseLock() PASSED
93+
94+
LockServerTest > testReleaseLockNotHeldByClient() PASSED
95+
96+
LockTest > testReleaseLock() PASSED
97+
98+
LockTest > testAcquireLock() PASSED
99+
100+
LockTest > testAcquireLockAlreadyHeld() PASSED
101+
102+
LockTest > testReleaseLockNotHeldByClient() PASSED
103+
104+
LockTest > testReleaseLockWhenNotLocked() PASSED
105+
106+
> Task :test
107+
108+
StructuredLoggerTest > testAllValuesFilled() PASSED
109+
110+
StructuredLoggerTest > testValuesNull() PASSED
111+
112+
TransactionLoggerTest > testLogReleaseRequest() PASSED
113+
114+
TransactionLoggerTest > testLogLockResp() PASSED
115+
116+
TransactionLoggerTest > testLogReleaseResp() PASSED
117+
118+
TransactionLoggerTest > testLogLockRequest() PASSED
119+
120+
BUILD SUCCESSFUL in 6s
121+
4 actionable tasks: 4 executed
122+
```
123+
124+
!!! success ""
125+
:confetti_ball: Congratulations! You have successfully set up and run PObserve with Java JUnit integration for real-time specification monitoring on a Lock Server Example!

‎Docs/docs/advanced/pobserve/gettingstarted.md‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,15 @@
11
# Getting Started with PObserve
22

3-
## [Step 1] Extend your P formal model package with support for PObserve
4-
As mentioned in the [PObserve overview page](./pobserve.md), PObserve requires two inputs from users:
3+
## [Step 1] Create a PObserve Package
4+
To get started with PObserve, you first need to set up an empty PObserve Gradle project structure. Follow the [Setting Up a PObserve Package with Gradle](./package-setup.md) guide to create the project structure and configure the build system.
55

6-
1. A [PObserve Log Parser](./logparser.md) to convert logs into PObserve events
7-
2. P specifications that should be checked on the logs
6+
Once you have the empty PObserve package set up, you'll need to implement two key components:
7+
8+
1. **[P specifications](../../../manual/monitors)** - P state machines that define the correctness properties to be checked
9+
2. **[PObserve Log Parser](./logparser.md)** - A Java class that converts your system's logs into PObserve events
10+
11+
After implementing these components in your PObserve package, you can build the project to generate artifacts that can be used with PObserve.
812

9-
Once you have defined your parser and specifications, follow the [Setting Up a PObserve Package with Gradle](./package-setup.md) guide to learn how to package them into a JAR file that can be consumed by the PObserve CLI.
1013

1114
## [Step 2] Checking specifications using PObserve
1215
PObserve allows checking formal specifications in two different modes: (1) unit testing and (2) locally (as a commandline tool)
@@ -27,6 +30,6 @@ Follow the [PObserve JUnit Integration Guide](./pobservejunit.md) to get started
2730
**[Mode 2] Check P specifications by running PObserve locally (as a commandline tool)**
2831

2932
!!!info ""
30-
✔ Enables checking specifications on a local machine at a smaller scale
33+
✔ Enables checking specifications against small service/test log files on local machine
3134

3235
Follow the [PObserve CLI Guide](./pobservecli.md) to start using the PObserve command line tool.

‎Docs/docs/advanced/pobserve/logparser.md‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# PObserve: Log Parser
22
## What is a PObserve Log Parser?
3-
In order to use PObserve, a *log parser* is an essential component that converts system-generated log lines to PObserve events which are later consumed by a PObserve monitor. It takes a log line (text or JSON) as input and converts it into a PObserveEvent object.
3+
In order to use PObserve, a *log parser* is an essential component that converts system-generated log lines to PObserve events which are later consumed by a PObserve monitor. The log parser takes a log line (text or JSON) as input and converts it into a PObserveEvent object.
44

55
!!! note ""
66

@@ -85,8 +85,4 @@ public class LockServerParser implements Parser<PEvent> {
8585
!!!note "Note"
8686
The key used while creating the PObserve event will be used for partitioning the events to appropriate monitors.
8787

88-
**[Step 3] Move the Parser code to the right package**
89-
90-
Put the parser file in the "Parser" folder of your PObserve package. Check out the completed [LockServerParser](https://github.com/p-org/P/blob/dev/pobserve/Src/PObserve/Examples/LockServerPObserve/src/main/java/lockserver/pobserve/parser/LockServerParser.java) in the [LockServerPObserve](http://github.com/p-org/P/tree/dev/pobserve/Src/PObserve/Examples/LockServerPObserve) package.
91-
92-
Building the PObserve package will include the parser in the generated uber JAR which can then be used with PObserve.
88+
Refer to the completed [LockServerParser](https://github.com/p-org/P/blob/dev/pobserve/Src/PObserve/Examples/LockServerPObserve/src/main/java/lockserver/pobserve/parser/LockServerParser.java) in the [LockServerPObserve](http://github.com/p-org/P/tree/dev/pobserve/Src/PObserve/Examples/LockServerPObserve) package.

0 commit comments

Comments
 (0)