Merging PEx into the Major release P 3.0 branch.

.github/workflows/pex.yml

@@ -0,0 +1,39 @@
+# This workflow will build and test PEx, and cache/restore any dependencies to improve the workflow execution time
+# For more information see: https://help.github.com/actions/language-and-framework-guides/building-and-testing-java-with-maven
+
+name: PEx on Ubuntu
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+    inputs:
+      args:
+        description: Additional arguments
+        default: ""
+        required: false
+jobs:
+  PEx-Build-And-Test-Ubuntu:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v1
+      - name: Setup .NET Core
+        uses: actions/setup-dotnet@v1
+        with:
+          dotnet-version: 8.0.x
+      - name: Set up JDK
+        uses: actions/setup-java@v1
+        with:
+          java-version: 17
+      - name: Cache Maven packages
+        uses: actions/cache@v4
+        with:
+          path: ~/.m2
+          key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}
+          restore-keys: ${{ runner.os }}-m2
+      - name: Build PEx
+        working-directory: Src/PEx
+        run: ./scripts/build_and_test.sh --build
+      - name: Test PEx
+        working-directory: Src/PEx
+        run: ./scripts/build_and_test.sh --test

.gitignore

@@ -230,6 +230,7 @@ Bld/*
 !Bld/Jars/
 !Bld/Deps/
 PGenerated/
+PCheckerOutput/
 !Src/**/Zing/*.zing
 stubs.c
 *.idb

Src/PChecker/CheckerCore/Checker.cs

@@ -35,8 +35,7 @@ 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;
                 default:
@@ -54,8 +53,7 @@ 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;
                 default:
@@ -66,4 +64,4 @@ public static void Run(CheckerConfiguration configuration)
             logger.WriteLine(". Done");
         }
     }
-}
+}

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -238,6 +238,12 @@ public int MaxSchedulingSteps
         [DataMember]
         public string CustomStateMachineRuntimeLogType;
 
+        /// <summary>
+        /// Enables debugging.
+        /// </summary>
+        [DataMember]
+        public bool EnableDebugging;
+
 
         /// <summary>
         /// The testing scheduler unique endpoint.
@@ -269,10 +275,10 @@ public int MaxSchedulingSteps
         public bool DisableEnvironmentExit;
 
         /// <summary>
-        /// Additional arguments to pass to PSym.
+        /// Additional arguments to pass to checker.
         /// </summary>
         [DataMember]
-        public string PSymArgs;
+        public string CheckerArgs;
 
         /// <summary>
         /// Additional arguments to pass to JVM-based checker.
@@ -321,11 +327,12 @@ protected CheckerConfiguration()
             DebugActivityCoverage = false;
 
             IsVerbose = false;
+            EnableDebugging = false;
 
             EnableColoredConsoleOutput = false;
             DisableEnvironmentExit = true;
 
-            PSymArgs = "";
+            CheckerArgs = "";
             JvmArgs = "";
         }
 

Src/PChecker/CheckerCore/CheckerCore.csproj

@@ -4,6 +4,7 @@
         <AssemblyName>PCheckerCore</AssemblyName>
         <RootNamespace>PChecker</RootNamespace>
         <GenerateDocumentationFile>true</GenerateDocumentationFile>
+        <NoWarn>$(NoWarn);1591</NoWarn>
         <OutputPath>$(PSdkFolder)\Binaries</OutputPath>
         <TargetFramework>net8.0</TargetFramework>
         <PackageLicenseExpression>MIT</PackageLicenseExpression>
@@ -22,4 +23,4 @@
         <None Include="../../../Icon/icon.png" Pack="true" PackagePath="" />
         <None Include="../../../README.md" Pack="true" PackagePath="" />
     </ItemGroup>
-</Project>
+</Project>

Src/PChecker/CheckerCore/CheckerMode.cs

@@ -9,12 +9,9 @@ public enum CheckerMode
     /// Mode for prioritized random search
     /// </summary>
     BugFinding,
+
     /// <summary>
-    /// Mode for exhaustive symbolic exploration
+    /// Mode for P exploration and execution
     /// </summary>
-    Verification,
-    /// <summary>
-    /// Mode for exhaustive explicit-state search with state-space coverage reporting
-    /// </summary>
-    Coverage
-}
+    PEx
+}

Src/PChecker/CheckerCore/ExhaustiveEngine.cs

@@ -74,10 +74,7 @@ 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;
                     default:
@@ -109,7 +106,7 @@ private string CreateArguments()
                 }
             }
 
-            arguments.Append($"{_checkerConfiguration.PSymArgs} ");
+            arguments.Append($"{_checkerConfiguration.CheckerArgs} ");
 
             return arguments.ToString();
         }
@@ -234,4 +231,4 @@ public void Run()
             }
         }
     }
-}
+}

Src/PChecker/CheckerCore/Runtime/Logging/IControlledRuntimeLog.cs

@@ -9,7 +9,7 @@ namespace PChecker.Runtime.Logging
 {
     /// <summary>
     /// Interface that allows an external module to track what
-    /// is happening in the <see cref="ControlledRuntime"/>.
+    /// is happening in the controlled runtime.
     /// </summary>
     public interface IControlledRuntimeLog
     {
@@ -38,7 +38,6 @@ public interface IControlledRuntimeLog
         /// <param name="senderType">The type of the sender, if any.</param>
         /// <param name="senderStateName">The state name, if the sender is a state machine, else null.</param>
         /// <param name="e">The event being sent.</param>
-        /// <param name="opGroupId">The id used to identify the send operation.</param>
         /// <param name="isTargetHalted">Is the target state machine halted.</param>
         void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, bool isTargetHalted);
@@ -241,4 +240,4 @@ void OnMonitorProcessEvent(string monitorType, string stateName, string senderNa
         /// </summary>
         void OnCompleted();
     }
-}
+}

Src/PChecker/CheckerCore/Runtime/Logging/LogWriter.cs

@@ -92,7 +92,6 @@ public void LogExecuteAction(StateMachineId id, string handlingStateName, string
         /// <param name="senderType">The type of the sender, if any.</param>
         /// <param name="senderState">The state name, if the sender is a state machine, else null.</param>
         /// <param name="e">The event being sent.</param>
-        /// <param name="opGroupId">The id used to identify the send operation.</param>
         /// <param name="isTargetHalted">Is the target state machine halted.</param>
         public void LogSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderState,
             Event e, bool isTargetHalted)
@@ -624,4 +623,4 @@ internal void RemoveLog(IControlledRuntimeLog log)
             }
         }
     }
-}
+}

Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs

@@ -96,10 +96,17 @@ private static object GetEventPayloadInJson(Event e)
             return pe.Payload?.ToDict();
         }
 
+        /// <summary>
+        /// Called when the log is complete and about to be closed.
+        /// </summary>
         public void OnCompleted()
         {
         }
 
+        /// <summary>
+        /// Invoked when the specified assertion failure has occurred.
+        /// </summary>
+        /// <param name="error">The text of the error.</param>
         public void OnAssertionFailure(string error)
         {
             error = RemoveLogTag(error);
@@ -124,6 +131,11 @@ public void OnCreateStateMachine(StateMachineId id, string creatorName, string c
             Writer.AddToLogs(updateVcMap: true);
         }
 
+        /// <summary>
+        /// Invoked when the specified state machine is idle and the default event handler is about to be executed.
+        /// </summary>
+        /// <param name="id">The id of the state machine that the state will execute in.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         public void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             stateName = GetShortName(stateName);
@@ -139,6 +151,12 @@ public void OnDefaultEventHandler(StateMachineId id, string stateName)
             Writer.AddToLogs(updateVcMap: true);
         }
 
+        /// <summary>
+        /// Invoked when the specified event is dequeued by an state machine.
+        /// </summary>
+        /// <param name="id">The id of the state machine that the event is being dequeued by.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
+        /// <param name="e">The event being dequeued.</param>
         public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             var eventName = GetEventNameWithPayload(e);
@@ -528,4 +546,4 @@ public void OnStrategyDescription(string strategyName, string description)
             Writer.AddToLogs();
         }
     }
-}
+}

Src/PChecker/CheckerCore/Runtime/StateMachines/Exceptions/OnEventDroppedHandler.cs

@@ -6,7 +6,7 @@
 namespace PChecker.Runtime.StateMachines.Exceptions
 {
     /// <summary>
-    /// Handles the <see cref="ControlledRuntime.OnEventDropped"/> event.
+    /// Handles the event dropped notification.
     /// </summary>
     public delegate void OnEventDroppedHandler(Event e, StateMachineId target);
-}
+}

Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs

@@ -519,7 +519,6 @@ private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, str
         /// <param name="type">Type of the state machine.</param>
         /// <param name="name">Optional name used for logging.</param>
         /// <param name="initialEvent">Optional initialization event.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>The unique state machine id.</returns>
         protected StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null) =>
             Runtime.CreateStateMachine(null, type, name, initialEvent, this);
@@ -529,8 +528,7 @@ protected StateMachineId CreateStateMachine(Type type, string name, Event initia
         /// Sends an asynchronous <see cref="Event"/> to a target.
         /// </summary>
         /// <param name="target">The target.</param>
-        /// <param name="e">The event to send.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <param name="ev">The event to send.</param>
         public void SendEvent(PMachineValue target, Event ev)
         {
             Assert(ev != null, $"Machine cannot send a null event. Machine {Id} trying to send null event in state {CurrentStateName}.");
@@ -2063,4 +2061,4 @@ public IgnoreEventsAttribute(params Type[] eventTypes)
             }
         }
     }
-}
+}

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/TimelineObserver.cs

@@ -7,13 +7,11 @@
 
 namespace PChecker.Feedback;
 
-internal class TimelineObserver: IControlledRuntimeLog
+internal class TimelineObserver : IControlledRuntimeLog
 {
-
     private HashSet<(string, string, string)> _timelines = new();
     private Dictionary<string, HashSet<string>> _allEvents = new();
     private Dictionary<string, List<string>> _orderedEvents = new();
-    private IControlledRuntimeLog _controlledRuntimeLogImplementation;
 
     public static readonly List<(int, int)> Coefficients = new();
     public static int NumOfCoefficients = 50;
@@ -188,4 +186,4 @@ public void OnStrategyDescription(string strategyName, string description)
     public void OnCompleted()
     {
     }
-}
+}

Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs

@@ -6,6 +6,8 @@ namespace Plang.Compiler.Backend
 {
     public interface ICodeGenerator
     {
+        public const string GlobalConfigName = "GlobalConfig";
+
         /// <summary>
         /// Generate target language source files from a P project.
         /// </summary>