From e50bd3b46aff87728407b5bdf308738ce727107c Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Thu, 26 Jan 2023 13:41:25 -0800 Subject: [PATCH] deterministic creation sequence id for operations (#448) --- .../Logging/ActorRuntimeLogTextFormatter.cs | 2 +- Source/Core/Coverage/CoverageInfo.cs | 25 ++ Source/Core/Runtime/CoyoteRuntime.cs | 95 +++-- Source/Core/Runtime/ExecutionTrace.cs | 301 +++++++++----- .../Runtime/Operations/ControlledOperation.cs | 77 ++++ .../Runtime/Scheduling/OperationScheduler.cs | 6 +- .../Core/Testing/Interleaving/DFSStrategy.cs | 8 +- .../Interleaving/DelayBoundingStrategy.cs | 4 +- .../Interleaving/InterleavingStrategy.cs | 73 ++-- .../Interleaving/PrioritizationStrategy.cs | 2 +- .../ProbabilisticRandomStrategy.cs | 2 +- .../Testing/Interleaving/QLearningStrategy.cs | 8 +- .../Passes/Rewriting/RewritingPass.cs | 2 +- .../Types/MethodBodyTypeRewritingPass.cs | 10 +- .../Rewriting/Types/TypeRewritingPass.cs | 2 +- .../Types/Threading/SemaphoreSlim.cs | 4 +- .../SystematicTesting/Reports/TestReport.cs | 116 +++--- .../SystematicTesting/Reports/TraceReport.cs | 68 ++-- .../Test/SystematicTesting/TestMethodInfo.cs | 2 +- .../Exploration/ExecutionTraceTests.cs | 375 +++++++++--------- .../Logging/TestingEngineLoggingTests.cs | 24 +- 21 files changed, 703 insertions(+), 503 deletions(-) diff --git a/Source/Actors/Logging/ActorRuntimeLogTextFormatter.cs b/Source/Actors/Logging/ActorRuntimeLogTextFormatter.cs index 81a5e14b..eae6363c 100644 --- a/Source/Actors/Logging/ActorRuntimeLogTextFormatter.cs +++ b/Source/Actors/Logging/ActorRuntimeLogTextFormatter.cs @@ -307,7 +307,7 @@ namespace Microsoft.Coyote.Actors else { string[] eventNameArray = new string[eventTypes.Length - 1]; - for (int i = 0; i < eventTypes.Length - 2; i++) + for (int i = 0; i < eventTypes.Length - 2; ++i) { eventNameArray[i] = eventTypes[i].FullName; } diff --git a/Source/Core/Coverage/CoverageInfo.cs b/Source/Core/Coverage/CoverageInfo.cs index 4cb2ad86..312071ed 100644 --- a/Source/Core/Coverage/CoverageInfo.cs +++ b/Source/Core/Coverage/CoverageInfo.cs @@ -53,12 +53,23 @@ namespace Microsoft.Coyote.Coverage [DataMember] public Dictionary> SchedulingPointStackTraces { get; private set; } + /// + /// Set of explored paths represented as ordered operations identified by their creation sequence ids. + /// + [DataMember] + public HashSet ExploredPaths { get; private set; } + /// /// Set of visited program states represented as hashes. /// [DataMember] public HashSet VisitedStates { get; private set; } + /// + /// Set of encountered operation creation sequence ids. + /// + public HashSet OperationSequenceIds { get; private set; } + /// /// Initializes a new instance of the class. /// @@ -68,7 +79,9 @@ namespace Microsoft.Coyote.Coverage this.MonitorsToStates = new Dictionary>(); this.RegisteredMonitorEvents = new Dictionary>(); this.SchedulingPointStackTraces = new Dictionary>(); + this.ExploredPaths = new HashSet(); this.VisitedStates = new HashSet(); + this.OperationSequenceIds = new HashSet(); } /// @@ -141,11 +154,21 @@ namespace Microsoft.Coyote.Coverage } } + /// + /// Declares a new explored execution path. + /// + internal void DeclareExploredExecutionPath(string path) => this.ExploredPaths.Add(path); + /// /// Declares a new visited state. /// internal void DeclareVisitedState(int state) => this.VisitedStates.Add(state); + /// + /// Declares a new operation creation sequence id. + /// + internal void DeclareOperationSequenceId(ulong sequenceId) => this.OperationSequenceIds.Add(sequenceId); + /// /// Loads the coverage info XML file into a object of the specified type. /// @@ -246,7 +269,9 @@ namespace Microsoft.Coyote.Coverage } } + this.ExploredPaths.UnionWith(coverageInfo.ExploredPaths); this.VisitedStates.UnionWith(coverageInfo.VisitedStates); + this.OperationSequenceIds.UnionWith(coverageInfo.OperationSequenceIds); } } } diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 0024ceef..551ef262 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -678,8 +678,11 @@ namespace Microsoft.Coyote.Runtime this.PendingStartOperationMap.Add(op, new ManualResetEventSlim(false)); } - this.LogWriter.LogDebug("[coyote::debug] Created operation '{0}' of group '{1}' on thread '{2}'.", - op.Name, op.Group, Thread.CurrentThread.ManagedThreadId); + // Register the operation creation sequence id for coverage. + this.CoverageInfo.DeclareOperationSequenceId(op.SequenceId); + + this.LogWriter.LogDebug("[coyote::debug] Created operation {0} on thread '{1}'.", + op.DebugInfo, Thread.CurrentThread.ManagedThreadId); } } @@ -697,8 +700,8 @@ namespace Microsoft.Coyote.Runtime this.SetCurrentExecutionContext(op); using (SynchronizedSection.Enter(this.RuntimeLock)) { - this.LogWriter.LogDebug("[coyote::debug] Started operation '{0}' of group '{1}' on thread '{2}'.", - op.Name, op.Group, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Started operation {0} on thread '{1}'.", + op.DebugInfo, Thread.CurrentThread.ManagedThreadId); op.Status = OperationStatus.Enabled; if (this.SchedulingPolicy is SchedulingPolicy.Interleaving) { @@ -733,8 +736,8 @@ namespace Microsoft.Coyote.Runtime var pendingOp = this.PendingStartOperationMap.First(); while (pendingOp.Key.Status is OperationStatus.None) { - this.LogWriter.LogDebug("[coyote::debug] Sleeping thread '{0}' until operation '{1}' of group '{2}' starts.", - Thread.CurrentThread.ManagedThreadId, pendingOp.Key.Name, pendingOp.Key.Group); + this.LogWriter.LogDebug("[coyote::debug] Sleeping thread '{0}' until operation {1} starts.", + Thread.CurrentThread.ManagedThreadId, pendingOp.Key.DebugInfo); using (SynchronizedSection.Exit(this.RuntimeLock)) { try @@ -771,15 +774,15 @@ namespace Microsoft.Coyote.Runtime // Do not allow the operation to wake up, unless its currently scheduled and enabled or the runtime stopped running. while (!(op == this.ScheduledOperation && op.Status is OperationStatus.Enabled) && this.ExecutionStatus is ExecutionStatus.Running) { - this.LogWriter.LogDebug("[coyote::debug] Sleeping operation '{0}' of group '{1}' on thread '{2}'.", - op.Name, op.Group, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Sleeping operation {0} on thread '{1}'.", + op.DebugInfo, Thread.CurrentThread.ManagedThreadId); using (SynchronizedSection.Exit(this.RuntimeLock)) { op.WaitSignal(); } - this.LogWriter.LogDebug("[coyote::debug] Waking up operation '{0}' of group '{1}' on thread '{2}'.", - op.Name, op.Group, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Waking up operation {0} on thread '{1}'.", + op.DebugInfo, Thread.CurrentThread.ManagedThreadId); } } } @@ -798,8 +801,8 @@ namespace Microsoft.Coyote.Runtime current ??= this.GetExecutingOperation(); while (current != null && !condition() && this.ExecutionStatus is ExecutionStatus.Running) { - this.LogWriter.LogDebug("[coyote::debug] Operation '{0}' of group '{1}' is waiting for {2} on thread '{3}'.", - current.Name, current.Group, debugMsg ?? "condition to get resolved", Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Operation {0} is waiting for {1} on thread '{2}'.", + current.DebugInfo, debugMsg ?? "condition to get resolved", Thread.CurrentThread.ManagedThreadId); // TODO: can we identify when the dependency is uncontrolled? current.PauseWithDependency(condition, isConditionControlled); this.ScheduleNextOperation(current, SchedulingPointType.Pause); @@ -862,8 +865,8 @@ namespace Microsoft.Coyote.Runtime // now been resolved, so resume it on this uncontrolled thread. current = this.ScheduledOperation; type = this.LastPostponedSchedulingPoint.Value; - this.LogWriter.LogDebug("[coyote::debug] Resuming scheduling point '{0}' of operation '{1}' in uncontrolled thread '{2}'.", - type, current, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Resuming scheduling point '{0}' of operation {1} in uncontrolled thread '{2}'.", + type, current.DebugInfo, Thread.CurrentThread.ManagedThreadId); } else if (type is SchedulingPointType.Create || type is SchedulingPointType.ContinueWith) { @@ -899,14 +902,14 @@ namespace Microsoft.Coyote.Runtime isSuppressible && current.Status is OperationStatus.Enabled) { // Suppress the scheduling point. - this.LogWriter.LogDebug("[coyote::debug] Operation '{0}' of group '{1}' suppressed scheduling point '{2}'.", - current.Name, current.Group, type); + this.LogWriter.LogDebug("[coyote::debug] Operation {0} suppressed scheduling point '{1}'.", + current.DebugInfo, type); return false; } this.LogWriter.LogDebug( - "[coyote::debug] Operation '{0}' of group '{1}' reached scheduling point '{2}' at execution step '{3}' on thread '{4}'.", - current.Name, current.Group, type, this.Scheduler.StepCount, Thread.CurrentThread.ManagedThreadId); + "[coyote::debug] Operation {0} reached scheduling point '{1}' at execution step '{2}' on thread '{3}'.", + current.DebugInfo, type, this.Scheduler.StepCount, Thread.CurrentThread.ManagedThreadId); this.Assert(!this.IsSpecificationInvoked, "Executing a specification monitor must be atomic."); // Checks if the scheduling steps bound has been reached. @@ -931,8 +934,8 @@ namespace Microsoft.Coyote.Runtime // If uncontrolled concurrency is detected, then do not check for deadlocks directly, // but instead leave it to the background deadlock detection timer and postpone the // scheduling point, which might get resolved from an uncontrolled thread. - this.LogWriter.LogDebug("[coyote::debug] Postponing scheduling point '{0}' of operation '{1}' due to potential deadlock.", - type, current); + this.LogWriter.LogDebug("[coyote::debug] Postponing scheduling point '{0}' of operation {1} due to potential deadlock.", + type, current.DebugInfo); this.LastPostponedSchedulingPoint = type; this.PauseOperation(current); return false; @@ -960,8 +963,8 @@ namespace Microsoft.Coyote.Runtime return false; } - this.LogWriter.LogDebug("[coyote::debug] Scheduling operation '{0}' of group '{1}' from thread '{2}'.", - next.Name, next.Group, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Scheduling operation {0} from thread '{1}'.", + next.DebugInfo, Thread.CurrentThread.ManagedThreadId); bool isNextOperationScheduled = current != next; if (isNextOperationScheduled) { @@ -1001,8 +1004,8 @@ namespace Microsoft.Coyote.Runtime { // Choose the next delay to inject. The value is in milliseconds. int delay = this.GetNondeterministicDelay(current, (int)this.Configuration.MaxFuzzingDelay); - this.LogWriter.LogDebug("[coyote::debug] Delaying operation '{0}' on thread '{1}' by {2}ms.", - current.Name, Thread.CurrentThread.ManagedThreadId, delay); + this.LogWriter.LogDebug("[coyote::debug] Delaying operation {0} on thread '{1}' by {2}ms.", + current.DebugInfo, Thread.CurrentThread.ManagedThreadId, delay); // Only sleep the executing operation if a non-zero delay was chosen. if (delay > 0) @@ -1028,8 +1031,8 @@ namespace Microsoft.Coyote.Runtime op.ExecuteContinuations(); using (SynchronizedSection.Enter(this.RuntimeLock)) { - this.LogWriter.LogDebug("[coyote::debug] Completed operation '{0}' of group '{1}' on thread '{2}'.", - op.Name, op.Group, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Completed operation {0} on thread '{1}'.", + op.DebugInfo, Thread.CurrentThread.ManagedThreadId); op.Status = OperationStatus.Completed; } } @@ -1045,8 +1048,8 @@ namespace Microsoft.Coyote.Runtime { if (op.Status is OperationStatus.Completed) { - this.LogWriter.LogDebug("[coyote::debug] Resetting operation '{0}' of group '{1}' from thread '{2}'.", - op.Name, op.Group, Thread.CurrentThread.ManagedThreadId); + this.LogWriter.LogDebug("[coyote::debug] Resetting operation {0} from thread '{1}'.", + op.DebugInfo, Thread.CurrentThread.ManagedThreadId); op.Status = OperationStatus.None; if (this.SchedulingPolicy is SchedulingPolicy.Interleaving) { @@ -1244,8 +1247,7 @@ namespace Microsoft.Coyote.Runtime this.TryEnableOperation(op); if (previousStatus == op.Status) { - this.LogWriter.LogDebug("[coyote::debug] Operation '{0}' of group '{1}' has status '{2}'.", - op.Name, op.Group, op.Status); + this.LogWriter.LogDebug("[coyote::debug] Operation {0} has status '{1}'.", op.DebugInfo, op.Status); if (op.IsPaused && op.IsDependencyUncontrolled) { if (op.IsRoot) @@ -1260,8 +1262,8 @@ namespace Microsoft.Coyote.Runtime } else { - this.LogWriter.LogDebug("[coyote::debug] Operation '{0}' of group '{1}' changed status from '{2}' to '{3}'.", - op.Name, op.Group, previousStatus, op.Status); + this.LogWriter.LogDebug("[coyote::debug] Operation {0} changed status from '{1}' to '{2}'.", + op.DebugInfo, previousStatus, op.Status); statusChanges++; } } @@ -1400,6 +1402,9 @@ namespace Microsoft.Coyote.Runtime /// Returns the currently executing , /// or null if no such operation is executing. /// + /// + /// Invoking this method checks if the current thread is uncontrolled or not. + /// internal ControlledOperation GetExecutingOperation() { using (SynchronizedSection.Enter(this.RuntimeLock)) @@ -1418,6 +1423,9 @@ namespace Microsoft.Coyote.Runtime /// Returns the currently executing of the /// specified type, or null if no such operation is executing. /// + /// + /// Invoking this method checks if the current thread is uncontrolled or not. + /// internal TControlledOperation GetExecutingOperation() where TControlledOperation : ControlledOperation { @@ -1433,6 +1441,18 @@ namespace Microsoft.Coyote.Runtime } } + /// + /// Returns the currently executing , + /// or null if no such operation is executing. + /// + internal ControlledOperation GetExecutingOperationUnsafe() + { + using (SynchronizedSection.Enter(this.RuntimeLock)) + { + return ExecutingOperation; + } + } + /// /// Tries to return the currently executing , /// or false if no such operation is executing. @@ -1840,7 +1860,7 @@ namespace Microsoft.Coyote.Runtime if (pausedOperations.Count > 0) { - for (int idx = 0; idx < pausedOperations.Count; idx++) + for (int idx = 0; idx < pausedOperations.Count; ++idx) { msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOperations[idx].Name)); if (idx == pausedOperations.Count - 2) @@ -1859,7 +1879,7 @@ namespace Microsoft.Coyote.Runtime if (pausedOnResources.Count > 0) { - for (int idx = 0; idx < pausedOnResources.Count; idx++) + for (int idx = 0; idx < pausedOnResources.Count; ++idx) { msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOnResources[idx].Name)); if (idx == pausedOnResources.Count - 2) @@ -1879,7 +1899,7 @@ namespace Microsoft.Coyote.Runtime if (pausedOnReceiveOperations.Count > 0) { - for (int idx = 0; idx < pausedOnReceiveOperations.Count; idx++) + for (int idx = 0; idx < pausedOnReceiveOperations.Count; ++idx) { msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOnReceiveOperations[idx].Name)); if (idx == pausedOnReceiveOperations.Count - 2) @@ -2364,7 +2384,7 @@ namespace Microsoft.Coyote.Runtime #else string[] lines = exception.ToString().Split(new[] { Environment.NewLine }, StringSplitOptions.None); #endif - for (int i = 0; i < lines.Length; i++) + for (int i = 0; i < lines.Length; ++i) { if (lines[i].StartsWith(" at Microsoft.Coyote.Rewriting", StringComparison.Ordinal)) { @@ -2538,6 +2558,9 @@ namespace Microsoft.Coyote.Runtime this.Id, this.Scheduler.GetStrategyName()); } + // Register the explored execution path for coverage. + this.CoverageInfo.DeclareExploredExecutionPath(this.Scheduler.Trace.ToString()); + this.ExecutionStatus = status; this.CancellationSource.Cancel(); diff --git a/Source/Core/Runtime/ExecutionTrace.cs b/Source/Core/Runtime/ExecutionTrace.cs index b764e707..0dba0295 100644 --- a/Source/Core/Runtime/ExecutionTrace.cs +++ b/Source/Core/Runtime/ExecutionTrace.cs @@ -4,6 +4,7 @@ using System; using System.Collections; using System.Collections.Generic; +using System.Text; namespace Microsoft.Coyote.Runtime { @@ -49,29 +50,47 @@ namespace Microsoft.Coyote.Runtime internal static ExecutionTrace Create() => new ExecutionTrace(); /// - /// Adds a scheduling choice. + /// Adds a scheduling decision. /// - internal void AddSchedulingChoice(ulong scheduledOperationId, SchedulingPointType sp) + internal void AddSchedulingDecision(ControlledOperation current, SchedulingPointType sp, ControlledOperation next) => + this.AddSchedulingDecision(current.Id, current.SequenceId, sp, next.Id, next.SequenceId); + + /// + /// Adds a scheduling decision. + /// + internal void AddSchedulingDecision(ulong current, ulong currentSeqId, SchedulingPointType sp, ulong next, ulong nextSeqId) { - var scheduleStep = Step.CreateSchedulingChoice(this.Length, scheduledOperationId, sp); + var scheduleStep = new SchedulingStep(this.Length, current, currentSeqId, sp, next, nextSeqId); this.Push(scheduleStep); } /// - /// Adds a nondeterministic boolean choice. + /// Adds a nondeterministic boolean decision. /// - internal void AddNondeterministicBooleanChoice(bool choice, SchedulingPointType sp) + internal void AddNondeterministicBooleanDecision(ControlledOperation current, bool value) => + this.AddNondeterministicBooleanDecision(current.Id, current.SequenceId, value); + + /// + /// Adds a nondeterministic boolean decision. + /// + internal void AddNondeterministicBooleanDecision(ulong current, ulong currentSeqId, bool value) { - var scheduleStep = Step.CreateNondeterministicBooleanChoice(this.Length, choice, sp); + var scheduleStep = new BooleanChoiceStep(this.Length, current, currentSeqId, value); this.Push(scheduleStep); } /// - /// Adds a nondeterministic integer choice. + /// Adds a nondeterministic integer decision. /// - internal void AddNondeterministicIntegerChoice(int choice, SchedulingPointType sp) + internal void AddNondeterministicIntegerDecision(ControlledOperation current, int value) => + this.AddNondeterministicIntegerDecision(current.Id, current.SequenceId, value); + + /// + /// Adds a nondeterministic integer decision. + /// + internal void AddNondeterministicIntegerDecision(ulong current, ulong currentSeqId, int value) { - var scheduleStep = Step.CreateNondeterministicIntegerChoice(this.Length, choice, sp); + var scheduleStep = new IntegerChoiceStep(this.Length, current, currentSeqId, value); this.Push(scheduleStep); } @@ -143,17 +162,18 @@ namespace Microsoft.Coyote.Runtime { foreach (var step in trace.Steps) { - if (step.Kind is DecisionKind.SchedulingChoice) + if (step is SchedulingStep schedulingStep) { - this.AddSchedulingChoice(step.ScheduledOperationId, step.SchedulingPoint); + this.AddSchedulingDecision(schedulingStep.Current, schedulingStep.CurrentSequenceId, schedulingStep.SchedulingPoint, + schedulingStep.Value, schedulingStep.SequenceId); } - else if (step.Kind is DecisionKind.NondeterministicChoice && step.BooleanChoice.HasValue) + else if (step is BooleanChoiceStep boolChoiceStep) { - this.AddNondeterministicBooleanChoice(step.BooleanChoice.Value, step.SchedulingPoint); + this.AddNondeterministicBooleanDecision(boolChoiceStep.Current, boolChoiceStep.CurrentSequenceId, boolChoiceStep.Value); } - else if (step.Kind is DecisionKind.NondeterministicChoice && step.IntegerChoice.HasValue) + else if (step is IntegerChoiceStep intChoiceStep) { - this.AddNondeterministicIntegerChoice(step.IntegerChoice.Value, step.SchedulingPoint); + this.AddNondeterministicIntegerDecision(intChoiceStep.Current, intChoiceStep.CurrentSequenceId, intChoiceStep.Value); } } @@ -185,17 +205,18 @@ namespace Microsoft.Coyote.Runtime while (appendIndex < trace.Length) { Step step = trace[appendIndex]; - if (step.Kind is DecisionKind.SchedulingChoice) + if (step is SchedulingStep schedulingStep) { - this.AddSchedulingChoice(step.ScheduledOperationId, step.SchedulingPoint); + this.AddSchedulingDecision(schedulingStep.Current, schedulingStep.CurrentSequenceId, schedulingStep.SchedulingPoint, + schedulingStep.Value, schedulingStep.SequenceId); } - else if (step.Kind is DecisionKind.NondeterministicChoice && step.BooleanChoice.HasValue) + else if (step is BooleanChoiceStep boolChoiceStep) { - this.AddNondeterministicBooleanChoice(step.BooleanChoice.Value, step.SchedulingPoint); + this.AddNondeterministicBooleanDecision(boolChoiceStep.Current, boolChoiceStep.CurrentSequenceId, boolChoiceStep.Value); } - else if (step.Kind is DecisionKind.NondeterministicChoice && step.IntegerChoice.HasValue) + else if (step is IntegerChoiceStep intChoiceStep) { - this.AddNondeterministicIntegerChoice(step.IntegerChoice.Value, step.SchedulingPoint); + this.AddNondeterministicIntegerDecision(intChoiceStep.Current, intChoiceStep.CurrentSequenceId, intChoiceStep.Value); } appendIndex++; @@ -210,18 +231,28 @@ namespace Microsoft.Coyote.Runtime internal void Clear() => this.Steps.Clear(); /// - /// The kind of decision taken during an execution step. + /// Returns a string that represents the execution trace with all operations + /// identified by their creation sequence ids. /// - internal enum DecisionKind + public override string ToString() { - SchedulingChoice = 0, - NondeterministicChoice + var sb = new StringBuilder(); + for (int idx = 0; idx < this.Length; ++idx) + { + sb.Append(this.Steps[idx].ToSequenceString()); + if (idx < this.Length - 1) + { + sb.Append(";"); + } + } + + return sb.ToString(); } /// /// Contains metadata related to a single execution step. /// - internal sealed class Step : IEquatable, IComparable + internal abstract class Step : IEquatable, IComparable { /// /// The unique index of this execution step. @@ -229,32 +260,14 @@ namespace Microsoft.Coyote.Runtime internal int Index; /// - /// The kind of controlled decision taken in this execution step. + /// The id of the currently executing operation. /// - internal DecisionKind Kind { get; private set; } + internal ulong Current; /// - /// The type of scheduling point encountered in this execution step. + /// The creation sequence id of the currently executing operation. /// - internal SchedulingPointType SchedulingPoint { get; private set; } - - /// - /// The id of the scheduled operation. Only relevant if this is - /// a regular execution step. - /// - internal ulong ScheduledOperationId; - - /// - /// The non-deterministic boolean choice value. Only relevant if - /// this is a choice execution step. - /// - internal bool? BooleanChoice; - - /// - /// The non-deterministic integer choice value. Only relevant if - /// this is a choice execution step. - /// - internal int? IntegerChoice; + internal ulong CurrentSequenceId; /// /// The previous execution step. @@ -267,74 +280,27 @@ namespace Microsoft.Coyote.Runtime internal Step Next; /// - /// Creates an execution step. + /// Initializes a new instance of the class. /// - internal static Step CreateSchedulingChoice(int index, ulong scheduledOperationId, SchedulingPointType sp) + protected Step(int index, ulong current, ulong currentSeqId) { - var scheduleStep = new Step(); - scheduleStep.Index = index; - scheduleStep.Kind = DecisionKind.SchedulingChoice; - scheduleStep.SchedulingPoint = sp; - scheduleStep.ScheduledOperationId = scheduledOperationId; - scheduleStep.BooleanChoice = null; - scheduleStep.IntegerChoice = null; - scheduleStep.Previous = null; - scheduleStep.Next = null; - return scheduleStep; + this.Index = index; + this.Current = current; + this.CurrentSequenceId = currentSeqId; + this.Previous = null; + this.Next = null; } - /// - /// Creates a nondeterministic boolean choice execution step. - /// - internal static Step CreateNondeterministicBooleanChoice(int index, bool choice, SchedulingPointType sp) - { - var scheduleStep = new Step(); - scheduleStep.Index = index; - scheduleStep.Kind = DecisionKind.NondeterministicChoice; - scheduleStep.SchedulingPoint = sp; - scheduleStep.BooleanChoice = choice; - scheduleStep.IntegerChoice = null; - scheduleStep.Previous = null; - scheduleStep.Next = null; - return scheduleStep; - } - - /// - /// Creates a nondeterministic integer choice execution step. - /// - internal static Step CreateNondeterministicIntegerChoice(int index, int choice, SchedulingPointType sp) - { - var scheduleStep = new Step(); - scheduleStep.Index = index; - scheduleStep.Kind = DecisionKind.NondeterministicChoice; - scheduleStep.SchedulingPoint = sp; - scheduleStep.BooleanChoice = null; - scheduleStep.IntegerChoice = choice; - scheduleStep.Previous = null; - scheduleStep.Next = null; - return scheduleStep; - } - - /// - /// Returns the hash code for this instance. - /// + /// public override int GetHashCode() => this.Index.GetHashCode(); /// /// Indicates whether the specified is equal /// to the current . /// - internal bool Equals(Step other) => other != null ? - this.Index == other.Index && this.Kind == other.Kind && - this.SchedulingPoint == other.SchedulingPoint && - this.ScheduledOperationId == other.ScheduledOperationId && - this.BooleanChoice == other.BooleanChoice && - this.IntegerChoice == other.IntegerChoice : - false; + internal abstract bool Equals(Step other); - /// - /// Determines whether the specified object is equal to the current object. - /// + /// public override bool Equals(object obj) => this.Equals(obj as Step); /// @@ -348,6 +314,131 @@ namespace Microsoft.Coyote.Runtime /// for ordering or sorting purposes. /// int IComparable.CompareTo(Step other) => this.Index - other.Index; + + /// + /// Returns a string that represents the execution step with all operations + /// identified by their creation sequence ids. + /// + public abstract string ToSequenceString(); + } + + /// + /// Contains metadata related to a single scheduling step. + /// + internal sealed class SchedulingStep : Step + { + /// + /// The type of scheduling point encountered in this execution step. + /// + internal SchedulingPointType SchedulingPoint { get; private set; } + + /// + /// The id of the chosen operation. + /// + internal ulong Value; + + /// + /// The creation sequence id of the chosen operation. + /// + internal ulong SequenceId; + + /// + /// Initializes a new instance of the class. + /// + internal SchedulingStep(int index, ulong current, ulong currentSeqId, SchedulingPointType sp, ulong next, ulong seqId) + : base(index, current, currentSeqId) + { + this.SchedulingPoint = sp; + this.Value = next; + this.SequenceId = seqId; + } + + /// + internal override bool Equals(Step other) => other is SchedulingStep step ? + this.Index == step.Index && + this.Current == step.Current && + this.SchedulingPoint == step.SchedulingPoint && + this.Value == step.Value : + false; + + /// + /// Returns a string that represents the execution step. + /// + public override string ToString() => + $"op({this.Current}:{this.CurrentSequenceId}),sp({this.SchedulingPoint}),next({this.Value}:{this.SequenceId})"; + + /// + public override string ToSequenceString() => $"op({this.CurrentSequenceId}),sp({this.SchedulingPoint}),next({this.SequenceId})"; + } + + /// + /// Contains metadata related to a single boolean choice step. + /// + internal sealed class BooleanChoiceStep : Step + { + /// + /// The chosen boolean value. + /// + internal bool Value; + + /// + /// Initializes a new instance of the class. + /// + internal BooleanChoiceStep(int index, ulong current, ulong currentSeqId, bool value) + : base(index, current, currentSeqId) + { + this.Value = value; + } + + /// + internal override bool Equals(Step other) => other is BooleanChoiceStep step ? + this.Index == step.Index && + this.Current == step.Current && + this.Value == step.Value : + false; + + /// + /// Returns a string that represents the execution step. + /// + public override string ToString() => $"op({this.Current}:{this.CurrentSequenceId}),bool({this.Value})"; + + /// + public override string ToSequenceString() => $"op({this.CurrentSequenceId}),bool({this.Value})"; + } + + /// + /// Contains metadata related to a single integer choice step. + /// + internal sealed class IntegerChoiceStep : Step + { + /// + /// The chosen integer value. + /// + internal int Value; + + /// + /// Initializes a new instance of the class. + /// + internal IntegerChoiceStep(int index, ulong current, ulong currentSeqId, int value) + : base(index, current, currentSeqId) + { + this.Value = value; + } + + /// + internal override bool Equals(Step other) => other is IntegerChoiceStep step ? + this.Index == step.Index && + this.Current == step.Current && + this.Value == step.Value : + false; + + /// + /// Returns a string that represents the execution step. + /// + public override string ToString() => $"op({this.Current}:{this.CurrentSequenceId}),int({this.Value})"; + + /// + public override string ToSequenceString() => $"op({this.CurrentSequenceId}),int({this.Value})"; } } } diff --git a/Source/Core/Runtime/Operations/ControlledOperation.cs b/Source/Core/Runtime/Operations/ControlledOperation.cs index 0c993d93..3f68eede 100644 --- a/Source/Core/Runtime/Operations/ControlledOperation.cs +++ b/Source/Core/Runtime/Operations/ControlledOperation.cs @@ -22,6 +22,11 @@ namespace Microsoft.Coyote.Runtime /// internal ulong Id { get; } + /// + /// The creation sequence id of this operation. + /// + internal ulong SequenceId { get; } + /// /// The name of this operation. /// @@ -39,6 +44,11 @@ namespace Microsoft.Coyote.Runtime /// internal readonly OperationGroup Group; + /// + /// The creation sequence of this operation. + /// + private readonly List Sequence; + /// /// Queue of continuations that this operation must execute before it completes. /// @@ -77,6 +87,11 @@ namespace Microsoft.Coyote.Runtime /// internal IEqualityComparer LastAccessedSharedStateComparer; + /// + /// The count of operations created by this operation. + /// + internal ulong OperationCreationCount; + /// /// True if the source of this operation is uncontrolled, else false. /// @@ -87,6 +102,11 @@ namespace Microsoft.Coyote.Runtime /// internal bool IsDependencyUncontrolled; + /// + /// The debug information of this operation. + /// + internal string DebugInfo { get; } + /// /// True if this is the root operation, else false. /// @@ -117,9 +137,27 @@ namespace Microsoft.Coyote.Runtime this.LastHashedProgramState = 0; this.LastAccessedSharedState = string.Empty; this.LastAccessedSharedStateComparer = null; + this.OperationCreationCount = 0; this.IsSourceUncontrolled = false; this.IsDependencyUncontrolled = false; + // Only compute the sequence if the runtime scheduler is controlled. + if (this.Runtime.SchedulingPolicy is SchedulingPolicy.None) + { + this.SequenceId = 0; + } + else + { + // If no parent operation is found, and this is not the root operation, then assign the root operation as the + // parent operation. This is just an approximation that is applied in the case of uncontrolled threads. + ControlledOperation parent = this.Runtime.GetExecutingOperationUnsafe() ?? this.Runtime.GetOperationWithId(0); + this.Sequence = GetSequenceFromParent(operationId, parent); + this.SequenceId = this.GetSequenceHash(); + } + + // Set the debug information for this operation. + this.DebugInfo = $"'{this.Name}' with sequence id '{this.SequenceId}' and group id '{this.Group.Id}'"; + // Register this operation with the runtime. this.Runtime.RegisterNewOperation(this); } @@ -193,6 +231,45 @@ namespace Microsoft.Coyote.Runtime return this.Status is OperationStatus.Enabled; } + /// + /// Returns the creation sequence based on the specified parent operation. + /// + private static List GetSequenceFromParent(ulong operationId, ControlledOperation parent) + { + var sequence = new List(); + if (operationId is 0) + { + // If this is the root operation, then the sequence only contains the root operation itself. + sequence.Add(0); + } + else + { + sequence.AddRange(parent.Sequence); + sequence.Add(parent.OperationCreationCount); + parent.OperationCreationCount++; + } + + return sequence; + } + + /// + /// Returns the hash of the creation sequence. + /// + private ulong GetSequenceHash() + { + // Iterate the creation sequence and create a low collision rate hash. + ulong hash = (ulong)this.Sequence.Count; + foreach (ulong element in this.Sequence) + { + ulong seq = ((element >> 16) ^ element) * 0x45d9f3b; + seq = ((seq >> 16) ^ seq) * 0x45d9f3b; + seq = (seq >> 16) ^ seq; + hash ^= seq + 0x9e3779b9 + (hash << 6) + (hash >> 2); + } + + return hash; + } + /// /// Returns the hashed state of this operation for the specified policy. /// diff --git a/Source/Core/Runtime/Scheduling/OperationScheduler.cs b/Source/Core/Runtime/Scheduling/OperationScheduler.cs index b6e6c39f..7ae6de03 100644 --- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs +++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs @@ -250,7 +250,7 @@ namespace Microsoft.Coyote.Runtime if (this.Strategy is InterleavingStrategy strategy && strategy.GetNextOperation(enabledOps, current, isYielding, out next)) { - this.Trace.AddSchedulingChoice(next.Id, current.LastSchedulingPoint); + this.Trace.AddSchedulingDecision(current, current.LastSchedulingPoint, next); return true; } } @@ -270,7 +270,7 @@ namespace Microsoft.Coyote.Runtime if (this.Strategy is InterleavingStrategy strategy && strategy.GetNextBoolean(current, out next)) { - this.Trace.AddNondeterministicBooleanChoice(next, current.LastSchedulingPoint); + this.Trace.AddNondeterministicBooleanDecision(current, next); return true; } @@ -290,7 +290,7 @@ namespace Microsoft.Coyote.Runtime if (this.Strategy is InterleavingStrategy strategy && strategy.GetNextInteger(current, maxValue, out next)) { - this.Trace.AddNondeterministicIntegerChoice(next, current.LastSchedulingPoint); + this.Trace.AddNondeterministicIntegerDecision(current, next); return true; } diff --git a/Source/Core/Testing/Interleaving/DFSStrategy.cs b/Source/Core/Testing/Interleaving/DFSStrategy.cs index a5406142..54074210 100644 --- a/Source/Core/Testing/Interleaving/DFSStrategy.cs +++ b/Source/Core/Testing/Interleaving/DFSStrategy.cs @@ -235,7 +235,7 @@ namespace Microsoft.Coyote.Testing.Interleaving else { ncs = new List(); - for (int value = 0; value < maxValue; value++) + for (int value = 0; value < maxValue; ++value) { ncs.Add(new NondetIntegerChoice(value)); } @@ -278,7 +278,7 @@ namespace Microsoft.Coyote.Testing.Interleaving StringBuilder sb = new StringBuilder(); sb.AppendLine("*******************"); sb.AppendLine($"Schedule stack size: {this.ScheduleStack.Count}"); - for (int idx = 0; idx < this.ScheduleStack.Count; idx++) + for (int idx = 0; idx < this.ScheduleStack.Count; ++idx) { sb.AppendLine($"Index: {idx}"); foreach (var sc in this.ScheduleStack[idx]) @@ -291,7 +291,7 @@ namespace Microsoft.Coyote.Testing.Interleaving sb.AppendLine("*******************"); sb.AppendLine($"Random bool stack size: {this.BoolNondetStack.Count}"); - for (int idx = 0; idx < this.BoolNondetStack.Count; idx++) + for (int idx = 0; idx < this.BoolNondetStack.Count; ++idx) { sb.AppendLine($"Index: {idx}"); foreach (var nc in this.BoolNondetStack[idx]) @@ -304,7 +304,7 @@ namespace Microsoft.Coyote.Testing.Interleaving sb.AppendLine("*******************"); sb.AppendLine($"Random int stack size: {this.IntNondetStack.Count}"); - for (int idx = 0; idx < this.IntNondetStack.Count; idx++) + for (int idx = 0; idx < this.IntNondetStack.Count; ++idx) { sb.AppendLine($"Index: {idx}"); foreach (var nc in this.IntNondetStack[idx]) diff --git a/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs b/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs index 237b7ec8..97c0d5eb 100644 --- a/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs +++ b/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs @@ -68,7 +68,7 @@ namespace Microsoft.Coyote.Testing.Interleaving if (this.MaxDelaysPerIteration > 0) { var delays = this.RandomValueGenerator.Next(this.MaxDelaysPerIteration) + 1; - for (int i = 0; i < delays; i++) + for (int i = 0; i < delays; ++i) { this.DelayPoints.Add(this.RandomValueGenerator.Next(this.MaxDelayPoints + 1)); } @@ -192,7 +192,7 @@ namespace Microsoft.Coyote.Testing.Interleaving { var sb = new StringBuilder(); sb.AppendLine("[coyote::strategy] Updated operation group round-robin list: "); - for (int idx = 0; idx < this.OperationGroups.Count; idx++) + for (int idx = 0; idx < this.OperationGroups.Count; ++idx) { var group = this.OperationGroups[idx]; if (group.Any(m => m.Status is OperationStatus.Enabled)) diff --git a/Source/Core/Testing/Interleaving/InterleavingStrategy.cs b/Source/Core/Testing/Interleaving/InterleavingStrategy.cs index ead46ab9..d9a229e0 100644 --- a/Source/Core/Testing/Interleaving/InterleavingStrategy.cs +++ b/Source/Core/Testing/Interleaving/InterleavingStrategy.cs @@ -51,23 +51,26 @@ namespace Microsoft.Coyote.Testing.Interleaving if (this.StepCount < this.TracePrefix.Length) { ExecutionTrace.Step nextStep = this.TracePrefix[this.StepCount]; - if (nextStep.Kind != ExecutionTrace.DecisionKind.SchedulingChoice) + if (nextStep is ExecutionTrace.SchedulingStep step) + { + next = ops.FirstOrDefault(op => op.Id == step.Value); + if (next is null) + { + this.ErrorText = this.FormatReplayError(nextStep.Index, $"cannot detect id '{step.Value}'"); + throw new InvalidOperationException(this.ErrorText); + } + else if (step.SchedulingPoint != current.LastSchedulingPoint) + { + this.ErrorText = this.FormatReplayError(nextStep.Index, + $"expected scheduling point '{step.SchedulingPoint}' instead of '{current.LastSchedulingPoint}'"); + throw new InvalidOperationException(this.ErrorText); + } + } + else { this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a scheduling choice"); throw new InvalidOperationException(this.ErrorText); } - - next = ops.FirstOrDefault(op => op.Id == nextStep.ScheduledOperationId); - if (next is null) - { - this.ErrorText = this.FormatReplayError(nextStep.Index, $"cannot detect id '{nextStep.ScheduledOperationId}'"); - throw new InvalidOperationException(this.ErrorText); - } - else if (nextStep.SchedulingPoint != current.LastSchedulingPoint) - { - this.ErrorText = this.FormatSchedulingPointReplayError(nextStep.Index, nextStep.SchedulingPoint, current.LastSchedulingPoint); - throw new InvalidOperationException(this.ErrorText); - } } else { @@ -110,24 +113,15 @@ namespace Microsoft.Coyote.Testing.Interleaving if (this.StepCount < this.TracePrefix.Length) { ExecutionTrace.Step nextStep = this.TracePrefix[this.StepCount]; - if (nextStep.Kind != ExecutionTrace.DecisionKind.NondeterministicChoice) + if (nextStep is ExecutionTrace.BooleanChoiceStep step) + { + next = step.Value; + } + else { this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic choice"); throw new InvalidOperationException(this.ErrorText); } - - if (nextStep.BooleanChoice is null) - { - this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic boolean choice"); - throw new InvalidOperationException(this.ErrorText); - } - else if (nextStep.SchedulingPoint != current.LastSchedulingPoint) - { - this.ErrorText = this.FormatSchedulingPointReplayError(nextStep.Index, nextStep.SchedulingPoint, current.LastSchedulingPoint); - throw new InvalidOperationException(this.ErrorText); - } - - next = nextStep.BooleanChoice.Value; } else { @@ -168,24 +162,15 @@ namespace Microsoft.Coyote.Testing.Interleaving if (this.StepCount < this.TracePrefix.Length) { ExecutionTrace.Step nextStep = this.TracePrefix[this.StepCount]; - if (nextStep.Kind != ExecutionTrace.DecisionKind.NondeterministicChoice) + if (nextStep is ExecutionTrace.IntegerChoiceStep step) + { + next = step.Value; + } + else { this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic choice"); throw new InvalidOperationException(this.ErrorText); } - - if (nextStep.IntegerChoice is null) - { - this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic integer choice"); - throw new InvalidOperationException(this.ErrorText); - } - else if (nextStep.SchedulingPoint != current.LastSchedulingPoint) - { - this.ErrorText = this.FormatSchedulingPointReplayError(nextStep.Index, nextStep.SchedulingPoint, current.LastSchedulingPoint); - throw new InvalidOperationException(this.ErrorText); - } - - next = nextStep.IntegerChoice.Value; } else { @@ -220,12 +205,6 @@ namespace Microsoft.Coyote.Testing.Interleaving /// internal virtual void Reset() => this.StepCount = 0; - /// - /// Formats the error message regarding an unexpected scheduling point. - /// - private string FormatSchedulingPointReplayError(int step, SchedulingPointType expected, SchedulingPointType actual) => - this.FormatReplayError(step, $"expected scheduling point '{expected}' instead of '{actual}'"); - /// /// Formats the error message. /// diff --git a/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs b/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs index b0d11c99..b705ecd8 100644 --- a/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs +++ b/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs @@ -221,7 +221,7 @@ namespace Microsoft.Coyote.Testing.Interleaving { var sb = new StringBuilder(); sb.AppendLine("[coyote::strategy] Updated operation group priority list: "); - for (int idx = 0; idx < this.PrioritizedOperationGroups.Count; idx++) + for (int idx = 0; idx < this.PrioritizedOperationGroups.Count; ++idx) { var group = this.PrioritizedOperationGroups[idx]; if (group.Any(m => m.Status is OperationStatus.Enabled)) diff --git a/Source/Core/Testing/Interleaving/ProbabilisticRandomStrategy.cs b/Source/Core/Testing/Interleaving/ProbabilisticRandomStrategy.cs index f4e05085..efa663c2 100644 --- a/Source/Core/Testing/Interleaving/ProbabilisticRandomStrategy.cs +++ b/Source/Core/Testing/Interleaving/ProbabilisticRandomStrategy.cs @@ -58,7 +58,7 @@ namespace Microsoft.Coyote.Testing.Interleaving /// private bool ShouldCurrentOperationChange() { - for (int idx = 0; idx < this.Bound; idx++) + for (int idx = 0; idx < this.Bound; ++idx) { if (this.RandomValueGenerator.Next(2) is 1) { diff --git a/Source/Core/Testing/Interleaving/QLearningStrategy.cs b/Source/Core/Testing/Interleaving/QLearningStrategy.cs index aaeb9380..7267a540 100644 --- a/Source/Core/Testing/Interleaving/QLearningStrategy.cs +++ b/Source/Core/Testing/Interleaving/QLearningStrategy.cs @@ -190,7 +190,7 @@ namespace Microsoft.Coyote.Testing.Interleaving private int GetNextIntegerChoiceByPolicy(int state, int maxValue) { var qValues = new List(maxValue); - for (ulong i = 0; i < (ulong)maxValue; i++) + for (ulong i = 0; i < (ulong)maxValue; ++i) { qValues.Add(this.OperationQTable[state][this.MinIntegerChoiceOpValue - i]); } @@ -205,13 +205,13 @@ namespace Microsoft.Coyote.Testing.Interleaving private int ChooseQValueIndexFromDistribution(List qValues) { double sum = 0; - for (int i = 0; i < qValues.Count; i++) + for (int i = 0; i < qValues.Count; ++i) { qValues[i] = Math.Exp(qValues[i]); sum += qValues[i]; } - for (int i = 0; i < qValues.Count; i++) + for (int i = 0; i < qValues.Count; ++i) { qValues[i] /= sum; } @@ -331,7 +331,7 @@ namespace Microsoft.Coyote.Testing.Interleaving this.OperationQTable.Add(state, qValues); } - for (ulong i = 0; i < (ulong)maxValue; i++) + for (ulong i = 0; i < (ulong)maxValue; ++i) { ulong opValue = this.MinIntegerChoiceOpValue - i; if (!qValues.ContainsKey(opValue)) diff --git a/Source/Test/Rewriting/Passes/Rewriting/RewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/RewritingPass.cs index b5c78fad..4e28cc72 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/RewritingPass.cs +++ b/Source/Test/Rewriting/Passes/Rewriting/RewritingPass.cs @@ -40,7 +40,7 @@ namespace Microsoft.Coyote.Rewriting if (method.Name == name && method.Parameters.Count == parameterTypes.Length) { bool isMatch = true; - for (int i = 0; isMatch && i < method.Parameters.Count; i++) + for (int i = 0; isMatch && i < method.Parameters.Count; ++i) { var left = parameterTypes[i]; var right = method.Parameters[i].ParameterType; diff --git a/Source/Test/Rewriting/Passes/Rewriting/Types/MethodBodyTypeRewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/Types/MethodBodyTypeRewritingPass.cs index 8b3f0beb..7c747b4f 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/Types/MethodBodyTypeRewritingPass.cs +++ b/Source/Test/Rewriting/Passes/Rewriting/Types/MethodBodyTypeRewritingPass.cs @@ -183,7 +183,7 @@ namespace Microsoft.Coyote.Rewriting // if it has, find the rewritten method. The signature does not include the return // type according to C# rules, so we do not take it into account. List paramTypes = new List(); - for (int i = 0; i < method.Parameters.Count; i++) + for (int i = 0; i < method.Parameters.Count; ++i) { var p = method.Parameters[i]; paramTypes.Add(this.RewriteType(p.ParameterType, Options.None)); @@ -282,7 +282,7 @@ namespace Microsoft.Coyote.Rewriting Collection genericArguments, ref bool isRewritten) { var genericMethod = new GenericInstanceMethod(method); - for (int i = 0; i < genericArguments.Count; i++) + for (int i = 0; i < genericArguments.Count; ++i) { GenericParameter parameter = new GenericParameter(genericParameters[i].Name, genericMethod); method.GenericParameters.Add(parameter); @@ -301,7 +301,7 @@ namespace Microsoft.Coyote.Rewriting private MethodReference RewriteParameters(MethodReference method, Collection parameters, ref bool isRewritten) { - for (int i = 0; i < parameters.Count; i++) + for (int i = 0; i < parameters.Count; ++i) { // Try rewrite the parameter only if the declaring type is a non-runtime type, // else assign the generic arguments if the parameter is generic. @@ -347,7 +347,7 @@ namespace Microsoft.Coyote.Rewriting return false; } - for (int idx = 0; idx < right.Parameters.Count; idx++) + for (int idx = 0; idx < right.Parameters.Count; ++idx) { var leftParam = left.Parameters[idx]; var rightParam = right.Parameters[idx]; @@ -407,7 +407,7 @@ namespace Microsoft.Coyote.Rewriting } // Check if the parameters match. - for (int idx = 0; idx < originalMethod.Parameters.Count; idx++) + for (int idx = 0; idx < originalMethod.Parameters.Count; ++idx) { // If we are converting to static, we have one extra parameter, so skip it. var newParameter = newMethod.Parameters[isConvertedToStatic ? idx + 1 : idx]; diff --git a/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs index 9b659c9c..24b19c51 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs +++ b/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs @@ -172,7 +172,7 @@ namespace Microsoft.Coyote.Rewriting onlyImport, ref isRewritten); GenericInstanceType newGenericType = newElementType as GenericInstanceType ?? new GenericInstanceType(newElementType); - for (int idx = 0; idx < genericType.GenericArguments.Count; idx++) + for (int idx = 0; idx < genericType.GenericArguments.Count; ++idx) { newGenericType.GenericArguments.Add(this.RewriteType(genericType.GenericArguments[idx], options & ~Options.AllowStaticRewrittenType, false, ref isRewritten)); diff --git a/Source/Test/Rewriting/Types/Threading/SemaphoreSlim.cs b/Source/Test/Rewriting/Types/Threading/SemaphoreSlim.cs index 3bcb612f..54ef9dfe 100644 --- a/Source/Test/Rewriting/Types/Threading/SemaphoreSlim.cs +++ b/Source/Test/Rewriting/Types/Threading/SemaphoreSlim.cs @@ -303,8 +303,8 @@ namespace Microsoft.Coyote.Rewriting.Types.Threading } runtime.LogWriter.LogDebug( - "[coyote::debug] Operation '{0}' of group '{1}' is waiting for '{2}' to get released on thread '{3}'.", - current.Name, current.Group, this.DebugName, SystemThread.CurrentThread.ManagedThreadId); + "[coyote::debug] Operation {0} is waiting for '{1}' to get released on thread '{2}'.", + current.DebugInfo, this.DebugName, SystemThread.CurrentThread.ManagedThreadId); current.Status = OperationStatus.PausedOnResource; this.PausedOperations.Enqueue(current); runtime.ScheduleNextOperation(current, SchedulingPointType.Pause); diff --git a/Source/Test/SystematicTesting/Reports/TestReport.cs b/Source/Test/SystematicTesting/Reports/TestReport.cs index 627c9cd4..d19189e9 100644 --- a/Source/Test/SystematicTesting/Reports/TestReport.cs +++ b/Source/Test/SystematicTesting/Reports/TestReport.cs @@ -29,16 +29,16 @@ namespace Microsoft.Coyote.SystematicTesting public ActorCoverageInfo CoverageInfo { get; private set; } /// - /// Number of explored fair schedules. + /// Number of explored fair execution paths. /// [DataMember] - public int NumOfExploredFairSchedules { get; internal set; } + public int NumOfExploredFairPaths { get; internal set; } /// - /// Number of explored unfair schedules. + /// Number of explored unfair execution paths. /// [DataMember] - public int NumOfExploredUnfairSchedules { get; internal set; } + public int NumOfExploredUnfairPaths { get; internal set; } /// /// Number of found bugs. @@ -113,37 +113,37 @@ namespace Microsoft.Coyote.SystematicTesting public int TotalOperationGroupingDegree { get; internal set; } /// - /// The min explored scheduling steps in fair tests. + /// The min explored execution steps in fair tests. /// [DataMember] public int MinExploredFairSteps { get; internal set; } /// - /// The max explored scheduling steps in fair tests. + /// The max explored execution steps in fair tests. /// [DataMember] public int MaxExploredFairSteps { get; internal set; } /// - /// The total explored scheduling steps (across all testing iterations) in fair tests. + /// The total explored execution steps (across all testing iterations) in fair tests. /// [DataMember] public int TotalExploredFairSteps { get; internal set; } /// - /// The min explored scheduling steps in unfair tests. + /// The min explored execution steps in unfair tests. /// [DataMember] public int MinExploredUnfairSteps { get; internal set; } /// - /// The max explored scheduling steps in unfair tests. + /// The max explored execution steps in unfair tests. /// [DataMember] public int MaxExploredUnfairSteps { get; internal set; } /// - /// The total explored scheduling steps (across all testing iterations) in unfair tests. + /// The total explored execution steps (across all testing iterations) in unfair tests. /// [DataMember] public int TotalExploredUnfairSteps { get; internal set; } @@ -191,8 +191,8 @@ namespace Microsoft.Coyote.SystematicTesting this.CoverageInfo = new ActorCoverageInfo(); - this.NumOfExploredFairSchedules = 0; - this.NumOfExploredUnfairSchedules = 0; + this.NumOfExploredFairPaths = 0; + this.NumOfExploredUnfairPaths = 0; this.NumOfFoundBugs = 0; this.BugReports = new HashSet(); this.UncontrolledInvocations = new HashSet(); @@ -223,7 +223,7 @@ namespace Microsoft.Coyote.SystematicTesting /// void ITestReport.SetSchedulingStatistics(bool isBugFound, string bugReport, int numOperations, int concurrencyDegree, - int groupingDegree, int scheduledSteps, bool isMaxScheduledStepsBoundReached, bool isScheduleFair) + int groupingDegree, int executionSteps, bool isMaxStepsBoundReached, bool isExecutionPathFair) { if (isBugFound) { @@ -255,39 +255,39 @@ namespace Microsoft.Coyote.SystematicTesting this.MinOperationGroupingDegree = groupingDegree; } - if (isScheduleFair) + if (isExecutionPathFair) { - this.NumOfExploredFairSchedules++; - this.TotalExploredFairSteps += scheduledSteps; - this.MaxExploredFairSteps = Math.Max(this.MaxExploredFairSteps, scheduledSteps); + this.NumOfExploredFairPaths++; + this.TotalExploredFairSteps += executionSteps; + this.MaxExploredFairSteps = Math.Max(this.MaxExploredFairSteps, executionSteps); if (this.MinExploredFairSteps < 0 || - this.MinExploredFairSteps > scheduledSteps) + this.MinExploredFairSteps > executionSteps) { - this.MinExploredFairSteps = scheduledSteps; + this.MinExploredFairSteps = executionSteps; } - if (isMaxScheduledStepsBoundReached) + if (isMaxStepsBoundReached) { this.MaxFairStepsHitInFairTests++; } - if (scheduledSteps >= this.Configuration.MaxUnfairSchedulingSteps) + if (executionSteps >= this.Configuration.MaxUnfairSchedulingSteps) { this.MaxUnfairStepsHitInFairTests++; } } else { - this.NumOfExploredUnfairSchedules++; - this.TotalExploredUnfairSteps += scheduledSteps; - this.MaxExploredUnfairSteps = Math.Max(this.MaxExploredUnfairSteps, scheduledSteps); + this.NumOfExploredUnfairPaths++; + this.TotalExploredUnfairSteps += executionSteps; + this.MaxExploredUnfairSteps = Math.Max(this.MaxExploredUnfairSteps, executionSteps); if (this.MinExploredUnfairSteps < 0 || - this.MinExploredUnfairSteps > scheduledSteps) + this.MinExploredUnfairSteps > executionSteps) { - this.MinExploredUnfairSteps = scheduledSteps; + this.MinExploredUnfairSteps = executionSteps; } - if (isMaxScheduledStepsBoundReached) + if (isMaxStepsBoundReached) { this.MaxUnfairStepsHitInUnfairTests++; } @@ -354,8 +354,8 @@ namespace Microsoft.Coyote.SystematicTesting this.MinOperationGroupingDegree = testReport.MinOperationGroupingDegree; } - this.NumOfExploredFairSchedules += testReport.NumOfExploredFairSchedules; - this.NumOfExploredUnfairSchedules += testReport.NumOfExploredUnfairSchedules; + this.NumOfExploredFairPaths += testReport.NumOfExploredFairPaths; + this.NumOfExploredUnfairPaths += testReport.NumOfExploredUnfairPaths; this.TotalExploredFairSteps += testReport.TotalExploredFairSteps; this.MaxExploredFairSteps = Math.Max(this.MaxExploredFairSteps, testReport.MaxExploredFairSteps); @@ -420,26 +420,27 @@ namespace Microsoft.Coyote.SystematicTesting report.AppendLine(); report.AppendFormat("{0} Scheduling statistics:", prefix); - int totalExploredSchedules = this.NumOfExploredFairSchedules + - this.NumOfExploredUnfairSchedules; + int totalExploredPaths = this.NumOfExploredFairPaths + + this.NumOfExploredUnfairPaths; report.AppendLine(); report.AppendFormat( - "{0} Explored {1} schedule{2}: {3} fair and {4} unfair.", + "{0} Explored {1} execution path{2}: {3} fair, {4} unfair, {5} unique.", prefix.Equals("...") ? "....." : prefix, - totalExploredSchedules, - totalExploredSchedules is 1 ? string.Empty : "s", - this.NumOfExploredFairSchedules, - this.NumOfExploredUnfairSchedules); + totalExploredPaths, + totalExploredPaths is 1 ? string.Empty : "s", + this.NumOfExploredFairPaths, + this.NumOfExploredUnfairPaths, + this.CoverageInfo.ExploredPaths.Count); - if (totalExploredSchedules > 0 && + if (totalExploredPaths > 0 && this.NumOfFoundBugs > 0) { report.AppendLine(); report.AppendFormat( - "{0} Found {1:F2}% buggy schedules.", + "{0} Found {1:F2}% buggy execution paths.", prefix.Equals("...") ? "....." : prefix, - this.NumOfFoundBugs * 100.0 / totalExploredSchedules); + this.NumOfFoundBugs * 100.0 / totalExploredPaths); } int visitedStatesCount = this.CoverageInfo.VisitedStates.Count; @@ -447,7 +448,7 @@ namespace Microsoft.Coyote.SystematicTesting { report.AppendLine(); report.AppendFormat( - "{0} Visited {1} state{2}.", + "{0} Visited {1} unique state{2}.", prefix.Equals("...") ? "....." : prefix, visitedStatesCount, visitedStatesCount is 1 ? string.Empty : "s"); @@ -457,13 +458,14 @@ namespace Microsoft.Coyote.SystematicTesting { report.AppendLine(); report.AppendFormat( - "{0} Controlled {1} operation{2}: {3} (min), {4} (avg), {5} (max).", + "{0} Controlled {1} operation{2}: {3} (min), {4} (avg), {5} (max), {6} (unique).", prefix.Equals("...") ? "....." : prefix, this.TotalControlledOperations, this.TotalControlledOperations is 1 ? string.Empty : "s", this.MinControlledOperations, - this.TotalControlledOperations / totalExploredSchedules, - this.MaxControlledOperations); + this.TotalControlledOperations / totalExploredPaths, + this.MaxControlledOperations, + this.CoverageInfo.OperationSequenceIds.Count); } if (this.TotalConcurrencyDegree > 0) @@ -473,7 +475,7 @@ namespace Microsoft.Coyote.SystematicTesting "{0} Degree of concurrency: {1} (min), {2} (avg), {3} (max).", prefix.Equals("...") ? "....." : prefix, this.MinConcurrencyDegree, - this.TotalConcurrencyDegree / totalExploredSchedules, + this.TotalConcurrencyDegree / totalExploredPaths, this.MaxConcurrencyDegree); } @@ -484,18 +486,18 @@ namespace Microsoft.Coyote.SystematicTesting "{0} Degree of operation grouping: {1} (min), {2} (avg), {3} (max).", prefix.Equals("...") ? "....." : prefix, this.MinOperationGroupingDegree, - this.TotalOperationGroupingDegree / totalExploredSchedules, + this.TotalOperationGroupingDegree / totalExploredPaths, this.MaxOperationGroupingDegree); } - if (this.NumOfExploredFairSchedules > 0) + if (this.NumOfExploredFairPaths > 0) { report.AppendLine(); report.AppendFormat( - "{0} Number of scheduling decisions in fair terminating schedules: {1} (min), {2} (avg), {3} (max).", + "{0} Number of scheduling decisions in fair terminating execution paths: {1} (min), {2} (avg), {3} (max).", prefix.Equals("...") ? "....." : prefix, this.MinExploredFairSteps < 0 ? 0 : this.MinExploredFairSteps, - this.TotalExploredFairSteps / this.NumOfExploredFairSchedules, + this.TotalExploredFairSteps / this.NumOfExploredFairPaths, this.MaxExploredFairSteps < 0 ? 0 : this.MaxExploredFairSteps); if (configuration.MaxUnfairSchedulingSteps > 0 && @@ -503,10 +505,10 @@ namespace Microsoft.Coyote.SystematicTesting { report.AppendLine(); report.AppendFormat( - "{0} Exceeded the max-steps bound of '{1}' in {2:F2}% of the fair schedules.", + "{0} Exceeded the max-steps bound of '{1}' in {2:F2}% of the fair execution paths.", prefix.Equals("...") ? "....." : prefix, configuration.MaxUnfairSchedulingSteps, - (double)this.MaxUnfairStepsHitInFairTests / this.NumOfExploredFairSchedules * 100); + (double)this.MaxUnfairStepsHitInFairTests / this.NumOfExploredFairPaths * 100); } if (configuration.UserExplicitlySetMaxFairSchedulingSteps && @@ -515,21 +517,21 @@ namespace Microsoft.Coyote.SystematicTesting { report.AppendLine(); report.AppendFormat( - "{0} Hit the max-steps bound of '{1}' in {2:F2}% of the fair schedules.", + "{0} Hit the max-steps bound of '{1}' in {2:F2}% of the fair execution paths.", prefix.Equals("...") ? "....." : prefix, configuration.MaxFairSchedulingSteps, - (double)this.MaxFairStepsHitInFairTests / this.NumOfExploredFairSchedules * 100); + (double)this.MaxFairStepsHitInFairTests / this.NumOfExploredFairPaths * 100); } } - if (this.NumOfExploredUnfairSchedules > 0) + if (this.NumOfExploredUnfairPaths > 0) { report.AppendLine(); report.AppendFormat( - "{0} Number of scheduling decisions in unfair terminating schedules: {1} (min), {2} (avg), {3} (max).", + "{0} Number of scheduling decisions in unfair terminating execution paths: {1} (min), {2} (avg), {3} (max).", prefix.Equals("...") ? "....." : prefix, this.MinExploredUnfairSteps < 0 ? 0 : this.MinExploredUnfairSteps, - this.TotalExploredUnfairSteps / this.NumOfExploredUnfairSchedules, + this.TotalExploredUnfairSteps / this.NumOfExploredUnfairPaths, this.MaxExploredUnfairSteps < 0 ? 0 : this.MaxExploredUnfairSteps); if (configuration.MaxUnfairSchedulingSteps > 0 && @@ -537,10 +539,10 @@ namespace Microsoft.Coyote.SystematicTesting { report.AppendLine(); report.AppendFormat( - "{0} Hit the max-steps bound of '{1}' in {2:F2}% of the unfair schedules.", + "{0} Hit the max-steps bound of '{1}' in {2:F2}% of the unfair execution paths.", prefix.Equals("...") ? "....." : prefix, configuration.MaxUnfairSchedulingSteps, - (double)this.MaxUnfairStepsHitInUnfairTests / this.NumOfExploredUnfairSchedules * 100); + (double)this.MaxUnfairStepsHitInUnfairTests / this.NumOfExploredUnfairPaths * 100); } } diff --git a/Source/Test/SystematicTesting/Reports/TraceReport.cs b/Source/Test/SystematicTesting/Reports/TraceReport.cs index 430cb155..a0e6959f 100644 --- a/Source/Test/SystematicTesting/Reports/TraceReport.cs +++ b/Source/Test/SystematicTesting/Reports/TraceReport.cs @@ -33,9 +33,9 @@ namespace Microsoft.Coyote.SystematicTesting public TestSettings Settings { get; set; } /// - /// The controlled decisions of this trace. + /// The execution steps in this trace. /// - public List Decisions { get; set; } + public List Steps { get; set; } /// /// Constructs a from the specified @@ -110,35 +110,47 @@ namespace Microsoft.Coyote.SystematicTesting configuration.UncontrolledConcurrencyResolutionAttempts = report.Settings.UncontrolledConcurrencyResolutionAttempts; configuration.UncontrolledConcurrencyResolutionDelay = report.Settings.UncontrolledConcurrencyResolutionDelay; - foreach (var decision in report.Decisions) + for (int idx = 0; idx < report.Steps.Count; idx++) { - string[] tokens = decision.Split(','); - string kindToken = tokens[0]; - string spToken = tokens[1]; + string[] tokens = report.Steps[idx].Split(','); + // The current operation token is of the form 'op(id:seqId)'. + string opToken = tokens[0]; + string[] opTokens = opToken.Substring(3, opToken.Length - 4).Split(':'); + ulong opId = ulong.Parse(opTokens[0]); + ulong opSeqId = ulong.Parse(opTokens[1]); + + string decisionToken = tokens[1]; + if (decisionToken.StartsWith("sp(")) + { #if NET || NETCOREAPP3_1 - SchedulingPointType sp = Enum.Parse(spToken.Substring(3, spToken.Length - 4)); + SchedulingPointType sp = Enum.Parse(decisionToken.Substring( + 3, decisionToken.Length - 4)); #else - SchedulingPointType sp = (SchedulingPointType)Enum.Parse(typeof(SchedulingPointType), spToken.Substring(3, spToken.Length - 4)); + SchedulingPointType sp = (SchedulingPointType)Enum.Parse(typeof(SchedulingPointType), + decisionToken.Substring(3, decisionToken.Length - 4)); #endif - if (kindToken.StartsWith("op(")) - { - ulong id = ulong.Parse(kindToken.Substring(3, kindToken.Length - 4)); - trace.AddSchedulingChoice(id, sp); + + // The next operation token is of the form 'next(id:seqId)'. + string nextToken = tokens[2]; + string[] nextTokens = nextToken.Substring(5, nextToken.Length - 6).Split(':'); + ulong nextId = ulong.Parse(nextTokens[0]); + ulong nextSeqId = ulong.Parse(nextTokens[1]); + trace.AddSchedulingDecision(opId, opSeqId, sp, nextId, nextSeqId); } - else if (kindToken.StartsWith("bool(")) + else if (decisionToken.StartsWith("bool(")) { - bool value = bool.Parse(kindToken.Substring(5, kindToken.Length - 6)); - trace.AddNondeterministicBooleanChoice(value, sp); + bool value = bool.Parse(decisionToken.Substring(5, decisionToken.Length - 6)); + trace.AddNondeterministicBooleanDecision(opId, opSeqId, value); } - else if (kindToken.StartsWith("int(")) + else if (decisionToken.StartsWith("int(")) { - int value = int.Parse(kindToken.Substring(4, kindToken.Length - 5)); - trace.AddNondeterministicIntegerChoice(value, sp); + int value = int.Parse(decisionToken.Substring(4, decisionToken.Length - 5)); + trace.AddNondeterministicIntegerDecision(opId, opSeqId, value); } else { - throw new InvalidOperationException($"Unexpected decision '{decision}'."); + throw new InvalidOperationException($"Unexpected execution step '{report.Steps[idx]}'."); } } } @@ -151,22 +163,10 @@ namespace Microsoft.Coyote.SystematicTesting /// internal void ReportTrace(ExecutionTrace trace) { - this.Decisions = new List(); - for (int idx = 0; idx < trace.Length; idx++) + this.Steps = new List(); + foreach (var step in trace) { - ExecutionTrace.Step step = trace[idx]; - if (step.Kind == ExecutionTrace.DecisionKind.SchedulingChoice) - { - this.Decisions.Add($"op({step.ScheduledOperationId}),sp({step.SchedulingPoint})"); - } - else if (step.BooleanChoice != null) - { - this.Decisions.Add($"bool({step.BooleanChoice.Value}),sp({step.SchedulingPoint})"); - } - else - { - this.Decisions.Add($"int({step.IntegerChoice.Value}),sp({step.SchedulingPoint})"); - } + this.Steps.Add(step.ToString()); } } diff --git a/Source/Test/SystematicTesting/TestMethodInfo.cs b/Source/Test/SystematicTesting/TestMethodInfo.cs index bdc79f73..e752e04e 100644 --- a/Source/Test/SystematicTesting/TestMethodInfo.cs +++ b/Source/Test/SystematicTesting/TestMethodInfo.cs @@ -181,7 +181,7 @@ namespace Microsoft.Coyote.SystematicTesting error += " Possible methods are:" + Environment.NewLine; var possibleMethods = filteredTestMethods?.Count > 1 ? filteredTestMethods : testMethods; - for (int idx = 0; idx < possibleMethods.Count; idx++) + for (int idx = 0; idx < possibleMethods.Count; ++idx) { var mi = possibleMethods[idx]; error += string.Format(" {0}.{1}", mi.DeclaringType.FullName, mi.Name); diff --git a/Tests/Tests.Runtime/Exploration/ExecutionTraceTests.cs b/Tests/Tests.Runtime/Exploration/ExecutionTraceTests.cs index 834842d0..8651fdb5 100644 --- a/Tests/Tests.Runtime/Exploration/ExecutionTraceTests.cs +++ b/Tests/Tests.Runtime/Exploration/ExecutionTraceTests.cs @@ -15,116 +15,115 @@ namespace Microsoft.Coyote.Runtime.Tests } [Fact(Timeout = 5000)] - public void TestExecutionTraceAddSchedulingChoices() + public void TestExecutionTraceAddSchedulingDecisions() { ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(2, SchedulingPointType.Default); - trace.AddSchedulingChoice(3, SchedulingPointType.Default); - trace.AddSchedulingChoice(1, SchedulingPointType.Default); - trace.AddSchedulingChoice(2, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); + trace.AddSchedulingDecision(1, 1, SchedulingPointType.Default, 3, 3); + trace.AddSchedulingDecision(2, 2, SchedulingPointType.Default, 1, 1); + trace.AddSchedulingDecision(1, 1, SchedulingPointType.Default, 2, 2); this.LogTrace(trace); Assert.True(trace.Length is 5); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.SchedulingStep); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).SequenceId is 0); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[1].ScheduledOperationId is 2); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(!trace[1].IntegerChoice.HasValue); + Assert.True(trace[1] is ExecutionTrace.SchedulingStep); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).SequenceId is 2); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[2].ScheduledOperationId is 3); - Assert.True(!trace[2].BooleanChoice.HasValue); - Assert.True(!trace[2].IntegerChoice.HasValue); + Assert.True(trace[2] is ExecutionTrace.SchedulingStep); + Assert.True((trace[2] as ExecutionTrace.SchedulingStep).Current is 1); + Assert.True((trace[2] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 1); + Assert.True((trace[2] as ExecutionTrace.SchedulingStep).Value is 3); + Assert.True((trace[2] as ExecutionTrace.SchedulingStep).SequenceId is 3); Assert.True(trace[3].Index is 3); - Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[3].ScheduledOperationId is 1); - Assert.True(!trace[3].BooleanChoice.HasValue); - Assert.True(!trace[3].IntegerChoice.HasValue); + Assert.True(trace[3] is ExecutionTrace.SchedulingStep); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Current is 2); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 2); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).SequenceId is 1); Assert.True(trace[4].Index is 4); - Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[4].ScheduledOperationId is 2); - Assert.True(!trace[4].BooleanChoice.HasValue); - Assert.True(!trace[4].IntegerChoice.HasValue); + Assert.True(trace[4] is ExecutionTrace.SchedulingStep); + Assert.True((trace[4] as ExecutionTrace.SchedulingStep).Current is 1); + Assert.True((trace[4] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 1); + Assert.True((trace[4] as ExecutionTrace.SchedulingStep).Value is 2); + Assert.True((trace[4] as ExecutionTrace.SchedulingStep).SequenceId is 2); } [Fact(Timeout = 5000)] - public void TestExecutionTraceAddNondeterministicBooleanChoices() + public void TestExecutionTraceAddNondeterministicBooleanDecisions() { ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(false, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); + trace.AddNondeterministicBooleanDecision(0, 0, true); + trace.AddNondeterministicBooleanDecision(0, 0, false); + trace.AddNondeterministicBooleanDecision(0, 0, true); this.LogTrace(trace); Assert.True(trace.Length is 3); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(trace[0].BooleanChoice.HasValue); - Assert.True(trace[0].BooleanChoice.Value is true); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[0] as ExecutionTrace.BooleanChoiceStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.BooleanChoiceStep).Value is true); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[1].ScheduledOperationId is 0); - Assert.True(trace[1].BooleanChoice.HasValue); - Assert.True(trace[1].BooleanChoice.Value is false); - Assert.True(!trace[1].IntegerChoice.HasValue); + Assert.True(trace[1] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[1] as ExecutionTrace.BooleanChoiceStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.BooleanChoiceStep).Value is false); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[2].ScheduledOperationId is 0); - Assert.True(trace[2].BooleanChoice.HasValue); - Assert.True(trace[2].BooleanChoice.Value is true); - Assert.True(!trace[2].IntegerChoice.HasValue); + Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Current is 0); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true); } [Fact(Timeout = 5000)] - public void TestExecutionTraceAddNondeterministicIntegerChoices() + public void TestExecutionTraceAddNondeterministicIntegerDecisions() { ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddNondeterministicIntegerChoice(3, SchedulingPointType.Default); - trace.AddNondeterministicIntegerChoice(7, SchedulingPointType.Default); - trace.AddNondeterministicIntegerChoice(4, SchedulingPointType.Default); + trace.AddNondeterministicIntegerDecision(0, 0, 3); + trace.AddNondeterministicIntegerDecision(0, 0, 7); + trace.AddNondeterministicIntegerDecision(0, 0, 4); this.LogTrace(trace); Assert.True(trace.Length is 3); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(trace[0].IntegerChoice.HasValue); - Assert.True(trace[0].IntegerChoice.Value is 3); + Assert.True(trace[0] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[0] as ExecutionTrace.IntegerChoiceStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.IntegerChoiceStep).Value is 3); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[1].ScheduledOperationId is 0); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(trace[1].IntegerChoice.HasValue); - Assert.True(trace[1].IntegerChoice.Value is 7); + Assert.True(trace[1] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).Value is 7); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[2].ScheduledOperationId is 0); - Assert.True(!trace[2].BooleanChoice.HasValue); - Assert.True(trace[2].IntegerChoice.HasValue); - Assert.True(trace[2].IntegerChoice.Value is 4); + Assert.True(trace[2] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[2] as ExecutionTrace.IntegerChoiceStep).Current is 0); + Assert.True((trace[2] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[2] as ExecutionTrace.IntegerChoiceStep).Value is 4); } [Fact(Timeout = 5000)] @@ -133,45 +132,46 @@ namespace Microsoft.Coyote.Runtime.Tests ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(2, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); - trace.AddSchedulingChoice(1, SchedulingPointType.Default); - trace.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); + trace.AddNondeterministicBooleanDecision(2, 2, true); + trace.AddSchedulingDecision(2, 2, SchedulingPointType.Default, 1, 1); + trace.AddNondeterministicIntegerDecision(1, 1, 5); this.LogTrace(trace); Assert.True(trace.Length is 5); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.SchedulingStep); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).SequenceId is 0); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[1].ScheduledOperationId is 2); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(!trace[1].IntegerChoice.HasValue); + Assert.True(trace[1] is ExecutionTrace.SchedulingStep); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).SequenceId is 2); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[2].ScheduledOperationId is 0); - Assert.True(trace[2].BooleanChoice.HasValue); - Assert.True(trace[2].BooleanChoice.Value is true); - Assert.True(!trace[2].IntegerChoice.HasValue); + Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Current is 2); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 2); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true); Assert.True(trace[3].Index is 3); - Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[3].ScheduledOperationId is 1); - Assert.True(!trace[3].BooleanChoice.HasValue); - Assert.True(!trace[3].IntegerChoice.HasValue); + Assert.True(trace[3] is ExecutionTrace.SchedulingStep); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Current is 2); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 2); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).SequenceId is 1); Assert.True(trace[4].Index is 4); - Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[4].ScheduledOperationId is 0); - Assert.True(!trace[4].BooleanChoice.HasValue); - Assert.True(trace[4].IntegerChoice.HasValue); - Assert.True(trace[4].IntegerChoice.Value is 5); + Assert.True(trace[4] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Current is 1); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 1); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Value is 5); } [Fact(Timeout = 5000)] @@ -180,17 +180,17 @@ namespace Microsoft.Coyote.Runtime.Tests ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(2, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); + trace.AddNondeterministicBooleanDecision(2, 2, true); this.LogTrace(trace); Assert.True(trace.Length is 3); ExecutionTrace other = ExecutionTrace.Create(); Assert.True(other.Length is 0); - other.AddSchedulingChoice(0, SchedulingPointType.Default); - other.AddSchedulingChoice(2, SchedulingPointType.Default); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); this.LogTrace(other); Assert.True(other.Length is 2); @@ -199,23 +199,24 @@ namespace Microsoft.Coyote.Runtime.Tests Assert.True(trace.Length is 3); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.SchedulingStep); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).SequenceId is 0); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[1].ScheduledOperationId is 2); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(!trace[1].IntegerChoice.HasValue); + Assert.True(trace[1] is ExecutionTrace.SchedulingStep); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).SequenceId is 2); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[2].ScheduledOperationId is 0); - Assert.True(trace[2].BooleanChoice.HasValue); - Assert.True(trace[2].BooleanChoice.Value is true); - Assert.True(!trace[2].IntegerChoice.HasValue); + Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Current is 2); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 2); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true); } [Fact(Timeout = 5000)] @@ -224,20 +225,20 @@ namespace Microsoft.Coyote.Runtime.Tests ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(2, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); + trace.AddNondeterministicBooleanDecision(2, 2, true); this.LogTrace(trace); Assert.True(trace.Length is 3); ExecutionTrace other = ExecutionTrace.Create(); Assert.True(other.Length is 0); - other.AddSchedulingChoice(0, SchedulingPointType.Default); - other.AddSchedulingChoice(2, SchedulingPointType.Default); - other.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); - other.AddSchedulingChoice(1, SchedulingPointType.Default); - other.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); + other.AddNondeterministicBooleanDecision(2, 2, true); + other.AddSchedulingDecision(2, 2, SchedulingPointType.Default, 1, 1); + other.AddNondeterministicIntegerDecision(1, 1, 5); this.LogTrace(other); Assert.True(other.Length is 5); @@ -246,36 +247,37 @@ namespace Microsoft.Coyote.Runtime.Tests Assert.True(trace.Length is 5); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.SchedulingStep); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).SequenceId is 0); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[1].ScheduledOperationId is 2); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(!trace[1].IntegerChoice.HasValue); + Assert.True(trace[1] is ExecutionTrace.SchedulingStep); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).SequenceId is 2); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[2].ScheduledOperationId is 0); - Assert.True(trace[2].BooleanChoice.HasValue); - Assert.True(trace[2].BooleanChoice.Value is true); - Assert.True(!trace[2].IntegerChoice.HasValue); + Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Current is 2); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 2); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true); Assert.True(trace[3].Index is 3); - Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[3].ScheduledOperationId is 1); - Assert.True(!trace[3].BooleanChoice.HasValue); - Assert.True(!trace[3].IntegerChoice.HasValue); + Assert.True(trace[3] is ExecutionTrace.SchedulingStep); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Current is 2); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 2); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).SequenceId is 1); Assert.True(trace[4].Index is 4); - Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[4].ScheduledOperationId is 0); - Assert.True(!trace[4].BooleanChoice.HasValue); - Assert.True(trace[4].IntegerChoice.HasValue); - Assert.True(trace[4].IntegerChoice.Value is 5); + Assert.True(trace[4] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Current is 1); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 1); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Value is 5); } [Fact(Timeout = 5000)] @@ -284,9 +286,9 @@ namespace Microsoft.Coyote.Runtime.Tests ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(3, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(false, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 3, 3); + trace.AddNondeterministicBooleanDecision(3, 3, false); this.LogTrace(trace); Assert.True(trace.Length is 3); @@ -305,17 +307,17 @@ namespace Microsoft.Coyote.Runtime.Tests ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(3, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 3, 3); + trace.AddNondeterministicBooleanDecision(3, 3, true); this.LogTrace(trace); Assert.True(trace.Length is 3); ExecutionTrace other = ExecutionTrace.Create(); Assert.True(other.Length is 0); - other.AddSchedulingChoice(0, SchedulingPointType.Default); - other.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + other.AddNondeterministicIntegerDecision(0, 0, 5); this.LogTrace(other); Assert.True(other.Length is 2); @@ -324,17 +326,17 @@ namespace Microsoft.Coyote.Runtime.Tests Assert.True(trace.Length is 2); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.SchedulingStep); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).SequenceId is 0); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[1].ScheduledOperationId is 0); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(trace[1].IntegerChoice.HasValue); - Assert.True(trace[1].IntegerChoice.Value is 5); + Assert.True(trace[1] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).Value is 5); } [Fact(Timeout = 5000)] @@ -343,20 +345,20 @@ namespace Microsoft.Coyote.Runtime.Tests ExecutionTrace trace = ExecutionTrace.Create(); Assert.True(trace.Length is 0); - trace.AddSchedulingChoice(0, SchedulingPointType.Default); - trace.AddSchedulingChoice(2, SchedulingPointType.Default); - trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + trace.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 2, 2); + trace.AddNondeterministicBooleanDecision(2, 2, true); this.LogTrace(trace); Assert.True(trace.Length is 3); ExecutionTrace other = ExecutionTrace.Create(); Assert.True(other.Length is 0); - other.AddSchedulingChoice(0, SchedulingPointType.Default); - other.AddSchedulingChoice(3, SchedulingPointType.Default); - other.AddNondeterministicBooleanChoice(false, SchedulingPointType.Default); - other.AddSchedulingChoice(1, SchedulingPointType.Default); - other.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 0, 0); + other.AddSchedulingDecision(0, 0, SchedulingPointType.Default, 3, 3); + other.AddNondeterministicBooleanDecision(3, 3, false); + other.AddSchedulingDecision(3, 3, SchedulingPointType.Default, 1, 1); + other.AddNondeterministicIntegerDecision(1, 1, 5); this.LogTrace(other); Assert.True(other.Length is 5); @@ -365,36 +367,37 @@ namespace Microsoft.Coyote.Runtime.Tests Assert.True(trace.Length is 5); Assert.True(trace[0].Index is 0); - Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[0].ScheduledOperationId is 0); - Assert.True(!trace[0].BooleanChoice.HasValue); - Assert.True(!trace[0].IntegerChoice.HasValue); + Assert.True(trace[0] is ExecutionTrace.SchedulingStep); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0); + Assert.True((trace[0] as ExecutionTrace.SchedulingStep).SequenceId is 0); Assert.True(trace[1].Index is 1); - Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[1].ScheduledOperationId is 3); - Assert.True(!trace[1].BooleanChoice.HasValue); - Assert.True(!trace[1].IntegerChoice.HasValue); + Assert.True(trace[1] is ExecutionTrace.SchedulingStep); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Current is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 0); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 3); + Assert.True((trace[1] as ExecutionTrace.SchedulingStep).SequenceId is 3); Assert.True(trace[2].Index is 2); - Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[2].ScheduledOperationId is 0); - Assert.True(trace[2].BooleanChoice.HasValue); - Assert.True(trace[2].BooleanChoice.Value is false); - Assert.True(!trace[2].IntegerChoice.HasValue); + Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Current is 3); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).CurrentSequenceId is 3); + Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is false); Assert.True(trace[3].Index is 3); - Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice); - Assert.True(trace[3].ScheduledOperationId is 1); - Assert.True(!trace[3].BooleanChoice.HasValue); - Assert.True(!trace[3].IntegerChoice.HasValue); + Assert.True(trace[3] is ExecutionTrace.SchedulingStep); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Current is 3); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).CurrentSequenceId is 3); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1); + Assert.True((trace[3] as ExecutionTrace.SchedulingStep).SequenceId is 1); Assert.True(trace[4].Index is 4); - Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice); - Assert.True(trace[4].ScheduledOperationId is 0); - Assert.True(!trace[4].BooleanChoice.HasValue); - Assert.True(trace[4].IntegerChoice.HasValue); - Assert.True(trace[4].IntegerChoice.Value is 5); + Assert.True(trace[4] is ExecutionTrace.IntegerChoiceStep); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Current is 1); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).CurrentSequenceId is 1); + Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Value is 5); } private void LogTrace(ExecutionTrace trace) diff --git a/Tests/Tests.Runtime/Logging/TestingEngineLoggingTests.cs b/Tests/Tests.Runtime/Logging/TestingEngineLoggingTests.cs index 13a2ec17..4be1f9d2 100644 --- a/Tests/Tests.Runtime/Logging/TestingEngineLoggingTests.cs +++ b/Tests/Tests.Runtime/Logging/TestingEngineLoggingTests.cs @@ -80,11 +80,11 @@ namespace Microsoft.Coyote.Runtime.Tests.Logging "[coyote::report] Testing statistics:", "[coyote::report] Found 2 bugs.", "[coyote::report] Scheduling statistics:", - "[coyote::report] Explored 2 schedules: 2 fair and 0 unfair.", - "[coyote::report] Found 100.00% buggy schedules.", - "[coyote::report] Controlled 2 operations: 1 (), 1 (), 1 ().", + "[coyote::report] Explored 2 execution paths: 2 fair, 0 unfair, 1 unique.", + "[coyote::report] Found 100.00% buggy execution paths.", + "[coyote::report] Controlled 2 operations: 1 (), 1 (), 1 (), 1 ().", "[coyote::report] Degree of operation grouping: 1 (), 1 (), 1 ().", - "[coyote::report] Number of scheduling decisions in fair terminating schedules: 0 (), 0 (), 0 ()."); + "[coyote::report] Number of scheduling decisions in fair terminating execution paths: 0 (), 0 (), 0 ()."); this.TestOutput.WriteLine($"Observed (length: {observed.Length}):"); this.TestOutput.WriteLine(observed); Assert.Equal(expectedObserved, observed); @@ -158,11 +158,11 @@ namespace Microsoft.Coyote.Runtime.Tests.Logging "[coyote::report] Testing statistics:", "[coyote::report] Found 2 bugs.", "[coyote::report] Scheduling statistics:", - "[coyote::report] Explored 2 schedules: 2 fair and 0 unfair.", - "[coyote::report] Found 100.00% buggy schedules.", - "[coyote::report] Controlled 2 operations: 1 (), 1 (), 1 ().", + "[coyote::report] Explored 2 execution paths: 2 fair, 0 unfair, 1 unique.", + "[coyote::report] Found 100.00% buggy execution paths.", + "[coyote::report] Controlled 2 operations: 1 (), 1 (), 1 (), 1 ().", "[coyote::report] Degree of operation grouping: 1 (), 1 (), 1 ().", - "[coyote::report] Number of scheduling decisions in fair terminating schedules: 0 (), 0 (), 0 ()."); + "[coyote::report] Number of scheduling decisions in fair terminating execution paths: 0 (), 0 (), 0 ()."); this.TestOutput.WriteLine($"Observed (length: {observed.Length}):"); this.TestOutput.WriteLine(observed); Assert.Equal(expectedObserved, observed); @@ -232,11 +232,11 @@ namespace Microsoft.Coyote.Runtime.Tests.Logging "[coyote::report] Testing statistics:", "[coyote::report] Found 2 bugs.", "[coyote::report] Scheduling statistics:", - "[coyote::report] Explored 2 schedules: 2 fair and 0 unfair.", - "[coyote::report] Found 100.00% buggy schedules.", - "[coyote::report] Controlled 2 operations: 1 (), 1 (), 1 ().", + "[coyote::report] Explored 2 execution paths: 2 fair, 0 unfair, 1 unique.", + "[coyote::report] Found 100.00% buggy execution paths.", + "[coyote::report] Controlled 2 operations: 1 (), 1 (), 1 (), 1 ().", "[coyote::report] Degree of operation grouping: 1 (), 1 (), 1 ().", - "[coyote::report] Number of scheduling decisions in fair terminating schedules: 0 (), 0 (), 0 ()."); + "[coyote::report] Number of scheduling decisions in fair terminating execution paths: 0 (), 0 (), 0 ()."); this.TestOutput.WriteLine($"Observed (length: {observed.Length}):"); this.TestOutput.WriteLine(observed); Assert.Equal(expectedObserved, observed);