Task.Delay 不适用于 Microsoft.Coyote

Question

我有一个遗留项目，我想使用 Coyote 来测试它。
我需要在两次操作之间有一个延迟，Coyote 忽略了它。
如何实现这个延迟？

工具： .NET 6 Microsoft.Coyote.Core 版本=“1.7.11”

Microsoft.Coyote.Test 版本=“1.7.11”

Coyote 忽略延迟、测试持续时间少于 1 秒的示例：

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

在官方github账号上没有发现类似的问题。

Answer 1

使用 WhenAll 时，您实际上是在告诉两个 WriteWithDelayAsync 命令同时启动。这样想吧：

您告诉主线程它应该等待以下任务的完成：task1 和task2。当两者都完成后，由于您正在等待它，因此它将在两者都完成后继续。但是，这将同时启动这两个任务。先执行任务 1，然后执行任务 2 的方法是等待这两个任务。即：

    var startDate = DateTime.Now;
    await WriteWithDelayAsync(3);
    await WriteWithDelayAsync(5);

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