1use crate::ast::{Choreography, Protocol, Role};
4use std::collections::{HashMap, HashSet};
5
6#[path = "analysis_graph.rs"]
7mod analysis_graph;
8use analysis_graph::{has_communication, has_cycle};
9
10#[derive(Debug)]
12pub struct AnalysisResult {
13 pub is_deadlock_free: bool,
14 pub has_progress: bool,
15 pub role_participation: HashMap<Role, ParticipationInfo>,
16 pub warnings: Vec<AnalysisWarning>,
17 pub communication_graph: CommunicationGraph,
18}
19
20#[derive(Debug)]
22pub struct ParticipationInfo {
23 pub sends: usize,
24 pub receives: usize,
25 pub choices: usize,
26 pub is_active: bool,
27}
28
29#[derive(Debug, Clone)]
31pub enum AnalysisWarning {
32 UnusedRole(Role),
33 PotentialDeadlock(String),
34 NoProgress(String),
35 AsymmetricChoice(Role),
36 UnreachableCode(String),
37}
38
39#[derive(Debug, Clone)]
41pub struct CommunicationGraph {
42 pub nodes: Vec<Role>,
43 pub edges: Vec<(Role, Role, String)>, }
45
46#[must_use]
48pub fn analyze(choreography: &Choreography) -> AnalysisResult {
49 let mut analyzer = Analyzer::new(choreography);
50 analyzer.analyze()
51}
52
53struct Analyzer<'a> {
54 choreography: &'a Choreography,
55 warnings: Vec<AnalysisWarning>,
56 role_stats: HashMap<Role, RoleStats>,
57 comm_graph: CommunicationGraph,
58}
59
60#[derive(Default)]
61struct RoleStats {
62 sends: usize,
63 receives: usize,
64 choices: usize,
65}
66
67impl<'a> Analyzer<'a> {
68 fn new(choreography: &'a Choreography) -> Self {
69 let mut role_stats = HashMap::new();
70 for role in &choreography.roles {
71 role_stats.insert(role.clone(), RoleStats::default());
72 }
73
74 Analyzer {
75 choreography,
76 warnings: Vec::new(),
77 role_stats,
78 comm_graph: CommunicationGraph {
79 nodes: choreography.roles.clone(),
80 edges: Vec::new(),
81 },
82 }
83 }
84
85 fn analyze(&mut self) -> AnalysisResult {
86 self.analyze_protocol(&self.choreography.protocol);
88
89 let is_deadlock_free = self.check_deadlock_freedom();
91
92 let has_progress = self.check_progress();
94
95 let role_participation = self.compute_participation_info();
97
98 for role in &self.choreography.roles {
100 if let Some(info) = role_participation.get(role) {
101 if !info.is_active {
102 self.warnings
103 .push(AnalysisWarning::UnusedRole(role.clone()));
104 }
105 }
106 }
107
108 AnalysisResult {
109 is_deadlock_free,
110 has_progress,
111 role_participation,
112 warnings: self.warnings.clone(),
113 communication_graph: self.comm_graph.clone(),
114 }
115 }
116
117 fn analyze_protocol(&mut self, protocol: &Protocol) {
118 match protocol {
119 Protocol::Send {
120 from,
121 to,
122 message,
123 continuation,
124 ..
125 } => self.analyze_send(from, to, &message.name.to_string(), continuation),
126
127 Protocol::Broadcast {
128 from,
129 to_all,
130 message,
131 continuation,
132 ..
133 } => self.analyze_broadcast(from, to_all, &message.name.to_string(), continuation),
134
135 Protocol::Choice { role, branches, .. } => self.analyze_choice(role, branches),
136 Protocol::Case { branches, .. } => {
137 for branch in branches {
138 self.analyze_protocol(&branch.protocol);
139 }
140 }
141 Protocol::Timeout {
142 body,
143 on_timeout,
144 on_cancel,
145 ..
146 } => {
147 self.analyze_protocol(body);
148 self.analyze_protocol(on_timeout);
149 if let Some(on_cancel) = on_cancel.as_deref() {
150 self.analyze_protocol(on_cancel);
151 }
152 }
153
154 Protocol::Loop { body, .. } => {
155 self.analyze_protocol(body);
156 }
157
158 Protocol::Parallel { protocols } => {
159 for p in protocols {
160 self.analyze_protocol(p);
161 }
162 }
163
164 Protocol::Rec { body, .. } => {
165 self.analyze_protocol(body);
166 }
167
168 Protocol::Var(_) | Protocol::End => {}
169
170 Protocol::Begin { continuation, .. }
171 | Protocol::Await { continuation, .. }
172 | Protocol::Resolve { continuation, .. }
173 | Protocol::Invalidate { continuation, .. }
174 | Protocol::Extension { continuation, .. }
175 | Protocol::Let { continuation, .. }
176 | Protocol::Publish { continuation, .. }
177 | Protocol::PublishAuthority { continuation, .. }
178 | Protocol::Materialize { continuation, .. }
179 | Protocol::Handoff { continuation, .. }
180 | Protocol::DependentWork { continuation, .. } => {
181 self.analyze_protocol(continuation);
182 }
183 }
184 }
185
186 fn analyze_send(
187 &mut self,
188 from: &Role,
189 to: &Role,
190 message_name: &str,
191 continuation: &Protocol,
192 ) {
193 if let Some(stats) = self.role_stats.get_mut(from) {
194 stats.sends += 1;
195 }
196 if let Some(stats) = self.role_stats.get_mut(to) {
197 stats.receives += 1;
198 }
199 self.comm_graph
200 .edges
201 .push((from.clone(), to.clone(), message_name.to_string()));
202 self.analyze_protocol(continuation);
203 }
204
205 fn analyze_broadcast(
206 &mut self,
207 from: &Role,
208 to_all: &crate::ast::NonEmptyVec<Role>,
209 message_name: &str,
210 continuation: &Protocol,
211 ) {
212 if let Some(stats) = self.role_stats.get_mut(from) {
213 stats.sends += to_all.len();
214 }
215 for to in to_all {
216 if let Some(stats) = self.role_stats.get_mut(to) {
217 stats.receives += 1;
218 }
219 self.comm_graph.edges.push((
220 from.clone(),
221 to.clone(),
222 format!("{message_name} (broadcast)"),
223 ));
224 }
225 self.analyze_protocol(continuation);
226 }
227
228 fn analyze_choice(
229 &mut self,
230 role: &Role,
231 branches: &crate::ast::NonEmptyVec<crate::ast::Branch>,
232 ) {
233 if let Some(stats) = self.role_stats.get_mut(role) {
234 stats.choices += 1;
235 }
236
237 let recipients: HashSet<_> = branches
238 .iter()
239 .filter_map(|branch| match &branch.protocol {
240 Protocol::Send { to, .. } => Some(to.clone()),
241 _ => None,
242 })
243 .collect();
244 if recipients.len() > 1 {
245 self.warnings
246 .push(AnalysisWarning::AsymmetricChoice(role.clone()));
247 }
248
249 for branch in branches {
250 self.analyze_protocol(&branch.protocol);
251 }
252 }
253
254 fn check_deadlock_freedom(&self) -> bool {
255 let mut dependencies: HashMap<Role, HashSet<Role>> = HashMap::new();
260 for role in &self.choreography.roles {
261 dependencies.insert(role.clone(), HashSet::new());
262 }
263
264 Self::extract_dependencies(&self.choreography.protocol, &mut dependencies);
266
267 !has_cycle(&dependencies)
269 }
270
271 fn extract_dependencies(protocol: &Protocol, deps: &mut HashMap<Role, HashSet<Role>>) {
272 match protocol {
273 Protocol::Send {
274 from,
275 to,
276 continuation,
277 ..
278 } => {
279 if let Some(to_deps) = deps.get_mut(to) {
280 to_deps.insert(from.clone());
281 }
282 Self::extract_dependencies(continuation, deps);
283 }
284 Protocol::Choice { branches, .. } => {
285 for branch in branches {
286 Self::extract_dependencies(&branch.protocol, deps);
287 }
288 }
289 Protocol::Case { branches, .. } => {
290 for branch in branches {
291 Self::extract_dependencies(&branch.protocol, deps);
292 }
293 }
294 Protocol::Timeout {
295 body,
296 on_timeout,
297 on_cancel,
298 ..
299 } => {
300 Self::extract_dependencies(body, deps);
301 Self::extract_dependencies(on_timeout, deps);
302 if let Some(on_cancel) = on_cancel.as_deref() {
303 Self::extract_dependencies(on_cancel, deps);
304 }
305 }
306 Protocol::Loop { body, .. } => {
307 Self::extract_dependencies(body, deps);
308 }
309 Protocol::Parallel { protocols } => {
310 for p in protocols {
312 Self::extract_dependencies(p, deps);
313 }
314 }
315 Protocol::Rec { body, .. } => {
316 Self::extract_dependencies(body, deps);
317 }
318 Protocol::Broadcast { continuation, .. } => {
319 Self::extract_dependencies(continuation, deps);
320 }
321 Protocol::Var(_) | Protocol::End => {}
322
323 Protocol::Begin { continuation, .. }
324 | Protocol::Await { continuation, .. }
325 | Protocol::Resolve { continuation, .. }
326 | Protocol::Invalidate { continuation, .. }
327 | Protocol::Extension { continuation, .. }
328 | Protocol::Let { continuation, .. }
329 | Protocol::Publish { continuation, .. }
330 | Protocol::PublishAuthority { continuation, .. }
331 | Protocol::Materialize { continuation, .. }
332 | Protocol::Handoff { continuation, .. }
333 | Protocol::DependentWork { continuation, .. } => {
334 Self::extract_dependencies(continuation, deps);
335 }
336 }
337 }
338
339 fn check_progress(&self) -> bool {
340 Self::check_protocol_progress(&self.choreography.protocol)
342 }
343
344 fn check_protocol_progress(protocol: &Protocol) -> bool {
345 match protocol {
346 Protocol::End => true,
347 Protocol::Send { continuation, .. } => {
348 Self::check_protocol_progress(continuation)
350 }
351 Protocol::Choice { branches, .. } => {
352 branches
354 .iter()
355 .all(|b| Self::check_protocol_progress(&b.protocol))
356 }
357 Protocol::Case { branches, .. } => branches
358 .iter()
359 .all(|b| Self::check_protocol_progress(&b.protocol)),
360 Protocol::Timeout {
361 body,
362 on_timeout,
363 on_cancel,
364 ..
365 } => {
366 Self::check_protocol_progress(body)
367 && Self::check_protocol_progress(on_timeout)
368 && match on_cancel.as_deref() {
369 Some(protocol) => Self::check_protocol_progress(protocol),
370 None => true,
371 }
372 }
373 Protocol::Loop { body, .. } => {
374 has_communication(body)
376 }
377 Protocol::Parallel { protocols } => protocols.iter().all(Self::check_protocol_progress),
378 Protocol::Rec { body, .. } => {
379 has_communication(body)
381 }
382 Protocol::Var(_) => true, Protocol::Broadcast { continuation, .. } => Self::check_protocol_progress(continuation),
384
385 Protocol::Begin { continuation, .. }
386 | Protocol::Await { continuation, .. }
387 | Protocol::Resolve { continuation, .. }
388 | Protocol::Invalidate { continuation, .. }
389 | Protocol::Extension { continuation, .. }
390 | Protocol::Let { continuation, .. }
391 | Protocol::Publish { continuation, .. }
392 | Protocol::PublishAuthority { continuation, .. }
393 | Protocol::Materialize { continuation, .. }
394 | Protocol::Handoff { continuation, .. }
395 | Protocol::DependentWork { continuation, .. } => {
396 Self::check_protocol_progress(continuation)
397 }
398 }
399 }
400
401 fn compute_participation_info(&self) -> HashMap<Role, ParticipationInfo> {
402 let mut result = HashMap::new();
403
404 for (role, stats) in &self.role_stats {
405 result.insert(
406 role.clone(),
407 ParticipationInfo {
408 sends: stats.sends,
409 receives: stats.receives,
410 choices: stats.choices,
411 is_active: stats.sends > 0 || stats.receives > 0 || stats.choices > 0,
412 },
413 );
414 }
415
416 result
417 }
418}
419
420#[must_use]
422pub fn generate_dot_graph(comm_graph: &CommunicationGraph) -> String {
423 let mut dot = String::from("digraph G {\n");
424 dot.push_str(" rankdir=LR;\n");
425 dot.push_str(" node [shape=circle];\n");
426
427 for node in &comm_graph.nodes {
429 dot.push_str(&format!(" {};\n", node.name()));
430 }
431
432 for (from, to, label) in &comm_graph.edges {
434 dot.push_str(&format!(
435 " {} -> {} [label=\"{}\"];\n",
436 from.name(),
437 to.name(),
438 label
439 ));
440 }
441
442 dot.push_str("}\n");
443 dot
444}