<commit_before>﻿//-----------------------------------------------------------------------
// <copyright file="LivenessChecker.cs" company="Microsoft">
//      Copyright (c) Microsoft Corporation. All rights reserved.
// 
//      THIS CODE AND INFORMATION ARE PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, 
//      EITHER EXPRESSED OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES 
//      OF MERCHANTABILITY AND/OR FITNESS FOR A PARTICULAR PURPOSE.
// ----------------------------------------------------------------------------------
//      The example companies, organizations, products, domain names,
//      e-mail addresses, logos, people, places, and events depicted
//      herein are fictitious.  No association with any real company,
//      organization, product, domain name, email address, logo, person,
//      places, or events is intended or should be inferred.
// </copyright>
//-----------------------------------------------------------------------

using System;
using System.Collections.Generic;
using System.Linq;

using Microsoft.PSharp.StateCaching;
using Microsoft.PSharp.Tooling;

namespace Microsoft.PSharp.Scheduling
{
    /// <summary>
    /// Class implementing the P# liveness property checker.
    /// </summary>
    internal sealed class LivenessChecker
    {
        #region fields

        /// <summary>
        /// List of monitors in the program.
        /// </summary>
        private List<Monitor> Monitors;

        #endregion

        #region internal methods

        /// <summary>
        /// Constructor.
        /// </summary>
        internal LivenessChecker()
        {
            this.Monitors = new List<Monitor>();
        }

        /// <summary>
        /// Registers a new monitor.
        /// </summary>
        /// <param name="monitor">Monitor</param>
        internal void RegisterMonitor(Monitor monitor)
        {
            this.Monitors.Add(monitor);
        }

        /// <summary>
        /// Runs the liveness checker and reports any liveness property violations.
        /// Requires the P# program to have reached quiescence.
        /// </summary>
        internal void Run()
        {
            if (!Configuration.CheckLiveness)
            {
                return;
            }

            foreach (var monitor in this.Monitors)
            {
                var stateName = "";
                if (monitor.IsInHotState(out stateName))
                {
                    string message = Output.Format("Monitor '{0}' detected liveness property " +
                        "violation in hot state '{1}'.", monitor.GetType().Name, stateName);
                    PSharpRuntime.BugFinder.NotifyAssertionFailure(message, false);
                }
            }
        }

        /// <summary>
        /// Checks liveness at a trace cycle.
        /// </summary>
        /// <param name="root">Cycle start</param>
        internal void CheckLivenessAtTraceCycle(Fingerprint root, Trace trace)
        {
            var cycle = new List<TraceStep>();

            do
            {
                Output.Debug(DebugType.Liveness, "<LivenessDebug> Cycle contains {0}.",
                    trace.Peek().Fingerprint.ToString());
                cycle.Add(trace.Pop());
            }
            while (trace.Peek() != null && !trace.Peek().Fingerprint.Equals(root));
            
            if (!this.IsSchedulingFair(cycle))
            {
                Output.Debug(DebugType.Liveness, "<LivenessDebug> Scheduling in cycle is unfair.");
                return;
            }
            else if (!this.IsNondeterminismFair(cycle))
            {
                Output.Debug(DebugType.Liveness, "<LivenessDebug> Nondeterminism in cycle is unfair.");
                return;
            }

            Output.Debug(DebugType.Liveness, "<LivenessDebug> Cycle execution is fair.");

            var hotMonitors = this.GetHotMonitors(cycle);
            foreach (var monitor in hotMonitors)
            {
                string message = Output.Format("Monitor '{0}' detected infinite execution that " +
                    "violates a liveness property.", monitor.GetType().Name);
                PSharpRuntime.BugFinder.NotifyAssertionFailure(message, false);
            }

            if (Configuration.DepthBound == 0)
            {
                PSharpRuntime.BugFinder.Stop();
            }
        }

        /// <summary>
        /// Returns the monitor status.
        /// </summary>
        /// <returns>Monitor status</returns>
        internal Dictionary<Monitor, MonitorStatus> GetMonitorStatus()
        {
            var monitors = new Dictionary<Monitor, MonitorStatus>();
            foreach (var monitor in this.Monitors)
            {
                MonitorStatus status = MonitorStatus.None;
                if (monitor.IsInHotState())
                {
                    status = MonitorStatus.Hot;
                }
                else if (monitor.IsInColdState())
                {
                    status = MonitorStatus.Cold;
                }<commit_msg>bug fix in liveness checker<commit_after>﻿//-----------------------------------------------------------------------
// <copyright file="LivenessChecker.cs" company="Microsoft">
//      Copyright (c) Microsoft Corporation. All rights reserved.
// 
//      THIS CODE AND INFORMATION ARE PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, 
//      EITHER EXPRESSED OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES 
//      OF MERCHANTABILITY AND/OR FITNESS FOR A PARTICULAR PURPOSE.
// ----------------------------------------------------------------------------------
//      The example companies, organizations, products, domain names,
//      e-mail addresses, logos, people, places, and events depicted
//      herein are fictitious.  No association with any real company,
//      organization, product, domain name, email address, logo, person,
//      places, or events is intended or should be inferred.
// </copyright>
//-----------------------------------------------------------------------

using System;
using System.Collections.Generic;
using System.Linq;

using Microsoft.PSharp.StateCaching;
using Microsoft.PSharp.Tooling;

namespace Microsoft.PSharp.Scheduling
{
    /// <summary>
    /// Class implementing the P# liveness property checker.
    /// </summary>
    internal sealed class LivenessChecker
    {
        #region fields

        /// <summary>
        /// List of monitors in the program.
        /// </summary>
        private List<Monitor> Monitors;

        #endregion

        #region internal methods

        /// <summary>
        /// Constructor.
        /// </summary>
        internal LivenessChecker()
        {
            this.Monitors = new List<Monitor>();
        }

        /// <summary>
        /// Registers a new monitor.
        /// </summary>
        /// <param name="monitor">Monitor</param>
        internal void RegisterMonitor(Monitor monitor)
        {
            this.Monitors.Add(monitor);
        }

        /// <summary>
        /// Runs the liveness checker and reports any liveness property violations.
        /// Requires the P# program to have reached quiescence.
        /// </summary>
        internal void Run()
        {
            if (!Configuration.CheckLiveness)
            {
                return;
            }

            foreach (var monitor in this.Monitors)
            {
                var stateName = "";
                if (monitor.IsInHotState(out stateName))
                {
                    string message = Output.Format("Monitor '{0}' detected liveness property " +
                        "violation in hot state '{1}'.", monitor.GetType().Name, stateName);
                    PSharpRuntime.BugFinder.NotifyAssertionFailure(message, false);
                }
            }
        }

        /// <summary>
        /// Checks liveness at a trace cycle.
        /// </summary>
        /// <param name="root">Cycle start</param>
        internal void CheckLivenessAtTraceCycle(Fingerprint root, Trace trace)
        {
            var cycle = new List<TraceStep>();

            do
            {
                Output.Debug(DebugType.Liveness, "<LivenessDebug> Cycle contains {0}.",
                    trace.Peek().Fingerprint.ToString());
                cycle.Add(trace.Pop());
            }
            while (trace.Peek() != null && !trace.Peek().Fingerprint.Equals(root));
            
            if (!this.IsSchedulingFair(cycle))
            {
                Output.Debug(DebugType.Liveness, "<LivenessDebug> Scheduling in cycle is unfair.");
                return;
            }
            else if (!this.IsNondeterminismFair(cycle))
            {
                Output.Debug(DebugType.Liveness, "<LivenessDebug> Nondeterminism in cycle is unfair.");
                return;
            }

            Output.Debug(DebugType.Liveness, "<LivenessDebug> Cycle execution is fair.");

            var hotMonitors = this.GetHotMonitors(cycle);
            foreach (var monitor in hotMonitors)
            {
                string message = Output.Format("Monitor '{0}' detected infinite execution that " +
                    "violates a liveness property.", monitor.GetType().Name);
                PSharpRuntime.BugFinder.NotifyAssertionFailure(message, false);
            }

            if (Configuration.DepthBound == 0 || hotMonitors.Count > 0)
            {
                PSharpRuntime.BugFinder.Stop();
            }
        }

        /// <summary>
        /// Returns the monitor status.
        /// </summary>
        /// <returns>Monitor status</returns>
        internal Dictionary<Monitor, MonitorStatus> GetMonitorStatus()
        {
            var monitors = new Dictionary<Monitor, MonitorStatus>();
            foreach (var monitor in this.Monitors)
            {
                MonitorStatus status = MonitorStatus.None;
                if (monitor.IsInHotState())
                {
                    status = MonitorStatus.Hot;
                }
                else if (monitor.IsInColdState())
                {
                    status = MonitorStatus.Cold;
                }
{'fraction_non_alphanumeric': 0.14497302599313389, 'fraction_numerical': 0.0010789602746444336, 'mean_word_length': 1.4392344497607656, 'pattern_counts': {'":': 0, '<': 65, '<?xml version=': 0, '>': 66, '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': '7244202', 'n_tokens_mistral': 2466, 'n_tokens_neox': 2327, 'n_words': 650}