-
Notifications
You must be signed in to change notification settings - Fork 76
/
SafetyMonitor.cs
45 lines (38 loc) · 1.25 KB
/
SafetyMonitor.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
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Collections.Generic;
using Microsoft.Coyote.Specifications;
namespace Microsoft.Coyote.Samples.CloudMessaging
{
/// <summary>
/// Monitor that checks the safety specification that
/// only one leader can be elected at any given term.
/// </summary>
internal class SafetyMonitor : Monitor
{
internal class NotifyLeaderElected : Event
{
internal int Term;
internal NotifyLeaderElected(int term)
: base()
{
this.Term = term;
}
}
private HashSet<int> TermsWithLeader;
[Start]
[OnEntry(nameof(InitOnEntry))]
[OnEventDoAction(typeof(NotifyLeaderElected), nameof(ProcessLeaderElected))]
private class Monitoring : State { }
private void InitOnEntry()
{
this.TermsWithLeader = new HashSet<int>();
}
private void ProcessLeaderElected(Event e)
{
var term = (e as NotifyLeaderElected).Term;
this.Assert(!this.TermsWithLeader.Contains(term), $"Detected more than one leader in term {term}.");
this.TermsWithLeader.Add(term);
}
}
}