diff --git a/.github/workflows/publishdocs.yml b/.github/workflows/publishdocs.yml index ac3e21117..348f0038d 100644 --- a/.github/workflows/publishdocs.yml +++ b/.github/workflows/publishdocs.yml @@ -1,7 +1,9 @@ name: Publish Docs on: push: - branches: [ main ] + branches: [ master ] + workflow_dispatch: + permissions: contents: write jobs: diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 17f29b3b4..bed46e38c 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -11,7 +11,7 @@ on: description: Additional arguments default: "" required: false - + jobs: Release: name: P release diff --git a/.gitignore b/.gitignore index 359fe07e2..f3310943e 100644 --- a/.gitignore +++ b/.gitignore @@ -241,7 +241,7 @@ Tst/temp_builds/* target/ *.class -#Mkdocs +#Mkdocs site/ # Output diff --git a/Bld/Deps/cvc5/cvc5-0.0.7-v5.pom b/Bld/Deps/cvc5/cvc5-0.0.7-v5.pom index b90ec95f5..c4452051c 100644 --- a/Bld/Deps/cvc5/cvc5-0.0.7-v5.pom +++ b/Bld/Deps/cvc5/cvc5-0.0.7-v5.pom @@ -5,7 +5,7 @@ cvc5 0.0.7-v5 jar - + CVC5 Java Bindings CVC5 Java Bindings https://github.com/cvc5/cvc5 @@ -15,15 +15,15 @@ ${project.url} - + ${project.url} - + ${project.url} - + \ No newline at end of file diff --git a/Bld/Deps/monosat/monosat-1.6.0-v5.pom b/Bld/Deps/monosat/monosat-1.6.0-v5.pom index 130979e87..b5c4aeb95 100644 --- a/Bld/Deps/monosat/monosat-1.6.0-v5.pom +++ b/Bld/Deps/monosat/monosat-1.6.0-v5.pom @@ -5,7 +5,7 @@ monosat 1.6.0-v5 jar - + MonoSAT Java Bindings MonoSAT Java Bindings https://github.com/sambayless/monosat @@ -15,15 +15,15 @@ ${project.url} - + ${project.url} - + ${project.url} - + \ No newline at end of file diff --git a/Bld/Deps/pjbdd/pjbdd-1.0.10-10-v5.pom b/Bld/Deps/pjbdd/pjbdd-1.0.10-10-v5.pom index 5ccc394e2..f2ee7559e 100644 --- a/Bld/Deps/pjbdd/pjbdd-1.0.10-10-v5.pom +++ b/Bld/Deps/pjbdd/pjbdd-1.0.10-10-v5.pom @@ -5,7 +5,7 @@ pjbdd 1.0.10-10-v5 jar - + PJBDD Java Bindings PJBDD Java Bindings https://gitlab.com/sosy-lab/software/paralleljbdd/ @@ -15,15 +15,15 @@ ${project.url} - + ${project.url} - + ${project.url} - + \ No newline at end of file diff --git a/Bld/Deps/yices/yices-1.0-v5.pom b/Bld/Deps/yices/yices-1.0-v5.pom index 55f7d8d3c..dd6b4c6f7 100644 --- a/Bld/Deps/yices/yices-1.0-v5.pom +++ b/Bld/Deps/yices/yices-1.0-v5.pom @@ -5,7 +5,7 @@ yices 1.0-v5 jar - + Yices 2 Java Bindings Yices 2 Java Bindings https://github.com/aman-goel/yices2_java_bindings @@ -15,15 +15,15 @@ ${project.url} - + ${project.url} - + ${project.url} - + \ No newline at end of file diff --git a/Bld/Deps/z3/z3-4.8.14-v5.pom b/Bld/Deps/z3/z3-4.8.14-v5.pom index dcf55086e..ef97f33e0 100644 --- a/Bld/Deps/z3/z3-4.8.14-v5.pom +++ b/Bld/Deps/z3/z3-4.8.14-v5.pom @@ -5,7 +5,7 @@ z3 4.8.14-v5 jar - + Z3 Java Bindings Z3 Java Bindings https://github.com/Z3Prover/z3 @@ -15,13 +15,13 @@ ${project.url} - + ${project.url} - + ${project.url} diff --git a/Docs/docs/advanced/p2c.md b/Docs/docs/advanced/p2c.md index 47c24c52b..12629f466 100644 --- a/Docs/docs/advanced/p2c.md +++ b/Docs/docs/advanced/p2c.md @@ -99,7 +99,7 @@ int main(int argc, char *argv[]) { processGuid.data3 = 0; processGuid.data4 = 0; MAIN_P_PROCESS = PrtStartProcess(processGuid, &P_GEND_IMPL_DefaultImpl, ErrorHandler, Log); - + if (cooperative) { PrtSetSchedulingPolicy(MAIN_P_PROCESS, PRT_SCHEDULINGPOLICY_COOPERATIVE); } @@ -113,12 +113,12 @@ int main(int argc, char *argv[]) { PrtUpdateAssertFn(MyAssert); PRT_UINT32 machineId; PRT_BOOLEAN foundMainMachine = PrtLookupMachineByName("myMachine", &machineId); - + if (foundMainMachine == PRT_FALSE) { printf("%s\n", "FAILED TO FIND DroneMachine"); exit(1); } - + PrtMkMachine(MAIN_P_PROCESS, machineId, 1, &payload); if (cooperative) { diff --git a/Docs/docs/advanced/psemantics.md b/Docs/docs/advanced/psemantics.md index 48511eccc..e1eca6a28 100644 --- a/Docs/docs/advanced/psemantics.md +++ b/Docs/docs/advanced/psemantics.md @@ -2,18 +2,18 @@ Before getting started with the tutorials, we provide a quick informal overview **P is a programming language.** P is a state machine based _programming language_ and hence, just like any other imperative programming language it supports basic [data types](../manual/datatypes.md), [expressions](../manual/expressions.md), and [statements](../manual/statemachines.md) that enable programmers to capture complex distributed systems protocol logic as a collection of event-handlers or [functions](../manual/functions.md) (in P state machines). -**P State machines.** The underlying model of computation for P state machines is similar to that of [Gul Agha's](http://osl.cs.illinois.edu/members/agha.html) [Actor-model-of-computation](https://dspace.mit.edu/handle/1721.1/6952) ([wiki](https://en.wikipedia.org/wiki/Actor_model)). A P program is a collection of concurrently executing state machines that communicate with eachother by sending events (or messages) asynchronously. Each P state machine has an **unbounded FIFO buffer** associated with it. -Sends are **asynchronous**, i.e., executing a send operation `send t,e,v;` adds event `e` with payload value `v` into the FIFO buffer of the target machine `t`. +**P State machines.** The underlying model of computation for P state machines is similar to that of [Gul Agha's](http://osl.cs.illinois.edu/members/agha.html) [Actor-model-of-computation](https://dspace.mit.edu/handle/1721.1/6952) ([wiki](https://en.wikipedia.org/wiki/Actor_model)). A P program is a collection of concurrently executing state machines that communicate with eachother by sending events (or messages) asynchronously. Each P state machine has an **unbounded FIFO buffer** associated with it. +Sends are **asynchronous**, i.e., executing a send operation `send t,e,v;` adds event `e` with payload value `v` into the FIFO buffer of the target machine `t`. Each state in the P state machine has an entry function associated with it which gets executed when the state machine enters that state. After executing the entry -function, the machine tries to dequeue an event from the input buffer or blocks if the buffer is empty. Upon dequeuing an event from the input queue of the machine, the attached handler is executed which might transition the machine to a different state. We will provide more details about the P state machines in tutorials as well as the language manual. +function, the machine tries to dequeue an event from the input buffer or blocks if the buffer is empty. Upon dequeuing an event from the input queue of the machine, the attached handler is executed which might transition the machine to a different state. We will provide more details about the P state machines in tutorials as well as the language manual. For detailed formal semantics of P state machines, we refer the readers to the [original P paper](https://ankushdesai.github.io/assets/papers/p.pdf) and the [more recent paper](https://ankushdesai.github.io/assets/papers/modp.pdf) with updated semantics. -There are **two main distinctions** with actor model of computation: (1) P adds the **syntactic sugar** of state machines to actors, and (2) each state machine in P has an **unbounded FIFO buffer** associated with it instead of an unbounded bag in actors (semantic difference). +There are **two main distinctions** with actor model of computation: (1) P adds the **syntactic sugar** of state machines to actors, and (2) each state machine in P has an **unbounded FIFO buffer** associated with it instead of an unbounded bag in actors (semantic difference). !!! danger "[Important] Send semantics in P" Sends are reliable, buffered, non-blocking, and directed (not broadcast). Sends are **reliable** i.e., executing a send operation in P adds an event into the target machines buffer. Hence, if one wants to model message loss it has to be modeled explicitly (discussed in the Failure Detector example in the tutorial). Similarly, as P state machine buffers are FIFO, events are dequeued at the state machine in the **causal order** in which they were sent. Note that events that are sent by two different concurrent machines will be interleaved by the checker and hence, will appear in different order at the target machine but the events sent by the same machine will always appear in the same order at the target state machine. So, just like message loss, arbitrary message re-ordering also has to be explicitly modeled in P (explained in the Paxos example in the tutorials). In general, we find that re-ordering messages/events coming from the same machine is not important and does not lead to any interesting behaviors. More interesting behaviors happen because of interleaving of messages across different state machines which the P checker explores automatically. - Summary, by default, the communication between state machines using `send` operation follows the above semantics. If you would like to check your system correctness against an arbitrarily network then one would have to model the corresponding `send` semantics in P explicitly. One can then make the arbitrarily network behave as expected with message duplicates, loss, re-order, etc. + Summary, by default, the communication between state machines using `send` operation follows the above semantics. If you would like to check your system correctness against an arbitrarily network then one would have to model the corresponding `send` semantics in P explicitly. One can then make the arbitrarily network behave as expected with message duplicates, loss, re-order, etc. If you have any further doubts related to this topic and modeling network semantics when reasoning using P, feel free to get in touch with Ankush Desai. We have several examples of such cases. diff --git a/Docs/docs/advanced/psym/install.md b/Docs/docs/advanced/psym/install.md index 368a3d5a9..b65bda624 100644 --- a/Docs/docs/advanced/psym/install.md +++ b/Docs/docs/advanced/psym/install.md @@ -1,7 +1,7 @@ PSym is built to be cross-platform and can be used on MacOS, Linux, and Windows. ### [Steps 1 to 5] Install P -Follow the instructions on installing P from [Installing P](../../getstarted/install.md) +Follow the instructions on installing P from [Installing P](../../getstarted/install.md) (at least up to and including [Step 3](../../getstarted/install.md#step-3-install-p-compiler)) ### [Step 6] Install Maven @@ -17,12 +17,12 @@ To install Maven use: brew install maven ``` - Dont have Homebrew? Directly use [installer](https://maven.apache.org/install.html). + Dont have Homebrew? Directly use [installer](https://maven.apache.org/install.html). === "Ubuntu" Installing Maven on Ubuntu ([details](https://phoenixnap.com/kb/install-maven-on-ubuntu)) - + ``` sudo apt install maven ``` @@ -40,11 +40,11 @@ To install Maven use: wget https://dlcdn.apache.org/maven/maven-3/3.8.6/binaries/apache-maven-3.8.6-bin.tar.gz tar xfv apache-maven-3.8.6-bin.tar.gz ``` - + You might do this in your home directory, yielding a folder like `` /home/$USER/apache-maven-3.8.6 `` - + Next, install the software into your environment by adding it to your path, and by defining Maven's environment variables: - + ``` export M2_HOME=/home/$USER/apache-maven-3.6.3 export M2=$M2_HOME/bin diff --git a/Docs/docs/advanced/psym/usingPSym.md b/Docs/docs/advanced/psym/usingPSym.md index d6ed73dab..ddd52618e 100644 --- a/Docs/docs/advanced/psym/usingPSym.md +++ b/Docs/docs/advanced/psym/usingPSym.md @@ -1,4 +1,4 @@ -!!! check "" +!!! check "" Before moving forward, we assume that you have successfully [installed PSym](install.md) :metal: . In this section, we provide an overview of the steps involved in compiling and checking a P program with PSym @@ -47,7 +47,7 @@ Simply pass the commandline argument `-generate:PSym` when running the P compile !!! tip "Recommendation" - We recommend using the P project file `*.pproj` along with passing `-generate:PSym` as commandline argument to the compiler + We recommend using the P project file `*.pproj` along with passing `-generate:PSym` as commandline argument to the compiler to compile a P program for PSym. Commandline argument `-generate:XXX` takes priority over `YYY` in `*.pproj` file. @@ -57,7 +57,7 @@ Simply pass the commandline argument `-generate:PSym` when running the P compile ``` shell pc -proj:ClientServer.pproj -generate:PSym ``` - + ??? info "Expected Output" ``` $ pc -proj:ClientServer.pproj -generate:PSym @@ -101,7 +101,7 @@ java -jar target/ClientServer-jar-with-dependencies.jar ??? info "Expected Output" ```hl_lines="9 10 11 12" java -jar target/ClientServer-jar-with-dependencies.jar - + Picked up JAVA_TOOL_OPTIONS: -Dlog4j2.formatMsgNoLookups=true WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance. Reflections took 100 ms to scan 1 urls, producing 38 keys and 168 values @@ -137,7 +137,7 @@ java -jar target/ClientServer-jar-with-dependencies.jar \ ... Method tcSingleClient ... Project clientserver is using 'default' strategy (seed:0) -------------------- - Time Memory Coverage Schedule Remaining Depth States + Time Memory Coverage Schedule Remaining Depth States 00:00:10 0.2 GB 1.4246418994 % 140 1820 (100 % data) 1 8043 -------------------- Estimated Coverage:: 1.4246418994 % @@ -163,7 +163,7 @@ java -jar target/ClientServer-jar-with-dependencies.jar \ ### Coverage At the end of a run, PSym reports a coverage metric as an estimated percentage of the execution tree that is explored during -the run. Assuming a uniform probability for each scheduling/data choice, this metric reports the probability of a +the run. Assuming a uniform probability for each scheduling/data choice, this metric reports the probability of a randomly-sampled schedule to be bug free. ??? info "Continuous Feedback" @@ -171,14 +171,14 @@ randomly-sampled schedule to be bug free. During the run, PSym prints useful metrics that summarizes the current status of the run. For example, for the ClientServer run above, PSym prints: - + ``` - Time Memory Coverage Schedule Remaining Depth States + Time Memory Coverage Schedule Remaining Depth States 00:00:10 0.2 GB 1.4246418994 % 140 1820 (100 % data) 1 8043 ``` - + that summarizes: - + | Label | Description | |-----------|----------------------------------------------------------------------------------| | Time | Elapsed runtime in ``hh:mm:ss`` format | @@ -194,20 +194,20 @@ randomly-sampled schedule to be bug free. Sadly, No :pensive:! - PSym's coverage metric is **not** a perfect state-space coverage metric. - This metric gives more weightage to shorter schedules, or more precisely, schedules with fewer schedule/data + PSym's coverage metric is **not** a perfect state-space coverage metric. + This metric gives more weightage to shorter schedules, or more precisely, schedules with fewer schedule/data choices at shallower search depths. - Therefore, a PSym run can quickly reach a high estimated coverage (> 99 %) due to exploring shorter schedules + Therefore, a PSym run can quickly reach a high estimated coverage (> 99 %) due to exploring shorter schedules first, after which gaining the remaining left-over percentage can become increasingly (and exponentially) difficult. - + Our recommendation is to target achieving coverage up to 11 nines, i.e., 99.999999999 % to be sufficiently confident of the absence of bug. - Additionally, check PSym's Coverage Report (`` output/coverage-*.log ``) to understand the state-space covered + Additionally, check PSym's Coverage Report (`` output/coverage-*.log ``) to understand the state-space covered during the run, as well as the number of distinct states explored. -At the end of a run, PSym also prints a coverage report in `` output/coverage-*.log `` that tabulates, for each -exploration step/depth, the number of schedule/data choices explored during the run, along with the number of +At the end of a run, PSym also prints a coverage report in `` output/coverage-*.log `` that tabulates, for each +exploration step/depth, the number of schedule/data choices explored during the run, along with the number of choices remaining as unexplored backtracks. For example, coverage report corresponding to the previous ClientServer run can be found in `` output/coverage-clientserver.log `` @@ -226,21 +226,21 @@ For example, coverage report corresponding to the previous ClientServer run can Depth Covered Remaining sch data sch data ------------------------------------- - 0 100 - 1 100 + 0 100 + 1 100 2 100 134 5806 - 3 135 - 4 134 - 5 134 - 6 134 + 3 135 + 4 134 + 5 134 + 6 134 7 134 50 1162 8 134 77 2659 - 9 127 - 10 127 + 9 127 + 10 127 11 127 36 559 12 127 48 1045 13 124 36 1149 - 14 120 + 14 120 15 120 23 296 16 120 36 621 17 114 34 766 @@ -283,9 +283,9 @@ For example, coverage report corresponding to the previous ClientServer run can ``` ??? tip "Improving Coverage for ClientServer" - Looks like the ClientServer example is quite data heavy, since there are lots of unexplored data choices at different steps + Looks like the ClientServer example is quite data heavy, since there are lots of unexplored data choices at different steps (check the rightmost column of `` output/coverage-clientserver.log ``). - A good idea is to reduce the amount of data non-determinism by reducing the number of choices in the + A good idea is to reduce the amount of data non-determinism by reducing the number of choices in the `choose(*)` expressions, such as the number of data choices in setting the initial bank balances in expression `choose(100)` [here](https://github.com/p-org/P/blob/master/Tutorial/1_ClientServer/PTst/TestDriver.p#L30). @@ -315,7 +315,7 @@ For a complete list of options, pass the argument ` --help `. ??? tip "Exploration Techniques" PSym implements a collection of configurable techniques summarized as follows: - + | Technique | Description | |-----------------------|-------------------------------------------------------------------------------------| | Search Strategy | Configure the order in which search is performed: `astar`, `random`, `dfs`, `learn` | @@ -328,7 +328,7 @@ For a complete list of options, pass the argument ` --help `. !!! info "Preconfigured Modes" For ease of usage, PSym provides a set of preconfigured exploration modes as follows: - + | Mode | Description | |-----------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| | `default` | Explore single execution at a time
Search Strategy = `astar`
Choice Selection = `random`
Never Repeat States = `ON`
Stateful Backtracking = `ON`
BMC = `OFF` | @@ -336,7 +336,7 @@ For a complete list of options, pass the argument ` --help `. | `fuzz` | Explore like a random fuzzer (but never repeat an execution!)
Search Strategy = `random`
Choice Selection = `random`
Never Repeat States = `OFF`
Stateful Backtracking = `OFF`
BMC = `OFF` | | `dfs` | Explore single executions at a time in depth-first manner
Search Strategy = `dfs`
Choice Selection = `random`
Never Repeat States = `ON`
Stateful Backtracking = `ON`
BMC = `OFF` | | `learn` | Explore single execution at a time with learning
Search Strategy = `learn`
Choice Selection = `learn`
Never Repeat States = `ON`
Stateful Backtracking = `ON`
BMC = `OFF` | - + Pass the CLI argument ` --mode