microsoft
/
coyote
зеркало из
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

Merged PR 2356: fix problem with XUnit tests that return Microsoft.Coyote.Tasks.Task 

Turns out XUnit does **not** work properly with Microsoft.Coyote.Tasks.Task.  It hides unhandled exceptions, so a bunch of failing tests were not reporting those failures.
This commit is contained in:
Chris Lovett 2020-06-11 21:52:26 +00:00
Родитель 4b48d78697
Коммит 761f11511c
39 изменённых файлов: 375 добавлений и 301 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

2
Source/Test/Telemetry/CoyoteTelemetryClient.cs
Просмотреть файл

@ -5,10 +5,8 @@ using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.IO;
using System.Reflection;
using System.Threading;
using System.Threading.Tasks;
using Microsoft.Coyote;
using Microsoft.Coyote.SmartSockets;
namespace Microsoft.Coyote.Telemetry

1
Source/Test/Telemetry/CoyoteTelemetryServer.cs
Просмотреть файл

@ -7,7 +7,6 @@ using System.Threading.Tasks;
using Microsoft.ApplicationInsights;
using Microsoft.ApplicationInsights.DataContracts;
using Microsoft.ApplicationInsights.Extensibility;
using Microsoft.ApplicationInsights.Extensibility.Implementation;
using Microsoft.Coyote.SmartSockets;
namespace Microsoft.Coyote.Telemetry

5
Tests/Production.Tests/Actors/ActorAssertionFailureTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using System.Threading.Tasks;
using Microsoft.Coyote.Actors;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests
{
@ -82,7 +83,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestSendNullEventInActor()
public async SystemTasks.Task TestSendNullEventInActor()
{
TaskCompletionSource<bool> completed = new TaskCompletionSource<bool>();
var runtime = RuntimeFactory.Create();
@ -96,7 +97,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestSendNullSendorInActor()
public async SystemTasks.Task TestSendNullSendorInActor()
{
TaskCompletionSource<bool> completed = new TaskCompletionSource<bool>();
var runtime = RuntimeFactory.Create();

11
Tests/Production.Tests/Actors/ActorInheritanceTests.cs
Просмотреть файл

@ -4,8 +4,10 @@
using System.IO;
using System.Threading.Tasks;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tests.Common;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors
{
@ -99,7 +101,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestActorInheritance()
public async SystemTasks.Task TestActorInheritance()
{
var runtime = RuntimeFactory.Create();
var config = new ConfigEvent();
@ -111,12 +113,13 @@ namespace Microsoft.Coyote.Production.Tests.Actors
runtime.SendEvent(actor, new CompletedEvent());
await config.Completed.Task;
var actual = NormalizeNewLines(config.Log.ToString());
var expected = NormalizeNewLines(@"ActorSubclass handling E1
var actual = config.Log.ToString().NormalizeNewLines();
var expected = @"ActorSubclass handling E1
ActorSubclass handling E2
BaseActor handling E3
Inherited handling of E4
");
";
expected = expected.NormalizeNewLines();
Assert.Equal(expected, actual);
}
}

7
Tests/Production.Tests/Actors/EventQueues/EventQueueStressTests.cs
Просмотреть файл

@ -7,6 +7,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tests.Common;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors
{
@ -30,7 +31,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestEnqueueDequeueEvents()
public async SystemTasks.Task TestEnqueueDequeueEvents()
{
var logger = new TestOutputLogger(this.TestOutput, false);
var machineStateManager = new MockActorManager(logger,
@ -65,7 +66,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestEnqueueReceiveEvents()
public async SystemTasks.Task TestEnqueueReceiveEvents()
{
var logger = new TestOutputLogger(this.TestOutput, false);
var machineStateManager = new MockActorManager(logger,
@ -96,7 +97,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestEnqueueReceiveEventsAlternateType()
public async SystemTasks.Task TestEnqueueReceiveEventsAlternateType()
{
var logger = new TestOutputLogger(this.TestOutput, false);
var machineStateManager = new MockActorManager(logger,

15
Tests/Production.Tests/Actors/EventQueues/EventQueueTests.cs
Просмотреть файл

@ -7,6 +7,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tests.Common;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors
{
@ -153,7 +154,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEvent()
public async SystemTasks.Task TestReceiveEvent()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();
@ -191,7 +192,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventWithPredicate()
public async SystemTasks.Task TestReceiveEventWithPredicate()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();
@ -240,7 +241,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventWithoutWaiting()
public async SystemTasks.Task TestReceiveEventWithoutWaiting()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();
@ -287,7 +288,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventWithPredicateWithoutWaiting()
public async SystemTasks.Task TestReceiveEventWithPredicateWithoutWaiting()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();
@ -323,7 +324,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventMultipleTypes()
public async SystemTasks.Task TestReceiveEventMultipleTypes()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();
@ -361,7 +362,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventAfterMultipleEnqueues()
public async SystemTasks.Task TestReceiveEventAfterMultipleEnqueues()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();
@ -413,7 +414,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventWithoutWaitingAndWithMultipleEventsInQueue()
public async SystemTasks.Task TestReceiveEventWithoutWaitingAndWithMultipleEventsInQueue()
{
int notificationCount = 0;
var tcs = new TaskCompletionSource<bool>();

6
Tests/Production.Tests/Actors/HandleEventTests.cs
Просмотреть файл

@ -1,11 +1,11 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Threading.Tasks;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.UnitTesting;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors
{
@ -100,7 +100,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestHandleEventInStateMachine()
public async SystemTasks.Task TestHandleEventInStateMachine()
{
var result = new Result();
@ -116,7 +116,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 5000)]
public async Task TestHandleMultipleEventsInStateMachine()
public async SystemTasks.Task TestHandleMultipleEventsInStateMachine()
{
var result = new Result();

26
Tests/Production.Tests/Actors/Logging/CustomActorRuntimeLogTests.cs
Просмотреть файл

@ -8,7 +8,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Coverage;
using Microsoft.Coyote.Specifications;
using Microsoft.Coyote.Tasks;
using Microsoft.Coyote.Tests.Common.IO;
using Microsoft.Coyote.Tests.Common;
using Microsoft.Coyote.Tests.Common.Runtime;
using Xunit;
using Xunit.Abstractions;
@ -167,10 +167,10 @@ namespace Microsoft.Coyote.Production.Tests.Actors
<MonitorLog> TestMonitor is processing event 'CompletedEvent' in state 'Init'.
<MonitorLog> TestMonitor executed action 'OnCompleted' in state 'Init'.";
string actual = RemoveNonDeterministicValuesFromReport(logger.ToString());
expected = NormalizeNewLines(expected);
actual = SortLines(actual); // threading makes this non-deterministic otherwise.
expected = SortLines(expected);
string actual = logger.ToString().RemoveNonDeterministicValues();
expected = expected.NormalizeNewLines();
actual = actual.SortLines(); // threading makes this non-deterministic otherwise.
expected = expected.SortLines();
Assert.Equal(expected, actual);
}
}), config);
@ -220,8 +220,8 @@ namespace Microsoft.Coyote.Production.Tests.Actors
";
string dgml = graphBuilder.Graph.ToString();
string actual = RemoveNonDeterministicValuesFromReport(dgml);
expected = RemoveNonDeterministicValuesFromReport(expected);
string actual = dgml.RemoveNonDeterministicValues();
expected = expected.RemoveNonDeterministicValues();
Assert.Equal(expected, actual);
}
}), config);
@ -284,8 +284,8 @@ CreateStateMachine
StateTransition
StateTransition
StateTransition";
string actual = RemoveNonDeterministicValuesFromReport(logger.ToString());
expected = NormalizeNewLines(expected);
string actual = logger.ToString().RemoveNonDeterministicValues();
expected = expected.NormalizeNewLines();
Assert.Equal(expected, actual);
}), config);
}
@ -403,7 +403,7 @@ StateTransition";
Assert.True(tcs.Task.IsCompleted, "The task await returned but the task is not completed???");
string actual = graphBuilder.Graph.ToString();
actual = RemoveInstanceIds(actual);
actual = actual.RemoveInstanceIds();
Assert.Contains("<Node Id='Microsoft.Coyote.Production.Tests.Actors.CustomActorRuntimeLogTests+Client().Client()' Label='Client()'/>", actual);
Assert.Contains("<Node Id='Microsoft.Coyote.Production.Tests.Actors.CustomActorRuntimeLogTests+Server().Complete' Label='Complete'/>", actual);
@ -422,8 +422,10 @@ StateTransition";
{
runtime.SetLogger(logger);
var graphBuilder = new ActorRuntimeLogGraphBuilder(false);
graphBuilder.CollapseMachineInstances = true;
var graphBuilder = new ActorRuntimeLogGraphBuilder(false)
{
CollapseMachineInstances = true
};
var tcs = TaskCompletionSource.Create<bool>();
runtime.RegisterMonitor<TestMonitor>();

31
Tests/Production.Tests/Actors/SendAndExecuteTests.cs
Просмотреть файл

@ -80,7 +80,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as Config1).Tcs;
var e1 = new E1();
@ -121,7 +121,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
}
[Fact(Timeout = 5000)]
public async Task TestSyncSendBlocks()
public async SystemTasks.Task TestSyncSendBlocks()
{
await this.RunAsync(async r =>
{
@ -149,7 +149,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as Config1).Tcs;
var m = await this.Runtime.CreateActorAndExecuteAsync(typeof(N2), new E2(this.Id));
@ -168,7 +168,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var creator = (e as E2).Id;
var handled = await this.Id.Runtime.SendEventAndExecuteAsync(creator, new E3());
@ -177,7 +177,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
}
[Fact(Timeout = 5000)]
public async Task TestSendCycleDoesNotDeadlock()
public async SystemTasks.Task TestSendCycleDoesNotDeadlock()
{
await this.RunAsync(async r =>
{
@ -204,7 +204,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as Config1).Tcs;
var m = await this.Runtime.CreateActorAndExecuteAsync(typeof(N3));
@ -265,7 +265,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
}
[Fact(Timeout = 5000)]
public async Task TestMachineHaltsOnSendExec()
public async SystemTasks.Task TestMachineHaltsOnSendExec()
{
var config = GetConfiguration();
config.IsMonitoringEnabledInInProduction = true;
@ -295,7 +295,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as Config2).Tcs;
var m = await this.Runtime.CreateActorAndExecuteAsync(typeof(N4), e);
@ -341,7 +341,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
}
[Fact(Timeout = 5000)]
public async Task TestHandledExceptionOnSendExec()
public async SystemTasks.Task TestHandledExceptionOnSendExec()
{
await this.RunAsync(async r =>
{
@ -361,7 +361,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
}
[Fact(Timeout = 5000)]
public async Task TestUnHandledExceptionOnSendExec()
public async SystemTasks.Task TestUnHandledExceptionOnSendExec()
{
await this.RunAsync(async r =>
{
@ -395,7 +395,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as Config1).Tcs;
var m = await this.Runtime.CreateActorAndExecuteAsync(typeof(N5));
@ -414,7 +414,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
}
[Fact(Timeout = 5000)]
public async Task TestUnhandledEventOnSendExec()
public async SystemTasks.Task TestUnhandledEventOnSendExec()
{
await this.RunAsync(async r =>
{
@ -436,9 +436,10 @@ namespace Microsoft.Coyote.Production.Tests.Actors.Operations
await this.WaitAsync(tcs.Task);
Assert.True(failed);
Assert.Equal(
"Microsoft.Coyote.Production.Tests.Actors.SendAndExecuteTests+N5(1) received event " +
"'Microsoft.Coyote.Production.Tests.Actors.SendAndExecuteTests+E3' that cannot be handled.", message);
var className = this.GetType().FullName;
var expected = string.Format("{0}+N5(1) received event '{0}+E3' that cannot be handled.", className);
Assert.Equal(expected, message);
});
}
}

10
Tests/Production.Tests/Actors/StateMachines/ClassHandlerTests.cs
Просмотреть файл

@ -1,11 +1,11 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Threading.Tasks;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.UnitTesting;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -126,7 +126,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestClassEventHandler()
public async SystemTasks.Task TestClassEventHandler()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M1>(configuration: configuration);
@ -137,7 +137,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestClassEventHandlerOverride()
public async SystemTasks.Task TestClassEventHandlerOverride()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M2>(configuration: configuration);
@ -148,7 +148,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestClassEventHandlerDeferOverride()
public async SystemTasks.Task TestClassEventHandlerDeferOverride()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M3>(configuration: configuration);
@ -159,7 +159,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestClassEventHandlerWildcardOverride()
public async SystemTasks.Task TestClassEventHandlerWildcardOverride()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M3>(configuration: configuration);

11
Tests/Production.Tests/Actors/StateMachines/ExceptionPropagationTests.cs
Просмотреть файл

@ -6,6 +6,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests
{
@ -71,7 +72,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestAssertFailureNoEventHandler()
public async SystemTasks.Task TestAssertFailureNoEventHandler()
{
var runtime = RuntimeFactory.Create();
var tcs = TaskCompletionSource.Create<bool>();
@ -80,7 +81,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestAssertFailureEventHandler()
public async SystemTasks.Task TestAssertFailureEventHandler()
{
await this.RunAsync(async r =>
{
@ -99,15 +100,13 @@ namespace Microsoft.Coyote.Production.Tests
var tcs = TaskCompletionSource.Create<bool>();
r.CreateActor(typeof(M), new SetupEvent(tcs));
await this.WaitAsync(tcs.Task);
AssertionFailureException ex = await Assert.ThrowsAsync<AssertionFailureException>(async () => await tcsFail.Task);
AssertionFailureException ex = await Assert.ThrowsAsync<AssertionFailureException>(async () => await this.WaitAsync(tcsFail.Task));
Assert.Equal(1, count);
});
}
[Fact(Timeout = 5000)]
public async Task TestUnhandledExceptionEventHandler()
public async SystemTasks.Task TestUnhandledExceptionEventHandler()
{
await this.RunAsync(async r =>
{

5
Tests/Production.Tests/Actors/StateMachines/GetOperationGroupIdTests.cs
Просмотреть файл

@ -6,6 +6,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -54,7 +55,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestGetOperationGroupIdNotSet()
public async SystemTasks.Task TestGetOperationGroupIdNotSet()
{
await this.RunAsync(async r =>
{
@ -90,7 +91,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestGetOperationGroupIdSet()
public async SystemTasks.Task TestGetOperationGroupIdSet()
{
await this.RunAsync(async r =>
{

8
Tests/Production.Tests/Actors/StateMachines/GotoStateTransitionTests.cs
Просмотреть файл

@ -1,11 +1,11 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Threading.Tasks;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.UnitTesting;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -65,7 +65,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestGotoStateTransition()
public async SystemTasks.Task TestGotoStateTransition()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M1>(configuration: configuration);
@ -74,7 +74,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestGotoStateTransitionAfterSend()
public async SystemTasks.Task TestGotoStateTransitionAfterSend()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M2>(configuration: configuration);
@ -86,7 +86,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestGotoStateTransitionAfterRaise()
public async SystemTasks.Task TestGotoStateTransitionAfterRaise()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M3>(configuration: configuration);

5
Tests/Production.Tests/Actors/StateMachines/InvokeMethodTests.cs
Просмотреть файл

@ -7,6 +7,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.UnitTesting;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -45,7 +46,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestInvokeInternalAsyncMethod()
public async SystemTasks.Task TestInvokeInternalAsyncMethod()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M2>(configuration: configuration);
@ -89,7 +90,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestInvokePrivateAsyncMethod()
public async SystemTasks.Task TestInvokePrivateAsyncMethod()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M4>(configuration: configuration);

5
Tests/Production.Tests/Actors/StateMachines/MemoryLeak/NoMemoryLeakAfterHaltTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -44,7 +45,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupEvent).Tcs;
@ -94,7 +95,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 15000)]
public async Task TestNoMemoryLeakAfterHalt()
public async SystemTasks.Task TestNoMemoryLeakAfterHalt()
{
await this.RunAsync(async r =>
{

5
Tests/Production.Tests/Actors/StateMachines/MemoryLeak/NoMemoryLeakInEventSendingTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -46,7 +47,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupEvent).Tcs;
@ -88,7 +89,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 22000)]
public async Task TestNoMemoryLeakInEventSending()
public async SystemTasks.Task TestNoMemoryLeakInEventSending()
{
await this.RunAsync(async r =>
{

5
Tests/Production.Tests/Actors/StateMachines/NondeterministicChoiceTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -47,7 +48,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestNondeterministicBooleanChoiceInMachineHandler()
public async SystemTasks.Task TestNondeterministicBooleanChoiceInMachineHandler()
{
await this.RunAsync(async r =>
{
@ -85,7 +86,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestNondeterministicIntegerChoiceInMachineHandler()
public async SystemTasks.Task TestNondeterministicIntegerChoiceInMachineHandler()
{
await this.RunAsync(async r =>
{

8
Tests/Production.Tests/Actors/StateMachines/OnEventDroppedTests.cs
Просмотреть файл

@ -52,7 +52,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestOnDroppedCalled1()
public async SystemTasks.Task TestOnDroppedCalled1()
{
await this.RunAsync(async r =>
{
@ -89,7 +89,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestOnDroppedCalled2()
public async SystemTasks.Task TestOnDroppedCalled2()
{
await this.RunAsync(async r =>
{
@ -110,7 +110,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestOnDroppedParams()
public async SystemTasks.Task TestOnDroppedParams()
{
await this.RunAsync(async r =>
{
@ -218,7 +218,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestProcessedOrDropped()
public async SystemTasks.Task TestProcessedOrDropped()
{
var config = GetConfiguration();
config.IsMonitoringEnabledInInProduction = true;

16
Tests/Production.Tests/Actors/StateMachines/OnExceptionTests.cs
Просмотреть файл

@ -63,7 +63,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestOnExceptionCalledOnce1()
public async SystemTasks.Task TestOnExceptionCalledOnce1()
{
await this.RunAsync(async r =>
{
@ -106,7 +106,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestOnExceptionCalledOnce2()
public async SystemTasks.Task TestOnExceptionCalledOnce2()
{
await this.RunAsync(async r =>
{
@ -138,7 +138,7 @@ namespace Microsoft.Coyote.Production.Tests
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
await Task.CompletedTask;
this.Event = e as E;
@ -158,7 +158,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestOnExceptionCalledOnceAsync1()
public async SystemTasks.Task TestOnExceptionCalledOnceAsync1()
{
await this.RunAsync(async r =>
{
@ -188,7 +188,7 @@ namespace Microsoft.Coyote.Production.Tests
{
}
private async Task InitOnEntry()
private async SystemTasks.Task InitOnEntry()
{
await Task.CompletedTask;
throw new NotImplementedException();
@ -202,7 +202,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestOnExceptionCalledOnceAsync2()
public async SystemTasks.Task TestOnExceptionCalledOnceAsync2()
{
await this.RunAsync(async r =>
{
@ -249,7 +249,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestOnExceptionCanHalt()
public async SystemTasks.Task TestOnExceptionCanHalt()
{
await this.RunAsync(async r =>
{
@ -304,7 +304,7 @@ namespace Microsoft.Coyote.Production.Tests
}
[Fact(Timeout = 5000)]
public async Task TestUnhandledEventCanHalt()
public async SystemTasks.Task TestUnhandledEventCanHalt()
{
await this.RunAsync(async r =>
{

6
Tests/Production.Tests/Actors/StateMachines/OnHaltTests.cs
Просмотреть файл

@ -54,7 +54,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestHaltCalled()
public async SystemTasks.Task TestHaltCalled()
{
await this.RunAsync(async r =>
{
@ -90,7 +90,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveOnHalt()
public async SystemTasks.Task TestReceiveOnHalt()
{
await this.RunAsync(async r =>
{
@ -149,7 +149,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestAPIsOnHalt()
public async SystemTasks.Task TestAPIsOnHalt()
{
await this.RunAsync(async r =>
{

14
Tests/Production.Tests/Actors/StateMachines/PushPopStateTests.cs
Просмотреть файл

@ -3,11 +3,11 @@
using System;
using System.Collections.Generic;
using System.Threading.Tasks;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.UnitTesting;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -50,7 +50,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestPushStateTransition()
public async SystemTasks.Task TestPushStateTransition()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M1>(configuration: configuration);
@ -72,7 +72,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestPushStateTransitionAfterSend()
public async SystemTasks.Task TestPushStateTransitionAfterSend()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M2>(configuration: configuration);
@ -100,7 +100,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestPushStateTransitionAfterRaise()
public async SystemTasks.Task TestPushStateTransitionAfterRaise()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M3>(configuration: configuration);
@ -131,7 +131,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestPushPopTransition()
public async SystemTasks.Task TestPushPopTransition()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M4>(configuration: configuration);
@ -170,7 +170,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestPushStateInheritance()
public async SystemTasks.Task TestPushStateInheritance()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M5>(configuration: configuration);
@ -328,7 +328,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestInheritedDuplicateDeferHandler()
public async SystemTasks.Task TestInheritedDuplicateDeferHandler()
{
// inherited state can re-define a DeferEvent, IgnoreEvent or a Goto if it wants to, this is not an error.
var configuration = GetConfiguration();

21
Tests/Production.Tests/Actors/StateMachines/ReceiveEventIntegrationTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -47,7 +48,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupEvent).Tcs;
this.SendEvent(this.Id, new E1());
@ -64,7 +65,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupEvent).Tcs;
this.SendEvent(this.Id, new E1());
@ -81,7 +82,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupEvent).Tcs;
this.SendEvent(this.Id, new E1());
@ -98,7 +99,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupEvent).Tcs;
var id = this.CreateActor(typeof(M5), new E2(this.Id));
@ -120,14 +121,14 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var id = (e as E2).Id;
var received = (E2)await this.ReceiveEventAsync(typeof(E2));
this.SendEvent(received.Id, new E2(this.Id));
}
private async Task Handle(Event e)
private async SystemTasks.Task Handle(Event e)
{
var id = (e as E2).Id;
var received = (E2)await this.ReceiveEventAsync(typeof(E2));
@ -136,7 +137,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventOneMachine()
public async SystemTasks.Task TestReceiveEventOneMachine()
{
await this.RunAsync(async r =>
{
@ -149,7 +150,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventWithPredicateOneMachine()
public async SystemTasks.Task TestReceiveEventWithPredicateOneMachine()
{
await this.RunAsync(async r =>
{
@ -162,7 +163,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventMultipleTypesOneMachine()
public async SystemTasks.Task TestReceiveEventMultipleTypesOneMachine()
{
await this.RunAsync(async r =>
{
@ -175,7 +176,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventTwoMachines()
public async SystemTasks.Task TestReceiveEventTwoMachines()
{
await this.RunAsync(async r =>
{

15
Tests/Production.Tests/Actors/StateMachines/ReceiveEventStressTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -77,7 +78,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupTcsEvent).Tcs;
var numMessages = (e as SetupTcsEvent).NumMessages;
@ -94,7 +95,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 20000)]
public async Task TestReceiveEvent()
public async SystemTasks.Task TestReceiveEvent()
{
for (int i = 0; i < 100; i++)
{
@ -157,7 +158,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
this.Counter = 0;
}
private async Task HandleMessage()
private async SystemTasks.Task HandleMessage()
{
await this.ReceiveEventAsync(typeof(Message));
this.Counter += 2;
@ -170,7 +171,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 20000)]
public async Task TestReceiveEventAlternate()
public async SystemTasks.Task TestReceiveEventAlternate()
{
for (int i = 0; i < 100; i++)
{
@ -195,7 +196,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var tcs = (e as SetupTcsEvent).Tcs;
var numMessages = (e as SetupTcsEvent).NumMessages;
@ -222,7 +223,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
}
private async Task InitOnEntry(Event e)
private async SystemTasks.Task InitOnEntry(Event e)
{
var id = (e as SetupIdEvent).Id;
var numMessages = (e as SetupIdEvent).NumMessages;
@ -238,7 +239,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 20000)]
public async Task TestReceiveEventExchange()
public async SystemTasks.Task TestReceiveEventExchange()
{
for (int i = 0; i < 100; i++)
{

11
Tests/Production.Tests/Actors/StateMachines/ReceiveEventTests.cs
Просмотреть файл

@ -6,6 +6,7 @@ using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.UnitTesting;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
{
@ -89,7 +90,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventStatement()
public async SystemTasks.Task TestReceiveEventStatement()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M1>(configuration: configuration);
@ -103,7 +104,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestMultipleReceiveEventStatements()
public async SystemTasks.Task TestMultipleReceiveEventStatements()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M2>(configuration: configuration);
@ -123,7 +124,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestMultipleReceiveEventStatementsUnordered()
public async SystemTasks.Task TestMultipleReceiveEventStatementsUnordered()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M2>(configuration: configuration);
@ -145,7 +146,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestReceiveEventStatementWithMultipleTypes()
public async SystemTasks.Task TestReceiveEventStatementWithMultipleTypes()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M3>(configuration: configuration);
@ -159,7 +160,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors.StateMachines
}
[Fact(Timeout = 5000)]
public async Task TestMultipleReceiveEventStatementsWithMultipleTypes()
public async SystemTasks.Task TestMultipleReceiveEventStatementsWithMultipleTypes()
{
var configuration = GetConfiguration();
var test = new ActorTestKit<M4>(configuration: configuration);

5
Tests/Production.Tests/Actors/Timers/TimerStressTests.cs
Просмотреть файл

@ -7,6 +7,7 @@ using Microsoft.Coyote.Actors.Timers;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors
{
@ -54,7 +55,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 6000)]
public async Task TestTimerLifetime()
public async SystemTasks.Task TestTimerLifetime()
{
await this.RunAsync(async r =>
{
@ -105,7 +106,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 6000)]
public async Task TestPeriodicTimerLifetime()
public async SystemTasks.Task TestPeriodicTimerLifetime()
{
await this.RunAsync(async r =>
{

17
Tests/Production.Tests/Actors/Timers/TimerTests.cs
Просмотреть файл

@ -7,6 +7,7 @@ using Microsoft.Coyote.Actors.Timers;
using Microsoft.Coyote.Tasks;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
namespace Microsoft.Coyote.Production.Tests.Actors
{
@ -78,7 +79,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestBasicTimerOperationInStateMachine()
public async SystemTasks.Task TestBasicTimerOperationInStateMachine()
{
await this.RunAsync(async r =>
{
@ -126,7 +127,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestBasicPeriodicTimerOperationInStateMachine()
public async SystemTasks.Task TestBasicPeriodicTimerOperationInStateMachine()
{
await this.RunAsync(async r =>
{
@ -166,7 +167,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
{
}
private async Task DoPing(Event e)
private async SystemTasks.Task DoPing(Event e)
{
this.Tcs = (e as SetupEvent).Tcs;
this.PingTimer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(5), TimeSpan.FromMilliseconds(5));
@ -197,7 +198,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestDropTimeoutsAfterTimerDisposalInStateMachine()
public async SystemTasks.Task TestDropTimeoutsAfterTimerDisposalInStateMachine()
{
await this.RunAsync(async r =>
{
@ -238,7 +239,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestIllegalDueTimeSpecificationInStateMachine()
public async SystemTasks.Task TestIllegalDueTimeSpecificationInStateMachine()
{
await this.RunAsync(async r =>
{
@ -279,7 +280,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestIllegalPeriodSpecificationInStateMachine()
public async SystemTasks.Task TestIllegalPeriodSpecificationInStateMachine()
{
await this.RunAsync(async r =>
{
@ -363,7 +364,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestCustomTimerEventInStateMachine()
public async SystemTasks.Task TestCustomTimerEventInStateMachine()
{
await this.RunAsync(async r =>
{
@ -376,7 +377,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
}
[Fact(Timeout = 10000)]
public async Task TestCustomPeriodicTimerEventInStateMachine()
public async SystemTasks.Task TestCustomPeriodicTimerEventInStateMachine()
{
await this.RunAsync(async r =>
{

6
Tests/Production.Tests/Tasks/Logging/CustomTaskRuntimeLogTests.cs
Просмотреть файл

@ -4,7 +4,7 @@
using Microsoft.Coyote.Random;
using Microsoft.Coyote.Runtime;
using Microsoft.Coyote.Tasks;
using Microsoft.Coyote.Tests.Common.IO;
using Microsoft.Coyote.Tests.Common;
using Xunit;
using Xunit.Abstractions;
using SystemTasks = System.Threading.Tasks;
@ -41,8 +41,8 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
string expected = @"<RandomLog> Task '' nondeterministically chose ''.
Task '' completed with result ''.";
string actual = RemoveNonDeterministicValuesFromReport(logger.ToString());
expected = NormalizeNewLines(expected);
string actual = logger.ToString().RemoveNonDeterministicValues();
expected = expected.NormalizeNewLines();
Assert.Equal(expected, actual);
logger.Dispose();

39
Tests/Production.Tests/Tasks/TestMethodSignatures.cs Normal file
Просмотреть файл

@ -0,0 +1,39 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System;
using System.Linq;
using Microsoft.Coyote.Tests.Common;
using Xunit;
using Xunit.Abstractions;
namespace Microsoft.Coyote.Production.Tests.Tasks
{
public class TestMethodSignatures : BaseTest
{
public TestMethodSignatures(ITestOutputHelper output)
: base(output)
{
}
[Fact(Timeout = 5000)]
public void TestForCoyoteMethodSignatures()
{
foreach (var type in this.GetType().Assembly.GetTypes())
{
foreach (var method in type.GetMethods())
{
if (method.GetCustomAttributes(typeof(FactAttribute), false).Any() ||
method.GetCustomAttributes(typeof(TheoryAttribute), false).Any())
{
Type returnType = method.ReturnType;
if (returnType.FullName.Contains("Coyote"))
{
Assert.False(true, string.Format("XUnit does not support Coyote return types in method: {0}.{1}", type.FullName, method.Name));
}
}
}
}
}
}
}

37
Tests/SystematicTesting.Tests/Coverage/ActivityCoverageTests.cs
Просмотреть файл

@ -4,6 +4,7 @@
using System.Diagnostics;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Specifications;
using Microsoft.Coyote.Tests.Common;
using Microsoft.Coyote.Tests.Common.Events;
using Xunit;
using Xunit.Abstractions;
@ -52,7 +53,7 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Coverage
},
configuration);
string result = RemoveExcessiveEmptySpaceFromReport(report);
string result = report.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 100.0%
============================
@ -64,7 +65,7 @@ Event coverage: 100.0%
State has no expected events, so coverage is 100%
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
@ -95,7 +96,7 @@ Event coverage: 100.0%
},
configuration);
string result = RemoveExcessiveEmptySpaceFromReport(report);
string result = report.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 100.0%
============================
@ -112,7 +113,7 @@ Event coverage: 100.0%
Previous states: Init
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
@ -144,7 +145,7 @@ Event coverage: 100.0%
},
configuration);
string result = RemoveExcessiveEmptySpaceFromReport(report);
string result = report.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 100.0%
============================
StateMachine: M2
@ -162,7 +163,7 @@ Event coverage: 100.0%
Previous states: Init
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
@ -222,7 +223,7 @@ Event coverage: 100.0%
},
configuration);
string result = RemoveExcessiveEmptySpaceFromReport(report);
string result = report.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 100.0%
============================
@ -248,7 +249,7 @@ Event coverage: 100.0%
Events sent: HelloEvent, Events.UnitEvent
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
@ -302,8 +303,8 @@ Event coverage: 100.0%
Events sent: Events.UnitEvent
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
string result = RemoveExcessiveEmptySpaceFromReport(report1);
expected = expected.RemoveExcessiveEmptySpace();
string result = report1.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
// Make sure second run is not confused by the first.
@ -352,7 +353,7 @@ Event coverage: 100.0%
},
configuration);
string result = RemoveExcessiveEmptySpaceFromReport(report);
string result = report.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 50.0%
===========================
StateMachine: M5
@ -378,7 +379,7 @@ Event coverage: 100.0%
Events sent: E1
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
@ -414,7 +415,7 @@ Event coverage: 100.0%
}
[Fact(Timeout = 5000)]
private void TestPushStateActivityCoverage()
public void TestPushStateActivityCoverage()
{
var configuration = Configuration.Create();
configuration.ReportActivityCoverage = true;
@ -427,7 +428,7 @@ Event coverage: 100.0%
},
configuration);
string result = RemoveExcessiveEmptySpaceFromReport(report);
string result = report.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 100.0%
============================
@ -454,7 +455,7 @@ Event coverage: 100.0%
Events sent: E1, E2
";
expected = RemoveExcessiveEmptySpaceFromReport(expected);
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
@ -521,7 +522,7 @@ Event coverage: 100.0%
},
configuration);
result = RemoveExcessiveEmptySpaceFromReport(result);
result = result.RemoveExcessiveEmptySpace();
var expected = @"Total event coverage: 100.0%
============================
@ -562,8 +563,8 @@ Event coverage: 100.0%
Events sent: E1, E2
";
result = RemoveExcessiveEmptySpaceFromReport(result);
expected = RemoveExcessiveEmptySpaceFromReport(expected);
result = result.RemoveExcessiveEmptySpace();
expected = expected.RemoveExcessiveEmptySpace();
Assert.Equal(expected, result);
}
}

7
Tests/SystematicTesting.Tests/Runtime/CustomTaskRuntimeLogTests.cs
Просмотреть файл

@ -5,6 +5,7 @@ using System;
using Microsoft.Coyote.Runtime;
using Microsoft.Coyote.Specifications;
using Microsoft.Coyote.Tasks;
using Microsoft.Coyote.Tests.Common;
using Microsoft.Coyote.Tests.Common.Tasks;
using Xunit;
using Xunit.Abstractions;
@ -72,9 +73,9 @@ Task '' completed.
<StrategyLog> Found 100.00% buggy schedules.";
string actual = engine.ReadableTrace.ToString();
actual = RemoveStackTraceFromReport(actual, "<StrategyLog>");
actual = RemoveNonDeterministicValuesFromReport(actual);
expected = RemoveNonDeterministicValuesFromReport(expected);
actual = actual.RemoveStackTrace("<StrategyLog>");
actual = actual.RemoveNonDeterministicValues();
expected = expected.RemoveNonDeterministicValues();
Assert.Equal(expected, actual);
}
catch (Exception ex)

1
Tests/SystematicTesting.Tests/Tasks/Integration/ExtremeProgrammingChallenge14Tests.cs
Просмотреть файл

@ -2,7 +2,6 @@
// Licensed under the MIT License.
using System.Collections.Generic;
using Microsoft.Coyote.Specifications;
using Microsoft.Coyote.Tasks;
using Microsoft.Coyote.Tests.Common;
using Xunit;

8
Tests/SystematicTesting.Tests/Tasks/Logging/CustomTaskRuntimeLogTests.cs
Просмотреть файл

@ -2,7 +2,6 @@
// Licensed under the MIT License.
using System.IO;
using System.Text.RegularExpressions;
using Microsoft.Coyote.Runtime;
using Microsoft.Coyote.Tests.Common;
using Xunit;
@ -34,8 +33,8 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
engine.Run();
var result = log.ToString();
result = RemoveNonDeterministicValuesFromReport(result);
var expected = RemoveNonDeterministicValuesFromReport(@"... Task 0 is using 'random' strategy (seed:4005173804).
result = result.RemoveNonDeterministicValues();
var expected = @"... Task 0 is using 'random' strategy (seed:4005173804).
..... Iteration #1
<TestLog> Running test.
Hi mom!
@ -45,7 +44,8 @@ Hi mom!
..... Iteration #3
<TestLog> Running test.
Hi mom!
");
";
expected = expected.RemoveNonDeterministicValues();
Assert.Equal(expected, result);
}

17
Tests/SystematicTesting.Tests/Tasks/TestMethodSignatures.cs Normal file
Просмотреть файл

@ -0,0 +1,17 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using Xunit.Abstractions;
namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
{
public class TestMethodSignatures : Microsoft.Coyote.Production.Tests.Tasks.TestMethodSignatures
{
public TestMethodSignatures(ITestOutputHelper output)
: base(output)
{
}
public override bool SystematicTest => true;
}
}

172
Tests/Tests.Common/BaseTest.cs
Просмотреть файл

@ -2,13 +2,11 @@
// Licensed under the MIT License.
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.IO;
using System.Linq;
using System.Runtime.CompilerServices;
using System.Text;
using System.Text.RegularExpressions;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Coverage;
using Microsoft.Coyote.SystematicTesting;
@ -24,7 +22,6 @@ namespace Microsoft.Coyote.Tests.Common
public abstract class BaseTest
{
protected readonly ITestOutputHelper TestOutput;
private Exception Failure;
public BaseTest(ITestOutputHelper output)
{
@ -36,116 +33,6 @@ namespace Microsoft.Coyote.Tests.Common
/// </summary>
public virtual bool SystematicTest => false;
protected static Configuration GetConfiguration()
{
return Configuration.Create().WithTelemetryEnabled(false);
}
protected static string RemoveNonDeterministicValuesFromReport(string report)
{
// Match a GUID or other ids (since they can be nondeterministic).
report = Regex.Replace(report, @"\'[0-9|a-z|A-Z|-]{36}\'|\'[0-9]+\'|\'<unknown>\'", "''");
report = RemoveInstanceIds(report);
report = NormalizeNewLines(report);
// Match a namespace.
return RemoveNamespaceReferencesFromReport(report).Trim();
}
protected static string RemoveInstanceIds(string actual)
{
actual = Regex.Replace(actual, @"\([^)]*\)", "()");
return actual;
}
protected static string NormalizeNewLines(string text)
{
return Regex.Replace(text, "[\r\n]+", "\n");
}
protected static string SortLines(string text)
{
var list = new List<string>(text.Split('\n'));
list.Sort(StringComparer.Ordinal);
return string.Join("\n", list);
}
protected static string RemoveNamespaceReferencesFromReport(string report)
{
report = Regex.Replace(report, @"Microsoft.Coyote.Tests.Common\.", string.Empty);
return Regex.Replace(report, @"Microsoft\.[^+]*\+", string.Empty);
}
protected static string RemoveExcessiveEmptySpaceFromReport(string report)
{
return Regex.Replace(report, @"\s+", " ");
}
protected static string RemoveStackTraceFromReport(string report,
string removeUntilContainsText = "Microsoft.Coyote.SystematicTesting.Tests")
{
StringBuilder result = new StringBuilder();
bool strip = false;
foreach (var line in report.Split('\n'))
{
string trimmed = line.Trim('\r');
string nows = trimmed.Trim();
if (nows.StartsWith("<StackTrace>"))
{
result.AppendLine("<StackTrace> ");
strip = true;
}
else if (strip && string.IsNullOrEmpty(nows))
{
strip = false;
continue;
}
if (!strip)
{
result.AppendLine(trimmed);
}
else if (strip && trimmed.Contains(removeUntilContainsText))
{
result.AppendLine(trimmed);
}
}
return result.ToString();
}
protected static string RemoveStackTraceFromXmlReport(string report)
{
StringBuilder result = new StringBuilder();
bool strip = false;
foreach (var line in report.Split('\n'))
{
string trimmed = line.Trim('\r');
string nows = trimmed.Trim();
if (nows.StartsWith("<AssertionFailure>&lt;StackTrace&gt;"))
{
result.AppendLine(" <AssertionFailure>StackTrace:");
strip = true;
}
else if (strip && nows.StartsWith("</AssertionFailure>"))
{
result.AppendLine(" </AssertionFailure>");
strip = false;
continue;
}
if (!strip)
{
result.AppendLine(trimmed);
}
else if (strip && trimmed.Contains("Microsoft.Coyote.SystematicTesting.Tests"))
{
result.AppendLine(trimmed);
}
}
return result.ToString();
}
protected void Test(Action test, Configuration configuration = null)
{
if (this.SystematicTest)
@ -201,7 +88,7 @@ namespace Microsoft.Coyote.Tests.Common
{
var activityCoverageReporter = new ActivityCoverageReporter(engine.TestReport.CoverageInfo);
activityCoverageReporter.WriteCoverageText(writer);
string result = RemoveNamespaceReferencesFromReport(writer.ToString());
string result = writer.ToString().RemoveNamespaceReferences();
return result;
}
}
@ -567,7 +454,6 @@ namespace Microsoft.Coyote.Tests.Common
{
configuration.IsMonitoringEnabledInInProduction = true;
var runtime = RuntimeFactory.Create(configuration);
runtime.OnFailure += this.OnFailure;
runtime.SetLogger(logger);
await test(runtime);
}
@ -581,12 +467,6 @@ namespace Microsoft.Coyote.Tests.Common
}
}
private void OnFailure(Exception ex)
{
this.Failure = ex;
Assert.False(true, ex.Message + "\n" + ex.StackTrace);
}
private void RunWithErrors(Action<IActorRuntime> test, Configuration configuration, TestErrorChecker errorChecker)
{
configuration = configuration ?? GetConfiguration();
@ -704,6 +584,11 @@ namespace Microsoft.Coyote.Tests.Common
protected async Task WaitAsync(Task task, int millisecondsDelay = 5000)
{
if (Debugger.IsAttached)
{
millisecondsDelay = 500000;
}
if (this.SystematicTest)
{
// WhenAny delay is ignored in test mode...
@ -718,7 +603,12 @@ namespace Microsoft.Coyote.Tests.Common
await Task.WhenAny(task, Task.Delay(millisecondsDelay));
}
this.CheckFailure();
if (task.IsFaulted)
{
// unwrap the AggregateException.
throw task.Exception.InnerException;
}
Assert.True(task.IsCompleted);
}
@ -759,21 +649,13 @@ namespace Microsoft.Coyote.Tests.Common
}
}
private void CheckFailure()
{
// XUnit doesn't report unhandled exceptions from background threads which happens
// with Actors a lot, so this brings that error over to the main thread so the unit
// test fails with the most meaningful error.
var e = this.Failure;
if (e != null)
{
this.Failure = null;
throw e;
}
}
protected async Task<TResult> GetResultAsync<TResult>(TaskCompletionSource<TResult> tcs, int millisecondsDelay = 5000)
{
if (Debugger.IsAttached)
{
millisecondsDelay = 500000;
}
var task = tcs.Task;
if (this.SystematicTest)
{
@ -784,7 +666,12 @@ namespace Microsoft.Coyote.Tests.Common
await Task.WhenAny(task, Task.Delay(millisecondsDelay));
}
this.CheckFailure();
if (task.IsFaulted)
{
// unwrap the AggregateException.
throw task.Exception.InnerException;
}
Assert.True(task.IsCompleted, string.Format("Task timed out after '{0}' milliseconds", millisecondsDelay));
return await task;
}
@ -799,17 +686,17 @@ namespace Microsoft.Coyote.Tests.Common
private static void CheckSingleError(string actual, string expected)
{
var a = RemoveNonDeterministicValuesFromReport(actual);
var b = RemoveNonDeterministicValuesFromReport(expected);
var a = actual.RemoveNonDeterministicValues();
var b = expected.RemoveNonDeterministicValues();
Assert.Equal(b, a);
}
private static void CheckMultipleErrors(string actual, string[] expectedErrors)
{
var stripped = RemoveNonDeterministicValuesFromReport(actual);
var stripped = actual.RemoveNonDeterministicValues();
try
{
Assert.Contains(expectedErrors, (e) => RemoveNonDeterministicValuesFromReport(e) == stripped);
Assert.Contains(expectedErrors, (e) => e.RemoveNonDeterministicValues() == stripped);
}
catch (Exception)
{
@ -834,6 +721,11 @@ namespace Microsoft.Coyote.Tests.Common
engine.TestReport.BugReports.First().Split(new[] { '\r', '\n' }).FirstOrDefault());
}
protected static Configuration GetConfiguration()
{
return Configuration.Create().WithTelemetryEnabled(false);
}
protected static string GetBugReport(TestingEngine engine)
{
string report = string.Empty;

2
Tests/Tests.Common/IO/Logging/CustomLogger.cs → Tests/Tests.Common/Logging/CustomLogger.cs
Просмотреть файл

@ -4,7 +4,7 @@
using System.IO;
using System.Text;
namespace Microsoft.Coyote.Tests.Common.IO
namespace Microsoft.Coyote.Tests.Common
{
public class CustomLogger : TextWriter
{

113
Tests/Tests.Common/Text/StringExtensions.cs Normal file
Просмотреть файл

@ -0,0 +1,113 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System;
using System.Collections.Generic;
using System.Text;
using System.Text.RegularExpressions;
namespace Microsoft.Coyote.Tests.Common
{
/// <summary>
/// Provides methods for cleaning up test strings so they can be compared against expected results
/// after eliminating stuff that is unstable across test runs, test machines or OS platforms.
/// </summary>
public static class StringExtensions
{
public static string SortLines(this string text)
{
var list = new List<string>(text.Split('\n'));
list.Sort(StringComparer.Ordinal);
return string.Join("\n", list);
}
public static string RemoveInstanceIds(this string actual) => Regex.Replace(actual, @"\([^)]*\)", "()");
public static string RemoveExcessiveEmptySpace(this string text) => Regex.Replace(text, @"\s+", " ");
public static string NormalizeNewLines(this string text) => Regex.Replace(text, "[\r\n]+", "\n");
public static string RemoveNonDeterministicValues(this string text)
{
// Match a GUID or other ids (since they can be nondeterministic).
text = Regex.Replace(text, @"\'[0-9|a-z|A-Z|-]{36}\'|\'[0-9]+\'|\'<unknown>\'", "''");
text = RemoveInstanceIds(text);
text = NormalizeNewLines(text);
// Match a namespace.
return RemoveNamespaceReferences(text).Trim();
}
public static string RemoveNamespaceReferences(this string text)
{
text = Regex.Replace(text, @"Microsoft.Coyote.Tests.Common\.", string.Empty);
return Regex.Replace(text, @"Microsoft\.[^+]*\+", string.Empty);
}
public static string RemoveStackTrace(this string text,
string removeUntilContainsText = "Microsoft.Coyote.SystematicTesting.Tests")
{
StringBuilder result = new StringBuilder();
bool strip = false;
foreach (var line in text.Split('\n'))
{
string trimmed = line.Trim('\r');
string nows = trimmed.Trim();
if (nows.StartsWith("<StackTrace>"))
{
result.AppendLine("<StackTrace> ");
strip = true;
}
else if (strip && string.IsNullOrEmpty(nows))
{
strip = false;
continue;
}
if (!strip)
{
result.AppendLine(trimmed);
}
else if (strip && trimmed.Contains(removeUntilContainsText))
{
result.AppendLine(trimmed);
}
}
return result.ToString();
}
public static string RemoveStackTraceFromXml(this string text)
{
StringBuilder result = new StringBuilder();
bool strip = false;
foreach (var line in text.Split('\n'))
{
string trimmed = line.Trim('\r');
string nows = trimmed.Trim();
if (nows.StartsWith("<AssertionFailure>&lt;StackTrace&gt;"))
{
result.AppendLine(" <AssertionFailure>StackTrace:");
strip = true;
}
else if (strip && nows.StartsWith("</AssertionFailure>"))
{
result.AppendLine(" </AssertionFailure>");
strip = false;
continue;
}
if (!strip)
{
result.AppendLine(trimmed);
}
else if (strip && trimmed.Contains("Microsoft.Coyote.SystematicTesting.Tests"))
{
result.AppendLine(trimmed);
}
}
return result.ToString();
}
}
}

1
Tools/Coyote/Instrumentation/CodeCoverageInstrumentation.cs
Просмотреть файл

@ -6,7 +6,6 @@ using System.Collections.Generic;
using System.Configuration;
using System.Diagnostics;
using System.IO;
using System.Linq;
using Microsoft.Coyote.IO;
using Microsoft.Coyote.SystematicTesting.Utilities;

1
Tools/Coyote/Interfaces/TestReportMessage.cs
Просмотреть файл

@ -3,7 +3,6 @@
using System.Runtime.Serialization;
using Microsoft.Coyote.SmartSockets;
using Microsoft.Coyote.SystematicTesting;
namespace Microsoft.Coyote.SystematicTesting.Interfaces
{

1
Tools/Coyote/Utilities/DependencyGraph.cs
Просмотреть файл

@ -1,7 +1,6 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;