Merge pull request #229 from p-org/LoggingAPI

Logging improvements

Author: pdeligia

Samples/PingPong/PingPong.CustomLogging/Test.cs

@@ -6,14 +6,14 @@ namespace PingPong.CustomLogging
 {
     /// <summary>
     /// A simple PingPong application written using the P# high-level syntax.
-    /// 
+    ///
     /// The P# runtime starts by creating the P# machine 'NetworkEnvironment'. The
     /// 'NetworkEnvironment' machine then creates a 'Server' and a 'Client' machine,
     /// which then communicate by sending 'Ping' and 'Pong' events to each other for
     /// a limited amount of turns.
-    /// 
+    ///
     /// This sample shows how to install a custom logger during testing.
-    /// 
+    ///
     /// Note: this is an abstract implementation aimed primarily to showcase the testing
     /// capabilities of P#.
     /// </summary>
@@ -60,13 +60,13 @@ public static void Execute(PSharpRuntime runtime)
     /// <summary>
     /// Custom logger that just dumps to console.
     /// </summary>
-    class MyLogger : ILogger
+    class MyLogger : StateMachineLogger
     {
         /// <summary>
         /// Writes the specified string value.
         /// </summary>
         /// <param name="value">Text</param>
-        public void Write(string value)
+        public override void Write(string value)
         {
             Console.Write(value);
         }
@@ -76,7 +76,7 @@ public void Write(string value)
         /// </summary>
         /// <param name="format">Text</param>
         /// <param name="args">Arguments</param>
-        public void Write(string format, params object[] args)
+        public override void Write(string format, params object[] args)
         {
             Console.Write($"MyLogger: {format}", args);
         }
@@ -86,7 +86,7 @@ public void Write(string format, params object[] args)
         /// current line terminator.
         /// </summary>
         /// <param name="value">Text</param>
-        public void WriteLine(string value)
+        public override void WriteLine(string value)
         {
             Console.WriteLine($"MyLogger: {value}");
         }
@@ -97,14 +97,14 @@ public void WriteLine(string value)
         /// </summary>
         /// <param name="format">Text</param>
         /// <param name="args">Arguments</param>
-        public void WriteLine(string format, params object[] args)
+        public override void WriteLine(string format, params object[] args)
         {
             Console.WriteLine($"MyLogger: {format}", args);
         }
 
         /// <summary>
         /// Disposes the logger.
         /// </summary>
-        public void Dispose() { }
+        public override void Dispose() { }
     }
 }

Source/Core/IO/Logging/ConsoleLogger.cs

@@ -19,13 +19,13 @@ namespace Microsoft.PSharp.IO
     /// <summary>
     /// Logger that writes text to the console.
     /// </summary>
-    internal sealed class ConsoleLogger : ILogger
+    internal sealed class ConsoleLogger : StateMachineLogger
     {
         /// <summary>
         /// Writes the specified string value.
         /// </summary>
         /// <param name="value">Text</param>
-        public void Write(string value)
+        public override void Write(string value)
         {
             Console.Write(value);
         }
@@ -35,7 +35,7 @@ public void Write(string value)
         /// </summary>
         /// <param name="format">Text</param>
         /// <param name="args">Arguments</param>
-        public void Write(string format, params object[] args)
+        public override void Write(string format, params object[] args)
         {
             Console.Write(format, args);
         }
@@ -45,7 +45,7 @@ public void Write(string format, params object[] args)
         /// current line terminator.
         /// </summary>
         /// <param name="value">Text</param>
-        public void WriteLine(string value)
+        public override void WriteLine(string value)
         {
             Console.WriteLine(value);
         }
@@ -56,14 +56,14 @@ public void WriteLine(string value)
         /// </summary>
         /// <param name="format">Text</param>
         /// <param name="args">Arguments</param>
-        public void WriteLine(string format, params object[] args)
+        public override void WriteLine(string format, params object[] args)
         {
             Console.WriteLine(format, args);
         }
 
         /// <summary>
         /// Disposes the logger.
         /// </summary>
-        public void Dispose() { }
+        public override void Dispose() { }
     }
 }

Source/Core/IO/Logging/DisposingLogger.cs

@@ -12,13 +12,26 @@
 // </copyright>
 //-----------------------------------------------------------------------
 
+using Microsoft.PSharp.Utilities;
+using System;
+
 namespace Microsoft.PSharp.IO
 {
     /// <summary>
     /// Logger that disposes all written text.
     /// </summary>
     internal sealed class DisposingLogger : ILogger
     {
+        /// <summary>
+        /// The configuration that sets the logging verbosity.
+        /// </summary>
+        public Configuration Configuration { get; set; }
+
+        /// <summary>
+        /// The minimum logging verbosity level (should be >= 0, use 0 to log all messages).
+        /// </summary>
+        public int LoggingVerbosity { get; set; }
+
         /// <summary>
         /// Writes the specified string value.
         /// </summary>
@@ -47,6 +60,179 @@ public void WriteLine(string value) { }
         /// <param name="args">Arguments</param>
         public void WriteLine(string format, params object[] args) { }
 
+        /// <summary>
+        /// Called when an event is about to be enqueued to a machine.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that the event is being enqueued to.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
+        /// <param name="eventName">Name of the event.</param>
+        public void OnEnqueue(MachineId machineId, string currentStateName, string eventName) { }
+
+        /// <summary>
+        /// Called when an event is dequeued by a machine.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that the event is being dequeued by.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
+        /// <param name="eventName">Name of the event.</param>
+        public void OnDequeue(MachineId machineId, string currentStateName, string eventName) { }
+
+        /// <summary>
+        /// Called when the default event handler for a state is about to be executed.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that the state will execute in.</param>
+        /// <param name="currentStateName">Name of the current state of the machine.</param>
+        public void OnDefault(MachineId machineId, string currentStateName) { }
+
+        /// <summary>
+        /// Called when a machine is being pushed to a state.
+        /// </summary>
+        /// <param name="machineId">Id of the machine being pushed to the state.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
+        /// <param name="newStateName">The state the machine is pushed to.</param>
+        public void OnPush(MachineId machineId, string currentStateName, string newStateName) { }
+
+        /// <summary>
+        /// Called when a machine has been popped from a state.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that the pop executed in.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
+        /// <param name="restoredStateName">The name of the state being restored, if any.</param>
+        public void OnPop(MachineId machineId, string currentStateName, string restoredStateName) { }
+
+        /// <summary>
+        /// When an event cannot be handled in the current state, its exit handler is executed and then the state is 
+        /// popped and any previous "current state" is reentered. This handler is called when that pop has been done.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that the pop executed in.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/> (which is being re-entered), if any.</param>
+        /// <param name="eventName">The name of the event that cannot be handled.</param>
+        public void OnPopUnhandledEvent(MachineId machineId, string currentStateName, string eventName) { }
+
+        /// <summary>
+        /// Called when an event is received by a machine.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that received the event.</param>
+        /// <param name="eventName">The name of the event.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
+        /// <param name="wasBlocked">The machine was waiting for one or more specific events, and <paramref name="eventName"/> was one of them.</param>
+        public void OnReceive(MachineId machineId, string currentStateName, string eventName, bool wasBlocked) { }
+
+        /// <summary>
+        /// Called when a machine enters a wait state.
+        /// </summary>
+        /// <param name="machineId">Id of the machine that is entering the wait state.</param>
+        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
+        /// <param name="eventNames">The names of the specific events being waited for, if any.</param>
+        public void OnWait(MachineId machineId, string currentStateName, string eventNames) { }
+
+        /// <summary>
+        /// Called when an event is sent to a target machine.
+        /// </summary>
+        /// <param name="targetMachineId">Id of the target machine.</param>
+        /// <param name="targetStateName">The name of the current state of the target machine.</param>
+        /// <param name="senderId">The machine that sent the event, if any.</param>
+        /// <param name="senderStateName">The name of the current state of the sender machine, if applicable
+        ///     (if it is a non-Machine specialization of an AbstractMachine, it is not applicable).</param>
+        /// <param name="eventName">The event being sent.</param>
+        /// <param name="operationGroupId">The operation group id, if any.</param>
+        /// <param name="isTargetHalted">Is the target machine halted.</param>
+        public void OnSend(MachineId targetMachineId, string targetStateName, MachineId senderId, string senderStateName,
+            string eventName, Guid? operationGroupId, bool isTargetHalted) { }
+
+        /// <summary>
+        /// Called when a machine has been created.
+        /// </summary>
+        /// <param name="machineId">The id of the machine that has been created.</param>
+        public void OnCreateMachine(MachineId machineId) { }
+
+        /// <summary>
+        /// Called when a monitor has been created.
+        /// </summary>
+        /// <param name="monitorTypeName">The name of the type of the monitor that has been created.</param>
+        /// <param name="monitorId">The id of the monitor that has been created.</param>
+        public void OnCreateMonitor(string monitorTypeName, MachineId monitorId) { }
+
+        /// <summary>
+        /// Called when a machine has been halted.
+        /// </summary>
+        /// <param name="machineId">The id of the machine that has been halted.</param>
+        public void OnHalt(MachineId machineId) { }
+
+        /// <summary>
+        /// Called when a random result has been obtained.
+        /// </summary>
+        /// <param name="machineId">The id of the source machine, if any; otherwise, the runtime itself was the source.</param>
+        /// <param name="result">The random result (may be bool or int).</param>
+        public void OnRandom(MachineId machineId, object result) { }
+
+        /// <summary>
+        /// Called when a machine enters or exits a state.
+        /// </summary>
+        /// <param name="machineId">The id of the machine entering or exiting the state.</param>
+        /// <param name="stateName">The name of the state being entered or exited.</param>
+        /// <param name="isEntry">If true, this is called for a state entry; otherwise, exit.</param>
+        public void OnMachineState(MachineId machineId, string stateName, bool isEntry) { }
+
+        /// <summary>
+        /// Called when a machine raises an event.
+        /// </summary>
+        /// <param name="machineId">The id of the machine raising the event.</param>
+        /// <param name="currentStateName">The name of the current state of the machine raising the event.</param>
+        /// <param name="eventName">The name of the event being raised.</param>
+        public void OnMachineEvent(MachineId machineId, string currentStateName, string eventName) { }
+
+        /// <summary>
+        /// Called when a machine executes an action.
+        /// </summary>
+        /// <param name="machineId">The id of the machine executing the action.</param>
+        /// <param name="currentStateName">The name of the state in which the action is being executed.</param>
+        /// <param name="actionName">The name of the action being executed.</param>
+        public void OnMachineAction(MachineId machineId, string currentStateName, string actionName) { }
+
+        /// <summary>
+        /// Called when a monitor enters or exits a state.
+        /// </summary>
+        /// <param name="monitorTypeName">The name of the monitor entering or exiting the state.</param>
+        /// <param name="monitorId">The id of the monitor entering or exiting the state.</param>
+        /// <param name="stateName">The name of the state being entered or exited; if <paramref name="isInHotState"/>
+        ///     is not null, then the temperature is appended to the statename in brackets, e.g. "stateName[hot]".</param>
+        /// <param name="isEntry">If true, this is called for a state entry; otherwise, exit.</param>
+        /// <param name="isInHotState">If true, the monitor is in a hot state; if false, the monitor is in a cold state;
+        ///     else no liveness state is available.</param>
+        public void OnMonitorState(string monitorTypeName, MachineId monitorId, string stateName, bool isEntry, bool? isInHotState) { }
+
+        /// <summary>
+        /// Called when a monitor is about to process or has raised an event.
+        /// </summary>
+        /// <param name="monitorTypeName">Name of type of the monitor that will process or has raised the event.</param>
+        /// <param name="monitorId">Id of the monitor that will process or has raised the event.</param>
+        /// <param name="currentStateName">The name of the state in which the event is being raised.</param>
+        /// <param name="eventName">The name of the event.</param>
+        /// <param name="isProcessing">If true, the monitor is processing the event; otherwise it has raised it.</param>
+        public void OnMonitorEvent(string monitorTypeName, MachineId monitorId, string currentStateName, string eventName, bool isProcessing) { }
+
+        /// <summary>
+        /// Called when a monitor executes an action.
+        /// </summary>
+        /// <param name="monitorTypeName">Name of type of the monitor that is executing the action.</param>
+        /// <param name="monitorId">Name of type of the monitor that is executing the action.</param>
+        /// <param name="currentStateName">The name of the state in which the action is being executed.</param>
+        /// <param name="actionName">The name of the action being executed.</param>
+        public void OnMonitorAction(string monitorTypeName, MachineId monitorId, string currentStateName, string actionName) { }
+
+        /// <summary>
+        /// Called for general error reporting via pre-constructed text.
+        /// </summary>
+        /// <param name="text">The text of the error report.</param>
+        public void OnError(string text) { }
+
+        /// <summary>
+        /// Called for errors detected by a specific scheduling strategy.
+        /// </summary>
+        /// <param name="strategy">The scheduling strategy that was used.</param>
+        /// <param name="strategyDescription">More information about the scheduling strategy.</param>
+        public void OnStrategyError(SchedulingStrategy strategy, string strategyDescription) { }
+
         /// <summary>
         /// Disposes the logger.
         /// </summary>