Task.Delay does not work with Microsoft.Coyote

Question

I have a legacy project and I want to test it using Coyote.
I need a delay between two operations, Coyote ignores it.
How to make this delay?

Tools: .NET 6 Microsoft.Coyote.Core Version="1.7.11"

Microsoft.Coyote.Test Version="1.7.11"

Example where Coyote ignores the delay, duration of the test less that 1 sec:

    public class Program
    {
        public static int Value = 0;

        public static async Task Main(string[] args)
        {
            await MyTest();
        }

        public static async Task WriteWithDelayAsync(int value)
        {
            await Task.Delay(5000);
            Value = value;
            Thread.Sleep(5000);
        }

        [Microsoft.Coyote.SystematicTesting.Test]
        public static async Task MyTest()
        {
            var startDate = DateTime.Now;
            Task task1 = WriteWithDelayAsync(3);
            Task task2 = WriteWithDelayAsync(5);

            await Task.WhenAll(task1, task2);

            Console.WriteLine($">>> Duration: {(DateTime.Now - startDate).TotalSeconds} sec, Value={Value}");
        }
    }

Did not find any similar issues on official github account.

Answer 1

Note that during a Coyote test the absolute value of any Delay is ignored. Instead, the only thing that is important to Coyote is that a task switch is possible because of the delay, so it becomes what Coyote calls a SchedulingPoint. This way Coyote is sure to explore all possible task interleavings, but it can also run millions of those tests per second exactly because it is ignoring your delay absolute values.