使用Microsoft.Coyote时Task.Delay失效问题求助

原因分析 #

Microsoft.Coyote在系统性测试模式下，会自动虚拟化Task.Delay和Thread.Sleep这类延迟操作，目的是加速测试执行、避免真实等待消耗时间。这就是你看到测试时长不足1秒的核心原因——所有延迟都被Coyote拦截跳过了。

解决方案 #

方案一：使用Coyote可控延迟API #

替换原有Task.Delay和Thread.Sleep为Coyote提供的Runtime API，既可以让延迟在测试中生效，同时保留Coyote对延迟的可控性（比如模型检查时可快速推进）。

修改后的代码示例：

using Microsoft.Coyote.Runtime;

public class Program
{
    public static int Value = 0;

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

    public static async Task WriteWithDelayAsync(int value)
    {
        // 替换Task.Delay为Coyote的异步延迟API
        await RuntimeProvider.Current.SleepAsync(5000);
        Value = value;
        // 替换Thread.Sleep为Coyote的同步延迟API
        RuntimeProvider.Current.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}");
    }
}

方案二：禁用延迟虚拟化 #

如果需要完全保留原有代码中的Task.Delay和Thread.Sleep，可以通过测试配置禁用Coyote的延迟虚拟化功能，此时延迟会真实执行，测试时长会符合预期。

修改测试方法的特性配置：

[Microsoft.Coyote.SystematicTesting.Test(Configuration = "EnableUncontrolledDelay=true")]
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}");
}

方案对比 #

• 方案一：推荐用于大多数场景，Coyote依然可以对延迟进行管控，在模型检查时能灵活调整执行节奏，同时支持真实延迟测试。
• 方案二：仅适合需要验证真实延迟行为的场景，测试时长会显著增加，且丢失Coyote对延迟的虚拟化控制能力。

内容的提问来源于stack exchange，提问作者Max.Lesnov