addressed comments - modified yml files, Bld files, removed coverage, verification

Aishwarya Jagarapu · Aishwarya Jagarapu · commit 0bca88f01ac5 · 2025-03-06T16:42:17.000-08:00
diff --git a/.github/workflows/macosci.yml b/.github/workflows/macosci.yml
@@ -16,12 +16,14 @@ jobs:
       with:
         java-version: 11
     - name: Cache Maven packages
-      uses: actions/cache@v4
+      uses: actions/cache@v2
       with:
         path: ~/.m2
         key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}
         restore-keys: ${{ runner.os }}-m2
+    - name: Build Java P runtime
+      run: mvn clean package -f Src/PRuntimes/PJavaRuntime
     - name: Build
       run: dotnet build --configuration Release
     - name: Test
-      run: dotnet test --configuration Release
+      run: dotnet test --configuration Release
diff --git a/.github/workflows/pex.yml b/.github/workflows/pex.yml
@@ -26,7 +26,7 @@ jobs:
         with:
           java-version: 17
       - name: Cache Maven packages
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         with:
           path: ~/.m2
           key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}
@@ -36,4 +36,4 @@ jobs:
         run: ./scripts/build.sh
       - name: Test PEx
         working-directory: Src/PRuntimes/PExRuntime
-        run: mvn test
+        run: mvn test
diff --git a/.github/workflows/ubuntuci.yml b/.github/workflows/ubuntuci.yml
@@ -21,7 +21,9 @@ jobs:
         path: ~/.m2
         key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}
         restore-keys: ${{ runner.os }}-m2
+    - name: Build Java P runtime
+      run: mvn clean package -f Src/PRuntimes/PJavaRuntime
     - name: Build
       run: dotnet build --configuration Release
     - name: Test
-      run: dotnet test --configuration Release
+      run: dotnet test --configuration Release
diff --git a/Bld/build.ps1 b/Bld/build.ps1
@@ -4,6 +4,8 @@ pushd ..
 Write-Host "Initializing submodules .."  -ForegroundColor DarkGreen -BackgroundColor White
 git submodule update --init --recursive
 
+mvn clean compile -f ./Src/PRuntimes/PJavaRuntime/pom.xml
+
 # Run the build! :D
 dotnet build -c Release
 
diff --git a/Bld/build.sh b/Bld/build.sh
@@ -13,6 +13,9 @@ echo -e "${ORANGE} ---- Fetching git submodules ----${NOCOLOR}"
 # Initialize submodules
 git submodule update --init --recursive
 
+echo -e "${ORANGE} ---- Building the Java P runtime ----${NOCOLOR}"
+mvn compile -q -f ./Src/PRuntimes/PJavaRuntime/pom.xml
+
 echo -e "${ORANGE} ---- Building the PCompiler ----${NOCOLOR}"
 # Run the build!
 
diff --git a/Src/PChecker/CheckerCore/Checker.cs b/Src/PChecker/CheckerCore/Checker.cs
@@ -35,8 +35,6 @@ public static void Run(CheckerConfiguration configuration)
                     Error.Write(logger, ConsoleColor.Yellow, engine.GetReport());
                 }
                     break;
-                case CheckerMode.Verification:
-                case CheckerMode.Coverage:
                 case CheckerMode.PEx:
                     ExhaustiveEngine.Create(configuration).Run();
                     break;
@@ -55,8 +53,6 @@ public static void Run(CheckerConfiguration configuration)
                 case CheckerMode.BugFinding:
                     TestingProcess.Create(configuration).Run();
                     break;
-                case CheckerMode.Verification:
-                case CheckerMode.Coverage:
                 case CheckerMode.PEx:
                     ExhaustiveEngine.Create(configuration).Run();
                     break;
diff --git a/Src/PChecker/CheckerCore/CheckerMode.cs b/Src/PChecker/CheckerCore/CheckerMode.cs
@@ -10,14 +10,6 @@ public enum CheckerMode
     /// </summary>
     BugFinding,
     /// <summary>
-    /// Mode for exhaustive symbolic exploration
-    /// </summary>
-    Verification,
-    /// <summary>
-    /// Mode for exhaustive explicit-state search with state-space coverage reporting
-    /// </summary>
-    Coverage,
-    /// <summary>
     /// Mode for exhaustive explicit-state search with state-space coverage reporting
     /// </summary>
     PEx
diff --git a/Src/PChecker/CheckerCore/ExhaustiveEngine.cs b/Src/PChecker/CheckerCore/ExhaustiveEngine.cs
@@ -74,10 +74,6 @@ private String CreateArguments()
             {
                 switch (_checkerConfiguration.Mode)
                 {
-                    case CheckerMode.Verification:
-                        arguments.Append("--strategy symbolic ");
-                        break;
-                    case CheckerMode.Coverage:
                     case CheckerMode.PEx:
                         arguments.Append($"--strategy {_checkerConfiguration.SchedulingStrategy} ");
                         break;
diff --git a/Src/PCompiler/CompilerCore/CompilerOutput.cs b/Src/PCompiler/CompilerCore/CompilerOutput.cs
@@ -2,8 +2,6 @@ namespace Plang.Compiler
 {
     public enum CompilerOutput
     {
-        C,
-        Symbolic,
         CSharp,
         Java,
         PEx,
diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
@@ -31,7 +31,7 @@ public PCheckerOptions()
             basicOptions.AddPositionalArgument("path", "Path to the compiled file to check for correctness (*.dll)."+
                                                        " If this option is not passed, the compiler searches for a *.dll file in the current folder").IsRequired = false;
             var modes = basicOptions.AddArgument("mode", "md", "Checker mode to use. Can be bugfinding or pex. If this option is not passed, bugfinding mode is used as default");
-            modes.AllowedValues = new List<string>() { "bugfinding", "pex", "pobserve", "verification", "coverage" };
+            modes.AllowedValues = new List<string>() { "bugfinding", "pex", "pobserve" };
             basicOptions.AddArgument("testcase", "tc", "Test case to explore");
             // basicOptions.AddArgument("smoke-testing", "tsmoke",
             //     "Smoke test the program by running the checker on all the test cases", typeof(bool));
@@ -214,12 +214,6 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
                         case "bugfinding":
                             checkerConfiguration.Mode = CheckerMode.BugFinding;
                             break;
-                        case "verification":
-                            checkerConfiguration.Mode = CheckerMode.Verification;
-                            break;
-                        case "coverage":
-                            checkerConfiguration.Mode = CheckerMode.Coverage;
-                            break;
                         case "pex":
                             checkerConfiguration.Mode = CheckerMode.PEx;
                             break;
@@ -327,7 +321,6 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
                     checkerConfiguration.JvmArgs = ((string)option.Value).Replace(':', ' ');
                     break;
                 case "checker-args":
-                case "psym-args":
                     checkerConfiguration.CheckerArgs = ((string)option.Value).Replace(':', ' ');
                     break;
                 case "pproj":
@@ -393,8 +386,6 @@ private static void FindLocalPCompiledFile(CheckerConfiguration checkerConfigura
                 string filePattern =  checkerConfiguration.Mode switch
                 {
                     CheckerMode.BugFinding => "*.dll",
-                    CheckerMode.Verification => "*-jar-with-dependencies.jar",
-                    CheckerMode.Coverage => "*-jar-with-dependencies.jar",
                     CheckerMode.PEx => "*-jar-with-dependencies.jar",
                     _ => "*.dll"
                 };
@@ -421,11 +412,6 @@ from file in Directory.GetFiles(checkerConfiguration.PCompiledPath, filePattern,
                             || fileName.EndsWith($"{pathSep}p.dll"))
                             continue;
                     }
-                    else if (checkerConfiguration.Mode == CheckerMode.Verification || checkerConfiguration.Mode == CheckerMode.Coverage)
-                    {
-                        if (!fileName.Contains($"Symbolic{pathSep}"))
-                            continue;
-                    }
                     else if (checkerConfiguration.Mode == CheckerMode.PEx)
                     {
                         if (!fileName.Contains($"PEx{pathSep}"))
diff --git a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs
@@ -24,8 +24,6 @@ internal PCompilerOptions()
                 "The P compiler compiles all the P files in the project together and generates the executable that can be checked for correctness by the P checker."
                 // + "\n\nCompiler modes :: (default: bugfinding)\n" +
                 // "  --mode bugfinding   : for bug finding through stratified random search\n" +
-                // "  --mode verification : for verification through exhaustive symbolic exploration\n" +
-                // "  --mode coverage     : for achieving state-space coverage through exhaustive explicit-state search\n" +
                 // "  --mode pobserve     : for runtime monitoring of P specs against implementation logs"
             );
 
@@ -39,7 +37,7 @@ internal PCompilerOptions()
             pfilesGroup.AddArgument("outdir", "o", "Dump output to directory (absolute or relative path)");
 
             var modes = Parser.AddArgument("mode", "md", "Compilation mode to use. Can be bugfinding, pex, pobserve, or stately. If this option is not passed, bugfinding mode is used as default");
-            modes.AllowedValues = new List<string>() { "bugfinding", "pex", "pobserve", "stately", "verification", "coverage" };
+            modes.AllowedValues = new List<string>() { "bugfinding", "pex", "pobserve", "stately"};
 
             Parser.AddArgument("pobserve-package", "po", "PObserve package name").IsHidden = true;
 

Original file line number	Diff line number	Diff line change
`@@ -74,10 +74,6 @@ private String CreateArguments()`
`74`	`74`	`{`
`75`	`75`	`switch (_checkerConfiguration.Mode)`
`76`	`76`	`{`
`77`		`- case CheckerMode.Verification:`
`78`		`- arguments.Append("--strategy symbolic ");`
`79`		`- break;`
`80`		`- case CheckerMode.Coverage:`
`81`	`77`	`case CheckerMode.PEx:`
`82`	`78`	`arguments.Append($"--strategy {_checkerConfiguration.SchedulingStrategy} ");`
`83`	`79`	`break;`
Original file line number	Diff line number	Diff line change
`@@ -2,8 +2,6 @@ namespace Plang.Compiler`
`2`	`2`	`{`
`3`	`3`	`public enum CompilerOutput`
`4`	`4`	`{`
`5`		`- C,`
`6`		`- Symbolic,`
`7`	`5`	`CSharp,`
`8`	`6`	`Java,`
`9`	`7`	`PEx,`