progress

Source/Core/Runtime/CoyoteRuntime.cs

@@ -918,6 +918,7 @@ namespace Microsoft.Coyote.Runtime
         internal void DelayOperation()
         {
             int delay = 0;
+            AsyncOperation current = null;
             lock (this.SyncObject)
             {
                 if (!this.IsAttached)
@@ -925,7 +926,7 @@ namespace Microsoft.Coyote.Runtime
                     throw new ThreadInterruptedException();
                 }
 
-                var current = this.GetExecutingOperation<AsyncOperation>();
+                current = this.GetExecutingOperation<AsyncOperation>();
                 if (current != null)
                 {
                     // Choose the next delay to inject. The value is in milliseconds.
@@ -935,10 +936,13 @@ namespace Microsoft.Coyote.Runtime
                 }
             }
 
-            if (delay > 0)
+            // Only sleep the executing operation if a non-zero delay was .
+            if (delay > 0 && current != null)
             {
-                // Only sleep if a non-zero delay was chosen.
+                var previousStatus = current.Status;
+                current.Status = AsyncOperationStatus.Delayed;
                 Thread.Sleep(delay);
+                current.Status = previousStatus;
             }
         }
 
@@ -1030,7 +1034,7 @@ namespace Microsoft.Coyote.Runtime
 
                 // Choose the next delay to inject.
                 int maxDelay = maxValue > 0 ? (int)this.Configuration.TimeoutDelay : 1;
-                if (!this.Scheduler.GetNextDelay(op, maxDelay, out int next))
+                if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, out int next))
                 {
                     this.Detach(SchedulerDetachmentReason.BoundReached);
                 }
@@ -1251,7 +1255,7 @@ namespace Microsoft.Coyote.Runtime
         /// This operation is thread safe because the systematic testing
         /// runtime serializes the execution.
         /// </remarks>
-        internal IEnumerable<AsyncOperation> GetRegisteredOperations()
+        private IEnumerable<AsyncOperation> GetRegisteredOperations()
         {
             lock (this.SyncObject)
             {

Source/Core/Runtime/Scheduling/OperationScheduler.cs

@@ -164,12 +164,13 @@ namespace Microsoft.Coyote.Runtime
         /// <summary>
         /// Returns the next delay.
         /// </summary>
+        /// <param name="ops">Operations executing during the current test iteration.</param>
         /// <param name="current">The operation requesting the delay.</param>
         /// <param name="maxValue">The max value.</param>
         /// <param name="next">The next delay.</param>
         /// <returns>True if there is a next delay, else false.</returns>
-        internal bool GetNextDelay(AsyncOperation current, int maxValue, out int next) =>
-            (this.Strategy as FuzzingStrategy).GetNextDelay(current, maxValue, out next);
+        internal bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current, int maxValue, out int next) =>
+            (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, out next);
 
         /// <summary>
         /// Returns a description of the scheduling strategy in text format.

Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Concurrent;
+using System.Collections.Generic;
 using Microsoft.Coyote.Runtime;
 
 namespace Microsoft.Coyote.Testing.Fuzzing
@@ -55,7 +56,8 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         /// The delay has an injection probability of 0.05 and is in the range of [10, maxValue * 10]
         /// with an increment of 10 and an upper bound of 5000ms per operation.
         /// </remarks>
-        internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+        internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
+            int maxValue, out int next)
         {
             Guid id = this.GetOperationId();
 

Source/Core/Testing/Fuzzing/FuzzingStrategy.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Concurrent;
+using System.Collections.Generic;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Runtime;
@@ -52,11 +53,13 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         /// <summary>
         /// Returns the next delay.
         /// </summary>
+        /// <param name="ops">Operations executing during the current test iteration.</param>
         /// <param name="current">The operation requesting the delay.</param>
         /// <param name="maxValue">The max value.</param>
         /// <param name="next">The next delay.</param>
         /// <returns>True if there is a next delay, else false.</returns>
-        internal abstract bool GetNextDelay(AsyncOperation current, int maxValue, out int next);
+        internal abstract bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
+            int maxValue, out int next);
 
         /// <summary>
         /// Returns the current operation id.

Source/Core/Testing/Fuzzing/PCTStrategy.cs

@@ -77,7 +77,8 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         }
 
         /// <inheritdoc/>
-        internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+        internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
+            int maxValue, out int next)
         {
             Guid id = this.GetOperationId();
 

Source/Core/Testing/Fuzzing/QLearningStrategy.cs

@@ -26,11 +26,6 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         /// </summary>
         private readonly LinkedList<(int delay, int state)> ExecutionPath;
 
-        /// <summary>
-        /// Map of operation ids to their current activity status.
-        /// </summary>
-        private readonly ConcurrentDictionary<string, ActivityStatus> ActivityStatusMap;
-
         /// <summary>
         /// The previously chosen delay.
         /// </summary>
@@ -65,7 +60,6 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         {
             this.OperationQTable = new Dictionary<int, Dictionary<int, double>>();
             this.ExecutionPath = new LinkedList<(int, int)>();
-            this.ActivityStatusMap = new ConcurrentDictionary<string, ActivityStatus>();
             this.PreviousDelay = 0;
             this.LearningRate = 0.3;
             this.Gamma = 0.7;
@@ -74,9 +68,10 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         }
 
         /// <inheritdoc/>
-        internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+        internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
+            int maxValue, out int next)
         {
-            int state = this.CaptureExecutionStep(current);
+            int state = this.CaptureExecutionStep(ops, current);
             this.InitializeDelayQValues(state, maxValue);
 
             next = this.GetNextDelayByPolicy(state, maxValue);
@@ -86,14 +81,6 @@ namespace Microsoft.Coyote.Testing.Fuzzing
             return true;
         }
 
-        // /// <summary>
-        // /// Notifies the activity status of the current operation.
-        // /// </summary>
-        // // internal override void NotifyActivityStatus(AsyncOperation current, ActivityStatus status)
-        // // {
-        // //     this.ActivityStatusMap.AddOrUpdate(current.Name, status, (id, old) => status);
-        // // }
-
         /// <summary>
         /// Returns the next delay by drawing from the probability distribution
         /// over the specified state and range of delays.
@@ -167,10 +154,16 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         /// Captures metadata related to the current execution step, and returns
         /// a value representing the current program state.
         /// </summary>
-        private int CaptureExecutionStep(AsyncOperation operation)
+        private int CaptureExecutionStep(IEnumerable<AsyncOperation> ops, AsyncOperation operation)
         {
             int state = ComputeStateHash(operation);
 
+            Console.WriteLine($">---> {operation.Name}: state: {state}");
+            foreach (var op in ops)
+            {
+                Console.WriteLine($"  |---> {op.Name}: status: {op.Status}");
+            }
+
             // Update the list of chosen delays with the current state.
             this.ExecutionPath.AddLast((this.PreviousDelay, state));
             return state;
@@ -188,7 +181,7 @@ namespace Microsoft.Coyote.Testing.Fuzzing
                 // Add the hash of the current operation.
                 hash = (hash * 31) + operation.Name.GetHashCode();
 
-                // foreach (var kvp in this.ActivityStatusMap)
+                // foreach (var kvp in this.OperationStatusMap)
                 // {
                 //     // Console.WriteLine($">>>>>>> Hashing: id {kvp.Key} - status {kvp.Value}");
                 //     // int operationHash = 31 + kvp.Key.GetHashCode();
@@ -240,13 +233,13 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         /// </summary>
         private void LearnQValues()
         {
-            var pathBuilder = new System.Text.StringBuilder();
+            // var pathBuilder = new System.Text.StringBuilder();
 
             int idx = 0;
             var node = this.ExecutionPath.First;
             while (node?.Next != null)
             {
-                pathBuilder.Append($"{node.Value.delay},");
+                // pathBuilder.Append($"({node.Value.delay},{node.Value.state}), ");
 
                 var (_, state) = node.Value;
                 var (nextDelay, nextState) = node.Next.Value;
@@ -284,16 +277,12 @@ namespace Microsoft.Coyote.Testing.Fuzzing
                 node = node.Next;
                 idx++;
             }
+
+            Console.WriteLine($"Visited {this.OperationQTable.Count} states.");
+            // Console.WriteLine(pathBuilder.ToString());
         }
 
         /// <inheritdoc/>
         internal override string GetDescription() => $"RL[seed '{this.RandomValueGenerator.Seed}']";
-
-        private enum ActivityStatus
-        {
-            ActiveAwake,
-            ActiveSleeping,
-            Inactive
-        }
     }
 }

Source/Core/Testing/Fuzzing/RandomStrategy.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using Microsoft.Coyote.Runtime;
 
 namespace Microsoft.Coyote.Testing.Fuzzing
@@ -42,7 +43,8 @@ namespace Microsoft.Coyote.Testing.Fuzzing
         }
 
         /// <inheritdoc/>
-        internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+        internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
+            int maxValue, out int next)
         {
             next = this.RandomValueGenerator.Next(maxValue);
             this.StepCount++;

Source/Core/Testing/Systematic/QLearningStrategy.cs

@@ -359,14 +359,10 @@ namespace Microsoft.Coyote.Testing.Systematic
         /// </summary>
         private void LearnQValues()
         {
-            var pathBuilder = new System.Text.StringBuilder();
-
             int idx = 0;
             var node = this.ExecutionPath.First;
             while (node?.Next != null)
             {
-                pathBuilder.Append($"{node.Value.op},");
-
                 var (_, _, state) = node.Value;
                 var (nextOp, nextType, nextState) = node.Next.Value;