forked from microsoft/coyote
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMockStorage.cs
133 lines (113 loc) · 4.15 KB
/
MockStorage.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
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Collections.Generic;
using Microsoft.Coyote.Actors;
using Microsoft.Coyote.Specifications;
namespace Microsoft.Coyote.Samples.DrinksServingRobot
{
/// <summary>
/// A read operation.
/// </summary>
internal class ReadKeyEvent : Event
{
public readonly ActorId RequestorId;
public readonly string Key;
public ReadKeyEvent(ActorId requestorId, string key)
{
this.RequestorId = requestorId;
this.Key = key;
}
}
/// <summary>
/// A write operation.
/// </summary>
internal class KeyValueEvent : Event
{
public readonly ActorId RequestorId;
public readonly string Key;
public readonly object Value;
public KeyValueEvent(ActorId requestorId, string key, object value)
{
this.RequestorId = requestorId;
this.Key = key;
this.Value = value;
}
}
/// <summary>
/// Write operations are followed by a confirmation.
/// </summary>
internal class ConfirmedEvent : Event
{
public readonly string Key;
public readonly object Value;
public readonly bool Existing;
public ConfirmedEvent(string key, object value, bool result)
{
this.Key = key;
this.Value = value;
this.Existing = result;
}
}
internal class DeleteKeyEvent : Event
{
public readonly ActorId RequestorId;
public readonly string Key;
public DeleteKeyEvent(ActorId requestorId, string key)
{
this.RequestorId = requestorId;
this.Key = key;
}
}
/// <summary>
/// MockStorage is a Coyote Actor that models the asynchronous nature of a typical
/// cloud based storage service. It supports simple read, write, delete operations
/// where write operations are confirmed with a ConfirmedEvent, which is an Actor
/// model of pseudo-transactional storage.
/// </summary>
[OnEventDoAction(typeof(ReadKeyEvent), nameof(ReadKey))]
[OnEventDoAction(typeof(KeyValueEvent), nameof(WriteKey))]
[OnEventDoAction(typeof(DeleteKeyEvent), nameof(DeleteKey))]
internal class MockStorage : Actor
{
private readonly Dictionary<string, object> KeyValueStore = new Dictionary<string, object>();
private void ReadKey(Event e)
{
if (e is ReadKeyEvent rke)
{
var requestorId = rke.RequestorId;
var key = rke.Key;
ValidateArguments(requestorId, key, nameof(ReadKeyEvent));
var keyExists = this.KeyValueStore.TryGetValue(key, out object value);
this.SendEvent(requestorId, new KeyValueEvent(requestorId, key, value));
}
}
private void WriteKey(Event e)
{
if (e is KeyValueEvent kve)
{
var requestorId = kve.RequestorId;
var key = kve.Key;
ValidateArguments(requestorId, key, nameof(KeyValueEvent));
bool existing = this.KeyValueStore.ContainsKey(key);
this.KeyValueStore[key] = kve.Value;
// send back a confirmation, this is like the commit of a transaction in the storage layer.
this.SendEvent(requestorId, new ConfirmedEvent(key, kve.Value, existing));
}
}
private void DeleteKey(Event e)
{
if (e is DeleteKeyEvent dke)
{
var requestorId = dke.RequestorId;
var key = dke.Key;
ValidateArguments(requestorId, key, nameof(DeleteKeyEvent));
this.KeyValueStore.Remove(key);
}
}
private static void ValidateArguments(ActorId requestorId, string key, string eventName)
{
Specification.Assert(requestorId != null, $"Error: The RequestorId in the {eventName} received by MockStorage is null");
Specification.Assert(key != null, $"Error: The Key in the {eventName} received by MockStorage is null");
}
}
}