Merge branch 'dev/pexplicit_checker' into dev/aman

.github/workflows/publishdocs.yml

@@ -1,7 +1,9 @@
 name: Publish Docs
 on:
   push:
-    branches: [ main ]
+    branches: [ master ]
+  workflow_dispatch:
+
 permissions:
   contents: write
 jobs:

.github/workflows/release.yml

@@ -11,7 +11,7 @@ on:
         description: Additional arguments
         default: ""
         required: false
-        
+
 jobs:
   Release:
     name: P release

.gitignore

@@ -241,7 +241,7 @@ Tst/temp_builds/*
 target/
 *.class
 
-#Mkdocs 
+#Mkdocs
 site/
 
 # Output

Bld/Deps/cvc5/cvc5-0.0.7-v5.pom

@@ -5,7 +5,7 @@
       <artifactId>cvc5</artifactId>
       <version>0.0.7-v5</version>
       <packaging>jar</packaging>
-     
+
       <name>CVC5 Java Bindings</name>
       <description>CVC5 Java Bindings</description>
       <url>https://github.com/cvc5/cvc5</url>
@@ -15,15 +15,15 @@
           <url>${project.url}</url>
         </developer>
       </developers>
-     
+
       <licenses>
         <license>
           <url>${project.url}</url>
         </license>
       </licenses>
-     
+
       <scm>
         <url>${project.url}</url>
       </scm>
-     
+
     </project>

Bld/Deps/monosat/monosat-1.6.0-v5.pom

@@ -5,7 +5,7 @@
       <artifactId>monosat</artifactId>
       <version>1.6.0-v5</version>
       <packaging>jar</packaging>
-     
+
       <name>MonoSAT Java Bindings</name>
       <description>MonoSAT Java Bindings</description>
       <url>https://github.com/sambayless/monosat</url>
@@ -15,15 +15,15 @@
           <url>${project.url}</url>
         </developer>
       </developers>
-     
+
       <licenses>
         <license>
           <url>${project.url}</url>
         </license>
       </licenses>
-     
+
       <scm>
         <url>${project.url}</url>
       </scm>
-     
+
     </project>

Bld/Deps/pjbdd/pjbdd-1.0.10-10-v5.pom

@@ -5,7 +5,7 @@
       <artifactId>pjbdd</artifactId>
       <version>1.0.10-10-v5</version>
       <packaging>jar</packaging>
-     
+
       <name>PJBDD Java Bindings</name>
       <description>PJBDD Java Bindings</description>
       <url>https://gitlab.com/sosy-lab/software/paralleljbdd/</url>
@@ -15,15 +15,15 @@
           <url>${project.url}</url>
         </developer>
       </developers>
-     
+
       <licenses>
         <license>
           <url>${project.url}</url>
         </license>
       </licenses>
-     
+
       <scm>
         <url>${project.url}</url>
       </scm>
-     
+
     </project>

Bld/Deps/yices/yices-1.0-v5.pom

@@ -5,7 +5,7 @@
       <artifactId>yices</artifactId>
       <version>1.0-v5</version>
       <packaging>jar</packaging>
-     
+
       <name>Yices 2 Java Bindings</name>
       <description>Yices 2 Java Bindings</description>
       <url>https://github.com/aman-goel/yices2_java_bindings</url>
@@ -15,15 +15,15 @@
           <url>${project.url}</url>
         </developer>
       </developers>
-     
+
       <licenses>
         <license>
           <url>${project.url}</url>
         </license>
       </licenses>
-     
+
       <scm>
         <url>${project.url}</url>
       </scm>
-     
+
     </project>

Bld/Deps/z3/z3-4.8.14-v5.pom

@@ -5,7 +5,7 @@
       <artifactId>z3</artifactId>
       <version>4.8.14-v5</version>
       <packaging>jar</packaging>
-     
+
       <name>Z3 Java Bindings</name>
       <description>Z3 Java Bindings</description>
       <url>https://github.com/Z3Prover/z3</url>
@@ -15,13 +15,13 @@
           <url>${project.url}</url>
         </developer>
       </developers>
-     
+
       <licenses>
         <license>
           <url>${project.url}</url>
         </license>
       </licenses>
-     
+
       <scm>
         <url>${project.url}</url>
       </scm>

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) {

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.
 

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