moved actors to dedicated nuget package (microsoft#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,15 +96,15 @@ 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.
 - Improvements to how thread interrupts are handled at the end of each test iteration.
 - 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.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 @@
 
 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 @@ protected override Task OnInitializeAsync(Event initialEvent)
             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 @@ private void OnWaterHeaterButton(Event e)
 
             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 @@ private void OnPumpWater(Event e)
 
             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 @@ private void OnGrinderButtonChanged()
         {
             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 @@ private void OnDumpGrindsButton(Event e)
             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 @@ public static class Program
 
         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 @@ private static void OnRuntimeFailure(Exception ex)
         [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 @@ public ConfigEvent(bool runSlowly)
     /// </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 @@ internal class RegisterClientEvent : Event
     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 @@ internal class ReadWaterLevelEvent : Event { }
     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 @@ internal class ReadHopperLevelEvent : Event { }
     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 @@ internal class ReadWaterTemperatureEvent : Event { }
     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 @@ internal class ReadPortaFilterCoffeeLevelEvent : Event { }
     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 @@ internal class ReadDoorOpenEvent : Event { }
     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 @@ internal class WaterHeaterButtonEvent : Event
     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 @@ internal class PumpWaterEvent : Event
     {
         // 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; }
     }
 }