moved actors to dedicated nuget package (#406)

Coyote.sln

@@ -18,6 +18,8 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Test", "Source\Test\Test.cs
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Core", "Source\Core\Core.csproj", "{E75DB9C9-7842-4AE4-A29D-624F6B49F607}"
 EndProject
+Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Actors", "Source\Actors\Actors.csproj", "{8548010B-B99D-44FD-95BD-F716C1D707B7}"
+EndProject
 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Tests", "Tests", "{2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Tests.Actors", "Tests\Tests.Actors\Tests.Actors.csproj", "{911F1779-3558-4590-836C-C75112D65FD8}"
@@ -56,6 +58,10 @@ Global
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983}.Release|Any CPU.Build.0 = Release|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Release|Any CPU.Build.0 = Release|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Release|Any CPU.ActiveCfg = Release|Any CPU
@@ -114,6 +120,7 @@ Global
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
+		{8548010B-B99D-44FD-95BD-F716C1D707B7} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
 		{911F1779-3558-4590-836C-C75112D65FD8} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
 		{DABC68C1-79D3-4324-A750-7CF72E0A0ACF} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}

History.md

@@ -1,3 +1,12 @@
+## v1.6.3
+- Refactored the NuGet packages and moved `Microsoft.Coyote.Actors` to its own dedicated package.
+- Moved the actor `Event` type under the `Microsoft.Coyote.Actors` namespace.
+- Introduced a `Monitor.Event` type (nested in the `Microsoft.Coyote.Specifications.Monitor` class),
+  which must now be used for declaring specification monitor events.
+- Enhanced and streamlined the logging API, which is now available in the `Microsoft.Coyote.Logging`
+  namespace, instead of `Microsoft.Coyote.IO`.
+- Removed support for the end-of-life `net5.0` target framework.
+
 ## v1.6.2
 - Exposed new `IActorRuntime.GetCurrentActorIds()` API that returns the `ActorId` for each active
   actor managed by the runtime, as well as an `IActorRuntime.GetCurrentActorTypes()` API that
@@ -87,7 +96,7 @@ concurrent operations.
 - Various other runtime improvements and fixes.
 
 ## v1.4.3
-- Added support for the `netstandard2.0` target.
+- Added support for the `netstandard2.0` target framework.
 - Added support for rewriting the non-generic `TaskCompletionSource` type.
 - Added support for rewriting the `ValueTask` type (but `IValueTaskSource` is not supported).
 - Improvements to systematic fuzzing, especially for actor-based programs.
@@ -95,7 +104,7 @@ concurrent operations.
 - Tests now report the degree of concurrency and number of controlled operations.
 
 ## v1.4.2
-- Added support for the `net6.0` target.
+- Added support for the `net6.0` target framework.
 - The `TestingEngine` is now giving a warning if the DLL being tested has not been rewritten.
 - The number of controlled operations are now reported as part of test statistics.
 - Improvements, optimizations and bug-fixes in binary rewriting.
@@ -128,8 +137,8 @@ concurrent operations.
 - Improved the binary rewriting engine and fixed various rewriting bugs.
 - Removed the deprecated `Microsoft.Coyote.Tasks` namespace. Testing task-based code should now only
   be done via binary rewriting, instead of using a custom task type.
-- Removed the `net48` target, can instead just use the `net462` target for legacy .NET Framework
-  projects.
+- Removed the `net48` target framework, can instead just use the `net462` target framework for
+  legacy .NET Framework projects.
 
 ## v1.2.8
 - Improved the strategies used for systematic fuzzing.
@@ -147,7 +156,7 @@ concurrent operations.
 - Added an experimental rewriting pass that adds assertion checks to find data races in uses of the
   `System.Collections.Generic.List<T>` and `System.Collections.Generic.Dictionary<TKey, TValue>`
   collections.
-- Added support for the `net462` target.
+- Added support for the `net462` target framework.
 
 ## v1.2.5
 - Added the `SchedulingPoint` static class that exposes methods for adding manual scheduling points
@@ -177,8 +186,8 @@ concurrent operations.
 - Added the `Configuration.WithTestingTimeout` API for specifying a systematic testing timeout
   instead of iterations.
 - Optimized state space exploration in programs using `Task.Delay`.
-- Added support for the `net5.0` target.
-- Removed the `net47` target.
+- Added support for the `net5.0` target framework.
+- Removed the `net47` target framework.
 
 ## v1.2.1
 - Added the `OnEventIgnored` and `OnEventDeferred` callbacks in the `Actor` type.

Samples/CloudMessaging/Raft.Azure/AzureClusterManager.cs

@@ -5,6 +5,7 @@ using System.Runtime.Serialization;
 using System.Text;
 using System.Threading.Tasks;
 using Microsoft.Azure.ServiceBus;
+using Microsoft.Coyote.Actors;
 using Newtonsoft.Json;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging

Samples/CloudMessaging/Raft.Mocking/Mocks/MockClusterManager.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Threading.Tasks;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft.Nondeterminism/Mocks/MockClusterManagerWithFailure.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Threading.Tasks;
+using Microsoft.Coyote.Actors;
 using Microsoft.Coyote.Runtime;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging

Samples/CloudMessaging/Raft/Events/AppendLogEntriesRequestEvent.cs

@@ -3,6 +3,7 @@
 
 using System.Collections.Generic;
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft/Events/AppendLogEntriesResponseEvent.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft/Events/ClientRequestEvent.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft/Events/ClientResponseEvent.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft/Events/NotifyJoinedServiceEvent.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft/Events/VoteRequestEvent.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CloudMessaging/Raft/Events/VoteResponseEvent.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System.Runtime.Serialization;
+using Microsoft.Coyote.Actors;
 
 namespace Microsoft.Coyote.Samples.CloudMessaging
 {

Samples/CoffeeMachineActors/MockSensors.cs

@@ -11,13 +11,20 @@ using Microsoft.Coyote.Specifications;
 
 namespace Microsoft.Coyote.Samples.CoffeeMachineActors
 {
-    public class BusyEvent : Event { }
-
     /// <summary>
     /// This safety monitor ensure nothing bad happens while a door is open on the coffee machine.
     /// </summary>
     internal class DoorSafetyMonitor : Monitor
     {
+        internal class DoorOpenEvent : Event
+        {
+            internal bool Open;
+
+            internal DoorOpenEvent(bool value) { this.Open = value; }
+        }
+
+        internal class BusyEvent : Event { }
+
         [Start]
         [OnEventGotoState(typeof(DoorOpenEvent), typeof(Error))]
         [IgnoreEvents(typeof(BusyEvent))]
@@ -51,7 +58,7 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
             this.DoorOpen = this.RandomInteger(5) is 0;
             if (this.DoorOpen)
             {
-                this.Monitor<DoorSafetyMonitor>(new DoorOpenEvent(this.DoorOpen));
+                this.Monitor<DoorSafetyMonitor>(new DoorSafetyMonitor.DoorOpenEvent(this.DoorOpen));
             }
 
             return base.OnInitializeAsync(initialEvent);
@@ -161,7 +168,7 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
 
             if (this.WaterHeaterButton)
             {
-                this.Monitor<DoorSafetyMonitor>(new BusyEvent());
+                this.Monitor<DoorSafetyMonitor>(new DoorSafetyMonitor.BusyEvent());
                 this.WaterHeaterTimer = this.StartPeriodicTimer(TimeSpan.FromSeconds(0.1), TimeSpan.FromSeconds(0.1), new HeaterTimerEvent());
             }
             else if (this.WaterHeaterTimer != null)
@@ -221,7 +228,7 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
 
             if (this.WaterPump)
             {
-                this.Monitor<DoorSafetyMonitor>(new BusyEvent());
+                this.Monitor<DoorSafetyMonitor>(new DoorSafetyMonitor.BusyEvent());
                 // Should never turn on the make shots button when there is no water.
                 if (this.WaterLevel <= 0)
                 {
@@ -340,7 +347,7 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
         {
             if (this.GrinderButton)
             {
-                this.Monitor<DoorSafetyMonitor>(new BusyEvent());
+                this.Monitor<DoorSafetyMonitor>(new DoorSafetyMonitor.BusyEvent());
                 // Should never turn on the grinder when there is no coffee to grind.
                 if (this.HopperLevel <= 0)
                 {
@@ -426,7 +433,7 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
             var evt = e as DumpGrindsButtonEvent;
             if (evt.PowerOn)
             {
-                this.Monitor<DoorSafetyMonitor>(new BusyEvent());
+                this.Monitor<DoorSafetyMonitor>(new DoorSafetyMonitor.BusyEvent());
                 // This is a toggle button, in no time grinds are dumped (just for simplicity).
                 this.PortaFilterCoffeeLevel = 0;
             }

Samples/CoffeeMachineActors/Program.cs

@@ -13,8 +13,13 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
 
         public static void Main()
         {
+            // Optional: increases verbosity level to see the Coyote runtime log and sets it to output to the console.
+            // var configuration = Configuration.Create();
+            var configuration = Configuration.Create().WithVerbosityEnabled().WithConsoleLoggingEnabled();
             RunForever = true;
-            IActorRuntime runtime = RuntimeFactory.Create();
+
+            IActorRuntime runtime = RuntimeFactory.Create(configuration);
+            runtime.OnFailure += OnRuntimeFailure;
             Execute(runtime);
             Console.ReadLine();
             Console.WriteLine("User cancelled the test by pressing ENTER");
@@ -28,9 +33,7 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
         [Microsoft.Coyote.SystematicTesting.Test]
         public static void Execute(IActorRuntime runtime)
         {
-            LogWriter.Initialize(runtime.Logger, RunForever);
-
-            runtime.OnFailure += OnRuntimeFailure;
+            LogWriter.Initialize(runtime.Logger);
             runtime.RegisterMonitor<LivenessMonitor>();
             runtime.RegisterMonitor<DoorSafetyMonitor>();
             ActorId driver = runtime.CreateActor(typeof(FailoverDriver), new ConfigEvent(RunForever));

Samples/CoffeeMachineActors/SensorEvents.cs

@@ -15,9 +15,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     /// </summary>
     internal class ConfigEvent : Event
     {
-        public bool RunSlowly;
+        internal bool RunSlowly;
 
-        public ConfigEvent(bool runSlowly)
+        internal ConfigEvent(bool runSlowly)
         {
             this.RunSlowly = runSlowly;
         }
@@ -28,9 +28,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     /// </summary>
     internal class RegisterClientEvent : Event
     {
-        public ActorId Caller;
+        internal ActorId Caller;
 
-        public RegisterClientEvent(ActorId caller) { this.Caller = caller; }
+        internal RegisterClientEvent(ActorId caller) { this.Caller = caller; }
     }
 
     /// <summary>
@@ -39,9 +39,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class WaterLevelEvent : Event
     {
         // Starts at 100% full and drops when shot button is on.
-        public double WaterLevel;
+        internal double WaterLevel;
 
-        public WaterLevelEvent(double value) { this.WaterLevel = value; }
+        internal WaterLevelEvent(double value) { this.WaterLevel = value; }
     }
 
     /// <summary>
@@ -55,9 +55,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class HopperLevelEvent : Event
     {
         // Starts at 100% full of beans, and drops when grinder is on.
-        public double HopperLevel;
+        internal double HopperLevel;
 
-        public HopperLevelEvent(double value) { this.HopperLevel = value; }
+        internal HopperLevelEvent(double value) { this.HopperLevel = value; }
     }
 
     /// <summary>
@@ -71,9 +71,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class WaterTemperatureEvent : Event
     {
         // Starts at room temp, heats up to 100 when water heater is on.
-        public double WaterTemperature;
+        internal double WaterTemperature;
 
-        public WaterTemperatureEvent(double value) { this.WaterTemperature = value; }
+        internal WaterTemperatureEvent(double value) { this.WaterTemperature = value; }
     }
 
     /// <summary>
@@ -87,9 +87,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class PortaFilterCoffeeLevelEvent : Event
     {
         // Starts out empty=0, it gets filled to 100% with ground coffee while grinder is on.
-        public double CoffeeLevel;
+        internal double CoffeeLevel;
 
-        public PortaFilterCoffeeLevelEvent(double value) { this.CoffeeLevel = value; }
+        internal PortaFilterCoffeeLevelEvent(double value) { this.CoffeeLevel = value; }
     }
 
     /// <summary>
@@ -103,9 +103,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class DoorOpenEvent : Event
     {
         // True if open, a safety check to make sure machine is buttoned up properly before use.
-        public bool Open;
+        internal bool Open;
 
-        public DoorOpenEvent(bool value) { this.Open = value; }
+        internal DoorOpenEvent(bool value) { this.Open = value; }
     }
 
     internal class ReadDoorOpenEvent : Event { }
@@ -116,9 +116,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class WaterHeaterButtonEvent : Event
     {
         // True means the power is on.
-        public bool PowerOn;
+        internal bool PowerOn;
 
-        public WaterHeaterButtonEvent(bool value) { this.PowerOn = value; }
+        internal WaterHeaterButtonEvent(bool value) { this.PowerOn = value; }
     }
 
     /// <summary>
@@ -127,9 +127,9 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     internal class GrinderButtonEvent : Event
     {
         // True means the power is on.
-        public bool PowerOn;
+        internal bool PowerOn;
 
-        public GrinderButtonEvent(bool value) { this.PowerOn = value; }
+        internal GrinderButtonEvent(bool value) { this.PowerOn = value; }
     }
 
     internal class HopperEmptyEvent : Event
@@ -148,16 +148,16 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineActors
     {
         // True means the power is on, shot button produces 1 shot of espresso and turns off automatically,
         // raising a ShowCompleteEvent press it multiple times to get multiple shots.
-        public bool PowerOn;
+        internal bool PowerOn;
 
-        public PumpWaterEvent(bool value) { this.PowerOn = value; }
+        internal PumpWaterEvent(bool value) { this.PowerOn = value; }
     }
 
     internal class DumpGrindsButtonEvent : Event
     {
         // True means the power is on, empties the PortaFilter and turns off automatically.
-        public bool PowerOn;
+        internal bool PowerOn;
 
-        public DumpGrindsButtonEvent(bool value) { this.PowerOn = value; }
+        internal DumpGrindsButtonEvent(bool value) { this.PowerOn = value; }
     }
 }

Samples/CoffeeMachineTasks/Program.cs

@@ -16,23 +16,24 @@ namespace Microsoft.Coyote.Samples.CoffeeMachineTasks
         public static void Main()
         {
             RunForever = true;
-            ICoyoteRuntime runtime = RuntimeProvider.Create();
-            _ = Execute(runtime);
+
+            LogWriter.Initialize();
+            _ = RunTest();
+
             Console.ReadLine();
             Console.WriteLine("User cancelled the test by pressing ENTER");
         }
 
-        private static void OnRuntimeFailure(Exception ex)
-        {
-            Console.WriteLine("### Failure: " + ex.Message);
-        }
-
         [Microsoft.Coyote.SystematicTesting.Test]
         public static async Task Execute(ICoyoteRuntime runtime)
         {
-            LogWriter.Initialize(runtime.Logger, RunForever);
-            runtime.OnFailure += OnRuntimeFailure;
+            LogWriter.Initialize(runtime.Logger);
             Specification.RegisterMonitor<LivenessMonitor>();
+            await RunTest();
+        }
+
+        private static async Task RunTest()
+        {
             IFailoverDriver driver = new FailoverDriver(RunForever);
             await driver.RunTest();
         }

Samples/Common/LogWriter.cs

@@ -19,14 +19,19 @@ namespace Microsoft.Coyote.Samples.Common
 
         public static LogWriter Instance;
 
-        public static void Initialize(ILogger log, bool echo)
+        public static void Initialize()
         {
-            Instance = new LogWriter(log, echo);
+            Instance = new LogWriter(null, true);
+        }
+
+        public static void Initialize(ILogger log)
+        {
+            Instance = new LogWriter(log, false);
         }
 
         public void WriteLine(string format, params object[] args)
         {
-            this.Log.WriteLine(format, args);
+            this.Log?.WriteLine(format, args);
             if (this.Echo)
             {
                 Console.WriteLine(format, args);
@@ -36,7 +41,7 @@ namespace Microsoft.Coyote.Samples.Common
         public void WriteWarning(string format, params object[] args)
         {
             var msg = string.Format(format, args);
-            this.Log.WriteLine(LogSeverity.Warning, msg);
+            this.Log?.WriteLine(LogSeverity.Warning, msg);
             if (this.Echo)
             {
                 try
@@ -54,7 +59,7 @@ namespace Microsoft.Coyote.Samples.Common
         internal void WriteError(string format, params object[] args)
         {
             var msg = string.Format(format, args);
-            this.Log.WriteLine(LogSeverity.Error, msg);
+            this.Log?.WriteLine(LogSeverity.Error, msg);
             if (this.Echo)
             {
                 try

Samples/Common/build.props

@@ -32,10 +32,12 @@
   </ItemGroup>
   <ItemGroup Condition="'$(UseLocalCoyote)'=='false'">
     <PackageReference Include="Microsoft.Coyote" Version="$(Version)" />
+    <PackageReference Include="Microsoft.Coyote.Actors" Version="$(Version)" />
     <PackageReference Include="Microsoft.Coyote.Test" Version="$(Version)" />
   </ItemGroup>
   <ItemGroup Condition="'$(UseLocalCoyote)'=='true'">
     <ProjectReference Include="$(MSBuildThisFileDirectory)\..\..\Source\Core\Core.csproj" />
+    <ProjectReference Include="$(MSBuildThisFileDirectory)\..\..\Source\Actors\Actors.csproj" />
     <ProjectReference Include="$(MSBuildThisFileDirectory)\..\..\Source\Test\Test.csproj" />
     <ProjectReference Include="$(MSBuildThisFileDirectory)\..\..\Tools\Coyote\Coyote.csproj" />
   </ItemGroup>

Samples/DrinksServingRobotActors/Program.cs

@@ -13,11 +13,12 @@ namespace Microsoft.Coyote.Samples.DrinksServingRobot
 
         public static void Main()
         {
-            var conf = null as Configuration;
-            // var conf = Configuration.Create().WithVerbosityEnabled();
-
+            // Optional: increases verbosity level to see the Coyote runtime log and sets it to output to the console.
+            // var configuration = Configuration.Create();
+            var configuration = Configuration.Create().WithVerbosityEnabled().WithConsoleLoggingEnabled();
             RunForever = true;
-            IActorRuntime runtime = Actors.RuntimeFactory.Create(conf);
+
+            IActorRuntime runtime = Actors.RuntimeFactory.Create(configuration);
             runtime.OnFailure += OnRuntimeFailure;
             Execute(runtime);
             Console.ReadLine();
@@ -26,9 +27,9 @@ namespace Microsoft.Coyote.Samples.DrinksServingRobot
         [Microsoft.Coyote.SystematicTesting.Test]
         public static void Execute(IActorRuntime runtime)
         {
-            LogWriter.Initialize(runtime.Logger, RunForever);
+            LogWriter.Initialize(runtime.Logger);
             runtime.RegisterMonitor<LivenessMonitor>();
-            ActorId driver = runtime.CreateActor(typeof(FailoverDriver), new FailoverDriver.ConfigEvent(RunForever));
+            runtime.CreateActor(typeof(FailoverDriver), new FailoverDriver.ConfigEvent(RunForever));
         }
 
         private static void OnRuntimeFailure(Exception ex)

Samples/Monitors/Driver.cs

@@ -97,7 +97,8 @@ namespace Microsoft.Coyote.Samples.Monitors
         /// </summary>
         private void NodeFailedAction(Event e)
         {
-            this.Monitor<Liveness>(e);
+            var node = (e as FailureDetector.NodeFailed).Node;
+            this.Monitor<Liveness>(new Liveness.NodeFailed(node));
         }
     }
 }

Samples/Monitors/Liveness.cs

@@ -33,14 +33,24 @@ namespace Microsoft.Coyote.Samples.Monitors
     {
         internal class RegisterNodes : Event
         {
-            public HashSet<ActorId> Nodes;
+            internal HashSet<ActorId> Nodes;
 
-            public RegisterNodes(HashSet<ActorId> nodes)
+            internal RegisterNodes(HashSet<ActorId> nodes)
             {
                 this.Nodes = nodes;
             }
         }
 
+        internal class NodeFailed : Event
+        {
+            internal ActorId Node;
+
+            internal NodeFailed(ActorId node)
+            {
+                this.Node = node;
+            }
+        }
+
         private HashSet<ActorId> Nodes;
 
         [Start]
@@ -59,12 +69,12 @@ namespace Microsoft.Coyote.Samples.Monitors
         /// currently satisfied.
         /// </summary>
         [Hot]
-        [OnEventDoAction(typeof(FailureDetector.NodeFailed), nameof(NodeDownAction))]
+        [OnEventDoAction(typeof(NodeFailed), nameof(NodeDownAction))]
         private class Wait : State { }
 
         private void NodeDownAction(Event e)
         {
-            var node = (e as FailureDetector.NodeFailed).Node;
+            var node = (e as NodeFailed).Node;
             this.Nodes.Remove(node);
             if (this.Nodes.Count == 0)
             {

Samples/Timers/Test.cs

@@ -12,9 +12,9 @@ namespace Coyote.Examples.Timers
     {
         public static void Main()
         {
-            // Optional: increases verbosity level to see the Coyote runtime log.
+            // Optional: increases verbosity level to see the Coyote runtime log and sets it to output to the console.
             // var configuration = Configuration.Create();
-            var configuration = Configuration.Create().WithVerbosityEnabled();
+            var configuration = Configuration.Create().WithVerbosityEnabled().WithConsoleLoggingEnabled();
 
             // Creates a new Coyote runtime instance, and passes an optional configuration.
             var runtime = RuntimeFactory.Create(configuration);
@@ -30,7 +30,7 @@ namespace Coyote.Examples.Timers
         [Microsoft.Coyote.SystematicTesting.Test]
         public static void Execute(IActorRuntime runtime)
         {
-            LogWriter.Initialize(runtime.Logger, false);
+            LogWriter.Initialize(runtime.Logger);
             runtime.CreateActor(typeof(TimerSample));
         }
     }

Scripts/NuGet/Coyote.Actors.nuspec

@@ -0,0 +1,49 @@
+<?xml version="1.0"?>
+<package >
+  <metadata>
+    <id>Microsoft.Coyote.Actors</id>
+    <version>$version$</version>
+    <authors>Microsoft</authors>
+    <description>The Coyote actor runtime and library.</description>
+    <projectUrl>https://microsoft.github.io/coyote/</projectUrl>
+    <repository type="git" url="https://github.com/microsoft/coyote"/>
+    <license type="expression">MIT</license>
+    <requireLicenseAcceptance>false</requireLicenseAcceptance>
+    <copyright>© Microsoft Corporation. All rights reserved.</copyright>
+    <icon>images\icon.png</icon>
+    <readme>docs\readme.md</readme>
+    <tags>actors state-machines asynchronous reactive systematic-testing</tags>
+    <dependencies>
+      <group targetFramework=".NET6.0">
+        <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="System.Threading.Tasks.Extensions" version="4.5.4"/>
+      </group>
+      <group targetFramework=".NETCoreApp3.1">
+        <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="System.Threading.Tasks.Extensions" version="4.5.4"/>
+      </group>
+      <group targetFramework=".NETStandard2.0">
+        <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="System.Threading.Tasks.Extensions" version="4.5.4"/>
+      </group>
+    </dependencies>
+  </metadata>
+  <files>
+    <!-- .NET 6.0 -->
+    <file src="..\..\bin\net6.0\Microsoft.Coyote.Actors.dll" target="lib\net6.0" />
+    <file src="..\..\bin\net6.0\Microsoft.Coyote.Actors.xml" target="lib\net6.0" />
+    <file src="..\..\bin\net6.0\Microsoft.Coyote.Actors.pdb" target="lib\net6.0" />
+    <!-- .NET Core 3.1 -->
+    <file src="..\..\bin\netcoreapp3.1\Microsoft.Coyote.Actors.dll" target="lib\netcoreapp3.1" />
+    <file src="..\..\bin\netcoreapp3.1\Microsoft.Coyote.Actors.xml" target="lib\netcoreapp3.1" />
+    <file src="..\..\bin\netcoreapp3.1\Microsoft.Coyote.Actors.pdb" target="lib\netcoreapp3.1" />
+    <!-- .NET Standard 2.0 -->
+    <file src="..\..\bin\netstandard2.0\Microsoft.Coyote.Actors.dll" target="lib\netstandard2.0" />
+    <file src="..\..\bin\netstandard2.0\Microsoft.Coyote.Actors.xml" target="lib\netstandard2.0" />
+    <file src="..\..\bin\netstandard2.0\Microsoft.Coyote.Actors.pdb" target="lib\netstandard2.0" />
+    <!-- Readme -->
+    <file src="..\..\README.md" target="docs\readme.md" />
+    <!-- Assets -->
+    <file src="..\..\docs\assets\images\icon.png" target="images" />
+  </files>
+</package>

Scripts/NuGet/Coyote.CLI.nuspec

@@ -4,7 +4,7 @@
     <id>Microsoft.Coyote.CLI</id>
     <version>$version$</version>
     <authors>Microsoft</authors>
-    <description>The Coyote command line tool.</description>
+    <description>The Coyote systematic testing command line tool.</description>
     <projectUrl>https://microsoft.github.io/coyote/</projectUrl>
     <repository type="git" url="https://github.com/microsoft/coyote"/>
     <license type="expression">MIT</license>
@@ -12,7 +12,7 @@
     <copyright>© Microsoft Corporation. All rights reserved.</copyright>
     <icon>images\icon.png</icon>
     <readme>docs\readme.md</readme>
-    <tags>asynchrony reliability tasks actors state-machines specifications testing</tags>
+    <tags>systematic-testing specifications concurrency dotnet csharp</tags>
     <packageTypes>
       <packageType name="DotnetTool" />
     </packageTypes>

Scripts/NuGet/Coyote.Test.nuspec

@@ -4,7 +4,7 @@
     <id>Microsoft.Coyote.Test</id>
     <version>$version$</version>
     <authors>Microsoft</authors>
-    <description>The Coyote systematic testing library and tools.</description>
+    <description>The Coyote systematic testing library and tool.</description>
     <projectUrl>https://microsoft.github.io/coyote/</projectUrl>
     <repository type="git" url="https://github.com/microsoft/coyote"/>
     <license type="expression">MIT</license>
@@ -12,10 +12,11 @@
     <copyright>© Microsoft Corporation. All rights reserved.</copyright>
     <icon>images\icon.png</icon>
     <readme>docs\readme.md</readme>
-    <tags>asynchrony reliability tasks actors state-machines specifications testing</tags>
+    <tags>systematic-testing specifications concurrency dotnet csharp</tags>
     <dependencies>
       <group targetFramework=".NET6.0">
         <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="Microsoft.Coyote.Actors" version="$version$"/>
         <dependency id="Microsoft.ApplicationInsights" version="2.20.0"/>
         <dependency id="Microsoft.AspNetCore.Http.Abstractions" version="2.2.0"/>
         <dependency id="Microsoft.Extensions.DependencyModel" version="6.0.0"/>
@@ -23,6 +24,7 @@
       </group>
       <group targetFramework=".NETCoreApp3.1">
         <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="Microsoft.Coyote.Actors" version="$version$"/>
         <dependency id="Microsoft.ApplicationInsights" version="2.20.0"/>
         <dependency id="Microsoft.AspNetCore.Http.Abstractions" version="2.2.0"/>
         <dependency id="Microsoft.Extensions.DependencyModel" version="6.0.0"/>
@@ -31,6 +33,7 @@
       </group>
       <group targetFramework=".NETStandard2.0">
         <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="Microsoft.Coyote.Actors" version="$version$"/>
         <dependency id="Microsoft.ApplicationInsights" version="2.20.0"/>
         <dependency id="Microsoft.AspNetCore.Http.Abstractions" version="2.2.0"/>
         <dependency id="Mono.Cecil" version="0.11.4"/>
@@ -38,6 +41,7 @@
       </group>
       <group targetFramework=".NETFramework4.6.2">
         <dependency id="Microsoft.Coyote" version="$version$"/>
+        <dependency id="Microsoft.Coyote.Actors" version="$version$"/>
         <dependency id="Microsoft.ApplicationInsights" version="2.20.0"/>
         <dependency id="Microsoft.AspNetCore.Http.Abstractions" version="2.2.0"/>
         <dependency id="Mono.Cecil" version="0.11.4"/>

Scripts/NuGet/Coyote.nuspec

@@ -4,7 +4,7 @@
     <id>Microsoft.Coyote</id>
     <version>$version$</version>
     <authors>Microsoft</authors>
-    <description>Coyote is a library for building reliable asynchronous software.</description>
+    <description>Coyote is a library and tool for testing concurrent C# code and deterministically reproducing bugs.</description>
     <projectUrl>https://microsoft.github.io/coyote/</projectUrl>
     <repository type="git" url="https://github.com/microsoft/coyote"/>
     <license type="expression">MIT</license>
@@ -12,7 +12,7 @@
     <copyright>© Microsoft Corporation. All rights reserved.</copyright>
     <icon>images\icon.png</icon>
     <readme>docs\readme.md</readme>
-    <tags>asynchrony reliability tasks actors state-machines specifications testing</tags>
+    <tags>systematic-testing specifications concurrency dotnet csharp</tags>
     <dependencies>
       <group targetFramework=".NET6.0">
         <dependency id="System.Threading.Tasks.Extensions" version="4.5.4"/>
@@ -23,10 +23,6 @@
       <group targetFramework=".NETStandard2.0">
         <dependency id="System.Threading.Tasks.Extensions" version="4.5.4"/>
       </group>
-      <group targetFramework=".NETFramework4.6.2">
-        <dependency id="System.Threading.Tasks.Extensions" version="4.5.4"/>
-        <dependency id="System.ValueTuple" version="4.5.0"/>
-      </group>
     </dependencies>
   </metadata>
   <files>
@@ -42,10 +38,6 @@
     <file src="..\..\bin\netstandard2.0\Microsoft.Coyote.dll" target="lib\netstandard2.0" />
     <file src="..\..\bin\netstandard2.0\Microsoft.Coyote.xml" target="lib\netstandard2.0" />
     <file src="..\..\bin\netstandard2.0\Microsoft.Coyote.pdb" target="lib\netstandard2.0" />
-    <!-- .NET Framework 4.6.2 -->
-    <file src="..\..\bin\net462\Microsoft.Coyote.dll" target="lib\net462" />
-    <file src="..\..\bin\net462\Microsoft.Coyote.xml" target="lib\net462" />
-    <file src="..\..\bin\net462\Microsoft.Coyote.pdb" target="lib\net462" />
     <!-- Readme -->
     <file src="..\..\README.md" target="docs\readme.md" />
     <!-- Assets -->

Scripts/build.ps1

@@ -85,19 +85,24 @@ if ($nuget.IsPresent -and $ci.IsPresent) {
             $cmd_options = "$cmd_options -Suffix $version_suffix"
         }
 
-        Write-Comment -text "Creating the 'Microsoft.Coyote' package." -color "magenta"
+        Write-Comment -text "Building the 'Microsoft.Coyote' package." -color "magenta"
         $command = "pack $PSScriptRoot/NuGet/Coyote.nuspec $cmd_options"
-        $error_msg = "Failed to build the Coyote NuGet package"
+        $error_msg = "Failed to build the 'Microsoft.Coyote' package"
         Invoke-ToolCommand -tool $nuget_cli -cmd $command -error_msg $error_msg
 
-        Write-Comment -text "Creating the 'Microsoft.Coyote.Test' package." -color "magenta"
+        Write-Comment -text "Building the 'Microsoft.Coyote.Actors' package." -color "magenta"
+        $command = "pack $PSScriptRoot/NuGet/Coyote.Actors.nuspec $cmd_options"
+        $error_msg = "Failed to build the 'Microsoft.Coyote.Actors' package"
+        Invoke-ToolCommand -tool $nuget_cli -cmd $command -error_msg $error_msg
+
+        Write-Comment -text "Building the 'Microsoft.Coyote.Test' package." -color "magenta"
         $command = "pack $PSScriptRoot/NuGet/Coyote.Test.nuspec $cmd_options"
-        $error_msg = "Failed to build the Coyote Test NuGet package"
+        $error_msg = "Failed to build the 'Microsoft.Coyote.Test' package"
         Invoke-ToolCommand -tool $nuget_cli -cmd $command -error_msg $error_msg
 
-        Write-Comment -text "Creating the 'Microsoft.Coyote.CLI' package." -color "magenta"
+        Write-Comment -text "Building the 'Microsoft.Coyote.CLI' package." -color "magenta"
         $command = "pack $PSScriptRoot/NuGet/Coyote.CLI.nuspec $cmd_options -Tool"
-        $error_msg = "Failed to build the Coyote CLI NuGet package"
+        $error_msg = "Failed to build the 'Microsoft.Coyote.CLI' package"
         Invoke-ToolCommand -tool $nuget_cli -cmd $command -error_msg $error_msg
     } else {
         Write-Comment -text "Building the Coyote NuGet packages supports only Windows." -color "yellow"

Scripts/gen-docs.ps1

@@ -51,14 +51,20 @@ Write-Host "Generating new markdown under $target"
 & $gendoc gen "$root_dir\bin\$framework\Microsoft.Coyote.dll" -o $target --namespace Microsoft.Coyote
 $coyotetoc = Get-Content -Path "$target\toc.yml"
 
-& $gendoc gen "$root_dir\bin\$framework\Microsoft.Coyote.Test.dll" -o $target --namespace Microsoft.Coyote.Test
-$newtoc = Get-Content -Path "$target\toc.yml"
-$newtoc = [System.Collections.ArrayList]$newtoc
-$newtoc.RemoveRange(0, 1); # remove -toc and assembly header
-$newtoc.InsertRange(0, $coyotetoc)
+& $gendoc gen "$root_dir\bin\$framework\Microsoft.Coyote.Actors.dll" -o $target --namespace Microsoft.Coyote.Actors
+$actorstoc = Get-Content -Path "$target\toc.yml"
+$actorstoc = [System.Collections.ArrayList]$actorstoc
+$actorstoc.RemoveRange(0, 1); # remove -toc and assembly header
+$actorstoc.InsertRange(0, $coyotetoc)
 
-# Save the merged toc containing both the contents of Microsoft.Coyote.dll and Microsoft.Coyote.Test.dll.
-Set-Content -Path "$target\toc.yml" -Value $newtoc
+& $gendoc gen "$root_dir\bin\$framework\Microsoft.Coyote.Test.dll" -o $target --namespace Microsoft.Coyote.Test
+$mergedtoc = Get-Content -Path "$target\toc.yml"
+$mergedtoc = [System.Collections.ArrayList]$mergedtoc
+$mergedtoc.RemoveRange(0, 1); # remove -toc and assembly header
+$mergedtoc.InsertRange(0, $actorstoc)
+
+# Save the merged toc containing the contents of all assemblies.
+Set-Content -Path "$target\toc.yml" -Value $mergedtoc
 
 Write-Host "Merging $toc..."
 # Now merge the new toc.

Source/Actors/Actors.csproj

@@ -0,0 +1,15 @@
+<Project Sdk="Microsoft.NET.Sdk">
+  <PropertyGroup>
+    <Description>The Coyote actor runtime and library.</Description>
+    <AssemblyName>Microsoft.Coyote.Actors</AssemblyName>
+    <RootNamespace>Microsoft.Coyote.Actors</RootNamespace>
+    <PackageTags>actors;state-machines;asynchronous;reactive;systematic-testing</PackageTags>
+    <OutputPath>..\..\bin\</OutputPath>
+    <Framework462Supported>false</Framework462Supported>
+  </PropertyGroup>
+  <Import Project="..\..\Common\build.props" />
+  <Import Project="..\..\Common\key.props" />
+  <ItemGroup>
+    <ProjectReference Include="..\..\Source\Core\Core.csproj" />
+  </ItemGroup>
+</Project>

Source/Actors/Coverage/ActorActivityCoverageReporter.cs

@@ -0,0 +1,244 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using Microsoft.Coyote.Coverage;
+
+namespace Microsoft.Coyote.Actors.Coverage
+{
+    /// <summary>
+    /// Reports actor activity coverage.
+    /// </summary>
+    internal class ActorActivityCoverageReporter : ActivityCoverageReporter
+    {
+        /// <summary>
+        /// Data structure containing information regarding testing coverage.
+        /// </summary>
+        private readonly ActorCoverageInfo CoverageInfo;
+
+        /// <summary>
+        /// Set of built in events which we hide in the coverage report.
+        /// </summary>
+        private readonly HashSet<string> BuiltInEvents = new HashSet<string>();
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="ActorActivityCoverageReporter"/> class.
+        /// </summary>
+        public ActorActivityCoverageReporter(ActorCoverageInfo coverageInfo)
+            : base(coverageInfo)
+        {
+            this.CoverageInfo = coverageInfo;
+            this.BuiltInEvents.Add(typeof(GotoStateEvent).FullName);
+            this.BuiltInEvents.Add(typeof(PushStateEvent).FullName);
+            this.BuiltInEvents.Add(typeof(DefaultEvent).FullName);
+        }
+
+        /// <inheritdoc/>
+        internal override void WriteCoverageText(TextWriter writer)
+        {
+            var machines = new List<string>(this.CoverageInfo.Machines);
+            machines.Sort(StringComparer.Ordinal);
+
+            var machineTypes = new Dictionary<string, string>();
+            foreach (var node in this.CoverageInfo.CoverageGraph.Nodes)
+            {
+                if (machines.Contains(node.Id))
+                {
+                    machineTypes[node.Id] = node.Category ?? ActorRuntimeLogGraphBuilder.StateMachineCategory;
+                }
+            }
+
+            // machines + "." + states => registered events
+            var uncoveredEvents = new Dictionary<string, HashSet<string>>();
+            foreach (var item in this.CoverageInfo.RegisteredActorEvents)
+            {
+                uncoveredEvents[item.Key] = new HashSet<string>(item.Value);
+            }
+
+            int totalEvents = (from h in uncoveredEvents select h.Value.Count).Sum();
+
+            // Now use the graph to find incoming links to each state and remove those from the list of uncovered events.
+            this.RemoveCoveredEvents(uncoveredEvents);
+
+            int totalUncoveredEvents = (from h in uncoveredEvents select h.Value.Count).Sum();
+            string eventCoverage = totalEvents is 0 ? "100.0" : ((totalEvents - totalUncoveredEvents) * 100.0 / totalEvents).ToString("F1");
+
+            if (machines.Count > 0)
+            {
+                WriteHeader(writer, string.Format("Total actor coverage: {0}%", eventCoverage));
+                foreach (var machine in machines)
+                {
+                    machineTypes.TryGetValue(machine, out string machineType);
+                    WriteHeader(writer, string.Format("{0}: {1}", machineType, machine));
+
+                    // Find all possible events for this machine.
+                    var uncoveredMachineEvents = new Dictionary<string, HashSet<string>>();
+                    var allMachineEvents = new Dictionary<string, HashSet<string>>();
+                    foreach (var item in this.CoverageInfo.RegisteredActorEvents)
+                    {
+                        var id = GetActorId(item.Key);
+                        if (id == machine)
+                        {
+                            uncoveredMachineEvents[item.Key] = new HashSet<string>(item.Value);
+                            allMachineEvents[item.Key] = new HashSet<string>(item.Value);
+                        }
+                    }
+
+                    // Now use the graph to find incoming links to each state in this machine and remove those from the list of uncovered events.
+                    this.RemoveCoveredEvents(uncoveredMachineEvents);
+
+                    int totalMachineEvents = (from h in allMachineEvents select h.Value.Count).Sum();
+                    var totalUncoveredMachineEvents = (from h in uncoveredMachineEvents select h.Value.Count).Sum();
+
+                    eventCoverage = totalMachineEvents is 0 ? "100.0" : ((totalMachineEvents - totalUncoveredMachineEvents) * 100.0 / totalMachineEvents).ToString("F1");
+                    writer.WriteLine("Event coverage: {0}%", eventCoverage);
+                    foreach (var state in this.CoverageInfo.MachinesToStates[machine])
+                    {
+                        var key = machine + "." + state;
+                        int totalStateEvents = (from h in allMachineEvents where h.Key == key select h.Value.Count).Sum();
+                        int uncoveredStateEvents = (from h in uncoveredMachineEvents where h.Key == key select h.Value.Count).Sum();
+
+                        writer.WriteLine();
+                        writer.WriteLine("\tState: {0}{1}", state, totalStateEvents > 0 && totalStateEvents == uncoveredStateEvents ? " is uncovered" : string.Empty);
+                        if (totalStateEvents is 0)
+                        {
+                            writer.WriteLine("\t\tState has no expected events, so coverage is 100%");
+                        }
+                        else if (totalStateEvents != uncoveredStateEvents)
+                        {
+                            eventCoverage = totalStateEvents is 0 ? "100.0" : ((totalStateEvents - uncoveredStateEvents) * 100.0 / totalStateEvents).ToString("F1");
+                            writer.WriteLine("\t\tState event coverage: {0}%", eventCoverage);
+                        }
+
+                        // Now use the graph to find incoming links to each state in this machine
+                        HashSet<string> stateIncomingStates = new HashSet<string>();
+                        HashSet<string> stateOutgoingStates = new HashSet<string>();
+                        foreach (var link in this.CoverageInfo.CoverageGraph.Links)
+                        {
+                            if (link.Category != "Contains")
+                            {
+                                string srcId = link.Source.Id;
+                                string srcMachine = GetActorId(srcId);
+                                string targetId = link.Target.Id;
+                                string targetMachine = GetActorId(targetId);
+                                bool intraMachineTransition = targetMachine == machine && srcMachine == machine;
+                                if (intraMachineTransition)
+                                {
+                                    foreach (string id in GetEventIds(link))
+                                    {
+                                        if (targetId == key)
+                                        {
+                                            // we want to show incoming/outgoing states within the current machine only.
+                                            stateIncomingStates.Add(GetStateName(srcId));
+                                        }
+
+                                        if (srcId == key)
+                                        {
+                                            // we want to show incoming/outgoing states within the current machine only.
+                                            stateOutgoingStates.Add(GetStateName(targetId));
+                                        }
+                                    }
+                                }
+                            }
+                        }
+
+                        HashSet<string> received = new HashSet<string>(this.CoverageInfo.ActorEventInfo.GetEventsReceived(key));
+                        this.RemoveBuiltInEvents(received);
+                        if (received.Count > 0)
+                        {
+                            writer.WriteLine("\t\tEvents received: {0}", string.Join(", ", SortHashSet(received)));
+                        }
+
+                        HashSet<string> sent = new HashSet<string>(this.CoverageInfo.ActorEventInfo.GetEventsSent(key));
+                        this.RemoveBuiltInEvents(sent);
+                        if (sent.Count > 0)
+                        {
+                            writer.WriteLine("\t\tEvents sent: {0}", string.Join(", ", SortHashSet(sent)));
+                        }
+
+                        var stateUncoveredEvents = (from h in uncoveredMachineEvents where h.Key == key select h.Value).FirstOrDefault();
+                        if (stateUncoveredEvents != null && stateUncoveredEvents.Count > 0)
+                        {
+                            writer.WriteLine("\t\tEvents not covered: {0}", string.Join(", ", SortHashSet(stateUncoveredEvents)));
+                        }
+
+                        if (stateIncomingStates.Count > 0)
+                        {
+                            writer.WriteLine("\t\tPrevious states: {0}", string.Join(", ", SortHashSet(stateIncomingStates)));
+                        }
+
+                        if (stateOutgoingStates.Count > 0)
+                        {
+                            writer.WriteLine("\t\tNext states: {0}", string.Join(", ", SortHashSet(stateOutgoingStates)));
+                        }
+                    }
+
+                    writer.WriteLine();
+                }
+
+                // Check if a non-actor event sender exists.
+                if (this.CoverageInfo.CoverageGraph.Links.Any(link => link.Source.Id == ActorRuntimeLogGraphBuilder.ExternalCodeName))
+                {
+                    WriteHeader(writer, ActorRuntimeLogGraphBuilder.ExternalCodeName);
+
+                    HashSet<string> sent = new HashSet<string>(this.CoverageInfo.ActorEventInfo.GetEventsSent(
+                        $"{ActorRuntimeLogGraphBuilder.ExternalCodeName}.{ActorRuntimeLogGraphBuilder.ExternalStateName}"));
+                    this.RemoveBuiltInEvents(sent);
+                    if (sent.Count > 0)
+                    {
+                        writer.WriteLine("Events sent: {0}", string.Join(", ", SortHashSet(sent)));
+                    }
+                }
+            }
+            else
+            {
+                WriteHeader(writer, "Total actor coverage: N/A");
+            }
+
+            base.WriteCoverageText(writer);
+        }
+
+        private void RemoveBuiltInEvents(HashSet<string> eventList)
+        {
+            foreach (var name in eventList.ToArray())
+            {
+                if (this.BuiltInEvents.Contains(name))
+                {
+                    eventList.Remove(name);
+                }
+            }
+        }
+
+        /// <summary>
+        /// Remove all events from expectedEvent that are found in the graph.
+        /// </summary>
+        /// <param name="expectedEvents">The list of all expected events organized by unique state Id.</param>
+        private void RemoveCoveredEvents(Dictionary<string, HashSet<string>> expectedEvents)
+        {
+            foreach (var pair in expectedEvents)
+            {
+                string stateId = pair.Key;
+                var eventSet = pair.Value;
+
+                foreach (var e in this.CoverageInfo.ActorEventInfo.GetEventsReceived(stateId))
+                {
+                    eventSet.Remove(e);
+                }
+            }
+        }
+
+        private static string GetActorId(string nodeId)
+        {
+            int i = nodeId.LastIndexOf(".");
+            if (i > 0)
+            {
+                return nodeId.Substring(0, i);
+            }
+
+            return nodeId;
+        }
+    }
+}

Source/Actors/Coverage/ActorCoverageInfo.cs

@@ -0,0 +1,139 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Collections.Generic;
+using System.Runtime.Serialization;
+using Microsoft.Coyote.Coverage;
+
+namespace Microsoft.Coyote.Actors.Coverage
+{
+    /// <summary>
+    /// Class for storing actor coverage-specific data across multiple testing iterations.
+    /// </summary>
+    [DataContract]
+    public class ActorCoverageInfo : CoverageInfo
+    {
+        /// <summary>
+        /// Set of known machines.
+        /// </summary>
+        [DataMember]
+        public HashSet<string> Machines { get; private set; }
+
+        /// <summary>
+        /// Map from machines to set of all states states defined in that machine.
+        /// </summary>
+        [DataMember]
+        public Dictionary<string, HashSet<string>> MachinesToStates { get; private set; }
+
+        /// <summary>
+        /// Set of (machine + "." + state => registered events). So all events that can
+        /// get us into each state.
+        /// </summary>
+        [DataMember]
+        public Dictionary<string, HashSet<string>> RegisteredActorEvents { get; private set; }
+
+        /// <summary>
+        /// Information about events sent and received.
+        /// </summary>
+        [DataMember]
+        public ActorEventCoverage ActorEventInfo { get; set; }
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="ActorCoverageInfo"/> class.
+        /// </summary>
+        public ActorCoverageInfo()
+            : base()
+        {
+            this.Machines = new HashSet<string>();
+            this.MachinesToStates = new Dictionary<string, HashSet<string>>();
+            this.RegisteredActorEvents = new Dictionary<string, HashSet<string>>();
+        }
+
+        /// <summary>
+        /// Checks if the machine type has already been registered for coverage.
+        /// </summary>
+        public bool IsMachineDeclared(string machineName) => this.MachinesToStates.ContainsKey(machineName);
+
+        /// <summary>
+        /// Declares a machine state.
+        /// </summary>
+        public void DeclareMachineState(string machine, string state) => this.AddMachineState(machine, state);
+
+        /// <summary>
+        /// Declares a registered machine state-event pair.
+        /// </summary>
+        public void DeclareMachineStateEventPair(string machine, string state, string eventName)
+        {
+            this.AddMachineState(machine, state);
+
+            string key = machine + "." + state;
+            this.AddActorEvent(key, eventName);
+        }
+
+        /// <summary>
+        /// Adds a new machine state.
+        /// </summary>
+        private void AddMachineState(string machineName, string stateName)
+        {
+            this.Machines.Add(machineName);
+            if (!this.MachinesToStates.ContainsKey(machineName))
+            {
+                this.MachinesToStates.Add(machineName, new HashSet<string>());
+            }
+
+            this.MachinesToStates[machineName].Add(stateName);
+        }
+
+        /// <summary>
+        /// Adds a new actor state.
+        /// </summary>
+        private void AddActorEvent(string key, string eventName)
+        {
+            if (!this.RegisteredActorEvents.ContainsKey(key))
+            {
+                this.RegisteredActorEvents.Add(key, new HashSet<string>());
+            }
+
+            this.RegisteredActorEvents[key].Add(eventName);
+        }
+
+        /// <inheritdoc/>
+        public override void Merge(CoverageInfo coverageInfo)
+        {
+            if (coverageInfo is ActorCoverageInfo actorCoverageInfo)
+            {
+                foreach (var machine in actorCoverageInfo.Machines)
+                {
+                    this.Machines.Add(machine);
+                }
+
+                foreach (var machine in actorCoverageInfo.MachinesToStates)
+                {
+                    foreach (var state in machine.Value)
+                    {
+                        this.DeclareMachineState(machine.Key, state);
+                    }
+                }
+
+                foreach (var tup in actorCoverageInfo.RegisteredActorEvents)
+                {
+                    foreach (var e in tup.Value)
+                    {
+                        this.AddActorEvent(tup.Key, e);
+                    }
+                }
+
+                if (this.ActorEventInfo is null)
+                {
+                    this.ActorEventInfo = actorCoverageInfo.ActorEventInfo;
+                }
+                else if (actorCoverageInfo.ActorEventInfo != null && this.ActorEventInfo != actorCoverageInfo.ActorEventInfo)
+                {
+                    this.ActorEventInfo.Merge(actorCoverageInfo.ActorEventInfo);
+                }
+            }
+
+            base.Merge(coverageInfo);
+        }
+    }
+}

Source/Actors/Coverage/ActorEventCoverage.cs

@@ -0,0 +1,101 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.Runtime.Serialization;
+
+namespace Microsoft.Coyote.Actors.Coverage
+{
+    /// <summary>
+    /// This class maintains information about events received and sent from each state of each actor.
+    /// </summary>
+    [DataContract]
+    public class ActorEventCoverage
+    {
+        /// <summary>
+        /// Map from states to the list of events received by that state.  The state id is fully qualified by
+        /// the actor id it belongs to.
+        /// </summary>
+        [DataMember]
+        private readonly Dictionary<string, HashSet<string>> EventsReceived = new Dictionary<string, HashSet<string>>();
+
+        /// <summary>
+        /// Map from states to the list of events sent by that state.  The state id is fully qualified by
+        /// the actor id it belongs to.
+        /// </summary>
+        [DataMember]
+        private readonly Dictionary<string, HashSet<string>> EventsSent = new Dictionary<string, HashSet<string>>();
+
+        internal void AddEventReceived(string stateId, string eventId)
+        {
+            if (!this.EventsReceived.TryGetValue(stateId, out HashSet<string> set))
+            {
+                set = new HashSet<string>();
+                this.EventsReceived[stateId] = set;
+            }
+
+            set.Add(eventId);
+        }
+
+        /// <summary>
+        /// Get list of events received by the given fully qualified state.
+        /// </summary>
+        /// <param name="stateId">The actor qualified state name.</param>
+        public IEnumerable<string> GetEventsReceived(string stateId)
+        {
+            if (this.EventsReceived.TryGetValue(stateId, out HashSet<string> set))
+            {
+                return set;
+            }
+
+            return Array.Empty<string>();
+        }
+
+        internal void AddEventSent(string stateId, string eventId)
+        {
+            if (!this.EventsSent.TryGetValue(stateId, out HashSet<string> set))
+            {
+                set = new HashSet<string>();
+                this.EventsSent[stateId] = set;
+            }
+
+            set.Add(eventId);
+        }
+
+        /// <summary>
+        /// Get list of events sent by the given state.
+        /// </summary>
+        /// <param name="stateId">The actor qualified state name.</param>
+        public IEnumerable<string> GetEventsSent(string stateId)
+        {
+            if (this.EventsSent.TryGetValue(stateId, out HashSet<string> set))
+            {
+                return set;
+            }
+
+            return Array.Empty<string>();
+        }
+
+        internal void Merge(ActorEventCoverage other)
+        {
+            MergeHashSets(this.EventsReceived, other.EventsReceived);
+            MergeHashSets(this.EventsSent, other.EventsSent);
+        }
+
+        private static void MergeHashSets(Dictionary<string, HashSet<string>> ours, Dictionary<string, HashSet<string>> theirs)
+        {
+            foreach (var pair in theirs)
+            {
+                var stateId = pair.Key;
+                if (!ours.TryGetValue(stateId, out HashSet<string> eventSet))
+                {
+                    eventSet = new HashSet<string>();
+                    ours[stateId] = eventSet;
+                }
+
+                eventSet.UnionWith(pair.Value);
+            }
+        }
+    }
+}

Source/Actors/Coverage/ActorRuntimeLogEventCoverage.cs

@@ -2,115 +2,24 @@
 // Licensed under the MIT License.
 
 using System;
-using System.Collections.Generic;
-using System.Runtime.Serialization;
 using Microsoft.Coyote.Actors.Timers;
+using Microsoft.Coyote.Coverage;
+using MonitorEvent = Microsoft.Coyote.Specifications.Monitor.Event;
 
 namespace Microsoft.Coyote.Actors.Coverage
 {
-    /// <summary>
-    /// This class maintains information about events received and sent from each state of each actor.
-    /// </summary>
-    [DataContract]
-    public class EventCoverage
-    {
-        /// <summary>
-        /// Map from states to the list of events received by that state.  The state id is fully qualified by
-        /// the actor id it belongs to.
-        /// </summary>
-        [DataMember]
-        private readonly Dictionary<string, HashSet<string>> EventsReceived = new Dictionary<string, HashSet<string>>();
-
-        /// <summary>
-        /// Map from states to the list of events sent by that state.  The state id is fully qualified by
-        /// the actor id it belongs to.
-        /// </summary>
-        [DataMember]
-        private readonly Dictionary<string, HashSet<string>> EventsSent = new Dictionary<string, HashSet<string>>();
-
-        internal void AddEventReceived(string stateId, string eventId)
-        {
-            if (!this.EventsReceived.TryGetValue(stateId, out HashSet<string> set))
-            {
-                set = new HashSet<string>();
-                this.EventsReceived[stateId] = set;
-            }
-
-            set.Add(eventId);
-        }
-
-        /// <summary>
-        /// Get list of events received by the given fully qualified state.
-        /// </summary>
-        /// <param name="stateId">The actor qualified state name.</param>
-        public IEnumerable<string> GetEventsReceived(string stateId)
-        {
-            if (this.EventsReceived.TryGetValue(stateId, out HashSet<string> set))
-            {
-                return set;
-            }
-
-            return Array.Empty<string>();
-        }
-
-        internal void AddEventSent(string stateId, string eventId)
-        {
-            if (!this.EventsSent.TryGetValue(stateId, out HashSet<string> set))
-            {
-                set = new HashSet<string>();
-                this.EventsSent[stateId] = set;
-            }
-
-            set.Add(eventId);
-        }
-
-        /// <summary>
-        /// Get list of events sent by the given state.
-        /// </summary>
-        /// <param name="stateId">The actor qualified state name.</param>
-        public IEnumerable<string> GetEventsSent(string stateId)
-        {
-            if (this.EventsSent.TryGetValue(stateId, out HashSet<string> set))
-            {
-                return set;
-            }
-
-            return Array.Empty<string>();
-        }
-
-        internal void Merge(EventCoverage other)
-        {
-            MergeHashSets(this.EventsReceived, other.EventsReceived);
-            MergeHashSets(this.EventsSent, other.EventsSent);
-        }
-
-        private static void MergeHashSets(Dictionary<string, HashSet<string>> ours, Dictionary<string, HashSet<string>> theirs)
-        {
-            foreach (var pair in theirs)
-            {
-                var stateId = pair.Key;
-                if (!ours.TryGetValue(stateId, out HashSet<string> eventSet))
-                {
-                    eventSet = new HashSet<string>();
-                    ours[stateId] = eventSet;
-                }
-
-                eventSet.UnionWith(pair.Value);
-            }
-        }
-    }
-
     internal class ActorRuntimeLogEventCoverage : IActorRuntimeLog
     {
-        private readonly EventCoverage InternalEventCoverage = new EventCoverage();
         private Event Dequeued;
 
+        public ActorEventCoverage ActorEventCoverage { get; } = new ActorEventCoverage();
+
+        public MonitorEventCoverage MonitorEventCoverage { get; } = new MonitorEventCoverage();
+
         public ActorRuntimeLogEventCoverage()
         {
         }
 
-        public EventCoverage EventCoverage => this.InternalEventCoverage;
-
         public void OnAssertionFailure(string error)
         {
         }
@@ -163,21 +72,12 @@ namespace Microsoft.Coyote.Actors.Coverage
 
         public void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
         {
-            this.OnEventHandled(id, handlingStateName);
-        }
-
-        private void OnEventHandled(ActorId id, string stateName)
-        {
-            if (this.Dequeued != null)
-            {
-                this.EventCoverage.AddEventReceived(GetStateId(id.Type, stateName), this.Dequeued.GetType().FullName);
-                this.Dequeued = null;
-            }
+            this.OnActorEventHandled(id, handlingStateName);
         }
 
         public void OnGotoState(ActorId id, string currentStateName, string newStateName)
         {
-            this.OnEventHandled(id, currentStateName);
+            this.OnActorEventHandled(id, currentStateName);
         }
 
         public void OnHalt(ActorId id, int inboxSize)
@@ -189,16 +89,16 @@ namespace Microsoft.Coyote.Actors.Coverage
         }
 
         public void OnMonitorProcessEvent(string monitorType, string stateName, string senderName,
-            string senderType, string senderStateName, Event e)
+            string senderType, string senderStateName, MonitorEvent e)
         {
             string eventName = e.GetType().FullName;
-            this.EventCoverage.AddEventReceived(GetStateId(monitorType, stateName), eventName);
+            this.MonitorEventCoverage.AddEventProcessed(GetStateId(monitorType, stateName), eventName);
         }
 
-        public void OnMonitorRaiseEvent(string monitorType, string stateName, Event e)
+        public void OnMonitorRaiseEvent(string monitorType, string stateName, MonitorEvent e)
         {
             string eventName = e.GetType().FullName;
-            this.EventCoverage.AddEventSent(GetStateId(monitorType, stateName), eventName);
+            this.MonitorEventCoverage.AddEventRaised(GetStateId(monitorType, stateName), eventName);
         }
 
         public void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState)
@@ -227,13 +127,13 @@ namespace Microsoft.Coyote.Actors.Coverage
 
         public void OnPushState(ActorId id, string currentStateName, string newStateName)
         {
-            this.OnEventHandled(id, currentStateName);
+            this.OnActorEventHandled(id, currentStateName);
         }
 
         public void OnRaiseEvent(ActorId id, string stateName, Event e)
         {
             string eventName = e.GetType().FullName;
-            this.EventCoverage.AddEventSent(GetStateId(id.Type, stateName), eventName);
+            this.ActorEventCoverage.AddEventSent(GetStateId(id.Type, stateName), eventName);
         }
 
         public void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
@@ -244,14 +144,14 @@ namespace Microsoft.Coyote.Actors.Coverage
         public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
         {
             string eventName = e.GetType().FullName;
-            this.EventCoverage.AddEventReceived(GetStateId(id.Type, stateName), eventName);
+            this.ActorEventCoverage.AddEventReceived(GetStateId(id.Type, stateName), eventName);
         }
 
         public void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
             Event e, Guid eventGroupId, bool isTargetHalted)
         {
             string eventName = e.GetType().FullName;
-            this.EventCoverage.AddEventSent(GetStateId(senderType, senderStateName), eventName);
+            this.ActorEventCoverage.AddEventSent(GetStateId(senderType, senderStateName), eventName);
         }
 
         public void OnStateTransition(ActorId id, string stateName, bool isEntry)
@@ -270,6 +170,15 @@ namespace Microsoft.Coyote.Actors.Coverage
         {
         }
 
+        private void OnActorEventHandled(ActorId id, string stateName)
+        {
+            if (this.Dequeued != null)
+            {
+                this.ActorEventCoverage.AddEventReceived(GetStateId(id.Type, stateName), this.Dequeued.GetType().FullName);
+                this.Dequeued = null;
+            }
+        }
+
         private static string GetStateId(string actorType, string stateName)
         {
             string id = ResolveActorTypeName(actorType);

Source/Actors/Coverage/ActorRuntimeLogGraphBuilder.cs

@@ -4,11 +4,10 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
-using System.Runtime.Serialization;
-using System.Text;
-using System.Xml.Linq;
 using Microsoft.Coyote.Actors.Timers;
 using Microsoft.Coyote.Actors.Timers.Mocks;
+using Microsoft.Coyote.Coverage;
+using MonitorEvent = Microsoft.Coyote.Specifications.Monitor.Event;
 
 namespace Microsoft.Coyote.Actors.Coverage
 {
@@ -18,16 +17,16 @@ namespace Microsoft.Coyote.Actors.Coverage
     /// </summary>
     internal class ActorRuntimeLogGraphBuilder : IActorRuntimeLog
     {
-        private const string ExternalCodeName = "ExternalCode";
-        private const string ExternalStateName = "ExternalState";
-        private const string StateMachineCategory = "StateMachine";
         private const string ActorCategory = "Actor";
+        internal const string StateMachineCategory = "StateMachine";
         private const string MonitorCategory = "Monitor";
+        internal const string ExternalCodeName = "ExternalCode";
+        internal const string ExternalStateName = "ExternalState";
 
         /// <summary>
-        /// The currently manipulated graph.
+        /// The currently manipulated coverage graph.
         /// </summary>
-        private Graph CurrentGraph;
+        private CoverageGraph CurrentGraph;
 
         /// <summary>
         /// Current dequeued event.
@@ -72,20 +71,9 @@ namespace Microsoft.Coyote.Actors.Coverage
         internal TextWriter Logger { get; set; }
 
         /// <summary>
-        /// Get the Graph object built by this logger.
+        /// Get the <see cref="CoverageGraph"/> object built by this logger.
         /// </summary>
-        internal Graph Graph
-        {
-            get
-            {
-                if (this.CurrentGraph is null)
-                {
-                    this.CurrentGraph = new Graph();
-                }
-
-                return this.CurrentGraph;
-            }
-        }
+        internal CoverageGraph Graph => this.CurrentGraph ?? new CoverageGraph();
 
         private class DoActionEvent : Event
         {
@@ -116,7 +104,7 @@ namespace Microsoft.Coyote.Actors.Coverage
         {
             this.MergeEventLinks = mergeEventLinks;
             this.CollapseInstances = collapseInstances;
-            this.CurrentGraph = new Graph();
+            this.CurrentGraph = new CoverageGraph();
         }
 
         /// <inheritdoc/>
@@ -125,13 +113,13 @@ namespace Microsoft.Coyote.Actors.Coverage
             lock (this.Inbox)
             {
                 var resolvedId = this.GetResolveActorId(id?.Name, id?.Type);
-                GraphNode node = this.Graph.GetOrCreateNode(resolvedId);
+                CoverageGraph.Node node = this.Graph.GetOrCreateNode(resolvedId);
                 node.Category = ActorCategory;
 
                 if (!string.IsNullOrEmpty(creatorName))
                 {
                     var creatorId = this.GetResolveActorId(creatorName, creatorType);
-                    GraphNode creator = this.Graph.GetOrCreateNode(creatorId);
+                    CoverageGraph.Node creator = this.Graph.GetOrCreateNode(creatorId);
                     this.GetOrCreateEventLink(creator, node, new EventInfo() { Event = "CreateActor" });
                 }
             }
@@ -143,13 +131,13 @@ namespace Microsoft.Coyote.Actors.Coverage
             lock (this.Inbox)
             {
                 var resolvedId = this.GetResolveActorId(id?.Name, id?.Type);
-                GraphNode node = this.Graph.GetOrCreateNode(resolvedId);
+                CoverageGraph.Node node = this.Graph.GetOrCreateNode(resolvedId);
                 node.Category = StateMachineCategory;
 
                 if (!string.IsNullOrEmpty(creatorName))
                 {
                     var creatorId = this.GetResolveActorId(creatorName, creatorType);
-                    GraphNode creator = this.Graph.GetOrCreateNode(creatorId);
+                    CoverageGraph.Node creator = this.Graph.GetOrCreateNode(creatorId);
                     this.GetOrCreateEventLink(creator, node, new EventInfo() { Event = "CreateActor" });
                 }
             }
@@ -331,7 +319,7 @@ namespace Microsoft.Coyote.Actors.Coverage
             }
         }
 
-        private int? GetLinkIndex(GraphNode source, GraphNode target, string id)
+        private int? GetLinkIndex(CoverageGraph.Node source, CoverageGraph.Node target, string id)
         {
             if (this.MergeEventLinks)
             {
@@ -396,7 +384,7 @@ namespace Microsoft.Coyote.Actors.Coverage
         {
             lock (this.Inbox)
             {
-                GraphNode node = this.Graph.GetOrCreateNode(monitorType, monitorType);
+                CoverageGraph.Node node = this.Graph.GetOrCreateNode(monitorType, monitorType);
                 node.Category = MonitorCategory;
             }
         }
@@ -421,7 +409,7 @@ namespace Microsoft.Coyote.Actors.Coverage
 
         /// <inheritdoc/>
         public void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, string senderType,
-            string senderStateName, Event e)
+            string senderStateName, MonitorEvent e)
         {
             lock (this.Inbox)
             {
@@ -439,7 +427,7 @@ namespace Microsoft.Coyote.Actors.Coverage
         }
 
         /// <inheritdoc/>
-        public void OnMonitorRaiseEvent(string monitorType, string stateName, Event e)
+        public void OnMonitorRaiseEvent(string monitorType, string stateName, MonitorEvent e)
         {
             // Raising event to self.
             string eventName = e.GetType().FullName;
@@ -515,9 +503,9 @@ namespace Microsoft.Coyote.Actors.Coverage
         /// </summary>
         /// <param name="reset">Set to true will reset the graph for the next iteration.</param>
         /// <returns>The graph.</returns>
-        internal Graph SnapshotGraph(bool reset)
+        internal CoverageGraph SnapshotGraph(bool reset)
         {
-            Graph result = this.CurrentGraph;
+            CoverageGraph result = this.CurrentGraph;
             if (reset)
             {
                 // Reset the graph to start fresh.
@@ -606,9 +594,9 @@ namespace Microsoft.Coyote.Actors.Coverage
             }
         }
 
-        private GraphNode GetOrCreateChild(string name, string type, string stateName, string label = null)
+        private CoverageGraph.Node GetOrCreateChild(string name, string type, string stateName, string label = null)
         {
-            GraphNode child = null;
+            CoverageGraph.Node child = null;
             lock (this.Inbox)
             {
                 this.AddNamespace(type);
@@ -619,7 +607,7 @@ namespace Microsoft.Coyote.Actors.Coverage
                 stateName = this.GetLabel(name, type, stateName);
 
                 string id = this.GetResolveActorId(name, type);
-                GraphNode parent = this.Graph.GetOrCreateNode(id);
+                CoverageGraph.Node parent = this.Graph.GetOrCreateNode(id);
                 parent.AddAttribute("Group", "Expanded");
 
                 if (string.IsNullOrEmpty(label))
@@ -639,9 +627,9 @@ namespace Microsoft.Coyote.Actors.Coverage
             return child;
         }
 
-        private GraphLink GetOrCreateEventLink(GraphNode source, GraphNode target, EventInfo e)
+        private CoverageGraph.Link GetOrCreateEventLink(CoverageGraph.Node source, CoverageGraph.Node target, EventInfo e)
         {
-            GraphLink link = null;
+            CoverageGraph.Link link = null;
             lock (this.Inbox)
             {
                 string label = this.GetEventLabel(e.Event);
@@ -743,571 +731,4 @@ namespace Microsoft.Coyote.Actors.Coverage
             return null;
         }
     }
-
-    /// <summary>
-    /// A directed graph made up of Nodes and Links.
-    /// </summary>
-    [DataContract]
-    public class Graph
-    {
-        internal const string DgmlNamespace = "http://schemas.microsoft.com/vs/2009/dgml";
-
-        // These [DataMember] fields are here so we can serialize the Graph across parallel or distributed
-        // test processes without losing any information.  There is more information here than in the serialized
-        // DGML which is we we can't just use Save/LoadDgml to do the same.
-
-        [DataMember]
-        private readonly Dictionary<string, GraphNode> InternalNodes = new Dictionary<string, GraphNode>();
-        [DataMember]
-        private readonly Dictionary<string, GraphLink> InternalLinks = new Dictionary<string, GraphLink>();
-        // last used index for simple link key "a->b".
-        [DataMember]
-        private readonly Dictionary<string, int> InternalNextLinkIndex = new Dictionary<string, int>();
-        // maps augmented link key to the index that has been allocated for that link id "a->b(goto)" => 0
-        [DataMember]
-        private readonly Dictionary<string, int> InternalAllocatedLinkIndexes = new Dictionary<string, int>();
-        [DataMember]
-        private readonly Dictionary<string, string> InternalAllocatedLinkIds = new Dictionary<string, string>();
-
-        /// <summary>
-        /// Return the current list of nodes (in no particular order).
-        /// </summary>
-        public IEnumerable<GraphNode> Nodes
-        {
-            get { return this.InternalNodes.Values; }
-        }
-
-        /// <summary>
-        /// Return the current list of links (in no particular order).
-        /// </summary>
-        public IEnumerable<GraphLink> Links
-        {
-            get
-            {
-                if (this.InternalLinks is null)
-                {
-                    return Array.Empty<GraphLink>();
-                }
-
-                return this.InternalLinks.Values;
-            }
-        }
-
-        /// <summary>
-        /// Get existing node or null.
-        /// </summary>
-        /// <param name="id">The id of the node.</param>
-        public GraphNode GetNode(string id)
-        {
-            this.InternalNodes.TryGetValue(id, out GraphNode node);
-            return node;
-        }
-
-        /// <summary>
-        /// Get existing node or create a new one with the given id and label.
-        /// </summary>
-        /// <returns>Returns the new node or the existing node if it was already defined.</returns>
-        public GraphNode GetOrCreateNode(string id, string label = null, string category = null)
-        {
-            if (!this.InternalNodes.TryGetValue(id, out GraphNode node))
-            {
-                node = new GraphNode(id, label, category);
-                this.InternalNodes.Add(id, node);
-            }
-
-            return node;
-        }
-
-        /// <summary>
-        /// Get existing node or create a new one with the given id and label.
-        /// </summary>
-        /// <returns>Returns the new node or the existing node if it was already defined.</returns>
-        private GraphNode GetOrCreateNode(GraphNode newNode)
-        {
-            if (!this.InternalNodes.ContainsKey(newNode.Id))
-            {
-                this.InternalNodes.Add(newNode.Id, newNode);
-            }
-
-            return newNode;
-        }
-
-        /// <summary>
-        /// Get existing link or create a new one connecting the given source and target nodes.
-        /// </summary>
-        /// <returns>The new link or the existing link if it was already defined.</returns>
-        public GraphLink GetOrCreateLink(GraphNode source, GraphNode target, int? index = null, string linkLabel = null, string category = null)
-        {
-            string key = source.Id + "->" + target.Id;
-            if (index.HasValue)
-            {
-                key += string.Format("({0})", index.Value);
-            }
-
-            if (!this.InternalLinks.TryGetValue(key, out GraphLink link))
-            {
-                link = new GraphLink(source, target, linkLabel, category);
-                if (index.HasValue)
-                {
-                    link.Index = index.Value;
-                }
-
-                this.InternalLinks.Add(key, link);
-            }
-
-            return link;
-        }
-
-        internal int GetUniqueLinkIndex(GraphNode source, GraphNode target, string id)
-        {
-            // augmented key
-            string key = string.Format("{0}->{1}({2})", source.Id, target.Id, id);
-            if (this.InternalAllocatedLinkIndexes.TryGetValue(key, out int index))
-            {
-                return index;
-            }
-
-            // allocate a new index for the simple key
-            var simpleKey = string.Format("{0}->{1}", source.Id, target.Id);
-            if (this.InternalNextLinkIndex.TryGetValue(simpleKey, out index))
-            {
-                index++;
-            }
-
-            this.InternalNextLinkIndex[simpleKey] = index;
-
-            // remember this index has been allocated for this link id.
-            this.InternalAllocatedLinkIndexes[key] = index;
-
-            // remember the original id associated with this link index.
-            key = string.Format("{0}->{1}({2})", source.Id, target.Id, index);
-            this.InternalAllocatedLinkIds[key] = id;
-
-            return index;
-        }
-
-        /// <summary>
-        /// Serialize the graph to a DGML string.
-        /// </summary>
-        public override string ToString()
-        {
-            using var writer = new StringWriter();
-            this.WriteDgml(writer, false);
-            return writer.ToString();
-        }
-
-        internal void SaveDgml(string graphFilePath, bool includeDefaultStyles)
-        {
-            using StreamWriter writer = new StreamWriter(graphFilePath, false, Encoding.UTF8);
-            this.WriteDgml(writer, includeDefaultStyles);
-        }
-
-        /// <summary>
-        /// Serialize the graph to DGML.
-        /// </summary>
-        public void WriteDgml(TextWriter writer, bool includeDefaultStyles)
-        {
-            writer.WriteLine("<DirectedGraph xmlns='{0}'>", DgmlNamespace);
-            writer.WriteLine("  <Nodes>");
-
-            if (this.InternalNodes != null)
-            {
-                List<string> nodes = new List<string>(this.InternalNodes.Keys);
-                nodes.Sort(StringComparer.Ordinal);
-                foreach (var id in nodes)
-                {
-                    GraphNode node = this.InternalNodes[id];
-                    writer.Write("    <Node Id='{0}'", node.Id);
-
-                    if (!string.IsNullOrEmpty(node.Label))
-                    {
-                        writer.Write(" Label='{0}'", node.Label);
-                    }
-
-                    if (!string.IsNullOrEmpty(node.Category))
-                    {
-                        writer.Write(" Category='{0}'", node.Category);
-                    }
-
-                    node.WriteAttributes(writer);
-                    writer.WriteLine("/>");
-                }
-            }
-
-            writer.WriteLine("  </Nodes>");
-            writer.WriteLine("  <Links>");
-
-            if (this.InternalLinks != null)
-            {
-                List<string> links = new List<string>(this.InternalLinks.Keys);
-                links.Sort(StringComparer.Ordinal);
-                foreach (var id in links)
-                {
-                    GraphLink link = this.InternalLinks[id];
-                    writer.Write("    <Link Source='{0}' Target='{1}'", link.Source.Id, link.Target.Id);
-                    if (!string.IsNullOrEmpty(link.Label))
-                    {
-                        writer.Write(" Label='{0}'", link.Label);
-                    }
-
-                    if (!string.IsNullOrEmpty(link.Category))
-                    {
-                        writer.Write(" Category='{0}'", link.Category);
-                    }
-
-                    if (link.Index.HasValue)
-                    {
-                        writer.Write(" Index='{0}'", link.Index.Value);
-                    }
-
-                    link.WriteAttributes(writer);
-                    writer.WriteLine("/>");
-                }
-            }
-
-            writer.WriteLine("  </Links>");
-            if (includeDefaultStyles)
-            {
-                writer.WriteLine(
-@"  <Styles>
-    <Style TargetType=""Node"" GroupLabel=""Error"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('Error')"" />
-      <Setter Property=""Background"" Value=""#FFC15656"" />
-    </Style>
-    <Style TargetType=""Node"" GroupLabel=""Actor"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('Actor')"" />
-      <Setter Property=""Background"" Value=""#FF57AC56"" />
-    </Style>
-    <Style TargetType=""Node"" GroupLabel=""Monitor"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('Monitor')"" />
-      <Setter Property=""Background"" Value=""#FF558FDA"" />
-    </Style>
-    <Style TargetType=""Link"" GroupLabel=""halt"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('halt')"" />
-      <Setter Property=""Stroke"" Value=""#FFFF6C6C"" />
-      <Setter Property=""StrokeDashArray"" Value=""4 2"" />
-    </Style>
-    <Style TargetType=""Link"" GroupLabel=""push"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('push')"" />
-      <Setter Property=""Stroke"" Value=""#FF7380F5"" />
-      <Setter Property=""StrokeDashArray"" Value=""4 2"" />
-    </Style>
-    <Style TargetType=""Link"" GroupLabel=""pop"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('pop')"" />
-      <Setter Property=""Stroke"" Value=""#FF7380F5"" />
-      <Setter Property=""StrokeDashArray"" Value=""4 2"" />
-    </Style>
-  </Styles>");
-            }
-
-            writer.WriteLine("</DirectedGraph>");
-        }
-
-        /// <summary>
-        /// Load a DGML file into a new Graph object.
-        /// </summary>
-        /// <param name="graphFilePath">Full path to the DGML file.</param>
-        /// <returns>The loaded Graph object.</returns>
-        public static Graph LoadDgml(string graphFilePath)
-        {
-            XDocument doc = XDocument.Load(graphFilePath);
-            Graph result = new Graph();
-            var ns = doc.Root.Name.Namespace;
-            if (ns != DgmlNamespace)
-            {
-                throw new InvalidOperationException(string.Format(
-                    "File '{0}' does not contain the DGML namespace", graphFilePath));
-            }
-
-            foreach (var e in doc.Root.Element(ns + "Nodes").Elements(ns + "Node"))
-            {
-                var id = (string)e.Attribute("Id");
-                var label = (string)e.Attribute("Label");
-                var category = (string)e.Attribute("Category");
-
-                GraphNode node = new GraphNode(id, label, category);
-                node.AddDgmlProperties(e);
-                result.GetOrCreateNode(node);
-            }
-
-            foreach (var e in doc.Root.Element(ns + "Links").Elements(ns + "Link"))
-            {
-                var srcId = (string)e.Attribute("Source");
-                var targetId = (string)e.Attribute("Target");
-                var label = (string)e.Attribute("Label");
-                var category = (string)e.Attribute("Category");
-                var srcNode = result.GetOrCreateNode(srcId);
-                var targetNode = result.GetOrCreateNode(targetId);
-                XAttribute indexAttr = e.Attribute("index");
-                int? index = null;
-                if (indexAttr != null)
-                {
-                    index = (int)indexAttr;
-                }
-
-                var link = result.GetOrCreateLink(srcNode, targetNode, index, label, category);
-                link.AddDgmlProperties(e);
-            }
-
-            return result;
-        }
-
-        /// <summary>
-        /// Merge the given graph so that this graph becomes a superset of both graphs.
-        /// </summary>
-        /// <param name="other">The new graph to merge into this graph.</param>
-        public void Merge(Graph other)
-        {
-            foreach (var node in other.InternalNodes.Values)
-            {
-                var newNode = this.GetOrCreateNode(node.Id, node.Label, node.Category);
-                newNode.Merge(node);
-            }
-
-            foreach (var link in other.InternalLinks.Values)
-            {
-                var source = this.GetOrCreateNode(link.Source.Id, link.Source.Label, link.Source.Category);
-                var target = this.GetOrCreateNode(link.Target.Id, link.Target.Label, link.Target.Category);
-                int? index = null;
-                if (link.Index.HasValue)
-                {
-                    // ouch, link indexes cannot be compared across Graph instances, we need to assign a new index here.
-                    string key = string.Format("{0}->{1}({2})", source.Id, target.Id, link.Index.Value);
-                    string linkId = other.InternalAllocatedLinkIds[key];
-                    index = this.GetUniqueLinkIndex(source, target, linkId);
-                }
-
-                var newLink = this.GetOrCreateLink(source, target, index, link.Label, link.Category);
-                newLink.Merge(link);
-            }
-        }
-    }
-
-    /// <summary>
-    /// A Node of a Graph.
-    /// </summary>
-    [DataContract]
-    public class GraphObject
-    {
-        /// <summary>
-        /// Optional list of attributes for the node.
-        /// </summary>
-        [DataMember]
-        public Dictionary<string, string> Attributes { get; internal set; }
-
-        /// <summary>
-        /// Optional list of attributes that have a multi-part value.
-        /// </summary>
-        [DataMember]
-        public Dictionary<string, HashSet<string>> AttributeLists { get; internal set; }
-
-        /// <summary>
-        /// Add an attribute to the node.
-        /// </summary>
-        public void AddAttribute(string name, string value)
-        {
-            if (this.Attributes is null)
-            {
-                this.Attributes = new Dictionary<string, string>();
-            }
-
-            this.Attributes[name] = value;
-        }
-
-        /// <summary>
-        /// Creates a compound attribute value containing a merged list of unique values.
-        /// </summary>
-        /// <param name="key">The attribute name.</param>
-        /// <param name="value">The new value to add to the unique list.</param>
-        public int AddListAttribute(string key, string value)
-        {
-            if (this.AttributeLists is null)
-            {
-                this.AttributeLists = new Dictionary<string, HashSet<string>>();
-            }
-
-            if (!this.AttributeLists.TryGetValue(key, out HashSet<string> list))
-            {
-                list = new HashSet<string>();
-                this.AttributeLists[key] = list;
-            }
-
-            list.Add(value);
-            return list.Count;
-        }
-
-        internal void WriteAttributes(TextWriter writer)
-        {
-            if (this.Attributes != null)
-            {
-                List<string> names = new List<string>(this.Attributes.Keys);
-                names.Sort(StringComparer.Ordinal);  // creates a more stable output file (can be handy for expected output during testing).
-                foreach (string name in names)
-                {
-                    var value = this.Attributes[name];
-                    writer.Write(" {0}='{1}'", name, value);
-                }
-            }
-
-            if (this.AttributeLists != null)
-            {
-                List<string> names = new List<string>(this.AttributeLists.Keys);
-                names.Sort(StringComparer.Ordinal);  // creates a more stable output file (can be handy for expected output during testing).
-                foreach (string name in names)
-                {
-                    var value = this.AttributeLists[name];
-                    writer.Write(" {0}='{1}'", name, string.Join(",", value));
-                }
-            }
-        }
-
-        internal void Merge(GraphObject other)
-        {
-            if (other.Attributes != null)
-            {
-                foreach (var key in other.Attributes.Keys)
-                {
-                    this.AddAttribute(key, other.Attributes[key]);
-                }
-            }
-
-            if (other.AttributeLists != null)
-            {
-                foreach (var key in other.AttributeLists.Keys)
-                {
-                    foreach (var value in other.AttributeLists[key])
-                    {
-                        this.AddListAttribute(key, value);
-                    }
-                }
-            }
-        }
-    }
-
-    /// <summary>
-    /// A Node of a Graph.
-    /// </summary>
-    [DataContract]
-    public class GraphNode : GraphObject
-    {
-        /// <summary>
-        /// The unique Id of the Node within the Graph.
-        /// </summary>
-        [DataMember]
-        public string Id { get; internal set; }
-
-        /// <summary>
-        /// An optional display label for the node (does not need to be unique).
-        /// </summary>
-        [DataMember]
-        public string Label { get; internal set; }
-
-        /// <summary>
-        /// An optional category for the node.
-        /// </summary>
-        [DataMember]
-        public string Category { get; internal set; }
-
-        /// <summary>
-        /// Initializes a new instance of the <see cref="GraphNode"/> class.
-        /// </summary>
-        public GraphNode(string id, string label, string category)
-        {
-            this.Id = id;
-            this.Label = label;
-            this.Category = category;
-        }
-
-        /// <summary>
-        /// Add additional properties from XML element.
-        /// </summary>
-        /// <param name="e">An XML element representing the graph node in DGML format.</param>
-        public void AddDgmlProperties(XElement e)
-        {
-            foreach (XAttribute a in e.Attributes())
-            {
-                switch (a.Name.LocalName)
-                {
-                    case "Id":
-                    case "Label":
-                    case "Category":
-                        break;
-                    default:
-                        this.AddAttribute(a.Name.LocalName, a.Value);
-                        break;
-                }
-            }
-        }
-    }
-
-    /// <summary>
-    /// A Link represents a directed graph connection between two Nodes.
-    /// </summary>
-    [DataContract]
-    public class GraphLink : GraphObject
-    {
-        /// <summary>
-        /// An optional display label for the link.
-        /// </summary>
-        [DataMember]
-        public string Label { get; internal set; }
-
-        /// <summary>
-        /// An optional category for the link.
-        /// The special category "Contains" is reserved for building groups.
-        /// </summary>
-        [DataMember]
-        public string Category { get; internal set; }
-
-        /// <summary>
-        /// The source end of the link.
-        /// </summary>
-        [DataMember]
-        public GraphNode Source { get; internal set; }
-
-        /// <summary>
-        /// The target end of the link.
-        /// </summary>
-        [DataMember]
-        public GraphNode Target { get; internal set; }
-
-        /// <summary>
-        /// The optional link index.
-        /// </summary>
-        [DataMember]
-        public int? Index { get; internal set; }
-
-        /// <summary>
-        /// Initializes a new instance of the <see cref="GraphLink"/> class.
-        /// </summary>
-        public GraphLink(GraphNode source, GraphNode target, string label, string category)
-        {
-            this.Source = source;
-            this.Target = target;
-            this.Label = label;
-            this.Category = category;
-        }
-
-        /// <summary>
-        /// Add additional properties from XML element.
-        /// </summary>
-        /// <param name="e">An XML element representing the graph node in DGML format.</param>
-        public void AddDgmlProperties(XElement e)
-        {
-            foreach (XAttribute a in e.Attributes())
-            {
-                switch (a.Name.LocalName)
-                {
-                    case "Source":
-                    case "Target":
-                    case "Label":
-                    case "Category":
-                        break;
-                    default:
-                        this.AddAttribute(a.Name.LocalName, a.Value);
-                        break;
-                }
-            }
-        }
-    }
 }

Source/Actors/Events/DefaultEvent.cs

@@ -13,7 +13,7 @@ namespace Microsoft.Coyote.Actors
     public sealed class DefaultEvent : Event
     {
         /// <summary>
-        /// Gets a <see cref="DefaultEvent"/> instance.
+        /// Gets a cached <see cref="DefaultEvent"/> instance.
         /// </summary>
         public static DefaultEvent Instance { get; } = new DefaultEvent();
 

Source/Actors/Events/Event.cs

@@ -3,10 +3,11 @@
 
 using System.Runtime.Serialization;
 
-namespace Microsoft.Coyote
+namespace Microsoft.Coyote.Actors
 {
     /// <summary>
-    /// Abstract class representing an event.
+    /// Abstract class representing an event that can be send to
+    /// an <see cref="Actor"/> or <see cref="StateMachine"/>.
     /// </summary>
     [DataContract]
     public abstract class Event

Source/Actors/Properties/InternalsVisibleTo.cs

@@ -0,0 +1,70 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Runtime.CompilerServices;
+
+// Libraries
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Test,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+
+// Tools
+[assembly: InternalsVisibleTo("Coyote,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("CoyoteCoverageReportMerger,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+
+// Tests
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Common,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Runtime,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Rewriting,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.BugFinding,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Actors,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Actors.BugFinding,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
+[assembly: InternalsVisibleTo("Tests.Performance,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]

Source/Actors/Runtime/Actor.cs

@@ -14,6 +14,7 @@ using Microsoft.Coyote.Actors.Coverage;
 using Microsoft.Coyote.Actors.Timers;
 using Microsoft.Coyote.Logging;
 using Microsoft.Coyote.Runtime;
+using MonitorEvent = Microsoft.Coyote.Specifications.Monitor.Event;
 
 namespace Microsoft.Coyote.Actors
 {
@@ -342,16 +343,14 @@ namespace Microsoft.Coyote.Actors
         }
 
         /// <summary>
-        /// Returns a nondeterministic boolean choice, that can be
-        /// controlled during analysis or testing.
+        /// Returns a nondeterministic boolean choice, that can be controlled during testing.
         /// </summary>
         /// <returns>The controlled nondeterministic choice.</returns>
         protected bool RandomBoolean() => this.Context.GetNondeterministicBooleanChoice(this.Id.Name, this.Id.Type);
 
         /// <summary>
-        /// Returns a nondeterministic integer, that can be controlled during
-        /// analysis or testing. The value is used to generate an integer in
-        /// the range [0..maxValue).
+        /// Returns a nondeterministic integer, that can be controlled during testing. The value
+        /// is used to generate an integer in the range [0..maxValue).
         /// </summary>
         /// <param name="maxValue">The max value.</param>
         /// <returns>The controlled nondeterministic integer.</returns>
@@ -359,18 +358,18 @@ namespace Microsoft.Coyote.Actors
             this.Context.GetNondeterministicIntegerChoice(maxValue, this.Id.Name, this.Id.Type);
 
         /// <summary>
-        /// Invokes the specified monitor with the specified <see cref="Event"/>.
+        /// Invokes the specified monitor with the specified <see cref="MonitorEvent"/>.
         /// </summary>
         /// <typeparam name="T">Type of the monitor.</typeparam>
-        /// <param name="e">Event to send to the monitor.</param>
-        protected void Monitor<T>(Event e) => this.Monitor(typeof(T), e);
+        /// <param name="e">The <see cref="MonitorEvent"/> to send to the monitor.</param>
+        protected void Monitor<T>(MonitorEvent e) => this.Monitor(typeof(T), e);
 
         /// <summary>
-        /// Invokes the specified monitor with the specified event.
+        /// Invokes the specified monitor with the specified <see cref="MonitorEvent"/>.
         /// </summary>
         /// <param name="type">Type of the monitor.</param>
-        /// <param name="e">The event to send.</param>
-        protected void Monitor(Type type, Event e)
+        /// <param name="e">The <see cref="MonitorEvent"/> to send to the monitor.</param>
+        protected void Monitor(Type type, MonitorEvent e)
         {
             this.Assert(e != null, "{0} is sending a null event.", this.Id);
             this.Context.InvokeMonitor(type, e, this.Id.Name, this.Id.Type, this.CurrentStateName);
@@ -930,7 +929,7 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// Reports the activity coverage of this actor.
         /// </summary>
-        internal virtual void ReportActivityCoverage(CoverageInfo coverageInfo)
+        internal virtual void ReportActivityCoverage(ActorCoverageInfo coverageInfo)
         {
             var name = this.GetType().FullName;
             if (coverageInfo.IsMachineDeclared(name))
@@ -944,7 +943,7 @@ namespace Microsoft.Coyote.Actors
             var registeredEvents = new HashSet<string>(from key in this.ActionMap.Keys select key.FullName);
             foreach (var eventId in registeredEvents)
             {
-                coverageInfo.DeclareStateEvent(name, fakeStateName, eventId);
+                coverageInfo.DeclareMachineStateEventPair(name, fakeStateName, eventId);
             }
         }
 

Source/Actors/Runtime/ActorExecutionContext.cs

@@ -15,6 +15,7 @@ using Microsoft.Coyote.Actors.Coverage;
 using Microsoft.Coyote.Actors.Mocks;
 using Microsoft.Coyote.Actors.Timers;
 using Microsoft.Coyote.Actors.Timers.Mocks;
+using Microsoft.Coyote.Coverage;
 using Microsoft.Coyote.Logging;
 using Microsoft.Coyote.Runtime;
 using Microsoft.Coyote.Specifications;
@@ -24,7 +25,7 @@ namespace Microsoft.Coyote.Actors
     /// <summary>
     /// The execution context of an actor program.
     /// </summary>
-    internal class ActorExecutionContext : IActorRuntime
+    internal class ActorExecutionContext : IActorRuntime, IRuntimeExtension
     {
         /// <summary>
         /// Object used to synchronize access to the runtime event handlers.
@@ -39,7 +40,7 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// The runtime associated with this context.
         /// </summary>
-        internal readonly CoyoteRuntime Runtime;
+        internal CoyoteRuntime Runtime { get; private set; }
 
         /// <summary>
         /// Map from unique actor ids to actors.
@@ -54,7 +55,7 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// Data structure containing information regarding testing coverage.
         /// </summary>
-        internal readonly CoverageInfo CoverageInfo;
+        internal readonly ActorCoverageInfo CoverageInfo;
 
         /// <summary>
         /// Responsible for writing to the installed <see cref="ILogger"/>.
@@ -127,19 +128,52 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// Initializes a new instance of the <see cref="ActorExecutionContext"/> class.
         /// </summary>
-        internal ActorExecutionContext(Configuration configuration, CoyoteRuntime runtime, ActorLogManager logManager)
+        internal ActorExecutionContext(Configuration configuration, ActorLogManager logManager)
         {
             this.Configuration = configuration;
-            this.Runtime = runtime;
             this.ActorMap = new ConcurrentDictionary<ActorId, Actor>();
             this.EnabledActors = new HashSet<ActorId>();
-            this.CoverageInfo = new CoverageInfo();
+            this.CoverageInfo = new ActorCoverageInfo();
             this.LogManager = logManager;
             this.QuiescenceCompletionSource = new TaskCompletionSource<bool>();
             this.IsActorQuiescenceAwaited = false;
             this.QuiescenceSyncObject = new object();
         }
 
+        /// <summary>
+        /// Installs the specified <see cref="CoyoteRuntime"/>. Only one runtime can be installed
+        /// at a time, and this method can only be called once.
+        /// </summary>
+        internal ActorExecutionContext WithRuntime(CoyoteRuntime runtime)
+        {
+            if (this.Runtime != null)
+            {
+                throw new InvalidOperationException("A runtime is already installed.");
+            }
+
+            this.Runtime = runtime;
+            return this;
+        }
+
+        /// <inheritdoc/>
+        bool IRuntimeExtension.RunTest(Delegate test, out Task task)
+        {
+            if (test is Action<IActorRuntime> actionWithRuntime)
+            {
+                actionWithRuntime(this);
+                task = Task.CompletedTask;
+                return true;
+            }
+            else if (test is Func<IActorRuntime, Task> functionWithRuntime)
+            {
+                task = functionWithRuntime(this);
+                return true;
+            }
+
+            task = Task.CompletedTask;
+            return false;
+        }
+
         /// <inheritdoc/>
         public ActorId CreateActorId(Type type, string name = null) => new ActorId(type, this.GetNextOperationId(), name, this);
 
@@ -656,11 +690,8 @@ namespace Microsoft.Coyote.Actors
             this.LogManager.LogExecuteAction(stateMachine.Id, stateMachine.CurrentStateName,
                 stateMachine.CurrentStateName, action.Name);
 
-        /// <summary>
-        /// Builds the coverage graph information, if any. This information is only available
-        /// when <see cref="Configuration.IsActivityCoverageReported"/> is enabled.
-        /// </summary>
-        internal CoverageInfo BuildCoverageInfo()
+        /// <inheritdoc/>
+        CoverageInfo IRuntimeExtension.BuildCoverageInfo()
         {
             var result = this.CoverageInfo;
             if (result != null)
@@ -675,19 +706,21 @@ namespace Microsoft.Coyote.Actors
                 var eventCoverage = this.LogManager.GetLogsOfType<ActorRuntimeLogEventCoverage>().FirstOrDefault();
                 if (eventCoverage != null)
                 {
-                    result.EventInfo = eventCoverage.EventCoverage;
+                    result.ActorEventInfo = eventCoverage.ActorEventCoverage;
+                    result.MonitorEventInfo = eventCoverage.MonitorEventCoverage;
                 }
             }
 
             return result;
         }
 
-        /// <summary>
-        /// Returns the DGML graph of the current execution, if there is any.
-        /// </summary>
-        internal Graph GetExecutionGraph()
+        /// <inheritdoc/>
+        CoverageInfo IRuntimeExtension.GetCoverageInfo() => this.CoverageInfo;
+
+        /// <inheritdoc/>
+        CoverageGraph IRuntimeExtension.GetCoverageGraph()
         {
-            Graph result = null;
+            CoverageGraph result = null;
             var builder = this.LogManager.GetLogsOfType<ActorRuntimeLogGraphBuilder>()
                 .FirstOrDefault(builder => !builder.CollapseInstances);
             if (builder != null)
@@ -710,14 +743,14 @@ namespace Microsoft.Coyote.Actors
             this.Runtime.RegisterMonitor<T>();
 
         /// <inheritdoc/>
-        public void Monitor<T>(Event e)
+        public void Monitor<T>(Monitor.Event e)
             where T : Monitor =>
             this.Runtime.Monitor<T>(e);
 
         /// <summary>
         /// Invokes the specified <see cref="Specifications.Monitor"/> with the specified <see cref="Event"/>.
         /// </summary>
-        internal void InvokeMonitor(Type type, Event e, string senderName, string senderType, string senderStateName) =>
+        internal void InvokeMonitor(Type type, Monitor.Event e, string senderName, string senderType, string senderStateName) =>
             this.Runtime.InvokeMonitor(type, e, senderName, senderType, senderStateName);
 
         /// <inheritdoc/>
@@ -779,10 +812,8 @@ namespace Microsoft.Coyote.Actors
         /// <inheritdoc/>
         public void RemoveLog(IRuntimeLog log) => this.LogManager.RemoveLog(log);
 
-        /// <summary>
-        /// Returns a task that completes once all actors reach quiescence.
-        /// </summary>
-        internal Task WaitUntilQuiescenceAsync()
+        /// <inheritdoc/>
+        Task IRuntimeExtension.WaitUntilQuiescenceAsync()
         {
             lock (this.QuiescenceSyncObject)
             {
@@ -849,8 +880,8 @@ namespace Microsoft.Coyote.Actors
             /// <summary>
             /// Initializes a new instance of the <see cref="Mock"/> class.
             /// </summary>
-            internal Mock(Configuration configuration, CoyoteRuntime runtime, ActorLogManager logManager)
-                : base(configuration, runtime, logManager)
+            internal Mock(Configuration configuration, ActorLogManager logManager)
+                : base(configuration, logManager)
             {
                 this.ActorIds = new ConcurrentDictionary<ActorId, byte>();
                 this.NameValueToActorId = new ConcurrentDictionary<string, ActorId>();

Source/Actors/Runtime/ActorOperation.cs

@@ -25,6 +25,15 @@ namespace Microsoft.Coyote.Actors
         }
 
         /// <inheritdoc/>
-        internal override int GetHashedState(SchedulingPolicy policy) => this.Actor.GetHashedState(policy);
+        internal override int GetHashedState(SchedulingPolicy policy)
+        {
+            unchecked
+            {
+                var hash = 19;
+                hash = (hash * 31) + this.Actor.GetHashedState(policy);
+                hash = (hash * 31) + base.GetHashedState(policy);
+                return hash;
+            }
+        }
     }
 }

Source/Actors/Runtime/RuntimeFactory.cs

@@ -35,13 +35,24 @@ namespace Microsoft.Coyote.Actors
             configuration ??= Configuration.Create();
             var logWriter = new LogWriter(configuration);
             var logManager = CreateLogManager(logWriter);
-            return Runtime.RuntimeProvider.CreateAndInstall(configuration, logWriter, logManager).DefaultActorExecutionContext;
+
+            var actorRuntime = new ActorExecutionContext(configuration, logManager);
+            var runtime = Runtime.RuntimeProvider.CreateAndInstall(configuration, logWriter, logManager, actorRuntime);
+            return actorRuntime.WithRuntime(runtime);
         }
 
+        /// <summary>
+        /// Creates a new actor runtime with the specified <see cref="Configuration"/> for the specified <see cref="SchedulingPolicy"/>.
+        /// </summary>
+        internal static ActorExecutionContext Create(Configuration configuration, ActorLogManager logManager, SchedulingPolicy schedulingPolicy) =>
+            schedulingPolicy is SchedulingPolicy.Interleaving ?
+                new ActorExecutionContext.Mock(configuration, logManager) :
+                new ActorExecutionContext(configuration, logManager);
+
         /// <summary>
         /// Creates a new runtime log manager that writes to the specified log writer.
         /// </summary>
-        internal static LogManager CreateLogManager(LogWriter logWriter)
+        internal static ActorLogManager CreateLogManager(LogWriter logWriter)
         {
             var logManager = new ActorLogManager();
             logManager.RegisterLog(new ActorRuntimeLogTextFormatter(), logWriter);

Source/Actors/Runtime/StateMachine.cs

@@ -990,7 +990,7 @@ namespace Microsoft.Coyote.Actors
         }
 
         /// <inheritdoc/>
-        internal override void ReportActivityCoverage(CoverageInfo coverageInfo)
+        internal override void ReportActivityCoverage(ActorCoverageInfo coverageInfo)
         {
             var name = this.GetType().FullName;
             if (coverageInfo.IsMachineDeclared(name))
@@ -1000,7 +1000,7 @@ namespace Microsoft.Coyote.Actors
 
             this.Assert(StateInstanceCache.ContainsKey(this.GetType()), "{0} has not populated its states yet.", this.Id);
 
-            // Fetch states.
+            // Fetch the machine states.
             var states = new HashSet<string>();
             foreach (var state in StateInstanceCache[this.GetType()])
             {
@@ -1012,7 +1012,7 @@ namespace Microsoft.Coyote.Actors
                 coverageInfo.DeclareMachineState(name, state);
             }
 
-            // Fetch registered events.
+            // Fetch the registered events.
             var pairs = new HashSet<Tuple<string, string>>();
             foreach (var state in StateInstanceCache[this.GetType()])
             {
@@ -1026,7 +1026,7 @@ namespace Microsoft.Coyote.Actors
 
             foreach (var tup in pairs)
             {
-                coverageInfo.DeclareStateEvent(name, tup.Item1, tup.Item2);
+                coverageInfo.DeclareMachineStateEventPair(name, tup.Item1, tup.Item2);
             }
         }
 

Source/Core/Actors/Coverage/ActivityCoverageReporter.cs

@@ -1,318 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System;
-using System.Collections.Generic;
-using System.IO;
-using System.Linq;
-
-namespace Microsoft.Coyote.Actors.Coverage
-{
-    /// <summary>
-    /// Reports actor activity coverage.
-    /// </summary>
-    internal class ActivityCoverageReporter
-    {
-        /// <summary>
-        /// Data structure containing information
-        /// regarding testing coverage.
-        /// </summary>
-        private readonly CoverageInfo CoverageInfo;
-
-        /// <summary>
-        /// Set of built in events which we hide in the coverage report.
-        /// </summary>
-        private readonly HashSet<string> BuiltInEvents = new HashSet<string>();
-
-        /// <summary>
-        /// Initializes a new instance of the <see cref="ActivityCoverageReporter"/> class.
-        /// </summary>
-        public ActivityCoverageReporter(CoverageInfo coverageInfo)
-        {
-            this.CoverageInfo = coverageInfo;
-            this.BuiltInEvents.Add(typeof(GotoStateEvent).FullName);
-            this.BuiltInEvents.Add(typeof(PushStateEvent).FullName);
-            this.BuiltInEvents.Add(typeof(DefaultEvent).FullName);
-        }
-
-        /// <summary>
-        /// Emits the visualization graph.
-        /// </summary>
-        public void EmitVisualizationGraph(string graphFile)
-        {
-            if (this.CoverageInfo.CoverageGraph != null)
-            {
-                this.CoverageInfo.CoverageGraph.SaveDgml(graphFile, true);
-            }
-        }
-
-        /// <summary>
-        /// Emits the code coverage report.
-        /// </summary>
-        public void EmitCoverageReport(string coverageFile)
-        {
-            using var writer = new StreamWriter(coverageFile);
-            this.WriteCoverageText(writer);
-        }
-
-        /// <summary>
-        /// Return all events represented by this link.
-        /// </summary>
-        private static IEnumerable<string> GetEventIds(GraphLink link)
-        {
-            if (link.AttributeLists != null)
-            {
-                // a collapsed edge graph
-                if (link.AttributeLists.TryGetValue("EventIds", out HashSet<string> idList))
-                {
-                    return idList;
-                }
-            }
-
-            // a fully expanded edge graph has individual links for each event.
-            if (link.Attributes.TryGetValue("EventId", out string eventId))
-            {
-                return new string[] { eventId };
-            }
-
-            return Array.Empty<string>();
-        }
-
-        /// <summary>
-        /// Writes the visualization text.
-        /// </summary>
-        internal void WriteCoverageText(TextWriter writer)
-        {
-            var machines = new List<string>(this.CoverageInfo.Machines);
-            machines.Sort(StringComparer.Ordinal);
-
-            var machineTypes = new Dictionary<string, string>();
-
-            bool hasExternalSource = false;
-            string externalSrcId = "ExternalCode";
-
-            // look for any external source links.
-            foreach (var link in this.CoverageInfo.CoverageGraph.Links)
-            {
-                string srcId = link.Source.Id;
-                if (srcId == externalSrcId && !hasExternalSource)
-                {
-                    machines.Add(srcId);
-                    hasExternalSource = true;
-                }
-            }
-
-            foreach (var node in this.CoverageInfo.CoverageGraph.Nodes)
-            {
-                string id = node.Id;
-                if (machines.Contains(id))
-                {
-                    machineTypes[id] = node.Category ?? "StateMachine";
-                }
-            }
-
-            // (machines + "." + states => registered events
-            var uncoveredEvents = new Dictionary<string, HashSet<string>>();
-            foreach (var item in this.CoverageInfo.RegisteredEvents)
-            {
-                uncoveredEvents[item.Key] = new HashSet<string>(item.Value);
-            }
-
-            int totalEvents = (from h in uncoveredEvents select h.Value.Count).Sum();
-
-            // Now use the graph to find incoming links to each state and remove those from the list of uncovered events.
-            this.RemoveCoveredEvents(uncoveredEvents);
-
-            int totalUncoveredEvents = (from h in uncoveredEvents select h.Value.Count).Sum();
-
-            string eventCoverage = totalEvents is 0 ? "100.0" : ((totalEvents - totalUncoveredEvents) * 100.0 / totalEvents).ToString("F1");
-
-            WriteHeader(writer, string.Format("Total event coverage: {0}%", eventCoverage));
-
-            // Per-machine data.
-            foreach (var machine in machines)
-            {
-                machineTypes.TryGetValue(machine, out string machineType);
-                WriteHeader(writer, string.Format("{0}: {1}", machineType, machine));
-
-                // find all possible events for this machine.
-                var uncoveredMachineEvents = new Dictionary<string, HashSet<string>>();
-                var allMachineEvents = new Dictionary<string, HashSet<string>>();
-
-                foreach (var item in this.CoverageInfo.RegisteredEvents)
-                {
-                    var id = GetMachineId(item.Key);
-                    if (id == machine)
-                    {
-                        uncoveredMachineEvents[item.Key] = new HashSet<string>(item.Value);
-                        allMachineEvents[item.Key] = new HashSet<string>(item.Value);
-                    }
-                }
-
-                // Now use the graph to find incoming links to each state in this machine and remove those from the list of uncovered events.
-                this.RemoveCoveredEvents(uncoveredMachineEvents);
-
-                int totalMachineEvents = (from h in allMachineEvents select h.Value.Count).Sum();
-                var totalUncoveredMachineEvents = (from h in uncoveredMachineEvents select h.Value.Count).Sum();
-
-                eventCoverage = totalMachineEvents is 0 ? "100.0" : ((totalMachineEvents - totalUncoveredMachineEvents) * 100.0 / totalMachineEvents).ToString("F1");
-                writer.WriteLine("Event coverage: {0}%", eventCoverage);
-
-                if (!this.CoverageInfo.MachinesToStates.ContainsKey(machine))
-                {
-                    this.CoverageInfo.MachinesToStates[machine] = new HashSet<string>(new string[] { "ExternalState" });
-                }
-
-                // Per-state data.
-                foreach (var state in this.CoverageInfo.MachinesToStates[machine])
-                {
-                    var key = machine + "." + state;
-                    int totalStateEvents = (from h in allMachineEvents where h.Key == key select h.Value.Count).Sum();
-                    int uncoveredStateEvents = (from h in uncoveredMachineEvents where h.Key == key select h.Value.Count).Sum();
-
-                    writer.WriteLine();
-                    writer.WriteLine("\tState: {0}{1}", state, totalStateEvents > 0 && totalStateEvents == uncoveredStateEvents ? " is uncovered" : string.Empty);
-                    if (totalStateEvents is 0)
-                    {
-                        writer.WriteLine("\t\tState has no expected events, so coverage is 100%");
-                    }
-                    else if (totalStateEvents != uncoveredStateEvents)
-                    {
-                        eventCoverage = totalStateEvents is 0 ? "100.0" : ((totalStateEvents - uncoveredStateEvents) * 100.0 / totalStateEvents).ToString("F1");
-                        writer.WriteLine("\t\tState event coverage: {0}%", eventCoverage);
-                    }
-
-                    // Now use the graph to find incoming links to each state in this machine
-                    HashSet<string> stateIncomingStates = new HashSet<string>();
-                    HashSet<string> stateOutgoingStates = new HashSet<string>();
-                    foreach (var link in this.CoverageInfo.CoverageGraph.Links)
-                    {
-                        if (link.Category != "Contains")
-                        {
-                            string srcId = link.Source.Id;
-                            string srcMachine = GetMachineId(srcId);
-                            string targetId = link.Target.Id;
-                            string targetMachine = GetMachineId(targetId);
-                            bool intraMachineTransition = targetMachine == machine && srcMachine == machine;
-                            if (intraMachineTransition)
-                            {
-                                foreach (string id in GetEventIds(link))
-                                {
-                                    if (targetId == key)
-                                    {
-                                        // we want to show incoming/outgoing states within the current machine only.
-                                        stateIncomingStates.Add(GetStateName(srcId));
-                                    }
-
-                                    if (srcId == key)
-                                    {
-                                        // we want to show incoming/outgoing states within the current machine only.
-                                        stateOutgoingStates.Add(GetStateName(targetId));
-                                    }
-                                }
-                            }
-                        }
-                    }
-
-                    HashSet<string> received = new HashSet<string>(this.CoverageInfo.EventInfo.GetEventsReceived(key));
-                    this.RemoveBuiltInEvents(received);
-
-                    if (received.Count > 0)
-                    {
-                        writer.WriteLine("\t\tEvents received: {0}", string.Join(", ", SortHashSet(received)));
-                    }
-
-                    HashSet<string> sent = new HashSet<string>(this.CoverageInfo.EventInfo.GetEventsSent(key));
-                    this.RemoveBuiltInEvents(sent);
-
-                    if (sent.Count > 0)
-                    {
-                        writer.WriteLine("\t\tEvents sent: {0}", string.Join(", ", SortHashSet(sent)));
-                    }
-
-                    var stateUncoveredEvents = (from h in uncoveredMachineEvents where h.Key == key select h.Value).FirstOrDefault();
-                    if (stateUncoveredEvents != null && stateUncoveredEvents.Count > 0)
-                    {
-                        writer.WriteLine("\t\tEvents not covered: {0}", string.Join(", ", SortHashSet(stateUncoveredEvents)));
-                    }
-
-                    if (stateIncomingStates.Count > 0)
-                    {
-                        writer.WriteLine("\t\tPrevious states: {0}", string.Join(", ", SortHashSet(stateIncomingStates)));
-                    }
-
-                    if (stateOutgoingStates.Count > 0)
-                    {
-                        writer.WriteLine("\t\tNext states: {0}", string.Join(", ", SortHashSet(stateOutgoingStates)));
-                    }
-                }
-
-                writer.WriteLine();
-            }
-        }
-
-        private void RemoveBuiltInEvents(HashSet<string> eventList)
-        {
-            foreach (var name in eventList.ToArray())
-            {
-                if (this.BuiltInEvents.Contains(name))
-                {
-                    eventList.Remove(name);
-                }
-            }
-        }
-
-        /// <summary>
-        /// Remove all events from expectedEvent that are found in the graph.
-        /// </summary>
-        /// <param name="expectedEvents">The list of all expected events organized by unique state Id.</param>
-        private void RemoveCoveredEvents(Dictionary<string, HashSet<string>> expectedEvents)
-        {
-            foreach (var pair in expectedEvents)
-            {
-                string stateId = pair.Key;
-                var eventSet = pair.Value;
-
-                foreach (var e in this.CoverageInfo.EventInfo.GetEventsReceived(stateId))
-                {
-                    eventSet.Remove(e);
-                }
-            }
-        }
-
-        private static List<string> SortHashSet(HashSet<string> items)
-        {
-            List<string> sorted = new List<string>(items);
-            sorted.Sort(StringComparer.Ordinal);
-            return sorted;
-        }
-
-        private static string GetStateName(string nodeId)
-        {
-            int i = nodeId.LastIndexOf(".");
-            if (i > 0)
-            {
-                return nodeId.Substring(i + 1);
-            }
-
-            return nodeId;
-        }
-
-        private static void WriteHeader(TextWriter writer, string header)
-        {
-            writer.WriteLine(header);
-            writer.WriteLine(new string('=', header.Length));
-        }
-
-        private static string GetMachineId(string nodeId)
-        {
-            int i = nodeId.LastIndexOf(".");
-            if (i > 0)
-            {
-                return nodeId.Substring(0, i);
-            }
-
-            return nodeId;
-        }
-    }
-}

Source/Core/Actors/Coverage/CoverageInfo.cs

@@ -1,183 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System.Collections.Generic;
-using System.IO;
-using System.Runtime.Serialization;
-using System.Xml;
-
-namespace Microsoft.Coyote.Actors.Coverage
-{
-    /// <summary>
-    /// Class for storing actor coverage-specific data across multiple testing iterations.
-    /// </summary>
-    [DataContract]
-    public class CoverageInfo
-    {
-        /// <summary>
-        /// Set of known machines.
-        /// </summary>
-        [DataMember]
-        public HashSet<string> Machines { get; private set; }
-
-        /// <summary>
-        /// Map from machines to set of all states states defined in that machine.
-        /// </summary>
-        [DataMember]
-        public Dictionary<string, HashSet<string>> MachinesToStates { get; private set; }
-
-        /// <summary>
-        /// Set of (machine + "." + state => registered events). So all events that can
-        /// get us into each state.
-        /// </summary>
-        [DataMember]
-        public Dictionary<string, HashSet<string>> RegisteredEvents { get; private set; }
-
-        /// <summary>
-        /// The coverage graph.
-        /// </summary>
-        [DataMember]
-        public Graph CoverageGraph { get; set; }
-
-        /// <summary>
-        /// Information about events sent and received.
-        /// </summary>
-        [DataMember]
-        public EventCoverage EventInfo { get; set; }
-
-        /// <summary>
-        /// Initializes a new instance of the <see cref="CoverageInfo"/> class.
-        /// </summary>
-        public CoverageInfo()
-        {
-            this.Machines = new HashSet<string>();
-            this.MachinesToStates = new Dictionary<string, HashSet<string>>();
-            this.RegisteredEvents = new Dictionary<string, HashSet<string>>();
-        }
-
-        /// <summary>
-        /// Checks if the machine type has already been registered for coverage.
-        /// </summary>
-        public bool IsMachineDeclared(string machineName) => this.MachinesToStates.ContainsKey(machineName);
-
-        /// <summary>
-        /// Declares a state.
-        /// </summary>
-        public void DeclareMachineState(string machine, string state) => this.AddState(machine, state);
-
-        /// <summary>
-        /// Declares a registered state, event pair.
-        /// </summary>
-        public void DeclareStateEvent(string machine, string state, string eventName)
-        {
-            this.AddState(machine, state);
-
-            string key = machine + "." + state;
-            this.InternalAddEvent(key, eventName);
-        }
-
-        private void InternalAddEvent(string key, string eventName)
-        {
-            if (!this.RegisteredEvents.ContainsKey(key))
-            {
-                this.RegisteredEvents.Add(key, new HashSet<string>());
-            }
-
-            this.RegisteredEvents[key].Add(eventName);
-        }
-
-        /// <summary>
-        /// Merges the information from the specified coverage info. This is not thread-safe.
-        /// </summary>
-        public void Merge(CoverageInfo coverageInfo)
-        {
-            foreach (var machine in coverageInfo.Machines)
-            {
-                this.Machines.Add(machine);
-            }
-
-            foreach (var machine in coverageInfo.MachinesToStates)
-            {
-                foreach (var state in machine.Value)
-                {
-                    this.DeclareMachineState(machine.Key, state);
-                }
-            }
-
-            foreach (var tup in coverageInfo.RegisteredEvents)
-            {
-                foreach (var e in tup.Value)
-                {
-                    this.InternalAddEvent(tup.Key, e);
-                }
-            }
-
-            if (this.CoverageGraph is null)
-            {
-                this.CoverageGraph = coverageInfo.CoverageGraph;
-            }
-            else if (coverageInfo.CoverageGraph != null && this.CoverageGraph != coverageInfo.CoverageGraph)
-            {
-                this.CoverageGraph.Merge(coverageInfo.CoverageGraph);
-            }
-
-            if (this.EventInfo is null)
-            {
-                this.EventInfo = coverageInfo.EventInfo;
-            }
-            else if (coverageInfo.EventInfo != null && this.EventInfo != coverageInfo.EventInfo)
-            {
-                this.EventInfo.Merge(coverageInfo.EventInfo);
-            }
-        }
-
-        /// <summary>
-        /// Adds a new state.
-        /// </summary>
-        private void AddState(string machineName, string stateName)
-        {
-            this.Machines.Add(machineName);
-
-            if (!this.MachinesToStates.ContainsKey(machineName))
-            {
-                this.MachinesToStates.Add(machineName, new HashSet<string>());
-            }
-
-            this.MachinesToStates[machineName].Add(stateName);
-        }
-
-        /// <summary>
-        /// Load the given Coverage info file.
-        /// </summary>
-        /// <param name="filename">Path to the file to load.</param>
-        /// <returns>The deserialized coverage info.</returns>
-        public static CoverageInfo Load(string filename)
-        {
-            using var fs = new FileStream(filename, FileMode.Open);
-            using var reader = XmlDictionaryReader.CreateTextReader(fs, new XmlDictionaryReaderQuotas());
-            DataContractSerializerSettings settings = new DataContractSerializerSettings
-            {
-                PreserveObjectReferences = true
-            };
-
-            var ser = new DataContractSerializer(typeof(CoverageInfo), settings);
-            return (CoverageInfo)ser.ReadObject(reader, true);
-        }
-
-        /// <summary>
-        /// Save the coverage info to the given XML file.
-        /// </summary>
-        /// <param name="serFilePath">The path to the file to create.</param>
-        public void Save(string serFilePath)
-        {
-            using var fs = new FileStream(serFilePath, FileMode.Create);
-            DataContractSerializerSettings settings = new DataContractSerializerSettings
-            {
-                PreserveObjectReferences = true
-            };
-
-            var ser = new DataContractSerializer(typeof(CoverageInfo), settings);
-            ser.WriteObject(fs, this);
-        }
-    }
-}

Source/Core/Core.csproj

@@ -3,7 +3,7 @@
     <Description>The Coyote core libraries and runtime.</Description>
     <AssemblyName>Microsoft.Coyote</AssemblyName>
     <RootNamespace>Microsoft.Coyote</RootNamespace>
-    <PackageTags>asynchronous;actors;state-machines;tasks;systematic-testing</PackageTags>
+    <PackageTags>systematic-testing;concurrency;tasks;dotnet;csharp</PackageTags>
     <OutputPath>..\..\bin\</OutputPath>
     <Framework462Supported>false</Framework462Supported>
   </PropertyGroup>

Source/Core/Coverage/ActivityCoverageReporter.cs

@@ -0,0 +1,294 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using SpecMonitor = Microsoft.Coyote.Specifications.Monitor;
+
+namespace Microsoft.Coyote.Coverage
+{
+    /// <summary>
+    /// Reports activity coverage.
+    /// </summary>
+    internal class ActivityCoverageReporter
+    {
+        /// <summary>
+        /// Data structure containing information regarding testing coverage.
+        /// </summary>
+        private readonly CoverageInfo CoverageInfo;
+
+        /// <summary>
+        /// Set of built in events which we hide in the coverage report.
+        /// </summary>
+        private readonly HashSet<string> BuiltInEvents = new HashSet<string>();
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="ActivityCoverageReporter"/> class.
+        /// </summary>
+        public ActivityCoverageReporter(CoverageInfo coverageInfo)
+        {
+            this.CoverageInfo = coverageInfo;
+            this.BuiltInEvents.Add(typeof(SpecMonitor.GotoStateEvent).FullName);
+            this.BuiltInEvents.Add(typeof(SpecMonitor.DefaultEvent).FullName);
+        }
+
+        /// <summary>
+        /// Emits the visualization graph.
+        /// </summary>
+        public void EmitVisualizationGraph(string graphFile) =>
+            this.CoverageInfo.CoverageGraph?.SaveDgml(graphFile, true);
+
+        /// <summary>
+        /// Emits the activity coverage report.
+        /// </summary>
+        public void EmitCoverageReport(string coverageFile)
+        {
+            using var writer = new StreamWriter(coverageFile);
+            this.WriteCoverageText(writer);
+        }
+
+        /// <summary>
+        /// Emits the activity coverage report.
+        /// </summary>
+        internal virtual void WriteCoverageText(TextWriter writer)
+        {
+            var monitors = new List<string>(this.CoverageInfo.Monitors);
+            monitors.Sort(StringComparer.Ordinal);
+
+            var monitorTypes = new Dictionary<string, string>();
+            foreach (var node in this.CoverageInfo.CoverageGraph.Nodes)
+            {
+                string id = node.Id;
+                if (monitors.Contains(id))
+                {
+                    monitorTypes[id] = node.Category ?? "Monitor";
+                }
+            }
+
+            // monitors + "." + states => registered monitor events
+            var uncoveredEvents = new Dictionary<string, HashSet<string>>();
+            foreach (var item in this.CoverageInfo.RegisteredMonitorEvents)
+            {
+                uncoveredEvents[item.Key] = new HashSet<string>(item.Value);
+            }
+
+            int totalEvents = (from h in uncoveredEvents select h.Value.Count).Sum();
+
+            // Now use the graph to find incoming links to each state and remove those from the list of uncovered monitor events.
+            this.RemoveCoveredEvents(uncoveredEvents);
+
+            int totalUncoveredEvents = (from h in uncoveredEvents select h.Value.Count).Sum();
+            string eventCoverage = totalEvents is 0 ? "100.0" : ((totalEvents - totalUncoveredEvents) * 100.0 / totalEvents).ToString("F1");
+
+            if (monitors.Count > 0)
+            {
+                WriteHeader(writer, string.Format("Total specification monitor coverage: {0}%", eventCoverage));
+                foreach (var monitor in monitors)
+                {
+                    monitorTypes.TryGetValue(monitor, out string monitorType);
+                    WriteHeader(writer, string.Format("{0}: {1}", monitorType, monitor));
+
+                    // Find all possible events for this specification monitor.
+                    var uncoveredMonitorEvents = new Dictionary<string, HashSet<string>>();
+                    var allMonitorEvents = new Dictionary<string, HashSet<string>>();
+                    foreach (var item in this.CoverageInfo.RegisteredMonitorEvents)
+                    {
+                        var id = GetMonitorId(item.Key);
+                        if (id == monitor)
+                        {
+                            uncoveredMonitorEvents[item.Key] = new HashSet<string>(item.Value);
+                            allMonitorEvents[item.Key] = new HashSet<string>(item.Value);
+                        }
+                    }
+
+                    // Now use the graph to find incoming links to each state in this specification monitor
+                    // and remove those from the list of uncovered events.
+                    this.RemoveCoveredEvents(uncoveredMonitorEvents);
+
+                    int totalMonitorEvents = (from h in allMonitorEvents select h.Value.Count).Sum();
+                    var totalUncoveredMonitorEvents = (from h in uncoveredMonitorEvents select h.Value.Count).Sum();
+
+                    eventCoverage = totalMonitorEvents is 0 ? "100.0" : ((totalMonitorEvents - totalUncoveredMonitorEvents) * 100.0 / totalMonitorEvents).ToString("F1");
+                    writer.WriteLine("Event coverage: {0}%", eventCoverage);
+
+                    foreach (var state in this.CoverageInfo.MonitorsToStates[monitor])
+                    {
+                        var key = monitor + "." + state;
+                        int totalStateEvents = (from h in allMonitorEvents where h.Key == key select h.Value.Count).Sum();
+                        int uncoveredStateEvents = (from h in uncoveredMonitorEvents where h.Key == key select h.Value.Count).Sum();
+
+                        writer.WriteLine();
+                        writer.WriteLine("\tState: {0}{1}", state, totalStateEvents > 0 && totalStateEvents == uncoveredStateEvents ? " is uncovered" : string.Empty);
+                        if (totalStateEvents is 0)
+                        {
+                            writer.WriteLine("\t\tState has no expected events, so coverage is 100%");
+                        }
+                        else if (totalStateEvents != uncoveredStateEvents)
+                        {
+                            eventCoverage = totalStateEvents is 0 ? "100.0" : ((totalStateEvents - uncoveredStateEvents) * 100.0 / totalStateEvents).ToString("F1");
+                            writer.WriteLine("\t\tState event coverage: {0}%", eventCoverage);
+                        }
+
+                        // Now use the graph to find incoming links to each state in this monitor.
+                        HashSet<string> stateIncomingStates = new HashSet<string>();
+                        HashSet<string> stateOutgoingStates = new HashSet<string>();
+                        foreach (var link in this.CoverageInfo.CoverageGraph.Links)
+                        {
+                            if (link.Category != "Contains")
+                            {
+                                string srcId = link.Source.Id;
+                                string srcMonitor = GetMonitorId(srcId);
+                                string targetId = link.Target.Id;
+                                string targetMonitor = GetMonitorId(targetId);
+                                bool intraMonitorTransition = targetMonitor == monitor && srcMonitor == monitor;
+                                if (intraMonitorTransition)
+                                {
+                                    foreach (string id in GetEventIds(link))
+                                    {
+                                        if (targetId == key)
+                                        {
+                                            // We want to show incoming/outgoing states within the current monitor only.
+                                            stateIncomingStates.Add(GetStateName(srcId));
+                                        }
+
+                                        if (srcId == key)
+                                        {
+                                            // We want to show incoming/outgoing states within the current monitor only.
+                                            stateOutgoingStates.Add(GetStateName(targetId));
+                                        }
+                                    }
+                                }
+                            }
+                        }
+
+                        HashSet<string> processed = new HashSet<string>(this.CoverageInfo.MonitorEventInfo.GetEventsProcessed(key));
+                        this.RemoveBuiltInEvents(processed);
+                        if (processed.Count > 0)
+                        {
+                            writer.WriteLine("\t\tEvents processed: {0}", string.Join(", ", SortHashSet(processed)));
+                        }
+
+                        HashSet<string> raised = new HashSet<string>(this.CoverageInfo.MonitorEventInfo.GetEventsRaised(key));
+                        this.RemoveBuiltInEvents(raised);
+                        if (raised.Count > 0)
+                        {
+                            writer.WriteLine("\t\tEvents raised: {0}", string.Join(", ", SortHashSet(raised)));
+                        }
+
+                        var stateUncoveredEvents = (from h in uncoveredMonitorEvents where h.Key == key select h.Value).FirstOrDefault();
+                        if (stateUncoveredEvents != null && stateUncoveredEvents.Count > 0)
+                        {
+                            writer.WriteLine("\t\tEvents not covered: {0}", string.Join(", ", SortHashSet(stateUncoveredEvents)));
+                        }
+
+                        if (stateIncomingStates.Count > 0)
+                        {
+                            writer.WriteLine("\t\tPrevious states: {0}", string.Join(", ", SortHashSet(stateIncomingStates)));
+                        }
+
+                        if (stateOutgoingStates.Count > 0)
+                        {
+                            writer.WriteLine("\t\tNext states: {0}", string.Join(", ", SortHashSet(stateOutgoingStates)));
+                        }
+                    }
+
+                    writer.WriteLine();
+                }
+            }
+            else
+            {
+                WriteHeader(writer, "Total specification monitor coverage: N/A");
+            }
+        }
+
+        private void RemoveBuiltInEvents(HashSet<string> eventList)
+        {
+            foreach (var name in eventList.ToArray())
+            {
+                if (this.BuiltInEvents.Contains(name))
+                {
+                    eventList.Remove(name);
+                }
+            }
+        }
+
+        /// <summary>
+        /// Remove all events from expectedEvent that are found in the graph.
+        /// </summary>
+        /// <param name="expectedEvents">The list of all expected events organized by unique state id.</param>
+        private void RemoveCoveredEvents(Dictionary<string, HashSet<string>> expectedEvents)
+        {
+            foreach (var pair in expectedEvents)
+            {
+                string stateId = pair.Key;
+                var eventSet = pair.Value;
+
+                foreach (var e in this.CoverageInfo.MonitorEventInfo.GetEventsProcessed(stateId))
+                {
+                    eventSet.Remove(e);
+                }
+            }
+        }
+
+        protected static List<string> SortHashSet(HashSet<string> items)
+        {
+            List<string> sorted = new List<string>(items);
+            sorted.Sort(StringComparer.Ordinal);
+            return sorted;
+        }
+
+        protected static string GetStateName(string nodeId)
+        {
+            int i = nodeId.LastIndexOf(".");
+            if (i > 0)
+            {
+                return nodeId.Substring(i + 1);
+            }
+
+            return nodeId;
+        }
+
+        /// <summary>
+        /// Return all events represented by this link.
+        /// </summary>
+        protected static IEnumerable<string> GetEventIds(CoverageGraph.Link link)
+        {
+            if (link.AttributeLists != null)
+            {
+                // A collapsed edge graph
+                if (link.AttributeLists.TryGetValue("EventIds", out HashSet<string> idList))
+                {
+                    return idList;
+                }
+            }
+
+            // A fully expanded edge graph has individual links for each event.
+            if (link.Attributes.TryGetValue("EventId", out string eventId))
+            {
+                return new string[] { eventId };
+            }
+
+            return Array.Empty<string>();
+        }
+
+        protected static void WriteHeader(TextWriter writer, string header)
+        {
+            writer.WriteLine(new string('=', header.Length));
+            writer.WriteLine(header);
+            writer.WriteLine(new string('=', header.Length));
+        }
+
+        private static string GetMonitorId(string nodeId)
+        {
+            int i = nodeId.LastIndexOf(".");
+            if (i > 0)
+            {
+                return nodeId.Substring(0, i);
+            }
+
+            return nodeId;
+        }
+    }
+}