diff --git a/Src/PChecker/CheckerCore/Actors/ActorId.cs b/Src/PChecker/CheckerCore/Actors/ActorId.cs index 5c48c481f..3c08aa10b 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorId.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorId.cs @@ -4,6 +4,7 @@ using System; using System.Globalization; using System.Runtime.Serialization; +using PChecker.SystematicTesting; namespace PChecker.Actors { @@ -62,7 +63,7 @@ public sealed class ActorId : IEquatable, IComparable /// /// Initializes a new instance of the class. /// - internal ActorId(Type type, string name, ActorRuntime runtime, bool useNameForHashing = false) + internal ActorId(Type type, string name, ControlledRuntime runtime, bool useNameForHashing = false) { Runtime = runtime; Endpoint = string.Empty; @@ -97,7 +98,7 @@ internal ActorId(Type type, string name, ActorRuntime runtime, bool useNameForHa /// /// Bind the actor id. /// - internal void Bind(ActorRuntime runtime) + internal void Bind(ControlledRuntime runtime) { Runtime = runtime; } diff --git a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs deleted file mode 100644 index 4743209b1..000000000 --- a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs +++ /dev/null @@ -1,652 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Collections.Concurrent; -using System.Collections.Generic; -using System.IO; -using System.Linq; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Threading.Tasks; -using PChecker.Actors.EventQueues; -using PChecker.Actors.Events; -using PChecker.Actors.Exceptions; -using PChecker.Actors.Logging; -using PChecker.Random; -using PChecker.Runtime; -using PChecker.Specifications.Monitors; -using EventInfo = PChecker.Actors.Events.EventInfo; - -namespace PChecker.Actors -{ - /// - /// Runtime for creating and executing actors. - /// - internal class ActorRuntime : CoyoteRuntime, IActorRuntime - { - /// - /// Map from unique actor ids to actors. - /// - private readonly ConcurrentDictionary ActorMap; - - /// - /// Responsible for writing to all registered objects. - /// - protected internal LogWriter LogWriter { get; private set; } - - /// - /// Used to log text messages. Use - /// to replace the logger with a custom one. - /// - public override TextWriter Logger => LogWriter.Logger; - - /// - /// Used to log json trace outputs. - /// - public JsonWriter JsonLogger => LogWriter.JsonLogger; - - /// - /// Callback that is fired when a Coyote event is dropped. - /// - public event OnEventDroppedHandler OnEventDropped; - - /// - /// Initializes a new instance of the class. - /// - internal ActorRuntime(CheckerConfiguration checkerConfiguration, IRandomValueGenerator valueGenerator) - : base(checkerConfiguration, valueGenerator) - { - ActorMap = new ConcurrentDictionary(); - LogWriter = new LogWriter(checkerConfiguration); - } - - /// - /// Creates a fresh actor id that has not yet been bound to any actor. - /// - public ActorId CreateActorId(Type type, string name = null) => new ActorId(type, name, this); - - /// - /// Creates an actor id that is uniquely tied to the specified unique name. The - /// returned actor id can either be a fresh id (not yet bound to any actor), or - /// it can be bound to a previously created actor. In the second case, this actor - /// id can be directly used to communicate with the corresponding actor. - /// - public virtual ActorId CreateActorIdFromName(Type type, string name) => new ActorId(type, name, this, true); - - /// - /// Creates a new actor of the specified and with the specified - /// optional . This event can only be used to access its payload, - /// and cannot be handled. - /// - public virtual ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) => - CreateActor(null, type, null, initialEvent, null, opGroupId); - - /// - /// Creates a new actor of the specified and name, and with the - /// specified optional . This event can only be used to access - /// its payload, and cannot be handled. - /// - public virtual ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => - CreateActor(null, type, name, initialEvent, null, opGroupId); - - /// - /// Creates a new actor of the specified type, using the specified . - /// This method optionally passes an to the new actor, which can only - /// be used to access its payload, and cannot be handled. - /// - public virtual ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Guid opGroupId = default) => - CreateActor(id, type, null, initialEvent, null, opGroupId); - - /// - /// Creates a new actor of the specified and with the specified - /// optional . This event can only be used to access its payload, - /// and cannot be handled. The method returns only when the actor is initialized and - /// the (if any) is handled. - /// - public virtual Task CreateActorAndExecuteAsync(Type type, Event initialEvent = null, Guid opGroupId = default) => - CreateActorAndExecuteAsync(null, type, null, initialEvent, null, opGroupId); - - /// - /// Creates a new actor of the specified and name, and with the - /// specified optional . This event can only be used to access - /// its payload, and cannot be handled. The method returns only when the actor is - /// initialized and the (if any) is handled. - /// - public virtual Task CreateActorAndExecuteAsync(Type type, string name, Event initialEvent = null, - Guid opGroupId = default) => - CreateActorAndExecuteAsync(null, type, name, initialEvent, null, opGroupId); - - /// - /// Creates a new actor of the specified , using the specified unbound - /// actor id, and passes the specified optional . This event can only - /// be used to access its payload, and cannot be handled. The method returns only when - /// the actor is initialized and the (if any) - /// is handled. - /// - public virtual Task CreateActorAndExecuteAsync(ActorId id, Type type, Event initialEvent = null, - Guid opGroupId = default) => - CreateActorAndExecuteAsync(id, type, null, initialEvent, null, opGroupId); - - /// - /// Sends an asynchronous to an actor. - /// - public virtual void SendEvent(ActorId targetId, Event initialEvent, Guid opGroupId = default) => - SendEvent(targetId, initialEvent, null, opGroupId); - - /// - /// Sends an to an actor. Returns immediately if the target was already - /// running. Otherwise blocks until the target handles the event and reaches quiescense. - /// - public virtual Task SendEventAndExecuteAsync(ActorId targetId, Event initialEvent, - Guid opGroupId = default) => - SendEventAndExecuteAsync(targetId, initialEvent, null, opGroupId); - - /// - /// Returns the operation group id of the actor with the specified id. Returns - /// if the id is not set, or if the is not associated with this runtime. During - /// testing, the runtime asserts that the specified actor is currently executing. - /// - public virtual Guid GetCurrentOperationGroupId(ActorId currentActorId) - { - var actor = GetActorWithId(currentActorId); - return actor is null ? Guid.Empty : actor.OperationGroupId; - } - - /// - /// Creates a new of the specified . - /// - internal virtual ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, - StateMachine creator, Guid opGroupId) - { - var actor = CreateActor(id, type, name, creator, opGroupId); - LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); - RunActorEventHandler(actor, initialEvent, true); - return actor.Id; - } - - /// - /// Creates a new of the specified . The method - /// returns only when the actor is initialized and the (if any) - /// is handled. - /// - internal virtual async Task CreateActorAndExecuteAsync(ActorId id, Type type, string name, - Event initialEvent, StateMachine creator, Guid opGroupId) - { - var actor = CreateActor(id, type, name, creator, opGroupId); - LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); - await RunActorEventHandlerAsync(actor, initialEvent, true); - return actor.Id; - } - - /// - /// Creates a new of the specified . - /// - private StateMachine CreateActor(ActorId id, Type type, string name, StateMachine creator, Guid opGroupId) - { - throw new NotImplementedException(); - } - - /// - /// Sends an asynchronous to an actor. - /// - internal virtual void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) - { - var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); - if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning) - { - RunActorEventHandler(target, null, false); - } - } - - /// - /// Sends an asynchronous to an actor. Returns immediately if the target was - /// already running. Otherwise blocks until the target handles the event and reaches quiescense. - /// - internal virtual async Task SendEventAndExecuteAsync(ActorId targetId, Event e, StateMachine sender, - Guid opGroupId) - { - var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); - if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning) - { - await RunActorEventHandlerAsync(target, null, false); - return true; - } - - return enqueueStatus is EnqueueStatus.Dropped; - } - - /// - /// Enqueues an event to the actor with the specified id. - /// - private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId, out StateMachine target) - { - if (e is null) - { - var message = sender != null ? - string.Format("{0} is sending a null event.", sender.Id.ToString()) : - "Cannot send a null event."; - Assert(false, message); - } - - if (targetId is null) - { - var message = (sender != null) ? $"{sender.Id.ToString()} is sending event {e.ToString()} to a null actor." - : $"Cannot send event {e.ToString()} to a null actor."; - - Assert(false, message); - } - - // The operation group id of this operation is set using the following precedence: - // (1) To the specified send operation group id, if it is non-empty. - // (2) To the operation group id of the sender actor, if it exists and is non-empty. - // (3) To the empty operation group id. - if (opGroupId == Guid.Empty && sender != null) - { - opGroupId = sender.OperationGroupId; - } - - target = GetActorWithId(targetId); - if (target is null || target.IsHalted) - { - LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type, - sender?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true); - TryHandleDroppedEvent(e, targetId); - return EnqueueStatus.Dropped; - } - - LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type, - sender?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: false); - - var enqueueStatus = target.Enqueue(e, opGroupId, null); - if (enqueueStatus == EnqueueStatus.Dropped) - { - TryHandleDroppedEvent(e, targetId); - } - - return enqueueStatus; - } - - /// - /// Runs a new asynchronous actor event handler. - /// This is a fire and forget invocation. - /// - private void RunActorEventHandler(StateMachine actor, Event initialEvent, bool isFresh) - { - Task.Run(async () => - { - try - { - if (isFresh) - { - await actor.InitializeAsync(initialEvent); - } - - await actor.RunEventHandlerAsync(); - } - catch (Exception ex) - { - IsRunning = false; - RaiseOnFailureEvent(ex); - } - finally - { - if (actor.IsHalted) - { - ActorMap.TryRemove(actor.Id, out var _); - } - } - }); - } - - /// - /// Runs a new asynchronous actor event handler. - /// - private async Task RunActorEventHandlerAsync(StateMachine actor, Event initialEvent, bool isFresh) - { - try - { - if (isFresh) - { - await actor.InitializeAsync(initialEvent); - } - - await actor.RunEventHandlerAsync(); - } - catch (Exception ex) - { - IsRunning = false; - RaiseOnFailureEvent(ex); - return; - } - } - - /// - internal override void TryCreateMonitor(Type type) - { - lock (Monitors) - { - if (Monitors.Any(m => m.GetType() == type)) - { - // Idempotence: only one monitor per type can exist. - return; - } - } - - Assert(type.IsSubclassOf(typeof(Monitor)), "Type '{0}' is not a subclass of Monitor.", type.FullName); - - var monitor = (Monitor)Activator.CreateInstance(type); - monitor.Initialize(this); - monitor.InitializeStateInformation(); - - lock (Monitors) - { - Monitors.Add(monitor); - } - - LogWriter.LogCreateMonitor(type.FullName); - - monitor.GotoStartState(); - } - - /// - internal override bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType) - { - var result = (ValueGenerator.Next(maxValue) == 0); - - LogWriter.LogRandom(result, callerName, callerType); - return result; - } - - /// - internal override int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType) - { - var result = ValueGenerator.Next(maxValue); - LogWriter.LogRandom(result, callerName, callerType); - return result; - } - - /// - /// Gets the actor of type with the specified id, - /// or null if no such actor exists. - /// - private TActor GetActorWithId(ActorId id) - where TActor : StateMachine => - id != null && ActorMap.TryGetValue(id, out var value) && - value is TActor actor ? actor : null; - - /// - /// Notifies that an actor invoked an action. - /// - internal virtual void NotifyInvokedAction(StateMachine actor, MethodInfo action, string handlingStateName, - string currentStateName, Event receivedEvent) - { - if (CheckerConfiguration.IsVerbose) - { - LogWriter.LogExecuteAction(actor.Id, handlingStateName, currentStateName, action.Name); - } - } - - /// - /// Notifies that an actor dequeued an . - /// - internal virtual void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventInfo) - { - if (CheckerConfiguration.IsVerbose) - { - var stateName = actor.CurrentStateName; - LogWriter.LogDequeueEvent(actor.Id, stateName, e); - } - } - - /// - /// Notifies that an actor dequeued the default . - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyDefaultEventDequeued(StateMachine actor) - { - } - - /// - /// Notifies that the inbox of the specified actor is about to be - /// checked to see if the default event handler should fire. - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyDefaultEventHandlerCheck(StateMachine actor) - { - } - - /// - /// Notifies that an actor raised an . - /// - internal virtual void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo) - { - if (CheckerConfiguration.IsVerbose) - { - var stateName = actor.CurrentStateName; - LogWriter.LogRaiseEvent(actor.Id, stateName, e); - } - } - - /// - /// Notifies that an actor is handling a raised . - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyHandleRaisedEvent(StateMachine actor, Event e) - { - } - - /// - /// Notifies that an actor called - /// or one of its overloaded methods. - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyReceiveCalled(StateMachine actor) - { - } - - /// - /// Notifies that an actor enqueued an event that it was waiting to receive. - /// - internal virtual void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo) - { - if (CheckerConfiguration.IsVerbose) - { - var stateName = actor.CurrentStateName; - LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true); - } - } - - /// - /// Notifies that an actor received an event without waiting because the event - /// was already in the inbox when the actor invoked the receive statement. - /// - internal virtual void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo) - { - if (CheckerConfiguration.IsVerbose) - { - var stateName = actor.CurrentStateName; - LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false); - } - } - - /// - /// Notifies that an actor is waiting for the specified task to complete. - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyWaitTask(StateMachine actor, Task task) - { - } - - /// - /// Notifies that an actor is waiting to receive an event of one of the specified types. - /// - internal virtual void NotifyWaitEvent(StateMachine actor, IEnumerable eventTypes) - { - if (CheckerConfiguration.IsVerbose) - { - var stateName = actor.CurrentStateName; - var eventWaitTypesArray = eventTypes.ToArray(); - if (eventWaitTypesArray.Length == 1) - { - LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray[0]); - } - else - { - LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray); - } - } - } - - /// - /// Notifies that a state machine entered a state. - /// - internal virtual void NotifyEnteredState(StateMachine stateMachine) - { - if (CheckerConfiguration.IsVerbose) - { - LogWriter.LogStateTransition(stateMachine.Id, stateMachine.CurrentStateName, isEntry: true); - } - } - - /// - /// Notifies that a state machine exited a state. - /// - internal virtual void NotifyExitedState(StateMachine stateMachine) - { - if (CheckerConfiguration.IsVerbose) - { - LogWriter.LogStateTransition(stateMachine.Id, stateMachine.CurrentStateName, isEntry: false); - } - } - - /// - /// Notifies that a state machine invoked pop. - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyPopState(StateMachine stateMachine) - { - } - - /// - /// Notifies that a state machine invoked an action. - /// - internal virtual void NotifyInvokedOnEntryAction(StateMachine stateMachine, MethodInfo action, Event receivedEvent) - { - if (CheckerConfiguration.IsVerbose) - { - LogWriter.LogExecuteAction(stateMachine.Id, stateMachine.CurrentStateName, - stateMachine.CurrentStateName, action.Name); - } - } - - /// - /// Notifies that a state machine invoked an action. - /// - internal virtual void NotifyInvokedOnExitAction(StateMachine stateMachine, MethodInfo action, Event receivedEvent) - { - if (CheckerConfiguration.IsVerbose) - { - LogWriter.LogExecuteAction(stateMachine.Id, stateMachine.CurrentStateName, - stateMachine.CurrentStateName, action.Name); - } - } - - /// - /// Notifies that a monitor entered a state. - /// - internal virtual void NotifyEnteredState(Monitor monitor) - { - if (CheckerConfiguration.IsVerbose) - { - var monitorState = monitor.CurrentStateNameWithTemperature; - LogWriter.LogMonitorStateTransition(monitor.GetType().FullName, monitorState, - true, monitor.GetHotState()); - } - } - - /// - /// Notifies that a monitor exited a state. - /// - internal virtual void NotifyExitedState(Monitor monitor) - { - if (CheckerConfiguration.IsVerbose) - { - var monitorState = monitor.CurrentStateNameWithTemperature; - LogWriter.LogMonitorStateTransition(monitor.GetType().FullName, monitorState, - false, monitor.GetHotState()); - } - } - - /// - /// Notifies that a monitor invoked an action. - /// - internal virtual void NotifyInvokedAction(Monitor monitor, MethodInfo action, string stateName, Event receivedEvent) - { - if (CheckerConfiguration.IsVerbose) - { - LogWriter.LogMonitorExecuteAction(monitor.GetType().FullName, action.Name, stateName); - } - } - - /// - /// Notifies that a monitor raised an . - /// - internal virtual void NotifyRaisedEvent(Monitor monitor, Event e) - { - if (CheckerConfiguration.IsVerbose) - { - var monitorState = monitor.CurrentStateNameWithTemperature; - LogWriter.LogMonitorRaiseEvent(monitor.GetType().FullName, monitorState, e); - } - } - - /// - /// Notifies that a monitor found an error. - /// - internal void NotifyMonitorError(Monitor monitor) - { - if (CheckerConfiguration.IsVerbose) - { - var monitorState = monitor.CurrentStateNameWithTemperature; - LogWriter.LogMonitorError(monitor.GetType().FullName, monitorState, monitor.GetHotState()); - } - } - - /// - /// Tries to handle the specified dropped . - /// - internal void TryHandleDroppedEvent(Event e, ActorId id) => OnEventDropped?.Invoke(e, id); - - /// - public override TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger); - - /// - /// Sets the JsonLogger in LogWriter.cs - /// - /// jsonLogger instance - public void SetJsonLogger(JsonWriter jsonLogger) => LogWriter.SetJsonLogger(jsonLogger); - - /// - /// Use this method to register an . - /// - public void RegisterLog(IActorRuntimeLog log) => LogWriter.RegisterLog(log); - - /// - /// Use this method to unregister a previously registered . - /// - public void RemoveLog(IActorRuntimeLog log) => LogWriter.RemoveLog(log); - - /// - protected override void Dispose(bool disposing) - { - if (disposing) - { - Monitors.Clear(); - ActorMap.Clear(); - } - - base.Dispose(disposing); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs index 44a72365d..d315d1cd7 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs @@ -557,7 +557,7 @@ public JsonWriter() /// /// Enum representing the different log types the JSON error trace logs. - /// Referenced from PLogFormatter.cs and ActorRuntimeLogTextFormatter.cs + /// Referenced from PLogFormatter.cs and PCheckerLogTextFormatter.cs /// to see what those formatter logs. Check IActorRuntimeLog.cs to see /// each log types' description and when they are invoked. /// diff --git a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs index aad60d8aa..c991b1378 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs @@ -549,7 +549,7 @@ internal TextWriter SetLogger(TextWriter logger) { Logger = TextWriter.Null; - var textLog = GetLogsOfType().FirstOrDefault(); + var textLog = GetLogsOfType().FirstOrDefault(); if (textLog != null) { textLog.Logger = Logger; @@ -573,9 +573,9 @@ internal TextWriter SetLogger(TextWriter logger) /// The jsonLogger instance created from runtime before running tests. internal void SetJsonLogger(JsonWriter jsonLogger) => JsonLogger = jsonLogger; - private ActorRuntimeLogTextFormatter GetOrCreateTextLog() + private PCheckerLogTextFormatter GetOrCreateTextLog() { - var textLog = GetLogsOfType().FirstOrDefault(); + var textLog = GetLogsOfType().FirstOrDefault(); if (textLog == null) { if (Logger == null) @@ -583,7 +583,7 @@ private ActorRuntimeLogTextFormatter GetOrCreateTextLog() Logger = new ConsoleLogger(); } - textLog = new ActorRuntimeLogTextFormatter + textLog = new PCheckerLogTextFormatter { Logger = Logger }; @@ -605,9 +605,9 @@ internal void RegisterLog(IActorRuntimeLog log) } // Make sure we only have one text logger - if (log is ActorRuntimeLogTextFormatter a) + if (log is PCheckerLogTextFormatter a) { - var textLog = GetLogsOfType().FirstOrDefault(); + var textLog = GetLogsOfType().FirstOrDefault(); if (textLog != null) { Logs.Remove(textLog); @@ -619,9 +619,9 @@ internal void RegisterLog(IActorRuntimeLog log) } } - // If log is or of subclass ActorRuntimeLogJsonFormatter (i.e. when log is PJsonFormatter), + // If log is or of subclass PCheckerLogJsonFormatter (i.e. when log is PJsonFormatter), // update the Writer reference to the JsonLogger instance defined within LogWriter.cs - if (log is ActorRuntimeLogJsonFormatter tempJsonFormatter) + if (log is PCheckerLogJsonFormatter tempJsonFormatter) { tempJsonFormatter.Writer = JsonLogger; } diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogJsonFormatter.cs similarity index 95% rename from Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs rename to Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogJsonFormatter.cs index e1718377d..a76928a44 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogJsonFormatter.cs @@ -9,7 +9,7 @@ namespace PChecker.Actors.Logging /// /// This class implements IActorRuntimeLog and generates log output in an XML format. /// - public class ActorRuntimeLogJsonFormatter : IActorRuntimeLog + public class PCheckerLogJsonFormatter : IActorRuntimeLog { /// /// Get or set the JsonWriter to write to. @@ -17,9 +17,9 @@ public class ActorRuntimeLogJsonFormatter : IActorRuntimeLog public JsonWriter Writer { get; set; } /// - /// Initializes a new instance of the class. + /// Initializes a new instance of the class. /// - protected ActorRuntimeLogJsonFormatter() + protected PCheckerLogJsonFormatter() { Writer = new JsonWriter(); } diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogTextFormatter.cs similarity index 98% rename from Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs rename to Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogTextFormatter.cs index 86859be23..17a01458c 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogTextFormatter.cs @@ -12,7 +12,7 @@ namespace PChecker.Actors.Logging /// /// This class implements IActorRuntimeLog and generates output in a a human readable text format. /// - public class ActorRuntimeLogTextFormatter : IActorRuntimeLog + public class PCheckerLogTextFormatter : IActorRuntimeLog { /// /// Get or set the TextWriter to write to. @@ -20,9 +20,9 @@ public class ActorRuntimeLogTextFormatter : IActorRuntimeLog public TextWriter Logger { get; set; } /// - /// Initializes a new instance of the class. + /// Initializes a new instance of the class. /// - public ActorRuntimeLogTextFormatter() + public PCheckerLogTextFormatter() { Logger = new ConsoleLogger(); } diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogXmlFormatter.cs similarity index 99% rename from Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs rename to Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogXmlFormatter.cs index ebc7fb18d..87954b2ae 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogXmlFormatter.cs @@ -12,12 +12,12 @@ namespace PChecker.Actors.Logging /// /// This class implements IActorRuntimeLog and generates log output in an XML format. /// - internal class ActorRuntimeLogXmlFormatter : IActorRuntimeLog + internal class PCheckerLogXmlFormatter : IActorRuntimeLog { private readonly XmlWriter Writer; private bool Closed; - public ActorRuntimeLogXmlFormatter(XmlWriter writer) + public PCheckerLogXmlFormatter(XmlWriter writer) { Writer = writer; Writer.WriteStartElement("Log"); diff --git a/Src/PChecker/CheckerCore/Actors/StateMachine.cs b/Src/PChecker/CheckerCore/Actors/StateMachine.cs index 25d79b62b..2c2affef3 100644 --- a/Src/PChecker/CheckerCore/Actors/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Actors/StateMachine.cs @@ -20,6 +20,7 @@ using PChecker.Actors.StateTransitions; using PChecker.Exceptions; using PChecker.IO.Debugging; +using PChecker.SystematicTesting; using EventInfo = PChecker.Actors.Events.EventInfo; @@ -34,7 +35,7 @@ public abstract class StateMachine /// /// The runtime that executes this state machine. /// - internal ActorRuntime Runtime { get; private set; } + internal ControlledRuntime Runtime { get; private set; } /// /// Unique id that identifies this state machine. @@ -155,7 +156,7 @@ protected StateMachine() /// /// Configures the state machine. /// - internal void Configure(ActorRuntime runtime, ActorId id, IStateMachineManager manager, IEventQueue inbox) + internal void Configure(ControlledRuntime runtime, ActorId id, IStateMachineManager manager, IEventQueue inbox) { Runtime = runtime; Id = id; diff --git a/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs index f654ff132..1ab95ee70 100644 --- a/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs @@ -14,7 +14,7 @@ namespace PChecker.PRuntime /// /// This class implements IActorRuntimeLog and generates log output in an XML format. /// - public class PJsonFormatter : ActorRuntimeLogJsonFormatter + public class PJsonFormatter : PCheckerLogJsonFormatter { /// diff --git a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs index 51d4ceb61..151ef1c1d 100644 --- a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs @@ -10,7 +10,7 @@ namespace PChecker.PRuntime /// /// Formatter for the runtime log. /// - public class PLogFormatter : ActorRuntimeLogTextFormatter + public class PLogFormatter : PCheckerLogTextFormatter { public PLogFormatter() : base() { diff --git a/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs b/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs index 55091af17..07c60cda0 100644 --- a/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs +++ b/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs @@ -3,6 +3,8 @@ using PChecker.Actors; using PChecker.Random; +using PChecker.SystematicTesting; +using PChecker.SystematicTesting.Strategies.Probabilistic; namespace PChecker.Runtime { @@ -66,7 +68,7 @@ private static CoyoteRuntime CreateWithConfiguration(CheckerConfiguration checke } var valueGenerator = new RandomValueGenerator(checkerConfiguration); - return new ActorRuntime(checkerConfiguration, valueGenerator); + return new ControlledRuntime(checkerConfiguration, valueGenerator); } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/Specifications/Monitor.cs index acf62c8dc..5674815c7 100644 --- a/Src/PChecker/CheckerCore/Specifications/Monitor.cs +++ b/Src/PChecker/CheckerCore/Specifications/Monitor.cs @@ -16,6 +16,7 @@ using PChecker.Actors.Logging; using PChecker.Actors.StateTransitions; using PChecker.Exceptions; +using PChecker.SystematicTesting; namespace PChecker.Specifications.Monitors { @@ -61,7 +62,7 @@ public abstract class Monitor /// /// The runtime that executes this monitor. /// - private ActorRuntime Runtime; + private ControlledRuntime Runtime; /// /// The active monitor state. @@ -172,7 +173,7 @@ protected Monitor() /// Initializes this monitor. /// /// The runtime that executes this monitor. - internal void Initialize(ActorRuntime runtime) + internal void Initialize(ControlledRuntime runtime) { Runtime = runtime; } diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index cf181d38c..c9b3911bf 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -6,7 +6,9 @@ using System.Collections.Generic; using System.Diagnostics; using System.Globalization; +using System.IO; using System.Linq; +using System.Linq.Expressions; using System.Reflection; using System.Threading.Tasks; using PChecker.Actors; @@ -14,6 +16,7 @@ using PChecker.Actors.EventQueues.Mocks; using PChecker.Actors.Events; using PChecker.Actors.Exceptions; +using PChecker.Actors.Logging; using PChecker.Actors.Managers; using PChecker.Actors.Managers.Mocks; using PChecker.Coverage; @@ -33,8 +36,9 @@ namespace PChecker.SystematicTesting /// /// Runtime for controlling asynchronous operations. /// - internal sealed class ControlledRuntime : ActorRuntime + internal sealed class ControlledRuntime : CoyoteRuntime, IActorRuntime { + /// /// The currently executing runtime. /// @@ -64,6 +68,38 @@ internal sealed class ControlledRuntime : ActorRuntime /// The root task id. /// internal readonly int? RootTaskId; + + /// + /// Cache storing state machine constructors. + /// + private static readonly Dictionary> StateMachineConstructorCache = + new Dictionary>(); + + /// + /// Map from unique actor ids to state machines. + /// + private readonly ConcurrentDictionary StateMachineMap; + + /// + /// Callback that is fired when a Coyote event is dropped. + /// + public event OnEventDroppedHandler OnEventDropped; + + /// + /// Responsible for writing to all registered objects. + /// + protected internal LogWriter LogWriter { get; private set; } + + /// + /// Used to log text messages. Use + /// to replace the logger with a custom one. + /// + public override TextWriter Logger => LogWriter.Logger; + + /// + /// Used to log json trace outputs. + /// + public JsonWriter JsonLogger => LogWriter.JsonLogger; /// @@ -129,6 +165,9 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration, ISchedulin IRandomValueGenerator valueGenerator) : base(checkerConfiguration, valueGenerator) { + StateMachineMap = new ConcurrentDictionary(); + LogWriter = new LogWriter(checkerConfiguration); + IsExecutionControlled = true; RootTaskId = Task.CurrentId; @@ -149,9 +188,41 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration, ISchedulin // allowing future retrieval in the same asynchronous call stack. AssignAsyncControlFlowRuntime(this); } + + /// + /// Initializes a new instance of the class. + /// + internal ControlledRuntime(CheckerConfiguration checkerConfiguration, + IRandomValueGenerator valueGenerator) + : base(checkerConfiguration, valueGenerator) + { + StateMachineMap = new ConcurrentDictionary(); + LogWriter = new LogWriter(checkerConfiguration); + + IsExecutionControlled = true; + + RootTaskId = Task.CurrentId; + NameValueToActorId = new ConcurrentDictionary(); + + CoverageInfo = new CoverageInfo(); + + // Update the current asynchronous control flow with this runtime instance, + // allowing future retrieval in the same asynchronous call stack. + AssignAsyncControlFlowRuntime(this); + } + + /// + /// Creates a fresh state machine id that has not yet been bound to any state machine. + /// + public ActorId CreateActorId(Type type, string name = null) => new ActorId(type, name, this); - /// - public override ActorId CreateActorIdFromName(Type type, string name) + /// + /// Creates an actor id that is uniquely tied to the specified unique name. The + /// returned actor id can either be a fresh id (not yet bound to any state machine), or + /// it can be bound to a previously created state machine. In the second case, this actor + /// id can be directly used to communicate with the corresponding actor. + /// + public ActorId CreateActorIdFromName(Type type, string name) { // It is important that all actor ids use the monotonically incrementing // value as the id during testing, and not the unique name. @@ -159,52 +230,89 @@ public override ActorId CreateActorIdFromName(Type type, string name) return NameValueToActorId.GetOrAdd(name, id); } - /// - public override ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) => + /// + /// Creates a new state machine of the specified and with the specified + /// optional . This event can only be used to access its payload, + /// and cannot be handled. + /// + public ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) => CreateActor(null, type, null, initialEvent, opGroupId); - /// - public override ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => + /// + /// Creates a new state machine of the specified and name, and with the + /// specified optional . This event can only be used to access + /// its payload, and cannot be handled. + /// + public ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => CreateActor(null, type, name, initialEvent, opGroupId); - /// - public override ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Guid opGroupId = default) + /// + /// Creates a new state machine of the specified type, using the specified . + /// This method optionally passes an to the new state machine, which can only + /// be used to access its payload, and cannot be handled. + /// + public ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Guid opGroupId = default) { Assert(id != null, "Cannot create an actor using a null actor id."); return CreateActor(id, type, null, initialEvent, opGroupId); } - /// - public override Task CreateActorAndExecuteAsync(Type type, Event e = null, Guid opGroupId = default) => + /// + /// Creates a new state machine of the specified and with the specified + /// optional . This event can only be used to access its payload, + /// and cannot be handled. The method returns only when the state machine is initialized and + /// the (if any) is handled. + /// + public Task CreateActorAndExecuteAsync(Type type, Event e = null, Guid opGroupId = default) => CreateActorAndExecuteAsync(null, type, null, e, opGroupId); - /// - public override Task CreateActorAndExecuteAsync(Type type, string name, Event e = null, Guid opGroupId = default) => + /// + /// Creates a new state machine of the specified and name, and with the + /// specified optional . This event can only be used to access + /// its payload, and cannot be handled. The method returns only when the state machine is + /// initialized and the (if any) is handled. + /// + public Task CreateActorAndExecuteAsync(Type type, string name, Event e = null, Guid opGroupId = default) => CreateActorAndExecuteAsync(null, type, name, e, opGroupId); - /// - public override Task CreateActorAndExecuteAsync(ActorId id, Type type, Event e = null, Guid opGroupId = default) + /// + /// Creates a new state machine of the specified , using the specified unbound + /// state machine id, and passes the specified optional . This event can only + /// be used to access its payload, and cannot be handled. The method returns only when + /// the state machine is initialized and the (if any) + /// is handled. + /// + public Task CreateActorAndExecuteAsync(ActorId id, Type type, Event e = null, Guid opGroupId = default) { Assert(id != null, "Cannot create an actor using a null actor id."); return CreateActorAndExecuteAsync(id, type, null, e, opGroupId); } - /// - public override void SendEvent(ActorId targetId, Event e, Guid opGroupId = default) + /// + /// Sends an asynchronous to a state machine. + /// + public void SendEvent(ActorId targetId, Event e, Guid opGroupId = default) { var senderOp = Scheduler.GetExecutingOperation(); SendEvent(targetId, e, senderOp?.Actor, opGroupId); } - /// - public override Task SendEventAndExecuteAsync(ActorId targetId, Event e, Guid opGroupId = default) + /// + /// Sends an to a state machine. Returns immediately if the target was already + /// running. Otherwise, blocks until the target handles the event and reaches quiescence. + /// + public Task SendEventAndExecuteAsync(ActorId targetId, Event e, Guid opGroupId = default) { var senderOp = Scheduler.GetExecutingOperation(); return SendEventAndExecuteAsync(targetId, e, senderOp?.Actor, opGroupId); } - /// - public override Guid GetCurrentOperationGroupId(ActorId currentActorId) + /// + /// Returns the operation group id of the state machine with the specified id. Returns + /// if the id is not set, or if the is not associated with this runtime. During + /// testing, the runtime asserts that the specified state machine is currently executing. + /// + public Guid GetCurrentOperationGroupId(ActorId currentActorId) { var callerOp = Scheduler.GetExecutingOperation(); Assert(callerOp != null && currentActorId == callerOp.Actor.Id, @@ -288,13 +396,16 @@ internal ActorId CreateActor(ActorId id, Type type, string name, Event initialEv return CreateActor(id, type, name, initialEvent, creatorOp?.Actor, opGroupId); } - /// - internal override ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, StateMachine creator, + /// + /// Creates a new of the specified . + /// + internal ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, StateMachine creator, Guid opGroupId) { AssertExpectedCallerActor(creator, "CreateActor"); var actor = CreateActor(id, type, name, creator, opGroupId); + LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); RunActorEventHandler(actor, initialEvent, true, null); return actor.Id; } @@ -312,8 +423,12 @@ internal Task CreateActorAndExecuteAsync(ActorId id, Type type, string return CreateActorAndExecuteAsync(id, type, name, initialEvent, creatorOp?.Actor, opGroupId); } - /// - internal override async Task CreateActorAndExecuteAsync(ActorId id, Type type, string name, + /// + /// Creates a new of the specified . The method + /// returns only when the state machine is initialized and the (if any) + /// is handled. + /// + internal async Task CreateActorAndExecuteAsync(ActorId id, Type type, string name, Event initialEvent, StateMachine creator, Guid opGroupId) { AssertExpectedCallerActor(creator, "CreateActorAndExecuteAsync"); @@ -329,7 +444,7 @@ internal override async Task CreateActorAndExecuteAsync(ActorId id, Typ } /// - /// Creates a new actor of the specified . + /// Creates a new state machine of the specified . /// private StateMachine CreateActor(ActorId id, Type type, string name, StateMachine creator, Guid opGroupId) { @@ -361,7 +476,7 @@ private StateMachine CreateActor(ActorId id, Type type, string name, StateMachin opGroupId = creator.OperationGroupId; } - var actor = StateMachineFactory.Create(type); + var actor = Create(type); IStateMachineManager stateMachineManager = new StateMachineManager(this, actor, opGroupId); IEventQueue eventQueue = new EventQueue(stateMachineManager, actor); @@ -379,9 +494,38 @@ private StateMachine CreateActor(ActorId id, Type type, string name, StateMachin return actor; } + + /// + /// Creates a new instance of the specified type. + /// + /// The type of the state machines. + /// The created state machine instance. + public static StateMachine Create(Type type) + { + Func constructor = null; + lock (StateMachineConstructorCache) + { + if (!StateMachineConstructorCache.TryGetValue(type, out constructor)) + { + var constructorInfo = type.GetConstructor(Type.EmptyTypes); + if (constructorInfo == null) + { + throw new Exception("Could not find empty constructor for type " + type.FullName); + } - /// - internal override void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) + constructor = Expression.Lambda>( + Expression.New(constructorInfo)).Compile(); + StateMachineConstructorCache.Add(type, constructor); + } + } + + return constructor(); + } + + /// + /// Sends an asynchronous to a state machine. + /// + internal void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) { if (e is null) { @@ -409,8 +553,11 @@ internal override void SendEvent(ActorId targetId, Event e, StateMachine sender, } } - /// - internal override async Task SendEventAndExecuteAsync(ActorId targetId, Event e, StateMachine sender, + /// + /// Sends an asynchronous to a state machine. Returns immediately if the target was + /// already running. Otherwise, blocks until the target handles the event and reaches quiescence. + /// + internal async Task SendEventAndExecuteAsync(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) { Assert(e != null, "{0} is sending a null event.", sender.Id); @@ -765,6 +912,15 @@ internal override int GetNondeterministicIntegerChoice(int maxValue, string call LogWriter.LogRandom(choice, callerName ?? caller?.Id.Name, callerType ?? caller?.Id.Type); return choice; } + + /// + /// Gets the actor of type with the specified id, + /// or null if no such actor exists. + /// + private TActor GetActorWithId(ActorId id) + where TActor : StateMachine => + id != null && StateMachineMap.TryGetValue(id, out var value) && + value is TActor actor ? actor : null; /// /// Gets the that is executing on the current @@ -798,15 +954,19 @@ internal void ScheduleNextOperation(AsyncOperationType type) } } - /// - internal override void NotifyInvokedAction(StateMachine actor, MethodInfo action, string handlingStateName, + /// + /// Notifies that a state machine invoked an action. + /// + internal void NotifyInvokedAction(StateMachine actor, MethodInfo action, string handlingStateName, string currentStateName, Event receivedEvent) { LogWriter.LogExecuteAction(actor.Id, handlingStateName, currentStateName, action.Name); } - /// - internal override void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventInfo) + /// + /// Notifies that a state machine dequeued an . + /// + internal void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventInfo) { var op = Scheduler.GetOperationWithId(actor.Id.Value); @@ -826,41 +986,55 @@ internal override void NotifyDequeuedEvent(StateMachine actor, Event e, EventInf LogWriter.LogDequeueEvent(actor.Id, stateName, e); } - /// - internal override void NotifyDefaultEventDequeued(StateMachine actor) + /// + /// Notifies that a state machine dequeued the default . + /// + internal void NotifyDefaultEventDequeued(StateMachine actor) { Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive); ResetProgramCounter(actor); } - /// - internal override void NotifyDefaultEventHandlerCheck(StateMachine actor) + /// + /// Notifies that the inbox of the specified state machine is about to be + /// checked to see if the default event handler should fire. + /// + internal void NotifyDefaultEventHandlerCheck(StateMachine actor) { Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Default); } - /// - internal override void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo) + /// + /// Notifies that a state machine raised an . + /// + internal void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo) { var stateName = actor.CurrentStateName; LogWriter.LogRaiseEvent(actor.Id, stateName, e); } - /// - internal override void NotifyHandleRaisedEvent(StateMachine actor, Event e) + /// + /// Notifies that a state machine is handling a raised . + /// + internal void NotifyHandleRaisedEvent(StateMachine actor, Event e) { var stateName = actor.CurrentStateName; LogWriter.LogHandleRaisedEvent(actor.Id, stateName, e); } - /// - internal override void NotifyReceiveCalled(StateMachine actor) + /// + /// Notifies that a state machine called + /// or one of its overloaded methods. + /// + internal void NotifyReceiveCalled(StateMachine actor) { AssertExpectedCallerActor(actor, "ReceiveEventAsync"); } - /// - internal override void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo) + /// + /// Notifies that a state machine enqueued an event that it was waiting to receive. + /// + internal void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo) { var stateName = actor.CurrentStateName; LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true); @@ -868,8 +1042,11 @@ internal override void NotifyReceivedEvent(StateMachine actor, Event e, EventInf op.OnReceivedEvent(); } - /// - internal override void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo) + /// + /// Notifies that a state machine received an event without waiting because the event + /// was already in the inbox when the state machine invoked the receiving statement. + /// + internal void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo) { var stateName = actor.CurrentStateName; LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false); @@ -877,8 +1054,10 @@ internal override void NotifyReceivedEventWithoutWaiting(StateMachine actor, Eve ResetProgramCounter(actor); } - /// - internal override void NotifyWaitTask(StateMachine actor, Task task) + /// + /// Notifies that a state machine is waiting for the specified task to complete. + /// + internal void NotifyWaitTask(StateMachine actor, Task task) { Assert(task != null, "{0} is waiting for a null task to complete.", actor.Id); @@ -894,8 +1073,10 @@ internal override void NotifyWaitTask(StateMachine actor, Task task) } } - /// - internal override void NotifyWaitEvent(StateMachine actor, IEnumerable eventTypes) + /// + /// Notifies that a state machine is waiting to receive an event of one of the specified types. + /// + internal void NotifyWaitEvent(StateMachine actor, IEnumerable eventTypes) { var stateName = actor.CurrentStateName; var op = Scheduler.GetOperationWithId(actor.Id.Value); @@ -915,59 +1096,111 @@ internal override void NotifyWaitEvent(StateMachine actor, IEnumerable eve ResetProgramCounter(actor); } - /// - internal override void NotifyEnteredState(StateMachine stateMachine) + /// + /// Notifies that a state machine entered a state. + /// + internal void NotifyEnteredState(StateMachine stateMachine) { var stateName = stateMachine.CurrentStateName; LogWriter.LogStateTransition(stateMachine.Id, stateName, isEntry: true); } - /// - internal override void NotifyExitedState(StateMachine stateMachine) + /// + /// Notifies that a state machine exited a state. + /// + internal void NotifyExitedState(StateMachine stateMachine) { LogWriter.LogStateTransition(stateMachine.Id, stateMachine.CurrentStateName, isEntry: false); } - /// - internal override void NotifyInvokedOnEntryAction(StateMachine stateMachine, MethodInfo action, Event receivedEvent) + /// + /// Notifies that a state machine invoked an action. + /// + internal void NotifyInvokedOnEntryAction(StateMachine stateMachine, MethodInfo action, Event receivedEvent) { var stateName = stateMachine.CurrentStateName; LogWriter.LogExecuteAction(stateMachine.Id, stateName, stateName, action.Name); } - /// - internal override void NotifyInvokedOnExitAction(StateMachine stateMachine, MethodInfo action, Event receivedEvent) + /// + /// Notifies that a state machine invoked an action. + /// + internal void NotifyInvokedOnExitAction(StateMachine stateMachine, MethodInfo action, Event receivedEvent) { var stateName = stateMachine.CurrentStateName; LogWriter.LogExecuteAction(stateMachine.Id, stateName, stateName, action.Name); } - /// - internal override void NotifyEnteredState(Monitor monitor) + /// + /// Notifies that a monitor entered a state. + /// + internal void NotifyEnteredState(Monitor monitor) { var monitorState = monitor.CurrentStateName; LogWriter.LogMonitorStateTransition(monitor.GetType().FullName, monitorState, true, monitor.GetHotState()); } - /// - internal override void NotifyExitedState(Monitor monitor) + /// + /// Notifies that a monitor exited a state. + /// + internal void NotifyExitedState(Monitor monitor) { LogWriter.LogMonitorStateTransition(monitor.GetType().FullName, monitor.CurrentStateName, false, monitor.GetHotState()); } - /// - internal override void NotifyInvokedAction(Monitor monitor, MethodInfo action, string stateName, Event receivedEvent) + /// + /// Notifies that a monitor invoked an action. + /// + internal void NotifyInvokedAction(Monitor monitor, MethodInfo action, string stateName, Event receivedEvent) { LogWriter.LogMonitorExecuteAction(monitor.GetType().FullName, stateName, action.Name); } - /// - internal override void NotifyRaisedEvent(Monitor monitor, Event e) + /// + /// Notifies that a monitor raised an . + /// + internal void NotifyRaisedEvent(Monitor monitor, Event e) { var monitorState = monitor.CurrentStateName; LogWriter.LogMonitorRaiseEvent(monitor.GetType().FullName, monitorState, e); } + + /// + /// Notifies that a monitor found an error. + /// + internal void NotifyMonitorError(Monitor monitor) + { + if (CheckerConfiguration.IsVerbose) + { + var monitorState = monitor.CurrentStateNameWithTemperature; + LogWriter.LogMonitorError(monitor.GetType().FullName, monitorState, monitor.GetHotState()); + } + } + + /// + /// Tries to handle the specified dropped . + /// + internal void TryHandleDroppedEvent(Event e, ActorId id) => OnEventDropped?.Invoke(e, id); + + /// + public override TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger); + + /// + /// Sets the JsonLogger in LogWriter.cs + /// + /// jsonLogger instance + public void SetJsonLogger(JsonWriter jsonLogger) => LogWriter.SetJsonLogger(jsonLogger); + + /// + /// Use this method to register an . + /// + public void RegisterLog(IActorRuntimeLog log) => LogWriter.RegisterLog(log); + + /// + /// Use this method to unregister a previously registered . + /// + public void RemoveLog(IActorRuntimeLog log) => LogWriter.RemoveLog(log); /// /// Get the coverage graph information (if any). This information is only available @@ -1132,6 +1365,7 @@ protected override void Dispose(bool disposing) if (disposing) { Monitors.Clear(); + StateMachineMap.Clear(); } base.Dispose(disposing); diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index b753ad029..84463cc24 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -805,7 +805,7 @@ private void InitializeCustomLogging(ControlledRuntime runtime) if (_checkerConfiguration.IsXmlLogEnabled) { XmlLog = new StringBuilder(); - runtime.RegisterLog(new ActorRuntimeLogXmlFormatter(XmlWriter.Create(XmlLog, + runtime.RegisterLog(new PCheckerLogXmlFormatter(XmlWriter.Create(XmlLog, new XmlWriterSettings() { Indent = true, IndentChars = " ", OmitXmlDeclaration = true }))); } }