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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
//! Implementation of events used in model checking.
use serde::Serialize;
use crate::logger::LogEntry;
use crate::Message;
use crate::mc::network::DeliveryOptions;
use crate::mc::McTime;
/// Identifier of McEvent.
pub type McEventId = usize;
/// Special events used in model checking instead of standard events.
#[derive(Serialize, Clone, Eq, Hash, PartialEq, Debug)]
pub enum McEvent {
/// The event of receiving a non-local message by a process.
MessageReceived {
/// The message itself.
msg: Message,
/// The name of the process that sent the message.
src: String,
/// The name of the process that received the message.
dst: String,
/// Network delivery options for the message.
options: DeliveryOptions,
},
/// The event of a timer expiration.
TimerFired {
/// The process to which the timer belongs to.
proc: String,
/// The timer name.
timer: String,
/// The timer duration.
timer_delay: McTime,
},
/// The event of cancelling a timer.
TimerCancelled {
/// The process to which the timer belongs to.
proc: String,
/// The timer name.
timer: String,
},
/// The event of dropping a message. Created by the model checking strategy.
MessageDropped {
/// The dropped message itself.
msg: Message,
/// The name of the process that sent the message.
src: String,
/// The name of the process the message was sent to.
dst: String,
/// The id of original MessageReceived event.
///
/// Can be `None` if the message is dropped unconditionally.
receive_event_id: Option<McEventId>,
},
/// The event of duplicating a message. Created by model checking strategy.
MessageDuplicated {
/// The duplicated message itself.
msg: Message,
/// The name of the process that sent the message.
src: String,
/// The name of the process the message was sent to.
dst: String,
/// The id of original MessageReceived event.
receive_event_id: McEventId,
},
/// The event of corrupting a message. Created by model checking strategy.
MessageCorrupted {
/// The original message.
msg: Message,
/// The message after corruption.
corrupted_msg: Message,
/// The name of the process that sent the message.
src: String,
/// The name of the process the message was sent to.
dst: String,
/// The id of original MessageReceived event.
receive_event_id: McEventId,
},
}
impl McEvent {
/// Duplicates the MessageReceived event with decreased max_dupl_count.
pub fn duplicate(&self) -> Option<McEvent> {
match self {
McEvent::MessageReceived {
msg,
src,
dst,
options:
DeliveryOptions::PossibleFailures {
can_be_dropped,
max_dupl_count,
can_be_corrupted,
},
} => Some(McEvent::MessageReceived {
msg: msg.clone(),
src: src.clone(),
dst: dst.clone(),
options: DeliveryOptions::PossibleFailures {
can_be_dropped: *can_be_dropped,
max_dupl_count: max_dupl_count - 1,
can_be_corrupted: *can_be_corrupted,
},
}),
_ => None,
}
}
/// Modifies event so it won't be duplicated in future.
pub fn disable_duplications(&mut self) {
if let McEvent::MessageReceived {
options: DeliveryOptions::PossibleFailures { max_dupl_count, .. },
..
} = self
{
*max_dupl_count = 0;
}
}
/// Converts McEvent to LogEntry.
pub fn to_log_entry(&self) -> LogEntry {
match self {
Self::MessageReceived {
msg,
src,
dst,
options: _,
} => LogEntry::McMessageReceived {
msg: msg.clone(),
src: src.clone(),
dst: dst.clone(),
},
Self::TimerFired {
proc,
timer,
timer_delay: _,
} => LogEntry::McTimerFired {
proc: proc.clone(),
timer: timer.clone(),
},
Self::TimerCancelled { proc, timer } => LogEntry::McTimerCancelled {
proc: proc.clone(),
timer: timer.clone(),
},
Self::MessageDropped { msg, src, dst, .. } => LogEntry::McMessageDropped {
msg: msg.clone(),
src: src.clone(),
dst: dst.clone(),
},
Self::MessageDuplicated { msg, src, dst, .. } => LogEntry::McMessageDuplicated {
msg: msg.clone(),
src: src.clone(),
dst: dst.clone(),
},
Self::MessageCorrupted {
msg,
corrupted_msg,
src,
dst,
..
} => LogEntry::McMessageCorrupted {
msg: msg.clone(),
corrupted_msg: corrupted_msg.clone(),
src: src.clone(),
dst: dst.clone(),
},
}
}
}
/// Defines possible orderings of events in the system.
#[derive(Clone)]
pub enum EventOrderingMode {
/// Events can be arbitrarily reordered (default mode).
Normal,
/// Message receive events always precede the timers (kind of fast network mode).
MessagesFirst,
}