How to use this example
We assume that you have cloned the P repository locally.
git clone https://github.com/p-org/P.git
The recommended way to work through this example is to open the P/Tutorial folder in IntelliJ side-by-side a browser using which you can simultaneously read the description for each example and browse the P program in IntelliJ.
To know more about the P language primitives used in the example, please look them up in the language manual.
We have reached the middle of our tutorials , it's time to take a break and have an espresso coffee!
P has been used in the past to implement device drivers and robotics systems (see case studies and publications). One of the many challenges in implementing such systems is that they are reactive and hence, must handle arbitrary sequences of events (inputs) appropriately depending on their current mode of operation.
System: We consider a fun example of modeling an espresso coffee machine and see how we can use P state machines to model a reactive system that must respond correctly to various user inputs. The user interacts with the coffee machine through its control panel. So the Espresso machine basically consists of two parts: the front-end control panel and the backend coffee maker that actually makes the coffee.
The control panel presents an interface to the user to perform operations like
reset machine, turn
steamer on and off, request an
espresso, and clear the
grounds by opening the container. The control panel interprets these inputs from the user and sends appropriate commands to the coffee maker.
By default, the P checker tests whether any event that is received in a state has a handler defined for it, otherwise, it would result in an unhandled event exception. If the P checker fails to find a bug then it implies that the system model can handle any sequence of events generated by the given environment which in our example's context implies that the coffee machine control panel can appropriately handle any sequence of inputs (button presses) by the user. We would also like to check that the coffee machine moves through a desired sequence of states, i.e.,
WarmUp -> Ready -> GrindBeans -> MakeCoffee -> Ready.
The P models (PSrc) for the EspressoMachine example consist of three files:
- CoffeeMakerControlPanel.p: Implements the CoffeeMakerControlPanel state machine. Basically, the control panel starts in the initial state and kicks off by warming up the coffee maker. After warming is successful, it moves to the ready state where it can either make coffee or start the steamer. When asked to make coffee, it first grinds the beans and then brews coffee. In any of these states, if there is an error due to. e.g, no water or no beans, the control panel informs the user of the error and moves to the error state waiting for the user to reset the machine.
[Expand]: Let's walk through CoffeeMakerControlPanel.p
- (L2 - L19) → Declare events that are used to communicate between the
ControlPanelmachines (manual: event declaration). These are events that represent the operations performed by the user, e.g., resetting the machine, pressing the steamer button on and off, etc.
- (L34 - L231) → Declares the
CoffeeMakerControlPanelstate machine. The interesting points that we would like to highlight are: (1) the state machine transitions from one mode (or state) to another based on the events received from the user and the
CoffeeMakermachine; (2) in all the states, the state machine appropriately handles different events that can be received, including ignoring or deferring them if they are stale events.
- CoffeeMaker.p: Implements the CoffeeMaker state machine.
[Expand]: Let's walk through CoffeeMaker.p
- (L4 - L29) → Declares the events used to communicate between the control panel and the backend coffee maker.
- (L31 - L78) → Declares the
EspressoCoffeeMakermachine. EspressoCoffeeMaker receives requests from the control panel of the coffee machine and based on its state e.g., whether heater is working, or it has beans and water, the coffee maker responds nondeterministically back to the controller if the operation succeeded or errored.
- EspressoMachineModules.p: Declares the P module corresponding to EspressoMachine.
The P Specification (PSpec) for the EspressoMachine example is implemented in Safety.p. We define a safety specification
EspressoMachineModesOfOperation that observes the internal state of the EspressoMachine through the events that are announced as the system moves through different states and asserts that it always moves through the desired sequence of states. Steady operation:
WarmUp -> Ready -> GrindBeans -> MakeCoffee -> Ready. If an error occurs in any of the states above then the EspressoMachine stays in the error state until
it is reset and after which it returns to the
[Expand]: Let's walk through Safety.p
- (L1 - L7) → Events used to inform the monitor about the state of the EspressoMachine system. The events are announced as the system moves from one state to another (manual: announce statement).
EspressoMachineModesOfOperationspec machine observes these events and ensures that the system moves through the states defined by the monitor. Note that if the system allows (has execution as) a sequence of events that are not accepted by the monitor (i.e., the monitor throws an unhandled event exception) then the system does not satisfy the desired specification. Hence, this monitor can be thought of accepting only those behaviors of the system that follow the sequence of states modelled by the spec machine. For example, if the system moves from Ready to CoffeeMaking state directly without Grinding then the monitor will raise an ALARM!
- To understand the semantics of the P spec machines, please read manual: p monitors.
The test scenarios folder in P has two parts: TestDrivers and TestScripts. TestDrivers are collections of state machines that implement the test harnesses (or environment state machines) for different test scenarios. TestScripts are collections of test cases that are automatically run by the P checker.
The test scenarios folder for EspressoMachine (PTst) consists of three files: TestDriver.p and TestScript.p are just like other previous examples. The User.p declares two machines: (1) a
SaneUser machine that uses the EspressoMachine with care, pressing the buttons in the right order, and cleaning up the grounds after the coffee is made; and (2) a
CrazyUser machine who has never used an espresso machine before, gets too excited, and starts pushing random buttons on the control panel.
Run the following command to compile the project:
---------------------------------------- ==== Loading project file: EspressoMachine.pproj ....... includes p file: P/Tutorial/3_EspressoMachine/PSrc/CoffeeMaker.p ....... includes p file: P/Tutorial/3_EspressoMachine/PSrc/CoffeeMakerControlPanel.p ....... includes p file: P/Tutorial/3_EspressoMachine/PSrc/EspressoMachineModules.p ....... includes p file: P/Tutorial/3_EspressoMachine/PSpec/Safety.p ....... includes p file: P/Tutorial/3_EspressoMachine/PTst/Users.p ....... includes p file: P/Tutorial/3_EspressoMachine/PTst/TestDrivers.p ....... includes p file: P/Tutorial/3_EspressoMachine/PTst/TestScripts.p ---------------------------------------- ---------------------------------------- Parsing .. Type checking ... Code generation .... Generated EspressoMachine.cs ---------------------------------------- Compiling EspressoMachine.csproj .. Microsoft (R) Build Engine version 16.10.2+857e5a733 for .NET Copyright (C) Microsoft Corporation. All rights reserved. Determining projects to restore... All projects are up-to-date for restore. EspressoMachine -> P/Tutorial/3_EspressoMachine/POutput/netcoreapp3.1/EspressoMachine.dll Build succeeded. 0 Warning(s) 0 Error(s)
You can get the list of test cases defined in the EspressoMachine program by passing the generated
to the P Checker:
pmc <Path>/EspressoMachine.dll Provide /method or -m flag to qualify the test method name you wish to use. Possible options are:: PImplementation.tcSaneUserUsingCoffeeMachine.Execute PImplementation.tcCrazyUserUsingCoffeeMachine.Execute
There are two test cases defined in the EspressoMachine project and you can specify which
test case to run by using the
-m parameter along with the
-i parameter for the number of schedules to explore.
tcSaneUserUsingCoffeeMachine test case for 10000 schedules:
pmc <Path>/EspressoMachine.dll \ -m PImplementation.tcSaneUserUsingCoffeeMachine.Execute \ -i 10000
tcCrazyUserUsingCoffeeMachine test case for 10000 schedules:
pmc <Path>/EspressoMachine.dll \ -m PImplementation.tcCrazyUserUsingCoffeeMachine.Execute \ -i 10000
- [Problem 1] Note that the current safety specification
CoffeeMakerModesOfOperationdoes not capture the case where the CoffeeMaker can move to GroundsOpen and GroundsClosed state. Extend the spec to cover those modes of operations as well.
Can you think of other cases where you would like to check that your system evolves through a certain sequence of states? Or that it allows only those executions which follow a pattern? Can these be specified as P monitors? If not, what are the challenges? A typical example of such cases is when for files in a storage system the sequence of operations that must succeed need to have a pattern of the form: open → read* → close; and similarly, for lock services, lockAcquire → readSuccess → lockReleased. More interestingly, you can also check things like: AuthenticationSuccess(x) → ReadSuccess(x), and never see a case of AuthenticationFailure(x) → ReadSuccess(x) in your executions! What do you think? Post your comments in the github discussions.
What did we learn through this example?
This was a fun example to demonstrate how to model a reactive system using P state machines. We saw how using P monitors allows us to check that the system moves through the correct modes of operation and that the executions only allow certain patterns.