Merge branch 'master' into master

.github/workflows/pcover.yml

@@ -0,0 +1,40 @@
+# This workflow will build and test PCover, 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: PCover on Ubuntu
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+    inputs:
+      args:
+        description: Additional arguments
+        default: ""
+        required: false
+
+jobs:
+  PCover-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: 6.0.x
+    - name: Set up JDK
+      uses: actions/setup-java@v1
+      with:
+        java-version: 11
+    - 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 PCover
+      working-directory: Src/PRuntimes/PSymRuntime
+      run: ./scripts/build.sh
+    - name: Test PCover
+      working-directory: Src/PRuntimes/PSymRuntime
+      run: mvn test -Dmode="coverage"

README.md

@@ -9,6 +9,8 @@
 ![GitHub Action (CI on Ubuntu)](https://github.com/p-org/P/workflows/CI%20on%20Ubuntu/badge.svg)
 ![GitHub Action (CI on MacOS)](https://github.com/p-org/P/workflows/CI%20on%20MacOS/badge.svg)
 [![Tutorials](https://github.com/p-org/P/actions/workflows/tutorials.yml/badge.svg)](https://github.com/p-org/P/actions/workflows/tutorials.yml)
+[![PSym](https://github.com/p-org/P/actions/workflows/psym.yml/badge.svg)](https://github.com/p-org/P/actions/workflows/psym.yml)
+[![PCover](https://github.com/p-org/P/actions/workflows/pcover.yml/badge.svg)](https://github.com/p-org/P/actions/workflows/pcover.yml)
 
 **Challenge**: 
 Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about correctness in the presence of myriad possible interleaving of messages and failures. Unsurprisingly, it is common for service teams to uncover correctness bugs after deployment. Formal methods can play an important role in addressing this challenge!

Src/PChecker/CheckerCore/Actors/ActorRuntime.cs

@@ -692,6 +692,12 @@ internal void NotifyMonitorError(Monitor monitor)
 
         /// <inheritdoc/>
         public override TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger);
+
+        /// <summary>
+        /// Sets the JsonLogger in LogWriter.cs
+        /// </summary>
+        /// <param name="jsonLogger">jsonLogger instance</param>
+        public void SetJsonLogger(JsonWriter jsonLogger) => LogWriter.SetJsonLogger(jsonLogger);
 
         /// <summary>
         /// Use this method to register an <see cref="IActorRuntimeLog"/>.

Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs

@@ -0,0 +1,182 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using PChecker.Actors.Events;
+
+namespace PChecker.Actors.Logging
+{
+    /// <summary>
+    /// This class implements IActorRuntimeLog and generates log output in an XML format.
+    /// </summary>
+    public class ActorRuntimeLogJsonFormatter : IActorRuntimeLog
+    {
+        /// <summary>
+        /// Get or set the JsonWriter to write to.
+        /// </summary>
+        public JsonWriter Writer { get; set; }
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="ActorRuntimeLogJsonFormatter"/> class. 
+        /// </summary>
+        protected ActorRuntimeLogJsonFormatter()
+        {
+            Writer = new JsonWriter();
+        }
+
+        /// <inheritdoc />
+        public virtual void OnCompleted()
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnAssertionFailure(string error)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnCreateActor(ActorId id, string creatorName, string creatorType)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnDefaultEventHandler(ActorId id, string stateName)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnDequeueEvent(ActorId id, string stateName, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnEnqueueEvent(ActorId id, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName,
+            string actionName)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnHalt(ActorId id, int inboxSize)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnPopState(ActorId id, string currentStateName, string restoredStateName)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnPushState(ActorId id, string currentStateName, string newStateName)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnRaiseEvent(ActorId id, string stateName, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnSendEvent(ActorId targetActorId, string senderName, string senderType,
+            string senderStateName,
+            Event e, Guid opGroupId, bool isTargetHalted)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnCreateMonitor(string monitorType)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnMonitorExecuteAction(string monitorType, string stateName, string actionName)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnMonitorProcessEvent(string monitorType, string stateName, string senderName,
+            string senderType, string senderStateName, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnMonitorRaiseEvent(string monitorType, string stateName, Event e)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry,
+            bool? isInHotState)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnMonitorError(string monitorType, string stateName, bool? isInHotState)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnRandom(object result, string callerName, string callerType)
+        {
+        }
+
+        /// <inheritdoc />
+        public virtual void OnStrategyDescription(string strategyName, string description)
+        {
+        }
+    }
+}