[PSym] Upgrades v0.5.8 (#547)

* [PSym] Improved support for Java foreign functions

Adds PMachineValue to PSym Java FFI

Corrects PSym compilation for FFI

* [PSym] Refactoring package

* [PSym] Update compiler to use latest PSym version by default

* [PSym] Add maven release GitHub action

* [CI] Update maven publish GitHub action

* [CI] Update maven release action

* [CI] Add gpg signing to maven publish action

* [CI] Minor update

* [PSym] Check monitors at event send (instead of at the start of handling)

Also updates machine id to be globally unique

* [CI] Adds manual action trigger

* [PSym] Update version number

* [PSym] Update Maven publish action

Trying with a separate step for gpg import

* [PSym] Trying correcting gpg import error in Maven action

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Trying correcting gpg import error

* [PSym] Cleaning up

* [PSym] Reset maven publish action to use default setup-java with gpg

* [PSym] Update pom

* [PSym] Update replayer when target is halted

* [PSym] Add parsing config file psym-config.json

Adds parsing config file to PSym. Right now, supports passing sync-events only.

* [PSym] Minor update

* [PSym] Report error if putting key-value in map already containing key

Changes PSym compiler target program name to avoid naming conflict

* [PSym] Minor update

* [PSym] Throw map KeyAlreadyPresent exception only for InsertStmt (not for MapAccess)

* [PSym] Minor changes

* [PSym] Update liveness checking for iterative symbolic exploration

Corrects checking if iteration finished due to reaching end of execution(s) for iterative symbolic exploration

* [PSym] Update CLI modes

* [PSym] Report map operation errors as cex

Report adding key-value to already-present key as cex

Report fetching for absent key in map as cex

Updates mapVS add, get, and getOrDefault operators to correctly handle errors dealing with already-present or missing keys

* [PSym] Bump PSym development version

* [PSym] Updates liveness checking

Updates liveness checking to correctly deal with checking during iterative BMC

Minor refactoring

.github/workflows/maven-publish.yml

@@ -1,39 +1,32 @@
 # This workflow will build a package using Maven and then publish it to GitHub packages when a release is created
 # For more information see: https://github.com/actions/setup-java/blob/main/docs/advanced-usage.md#apache-maven-with-a-settings-path
 
-name: Maven Package
+name: Maven Publish
 
 on:
-  release:
-    types: [created]
+  push:
+    branches: [ "maven-publish-**" ]
+  workflow_dispatch:
 
 jobs:
-  build:
-
+  Maven-Publish-Ubuntu:
     runs-on: ubuntu-latest
-    permissions:
-      contents: read
-      packages: write
-
     steps:
-    - uses: actions/checkout@v3
-    - name: Set up JDK 11
-      uses: actions/setup-java@v3
-      with:
-        java-version: '11'
-        distribution: 'temurin'
-        server-id: github # Value of the distributionManagement/repository/id field of the pom.xml
-        settings-path: ${{ github.workspace }} # location for the settings.xml file
-
-    - name: Build with Maven
-      working-directory: Src/PRuntimes/PJavaRuntime
-      run: |
-        # The environment variable GITHUB_REF is refs/tags/p-*
-        VERSION=${GITHUB_REF:12}
-        mvn -B package --file pom.xml -Drevision=${VERSION}
-
-    - name: Publish to GitHub Packages Apache Maven
-      working-directory: Src/PRuntimes/PJavaRuntime
-      run: mvn deploy -s $GITHUB_WORKSPACE/settings.xml
-      env:
-        GITHUB_TOKEN: ${{ github.token }}
+      - uses: actions/checkout@v3
+      - name: Set up Java for publishing to Maven Central Repository
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'temurin'
+          java-version: '11'
+          server-id: ossrh
+          server-username: MAVEN_USERNAME
+          server-password: MAVEN_PASSWORD
+          gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }} # Value of the GPG private key to import
+          gpg-passphrase: MAVEN_GPG_PASSPHRASE # env variable for GPG private key passphrase
+      - name: Publish to the Maven Central Repository
+        working-directory: Src/PRuntimes/PSymRuntime
+        run: mvn --batch-mode deploy -P release -Dmaven.test.skip
+        env:
+          MAVEN_USERNAME: ${{ secrets.OSSRH_USERNAME }}
+          MAVEN_PASSWORD: ${{ secrets.OSSRH_TOKEN }}
+          MAVEN_GPG_PASSPHRASE: ${{ secrets.GPG_PASSPHRASE }}

.github/workflows/psym.yml

@@ -25,18 +25,19 @@ jobs:
       with:
         dotnet-version: 3.1.100
     - name: Set up JDK
-      uses: actions/setup-java@v1
+      uses: actions/setup-java@v3
       with:
-        java-version: 11
+        java-version: '11'
+        distribution: 'corretto'
     - name: Cache Maven packages
       uses: actions/cache@v2
       with:
         path: ~/.m2
         key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}
         restore-keys: ${{ runner.os }}-m2
     - name: Build PSym
-      working-directory: Src/PRuntimes/PSymbolicRuntime
+      working-directory: Src/PRuntimes/PSymRuntime
       run: ./scripts/build.sh
     - name: Test PSym
-      working-directory: Src/PRuntimes/PSymbolicRuntime
+      working-directory: Src/PRuntimes/PSymRuntime
       run: mvn test

.gitignore

@@ -251,3 +251,4 @@ output/
 out/
 !**/src/main/**/out/
 !**/src/test/**/out/
+*.iml

Docs/docs/advanced/psym/usingPSym.md

@@ -148,9 +148,9 @@ java -jar target/ClientServer-jar-with-dependencies.jar \
     Result: partially safe with 1820 backtracks remaining
     --------------------
     java.lang.Exception: TIMEOUT
-    at psymbolic.commandline.EntryPoint.process(EntryPoint.java:97)
-    at psymbolic.commandline.EntryPoint.run(EntryPoint.java:138)
-    at psymbolic.commandline.PSymbolic.main(PSymbolic.java:73)
+    at psym.commandline.EntryPoint.process(EntryPoint.java:97)
+    at psym.commandline.EntryPoint.run(EntryPoint.java:138)
+    at psym.commandline.PSym.main(PSym.java:73)
     ```
 
     Here, PSym explores 140 schedules/iterations, checking 8043 distinct states, and achieving an estimated coverage of ~ 1.4 %.

Src/PCompiler/CompilerCore/Backend/Symbolic/CompilationContext.cs

@@ -38,7 +38,7 @@ internal CompilationContext(ICompilationJob job)
                     "When generating code for the 'Symbolic' target, the project name should " +
                     "begin with an alphabetic character and contain only alphanumeric characters");
 
-            MainClassName = ProjectName;
+            MainClassName = ProjectName+"Program";
             anonFuncIds = new Dictionary<Function, int>();
             continuationNames = new Dictionary<Continuation, int>();
         }

Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs

@@ -12,7 +12,7 @@ internal class Constants
 
     <modelVersion>4.0.0</modelVersion>
 
-    <groupId>psymbolic</groupId>
+    <groupId>psym.model</groupId>
     <artifactId>projectName</artifactId>
     <version>1.0</version>
 
@@ -48,7 +48,7 @@ internal class Constants
                     <archive>
                         <manifest>
                             <addClasspath>true</addClasspath>
-                            <mainClass>psymbolic.commandline.PSymbolic</mainClass>
+                            <mainClass>psym.commandline.PSym</mainClass>
                         </manifest>
                     </archive>
                     <descriptorRefs>

Src/PCompiler/CompilerCore/Backend/Symbolic/SymbolicCodeGenerator.cs

@@ -42,7 +42,7 @@ public void Compile(ICompilationJob job)
             }
 
             // compile the csproj file
-            string[] args = new[] { "clean package -q"};
+            string[] args = new[] { "versions:use-latest-versions -DgenerateBackupPoms=false clean package -q"};
 
             int exitCode = Compiler.RunWithOutput(job.ProjectRootPath.FullName, out stdout, out stderr, "mvn", args);
             if (exitCode != 0)
@@ -56,7 +56,7 @@ public void Compile(ICompilationJob job)
                 job.Output.WriteInfo("Build succeeded.");
             }
 
-            string sourceDirectory = "target/sources/psymbolic";
+            string sourceDirectory = "target/sources/psym/model";
 
             // create source folder
             args = new[] { $"-p {sourceDirectory}" };
@@ -69,11 +69,11 @@ public void Compile(ICompilationJob job)
 
             // copy source files
             string sourceFilePath = Path.GetRelativePath(job.ProjectRootPath.FullName, job.OutputDirectory.FullName);
-            args = new[] { $"{sourceFilePath}/{job.ProjectName}.java {sourceDirectory}" };
+            args = new[] { $"{sourceFilePath}/{job.ProjectName}Program.java {sourceDirectory}" };
             exitCode = Compiler.RunWithOutput(job.ProjectRootPath.FullName, out stdout, out stderr, "cp", args);
             if (exitCode != 0)
             {
-                throw new TranslationException($"Unable to copy source file {job.ProjectName}.java to source directory {sourceDirectory}\n" + $"{stdout}\n" + $"{stderr}\n");
+                throw new TranslationException($"Unable to copy source file {job.ProjectName}Program.java to source directory {sourceDirectory}\n" + $"{stdout}\n" + $"{stderr}\n");
             }
         }
 
@@ -624,7 +624,7 @@ private void WriteForeignFunction(CompilationContext context, StringWriter outpu
             {
                 if (i > 0)
                     context.WriteLine(output, ",");
-                context.Write(output, $"({GetConcreteForeignBoxedType(param.Type)}) args.get({i})");
+                context.Write(output, $"new {GetConcreteForeignBoxedType(param.Type)}(args.get({i}))");
                 i++;
             }
             context.WriteLine(output, ");");
@@ -955,7 +955,7 @@ private void WriteStmt(Function function, CompilationContext context, StringWrit
                     WriteExpr(context, output, flowContext.pcScope, assertStmt.Assertion);
                     context.Write(output, ").getValues().contains(Boolean.FALSE), ");
                     WriteExpr(context, output, flowContext.pcScope, assertStmt.Message);
-                    context.Write(output, $", {CompilationContext.SchedulerVar}, ");
+                    context.Write(output, $", ");
                     WriteExpr(context, output, flowContext.pcScope, assertStmt.Assertion);
                     context.Write(output, ".getGuardFor(Boolean.FALSE));");
                     break;
@@ -2456,6 +2456,9 @@ private string GetConcreteForeignBoxedType(PLanguageType type)
                     return "PFloat";
                 case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.String):
                     return "PString";
+                case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Machine):
+                case PermissionType _:
+                    return "PMachineValue";
                 case ForeignType foreignType:
                     return foreignType.CanonicalRepresentation;
                 case SequenceType _:
@@ -2616,17 +2619,18 @@ private string GetDefaultValueNoGuard(CompilationContext context, PLanguageType
 
         private void WriteSourcePrologue(CompilationContext context, StringWriter output)
         {
-            context.WriteLine(output, "package psymbolic;");
-            context.WriteLine(output, "import psymbolic.commandline.*;");
-            context.WriteLine(output, "import psymbolic.valuesummary.*;");
-            context.WriteLine(output, "import psymbolic.runtime.*;");
-            context.WriteLine(output, "import psymbolic.runtime.scheduler.*;");
-            context.WriteLine(output, "import psymbolic.runtime.machine.*;");
-            context.WriteLine(output, "import psymbolic.runtime.logger.*;");
-            context.WriteLine(output, "import psymbolic.runtime.machine.buffer.*;");
-            context.WriteLine(output, "import psymbolic.runtime.machine.eventhandlers.*;");
-            context.WriteLine(output, "import psymbolic.runtime.values.*;");
-            context.WriteLine(output, "import psymbolic.utils.*;");
+            context.WriteLine(output, "package psym.model;");
+            context.WriteLine(output);
+            context.WriteLine(output, "import psym.commandline.*;");
+            context.WriteLine(output, "import psym.valuesummary.*;");
+            context.WriteLine(output, "import psym.runtime.*;");
+            context.WriteLine(output, "import psym.runtime.scheduler.*;");
+            context.WriteLine(output, "import psym.runtime.machine.*;");
+            context.WriteLine(output, "import psym.runtime.logger.*;");
+            context.WriteLine(output, "import psym.runtime.machine.buffer.*;");
+            context.WriteLine(output, "import psym.runtime.machine.eventhandlers.*;");
+            context.WriteLine(output, "import psym.runtime.values.*;");
+            context.WriteLine(output, "import psym.utils.*;");
             context.WriteLine(output, "import java.util.List;");
             context.WriteLine(output, "import java.util.ArrayList;");
             context.WriteLine(output, "import java.util.Map;");
@@ -2636,7 +2640,7 @@ private void WriteSourcePrologue(CompilationContext context, StringWriter output
             context.WriteLine(output, "import java.text.MessageFormat;");
             context.WriteLine(output, "import lombok.Generated;");
             context.WriteLine(output);
-            context.WriteLine(output, $"public class {context.ProjectName} implements Program {{");
+            context.WriteLine(output, $"public class {context.MainClassName} implements Program {{");
             context.WriteLine(output);
             context.WriteLine(output, $"public static Scheduler programScheduler;");
             context.WriteLine(output);

Src/PRuntimes/PSymbolicRuntime/CLI_OPTIONS.md → Src/PRuntimes/PSymRuntime/CLI_OPTIONS.md

@@ -6,8 +6,9 @@ Here is a summary of these options:
 
 ````
 Commandline options for PSym
+ -config,--config <File Name (string)>          Name of the JSON configuration file
  -mode,--mode <Mode (string)>                   Mode of exploration: default, bmc, random, fuzz,
-                                                dfs, learn
+                                                dfs, coverage, learn
  -tl,--time-limit <Time Limit (seconds)>        Time limit in seconds (default: 60). Use 0 for no
                                                 limit.
  -ml,--memory-limit <Memory Limit (MB)>         Memory limit in megabytes (MB). Use 0 for no limit.

Src/PRuntimes/PSymRuntime/Examples/tests/PingPong/psym-config.json

@@ -0,0 +1,11 @@
+{
+
+    "sync-events": {
+        "help"    : "Names of sync events",
+        "metavar" : "SE",
+        "default" : [
+            "ping0"
+        ]
+    }
+
+}

Src/PRuntimes/PSymbolicRuntime/Examples/tests/PingPongForeign/pingPongForeign1/GlobalFunctions.java → Src/PRuntimes/PSymRuntime/Examples/tests/PingPongForeign/pingPongForeign1/GlobalFunctions.java

@@ -1,6 +1,6 @@
-package psymbolic;
+package psym.model;
 
-import p.runtime.values.*;
+import psym.runtime.values.*;
 
 public class GlobalFunctions {
 

Src/PRuntimes/PSymbolicRuntime/Examples/tests/PingPongForeign/pingPongForeign2/CustomInt.java → Src/PRuntimes/PSymRuntime/Examples/tests/PingPongForeign/pingPongForeign2/CustomInt.java

@@ -1,7 +1,7 @@
-package psymbolic;
+package psym.model;
 
 import lombok.Getter;
-import p.runtime.values.*;
+import psym.runtime.values.*;
 
 public class CustomInt {
     @Getter

Src/PRuntimes/PSymbolicRuntime/Examples/tests/PingPongForeign/pingPongForeign3/GlobalFunctions.java → Src/PRuntimes/PSymRuntime/Examples/tests/PingPongForeign/pingPongForeign2/GlobalFunctions.java

@@ -1,6 +1,6 @@
-package psymbolic;
+package psym.model;
 
-import p.runtime.values.*;
+import psym.runtime.values.*;
 
 public class GlobalFunctions {
 

Src/PRuntimes/PSymbolicRuntime/Examples/tests/PingPongForeign/pingPongForeign3/CustomInt.java → Src/PRuntimes/PSymRuntime/Examples/tests/PingPongForeign/pingPongForeign3/CustomInt.java

@@ -1,7 +1,7 @@
-package psymbolic;
+package psym.model;
 
 import lombok.Getter;
-import p.runtime.values.*;
+import psym.runtime.values.*;
 
 public class CustomInt {
     @Getter

Src/PRuntimes/PSymbolicRuntime/Examples/tests/PingPongForeign/pingPongForeign2/GlobalFunctions.java → Src/PRuntimes/PSymRuntime/Examples/tests/PingPongForeign/pingPongForeign3/GlobalFunctions.java

@@ -1,6 +1,6 @@
-package psymbolic;
+package psym.model;
 
-import p.runtime.values.*;
+import psym.runtime.values.*;
 
 public class GlobalFunctions {
 

Src/PRuntimes/PSymbolicRuntime/Examples/tests/PingPongForeign/pingPongForeign4/GlobalFunctions.java → Src/PRuntimes/PSymRuntime/Examples/tests/PingPongForeign/pingPongForeign4/GlobalFunctions.java

@@ -1,6 +1,6 @@
-package psymbolic;
+package psym.model;
 
-import p.runtime.values.*;
+import psym.runtime.values.*;
 
 public class GlobalFunctions {
 

Src/PRuntimes/PSymbolicRuntime/README.md → Src/PRuntimes/PSymRuntime/README.md

@@ -6,7 +6,7 @@ The basic idea behind PSym is to perform symbolic exploration of P models, power
 
 PSym is composed of two components: 
   1) [Compiler backend](../../PCompiler/CompilerCore/Backend/Symbolic) in C# that converts a P model to a customized symbolically-instrumented Java code.
-  2) [Runtime analysis](../PSymbolicRuntime) in Java that performs systematic symbolic exploration by executing the symbolically-instrumented Java code.
+  2) [Runtime analysis](../PSymRuntime) in Java that performs systematic symbolic exploration by executing the symbolically-instrumented Java code.
 
 ## Installing PSym
 Run: `` ./scripts/build.sh ``

Src/PRuntimes/PSymbolicRuntime/SOLVERS.md → Src/PRuntimes/PSymRuntime/SOLVERS.md

@@ -10,28 +10,28 @@ This installs PSym with the default BDD backend (powered by BDDs using the [PJBD
 ### Installing ABC
 Run: `` cd scripts && ./setup_abc.sh `` 
 
-If installing ABC in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymbolicRuntime/pom.xml) to update ``<abc.jarpath>`` and ``<abc.libpath>``
+If installing ABC in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymRuntime/pom.xml) to update ``<abc.jarpath>`` and ``<abc.libpath>``
 
 ### Installing MonoSAT
 Run: `` cd scripts && ./setup_monosat.sh ``
 
-If installing MonoSAT in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymbolicRuntime/pom.xml) to update ``<monosat.jarpath>`` and ``<monosat.libpath>``
+If installing MonoSAT in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymRuntime/pom.xml) to update ``<monosat.jarpath>`` and ``<monosat.libpath>``
 
 ### Installing Yices 2
 Run: `` cd scripts && ./setup_yices2.sh `` 
 
-If installing Yices 2 in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymbolicRuntime/pom.xml) to update ``<yices.jarpath>`` and ``<yices.libpath>``
+If installing Yices 2 in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymRuntime/pom.xml) to update ``<yices.jarpath>`` and ``<yices.libpath>``
 
 ### Installing Z3
 Run: `` cd scripts && ./setup_z3.sh `` 
 
-If installing Z3 in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymbolicRuntime/pom.xml) to update ``<z3.jarpath>`` and ``<z3.libpath>``
+If installing Z3 in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymRuntime/pom.xml) to update ``<z3.jarpath>`` and ``<z3.libpath>``
 
 
 ### Installing CVC5
 Run: `` cd scripts && ./setup_cvc5.sh `` 
 
-If installing CVC5 in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymbolicRuntime/pom.xml) to update ``<cvc5.jarpath>`` and ``<cvc5.libpath>``
+If installing CVC5 in a different directory, make changes to [pom.xml](https://github.com/p-org/P/blob/master/Src/PRuntimes/PSymRuntime/pom.xml) to update ``<cvc5.jarpath>`` and ``<cvc5.libpath>``
 
 
 ## Switching Solver and Expression Backends

Src/PRuntimes/PSymbolicRuntime/UNSUPPORTED.md → Src/PRuntimes/PSymRuntime/UNSUPPORTED.md

@@ -3,7 +3,6 @@
 Here is a summary of P features and constructs that PSym *does not* currently support:
 - C# foreign functions (PSym supports Java foreign functions instead)
 - Module refinement and interfaces
-- Liveness checking (coming soon)
 - Deadlock detection (coming soon)
 - Recursive functions (except tail recursion)
 - Relational operations over strings