added more actor rewriting tests (#79)

Scripts/run-tests.ps1

@@ -2,7 +2,7 @@ param(
     [string]$dotnet = "dotnet",
     [ValidateSet("all", "netcoreapp3.1", "net47", "net48", "net5.0")]
     [string]$framework = "all",
-    [ValidateSet("all", "actors", "actors-systematic", "systematic", "tasks", "standalone")]
+    [ValidateSet("all", "systematic", "tasks", "actors", "actors-systematic", "standalone")]
     [string]$test = "all",
     [string]$filter = "",
     [string]$logger = "",
@@ -15,10 +15,10 @@ Import-Module $PSScriptRoot/powershell/common.psm1 -Force
 $frameworks = Get-ChildItem -Path "$PSScriptRoot/../Tests/bin" | Where-Object Name -CNotIn "netstandard2.0", "netstandard2.1" | Select-Object -expand Name
 
 $targets = [ordered]@{
-    "actors" = "Tests.Actors"
-    "actors-systematic" = "Tests.Actors.SystematicTesting"
     "systematic" = "Tests.SystematicTesting"
     "tasks" = "Tests.Tasks"
+    "actors" = "Tests.Actors"
+    "actors-systematic" = "Tests.Actors.SystematicTesting"
     "standalone" = "Tests.Standalone"
 }
 
@@ -27,6 +27,38 @@ $key_file = "$PSScriptRoot/../Common/Key.snk"
 [System.Environment]::SetEnvironmentVariable('COYOTE_CLI_TELEMETRY_OPTOUT', '1')
 
 Write-Comment -prefix "." -text "Running the Coyote tests" -color "yellow"
+
+# Rewrite the systematic tests, if enabled.
+if (($test -eq "all") -or ($test -eq "systematic") -or ($test -eq "actors-systematic")) {
+    foreach ($f in $frameworks) {
+        if (($framework -ne "all") -and ($f -ne $framework)) {
+            continue
+        }
+    
+        $rewriting_target = "$PSScriptRoot/../Tests/bin/$f/rewrite.coyote.json"
+        Invoke-CoyoteTool -cmd "rewrite" -dotnet $dotnet -framework $f -target $rewriting_target -key $key_file
+            
+        # Try rewrite again to make sure we can skip a rewritten assembly and do no damage.
+        Invoke-CoyoteTool -cmd "rewrite" -dotnet $dotnet -framework $f -target $rewriting_target -key $key_file
+    }
+}
+
+# Rewrite the standalone test, if enabled.
+if (($test -eq "all") -or ($test -eq "standalone")) {
+    foreach ($f in $frameworks) {
+        if (($framework -ne "all") -and ($f -ne $framework)) {
+            continue
+        }
+    
+        $rewriting_target = "$PSScriptRoot/../Tests/bin/$f/Microsoft.Coyote.Tests.Standalone.dll"
+        Invoke-CoyoteTool -cmd "rewrite" -dotnet $dotnet -framework $f -target $rewriting_target -key $key_file
+        
+        # Try rewrite again to make sure we can skip a rewritten assembly and do no damage.
+        Invoke-CoyoteTool -cmd "rewrite" -dotnet $dotnet -framework $f -target $rewriting_target -key $key_file
+    }
+}
+
+# Run all enabled (rewritten) tests.
 foreach ($kvp in $targets.GetEnumerator()) {
     if (($test -ne "all") -and ($test -ne $($kvp.Name))) {
         continue
@@ -36,24 +68,7 @@ foreach ($kvp in $targets.GetEnumerator()) {
         if (($framework -ne "all") -and ($f -ne $framework)) {
             continue
         }
-
-        $rewriting_target = ""
-        if ($($kvp.Name) -eq "systematic") {
-            $rewriting_target = "$PSScriptRoot/../Tests/bin/$f/rewrite.coyote.json"
-        }
-        elseif ($($kvp.Name) -eq "standalone") {
-            $rewriting_target = "$PSScriptRoot/../Tests/bin/$f/Microsoft.Coyote.Tests.Standalone.dll"
-        }
-
-        if ($rewriting_target -ne "") {
-            # Rewrite the test.
-            Invoke-CoyoteTool -cmd "rewrite" -dotnet $dotnet -framework $f -target $rewriting_target -key $key_file
-            
-            # Try rewrite again to make sure we can skip a rewritten assembly and do no damage!
-            Invoke-CoyoteTool -cmd "rewrite" -dotnet $dotnet -framework $f -target $rewriting_target -key $key_file
-        }
-
-        # Run the (rewritten) test.
+        
         $target = "$PSScriptRoot/../Tests/$($kvp.Value)/$($kvp.Value).csproj"
         Invoke-DotnetTest -dotnet $dotnet -project $($kvp.Name) -target $target -filter $filter -logger $logger -framework $f -verbosity $v
     }

Source/Test/Rewriting/RewritingEngine.cs

@@ -281,13 +281,13 @@ namespace Microsoft.Coyote.Rewriting
                 if (IsAssemblyRewritten(assembly))
                 {
                     // The assembly has been already rewritten by this version of Coyote, so skip it.
-                    this.Logger.WriteLine(LogSeverity.Warning, $"..... Skipping assembly (reason: already rewritten by Coyote v{GetAssemblyRewritterVersion()})");
+                    this.Logger.WriteLine(LogSeverity.Warning, $"..... Skipping assembly with reason: already rewritten by Coyote v{GetAssemblyRewritterVersion()}");
                     return;
                 }
                 else if (IsMixedModeAssembly(assembly))
                 {
                     // Mono.Cecil does not support writing mixed-mode assemblies.
-                    this.Logger.WriteLine(LogSeverity.Warning, $"..... Skipping assembly (reason: rewriting a mixed-mode assembly is not supported)");
+                    this.Logger.WriteLine(LogSeverity.Warning, $"..... Skipping assembly with reason: rewriting a mixed-mode assembly is not supported");
                     return;
                 }
 

Tests/Tests.Actors.SystematicTesting/BaseActorSystematicTest.cs

@@ -1,18 +1,16 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-using Microsoft.Coyote.Tests.Common;
+using Microsoft.Coyote.SystematicTesting.Tests;
 using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public abstract class BaseActorSystematicTest : BaseTest
+    public abstract class BaseActorSystematicTest : BaseSystematicTest
     {
         public BaseActorSystematicTest(ITestOutputHelper output)
             : base(output)
         {
         }
-
-        protected override bool IsSystematicTest => true;
     }
 }

Tests/Tests.Actors.SystematicTesting/Creation/CreateActorIdFromNameTests.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class CreateActorIdFromNameTests : Coyote.Actors.Tests.CreateActorIdFromNameTests
+    public class CreateActorIdFromNameTests : Actors.Tests.CreateActorIdFromNameTests
     {
         public CreateActorIdFromNameTests(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Creation/CreateActorTests.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class CreateActorTests : Coyote.Actors.Tests.CreateActorTests
+    public class CreateActorTests : Actors.Tests.CreateActorTests
     {
         public CreateActorTests(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Logging/CustomActorRuntimeLogTests.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class CustomActorRuntimeLogTests : Coyote.Actors.Tests.CustomActorRuntimeLogTests
+    public class CustomActorRuntimeLogTests : Actors.Tests.CustomActorRuntimeLogTests
     {
         public CustomActorRuntimeLogTests(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Operations/EventGroupingTests.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class EventGroupingTests : Coyote.Actors.Tests.EventGroupingTests
+    public class EventGroupingTests : Actors.Tests.EventGroupingTests
     {
         public EventGroupingTests(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Operations/GetEventGroupIdTests.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class GetEventGroupIdTests : Coyote.Actors.Tests.GetEventGroupIdTests
+    public class GetEventGroupIdTests : Actors.Tests.GetEventGroupIdTests
     {
         public GetEventGroupIdTests(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Operations/LargeEventGroupTest.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class LargeEventGroupTest : Coyote.Actors.Tests.LargeEventGroupTest
+    public class LargeEventGroupTest : Actors.Tests.LargeEventGroupTest
     {
         public LargeEventGroupTest(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Runtime/ParallelTests.cs

@@ -1,191 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System;
-using System.IO;
-using System.Threading.Tasks;
-using Microsoft.Coyote.Specifications;
-using Microsoft.Coyote.SystematicTesting;
-using Xunit;
-
-namespace Microsoft.Coyote.Actors.SystematicTesting.Tests.Runtime
-{
-    public class ParallelTests
-    {
-        [Fact(Timeout = 5000)]
-        public void TestParallelTestEngines()
-        {
-            string tempDir = Path.GetTempPath();
-            string outdir1 = Path.Combine(tempDir, "Coyote", "test1");
-            string outdir2 = Path.Combine(tempDir, "Coyote", "test2");
-            string outdir3 = Path.Combine(tempDir, "Coyote", "test3");
-
-            SafeDeleteDirectory(outdir1);
-            SafeDeleteDirectory(outdir2);
-            SafeDeleteDirectory(outdir3);
-
-            var task1 = Task.Run(() =>
-            {
-                RunTest(PingPongClient.RunTest, outdir1);
-            });
-            var task2 = Task.Run(() =>
-            {
-                RunTest(PingPongClient.RunTest, outdir2);
-            });
-            var task3 = Task.Run(() =>
-            {
-                RunTest(PingPongClient.RunTest, outdir3);
-            });
-
-            Task.WaitAll(task1, task2, task3);
-
-            string[] expected = new string[]
-            {
-                "PingPongClient", "PingPongServer", "LivenessMonitor", "Init", "WaitForPong", "Pong", "Busy", "Idle"
-            };
-
-            AssertFileContainsKeywords(Path.Combine(outdir1, "foo_0.dgml"), expected);
-        }
-
-        private static void AssertFileContainsKeywords(string filename, string[] keywords)
-        {
-            string text = File.ReadAllText(filename);
-            foreach (string keyword in keywords)
-            {
-                Assert.True(text.Contains(keyword), string.Format("missing keyword '{0}' in output file: {1}", keyword, filename));
-            }
-        }
-
-        private static void SafeDeleteDirectory(string dir)
-        {
-            if (Directory.Exists(dir))
-            {
-                Directory.Delete(dir, true);
-            }
-        }
-
-        private static void RunTest(Action<IActorRuntime> test, string outdir)
-        {
-            Directory.CreateDirectory(outdir);
-            Configuration conf = Configuration.Create().WithTestingIterations(10).WithPCTStrategy(false, 10).WithActivityCoverageEnabled();
-            TestingEngine engine = TestingEngine.Create(conf, test);
-            engine.Run();
-
-            System.Threading.Thread.Sleep(2000);
-            foreach (var name in engine.TryEmitTraces(outdir, "foo"))
-            {
-                Console.WriteLine(name);
-            }
-
-            Console.WriteLine("Test complete");
-        }
-
-        [OnEventDoAction(typeof(PingPongClient.PingEvent), nameof(OnPing))]
-        public class PingPongServer : Actor
-        {
-            public class PongEvent : Event
-            {
-            }
-
-            private void OnPing(Event e)
-            {
-                if (e is PingPongClient.PingEvent pe)
-                {
-                    this.Logger.WriteLine("Server Sending Pong");
-                    this.SendEvent(pe.Client, new PongEvent());
-                }
-            }
-        }
-
-        public class PingPongClient : StateMachine
-        {
-            public class PingEvent : Event
-            {
-                public ActorId Client;
-            }
-
-            public class ConfigEvent : Event
-            {
-                public ActorId Server;
-            }
-
-            private ActorId ServerId;
-
-            [Start]
-            [OnEntry(nameof(OnInitEntry))]
-            private class Init : State
-            {
-            }
-
-            private void OnInitEntry(Event e)
-            {
-                if (e is ConfigEvent ce)
-                {
-                    this.ServerId = ce.Server;
-                }
-
-                this.Monitor<LivenessMonitor>(new LivenessMonitor.BusyEvent());
-                this.Logger.WriteLine("Client Sending ping");
-                this.SendEvent(this.ServerId, new PingEvent() { Client = this.Id });
-                this.RaiseGotoStateEvent<WaitForPong>();
-            }
-
-            [OnEntry(nameof(OnWaitForPong))]
-            [OnEventGotoState(typeof(PingPongServer.PongEvent), typeof(Pong))]
-            private class WaitForPong : State
-            {
-            }
-
-            private void OnWaitForPong()
-            {
-                this.Logger.WriteLine("Client waiting for pong");
-            }
-
-            [OnEntry(nameof(OnPongEntry))]
-            private class Pong : State
-            {
-            }
-
-            private void OnPongEntry()
-            {
-                this.Monitor<LivenessMonitor>(new LivenessMonitor.IdleEvent());
-                this.Logger.WriteLine("Pong received");
-            }
-
-            public static void RunTest(IActorRuntime runtime)
-            {
-                runtime.RegisterMonitor<LivenessMonitor>();
-                ActorId server = runtime.CreateActor(typeof(PingPongServer));
-                runtime.CreateActor(typeof(PingPongClient), new ConfigEvent() { Server = server });
-            }
-        }
-
-        private class LivenessMonitor : Monitor
-        {
-            public class BusyEvent : Event
-            {
-            }
-
-            public class IdleEvent : Event
-            {
-            }
-
-            [Start]
-            [Cold]
-            [IgnoreEvents(typeof(IdleEvent))]
-            [OnEventGotoState(typeof(BusyEvent), typeof(Busy))]
-
-            private class Idle : State
-            {
-            }
-
-            [Hot]
-            [IgnoreEvents(typeof(BusyEvent))]
-            [OnEventGotoState(typeof(IdleEvent), typeof(Idle))]
-
-            private class Busy : State
-            {
-            }
-        }
-    }
-}

Tests/Tests.Actors.SystematicTesting/StateMachines/StateInheritanceTests.cs

@@ -5,7 +5,7 @@ using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class StateInheritanceTests : Coyote.Actors.Tests.StateMachines.StateInheritanceTests
+    public class StateInheritanceTests : Actors.Tests.StateMachines.StateInheritanceTests
     {
         public StateInheritanceTests(ITestOutputHelper output)
             : base(output)

Tests/Tests.Actors.SystematicTesting/Tasks/ActorTaskCompletionSourceTests.cs

@@ -0,0 +1,237 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Threading.Tasks;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
+{
+    public class ActorTaskCompletionSourceTests : BaseActorSystematicTest
+    {
+        public ActorTaskCompletionSourceTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        private class SetupEvent : Event
+        {
+            internal readonly TaskCompletionSource<int> Tcs;
+
+            internal SetupEvent(TaskCompletionSource<int> tcs)
+            {
+                this.Tcs = tcs;
+            }
+        }
+
+        private class A1 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                var setupEvent = initialEvent as SetupEvent;
+                setupEvent.Tcs.SetResult(3);
+                await Task.CompletedTask;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestSetTaskCompletionSourceInActorInitializeAsync()
+        {
+            this.Test(async r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                r.CreateActor(typeof(A1), new SetupEvent(tcs));
+                var result = await tcs.Task;
+                Assert.Equal(3, result);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M1 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry(Event e)
+            {
+                var setupEvent = e as SetupEvent;
+                setupEvent.Tcs.SetResult(3);
+                await Task.CompletedTask;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestSetTaskCompletionSourceInStateMachineOnEntry()
+        {
+            this.Test(async r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                r.CreateActor(typeof(M1), new SetupEvent(tcs));
+                var result = await tcs.Task;
+                Assert.Equal(3, result);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        [OnEventDoAction(typeof(SetupEvent), nameof(HandleSetupEvent))]
+        private class A2 : Actor
+        {
+            private async Task HandleSetupEvent(Event e)
+            {
+                var setupEvent = e as SetupEvent;
+                setupEvent.Tcs.SetResult(3);
+                await Task.CompletedTask;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestSetTaskCompletionSourceInActorHandler()
+        {
+            this.Test(async r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                var id = r.CreateActor(typeof(A2));
+                r.SendEvent(id, new SetupEvent(tcs));
+                var result = await tcs.Task;
+                Assert.Equal(3, result);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M2 : StateMachine
+        {
+            [Start]
+            [OnEventDoAction(typeof(SetupEvent), nameof(HandleSetupEvent))]
+            private class Init : State
+            {
+            }
+
+            private async Task HandleSetupEvent(Event e)
+            {
+                var setupEvent = e as SetupEvent;
+                setupEvent.Tcs.SetResult(3);
+                await Task.CompletedTask;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestSetTaskCompletionSourceInStateMachineHandler()
+        {
+            this.Test(async r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                var id = r.CreateActor(typeof(M2));
+                r.SendEvent(id, new SetupEvent(tcs));
+                var result = await tcs.Task;
+                Assert.Equal(3, result);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class A3 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                var setupEvent = initialEvent as SetupEvent;
+                var result = await setupEvent.Tcs.Task;
+                this.Assert(result is 3);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestAwaitTaskCompletionSourceInActorInitializeAsync()
+        {
+            this.Test(r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                r.CreateActor(typeof(A3), new SetupEvent(tcs));
+                tcs.SetResult(3);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M3 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry(Event e)
+            {
+                var setupEvent = e as SetupEvent;
+                var result = await setupEvent.Tcs.Task;
+                this.Assert(result is 3);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestAwaitTaskCompletionSourceInStateMachineOnEntry()
+        {
+            this.Test(r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                r.CreateActor(typeof(M3), new SetupEvent(tcs));
+                tcs.SetResult(3);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        [OnEventDoAction(typeof(SetupEvent), nameof(HandleSetupEvent))]
+        private class A4 : Actor
+        {
+            private async Task HandleSetupEvent(Event e)
+            {
+                var setupEvent = e as SetupEvent;
+                var result = await setupEvent.Tcs.Task;
+                this.Assert(result is 3);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestAwaitTaskCompletionSourceInActorHandler()
+        {
+            this.Test(r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                var id = r.CreateActor(typeof(A4));
+                r.SendEvent(id, new SetupEvent(tcs));
+                tcs.SetResult(3);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M4 : StateMachine
+        {
+            [Start]
+            [OnEventDoAction(typeof(SetupEvent), nameof(HandleSetupEvent))]
+            private class Init : State
+            {
+            }
+
+            private async Task HandleSetupEvent(Event e)
+            {
+                var setupEvent = e as SetupEvent;
+                var result = await setupEvent.Tcs.Task;
+                this.Assert(result is 3);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestAwaitTaskCompletionSourceInStateMachineHandler()
+        {
+            this.Test(r =>
+            {
+                var tcs = new TaskCompletionSource<int>();
+                var id = r.CreateActor(typeof(M4));
+                r.SendEvent(id, new SetupEvent(tcs));
+                tcs.SetResult(3);
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+    }
+}

Tests/Tests.Actors.SystematicTesting/Tasks/ActorTaskDelayTests.cs

@@ -0,0 +1,385 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Threading.Tasks;
+using Microsoft.Coyote.Tests.Common.Events;
+using Microsoft.Coyote.Tests.Common.Tasks;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
+{
+    public class ActorTaskDelayTests : BaseActorSystematicTest
+    {
+        private static string ExpectedMethodName { get; } = $"{typeof(AsyncProvider).FullName}.{nameof(AsyncProvider.DelayAsync)}";
+
+        public ActorTaskDelayTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
+        private class A1 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await Task.Delay(10);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+
+            private void IgnoreUnitEvent()
+            {
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDelayInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A1));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M1 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            [IgnoreEvents(typeof(UnitEvent))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await Task.Delay(10);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDelayInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M1));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
+        private class A2 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await Task.Delay(10).ConfigureAwait(false);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+
+            private void IgnoreUnitEvent()
+            {
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDelayWithOtherSynchronizationContextInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M2 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            [IgnoreEvents(typeof(UnitEvent))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await Task.Delay(10).ConfigureAwait(false);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDelayWithOtherSynchronizationContextInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class A3 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                Task[] tasks = new Task[2];
+                for (int i = 0; i < 2; i++)
+                {
+                    tasks[i] = this.DelayedRandomAsync();
+                }
+
+                await Task.WhenAll(tasks);
+            }
+
+            private async Task DelayedRandomAsync()
+            {
+                await Task.Delay(10).ConfigureAwait(false);
+                this.RandomBoolean();
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDelayLoopWithOtherSynchronizationContextInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A3));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M3 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                Task[] tasks = new Task[2];
+                for (int i = 0; i < 2; i++)
+                {
+                    tasks[i] = this.DelayedRandomAsync();
+                }
+
+                await Task.WhenAll(tasks);
+            }
+
+            private async Task DelayedRandomAsync()
+            {
+                await Task.Delay(10).ConfigureAwait(false);
+                this.RandomBoolean();
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDelayLoopWithOtherSynchronizationContextInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M3));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
+        private class A4 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await AsyncProvider.DelayAsync(10);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+
+            private void IgnoreUnitEvent()
+            {
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestUncontrolledDelayInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A4));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100),
+            errorChecker: (e) =>
+            {
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
+            });
+        }
+
+        private class M4 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            [IgnoreEvents(typeof(UnitEvent))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await AsyncProvider.DelayAsync(10);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestUncontrolledDelayInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M4));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100),
+            errorChecker: (e) =>
+            {
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
+            });
+        }
+
+        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
+        private class A5 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await AsyncProvider.DelayAsync(10).ConfigureAwait(false);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+
+            private void IgnoreUnitEvent()
+            {
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestUncontrolledDelayWithOtherSynchronizationContextInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A5));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100),
+            errorChecker: (e) =>
+            {
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
+            });
+        }
+
+        private class M5 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            [IgnoreEvents(typeof(UnitEvent))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                this.SendEvent(this.Id, UnitEvent.Instance);
+                await AsyncProvider.DelayAsync(10).ConfigureAwait(false);
+                this.SendEvent(this.Id, UnitEvent.Instance);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestUncontrolledDelayWithOtherSynchronizationContextInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M5));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100),
+            errorChecker: (e) =>
+            {
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
+            });
+        }
+
+        private class A6 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                Task[] tasks = new Task[2];
+                for (int i = 0; i < 2; i++)
+                {
+                    tasks[i] = this.DelayedRandomAsync();
+                }
+
+                await Task.WhenAll(tasks);
+            }
+
+            private async Task DelayedRandomAsync()
+            {
+                await AsyncProvider.DelayAsync(10).ConfigureAwait(false);
+                this.RandomBoolean();
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestUncontrolledDelayLoopWithOtherSynchronizationContextInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A6));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100),
+            errorChecker: (e) =>
+            {
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
+            });
+        }
+
+        private class M6 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                Task[] tasks = new Task[2];
+                for (int i = 0; i < 2; i++)
+                {
+                    tasks[i] = this.DelayedRandomAsync();
+                }
+
+                await Task.WhenAll(tasks);
+            }
+
+            private async Task DelayedRandomAsync()
+            {
+                await AsyncProvider.DelayAsync(10).ConfigureAwait(false);
+                this.RandomBoolean();
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestUncontrolledDelayLoopWithOtherSynchronizationContextInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M6));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100),
+            errorChecker: (e) =>
+            {
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
+            });
+        }
+    }
+}

Tests/Tests.Actors.SystematicTesting/Tasks/ActorTaskInterleavingsTests.cs

@@ -0,0 +1,466 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Threading.Tasks;
+using Microsoft.Coyote.Tests.Common.Events;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
+{
+    public class ActorTaskInterleavingsTests : BaseActorSystematicTest
+    {
+        public ActorTaskInterleavingsTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        private static async Task WriteAsync(SharedEntry entry, int value)
+        {
+            await Task.CompletedTask;
+            entry.Value = value;
+        }
+
+        private static async Task WriteWithDelayAsync(SharedEntry entry, int value)
+        {
+            await Task.Delay(1);
+            entry.Value = value;
+        }
+
+        private class A1 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+                Task task = WriteAsync(entry, 3);
+                entry.Value = 5;
+                await task;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithOneSynchronousTaskInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A1));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200));
+        }
+
+        private class M1 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+                Task task = WriteAsync(entry, 3);
+                entry.Value = 5;
+                await task;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithOneSynchronousTaskInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M1));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200));
+        }
+
+        private class A2 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task = WriteWithDelayAsync(entry, 3);
+                entry.Value = 5;
+                await task;
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithOneAsynchronousTaskInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class M2 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task = WriteWithDelayAsync(entry, 3);
+                entry.Value = 5;
+                await task;
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithOneAsynchronousTaskInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class A3 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task = Task.Run(async () =>
+                {
+                    await WriteAsync(entry, 3);
+                });
+
+                await WriteAsync(entry, 5);
+                await task;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithOneParallelTaskInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A3));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class M3 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task = Task.Run(async () =>
+                {
+                    await WriteAsync(entry, 3);
+                });
+
+                await WriteAsync(entry, 5);
+                await task;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithOneParallelTaskInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M3));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class A4 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = WriteAsync(entry, 3);
+                Task task2 = WriteAsync(entry, 5);
+
+                await task1;
+                await task2;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithTwoSynchronousTasksInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A4));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200));
+        }
+
+        private class M4 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = WriteAsync(entry, 3);
+                Task task2 = WriteAsync(entry, 5);
+
+                await task1;
+                await task2;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithTwoSynchronousTasksInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M4));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200));
+        }
+
+        private class A5 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = WriteWithDelayAsync(entry, 3);
+                Task task2 = WriteWithDelayAsync(entry, 5);
+
+                await task1;
+                await task2;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithTwoAsynchronousTasksInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A5));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class M5 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = WriteWithDelayAsync(entry, 3);
+                Task task2 = WriteWithDelayAsync(entry, 5);
+
+                await task1;
+                await task2;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithTwoAsynchronousTasksInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M5));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class A6 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = Task.Run(async () =>
+                {
+                    await WriteAsync(entry, 3);
+                });
+
+                Task task2 = Task.Run(async () =>
+                {
+                    await WriteAsync(entry, 5);
+                });
+
+                await task1;
+                await task2;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithTwoParallelTasksInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A6));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class M6 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = Task.Run(async () =>
+                {
+                    await WriteAsync(entry, 3);
+                });
+
+                Task task2 = Task.Run(async () =>
+                {
+                    await WriteAsync(entry, 5);
+                });
+
+                await task1;
+                await task2;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithTwoParallelTasksInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M6));
+            },
+            configuration: GetConfiguration().WithTestingIterations(200),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class A7 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = Task.Run(async () =>
+                {
+                    Task task2 = Task.Run(async () =>
+                    {
+                        await WriteAsync(entry, 5);
+                    });
+
+                    await WriteAsync(entry, 3);
+                    await task2;
+                });
+
+                await task1;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithNestedParallelTasksInActor()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(A7));
+            },
+            configuration: GetConfiguration().WithTestingIterations(500),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+
+        private class M7 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+
+                Task task1 = Task.Run(async () =>
+                {
+                    Task task2 = Task.Run(async () =>
+                    {
+                        await WriteAsync(entry, 5);
+                    });
+
+                    await WriteAsync(entry, 3);
+                    await task2;
+                });
+
+                await task1;
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestInterleavingsWithNestedParallelTasksInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M7));
+            },
+            configuration: GetConfiguration().WithTestingIterations(500),
+            expectedError: "Value is 3 instead of 5.",
+            replay: true);
+        }
+    }
+}

Tests/Tests.Actors.SystematicTesting/Tasks/ActorTaskRunTests.cs

@@ -0,0 +1,193 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Threading.Tasks;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
+{
+    public class ActorTaskRunTests : BaseActorSystematicTest
+    {
+        public ActorTaskRunTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        private class A1 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+                await Task.Run(() =>
+                {
+                    entry.Value = 5;
+                });
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestTaskRunInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A1));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M1 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+                await Task.Run(() =>
+                {
+                    entry.Value = 5;
+                });
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestTaskRunInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M1));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class A2 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+                await Task.Run(async () =>
+                {
+                    await Task.Delay(100);
+                    entry.Value = 5;
+                });
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestTaskRunAsyncInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M2 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+                await Task.Run(async () =>
+                {
+                    await Task.Delay(100);
+                    entry.Value = 5;
+                });
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestTaskRunAsyncInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class A3 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                SharedEntry entry = new SharedEntry();
+                await Task.Run(async () =>
+                {
+                    await Task.Run(async () =>
+                    {
+                        await Task.Delay(100);
+                        entry.Value = 3;
+                    });
+
+                    entry.Value = 5;
+                });
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestNestedTaskRunInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A3));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M3 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                SharedEntry entry = new SharedEntry();
+                await Task.Run(async () =>
+                {
+                    await Task.Run(async () =>
+                    {
+                        await Task.Delay(100);
+                        entry.Value = 3;
+                    });
+
+                    entry.Value = 5;
+                });
+
+                AssertSharedEntryValue(entry, 5);
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestNestedTaskRunInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M3));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+    }
+}

Tests/Tests.Actors.SystematicTesting/Tasks/ActorTaskYieldTests.cs

@@ -3,14 +3,17 @@
 
 using System.Threading.Tasks;
 using Microsoft.Coyote.Tests.Common.Events;
+using Microsoft.Coyote.Tests.Common.Tasks;
 using Xunit;
 using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
 {
-    public class UncontrolledDelayTests : BaseActorSystematicTest
+    public class ActorTaskYieldTests : BaseActorSystematicTest
     {
-        public UncontrolledDelayTests(ITestOutputHelper output)
+        private static string ExpectedMethodName { get; } = $"{typeof(AsyncProvider).FullName}.{nameof(AsyncProvider.YieldAsync)}";
+
+        public ActorTaskYieldTests(ITestOutputHelper output)
             : base(output)
         {
         }
@@ -21,7 +24,7 @@ namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
             protected override async Task OnInitializeAsync(Event initialEvent)
             {
                 this.SendEvent(this.Id, UnitEvent.Instance);
-                await Task.Delay(10);
+                await Task.Yield();
                 this.SendEvent(this.Id, UnitEvent.Instance);
             }
 
@@ -31,18 +34,13 @@ namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledDelayInActor()
+        public void TestYieldInActor()
         {
-            this.TestWithError(r =>
+            this.Test(r =>
             {
                 r.CreateActor(typeof(A1));
             },
-            configuration: GetConfiguration().WithTestingIterations(100),
-            errorChecker: (e) =>
-            {
-                Assert.True(e.StartsWith("Method 'OnInitializeAsync' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
-            });
+            configuration: GetConfiguration().WithTestingIterations(100));
         }
 
         private class M1 : StateMachine
@@ -57,33 +55,94 @@ namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
             private async Task InitOnEntry()
             {
                 this.SendEvent(this.Id, UnitEvent.Instance);
-                await Task.Delay(10);
+                await Task.Yield();
                 this.SendEvent(this.Id, UnitEvent.Instance);
             }
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledDelayInStateMachine()
+        public void TestYieldInStateMachine()
         {
-            this.TestWithError(r =>
+            this.Test(r =>
             {
                 r.CreateActor(typeof(M1));
             },
-            configuration: GetConfiguration().WithTestingIterations(100),
-            errorChecker: (e) =>
-            {
-                Assert.True(e.StartsWith("Method 'InitOnEntry' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
-            });
+            configuration: GetConfiguration().WithTestingIterations(100));
         }
 
-        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
         private class A2 : Actor
+        {
+            protected override async Task OnInitializeAsync(Event initialEvent)
+            {
+                Task[] tasks = new Task[2];
+                for (int i = 0; i < 2; i++)
+                {
+                    tasks[i] = this.YieldedRandomAsync();
+                }
+
+                await Task.WhenAll(tasks);
+            }
+
+            private async Task YieldedRandomAsync()
+            {
+                await Task.Yield();
+                this.RandomBoolean();
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestYieldLoopInActor()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(A2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        private class M2 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            private class Init : State
+            {
+            }
+
+            private async Task InitOnEntry()
+            {
+                Task[] tasks = new Task[2];
+                for (int i = 0; i < 2; i++)
+                {
+                    tasks[i] = this.YieldedRandomAsync();
+                }
+
+                await Task.WhenAll(tasks);
+            }
+
+            private async Task YieldedRandomAsync()
+            {
+                await Task.Yield();
+                this.RandomBoolean();
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestYieldLoopInStateMachine()
+        {
+            this.Test(r =>
+            {
+                r.CreateActor(typeof(M2));
+            },
+            configuration: GetConfiguration().WithTestingIterations(100));
+        }
+
+        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
+        private class A3 : Actor
         {
             protected override async Task OnInitializeAsync(Event initialEvent)
             {
                 this.SendEvent(this.Id, UnitEvent.Instance);
-                await Task.Delay(10).ConfigureAwait(false);
+                await AsyncProvider.YieldAsync();
                 this.SendEvent(this.Id, UnitEvent.Instance);
             }
 
@@ -93,21 +152,20 @@ namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledDelayWithOtherSynchronizationContextInActor()
+        public void TestUncontrolledYieldInActor()
         {
             this.TestWithError(r =>
             {
-                r.CreateActor(typeof(A2));
+                r.CreateActor(typeof(A3));
             },
             configuration: GetConfiguration().WithTestingIterations(100),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Method 'OnInitializeAsync' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
             });
         }
 
-        private class M2 : StateMachine
+        private class M3 : StateMachine
         {
             [Start]
             [OnEntry(nameof(InitOnEntry))]
@@ -119,62 +177,60 @@ namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
             private async Task InitOnEntry()
             {
                 this.SendEvent(this.Id, UnitEvent.Instance);
-                await Task.Delay(10).ConfigureAwait(false);
+                await AsyncProvider.YieldAsync();
                 this.SendEvent(this.Id, UnitEvent.Instance);
             }
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledDelayWithOtherSynchronizationContextInStateMachine()
+        public void TestUncontrolledYieldInStateMachine()
         {
             this.TestWithError(r =>
             {
-                r.CreateActor(typeof(M2));
+                r.CreateActor(typeof(M3));
             },
             configuration: GetConfiguration().WithTestingIterations(100),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Method 'InitOnEntry' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
             });
         }
 
-        private class A3 : Actor
+        private class A4 : Actor
         {
             protected override async Task OnInitializeAsync(Event initialEvent)
             {
                 Task[] tasks = new Task[2];
                 for (int i = 0; i < 2; i++)
                 {
-                    tasks[i] = this.DelayedRandomAsync();
+                    tasks[i] = this.YieldedRandomAsync();
                 }
 
                 await Task.WhenAll(tasks);
             }
 
-            private async Task DelayedRandomAsync()
+            private async Task YieldedRandomAsync()
             {
-                await Task.Delay(10).ConfigureAwait(false);
+                await AsyncProvider.YieldAsync();
                 this.RandomBoolean();
             }
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledDelayLoopWithOtherSynchronizationContextInActor()
+        public void TestUncontrolledYieldLoopInActor()
         {
             this.TestWithError(r =>
             {
-                r.CreateActor(typeof(A3));
+                r.CreateActor(typeof(A4));
             },
             configuration: GetConfiguration().WithTestingIterations(100),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Method 'OnInitializeAsync' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
             });
         }
 
-        private class M3 : StateMachine
+        private class M4 : StateMachine
         {
             [Start]
             [OnEntry(nameof(InitOnEntry))]
@@ -187,31 +243,30 @@ namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
                 Task[] tasks = new Task[2];
                 for (int i = 0; i < 2; i++)
                 {
-                    tasks[i] = this.DelayedRandomAsync();
+                    tasks[i] = this.YieldedRandomAsync();
                 }
 
                 await Task.WhenAll(tasks);
             }
 
-            private async Task DelayedRandomAsync()
+            private async Task YieldedRandomAsync()
             {
-                await Task.Delay(10).ConfigureAwait(false);
+                await AsyncProvider.YieldAsync();
                 this.RandomBoolean();
             }
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledDelayLoopWithOtherSynchronizationContextInStateMachine()
+        public void TestUncontrolledYieldLoopInStateMachine()
         {
             this.TestWithError(r =>
             {
-                r.CreateActor(typeof(M3));
+                r.CreateActor(typeof(M4));
             },
             configuration: GetConfiguration().WithTestingIterations(100),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Method 'InitOnEntry' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
+                Assert.StartsWith($"Method '{ExpectedMethodName}' returned an uncontrolled task", e);
             });
         }
     }

Tests/Tests.Actors.SystematicTesting/Tests.Actors.SystematicTesting.csproj

@@ -11,6 +11,7 @@
   <Import Project="..\..\Common\key.props" />
   <ItemGroup>
     <ProjectReference Include="..\Tests.Actors\Tests.Actors.csproj" />
+    <ProjectReference Include="..\Tests.SystematicTesting\Tests.SystematicTesting.csproj" />
   </ItemGroup>
   <ItemGroup>
     <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.6.1" />

Tests/Tests.Actors.SystematicTesting/Threading/UncontrolledYieldTests.cs

@@ -1,156 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System.Threading.Tasks;
-using Microsoft.Coyote.Tests.Common.Events;
-using Xunit;
-using Xunit.Abstractions;
-
-namespace Microsoft.Coyote.Actors.SystematicTesting.Tests
-{
-    public class UncontrolledYieldTests : BaseActorSystematicTest
-    {
-        public UncontrolledYieldTests(ITestOutputHelper output)
-            : base(output)
-        {
-        }
-
-        [OnEventDoAction(typeof(UnitEvent), nameof(IgnoreUnitEvent))]
-        private class A1 : Actor
-        {
-            protected override async Task OnInitializeAsync(Event initialEvent)
-            {
-                this.SendEvent(this.Id, UnitEvent.Instance);
-                await Task.Yield();
-                this.SendEvent(this.Id, UnitEvent.Instance);
-            }
-
-            private void IgnoreUnitEvent()
-            {
-            }
-        }
-
-        [Fact(Timeout = 5000)]
-        public void TestUncontrolledYieldInActor()
-        {
-            this.TestWithError(r =>
-            {
-                r.CreateActor(typeof(A1));
-            },
-            configuration: GetConfiguration().WithTestingIterations(100),
-            errorChecker: (e) =>
-            {
-                Assert.True(e.StartsWith("Method 'OnInitializeAsync' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
-            });
-        }
-
-        private class M1 : StateMachine
-        {
-            [Start]
-            [OnEntry(nameof(InitOnEntry))]
-            [IgnoreEvents(typeof(UnitEvent))]
-            private class Init : State
-            {
-            }
-
-            private async Task InitOnEntry()
-            {
-                this.SendEvent(this.Id, UnitEvent.Instance);
-                await Task.Yield();
-                this.SendEvent(this.Id, UnitEvent.Instance);
-            }
-        }
-
-        [Fact(Timeout = 5000)]
-        public void TestUncontrolledYieldInStateMachine()
-        {
-            this.TestWithError(r =>
-            {
-                r.CreateActor(typeof(M1));
-            },
-            configuration: GetConfiguration().WithTestingIterations(100),
-            errorChecker: (e) =>
-            {
-                Assert.True(e.StartsWith("Method 'InitOnEntry' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
-            });
-        }
-
-        private class A2 : Actor
-        {
-            protected override async Task OnInitializeAsync(Event initialEvent)
-            {
-                Task[] tasks = new Task[2];
-                for (int i = 0; i < 2; i++)
-                {
-                    tasks[i] = this.YieldedRandomAsync();
-                }
-
-                await Task.WhenAll(tasks);
-            }
-
-            private async Task YieldedRandomAsync()
-            {
-                await Task.Yield();
-                this.RandomBoolean();
-            }
-        }
-
-        [Fact(Timeout = 5000)]
-        public void TestUncontrolledYieldLoopInActor()
-        {
-            this.TestWithError(r =>
-            {
-                r.CreateActor(typeof(A2));
-            },
-            configuration: GetConfiguration().WithTestingIterations(100),
-            errorChecker: (e) =>
-            {
-                Assert.True(e.StartsWith("Method 'OnInitializeAsync' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
-            });
-        }
-
-        private class M2 : StateMachine
-        {
-            [Start]
-            [OnEntry(nameof(InitOnEntry))]
-            private class Init : State
-            {
-            }
-
-            private async Task InitOnEntry()
-            {
-                Task[] tasks = new Task[2];
-                for (int i = 0; i < 2; i++)
-                {
-                    tasks[i] = this.YieldedRandomAsync();
-                }
-
-                await Task.WhenAll(tasks);
-            }
-
-            private async Task YieldedRandomAsync()
-            {
-                await Task.Yield();
-                this.RandomBoolean();
-            }
-        }
-
-        [Fact(Timeout = 5000)]
-        public void TestUncontrolledYieldLoopInStateMachine()
-        {
-            this.TestWithError(r =>
-            {
-                r.CreateActor(typeof(M2));
-            },
-            configuration: GetConfiguration().WithTestingIterations(100),
-            errorChecker: (e) =>
-            {
-                Assert.True(e.StartsWith("Method 'InitOnEntry' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
-            });
-        }
-    }
-}

Tests/Tests.Common/Tasks/AsyncProvider.cs

@@ -13,6 +13,8 @@ namespace Microsoft.Coyote.Tests.Common.Tasks
     /// </remarks>
     public static class AsyncProvider
     {
-        public static Task DelayAsync() => Task.Delay(100);
+        public static Task DelayAsync(int duration) => Task.Delay(duration);
+
+        public static async Task YieldAsync() => await Task.Yield();
     }
 }

Tests/Tests.SystematicTesting/BaseSystematicTest.cs

@@ -3,6 +3,7 @@
 
 using System.Threading.Tasks;
 using Microsoft.Coyote.Rewriting;
+using Microsoft.Coyote.Specifications;
 using Microsoft.Coyote.Tests.Common;
 using Xunit;
 using Xunit.Abstractions;
@@ -27,6 +28,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests
             }
         }
 
+        protected static void AssertSharedEntryValue(SharedEntry entry, int expected) =>
+            Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
+
         protected class SharedEntry
         {
             public volatile int Value = 0;

Tests/Tests.SystematicTesting/Invocations/UncontrolledTaskTests.cs

@@ -19,13 +19,13 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Invocations
         {
             this.TestWithError(async () =>
             {
-                await AsyncProvider.DelayAsync();
+                await AsyncProvider.DelayAsync(100);
             },
             configuration: GetConfiguration().WithTestingIterations(100),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Method 'Microsoft.Coyote.Tests.Common.Tasks.AsyncProvider.DelayAsync' returned an uncontrolled task"),
-                    "Expected uncontrolled task from invoking the async method.");
+                string expectedMethodName = $"{typeof(AsyncProvider).FullName}.{nameof(AsyncProvider.DelayAsync)}";
+                Assert.StartsWith($"Method '{expectedMethodName}' returned an uncontrolled task", e);
             },
             replay: true);
         }

Tests/Tests.SystematicTesting/Rewriting/ConfigurationTests.cs

@@ -32,8 +32,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Configuration
             Assert.Equal(Path.Combine(configDirectory), options.OutputDirectory);
             Assert.True(options.IsReplacingAssemblies);
 
-            Assert.Single(options.AssemblyPaths);
-            Assert.Equal(Path.Combine(options.AssembliesDirectory, "Microsoft.Coyote.Tests.SystematicTesting.dll"), options.AssemblyPaths.First());
+            Assert.Equal(2, options.AssemblyPaths.Count());
+            Assert.Equal(Path.Combine(options.AssembliesDirectory, "Microsoft.Coyote.Tests.SystematicTesting.dll"),
+                options.AssemblyPaths.First());
         }
 
         [Fact(Timeout = 5000)]

Tests/Tests.SystematicTesting/Rewriting/TaskExceptionFilterTests.cs

@@ -37,17 +37,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestAddExceptionFilter()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception.
-                TestFilterMethod();
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestFilterMethod);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestFilterMethod);
         }
 
         private static void TestFilterMethod2()
@@ -66,17 +58,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestAddExceptionFilter2()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception..
-                TestFilterMethod2();
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestFilterMethod2);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestFilterMethod2);
         }
 
         private static void TestFilterMethod3()
@@ -95,17 +79,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestAddExceptionFilter3()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception.
-                TestFilterMethod3();
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestFilterMethod3);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestFilterMethod3);
         }
 
         private static void TestFilterMethod4()
@@ -191,17 +167,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestEditComplexFilter()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception..
-                this.Test(TestComplexFilterMethod);
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod);
         }
 
         private static void TestComplexFilterMethod2()
@@ -223,17 +191,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestEditComplexFilter2()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception..
-                this.Test(TestComplexFilterMethod2);
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod2);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod2);
         }
 
         private static void TestComplexFilterMethod3()
@@ -251,17 +211,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestEditComplexFilter3()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception..
-                this.Test(TestComplexFilterMethod3);
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod3);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod3);
         }
 
         private static void TestComplexFilterMethod4()
@@ -285,17 +237,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Exceptions
         [Fact(Timeout = 5000)]
         public void TestEditComplexFilter4()
         {
-            if (!this.IsSystematicTest)
-            {
-                // The non-rewritten code should catch the coyote exception.
-                this.Test(TestComplexFilterMethod4);
-            }
-            else
-            {
-                // The rewritten code should add a !(e is ExecutionCanceledException) filter
-                // which should allow this exception to escape the catch block.
-                this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod4);
-            }
+            // The rewritten code should add a !(e is ExecutionCanceledException) filter
+            // which should allow this exception to escape the catch block.
+            this.RunWithException<ExecutionCanceledException>(TestComplexFilterMethod4);
         }
 
         private static void TestRethrowMethod()

Tests/Tests.SystematicTesting/Tasks/ConfigureAwait/TaskConfigureAwaitFalseTests.cs

@@ -34,7 +34,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -46,7 +46,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -60,7 +60,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -72,7 +72,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -98,7 +98,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -110,7 +110,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -124,7 +124,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -136,7 +136,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/ConfigureAwait/TaskConfigureAwaitTrueTests.cs

@@ -34,7 +34,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -46,7 +46,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -60,7 +60,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -72,7 +72,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -98,7 +98,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -110,7 +110,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -124,7 +124,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -136,7 +136,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/ConfigureAwait/TaskRunConfigureAwaitFalseTests.cs

@@ -26,7 +26,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -42,7 +42,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -61,7 +61,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -78,7 +78,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -97,7 +97,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -114,7 +114,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -138,7 +138,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -160,7 +160,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -184,7 +184,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -206,7 +206,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/ConfigureAwait/TaskRunConfigureAwaitTrueTests.cs

@@ -26,7 +26,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -42,7 +42,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -61,7 +61,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -78,7 +78,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -97,7 +97,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -114,7 +114,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -138,7 +138,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -160,7 +160,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -184,7 +184,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -206,7 +206,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/Integration/ExtremeProgrammingChallenge14Tests.cs

@@ -123,7 +123,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             configuration: GetConfiguration().WithTestingIterations(100),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }

Tests/Tests.SystematicTesting/Tasks/Join/TaskResultTests.cs

@@ -34,7 +34,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 entry.Value = 5;
 
                 Specification.Assert(result == 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -56,7 +56,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 int result = task.Result;
 
                 Specification.Assert(result == 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -86,7 +86,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 int result = task.Result;
 
                 Specification.Assert(result == 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -116,7 +116,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 int result = task.Result;
 
                 Specification.Assert(result == 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/Join/TaskWaitAllTests.cs

@@ -36,7 +36,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = WriteAsync(entry, 5);
                 Task task2 = WriteAsync(entry, 3);
                 Task.WaitAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -52,26 +52,13 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = WriteWithDelayAsync(entry, 3);
                 Task task2 = WriteWithDelayAsync(entry, 5);
                 Task.WaitAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
             replay: true);
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestWaitAllWithTwoParallelTasks()
         {
@@ -90,8 +77,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 });
 
                 Task.WaitAll(task1, task2);
-
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -150,18 +136,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 Task.WaitAll(task1, task2);
 
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(task1.Result == 5, $"The first task result is {task1.Result} instead of 5.");
-                    Specification.Assert(task2.Result == 3, $"The second task result is {task2.Result} instead of 3.");
-                    Specification.Assert(task1.Result == task2.Result, "Results are not equal.");
-                }
-                else
-                {
-                    // production version of this test we don't know which order the tasks execute and
-                    // with statement level interleaving we can even end up with duplicate values.
-                    Specification.Assert(false, "Results are not equal.");
-                }
+                Specification.Assert(task1.Result == 5, $"The first task result is {task1.Result} instead of 5.");
+                Specification.Assert(task2.Result == 3, $"The second task result is {task2.Result} instead of 3.");
+                Specification.Assert(task1.Result == task2.Result, "Results are not equal.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Results are not equal.",
@@ -197,12 +174,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
         [Fact(Timeout = 5000)]
         public void TestWaitAllDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WaitAll` deadlocks because one of the tasks cannot complete until later.
@@ -213,7 +184,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }
@@ -221,12 +192,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
         [Fact(Timeout = 5000)]
         public void TestWaitAllWithResultsAndDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WaitAll` deadlocks because one of the tasks cannot complete until later.
@@ -237,7 +202,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }

Tests/Tests.SystematicTesting/Tasks/Join/TaskWaitAnyTests.cs

@@ -217,17 +217,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             configuration: GetConfiguration().WithTestingIterations(200));
         }
 
-        private void AssertCompleted(Task task1, Task task2)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(task1.IsCompleted && task2.IsCompleted, "One task has not completed.");
-            }
-            else
-            {
-                // production cannot guarantee this.
-                Specification.Assert(false, "One task has not completed.");
-            }
-        }
+        private void AssertCompleted(Task task1, Task task2) =>
+            Specification.Assert(task1.IsCompleted && task2.IsCompleted, "One task has not completed.");
     }
 }

Tests/Tests.SystematicTesting/Tasks/Join/TaskWaitTests.cs

@@ -33,7 +33,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 task.Wait();
                 entry.Value = 5;
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -53,7 +53,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 entry.Value = 5;
                 task.Wait();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -81,7 +81,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 entry.Value = 5;
                 task.Wait();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -109,7 +109,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 entry.Value = 5;
                 task.Wait();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -136,7 +136,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 task.Wait(10);
                 await task;
 
-                Specification.Assert(entry.Value == 3, "Value is {0} instead of 3.", entry.Value);
+                AssertSharedEntryValue(entry, 3);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -162,7 +162,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 task.Wait(tokenSource.Token);
                 await task;
 
-                Specification.Assert(entry.Value == 3, "Value is {0} instead of 3.", entry.Value);
+                AssertSharedEntryValue(entry, 3);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -188,7 +188,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 task.Wait(10, tokenSource.Token);
                 await task;
 
-                Specification.Assert(entry.Value == 3, "Value is {0} instead of 3.", entry.Value);
+                AssertSharedEntryValue(entry, 3);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }

Tests/Tests.SystematicTesting/Tasks/Join/TaskWhenAllTests.cs

@@ -30,19 +30,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             entry.Value = value;
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestWhenAllWithTwoSynchronousTasks()
         {
@@ -52,7 +39,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = WriteAsync(entry, 5);
                 Task task2 = WriteAsync(entry, 3);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -68,7 +55,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = WriteWithDelayAsync(entry, 3);
                 Task task2 = WriteWithDelayAsync(entry, 5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -94,7 +81,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 await Task.WhenAll(task1, task2);
 
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -212,7 +199,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 };
 
                 var task = whenAll();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -240,7 +227,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 };
 
                 var task = whenAll();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -361,12 +348,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
         [Fact(Timeout = 5000)]
         public void TestWhenAllDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WhenAll` deadlocks because one of the tasks cannot complete until later.
@@ -377,7 +358,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }
@@ -385,12 +366,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
         [Fact(Timeout = 5000)]
         public void TestWhenAllWithResultsAndDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WhenAll` deadlocks because one of the tasks cannot complete until later.
@@ -401,7 +376,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }

Tests/Tests.SystematicTesting/Tasks/Join/TaskWhenAnyTests.cs

@@ -29,19 +29,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             entry.Value = value;
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestWhenAnyWithTwoSynchronousTasks()
         {
@@ -52,7 +39,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task2 = WriteAsync(entry, 3);
                 Task result = await Task.WhenAny(task1, task2);
                 Specification.Assert(result.IsCompleted, "No task has completed.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -69,7 +56,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task2 = WriteWithDelayAsync(entry, 5);
                 Task result = await Task.WhenAny(task1, task2);
                 Specification.Assert(result.IsCompleted, "No task has completed.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -96,7 +83,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task result = await Task.WhenAny(task1, task2);
 
                 Specification.Assert(result.IsCompleted, "No task has completed.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -117,7 +104,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     (result.Id == task1.Id && result.Result == 5) ||
                     (result.Id == task2.Id && result.Result == 3),
                     "Found unexpected value.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -134,19 +121,8 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task<int> task2 = entry.GetWriteResultWithDelayAsync(3);
                 Task<int> result = await Task.WhenAny(task1, task2);
                 Specification.Assert(result.IsCompleted, "One task has not completed.");
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(
-                        (result.Id == task1.Id && result.Result == 5) ||
-                        (result.Id == task2.Id && result.Result == 3),
-                        "Found unexpected value.");
-                }
-                else
-                {
-                    // production cannot guarantee to hit this case even with 200 iterations
-                    Specification.Assert(result.Result == 5 || result.Result == 3, "Found invalid value.");
-                    Specification.Assert(false, "Found unexpected value.");
-                }
+                Specification.Assert((result.Id == task1.Id && result.Result == 5) ||
+                    (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Found unexpected value.",
@@ -173,18 +149,9 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task<int> result = await Task.WhenAny(task1, task2);
 
                 Specification.Assert(result.IsCompleted, "One task has not completed.");
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(
-                        (result.Id == task1.Id && result.Result == 5) ||
-                        (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
-                    Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
-                }
-                else
-                {
-                    // production version cannot guarantee tasks will run in any particular order.
-                    Specification.Assert(false, "Value is 3 instead of 5.");
-                }
+                Specification.Assert((result.Id == task1.Id && result.Result == 5) ||
+                    (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -211,19 +178,8 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task<int> result = await Task.WhenAny(task1, task2);
 
                 Specification.Assert(result.IsCompleted, "One task has not completed.");
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(
-                        (result.Id == task1.Id && result.Result == 5) ||
-                        (result.Id == task2.Id && result.Result == 3),
-                        "Found unexpected value.");
-                }
-                else
-                {
-                    // production version cannot guarantee tasks will run in any particular order.
-                    Specification.Assert(result.Result == 5 || result.Result == 3, "Unexpected value");
-                    Specification.Assert(false, "Found unexpected value.");
-                }
+                Specification.Assert((result.Id == task1.Id && result.Result == 5) ||
+                    (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Found unexpected value.",
@@ -250,7 +206,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 };
 
                 var task = whenAny();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -278,7 +234,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 };
 
                 var task = whenAll();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),

Tests/Tests.SystematicTesting/Tasks/Logging/CustomTaskLogTests.cs

@@ -73,12 +73,6 @@ Hi mom!
         [Fact(Timeout = 5000)]
         public void TestCustomTaskRuntimeLog()
         {
-            if (!this.IsSystematicTest)
-            {
-                // assembly has not been rewritten, so skip this test.
-                return;
-            }
-
             var config = GetConfiguration().WithRandomGeneratorSeed(0);
             TestingEngine engine = TestingEngine.Create(config, this.RunAsync);
 

Tests/Tests.SystematicTesting/Tasks/RandomValues/TaskRandomBooleanTests.cs

@@ -38,7 +38,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 }
 
                 await WriteAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -67,7 +67,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 }
 
                 await WriteWithDelayAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -94,7 +94,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -122,7 +122,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -150,7 +150,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -181,7 +181,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     });
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/RandomValues/TaskRandomIntegerTests.cs

@@ -38,7 +38,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 }
 
                 await WriteAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -67,7 +67,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 }
 
                 await WriteWithDelayAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -94,7 +94,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -122,7 +122,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -150,7 +150,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -181,7 +181,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     });
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/TaskDelayTests.cs

@@ -40,7 +40,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 await Task.WhenAll(tasks);
 
-                Specification.Assert(entry.Value == 2, "Value is '{0}' instead of 2.", entry.Value);
+                AssertSharedEntryValue(entry, 2);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -97,7 +97,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task = InvokeWriteWithDelayAsync(entry, 3, 0);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -111,7 +111,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task = InvokeWriteWithDelayAsync(entry, 3, 1);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -127,7 +127,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithDelayAsync(entry, 3, 0);
                 Task task2 = InvokeWriteWithDelayAsync(entry, 5, 0);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -141,7 +141,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithDelayAsync(entry, 3, 1);
                 Task task2 = InvokeWriteWithDelayAsync(entry, 5, 1);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -162,19 +162,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             configuration: GetConfiguration().WithTestingIterations(200));
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestInterleavingsInRepeatedNestedAsynchronousDelays()
         {
@@ -184,7 +171,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithDelayAsync(entry, 3, 1, true);
                 Task task2 = InvokeWriteWithDelayAsync(entry, 5, 1, true);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -207,7 +194,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = invokeWriteWithDelayAsync(3, 0);
                 Task task2 = invokeWriteWithDelayAsync(5, 0);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -228,7 +215,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = invokeWriteWithDelayAsync(3, 1);
                 Task task2 = invokeWriteWithDelayAsync(5, 1);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -249,7 +236,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithDelayAsync(3, 0);
                 Task task2 = InvokeWriteWithDelayAsync(5, 0);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -268,7 +255,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithDelayAsync(3, 1);
                 Task task2 = InvokeWriteWithDelayAsync(5, 1);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -292,7 +279,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await InvokeParallelWriteWithDelayAsync(entry, 0);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -304,7 +291,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await InvokeParallelWriteWithDelayAsync(entry, 1);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Tasks/TaskExceptionTests.cs

@@ -40,7 +40,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -56,7 +56,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -76,7 +76,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -96,7 +96,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -118,7 +118,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -159,7 +159,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -186,7 +186,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -217,7 +217,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -249,7 +249,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -283,7 +283,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }

Tests/Tests.SystematicTesting/Tasks/TaskFactoryTests.cs

@@ -29,7 +29,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
                 Specification.Assert(false, "Reached test assertion.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -49,7 +49,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).Unwrap();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
                 Specification.Assert(false, "Reached test assertion.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -69,7 +69,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).Unwrap();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
                 Specification.Assert(false, "Reached test assertion.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -94,7 +94,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).Unwrap();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
                 Specification.Assert(false, "Reached test assertion.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -119,7 +119,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 }).Unwrap();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
                 Specification.Assert(false, "Reached test assertion.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),

Tests/Tests.SystematicTesting/Tasks/TaskInterleavingsTests.cs

@@ -30,19 +30,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             entry.Value = value;
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestInterleavingsWithOneSynchronousTask()
         {
@@ -52,7 +39,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task = WriteAsync(entry, 3);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of {1}.", entry.Value, 5);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -68,7 +55,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 entry.Value = 5;
                 await task;
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of {1}.", entry.Value, 5);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -89,7 +76,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 await WriteAsync(entry, 5);
                 await task;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -108,7 +95,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 await task1;
                 await task2;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -125,7 +112,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 await task1;
                 await task2;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -151,7 +138,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
 
                 await task1;
                 await task2;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -177,7 +164,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 });
 
                 await task1;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(500),
             expectedError: "Value is 3 instead of 5.",
@@ -187,12 +174,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
         [Fact(Timeout = 5000)]
         public void TestExploreAllInterleavings()
         {
-            if (!this.IsSystematicTest)
-            {
-                // production version cannot always find all combinations.
-                return;
-            }
-
             SortedSet<string> results = new SortedSet<string>();
 
             string success = "Explored interleavings.";

Tests/Tests.SystematicTesting/Tasks/TaskRunTests.cs

@@ -26,7 +26,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -42,7 +42,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -61,7 +61,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -78,7 +78,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -93,11 +93,11 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 SharedEntry entry = new SharedEntry();
                 await Task.Run(async () =>
                 {
-                    await Task.Delay(1);
+                    await Task.Delay(100);
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -110,11 +110,11 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 SharedEntry entry = new SharedEntry();
                 await Task.Run(async () =>
                 {
-                    await Task.Delay(1);
+                    await Task.Delay(100);
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -138,7 +138,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -160,7 +160,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -177,14 +177,14 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 {
                     await Task.Run(async () =>
                     {
-                        await Task.Delay(1);
+                        await Task.Delay(100);
                         entry.Value = 3;
                     });
 
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -199,14 +199,14 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 {
                     await Task.Run(async () =>
                     {
-                        await Task.Delay(1);
+                        await Task.Delay(100);
                         entry.Value = 5;
                     });
 
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -295,7 +295,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 SharedEntry entry = new SharedEntry();
                 int value = await Task.Run(async () =>
                 {
-                    await Task.Delay(1);
+                    await Task.Delay(100);
                     entry.Value = 5;
                     return entry.Value;
                 });
@@ -313,7 +313,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 SharedEntry entry = new SharedEntry();
                 int value = await Task.Run(async () =>
                 {
-                    await Task.Delay(1);
+                    await Task.Delay(100);
                     entry.Value = 3;
                     return entry.Value;
                 });
@@ -379,7 +379,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 {
                     return await Task.Run(async () =>
                     {
-                        await Task.Delay(1);
+                        await Task.Delay(100);
                         entry.Value = 5;
                         return entry.Value;
                     });
@@ -400,7 +400,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 {
                     return await Task.Run(async () =>
                     {
-                        await Task.Delay(1);
+                        await Task.Delay(100);
                         entry.Value = 3;
                         return entry.Value;
                     });

Tests/Tests.SystematicTesting/Tasks/TaskYieldTests.cs

@@ -89,10 +89,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 {
                     await Task.Yield();
                     entry = value;
-                    if (this.IsSystematicTest)
-                    {
-                        Specification.Assert(entry == value, "Value is {0} instead of '{1}'.", entry, value);
-                    }
+                    Specification.Assert(entry == value, "Value is {0} instead of '{1}'.", entry, value);
                 }
 
                 Task task1 = Task.Run(async () =>
@@ -150,7 +147,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = WriteAsync(3);
                 Task task2 = WriteAsync(5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -177,7 +174,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task = InvokeWriteWithYieldAsync(entry, 3);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -193,7 +190,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithYieldAsync(entry, 3);
                 Task task2 = InvokeWriteWithYieldAsync(entry, 5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -216,26 +213,13 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = invokeWriteWithYieldAsync(3);
                 Task task2 = invokeWriteWithYieldAsync(5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
             replay: true);
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestInterleavingsInLocalFunctionYields()
         {
@@ -250,7 +234,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
                 Task task1 = InvokeWriteWithYieldAsync(3);
                 Task task2 = InvokeWriteWithYieldAsync(5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(300),
             expectedError: "Value is 3 instead of 5.",
@@ -274,7 +258,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
             {
                 SharedEntry entry = new SharedEntry();
                 await InvokeParallelWriteWithYieldAsync(entry);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.SystematicTesting/Threading/ThreadPoolTests.cs

@@ -68,14 +68,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Threading
         [Fact(Timeout = 5000)]
         public void TestQueueUserWorkItemWithException()
         {
-            if (!this.IsSystematicTest)
-            {
-                // production version of this test results in an unhandled exception.
-                // bugbug: can we rewrite this test so it works both in production and systematic testing modes?
-                // TestQueueUserWorkItemWithAsyncException makes a lot more sense to me.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 ThreadPool.QueueUserWorkItem(_ =>
@@ -88,8 +80,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Threading
             configuration: GetConfiguration().WithTestingIterations(10),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Unhandled exception. System.InvalidOperationException"),
-                    "Expected 'InvalidOperationException', but found error: " + e);
+                Assert.StartsWith("Unhandled exception. System.InvalidOperationException", e);
             },
             replay: true);
         }
@@ -153,14 +144,6 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Threading
         [Fact(Timeout = 5000)]
         public void TestUnsafeQueueUserWorkItemWithException()
         {
-            if (!this.IsSystematicTest)
-            {
-                // production version of this test results in an unhandled exception.
-                // bugbug: can we rewrite this test so it works both in production and systematic testing modes?
-                // TestUnsafeQueueUserWorkItemWithAsyncException makes a lot more sense to me.
-                return;
-            }
-
             this.TestWithError(() =>
             {
                 ThreadPool.UnsafeQueueUserWorkItem(_ =>
@@ -171,8 +154,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Threading
             configuration: GetConfiguration().WithTestingIterations(10),
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Unhandled exception. System.InvalidOperationException"),
-                    "Expected 'InvalidOperationException', but found error: " + e);
+                Assert.StartsWith("Unhandled exception. System.InvalidOperationException", e);
             },
             replay: true);
         }

Tests/Tests.SystematicTesting/rewrite.coyote.json

@@ -2,7 +2,8 @@
   "AssembliesPath": "../../bin/$(Platform)",
   "OutputPath": "../../bin/$(Platform)",
   "Assemblies": [
-    "Microsoft.Coyote.Tests.SystematicTesting.dll"
+    "Microsoft.Coyote.Tests.SystematicTesting.dll",
+    "Microsoft.Coyote.Tests.Actors.SystematicTesting.dll"
   ],
   "IsRewritingThreads": true
 }

Tests/Tests.Tasks/BaseTaskTest.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using Microsoft.Coyote.Specifications;
 using Microsoft.Coyote.Tests.Common;
 using Xunit.Abstractions;
 
@@ -15,6 +16,9 @@ namespace Microsoft.Coyote.Tasks.Tests
 
         protected override bool IsSystematicTest => true;
 
+        protected static void AssertSharedEntryValue(SharedEntry entry, int expected) =>
+            Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
+
         protected class SharedEntry
         {
             public volatile int Value = 0;

Tests/Tests.Tasks/ConfigureAwait/TaskConfigureAwaitFalseTests.cs

@@ -33,7 +33,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -45,7 +45,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -59,7 +59,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -71,7 +71,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -97,7 +97,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -109,7 +109,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -123,7 +123,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 5).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -135,7 +135,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 3).ConfigureAwait(false);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/ConfigureAwait/TaskConfigureAwaitTrueTests.cs

@@ -33,7 +33,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -45,7 +45,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -59,7 +59,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -71,7 +71,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await WriteWithDelayAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -97,7 +97,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -109,7 +109,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -123,7 +123,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 5).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -135,7 +135,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await NestedWriteWithDelayAsync(entry, 3).ConfigureAwait(true);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/ConfigureAwait/TaskRunConfigureAwaitFalseTests.cs

@@ -25,7 +25,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -41,7 +41,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -60,7 +60,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -77,7 +77,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -96,7 +96,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -113,7 +113,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -137,7 +137,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -159,7 +159,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -183,7 +183,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -205,7 +205,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(false);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/ConfigureAwait/TaskRunConfigureAwaitTrueTests.cs

@@ -25,7 +25,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -41,7 +41,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -60,7 +60,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -77,7 +77,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -96,7 +96,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -113,7 +113,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -137,7 +137,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -159,7 +159,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -183,7 +183,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -205,7 +205,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 }).ConfigureAwait(true);
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/Join/TaskResultTests.cs

@@ -33,7 +33,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 entry.Value = 5;
 
                 Specification.Assert(result is 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value is 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -55,7 +55,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 int result = task.Result;
 
                 Specification.Assert(result is 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value is 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -85,7 +85,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 int result = task.Result;
 
                 Specification.Assert(result is 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value is 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -115,7 +115,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 int result = task.Result;
 
                 Specification.Assert(result is 7, "Result is {0} instead of 7.", result);
-                Specification.Assert(entry.Value is 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/Join/TaskWaitAllTests.cs

@@ -35,7 +35,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = WriteAsync(entry, 5);
                 Task task2 = WriteAsync(entry, 3);
                 Task.WaitAll(task1, task2);
-                Specification.Assert(entry.Value is 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -51,26 +51,13 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = WriteWithDelayAsync(entry, 3);
                 Task task2 = WriteWithDelayAsync(entry, 5);
                 Task.WaitAll(task1, task2);
-                Specification.Assert(entry.Value is 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
             replay: true);
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestWaitAllWithTwoParallelTasks()
         {
@@ -89,8 +76,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 });
 
                 Task.WaitAll(task1, task2);
-
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -149,18 +135,9 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 Task.WaitAll(task1, task2);
 
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(task1.Result is 5, $"The first task result is {task1.Result} instead of 5.");
-                    Specification.Assert(task2.Result is 3, $"The second task result is {task2.Result} instead of 3.");
-                    Specification.Assert(task1.Result == task2.Result, "Results are not equal.");
-                }
-                else
-                {
-                    // production version of this test we don't know which order the tasks execute and
-                    // with statement level interleaving we can even end up with duplicate values.
-                    Specification.Assert(false, "Results are not equal.");
-                }
+                Specification.Assert(task1.Result is 5, $"The first task result is {task1.Result} instead of 5.");
+                Specification.Assert(task2.Result is 3, $"The second task result is {task2.Result} instead of 3.");
+                Specification.Assert(task1.Result == task2.Result, "Results are not equal.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Results are not equal.",
@@ -196,12 +173,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestWaitAllDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WaitAll` deadlocks because one of the tasks cannot complete until later.
@@ -212,7 +183,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }
@@ -220,12 +191,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestWaitAllWithResultsAndDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WaitAll` deadlocks because one of the tasks cannot complete until later.
@@ -236,7 +201,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }

Tests/Tests.Tasks/Join/TaskWaitAnyTests.cs

@@ -217,17 +217,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             configuration: GetConfiguration().WithTestingIterations(200));
         }
 
-        private void AssertCompleted(Task task1, Task task2)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(task1.IsCompleted && task2.IsCompleted, "One task has not completed.");
-            }
-            else
-            {
-                // production cannot guarantee this.
-                Specification.Assert(false, "One task has not completed.");
-            }
-        }
+        private void AssertCompleted(Task task1, Task task2) =>
+            Specification.Assert(task1.IsCompleted && task2.IsCompleted, "One task has not completed.");
     }
 }

Tests/Tests.Tasks/Join/TaskWaitTests.cs

@@ -32,7 +32,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 task.Wait();
                 entry.Value = 5;
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -52,7 +52,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 entry.Value = 5;
                 task.Wait();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -80,7 +80,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 entry.Value = 5;
                 task.Wait();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -108,7 +108,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 entry.Value = 5;
                 task.Wait();
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -135,7 +135,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 task.Wait(10);
                 await task;
 
-                Specification.Assert(entry.Value == 3, "Value is {0} instead of 3.", entry.Value);
+                AssertSharedEntryValue(entry, 3);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -161,7 +161,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 task.Wait(tokenSource.Token);
                 await task;
 
-                Specification.Assert(entry.Value == 3, "Value is {0} instead of 3.", entry.Value);
+                AssertSharedEntryValue(entry, 3);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -187,7 +187,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 task.Wait(10, tokenSource.Token);
                 await task;
 
-                Specification.Assert(entry.Value == 3, "Value is {0} instead of 3.", entry.Value);
+                AssertSharedEntryValue(entry, 3);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }

Tests/Tests.Tasks/Join/TaskWhenAllTests.cs

@@ -29,19 +29,6 @@ namespace Microsoft.Coyote.Tasks.Tests
             entry.Value = value;
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestWhenAllWithTwoSynchronousTasks()
         {
@@ -51,7 +38,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = WriteAsync(entry, 5);
                 Task task2 = WriteAsync(entry, 3);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -67,7 +54,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = WriteWithDelayAsync(entry, 3);
                 Task task2 = WriteWithDelayAsync(entry, 5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -93,7 +80,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 await Task.WhenAll(task1, task2);
 
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -211,7 +198,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 };
 
                 var task = whenAll();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -239,7 +226,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 };
 
                 var task = whenAll();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -360,12 +347,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestWhenAllDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WhenAll` deadlocks because one of the tasks cannot complete until later.
@@ -376,7 +357,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }
@@ -384,12 +365,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestWhenAllWithResultsAndDeadlock()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 // Test that `WhenAll` deadlocks because one of the tasks cannot complete until later.
@@ -400,7 +375,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             },
             errorChecker: (e) =>
             {
-                Assert.True(e.StartsWith("Deadlock detected."), "Expected 'Deadlock detected', but found error: " + e);
+                Assert.StartsWith("Deadlock detected.", e);
             },
             replay: true);
         }

Tests/Tests.Tasks/Join/TaskWhenAnyTests.cs

@@ -28,19 +28,6 @@ namespace Microsoft.Coyote.Tasks.Tests
             entry.Value = value;
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestWhenAnyWithTwoSynchronousTasks()
         {
@@ -51,7 +38,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task2 = WriteAsync(entry, 3);
                 Task result = await Task.WhenAny(task1, task2);
                 Specification.Assert(result.IsCompleted, "No task has completed.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -68,7 +55,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task2 = WriteWithDelayAsync(entry, 5);
                 Task result = await Task.WhenAny(task1, task2);
                 Specification.Assert(result.IsCompleted, "No task has completed.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -95,7 +82,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task result = await Task.WhenAny(task1, task2);
 
                 Specification.Assert(result.IsCompleted, "No task has completed.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -116,7 +103,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     (result.Id == task1.Id && result.Result == 5) ||
                     (result.Id == task2.Id && result.Result == 3),
                     "Found unexpected value.");
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -133,19 +120,8 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task<int> task2 = entry.GetWriteResultWithDelayAsync(3);
                 Task<int> result = await Task.WhenAny(task1, task2);
                 Specification.Assert(result.IsCompleted, "One task has not completed.");
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(
-                        (result.Id == task1.Id && result.Result == 5) ||
-                        (result.Id == task2.Id && result.Result == 3),
-                        "Found unexpected value.");
-                }
-                else
-                {
-                    // production cannot guarantee to hit this case even with 200 iterations
-                    Specification.Assert(result.Result == 5 || result.Result == 3, "Found invalid value.");
-                    Specification.Assert(false, "Found unexpected value.");
-                }
+                Specification.Assert((result.Id == task1.Id && result.Result == 5) ||
+                    (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Found unexpected value.",
@@ -172,18 +148,9 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task<int> result = await Task.WhenAny(task1, task2);
 
                 Specification.Assert(result.IsCompleted, "One task has not completed.");
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(
-                        (result.Id == task1.Id && result.Result == 5) ||
-                        (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
-                    Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
-                }
-                else
-                {
-                    // production version cannot guarantee tasks will run in any particular order.
-                    Specification.Assert(false, "Value is 3 instead of 5.");
-                }
+                Specification.Assert((result.Id == task1.Id && result.Result == 5) ||
+                    (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -210,19 +177,8 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task<int> result = await Task.WhenAny(task1, task2);
 
                 Specification.Assert(result.IsCompleted, "One task has not completed.");
-                if (this.IsSystematicTest)
-                {
-                    Specification.Assert(
-                        (result.Id == task1.Id && result.Result == 5) ||
-                        (result.Id == task2.Id && result.Result == 3),
-                        "Found unexpected value.");
-                }
-                else
-                {
-                    // production version cannot guarantee tasks will run in any particular order.
-                    Specification.Assert(result.Result == 5 || result.Result == 3, "Unexpected value");
-                    Specification.Assert(false, "Found unexpected value.");
-                }
+                Specification.Assert((result.Id == task1.Id && result.Result == 5) ||
+                    (result.Id == task2.Id && result.Result == 3), "Found unexpected value.");
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Found unexpected value.",
@@ -249,7 +205,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 };
 
                 var task = whenAny();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),
@@ -277,7 +233,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 };
 
                 var task = whenAll();
-                this.AssertSharedEntryValue(entry, 1, 3);
+                AssertSharedEntryValue(entry, 1);
                 await task;
             },
             configuration: GetConfiguration().WithTestingIterations(200),

Tests/Tests.Tasks/Locks/AsyncLockTests.cs

@@ -31,12 +31,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestAcquireTwice()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot detect these deadlocks.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 AsyncLock mutex = AsyncLock.Create();
@@ -71,7 +65,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = WriteAsync(3);
                 Task task2 = WriteAsync(5);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is '{0}' instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -79,12 +73,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestSynchronizeTwoParallelTasks()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET cannot guarantee it will find this condition even with 200 iterations.
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 SharedEntry entry = new SharedEntry();
@@ -109,7 +97,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 });
 
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/Locks/SemaphoreTests.cs

@@ -139,12 +139,6 @@ Actual value was 2."
         [Fact(Timeout = 5000)]
         public void TestWaitTwiceWithOneMaxRequest()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET semaphores cannot detect deadlocks, that's why you need Coyote test :-)
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 Semaphore semaphore = Semaphore.Create(1, 1);
@@ -192,7 +186,7 @@ Actual value was 2."
                 Task task1 = WriteAsync(3);
                 Task task2 = WriteAsync(5);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value is 5, "Value is '{0}' instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -200,12 +194,6 @@ Actual value was 2."
         [Fact(Timeout = 5000)]
         public void TestSynchronizeTwoParallelTasksAndOneMaxRequest()
         {
-            if (!this.IsSystematicTest)
-            {
-                // .NET semaphores cannot detect deadlocks, that's why you need Coyote test :-)
-                return;
-            }
-
             this.TestWithError(async () =>
             {
                 SharedEntry entry = new SharedEntry();

Tests/Tests.Tasks/Logging/CustomTaskLogTests.cs

@@ -73,12 +73,6 @@ Hi mom!
         [Fact(Timeout = 5000)]
         public void TestCustomTaskRuntimeLog()
         {
-            if (!this.IsSystematicTest)
-            {
-                // assembly has not been rewritten, so skip this test.
-                return;
-            }
-
             var config = GetConfiguration().WithRandomGeneratorSeed(0);
             TestingEngine engine = TestingEngine.Create(config, this.RunAsync);
 

Tests/Tests.Tasks/RandomValues/TaskRandomBooleanTests.cs

@@ -37,7 +37,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 }
 
                 await WriteAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -66,7 +66,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 }
 
                 await WriteWithDelayAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -93,7 +93,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -121,7 +121,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -149,7 +149,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -180,7 +180,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     });
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/RandomValues/TaskRandomIntegerTests.cs

@@ -37,7 +37,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 }
 
                 await WriteAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -66,7 +66,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 }
 
                 await WriteWithDelayAsync();
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -93,7 +93,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -121,7 +121,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -149,7 +149,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     }
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -180,7 +180,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     });
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/TaskDelayTests.cs

@@ -39,7 +39,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 await Task.WhenAll(tasks);
 
-                Specification.Assert(entry.Value == 2, "Value is '{0}' instead of 2.", entry.Value);
+                AssertSharedEntryValue(entry, 2);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -96,7 +96,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task = InvokeWriteWithDelayAsync(entry, 3, 0);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -110,7 +110,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task = InvokeWriteWithDelayAsync(entry, 3, 1);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -126,7 +126,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithDelayAsync(entry, 3, 0);
                 Task task2 = InvokeWriteWithDelayAsync(entry, 5, 0);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -140,7 +140,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithDelayAsync(entry, 3, 1);
                 Task task2 = InvokeWriteWithDelayAsync(entry, 5, 1);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -161,19 +161,6 @@ namespace Microsoft.Coyote.Tasks.Tests
             configuration: GetConfiguration().WithTestingIterations(200));
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestInterleavingsInRepeatedNestedAsynchronousDelays()
         {
@@ -183,7 +170,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithDelayAsync(entry, 3, 1, true);
                 Task task2 = InvokeWriteWithDelayAsync(entry, 5, 1, true);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -206,7 +193,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = invokeWriteWithDelayAsync(3, 0);
                 Task task2 = invokeWriteWithDelayAsync(5, 0);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -227,7 +214,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = invokeWriteWithDelayAsync(3, 1);
                 Task task2 = invokeWriteWithDelayAsync(5, 1);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -248,7 +235,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithDelayAsync(3, 0);
                 Task task2 = InvokeWriteWithDelayAsync(5, 0);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -267,7 +254,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithDelayAsync(3, 1);
                 Task task2 = InvokeWriteWithDelayAsync(5, 1);
                 await Task.WhenAll(task1, task2);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -291,7 +278,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await InvokeParallelWriteWithDelayAsync(entry, 0);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -303,7 +290,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await InvokeParallelWriteWithDelayAsync(entry, 1);
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/TaskExceptionTests.cs

@@ -39,7 +39,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -55,7 +55,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -75,7 +75,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -95,7 +95,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -117,7 +117,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 Specification.Assert(task.Status == TaskStatus.RanToCompletion,
                     $"Status is '{task.Status}' instead of 'RanToCompletion'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -158,7 +158,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -185,7 +185,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -216,7 +216,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -248,7 +248,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -282,7 +282,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     $"Exception is not '{typeof(InvalidOperationException)}'.");
                 Specification.Assert(task.Status == TaskStatus.Faulted,
                     $"Status is '{task.Status}' instead of 'Faulted'.");
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }

Tests/Tests.Tasks/TaskInterleavingsTests.cs

@@ -29,19 +29,6 @@ namespace Microsoft.Coyote.Tasks.Tests
             entry.Value = value;
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestInterleavingsWithOneSynchronousTask()
         {
@@ -51,7 +38,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task = WriteAsync(entry, 3);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of {1}.", entry.Value, 5);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -67,7 +54,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 entry.Value = 5;
                 await task;
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of {1}.", entry.Value, 5);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -88,7 +75,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 await WriteAsync(entry, 5);
                 await task;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -107,7 +94,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 await task1;
                 await task2;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -124,7 +111,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 await task1;
                 await task2;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -150,7 +137,7 @@ namespace Microsoft.Coyote.Tasks.Tests
 
                 await task1;
                 await task2;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -176,7 +163,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 });
 
                 await task1;
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(500),
             expectedError: "Value is 3 instead of 5.",
@@ -186,12 +173,6 @@ namespace Microsoft.Coyote.Tasks.Tests
         [Fact(Timeout = 5000)]
         public void TestExploreAllInterleavings()
         {
-            if (!this.IsSystematicTest)
-            {
-                // production version cannot always find all combinations.
-                return;
-            }
-
             SortedSet<string> results = new SortedSet<string>();
 
             string success = "Explored interleavings.";

Tests/Tests.Tasks/TaskRunTests.cs

@@ -25,7 +25,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -41,7 +41,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -60,7 +60,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -77,7 +77,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -96,7 +96,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -113,7 +113,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -137,7 +137,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -159,7 +159,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -183,7 +183,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 5;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200));
         }
@@ -205,7 +205,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                     entry.Value = 3;
                 });
 
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",

Tests/Tests.Tasks/TaskYieldTests.cs

@@ -88,10 +88,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 {
                     await Task.Yield();
                     entry = value;
-                    if (this.IsSystematicTest)
-                    {
-                        Specification.Assert(entry == value, "Value is {0} instead of '{1}'.", entry, value);
-                    }
+                    Specification.Assert(entry == value, "Value is {0} instead of '{1}'.", entry, value);
                 }
 
                 Task task1 = Task.Run(async () =>
@@ -149,7 +146,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = WriteAsync(3);
                 Task task2 = WriteAsync(5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -176,7 +173,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task = InvokeWriteWithYieldAsync(entry, 3);
                 entry.Value = 5;
                 await task;
-                Specification.Assert(entry.Value == 5, "Value is {0} instead of 5.", entry.Value);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -192,7 +189,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithYieldAsync(entry, 3);
                 Task task2 = InvokeWriteWithYieldAsync(entry, 5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
@@ -215,26 +212,13 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = invokeWriteWithYieldAsync(3);
                 Task task2 = invokeWriteWithYieldAsync(5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",
             replay: true);
         }
 
-        private void AssertSharedEntryValue(SharedEntry entry, int expected, int other)
-        {
-            if (this.IsSystematicTest)
-            {
-                Specification.Assert(entry.Value == expected, "Value is {0} instead of {1}.", entry.Value, expected);
-            }
-            else
-            {
-                Specification.Assert(entry.Value == expected || entry.Value == other, "Unexpected value {0} in SharedEntry", entry.Value);
-                Specification.Assert(false, "Value is {0} instead of {1}.", other, expected);
-            }
-        }
-
         [Fact(Timeout = 5000)]
         public void TestInterleavingsInLocalFunctionYields()
         {
@@ -249,7 +233,7 @@ namespace Microsoft.Coyote.Tasks.Tests
                 Task task1 = InvokeWriteWithYieldAsync(3);
                 Task task2 = InvokeWriteWithYieldAsync(5);
                 await Task.WhenAll(task1, task2);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(300),
             expectedError: "Value is 3 instead of 5.",
@@ -273,7 +257,7 @@ namespace Microsoft.Coyote.Tasks.Tests
             {
                 SharedEntry entry = new SharedEntry();
                 await InvokeParallelWriteWithYieldAsync(entry);
-                this.AssertSharedEntryValue(entry, 5, 3);
+                AssertSharedEntryValue(entry, 5);
             },
             configuration: GetConfiguration().WithTestingIterations(200),
             expectedError: "Value is 3 instead of 5.",