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

Merged PR 1198: Implement optional custom Event type for timers 

Implement Dimitre's great idea of having an optional custom Event type for timer elapsed events.
See how this cleans up the [CoffeeMachine sample](https://dev.azure.com/foundry99/Coyote/_git/CoyoteSamples/pullrequest/1200?_a=overview) eliminating a switch statement on timer events.
This commit is contained in:
Chris Lovett 2020-02-08 00:33:20 +00:00 коммит произвёл Pantazis Deligiannis
Родитель ea821f04f3
Коммит bf3fc026de
7 изменённых файлов: 273 добавлений и 42 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

16
Source/Core/Actors/Actor.cs
Просмотреть файл

@ -254,13 +254,13 @@ namespace Microsoft.Coyote.Actors
/// See <see href="/coyote/learn/programming-models/actors/timers">Using timers in actors</see> for more information.
/// </remarks>
/// <param name="startDelay">The amount of time to wait before sending the timeout event.</param>
/// <param name="payload">Optional payload of the timeout event.</param>
/// <param name="customEvent">Optional custom event to raise instead of the default TimerElapsedEvent.</param>
/// <returns>Handle that contains information about the timer.</returns>
protected TimerInfo StartTimer(TimeSpan startDelay, object payload = null)
protected TimerInfo StartTimer(TimeSpan startDelay, TimerElapsedEvent customEvent = null)
{
// The specified due time and period must be valid.
this.Assert(startDelay.TotalMilliseconds >= 0, "{0} registered a timer with a negative due time.", this.Id);
return this.RegisterTimer(startDelay, Timeout.InfiniteTimeSpan, payload);
return this.RegisterTimer(startDelay, Timeout.InfiniteTimeSpan, customEvent);
}
/// <summary>
@ -274,14 +274,14 @@ namespace Microsoft.Coyote.Actors
/// </remarks>
/// <param name="startDelay">The amount of time to wait before sending the first timeout event.</param>
/// <param name="period">The time interval between timeout events.</param>
/// <param name="payload">Optional payload of the timeout event.</param>
/// <param name="customEvent">Optional custom event to raise instead of the default TimerElapsedEvent.</param>
/// <returns>Handle that contains information about the timer.</returns>
protected TimerInfo StartPeriodicTimer(TimeSpan startDelay, TimeSpan period, object payload = null)
protected TimerInfo StartPeriodicTimer(TimeSpan startDelay, TimeSpan period, TimerElapsedEvent customEvent = null)
{
// The specified due time and period must be valid.
this.Assert(startDelay.TotalMilliseconds >= 0, "{0} registered a periodic timer with a negative due time.", this.Id);
this.Assert(period.TotalMilliseconds >= 0, "{0} registered a periodic timer with a negative period.", this.Id);
return this.RegisterTimer(startDelay, period, payload);
return this.RegisterTimer(startDelay, period, customEvent);
}
/// <summary>
@ -722,9 +722,9 @@ namespace Microsoft.Coyote.Actors
/// <summary>
/// Registers a new timer using the specified configuration.
/// </summary>
private protected TimerInfo RegisterTimer(TimeSpan dueTime, TimeSpan period, object payload)
private protected TimerInfo RegisterTimer(TimeSpan dueTime, TimeSpan period, TimerElapsedEvent customEvent)
{
var info = new TimerInfo(this.Id, dueTime, period, payload);
var info = new TimerInfo(this.Id, dueTime, period, customEvent);
var timer = this.Runtime.CreateActorTimer(info, this);
this.Runtime.LogWriter.LogCreateTimer(info);
this.Timers.Add(info, timer);

10
Source/Core/Actors/Timers/ActorTimer.cs
Просмотреть файл

@ -39,7 +39,15 @@ namespace Microsoft.Coyote.Actors.Timers
this.Info = info;
this.Owner = owner;
this.TimeoutEvent = new TimerElapsedEvent(this.Info);
this.TimeoutEvent = this.Info.CustomEvent;
if (this.TimeoutEvent is null)
{
this.TimeoutEvent = new TimerElapsedEvent(this.Info);
}
else
{
this.TimeoutEvent.Info = this.Info;
}
// To avoid a race condition between assigning the field of the timer
// and HandleTimeout accessing the field before the assignment happens,

9
Source/Core/Actors/Timers/TimerElapsedEvent.cs
Просмотреть файл

@ -14,7 +14,14 @@ namespace Microsoft.Coyote.Actors.Timers
/// <summary>
/// Stores information about the timer.
/// </summary>
public readonly TimerInfo Info;
public TimerInfo Info { get; internal set; }
/// <summary>
/// Initializes a new instance of the <see cref="TimerElapsedEvent"/> class.
/// </summary>
public TimerElapsedEvent()
{
}
/// <summary>
/// Initializes a new instance of the <see cref="TimerElapsedEvent"/> class.

10
Source/Core/Actors/Timers/TimerInfo.cs
Просмотреть файл

@ -34,9 +34,9 @@ namespace Microsoft.Coyote.Actors.Timers
public readonly TimeSpan Period;
/// <summary>
/// The optional payload of the timer. This is null if there is no payload.
/// The optional custom event to raise instead of the default TimerElapsedEvent.
/// </summary>
public readonly object Payload;
public readonly TimerElapsedEvent CustomEvent;
/// <summary>
/// Initializes a new instance of the <see cref="TimerInfo"/> class.
@ -44,14 +44,14 @@ namespace Microsoft.Coyote.Actors.Timers
/// <param name="ownerId">The id of the actor that owns this timer.</param>
/// <param name="dueTime">The amount of time to wait before sending the first timeout event.</param>
/// <param name="period">The time interval between timeout events.</param>
/// <param name="payload">Optional payload of the timeout event.</param>
internal TimerInfo(ActorId ownerId, TimeSpan dueTime, TimeSpan period, object payload)
/// <param name="customEvent">Optional custom event to raise instead of a default TimerElapsedEvent.</param>
internal TimerInfo(ActorId ownerId, TimeSpan dueTime, TimeSpan period, TimerElapsedEvent customEvent)
{
this.Id = Guid.NewGuid();
this.OwnerId = ownerId;
this.DueTime = dueTime;
this.Period = period;
this.Payload = payload;
this.CustomEvent = customEvent;
}
/// <summary>

10
Source/TestingServices/Actors/Timers/MockStateMachineTimer.cs
Просмотреть файл

@ -52,7 +52,15 @@ namespace Microsoft.Coyote.TestingServices.Timers
this.TimerInfo = (e as TimerSetupEvent).Info;
this.Owner = (e as TimerSetupEvent).Owner;
this.Delay = (e as TimerSetupEvent).Delay;
this.TimeoutEvent = new TimerElapsedEvent(this.TimerInfo);
this.TimeoutEvent = this.TimerInfo.CustomEvent;
if (this.TimeoutEvent is null)
{
this.TimeoutEvent = new TimerElapsedEvent(this.TimerInfo);
}
else
{
this.TimeoutEvent.Info = this.TimerInfo;
}
}
/// <summary>

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

@ -293,5 +293,104 @@ namespace Microsoft.Coyote.Core.Tests.Actors
Assert.True(result);
});
}
private class T6 : StateMachine
{
private ConfigEvent Config;
internal class MyTimeoutEvent : TimerElapsedEvent
{
}
internal enum TestType
{
CustomTimer,
CustomPeriodicTimer
}
internal class ConfigEvent : Event
{
public TestType Test;
public TaskCompletionSource<bool> Tcs;
}
[Start]
[OnEntry(nameof(Initialize))]
[OnEventDoAction(typeof(MyTimeoutEvent), nameof(OnMyTimeout))]
[OnEventDoAction(typeof(TimerElapsedEvent), nameof(OnMyTimeout))]
private class Init : State
{
}
private Transition Initialize(Event e)
{
var ce = e as ConfigEvent;
this.Config = ce;
bool expectError = false;
try
{
switch (ce.Test)
{
case TestType.CustomTimer:
this.StartTimer(TimeSpan.FromMilliseconds(1), customEvent: new MyTimeoutEvent());
break;
case TestType.CustomPeriodicTimer:
this.StartPeriodicTimer(TimeSpan.FromMilliseconds(1), TimeSpan.FromMilliseconds(1), customEvent: new MyTimeoutEvent());
break;
default:
break;
}
}
catch (AssertionFailureException ex)
{
this.Logger.WriteLine(ex.Message);
ce.Tcs.SetResult(expectError == true);
return this.Halt();
}
return default;
}
private Transition OnMyTimeout(Event e)
{
if (e is MyTimeoutEvent)
{
this.Config.Tcs.SetResult(true);
}
else
{
this.Logger.WriteLine("Unexpected event type {0}", e.GetType().FullName);
this.Config.Tcs.SetResult(false);
}
return this.Halt();
}
}
[Fact(Timeout = 10000)]
public async Task TestCustomTimerEventInStateMachine()
{
await this.RunAsync(async r =>
{
var tcs = new TaskCompletionSource<bool>();
r.CreateActor(typeof(T6), new T6.ConfigEvent { Tcs = tcs, Test = T6.TestType.CustomTimer });
var result = await GetResultAsync(tcs.Task);
Assert.True(result);
});
}
[Fact(Timeout = 10000)]
public async Task TestCustomPeriodicTimerEventInStateMachine()
{
await this.RunAsync(async r =>
{
var tcs = new TaskCompletionSource<bool>();
r.CreateActor(typeof(T6), new T6.ConfigEvent { Tcs = tcs, Test = T6.TestType.CustomPeriodicTimer });
var result = await GetResultAsync(tcs.Task);
Assert.True(result);
});
}
}
}

161
Tests/TestingServices.Tests/Actors/Timers/BasicTimerTests.cs
Просмотреть файл

@ -17,14 +17,20 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
{
}
internal class TimerCountEvent : Event
{
public int Count;
}
[OnEventDoAction(typeof(TimerElapsedEvent), nameof(HandleTimeout))]
private class A1 : Actor
{
private int Count;
private TimerCountEvent Config;
protected override Task OnInitializeAsync(Event initialEvent)
{
this.Count = 0;
this.Config = (TimerCountEvent)initialEvent;
this.Config.Count = 0;
// Start a regular timer.
this.StartTimer(TimeSpan.FromMilliseconds(10));
@ -33,24 +39,26 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
private void HandleTimeout()
{
this.Count++;
this.Assert(this.Count == 1);
this.Config.Count++;
this.Assert(this.Config.Count == 1);
}
}
[Fact(Timeout = 10000)]
public void TestBasicTimerOperationInActor()
{
var config = new TimerCountEvent();
this.Test(r =>
{
r.CreateActor(typeof(A1));
r.CreateActor(typeof(A1), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200).WithMaxSteps(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
private class M1 : StateMachine
{
private int Count;
private TimerCountEvent Config;
[Start]
[OnEntry(nameof(InitOnEntry))]
@ -59,9 +67,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
{
}
private void InitOnEntry()
private void InitOnEntry(Event e)
{
this.Count = 0;
this.Config = (TimerCountEvent)e;
this.Config.Count = 0;
// Start a regular timer.
this.StartTimer(TimeSpan.FromMilliseconds(10));
@ -69,30 +78,33 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
private void HandleTimeout()
{
this.Count++;
this.Assert(this.Count == 1);
this.Config.Count++;
this.Assert(this.Config.Count == 1);
}
}
[Fact(Timeout = 10000)]
public void TestBasicTimerOperationInStateMachine()
{
var config = new TimerCountEvent();
this.Test(r =>
{
r.CreateActor(typeof(M1));
r.CreateActor(typeof(M1), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200).WithMaxSteps(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
[OnEventDoAction(typeof(TimerElapsedEvent), nameof(HandleTimeout))]
private class A2 : Actor
{
private TimerInfo Timer;
private int Count;
private TimerCountEvent Config;
protected override Task OnInitializeAsync(Event initialEvent)
{
this.Count = 0;
this.Config = (TimerCountEvent)initialEvent;
this.Config.Count = 0;
// Start a periodic timer.
this.Timer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(10), TimeSpan.FromMilliseconds(10));
@ -101,10 +113,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
private void HandleTimeout()
{
this.Count++;
this.Assert(this.Count <= 10);
this.Config.Count++;
this.Assert(this.Config.Count <= 10);
if (this.Count == 10)
if (this.Config.Count == 10)
{
this.StopTimer(this.Timer);
}
@ -114,17 +126,19 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
[Fact(Timeout = 10000)]
public void TestBasicPeriodicTimerOperationInActor()
{
var config = new TimerCountEvent();
this.Test(r =>
{
r.CreateActor(typeof(A2));
r.CreateActor(typeof(A2), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
private class M2 : StateMachine
{
private TimerInfo Timer;
private int Count;
private TimerCountEvent Config;
[Start]
[OnEntry(nameof(InitOnEntry))]
@ -133,9 +147,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
{
}
private void InitOnEntry()
private void InitOnEntry(Event e)
{
this.Count = 0;
this.Config = (TimerCountEvent)e;
this.Config.Count = 0;
// Start a periodic timer.
this.Timer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(10), TimeSpan.FromMilliseconds(10));
@ -143,10 +158,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
private void HandleTimeout()
{
this.Count++;
this.Assert(this.Count <= 10);
this.Config.Count++;
this.Assert(this.Config.Count <= 10);
if (this.Count == 10)
if (this.Config.Count == 10)
{
this.StopTimer(this.Timer);
}
@ -156,17 +171,20 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
[Fact(Timeout = 10000)]
public void TestBasicPeriodicTimerOperationInStateMachine()
{
var config = new TimerCountEvent();
this.Test(r =>
{
r.CreateActor(typeof(M2));
r.CreateActor(typeof(M2), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
private class M3 : StateMachine
{
private TimerInfo PingTimer;
private TimerInfo PongTimer;
private TimerCountEvent Config;
/// <summary>
/// Start the PingTimer and start handling the timeout events from it.
@ -189,8 +207,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
{
}
private Transition DoPing()
private Transition DoPing(Event e)
{
this.Config = (TimerCountEvent)e;
this.Config.Count = 0;
this.PingTimer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(5), TimeSpan.FromMilliseconds(5));
this.StopTimer(this.PingTimer);
return this.GotoState<Pong>();
@ -203,6 +223,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
private void HandleTimeout(Event e)
{
this.Config.Count++;
var timeout = e as TimerElapsedEvent;
this.Assert(timeout.Info == this.PongTimer);
}
@ -211,11 +232,13 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
[Fact(Timeout = 10000)]
public void TestDropTimeoutsAfterTimerDisposal()
{
var config = new TimerCountEvent();
this.Test(r =>
{
r.CreateActor(typeof(M3));
r.CreateActor(typeof(M3), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200).WithMaxSteps(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
private class M4 : StateMachine
@ -356,5 +379,91 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
},
configuration: Configuration.Create().WithNumberOfIterations(200).WithMaxSteps(200));
}
private class T6 : StateMachine
{
private ConfigEvent Config;
internal class MyTimeoutEvent : TimerElapsedEvent
{
}
internal enum TestType
{
CustomTimer,
CustomPeriodicTimer
}
internal class ConfigEvent : Event
{
public TestType Test;
public int Count;
}
[Start]
[OnEntry(nameof(Initialize))]
[OnEventDoAction(typeof(MyTimeoutEvent), nameof(OnMyTimeout))]
[OnEventDoAction(typeof(TimerElapsedEvent), nameof(OnMyTimeout))]
private class Init : State
{
}
private Transition Initialize(Event e)
{
var ce = e as ConfigEvent;
this.Config = ce;
this.Config.Count = 0;
switch (ce.Test)
{
case TestType.CustomTimer:
this.StartTimer(TimeSpan.FromMilliseconds(1), customEvent: new MyTimeoutEvent());
break;
case TestType.CustomPeriodicTimer:
this.StartPeriodicTimer(TimeSpan.FromMilliseconds(1), TimeSpan.FromMilliseconds(1), customEvent: new MyTimeoutEvent());
break;
default:
break;
}
return default;
}
private void OnMyTimeout(Event e)
{
if (e is MyTimeoutEvent)
{
this.Config.Count++;
this.Assert(this.Config.Count == 1 || this.Config.Test == TestType.CustomPeriodicTimer);
}
else
{
this.Assert(false, "Unexpected event type {0}", e.GetType().FullName);
}
}
}
[Fact(Timeout = 10000)]
public void TestCustomTimerEvent()
{
var config = new T6.ConfigEvent { Test = T6.TestType.CustomTimer };
this.Test(r =>
{
r.CreateActor(typeof(T6), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200).WithMaxSteps(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
[Fact(Timeout = 10000)]
public void TestCustomPeriodicTimerEvent()
{
var config = new T6.ConfigEvent { Test = T6.TestType.CustomPeriodicTimer };
this.Test(r =>
{
r.CreateActor(typeof(T6), config);
},
configuration: Configuration.Create().WithNumberOfIterations(200).WithMaxSteps(200));
Assert.True(config.Count > 0, "Timer never fired?");
}
}
}