deterministic creation sequence id for operations (#448)

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;
                 }

Source/Core/Coverage/CoverageInfo.cs

@@ -53,12 +53,23 @@ namespace Microsoft.Coyote.Coverage
         [DataMember]
         public Dictionary<string, Dictionary<string, long>> SchedulingPointStackTraces { get; private set; }
 
+        /// <summary>
+        /// Set of explored paths represented as ordered operations identified by their creation sequence ids.
+        /// </summary>
+        [DataMember]
+        public HashSet<string> ExploredPaths { get; private set; }
+
         /// <summary>
         /// Set of visited program states represented as hashes.
         /// </summary>
         [DataMember]
         public HashSet<int> VisitedStates { get; private set; }
 
+        /// <summary>
+        /// Set of encountered operation creation sequence ids.
+        /// </summary>
+        public HashSet<ulong> OperationSequenceIds { get; private set; }
+
         /// <summary>
         /// Initializes a new instance of the <see cref="CoverageInfo"/> class.
         /// </summary>
@@ -68,7 +79,9 @@ namespace Microsoft.Coyote.Coverage
             this.MonitorsToStates = new Dictionary<string, HashSet<string>>();
             this.RegisteredMonitorEvents = new Dictionary<string, HashSet<string>>();
             this.SchedulingPointStackTraces = new Dictionary<string, Dictionary<string, long>>();
+            this.ExploredPaths = new HashSet<string>();
             this.VisitedStates = new HashSet<int>();
+            this.OperationSequenceIds = new HashSet<ulong>();
         }
 
         /// <summary>
@@ -141,11 +154,21 @@ namespace Microsoft.Coyote.Coverage
             }
         }
 
+        /// <summary>
+        /// Declares a new explored execution path.
+        /// </summary>
+        internal void DeclareExploredExecutionPath(string path) => this.ExploredPaths.Add(path);
+
         /// <summary>
         /// Declares a new visited state.
         /// </summary>
         internal void DeclareVisitedState(int state) => this.VisitedStates.Add(state);
 
+        /// <summary>
+        /// Declares a new operation creation sequence id.
+        /// </summary>
+        internal void DeclareOperationSequenceId(ulong sequenceId) => this.OperationSequenceIds.Add(sequenceId);
+
         /// <summary>
         /// Loads the coverage info XML file into a <see cref="CoverageInfo"/> object of the specified type.
         /// </summary>
@@ -246,7 +269,9 @@ namespace Microsoft.Coyote.Coverage
                 }
             }
 
+            this.ExploredPaths.UnionWith(coverageInfo.ExploredPaths);
             this.VisitedStates.UnionWith(coverageInfo.VisitedStates);
+            this.OperationSequenceIds.UnionWith(coverageInfo.OperationSequenceIds);
         }
     }
 }

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 <see cref="ControlledOperation"/>,
         /// or null if no such operation is executing.
         /// </summary>
+        /// <remarks>
+        /// Invoking this method checks if the current thread is uncontrolled or not.
+        /// </remarks>
         internal ControlledOperation GetExecutingOperation()
         {
             using (SynchronizedSection.Enter(this.RuntimeLock))
@@ -1418,6 +1423,9 @@ namespace Microsoft.Coyote.Runtime
         /// Returns the currently executing <see cref="ControlledOperation"/> of the
         /// specified type, or null if no such operation is executing.
         /// </summary>
+        /// <remarks>
+        /// Invoking this method checks if the current thread is uncontrolled or not.
+        /// </remarks>
         internal TControlledOperation GetExecutingOperation<TControlledOperation>()
             where TControlledOperation : ControlledOperation
         {
@@ -1433,6 +1441,18 @@ namespace Microsoft.Coyote.Runtime
             }
         }
 
+        /// <summary>
+        /// Returns the currently executing <see cref="ControlledOperation"/>,
+        /// or null if no such operation is executing.
+        /// </summary>
+        internal ControlledOperation GetExecutingOperationUnsafe()
+        {
+            using (SynchronizedSection.Enter(this.RuntimeLock))
+            {
+                return ExecutingOperation;
+            }
+        }
+
         /// <summary>
         /// Tries to return the currently executing <see cref="ControlledOperation"/>,
         /// 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();
 

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();
 
         /// <summary>
-        /// Adds a scheduling choice.
+        /// Adds a scheduling decision.
         /// </summary>
-        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);
+
+        /// <summary>
+        /// Adds a scheduling decision.
+        /// </summary>
+        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);
         }
 
         /// <summary>
-        /// Adds a nondeterministic boolean choice.
+        /// Adds a nondeterministic boolean decision.
         /// </summary>
-        internal void AddNondeterministicBooleanChoice(bool choice, SchedulingPointType sp)
+        internal void AddNondeterministicBooleanDecision(ControlledOperation current, bool value) =>
+            this.AddNondeterministicBooleanDecision(current.Id, current.SequenceId, value);
+
+        /// <summary>
+        /// Adds a nondeterministic boolean decision.
+        /// </summary>
+        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);
         }
 
         /// <summary>
-        /// Adds a nondeterministic integer choice.
+        /// Adds a nondeterministic integer decision.
         /// </summary>
-        internal void AddNondeterministicIntegerChoice(int choice, SchedulingPointType sp)
+        internal void AddNondeterministicIntegerDecision(ControlledOperation current, int value) =>
+            this.AddNondeterministicIntegerDecision(current.Id, current.SequenceId, value);
+
+        /// <summary>
+        /// Adds a nondeterministic integer decision.
+        /// </summary>
+        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();
 
         /// <summary>
-        /// 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.
         /// </summary>
-        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();
         }
 
         /// <summary>
         /// Contains metadata related to a single execution step.
         /// </summary>
-        internal sealed class Step : IEquatable<Step>, IComparable<Step>
+        internal abstract class Step : IEquatable<Step>, IComparable<Step>
         {
             /// <summary>
             /// The unique index of this execution step.
@@ -229,32 +260,14 @@ namespace Microsoft.Coyote.Runtime
             internal int Index;
 
             /// <summary>
-            /// The kind of controlled decision taken in this execution step.
+            /// The id of the currently executing operation.
             /// </summary>
-            internal DecisionKind Kind { get; private set; }
+            internal ulong Current;
 
             /// <summary>
-            /// The type of scheduling point encountered in this execution step.
+            /// The creation sequence id of the currently executing operation.
             /// </summary>
-            internal SchedulingPointType SchedulingPoint { get; private set; }
-
-            /// <summary>
-            /// The id of the scheduled operation. Only relevant if this is
-            /// a regular execution step.
-            /// </summary>
-            internal ulong ScheduledOperationId;
-
-            /// <summary>
-            /// The non-deterministic boolean choice value. Only relevant if
-            /// this is a choice execution step.
-            /// </summary>
-            internal bool? BooleanChoice;
-
-            /// <summary>
-            /// The non-deterministic integer choice value. Only relevant if
-            /// this is a choice execution step.
-            /// </summary>
-            internal int? IntegerChoice;
+            internal ulong CurrentSequenceId;
 
             /// <summary>
             /// The previous execution step.
@@ -267,74 +280,27 @@ namespace Microsoft.Coyote.Runtime
             internal Step Next;
 
             /// <summary>
-            /// Creates an execution step.
+            /// Initializes a new instance of the <see cref="Step"/> class.
             /// </summary>
-            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;
             }
 
-            /// <summary>
-            /// Creates a nondeterministic boolean choice execution step.
-            /// </summary>
-            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;
-            }
-
-            /// <summary>
-            /// Creates a nondeterministic integer choice execution step.
-            /// </summary>
-            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;
-            }
-
-            /// <summary>
-            /// Returns the hash code for this instance.
-            /// </summary>
+            /// <inheritdoc/>
             public override int GetHashCode() => this.Index.GetHashCode();
 
             /// <summary>
             /// Indicates whether the specified <see cref="Step"/> is equal
             /// to the current <see cref="Step"/>.
             /// </summary>
-            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);
 
-            /// <summary>
-            /// Determines whether the specified object is equal to the current object.
-            /// </summary>
+            /// <inheritdoc/>
             public override bool Equals(object obj) => this.Equals(obj as Step);
 
             /// <summary>
@@ -348,6 +314,131 @@ namespace Microsoft.Coyote.Runtime
             /// <see cref="Step"/> for ordering or sorting purposes.
             /// </summary>
             int IComparable<Step>.CompareTo(Step other) => this.Index - other.Index;
+
+            /// <summary>
+            /// Returns a string that represents the execution step with all operations
+            /// identified by their creation sequence ids.
+            /// </summary>
+            public abstract string ToSequenceString();
+        }
+
+        /// <summary>
+        /// Contains metadata related to a single scheduling step.
+        /// </summary>
+        internal sealed class SchedulingStep : Step
+        {
+            /// <summary>
+            /// The type of scheduling point encountered in this execution step.
+            /// </summary>
+            internal SchedulingPointType SchedulingPoint { get; private set; }
+
+            /// <summary>
+            /// The id of the chosen operation.
+            /// </summary>
+            internal ulong Value;
+
+            /// <summary>
+            /// The creation sequence id of the chosen operation.
+            /// </summary>
+            internal ulong SequenceId;
+
+            /// <summary>
+            /// Initializes a new instance of the <see cref="SchedulingStep"/> class.
+            /// </summary>
+            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;
+            }
+
+            /// <inheritdoc/>
+            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;
+
+            /// <summary>
+            /// Returns a string that represents the execution step.
+            /// </summary>
+            public override string ToString() =>
+                $"op({this.Current}:{this.CurrentSequenceId}),sp({this.SchedulingPoint}),next({this.Value}:{this.SequenceId})";
+
+            /// <inheritdoc/>
+            public override string ToSequenceString() => $"op({this.CurrentSequenceId}),sp({this.SchedulingPoint}),next({this.SequenceId})";
+        }
+
+        /// <summary>
+        /// Contains metadata related to a single boolean choice step.
+        /// </summary>
+        internal sealed class BooleanChoiceStep : Step
+        {
+            /// <summary>
+            /// The chosen boolean value.
+            /// </summary>
+            internal bool Value;
+
+            /// <summary>
+            /// Initializes a new instance of the <see cref="BooleanChoiceStep"/> class.
+            /// </summary>
+            internal BooleanChoiceStep(int index, ulong current, ulong currentSeqId, bool value)
+                : base(index, current, currentSeqId)
+            {
+                this.Value = value;
+            }
+
+            /// <inheritdoc/>
+            internal override bool Equals(Step other) => other is BooleanChoiceStep step ?
+                this.Index == step.Index &&
+                this.Current == step.Current &&
+                this.Value == step.Value :
+                false;
+
+            /// <summary>
+            /// Returns a string that represents the execution step.
+            /// </summary>
+            public override string ToString() => $"op({this.Current}:{this.CurrentSequenceId}),bool({this.Value})";
+
+            /// <inheritdoc/>
+            public override string ToSequenceString() => $"op({this.CurrentSequenceId}),bool({this.Value})";
+        }
+
+        /// <summary>
+        /// Contains metadata related to a single integer choice step.
+        /// </summary>
+        internal sealed class IntegerChoiceStep : Step
+        {
+            /// <summary>
+            /// The chosen integer value.
+            /// </summary>
+            internal int Value;
+
+            /// <summary>
+            /// Initializes a new instance of the <see cref="IntegerChoiceStep"/> class.
+            /// </summary>
+            internal IntegerChoiceStep(int index, ulong current, ulong currentSeqId, int value)
+                : base(index, current, currentSeqId)
+            {
+                this.Value = value;
+            }
+
+            /// <inheritdoc/>
+            internal override bool Equals(Step other) => other is IntegerChoiceStep step ?
+                this.Index == step.Index &&
+                this.Current == step.Current &&
+                this.Value == step.Value :
+                false;
+
+            /// <summary>
+            /// Returns a string that represents the execution step.
+            /// </summary>
+            public override string ToString() => $"op({this.Current}:{this.CurrentSequenceId}),int({this.Value})";
+
+            /// <inheritdoc/>
+            public override string ToSequenceString() => $"op({this.CurrentSequenceId}),int({this.Value})";
         }
     }
 }

Source/Core/Runtime/Operations/ControlledOperation.cs

@@ -22,6 +22,11 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal ulong Id { get; }
 
+        /// <summary>
+        /// The creation sequence id of this operation.
+        /// </summary>
+        internal ulong SequenceId { get; }
+
         /// <summary>
         /// The name of this operation.
         /// </summary>
@@ -39,6 +44,11 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal readonly OperationGroup Group;
 
+        /// <summary>
+        /// The creation sequence of this operation.
+        /// </summary>
+        private readonly List<ulong> Sequence;
+
         /// <summary>
         /// Queue of continuations that this operation must execute before it completes.
         /// </summary>
@@ -77,6 +87,11 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal IEqualityComparer<string> LastAccessedSharedStateComparer;
 
+        /// <summary>
+        /// The count of operations created by this operation.
+        /// </summary>
+        internal ulong OperationCreationCount;
+
         /// <summary>
         /// True if the source of this operation is uncontrolled, else false.
         /// </summary>
@@ -87,6 +102,11 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal bool IsDependencyUncontrolled;
 
+        /// <summary>
+        /// The debug information of this operation.
+        /// </summary>
+        internal string DebugInfo { get; }
+
         /// <summary>
         /// True if this is the root operation, else false.
         /// </summary>
@@ -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;
         }
 
+        /// <summary>
+        /// Returns the creation sequence based on the specified parent operation.
+        /// </summary>
+        private static List<ulong> GetSequenceFromParent(ulong operationId, ControlledOperation parent)
+        {
+            var sequence = new List<ulong>();
+            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;
+        }
+
+        /// <summary>
+        /// Returns the hash of the creation sequence.
+        /// </summary>
+        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;
+        }
+
         /// <summary>
         /// Returns the hashed state of this operation for the specified policy.
         /// </summary>

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;
             }
 

Source/Core/Testing/Interleaving/DFSStrategy.cs

@@ -235,7 +235,7 @@ namespace Microsoft.Coyote.Testing.Interleaving
             else
             {
                 ncs = new List<NondetIntegerChoice>();
-                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])

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))

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
         /// </remarks>
         internal virtual void Reset() => this.StepCount = 0;
 
-        /// <summary>
-        /// Formats the error message regarding an unexpected scheduling point.
-        /// </summary>
-        private string FormatSchedulingPointReplayError(int step, SchedulingPointType expected, SchedulingPointType actual) =>
-            this.FormatReplayError(step, $"expected scheduling point '{expected}' instead of '{actual}'");
-
         /// <summary>
         /// Formats the error message.
         /// </summary>

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))

Source/Core/Testing/Interleaving/ProbabilisticRandomStrategy.cs

@@ -58,7 +58,7 @@ namespace Microsoft.Coyote.Testing.Interleaving
         /// </summary>
         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)
                 {

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<double>(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<double> 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))

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;

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<TypeReference> paramTypes = new List<TypeReference>();
-                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<TypeReference> 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<ParameterDefinition> 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];

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));

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);

Source/Test/SystematicTesting/Reports/TestReport.cs

@@ -29,16 +29,16 @@ namespace Microsoft.Coyote.SystematicTesting
         public ActorCoverageInfo CoverageInfo { get; private set; }
 
         /// <summary>
-        /// Number of explored fair schedules.
+        /// Number of explored fair execution paths.
         /// </summary>
         [DataMember]
-        public int NumOfExploredFairSchedules { get; internal set; }
+        public int NumOfExploredFairPaths { get; internal set; }
 
         /// <summary>
-        /// Number of explored unfair schedules.
+        /// Number of explored unfair execution paths.
         /// </summary>
         [DataMember]
-        public int NumOfExploredUnfairSchedules { get; internal set; }
+        public int NumOfExploredUnfairPaths { get; internal set; }
 
         /// <summary>
         /// Number of found bugs.
@@ -113,37 +113,37 @@ namespace Microsoft.Coyote.SystematicTesting
         public int TotalOperationGroupingDegree { get; internal set; }
 
         /// <summary>
-        /// The min explored scheduling steps in fair tests.
+        /// The min explored execution steps in fair tests.
         /// </summary>
         [DataMember]
         public int MinExploredFairSteps { get; internal set; }
 
         /// <summary>
-        /// The max explored scheduling steps in fair tests.
+        /// The max explored execution steps in fair tests.
         /// </summary>
         [DataMember]
         public int MaxExploredFairSteps { get; internal set; }
 
         /// <summary>
-        /// The total explored scheduling steps (across all testing iterations) in fair tests.
+        /// The total explored execution steps (across all testing iterations) in fair tests.
         /// </summary>
         [DataMember]
         public int TotalExploredFairSteps { get; internal set; }
 
         /// <summary>
-        /// The min explored scheduling steps in unfair tests.
+        /// The min explored execution steps in unfair tests.
         /// </summary>
         [DataMember]
         public int MinExploredUnfairSteps { get; internal set; }
 
         /// <summary>
-        /// The max explored scheduling steps in unfair tests.
+        /// The max explored execution steps in unfair tests.
         /// </summary>
         [DataMember]
         public int MaxExploredUnfairSteps { get; internal set; }
 
         /// <summary>
-        /// The total explored scheduling steps (across all testing iterations) in unfair tests.
+        /// The total explored execution steps (across all testing iterations) in unfair tests.
         /// </summary>
         [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<string>();
             this.UncontrolledInvocations = new HashSet<string>();
@@ -223,7 +223,7 @@ namespace Microsoft.Coyote.SystematicTesting
 
         /// <inheritdoc/>
         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);
                 }
             }
 

Source/Test/SystematicTesting/Reports/TraceReport.cs

@@ -33,9 +33,9 @@ namespace Microsoft.Coyote.SystematicTesting
         public TestSettings Settings { get; set; }
 
         /// <summary>
-        /// The controlled decisions of this trace.
+        /// The execution steps in this trace.
         /// </summary>
-        public List<string> Decisions { get; set; }
+        public List<string> Steps { get; set; }
 
         /// <summary>
         /// Constructs a <see cref="TraceReport"/> from the specified <see cref="OperationScheduler"/>
@@ -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<SchedulingPointType>(spToken.Substring(3, spToken.Length - 4));
+                        SchedulingPointType sp = Enum.Parse<SchedulingPointType>(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
         /// </summary>
         internal void ReportTrace(ExecutionTrace trace)
         {
-            this.Decisions = new List<string>();
-            for (int idx = 0; idx < trace.Length; idx++)
+            this.Steps = new List<string>();
+            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());
             }
         }
 

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);

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)

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);