forked from microsoft/coyote
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathFailoverDriver.cs
158 lines (131 loc) · 5.82 KB
/
FailoverDriver.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System;
using System.Collections.Generic;
using System.Linq;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Actors.Timers;
using Microsoft.Coyote.Samples.Common;
namespace Microsoft.Coyote.Samples.DrinksServingRobot
{
internal class FailoverDriver : StateMachine
{
private ActorId StorageId;
private ActorId RobotId;
private ActorId NavigatorId;
private bool RunForever;
private readonly LogWriter Log = LogWriter.Instance;
private TimerInfo HaltTimer;
private int Iterations;
private const int NavigatorTimeToLive = 500; // milliseconds
internal class ConfigEvent : Event
{
public bool RunForever;
public ConfigEvent(bool runForever)
{
this.RunForever = runForever;
}
}
[Start]
[OnEntry(nameof(OnInit))]
[DeferEvents(typeof(TimerElapsedEvent), typeof(Robot.RobotReadyEvent))]
[IgnoreEvents(typeof(Robot.NavigatorResetEvent))]
internal class Init : State { }
internal void OnInit(Event e)
{
if (e is ConfigEvent ce)
{
this.RunForever = ce.RunForever;
}
this.Log.WriteLine("<FailoverDriver> #################################################################");
this.Log.WriteLine("<FailoverDriver> Starting the Robot.");
this.StorageId = this.CreateActor(typeof(MockStorage));
this.NavigatorId = this.CreateNavigator();
// Create the Robot.
this.RobotId = this.CreateActor(typeof(Robot), new Robot.ConfigEvent(this.RunForever, this.Id));
// Wake up the Navigator.
this.SendEvent(this.NavigatorId, new Navigator.WakeUpEvent(this.RobotId));
this.RaiseGotoStateEvent<Active>();
}
[OnEventGotoState(typeof(TimerElapsedEvent), typeof(TerminatingNavigator))]
[OnEventDoAction(typeof(Robot.RobotReadyEvent), nameof(OnRobotReady))]
[IgnoreEvents(typeof(Robot.NavigatorResetEvent))]
internal class Active : State { }
private void OnRobotReady()
{
// We have to wait for the robot to be ready before we test killing the Navigator otherwise
// we end up killing the Navigator before the Robot has anything to do which is a waste of time.
// Setup a timer to randomly kill the Navigator. When the timer fires we will restart the
// Navigator and this is testing that the Navigator and Robot can recover gracefully when that happens.
int duration = this.RandomInteger(NavigatorTimeToLive) + NavigatorTimeToLive;
this.HaltTimer = this.StartTimer(TimeSpan.FromMilliseconds(duration));
}
private void StopTimer()
{
if (this.HaltTimer != null)
{
this.StopTimer(this.HaltTimer);
this.HaltTimer = null;
}
}
private ActorId CreateNavigator()
{
var cognitiveServiceId = this.CreateActor(typeof(MockCognitiveService));
var routePlannerServiceId = this.CreateActor(typeof(MockRoutePlanner));
return this.CreateActor(typeof(Navigator), new Navigator.NavigatorConfigEvent(this.Id, this.StorageId, cognitiveServiceId, routePlannerServiceId));
}
[OnEntry(nameof(OnTerminateNavigator))]
[OnEventDoAction(typeof(Navigator.HaltedEvent), nameof(OnHalted))]
[OnEventDoAction(typeof(Robot.NavigatorResetEvent), nameof(OnNavigatorReset))]
[IgnoreEvents(typeof(TimerElapsedEvent))]
internal class TerminatingNavigator : State { }
private void OnTerminateNavigator()
{
this.StopTimer();
this.Log.WriteLine("<FailoverDriver> #################################################################");
this.Log.WriteLine("<FailoverDriver> # Starting the fail over of the Navigator #");
this.Log.WriteLine("<FailoverDriver> #################################################################");
this.SendEvent(this.NavigatorId, new Navigator.TerminateEvent());
}
private void OnHalted()
{
this.Log.WriteLine("<FailoverDriver> ***** The Navigator confirmed that it has terminated ***** ");
// Create a new Navigator.
this.Log.WriteLine("<FailoverDriver> ***** Created a new Navigator -- paused *****");
this.NavigatorId = this.CreateNavigator();
this.Log.WriteLine("<FailoverDriver> ***** Waking up the new Navigator *****");
this.SendEvent(this.NavigatorId, new Navigator.WakeUpEvent(this.RobotId));
}
private void OnNavigatorReset()
{
this.Log.WriteLine("***** Robot confirmed it reset to the new Navigator *****");
this.Iterations++;
if (this.Iterations == 1 || this.RunForever)
{
// Continue on, we expect the WakeUpEvent to RegisterNavigator on the Robot which
// will cause the Robot to raise another RobotReady event.
}
else
{
this.HaltSystem();
}
this.RaiseGotoStateEvent<Active>();
}
private void HaltSystem()
{
this.KillActors(this.RobotId, this.NavigatorId, this.StorageId);
this.RaiseHaltEvent();
}
private void KillActors(params ActorId[] actors)
{
foreach (var actor in actors.Where(ac => ac != null))
{
this.SendEvent(actor, HaltEvent.Instance);
}
}
private void WriteLine(string s)
{
this.Log.WriteLine(s);
}
}
}