Description
The documentation needs a complete rewrite. Frankly, it's substandard. The whole thing reeks of Microsoft-was-here.
My big issue. 99% of the time the spec is tested it'll fail. So the documentation had better be darn clear what it does, how it does it so the context of failures is stunningly clear. Consider:
machine A { ... stmt1; stmt2; .... }
machine B { ... stmt1; stmt2; .... }
In the SPIN model checker (www.spinroot.com) it is clear every possible interleaving of these statements is run against safety and liveness checks. (The SPIN equivalent of machine is proc). Just because A.stmt1 is done does not mean A.stmt2 will start or, in corner cases, will ever run. Model writers are clear how statements are run, and need not run.
Now I guess that's what P does too, which is great. However, documentation needs to run this down in detail.
For example, a critical difference between TLA/SPIN checkers and P is P uses one unbounded FIFO queue for events. TLA/SPIN allow programmers to make multi-channels and send/recv in those channels as needed. In consequence SPIN/TLA model writers always know what kind of event could be dequeued before it is dequeued.
This matters greatly. Consider this P error:
<StateLog> Client(5) enters state 'NewRPC'.
<DequeueLog> 'Client(5)' dequeued event 'ClientRXEvent with payload (...)' in state 'NewRPC'.
<StateLog> Client(5) exits state 'NewRPC'.
<PopLog> Client(5) popped state NewRPC due to unhandled event 'ClientRXEvent'.
<ExceptionLog> Client(5) running action '' in state 'NewRPC' threw exception 'UnhandledEventException'.
<ErrorLog> Client(5) received event 'PImplementation.ClientRXEvent' that cannot be handled.
Every ``NewRPC" event handler ends with a goto statement that would handle "ClientRXEvent". So, reading between the lines, it looks like the P model checker is able to run some event handler code in some interleaving and, before it gets to the "goto", dequeues the next event due to interleaving. It's an error if the current state does not have a handler for it.
Therefore model writers need be careful every state has a handler for every possible de-queuable event which, in turn, needs to better motivate how states should be done. Implementing one state with every possible event handler may not be the intent P has. Implementing distinct orthogonal states seems like P intent, but it must come with the caveat that each state must still handle every possible de-queueable event.
P provides one FIFO queue per machine. Knowing the current state cannot and does not allow one to reason which event handlers are needed or could be eliminated. If I am error here, let me know so I can learn what I missed.
That's one interpretation. Another interpretation is there's a bug. The log says it left NewRPC and is in NewRPC. That's a bit argumentative on my part; in truth I give P the benefit of doubt. It looks like NewRPC dequeued an event it has no handler for, then some sort of exception was raised, and during that noise it exited NewRPC which created the log entry. I doubt this is a bug in fact and is a misunderstanding on my part.
Assuming that's the case we can just stick with composing the following documentation for the win:
- here's how P runs statements in event handlers (detailed, clear, thorough) including needed back ground on interleaving or whatever P does ...
- Point out P is an actor model: communication between actors (implemented as machines) is through messages.
- A model transitions between states as a consequence of messages
- Each machine has one unbounded FIFO queue
- A P machine can dequeue anything sent to it (a machine under test) at any time (see (1))
- Each state must handle any message that could be dequeued
- Consequently model writers must carefully come up with distinct states, that yet handle all possible events avoiding the extremes of 1 state handling all events, and N states all handling all events
Let's hit a few smaller points:
# P/Tutorial/1_ClientServer
ClientServer.pproj
PCheckerOutput
PGenerated
PSpec
PSrc
PTst
portfolio-config.json
Why on earth is every directory prefixed with 'P'? We already know it's the P language. Next, put all the darn .p files in one directory. There's absolutely no need to split the handful of .p files in 87 places. PGenerated, PCheckerOutput are output artifacts. Why are they in the repo? UNIX uses lower-cased (not camel case) directories and seems to do just fine.
Here's what I have:
test.pproj
src
Why in the heck is the code littered here and there with this?
manual/statements.md: kotlin
manual/statements.md: java
It looks like it's for the maintainers not users. What's in scope here is P-lang and C# if I need foreign functions. That's all I want to see.
Eliminate all circular explanations; it's noise that does not clarify:
#### Defer
An event can be deferred in a state. Defer basically defers the dequeue of the event `E` in state `S` until the machine transitions to a non-deferred state, i.e., a state that does not defer the event `E`. The position of the event `E` that is deferred in state `S` does not change the FIFO buffer of the machine.
Formatting. A lot of the code is an eye-sore:
/**************************************************************************
GuaranteedWithDrawProgress checks the liveness (or progress) property that all withdraw requests
submitted by the client are eventually responded.
***************************************************************************/
Professional code keeps text to 80 chars or maybe 120. Pick one of the following methods:
/*
GuaranteedWithDrawProgress checks the liveness (or progress) property
that all withdraw requests submitted by the client are eventually responded.
*/
// GuaranteedWithDrawProgress checks the liveness (or progress) property
// that all withdraw requests submitted by the client are eventually responded.
Naming: why is it necessary to prepend a lot of variables and all/most of the types with helper prefixes
so we can know what it is?
on eWithDrawResp do (resp: tWithDrawResp) {
I don't need to be reminded eWithDrawResp is an event. It's already preceded by on. Get rid of the 'e' or suffix it with "Event". Ditto tWithDrawResp: we already know this is a typed language, and type follows a formal variable name.
A few other items:
-
dgml format? This is some one-off corner case graph format that lives primarily in the world of Microsoft. I have zero interest in downloading Visual Studio to look at a file, which is the easiest way to accomplish this task. AT&T dot format is the first thing that should have been done unless there is a fantastic reason dgml is needed. Dot is universal.
-
The antl lexer/parser is brittle; I can look past that for now.
-
Where is the state count? TLA+ and Spin are the two obvious points of comparison. They tell me state size.
-
P is missing bitwise &, |, <<. >>, and ~ ... and cannot be implemented as foreign functions. See other issue for my update there.
Now, to not end on a negative note: there are several very nice things in P (actor model, state transitions) that is really good. I will not go into details now, however, the idea of P is clearly better for software engineers compared to TLA+/Lean/Coq/HOL/Isabelle and others. SPIN is a near second best except it lacks maps/sets. But SPIN documentation, and all its secondary resources including academic papers/books are superb.
Still, P deserves plaudits for its operational usefulness in theory. We just need the support to catch-up. We want the MIT approach: 49% book smart (in terms of model checking implementation) and 51% doing where book smarts shine if and only if it can be done in practice. Mind (book smarts) v. body (doing & practice) are permanently entangled in the other. The MIT approach is just to give that extra nod to doing through operational effectiveness.