<commit_before>﻿//-----------------------------------------------------------------------
// <copyright file="StateMachineLogger.cs">
//      Copyright (c) Microsoft Corporation. All rights reserved.
// 
//      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
//      EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
//      MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
//      IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
//      CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
//      TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
//      SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
// </copyright>
//-----------------------------------------------------------------------

using Microsoft.PSharp.Utilities;
using System;

namespace Microsoft.PSharp.IO
{
    /// <summary>
    /// An implementation of <see cref="ILogger"/> that by default passes all logging commands to the variants
    /// of the <see cref="Write(string)"/> method if the <see cref="Configuration.Verbose"/> option is set to
    /// >= <see cref="LoggingVerbosity"/>. This class may be subclassed and its methods overridden.
    /// </summary>
    public abstract class StateMachineLogger : ILogger
    {
        /// <summary>
        /// The configuration that sets the logging verbosity.
        /// </summary>
        public Configuration Configuration { get; set; }

        /// <summary>
        /// The minimum logging verbosity level. If <see cref="Configuration.Verbose"/> is >=
        /// <see cref="LoggingVerbosity"/>, then messages are logged (0 logs all messages).
        /// </summary>
        public int LoggingVerbosity { get; set; } = 2;

        /// <summary>
        /// Convenience method to indicate whether <see cref="Configuration.Verbose"/> is at or
        /// above <see cref="LoggingVerbosity"/>.
        /// </summary>
        public bool IsVerbose => this.Configuration.Verbose >= LoggingVerbosity;

        /// <summary>
        /// Constructs the logger. The logger will be assigned the Runtime's Configuration
        /// object when it is passed to <see cref="PSharpRuntime.SetLogger(ILogger)"/>.
        /// </summary>
        /// <param name="loggingVerbosity">The initial logging verbosity level.</param>
        public StateMachineLogger(int loggingVerbosity = 2)
        {
            this.LoggingVerbosity = loggingVerbosity;
        }

        /// <summary>
        /// Writes the specified string value.
        /// </summary>
        /// <param name="value">Text</param>
        public abstract void Write(string value);

        /// <summary>
        /// Writes the text representation of the specified array of objects.
        /// </summary>
        /// <param name="format">Text</param>
        /// <param name="args">Arguments</param>
        public abstract void Write(string format, params object[] args);

        /// <summary>
        /// Writes the specified string value, followed by the
        /// current line terminator.
        /// </summary>
        /// <param name="value">Text</param>
        public abstract void WriteLine(string value);

        /// <summary>
        /// Writes the text representation of the specified array of objects,
        /// followed by the current line terminator.
        /// </summary>
        /// <param name="format">Text</param>
        /// <param name="args">Arguments</param>
        public abstract 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="eventName">Name of the event.</param>
        public virtual void OnEnqueue(MachineId machineId, string eventName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<EnqueueLog> Machine '{machineId}' enqueued event '{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 virtual void OnDequeue(MachineId machineId, string currentStateName, string eventName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<DequeueLog> Machine '{machineId}' in state '{currentStateName}' dequeued event '{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 virtual void OnDefault(MachineId machineId, string currentStateName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<DefaultLog> Machine '{machineId}' in state '{currentStateName}' is executing the default handler.");
            }
        }

        /// <summary>
        /// Called when a machine transitions states via a 'goto'.
        /// </summary>
        /// <param name="machineId">Id of the machine.</param>
        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
        /// <param name="newStateName">The target state of goto.</param>
        public void OnGoto(MachineId machineId, string currentStateName, string newStateName)
        {
            if(this.IsVerbose)
            {
                this.WriteLine($"<GotoLog> Machine '{machineId}' is transitioning from state '{currentStateName}' to state '{newStateName}'.");
            }
        }


        /// <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 virtual void OnPush(MachineId machineId, string currentStateName, string newStateName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<PushLog> Machine '{0}' pushed from state '{1}' to state '{2}'.",
                    machineId, currentStateName, newStateName);
            }
        }

        /// <summary>
        /// Called when a machine has been popped from a state.<commit_msg>Fix #272<commit_after>﻿//-----------------------------------------------------------------------
// <copyright file="StateMachineLogger.cs">
//      Copyright (c) Microsoft Corporation. All rights reserved.
// 
//      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
//      EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
//      MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
//      IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
//      CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
//      TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
//      SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
// </copyright>
//-----------------------------------------------------------------------

using Microsoft.PSharp.Utilities;
using System;

namespace Microsoft.PSharp.IO
{
    /// <summary>
    /// An implementation of <see cref="ILogger"/> that by default passes all logging commands to the variants
    /// of the <see cref="Write(string)"/> method if the <see cref="Configuration.Verbose"/> option is set to
    /// >= <see cref="LoggingVerbosity"/>. This class may be subclassed and its methods overridden.
    /// </summary>
    public abstract class StateMachineLogger : ILogger
    {
        /// <summary>
        /// The configuration that sets the logging verbosity.
        /// </summary>
        public Configuration Configuration { get; set; }

        /// <summary>
        /// The minimum logging verbosity level. If <see cref="Configuration.Verbose"/> is >=
        /// <see cref="LoggingVerbosity"/>, then messages are logged (0 logs all messages).
        /// </summary>
        public int LoggingVerbosity { get; set; } = 2;

        /// <summary>
        /// Convenience method to indicate whether <see cref="Configuration.Verbose"/> is at or
        /// above <see cref="LoggingVerbosity"/>.
        /// </summary>
        public bool IsVerbose => this.Configuration.Verbose >= LoggingVerbosity;

        /// <summary>
        /// Constructs the logger. The logger will be assigned the Runtime's Configuration
        /// object when it is passed to <see cref="PSharpRuntime.SetLogger(ILogger)"/>.
        /// </summary>
        /// <param name="loggingVerbosity">The initial logging verbosity level.</param>
        public StateMachineLogger(int loggingVerbosity = 2)
        {
            this.LoggingVerbosity = loggingVerbosity;
        }

        /// <summary>
        /// Writes the specified string value.
        /// </summary>
        /// <param name="value">Text</param>
        public abstract void Write(string value);

        /// <summary>
        /// Writes the text representation of the specified array of objects.
        /// </summary>
        /// <param name="format">Text</param>
        /// <param name="args">Arguments</param>
        public abstract void Write(string format, params object[] args);

        /// <summary>
        /// Writes the specified string value, followed by the
        /// current line terminator.
        /// </summary>
        /// <param name="value">Text</param>
        public abstract void WriteLine(string value);

        /// <summary>
        /// Writes the text representation of the specified array of objects,
        /// followed by the current line terminator.
        /// </summary>
        /// <param name="format">Text</param>
        /// <param name="args">Arguments</param>
        public abstract 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="eventName">Name of the event.</param>
        public virtual void OnEnqueue(MachineId machineId, string eventName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<EnqueueLog> Machine '{machineId}' enqueued event '{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 virtual void OnDequeue(MachineId machineId, string currentStateName, string eventName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<DequeueLog> Machine '{machineId}' in state '{currentStateName}' dequeued event '{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 virtual void OnDefault(MachineId machineId, string currentStateName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine($"<DefaultLog> Machine '{machineId}' in state '{currentStateName}' is executing the default handler.");
            }
        }

        /// <summary>
        /// Called when a machine transitions states via a 'goto'.
        /// </summary>
        /// <param name="machineId">Id of the machine.</param>
        /// <param name="currentStateName">The name of the current state of <paramref name="machineId"/>, if any.</param>
        /// <param name="newStateName">The target state of goto.</param>
        public void OnGoto(MachineId machineId, string currentStateName, string newStateName)
        {
            if(this.IsVerbose)
            {
                this.WriteLine($"<GotoLog> Machine '{machineId}' is transitioning from state '{currentStateName}' to state '{newStateName}'.");
            }
        }


        /// <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 virtual void OnPush(MachineId machineId, string currentStateName, string newStateName)
        {
            if (this.IsVerbose)
            {
                this.WriteLine("<PushLog> Machine '{0}' pushed from state '{1}' to state '{2}'.",
                    machineId, currentStateName, newStateName);
            }
        }

        /// <summary>
        /// Called when a machine has been popped from a state.
{'fraction_non_alphanumeric': 0.14078228357779696, 'fraction_numerical': 0.0010785159620362382, 'mean_word_length': 1.977097602739726, 'pattern_counts': {'":': 0, '<': 179, '<?xml version=': 0, '>': 187, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3007325', 'n_tokens_mistral': 3492, 'n_tokens_neox': 3397, 'n_words': 1228}