From ddeb890cbbf4315a1482dfb719e53ff6768961a7 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Wed, 21 Aug 2024 15:16:33 -0700 Subject: [PATCH] [Cleanup] Moving PJsonFormatter to PCheckerLogJsonFormatter and moving PLogFormatter to PCheckerLogTextFormatter --- .../CheckerCore/PRuntime/PJsonFormatter.cs | 519 ------------------ .../CheckerCore/PRuntime/PLogFormatter.cs | 215 -------- .../StateMachines/Logging/LogWriter.cs | 3 +- .../Logging/PCheckerLogJsonFormatter.cs | 462 ++++++++++++++-- .../Logging/PCheckerLogTextFormatter.cs | 349 ++++++------ .../CheckerCore/Testing/TestingProcess.cs | 7 + .../Backend/CSharp/CSharpCodeGenerator.cs | 2 - 7 files changed, 612 insertions(+), 945 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs delete mode 100644 Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs diff --git a/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs deleted file mode 100644 index 250d43cf0c..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs +++ /dev/null @@ -1,519 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Linq; -using System.Threading.Tasks; -using PChecker.StateMachines; -using PChecker.StateMachines.Events; -using PChecker.StateMachines.Logging; -using PChecker.PRuntime.Exceptions; - -namespace PChecker.PRuntime -{ - /// - /// This class implements IStateMachineRuntimeLog and generates log output in an XML format. - /// - public class PJsonFormatter : PCheckerLogJsonFormatter - { - - /// - /// Removes the '<' and '>' tags for a log text. - /// - /// The text log - /// New string with the tag removed or just the string itself if there is no tag. - private static string RemoveLogTag(string log) - { - var openingTagIndex = log.IndexOf("<", StringComparison.Ordinal); - var closingTagIndex = log.IndexOf(">", StringComparison.Ordinal); - var potentialTagExists = openingTagIndex != -1 && closingTagIndex != -1; - var validOpeningTag = openingTagIndex == 0 && closingTagIndex > openingTagIndex; - - if (potentialTagExists && validOpeningTag) - { - return log[(closingTagIndex + 1)..].Trim(); - } - - return log; - } - - /// - /// Method taken from PLogFormatter.cs file. Takes in a string and only get the - /// last element of the string separated by a period. - /// I.e. - /// Input: PImplementation.TestWithSingleClient(2) - /// Output: TestWithSingleClient(2) - /// - /// String representing the name to be parsed. - /// The split string. - private static string GetShortName(string name) => name?.Split('.').Last(); - - /// - /// Method taken from PLogFormatter.cs file. Takes in Event e and returns string - /// with details about the event such as event name and its payload. Slightly modified - /// from the method in PLogFormatter.cs in that payload is parsed with the CleanPayloadString - /// method right above. - /// - /// Event input. - /// String with the event description. - private static string GetEventNameWithPayload(Event e) - { - if (e.GetType().Name.Contains("GotoStateEvent")) - { - return e.GetType().Name; - } - - var pe = (PEvent)(e); - var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString(); - var msg = pe.Payload == null ? "" : $" with payload ({payload})"; - return $"{GetShortName(e.GetType().Name)}{msg}"; - } - - /// - /// Takes in Event e and returns the dictionary representation of the payload of the event. - /// - /// Event input. - /// Dictionary representation of the payload for the event, if any. - private static object GetEventPayloadInJson(Event e) - { - if (e.GetType().Name.Contains("GotoStateEvent")) - { - return null; - } - - var pe = (PEvent)(e); - return pe.Payload?.ToDict(); - } - - public override void OnCompleted() - { - } - - public override void OnAssertionFailure(string error) - { - error = RemoveLogTag(error); - - Writer.AddLogType(JsonWriter.LogType.AssertionFailure); - Writer.LogDetails.Error = error; - Writer.AddLog(error); - Writer.AddToLogs(); - } - - /// - public override void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) - { - if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine")) - { - return; - } - - var source = creatorName ?? $"task '{Task.CurrentId}'"; - var log = $"{id} was created by {source}."; - - Writer.AddLogType(JsonWriter.LogType.CreateStateMachine); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.CreatorName = creatorName; - Writer.LogDetails.CreatorType = GetShortName(creatorType); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnDefaultEventHandler(StateMachineId id, string stateName) - { - stateName = GetShortName(stateName); - - var log = stateName is null - ? $"{id} is executing the default handler." - : $"{id} is executing the default handler in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.DefaultEventHandler); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.State = stateName; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnDequeueEvent(StateMachineId id, string stateName, Event e) - { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - - var eventName = GetEventNameWithPayload(e); - var log = stateName is null - ? $"'{id}' dequeued event '{eventName}'." - : $"'{id}' dequeued event '{eventName}' in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.DequeueEvent); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.Event = GetShortName(e.GetType().Name); - Writer.LogDetails.State = GetShortName(stateName); - Writer.LogDetails.Payload = GetEventPayloadInJson(e); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnEnqueueEvent(StateMachineId id, Event e) - { - } - - public override void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) - { - if (ex is PNonStandardReturnException) - { - return; - } - - var log = stateName is null - ? $"{id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'." - : $"{id} running action '{actionName}' in state '{stateName}' chose to handle exception '{ex.GetType().Name}'."; - - Writer.AddLogType(JsonWriter.LogType.ExceptionHandled); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.State = GetShortName(stateName); - Writer.LogDetails.Action = actionName; - Writer.LogDetails.Exception = ex.GetType().Name; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) - { - if (ex is PNonStandardReturnException) - { - return; - } - - var log = stateName is null - ? $"{id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'." - : $"{id} running action '{actionName}' in state '{stateName}' threw exception '{ex.GetType().Name}'."; - - Writer.AddLogType(JsonWriter.LogType.ExceptionThrown); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.State = GetShortName(stateName); - Writer.LogDetails.Action = actionName; - Writer.LogDetails.Exception = ex.GetType().Name; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) - { - } - - public override void OnGotoState(StateMachineId id, string currentStateName, string newStateName) - { - if (currentStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - - currentStateName = GetShortName(currentStateName); - newStateName = GetShortName(newStateName); - - var log = - $"{id} is transitioning from state '{currentStateName}' to state '{newStateName}'."; - - Writer.AddLogType(JsonWriter.LogType.GotoState); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.StartState = currentStateName; - Writer.LogDetails.EndState = newStateName; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnHalt(StateMachineId id, int inboxSize) - { - var log = $"{id} halted with {inboxSize} events in its inbox."; - - Writer.AddLogType(JsonWriter.LogType.Halt); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.HaltInboxSize = inboxSize; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) - { - } - - public override void OnPopState(StateMachineId id, string currentStateName, string restoredStateName) - { - currentStateName = string.IsNullOrEmpty(currentStateName) ? "[not recorded]" : currentStateName; - var reenteredStateName = restoredStateName ?? string.Empty; - var log = $"{id} popped state '{currentStateName}' and reentered state '{reenteredStateName}'."; - - Writer.AddLogType(JsonWriter.LogType.PopState); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.StartState = currentStateName; - Writer.LogDetails.EndState = reenteredStateName; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) - { - var log = $"{id} popped state {stateName} due to unhandled event '{e.GetType().Name}'."; - - Writer.AddLogType(JsonWriter.LogType.PopStateUnhandledEvent); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.State = stateName; - Writer.LogDetails.Event = e.GetType().Name; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnPushState(StateMachineId id, string currentStateName, string newStateName) - { - var log = $"{id} pushed from state '{currentStateName}' to state '{newStateName}'."; - - Writer.AddLogType(JsonWriter.LogType.PushState); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.StartState = currentStateName; - Writer.LogDetails.EndState = newStateName; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnRaiseEvent(StateMachineId id, string stateName, Event e) - { - stateName = GetShortName(stateName); - string eventName = GetEventNameWithPayload(e); - - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || - eventName.Contains("GotoStateEvent")) - { - return; - } - - var log = stateName is null - ? $"'{id}' raised event '{eventName}'." - : $"'{id}' raised event '{eventName}' in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.RaiseEvent); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.Event = GetShortName(e.GetType().Name); - Writer.LogDetails.State = stateName; - Writer.LogDetails.Payload = GetEventPayloadInJson(e); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) - { - stateName = GetShortName(stateName); - string eventName = GetEventNameWithPayload(e); - var unblocked = wasBlocked ? " and unblocked" : string.Empty; - var log = stateName is null - ? $"'{id}' dequeued event '{eventName}'{unblocked}." - : $"'{id}' dequeued event '{eventName}'{unblocked} in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.ReceiveEvent); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.State = stateName; - Writer.LogDetails.Event = GetShortName(e.GetType().Name); - Writer.LogDetails.WasBlocked = wasBlocked; - Writer.LogDetails.Payload = GetEventPayloadInJson(e); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted) - { - senderStateName = GetShortName(senderStateName); - string eventName = GetEventNameWithPayload(e); - var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; - var isHalted = isTargetHalted ? $" which has halted" : string.Empty; - var sender = !string.IsNullOrEmpty(senderName) - ? $"'{senderName}' in state '{senderStateName}'" - : $"The runtime"; - var log = $"{sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}."; - - Writer.AddLogType(JsonWriter.LogType.SendEvent); - Writer.LogDetails.Sender = !string.IsNullOrEmpty(senderName) ? senderName : "Runtime"; - Writer.LogDetails.State = senderStateName; - Writer.LogDetails.Event = GetShortName(e.GetType().Name); - Writer.LogDetails.Target = targetStateMachineId.ToString(); - Writer.LogDetails.OpGroupId = opGroupId.ToString(); - Writer.LogDetails.IsTargetHalted = isTargetHalted; - Writer.LogDetails.Payload = GetEventPayloadInJson(e); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnStateTransition(StateMachineId id, string stateName, bool isEntry) - { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - - stateName = GetShortName(stateName); - var direction = isEntry ? "enters" : "exits"; - var log = $"{id} {direction} state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.StateTransition); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.State = stateName; - Writer.LogDetails.IsEntry = isEntry; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnWaitEvent(StateMachineId id, string stateName, Type eventType) - { - stateName = GetShortName(stateName); - - var log = stateName is null - ? $"{id} is waiting to dequeue an event of type '{eventType.FullName}'." - : $"{id} is waiting to dequeue an event of type '{eventType.FullName}' in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.WaitEvent); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.EventType = eventType.FullName; - Writer.LogDetails.State = stateName; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) - { - stateName = GetShortName(stateName); - string eventNames; - - switch (eventTypes.Length) - { - case 0: - eventNames = "''"; - break; - case 1: - eventNames = "'" + eventTypes[0].Name + "'"; - break; - case 2: - eventNames = "'" + eventTypes[0].Name + "' or '" + eventTypes[1].Name + "'"; - break; - case 3: - eventNames = "'" + eventTypes[0].Name + "', '" + eventTypes[1].Name + "' or '" + - eventTypes[2].Name + - "'"; - break; - default: - { - var eventNameArray = new string[eventTypes.Length - 1]; - for (var i = 0; i < eventTypes.Length - 2; i++) - { - eventNameArray[i] = eventTypes[i].Name; - } - - eventNames = "'" + string.Join("', '", eventNameArray) + "' or '" + - eventTypes[^1].Name + "'"; - break; - } - } - - var log = stateName is null - ? $"{id} is waiting to dequeue an event of type {eventNames}." - : $"{id} is waiting to dequeue an event of type {eventNames} in state '{stateName}'."; - - var eventTypesNames = eventTypes.Select(eventType => eventType.Name).ToList(); - - Writer.AddLogType(JsonWriter.LogType.WaitMultipleEvents); - Writer.LogDetails.Id = id.ToString(); - Writer.LogDetails.EventTypes = eventTypesNames; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnCreateMonitor(string monitorType) - { - monitorType = GetShortName(monitorType); - var log = $"{monitorType} was created."; - - Writer.AddLogType(JsonWriter.LogType.CreateMonitor); - Writer.LogDetails.Monitor = monitorType; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) - { - } - - public override void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, - string senderType, string senderStateName, Event e) - { - monitorType = GetShortName(monitorType); - var log = $"{monitorType} is processing event '{GetEventNameWithPayload(e)}' in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.MonitorProcessEvent); - Writer.LogDetails.Monitor = monitorType; - Writer.LogDetails.State = stateName; - Writer.LogDetails.Sender = senderName; - Writer.LogDetails.Event = GetShortName(e.GetType().Name); - Writer.LogDetails.Payload = GetEventPayloadInJson(e); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) - { - stateName = GetShortName(stateName); - monitorType = GetShortName(monitorType); - string eventName = GetEventNameWithPayload(e); - var log = $"Monitor '{monitorType}' raised event '{eventName}' in state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.MonitorRaiseEvent); - Writer.LogDetails.Monitor = monitorType; - Writer.LogDetails.Event = GetShortName(e.GetType().Name); - Writer.LogDetails.State = stateName; - Writer.LogDetails.Payload = GetEventPayloadInJson(e); - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) - { - monitorType = GetShortName(monitorType); - - if (stateName.Contains("__InitState__")) - { - return; - } - - stateName = GetShortName(stateName); - var liveness = isInHotState.HasValue ? (isInHotState.Value ? "hot " : "cold ") : string.Empty; - var direction = isEntry ? "enters" : "exits"; - var log = $"{monitorType} {direction} {liveness}state '{stateName}'."; - - Writer.AddLogType(JsonWriter.LogType.MonitorStateTransition); - Writer.LogDetails.Monitor = monitorType; - Writer.LogDetails.State = stateName; - Writer.LogDetails.IsEntry = isEntry; - Writer.LogDetails.IsInHotState = isInHotState; - Writer.AddLog(log); - Writer.AddToLogs(updateVcMap: true); - } - - public override void OnMonitorError(string monitorType, string stateName, bool? isInHotState) - { - } - - public override void OnRandom(object result, string callerName, string callerType) - { - } - - public override void OnStrategyDescription(string strategyName, string description) - { - var desc = string.IsNullOrEmpty(description) ? $" Description: {description}" : string.Empty; - var log = $"Found bug using '{strategyName}' strategy.{desc}"; - - Writer.AddLogType(JsonWriter.LogType.StrategyDescription); - Writer.LogDetails.Strategy = strategyName; - Writer.LogDetails.StrategyDescription = description; - Writer.AddLog(log); - Writer.AddToLogs(); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs deleted file mode 100644 index 1364f178b1..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs +++ /dev/null @@ -1,215 +0,0 @@ -using System; -using System.Linq; -using PChecker.StateMachines; -using PChecker.StateMachines.Events; -using PChecker.StateMachines.Logging; -using PChecker.PRuntime.Exceptions; - -namespace PChecker.PRuntime -{ - /// - /// Formatter for the runtime log. - /// - public class PLogFormatter : PCheckerLogTextFormatter - { - public PLogFormatter() : base() - { - } - - private string GetShortName(string name) - { - return name.Split('.').Last(); - } - - private string GetEventNameWithPayload(Event e) - { - if (e.GetType().Name.Contains("GotoStateEvent")) - { - return e.GetType().Name; - } - var pe = (PEvent)(e); - var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString(); - var msg = pe.Payload == null ? "" : $" with payload ({payload})"; - return $"{GetShortName(e.GetType().Name)}{msg}"; - } - - public override void OnStateTransition(StateMachineId id, string stateName, bool isEntry) - { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - - base.OnStateTransition(id, GetShortName(stateName), isEntry); - } - - public override void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) - { - base.OnPopStateUnhandledEvent(id, GetShortName(stateName), e); - } - - public override void OnDefaultEventHandler(StateMachineId id, string stateName) - { - base.OnDefaultEventHandler(id, GetShortName(stateName)); - } - - public override void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) - { - base.OnWaitEvent(id, GetShortName(stateName), eventTypes); - } - - public override void OnWaitEvent(StateMachineId id, string stateName, Type eventType) - { - base.OnWaitEvent(id, GetShortName(stateName), eventType); - } - - public override void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) - { - if (stateName.Contains("__InitState__")) - { - return; - } - - base.OnMonitorStateTransition(monitorType: GetShortName(monitorType), stateName: GetShortName(stateName), isEntry: isEntry, isInHotState: isInHotState); - } - - public override void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, string senderType, - string senderStateName, Event e) - { - var text = $" {GetShortName(monitorType)} is processing event '{GetEventNameWithPayload(e)}' in state '{stateName}'."; - Logger.WriteLine(text); - } - - public override void OnDequeueEvent(StateMachineId id, string stateName, Event e) - { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - - stateName = GetShortName(stateName); - var eventName = GetEventNameWithPayload(e); - string text = null; - if (stateName is null) - { - text = $" '{id}' dequeued event '{eventName}'."; - } - else - { - text = $" '{id}' dequeued event '{eventName}' in state '{stateName}'."; - } - - Logger.WriteLine(text); - } - - public override void OnRaiseEvent(StateMachineId id, string stateName, Event e) - { - stateName = GetShortName(stateName); - var eventName = GetEventNameWithPayload(e); - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || eventName.Contains("GotoStateEvent")) - { - return; - } - - string text = null; - if (stateName is null) - { - text = $" '{id}' raised event '{eventName}'."; - } - else - { - text = $" '{id}' raised event '{eventName}' in state '{stateName}'."; - } - - Logger.WriteLine(text); - } - - public override void OnEnqueueEvent(StateMachineId id, Event e) { } - - public override void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) - { - stateName = GetShortName(stateName); - var eventName = GetEventNameWithPayload(e); - string text = null; - var unblocked = wasBlocked ? " and unblocked" : string.Empty; - if (stateName is null) - { - text = $" '{id}' dequeued event '{eventName}'{unblocked}."; - } - else - { - text = $" '{id}' dequeued event '{eventName}'{unblocked} in state '{stateName}'."; - } - - Logger.WriteLine(text); - } - - public override void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) - { - stateName = GetShortName(stateName); - var eventName = GetEventNameWithPayload(e); - var text = $" Monitor '{GetShortName(monitorType)}' raised event '{eventName}' in state '{stateName}'."; - Logger.WriteLine(text); - } - - public override void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted) - { - senderStateName = GetShortName(senderStateName); - var eventName = GetEventNameWithPayload(e); - var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; - var isHalted = isTargetHalted ? $" which has halted" : string.Empty; - var sender = !string.IsNullOrEmpty(senderName) ? $"'{senderName}' in state '{senderStateName}'" : $"The runtime"; - var text = $" {sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}."; - Logger.WriteLine(text); - } - - public override void OnGotoState(StateMachineId id, string currStateName, string newStateName) - { - if (currStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - - base.OnGotoState(id, GetShortName(currStateName), GetShortName(newStateName)); - } - - public override void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) - { - } - - public override void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) - { - } - - public override void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) - { - if (ex is PNonStandardReturnException) - { - return; - } - base.OnExceptionHandled(id: id, stateName: GetShortName(stateName), actionName: actionName, ex: ex); - } - - public override void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) - { - if (ex is PNonStandardReturnException) - { - return; - } - base.OnExceptionThrown(id: id, stateName: GetShortName(stateName), actionName: actionName, ex: ex); - } - - public override void OnCreateMonitor(string monitorType) - { - base.OnCreateMonitor(GetShortName(monitorType)); - } - - public override void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) - { - } - - public override void OnRandom(object result, string callerName, string callerType) - { - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs index 70d4ddad6c..58fa631bb8 100644 --- a/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs +++ b/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs @@ -7,6 +7,7 @@ using System.Linq; using PChecker.StateMachines.Events; using PChecker.IO.Logging; +using PChecker.PRuntime; namespace PChecker.StateMachines.Logging { @@ -602,7 +603,7 @@ internal void RegisterLog(IStateMachineRuntimeLog log) } } - // If log is or of subclass PCheckerLogJsonFormatter (i.e. when log is PJsonFormatter), + // If log is or of subclass PCheckerLogJsonFormatter (i.e. when log is PCheckerLogJsonFormatter), // update the Writer reference to the JsonLogger instance defined within LogWriter.cs if (log is PCheckerLogJsonFormatter tempJsonFormatter) { diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs index 07d7b1f832..5ea4fab5b0 100644 --- a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs +++ b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs @@ -2,9 +2,14 @@ // Licensed under the MIT License. using System; +using System.Linq; +using System.Threading.Tasks; +using PChecker.StateMachines; using PChecker.StateMachines.Events; +using PChecker.StateMachines.Logging; +using PChecker.PRuntime.Exceptions; -namespace PChecker.StateMachines.Logging +namespace PChecker.PRuntime { /// /// This class implements IStateMachineRuntimeLog and generates log output in an XML format. @@ -15,7 +20,7 @@ public class PCheckerLogJsonFormatter : IStateMachineRuntimeLog /// Get or set the JsonWriter to write to. /// public JsonWriter Writer { get; set; } - + /// /// Initializes a new instance of the class. /// @@ -24,154 +29,527 @@ protected PCheckerLogJsonFormatter() Writer = new JsonWriter(); } - /// - public virtual void OnCompleted() + /// + /// Removes the '<' and '>' tags for a log text. + /// + /// The text log + /// New string with the tag removed or just the string itself if there is no tag. + private static string RemoveLogTag(string log) { + var openingTagIndex = log.IndexOf("<", StringComparison.Ordinal); + var closingTagIndex = log.IndexOf(">", StringComparison.Ordinal); + var potentialTagExists = openingTagIndex != -1 && closingTagIndex != -1; + var validOpeningTag = openingTagIndex == 0 && closingTagIndex > openingTagIndex; + + if (potentialTagExists && validOpeningTag) + { + return log[(closingTagIndex + 1)..].Trim(); + } + + return log; } - /// - public virtual void OnAssertionFailure(string error) + /// + /// Method taken from PLogFormatter.cs file. Takes in a string and only get the + /// last element of the string separated by a period. + /// I.e. + /// Input: PImplementation.TestWithSingleClient(2) + /// Output: TestWithSingleClient(2) + /// + /// String representing the name to be parsed. + /// The split string. + private static string GetShortName(string name) => name?.Split('.').Last(); + + /// + /// Method taken from PLogFormatter.cs file. Takes in Event e and returns string + /// with details about the event such as event name and its payload. Slightly modified + /// from the method in PLogFormatter.cs in that payload is parsed with the CleanPayloadString + /// method right above. + /// + /// Event input. + /// String with the event description. + private static string GetEventNameWithPayload(Event e) { + if (e.GetType().Name.Contains("GotoStateEvent")) + { + return e.GetType().Name; + } + + var pe = (PEvent)(e); + var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString(); + var msg = pe.Payload == null ? "" : $" with payload ({payload})"; + return $"{GetShortName(e.GetType().Name)}{msg}"; + } + + /// + /// Takes in Event e and returns the dictionary representation of the payload of the event. + /// + /// Event input. + /// Dictionary representation of the payload for the event, if any. + private static object GetEventPayloadInJson(Event e) + { + if (e.GetType().Name.Contains("GotoStateEvent")) + { + return null; + } + + var pe = (PEvent)(e); + return pe.Payload?.ToDict(); + } + + public void OnCompleted() + { + } + + public void OnAssertionFailure(string error) + { + error = RemoveLogTag(error); + + Writer.AddLogType(JsonWriter.LogType.AssertionFailure); + Writer.LogDetails.Error = error; + Writer.AddLog(error); + Writer.AddToLogs(); } - /// - public virtual void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) + /// + public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) { + if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine")) + { + return; + } + + var source = creatorName ?? $"task '{Task.CurrentId}'"; + var log = $"{id} was created by {source}."; + + Writer.AddLogType(JsonWriter.LogType.CreateStateMachine); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.CreatorName = creatorName; + Writer.LogDetails.CreatorType = GetShortName(creatorType); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } - /// - public virtual void OnDefaultEventHandler(StateMachineId id, string stateName) + public void OnDefaultEventHandler(StateMachineId id, string stateName) { + stateName = GetShortName(stateName); + + var log = stateName is null + ? $"{id} is executing the default handler." + : $"{id} is executing the default handler in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.DefaultEventHandler); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } - /// - public virtual void OnDequeueEvent(StateMachineId id, string stateName, Event e) + public void OnDequeueEvent(StateMachineId id, string stateName, Event e) { + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + var eventName = GetEventNameWithPayload(e); + var log = stateName is null + ? $"'{id}' dequeued event '{eventName}'." + : $"'{id}' dequeued event '{eventName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.DequeueEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = GetShortName(stateName); + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnEnqueueEvent(StateMachineId id, Event e) + public void OnEnqueueEvent(StateMachineId id, Event e) { } /// - public virtual void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) + public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) { + if (ex is PNonStandardReturnException) + { + return; + } + + var log = stateName is null + ? $"{id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'." + : $"{id} running action '{actionName}' in state '{stateName}' chose to handle exception '{ex.GetType().Name}'."; + + Writer.AddLogType(JsonWriter.LogType.ExceptionHandled); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = GetShortName(stateName); + Writer.LogDetails.Action = actionName; + Writer.LogDetails.Exception = ex.GetType().Name; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) + public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) { - } + if (ex is PNonStandardReturnException) + { + return; + } + + var log = stateName is null + ? $"{id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'." + : $"{id} running action '{actionName}' in state '{stateName}' threw exception '{ex.GetType().Name}'."; + Writer.AddLogType(JsonWriter.LogType.ExceptionThrown); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = GetShortName(stateName); + Writer.LogDetails.Action = actionName; + Writer.LogDetails.Exception = ex.GetType().Name; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + /// - public virtual void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, - string actionName) + public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) { } /// - public virtual void OnGotoState(StateMachineId id, string currentStateName, string newStateName) + public void OnGotoState(StateMachineId id, string currentStateName, string newStateName) { + if (currentStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + currentStateName = GetShortName(currentStateName); + newStateName = GetShortName(newStateName); + + var log = + $"{id} is transitioning from state '{currentStateName}' to state '{newStateName}'."; + + Writer.AddLogType(JsonWriter.LogType.GotoState); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.StartState = currentStateName; + Writer.LogDetails.EndState = newStateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnHalt(StateMachineId id, int inboxSize) + public void OnHalt(StateMachineId id, int inboxSize) { - } + var log = $"{id} halted with {inboxSize} events in its inbox."; + Writer.AddLogType(JsonWriter.LogType.Halt); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.HaltInboxSize = inboxSize; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + /// - public virtual void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) + public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) { } /// - public virtual void OnPopState(StateMachineId id, string currentStateName, string restoredStateName) + public void OnPopState(StateMachineId id, string currentStateName, string restoredStateName) { + currentStateName = string.IsNullOrEmpty(currentStateName) ? "[not recorded]" : currentStateName; + var reenteredStateName = restoredStateName ?? string.Empty; + var log = $"{id} popped state '{currentStateName}' and reentered state '{reenteredStateName}'."; + + Writer.AddLogType(JsonWriter.LogType.PopState); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.StartState = currentStateName; + Writer.LogDetails.EndState = reenteredStateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) + public void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) { + var log = $"{id} popped state {stateName} due to unhandled event '{e.GetType().Name}'."; + + Writer.AddLogType(JsonWriter.LogType.PopStateUnhandledEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Event = e.GetType().Name; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnPushState(StateMachineId id, string currentStateName, string newStateName) + public void OnPushState(StateMachineId id, string currentStateName, string newStateName) { + var log = $"{id} pushed from state '{currentStateName}' to state '{newStateName}'."; + + Writer.AddLogType(JsonWriter.LogType.PushState); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.StartState = currentStateName; + Writer.LogDetails.EndState = newStateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnRaiseEvent(StateMachineId id, string stateName, Event e) + public void OnRaiseEvent(StateMachineId id, string stateName, Event e) { + stateName = GetShortName(stateName); + string eventName = GetEventNameWithPayload(e); + + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || + eventName.Contains("GotoStateEvent")) + { + return; + } + + var log = stateName is null + ? $"'{id}' raised event '{eventName}'." + : $"'{id}' raised event '{eventName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.RaiseEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) + public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) { + stateName = GetShortName(stateName); + string eventName = GetEventNameWithPayload(e); + var unblocked = wasBlocked ? " and unblocked" : string.Empty; + var log = stateName is null + ? $"'{id}' dequeued event '{eventName}'{unblocked}." + : $"'{id}' dequeued event '{eventName}'{unblocked} in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.ReceiveEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.WasBlocked = wasBlocked; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, - string senderStateName, + public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted) { + senderStateName = GetShortName(senderStateName); + string eventName = GetEventNameWithPayload(e); + var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; + var isHalted = isTargetHalted ? $" which has halted" : string.Empty; + var sender = !string.IsNullOrEmpty(senderName) + ? $"'{senderName}' in state '{senderStateName}'" + : $"The runtime"; + var log = $"{sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}."; + + Writer.AddLogType(JsonWriter.LogType.SendEvent); + Writer.LogDetails.Sender = !string.IsNullOrEmpty(senderName) ? senderName : "Runtime"; + Writer.LogDetails.State = senderStateName; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.Target = targetStateMachineId.ToString(); + Writer.LogDetails.OpGroupId = opGroupId.ToString(); + Writer.LogDetails.IsTargetHalted = isTargetHalted; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnStateTransition(StateMachineId id, string stateName, bool isEntry) + public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) { + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + stateName = GetShortName(stateName); + var direction = isEntry ? "enters" : "exits"; + var log = $"{id} {direction} state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.StateTransition); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.LogDetails.IsEntry = isEntry; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnWaitEvent(StateMachineId id, string stateName, Type eventType) + public void OnWaitEvent(StateMachineId id, string stateName, Type eventType) { + stateName = GetShortName(stateName); + + var log = stateName is null + ? $"{id} is waiting to dequeue an event of type '{eventType.FullName}'." + : $"{id} is waiting to dequeue an event of type '{eventType.FullName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.WaitEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.EventType = eventType.FullName; + Writer.LogDetails.State = stateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) + public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) { + stateName = GetShortName(stateName); + string eventNames; + + switch (eventTypes.Length) + { + case 0: + eventNames = "''"; + break; + case 1: + eventNames = "'" + eventTypes[0].Name + "'"; + break; + case 2: + eventNames = "'" + eventTypes[0].Name + "' or '" + eventTypes[1].Name + "'"; + break; + case 3: + eventNames = "'" + eventTypes[0].Name + "', '" + eventTypes[1].Name + "' or '" + + eventTypes[2].Name + + "'"; + break; + default: + { + var eventNameArray = new string[eventTypes.Length - 1]; + for (var i = 0; i < eventTypes.Length - 2; i++) + { + eventNameArray[i] = eventTypes[i].Name; + } + + eventNames = "'" + string.Join("', '", eventNameArray) + "' or '" + + eventTypes[^1].Name + "'"; + break; + } + } + + var log = stateName is null + ? $"{id} is waiting to dequeue an event of type {eventNames}." + : $"{id} is waiting to dequeue an event of type {eventNames} in state '{stateName}'."; + + var eventTypesNames = eventTypes.Select(eventType => eventType.Name).ToList(); + + Writer.AddLogType(JsonWriter.LogType.WaitMultipleEvents); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.EventTypes = eventTypesNames; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnCreateMonitor(string monitorType) + public void OnCreateMonitor(string monitorType) { + monitorType = GetShortName(monitorType); + var log = $"{monitorType} was created."; + + Writer.AddLogType(JsonWriter.LogType.CreateMonitor); + Writer.LogDetails.Monitor = monitorType; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) + public void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) { } /// - public virtual void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, + public void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, string senderType, string senderStateName, Event e) { + monitorType = GetShortName(monitorType); + var log = $"{monitorType} is processing event '{GetEventNameWithPayload(e)}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.MonitorProcessEvent); + Writer.LogDetails.Monitor = monitorType; + Writer.LogDetails.State = stateName; + Writer.LogDetails.Sender = senderName; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) + public void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) { + stateName = GetShortName(stateName); + monitorType = GetShortName(monitorType); + string eventName = GetEventNameWithPayload(e); + var log = $"Monitor '{monitorType}' raised event '{eventName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.MonitorRaiseEvent); + Writer.LogDetails.Monitor = monitorType; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, - bool? isInHotState) + public void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) { + monitorType = GetShortName(monitorType); + + if (stateName.Contains("__InitState__")) + { + return; + } + + stateName = GetShortName(stateName); + var liveness = isInHotState.HasValue ? (isInHotState.Value ? "hot " : "cold ") : string.Empty; + var direction = isEntry ? "enters" : "exits"; + var log = $"{monitorType} {direction} {liveness}state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.MonitorStateTransition); + Writer.LogDetails.Monitor = monitorType; + Writer.LogDetails.State = stateName; + Writer.LogDetails.IsEntry = isEntry; + Writer.LogDetails.IsInHotState = isInHotState; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); } /// - public virtual void OnMonitorError(string monitorType, string stateName, bool? isInHotState) + public void OnMonitorError(string monitorType, string stateName, bool? isInHotState) { } - + /// - public virtual void OnRandom(object result, string callerName, string callerType) + public void OnRandom(object result, string callerName, string callerType) { } /// - public virtual void OnStrategyDescription(string strategyName, string description) + public void OnStrategyDescription(string strategyName, string description) { + var desc = string.IsNullOrEmpty(description) ? $" Description: {description}" : string.Empty; + var log = $"Found bug using '{strategyName}' strategy.{desc}"; + + Writer.AddLogType(JsonWriter.LogType.StrategyDescription); + Writer.LogDetails.Strategy = strategyName; + Writer.LogDetails.StrategyDescription = description; + Writer.AddLog(log); + Writer.AddToLogs(); } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs index b22694712b..22025bab5a 100644 --- a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs +++ b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs @@ -1,16 +1,17 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; +using System; using System.IO; +using System.Linq; using System.Threading.Tasks; -using PChecker.StateMachines.Events; using PChecker.IO.Logging; +using PChecker.StateMachines; +using PChecker.StateMachines.Events; +using PChecker.StateMachines.Logging; +using PChecker.PRuntime.Exceptions; -namespace PChecker.StateMachines.Logging +namespace PChecker.PRuntime { /// - /// This class implements IStateMachineRuntimeLog and generates output in a a human readable text format. + /// Formatter for the runtime log. /// public class PCheckerLogTextFormatter : IStateMachineRuntimeLog { @@ -27,8 +28,25 @@ public PCheckerLogTextFormatter() Logger = new ConsoleLogger(); } + private string GetShortName(string name) + { + return name.Split('.').Last(); + } + + private string GetEventNameWithPayload(Event e) + { + if (e.GetType().Name.Contains("GotoStateEvent")) + { + return e.GetType().Name; + } + var pe = (PEvent)(e); + var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString(); + var msg = pe.Payload == null ? "" : $" with payload ({payload})"; + return $"{GetShortName(e.GetType().Name)}{msg}"; + } + /// - public virtual void OnAssertionFailure(string error) + public void OnAssertionFailure(string error) { Logger.WriteLine(error); } @@ -44,16 +62,30 @@ public void OnCreateStateMachine(StateMachineId id, string creatorName, string c var text = $" {id} was created by {source}."; Logger.WriteLine(text); } + + /// + public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) + { + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + var direction = isEntry ? "enters" : "exits"; + var text = $" {id} {direction} state '{stateName}'."; + Logger.WriteLine(text); + } /// - public virtual void OnCreateMonitor(string monitorType) + public void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) { - var text = $" {monitorType} was created."; + var eventName = e.GetType().Name; + var text = $" {id} popped state {stateName} due to unhandled event '{eventName}'."; Logger.WriteLine(text); } /// - public virtual void OnDefaultEventHandler(StateMachineId id, string stateName) + public void OnDefaultEventHandler(StateMachineId id, string stateName) { string text; if (stateName is null) @@ -69,296 +101,281 @@ public virtual void OnDefaultEventHandler(StateMachineId id, string stateName) } /// - public virtual void OnDequeueEvent(StateMachineId id, string stateName, Event e) + public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) { - var eventName = e.GetType().FullName; string text; - if (stateName is null) + string eventNames; + if (eventTypes.Length == 0) { - text = $" {id} dequeued event '{eventName}'."; + eventNames = "''"; + } + else if (eventTypes.Length == 1) + { + eventNames = "'" + eventTypes[0].Name + "'"; + } + else if (eventTypes.Length == 2) + { + eventNames = "'" + eventTypes[0].Name + "' or '" + eventTypes[1].Name + "'"; + } + else if (eventTypes.Length == 3) + { + eventNames = "'" + eventTypes[0].Name + "', '" + eventTypes[1].Name + "' or '" + eventTypes[2].Name + "'"; } else { - text = $" {id} dequeued event '{eventName}' in state '{stateName}'."; + var eventNameArray = new string[eventTypes.Length - 1]; + for (var i = 0; i < eventTypes.Length - 2; i++) + { + eventNameArray[i] = eventTypes[i].Name; + } + + eventNames = "'" + string.Join("', '", eventNameArray) + "' or '" + eventTypes[eventTypes.Length - 1].Name + "'"; } - Logger.WriteLine(text); - } + if (stateName is null) + { + text = $" {id} is waiting to dequeue an event of type {eventNames}."; + } + else + { + text = $" {id} is waiting to dequeue an event of type {eventNames} in state '{stateName}'."; + } - /// - public virtual void OnEnqueueEvent(StateMachineId id, Event e) - { - var eventName = e.GetType().FullName; - var text = $" {id} enqueued event '{eventName}'."; Logger.WriteLine(text); } /// - public virtual void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) + public void OnWaitEvent(StateMachineId id, string stateName, Type eventType) { string text; if (stateName is null) { - text = $" {id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'."; + text = $" {id} is waiting to dequeue an event of type '{eventType.FullName}'."; } else { - text = $" {id} running action '{actionName}' in state '{stateName}' chose to handle exception '{ex.GetType().Name}'."; + text = $" {id} is waiting to dequeue an event of type '{eventType.FullName}' in state '{stateName}'."; } - + Logger.WriteLine(text); } /// - public virtual void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) + public void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) { - string text; - if (stateName is null) + if (stateName.Contains("__InitState__")) { - text = $" {id} running action '{actionName}' threw exception '{ex.GetType().Name}'."; - } - else - { - text = $" {id} running action '{actionName}' in state '{stateName}' threw exception '{ex.GetType().Name}'."; + return; } + var liveness = isInHotState.HasValue ? (isInHotState.Value ? "hot " : "cold ") : string.Empty; + var direction = isEntry ? "enters" : "exits"; + var text = $" {monitorType} {direction} {liveness}state '{stateName}'."; + Logger.WriteLine(text); + } + + /// + public void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, string senderType, + string senderStateName, Event e) + { + var text = $" {GetShortName(monitorType)} is processing event '{GetEventNameWithPayload(e)}' in state '{stateName}'."; Logger.WriteLine(text); } /// - public virtual void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) + public void OnDequeueEvent(StateMachineId id, string stateName, Event e) { - string text; - if (currentStateName is null) + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) { - text = $" {id} invoked action '{actionName}'."; + return; } - else if (handlingStateName != currentStateName) + + stateName = GetShortName(stateName); + var eventName = GetEventNameWithPayload(e); + string text = null; + if (stateName is null) { - text = $" {id} invoked action '{actionName}' in state '{currentStateName}' where action was declared by state '{handlingStateName}'."; + text = $" '{id}' dequeued event '{eventName}'."; } else { - text = $" {id} invoked action '{actionName}' in state '{currentStateName}'."; + text = $" '{id}' dequeued event '{eventName}' in state '{stateName}'."; } Logger.WriteLine(text); } /// - public virtual void OnGotoState(StateMachineId id, string currentStateName, string newStateName) + public void OnRaiseEvent(StateMachineId id, string stateName, Event e) { - var text = $" {id} is transitioning from state '{currentStateName}' to state '{newStateName}'."; - Logger.WriteLine(text); - } + stateName = GetShortName(stateName); + var eventName = GetEventNameWithPayload(e); + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || eventName.Contains("GotoStateEvent")) + { + return; + } + + string text = null; + if (stateName is null) + { + text = $" '{id}' raised event '{eventName}'."; + } + else + { + text = $" '{id}' raised event '{eventName}' in state '{stateName}'."; + } - /// - public virtual void OnHalt(StateMachineId id, int inboxSize) - { - var text = $" {id} halted with {inboxSize} events in its inbox."; Logger.WriteLine(text); } /// - public virtual void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) - { - } + public void OnEnqueueEvent(StateMachineId id, Event e) { } /// - public virtual void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) + public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) { - var text = $" {monitorType} executed action '{actionName}' in state '{stateName}'."; - Logger.WriteLine(text); - } + stateName = GetShortName(stateName); + var eventName = GetEventNameWithPayload(e); + string text = null; + var unblocked = wasBlocked ? " and unblocked" : string.Empty; + if (stateName is null) + { + text = $" '{id}' dequeued event '{eventName}'{unblocked}."; + } + else + { + text = $" '{id}' dequeued event '{eventName}'{unblocked} in state '{stateName}'."; + } - /// - public virtual void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, - string senderType, string senderStateName, Event e) - { - var text = $" {monitorType} is processing event '{e.GetType().Name}' in state '{stateName}'."; Logger.WriteLine(text); } /// - public virtual void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) + public void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) { - var eventName = e.GetType().FullName; - var text = $" {monitorType} raised event '{eventName}' in state '{stateName}'."; + stateName = GetShortName(stateName); + var eventName = GetEventNameWithPayload(e); + var text = $" Monitor '{GetShortName(monitorType)}' raised event '{eventName}' in state '{stateName}'."; Logger.WriteLine(text); } /// - public virtual void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) + public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted) { - var liveness = isInHotState.HasValue ? (isInHotState.Value ? "hot " : "cold ") : string.Empty; - var direction = isEntry ? "enters" : "exits"; - var text = $" {monitorType} {direction} {liveness}state '{stateName}'."; + senderStateName = GetShortName(senderStateName); + var eventName = GetEventNameWithPayload(e); + var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; + var isHalted = isTargetHalted ? $" which has halted" : string.Empty; + var sender = !string.IsNullOrEmpty(senderName) ? $"'{senderName}' in state '{senderStateName}'" : $"The runtime"; + var text = $" {sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}."; Logger.WriteLine(text); } /// - public virtual void OnMonitorError(string monitorType, string stateName, bool? isInHotState) + public void OnGotoState(StateMachineId id, string currStateName, string newStateName) { - } + if (currStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } - /// - public virtual void OnPopState(StateMachineId id, string currentStateName, string restoredStateName) - { - currentStateName = string.IsNullOrEmpty(currentStateName) ? "[not recorded]" : currentStateName; - var reenteredStateName = restoredStateName ?? string.Empty; - var text = $" {id} popped state '{currentStateName}' and reentered state '{reenteredStateName}'."; + var text = $" {id} is transitioning from state '{currStateName}' to state '{newStateName}'."; Logger.WriteLine(text); } /// - public virtual void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) + public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) { - var eventName = e.GetType().Name; - var text = $" {id} popped state {stateName} due to unhandled event '{eventName}'."; - Logger.WriteLine(text); } /// - public virtual void OnPushState(StateMachineId id, string currentStateName, string newStateName) + public void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) { - var text = $" {id} pushed from state '{currentStateName}' to state '{newStateName}'."; - Logger.WriteLine(text); } /// - public virtual void OnRaiseEvent(StateMachineId id, string stateName, Event e) + public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) { - var eventName = e.GetType().FullName; + if (ex is PNonStandardReturnException) + { + return; + } string text; if (stateName is null) { - text = $" {id} raised event '{eventName}'."; + text = $" {id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'."; } else { - text = $" {id} raised event '{eventName}' in state '{stateName}'."; + text = $" {id} running action '{actionName}' in state '{stateName}' chose to handle exception '{ex.GetType().Name}'."; } Logger.WriteLine(text); } /// - public virtual void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) + public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) { - var eventName = e.GetType().FullName; + if (ex is PNonStandardReturnException) + { + return; + } string text; - var unblocked = wasBlocked ? " and unblocked" : string.Empty; if (stateName is null) { - text = $" {id} dequeued event '{eventName}'{unblocked}."; + text = $" {id} running action '{actionName}' threw exception '{ex.GetType().Name}'."; } else { - text = $" {id} dequeued event '{eventName}'{unblocked} in state '{stateName}'."; + text = $" {id} running action '{actionName}' in state '{stateName}' threw exception '{ex.GetType().Name}'."; } Logger.WriteLine(text); } /// - public virtual void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted) + public void OnCreateMonitor(string monitorType) { - var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; - var isHalted = isTargetHalted ? $" which has halted" : string.Empty; - var sender = senderName != null ? $"{senderName} in state '{senderStateName}'" : $"task '{Task.CurrentId}'"; - var eventName = e.GetType().FullName; - var text = $" {sender} sent event '{eventName}' to {targetStateMachineId}{isHalted}{opGroupIdMsg}."; + var text = $" {monitorType} was created."; Logger.WriteLine(text); } /// - public virtual void OnStateTransition(StateMachineId id, string stateName, bool isEntry) + public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) { - var direction = isEntry ? "enters" : "exits"; - var text = $" {id} {direction} state '{stateName}'."; - Logger.WriteLine(text); } /// - public virtual void OnStrategyDescription(string strategyName, string description) + public void OnRandom(object result, string callerName, string callerType) { - var desc = string.IsNullOrEmpty(description) ? $" Description: {description}" : string.Empty; - var text = $" Found bug using '{strategyName}' strategy.{desc}"; + var source = callerName ?? $"Task '{Task.CurrentId}'"; + var text = $" {source} nondeterministically chose '{result}'."; Logger.WriteLine(text); } - + /// - public virtual void OnWaitEvent(StateMachineId id, string stateName, Type eventType) + public void OnHalt(StateMachineId id, int inboxSize) { - string text; - if (stateName is null) - { - text = $" {id} is waiting to dequeue an event of type '{eventType.FullName}'."; - } - else - { - text = $" {id} is waiting to dequeue an event of type '{eventType.FullName}' in state '{stateName}'."; - } - + var text = $" {id} halted with {inboxSize} events in its inbox."; Logger.WriteLine(text); } - + /// - public virtual void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) + public void OnMonitorError(string monitorType, string stateName, bool? isInHotState) { - string text; - string eventNames; - if (eventTypes.Length == 0) - { - eventNames = "''"; - } - else if (eventTypes.Length == 1) - { - eventNames = "'" + eventTypes[0].Name + "'"; - } - else if (eventTypes.Length == 2) - { - eventNames = "'" + eventTypes[0].Name + "' or '" + eventTypes[1].Name + "'"; - } - else if (eventTypes.Length == 3) - { - eventNames = "'" + eventTypes[0].Name + "', '" + eventTypes[1].Name + "' or '" + eventTypes[2].Name + "'"; - } - else - { - var eventNameArray = new string[eventTypes.Length - 1]; - for (var i = 0; i < eventTypes.Length - 2; i++) - { - eventNameArray[i] = eventTypes[i].Name; - } - - eventNames = "'" + string.Join("', '", eventNameArray) + "' or '" + eventTypes[eventTypes.Length - 1].Name + "'"; - } - - if (stateName is null) - { - text = $" {id} is waiting to dequeue an event of type {eventNames}."; - } - else - { - text = $" {id} is waiting to dequeue an event of type {eventNames} in state '{stateName}'."; - } - - Logger.WriteLine(text); } /// - public virtual void OnRandom(object result, string callerName, string callerType) + public void OnCompleted() { - var source = callerName ?? $"Task '{Task.CurrentId}'"; - var text = $" {source} nondeterministically chose '{result}'."; - Logger.WriteLine(text); } - + /// - public virtual void OnCompleted() + public void OnStrategyDescription(string strategyName, string description) { + var desc = string.IsNullOrEmpty(description) ? $" Description: {description}" : string.Empty; + var text = $" Found bug using '{strategyName}' strategy.{desc}"; + Logger.WriteLine(text); } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs index 68a06f48e9..1751632652 100644 --- a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs +++ b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs @@ -161,6 +161,13 @@ private void EmitTestReport() } Console.WriteLine(testReport.GetText(_checkerConfiguration, "...")); + + var file = Path.GetFileNameWithoutExtension(testReport.CheckerConfiguration.AssemblyToBeAnalyzed); + var directory = testReport.CheckerConfiguration.OutputDirectory; + var pintPath = directory + file + "_pchecker_summary.txt"; + Console.WriteLine($"..... Writing {pintPath}"); + File.WriteAllText(pintPath, testReport.GetSummaryText(Profiler)); + Console.WriteLine($"... Elapsed {Profiler.GetElapsedTime()} sec."); if (testReport.InternalErrors.Count > 0) diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 242409b169..df9137281e 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -386,8 +386,6 @@ private void WriteTestFunction(CompilationContext context, StringWriter output, context.WriteLine(output); context.WriteLine(output, "[PChecker.SystematicTesting.Test]"); context.WriteLine(output, "public static void Execute(IStateMachineRuntime runtime) {"); - context.WriteLine(output, "runtime.RegisterLog(new PLogFormatter());"); - context.WriteLine(output, "runtime.RegisterLog(new PJsonFormatter());"); context.WriteLine(output, "PModule.runtime = runtime;"); context.WriteLine(output, "PHelper.InitializeInterfaces();"); context.WriteLine(output, "PHelper.InitializeEnums();");