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 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
//! This module contains the macros and the functions for
//! checking whether a protocol is well written or not,
//! according to a bottom-up method.
//!
//! *This module is available only if MultiCrusty is built with
//! the `"checking"` feature.*
use petgraph::Graph;
use std::collections::hash_map::RandomState;
use std::collections::HashMap;
use std::error::Error;
use std::fs::{create_dir_all, remove_file, File};
use std::io::Write;
use std::process::Command;
use std::str;
#[doc(hidden)]
mod aux_checker;
use aux_checker::*;
type HashGraph = HashMap<String, Graph<String, String>>;
/// The macro that allows to create digraphs from each endpoint,
/// along with `enum` if needed. You can also provide the name of
/// a file for running the [`KMC`] tool and checking the
/// properties of the provided protocol: it will
/// return the minimal `k` according to this tool if it exists,
/// and ```None``` if `k` is bigger than 50 or does not exist.
///
/// The [`KMC`] tool
/// must be installed with `cabal install` and the resulting
/// binary must be added to PATH.
///
/// /!\ The provided types and enum cannot be checked if they contain
/// a parameter, such as <N>, as seen in some examples.
///
/// # Arguments
///
/// * \[Optional\] The name of the new file after running the [`KMC`] tool
/// * Each starting endpoint, separated by a comma
/// * \[Optional\] Each new `MeshedChannels` adopted by each sender of each choice, along with all
/// the different branches sent.
///
/// Currently, we do not support parameters for branches with `enum`
///
/// # Example
///
/// Assume that there are two choices (Branches0BtoA and Branches0CtoA), each one with two branches
/// (Video and End). Assume also that the starting Endpoints of the three roles are EndpointAFull,
/// EndpointCFull and EndpointBFull (the order does not matter). The call for this macro would be as
/// followed
///
/// ```ignore
/// mpstthree::checker_concat!(
/// "", // It's important to have a strng here, either empty or not
/// EndpointAFull,
/// EndpointCFull,
/// EndpointBFull
/// =>
/// [
/// EndpointAVideo,
/// Branches0BtoA, Video,
/// Branches0CtoA, Video
/// ],
/// [
/// EndpointAEnd,
/// Branches0BtoA, End,
/// Branches0CtoA, End
/// ]
/// )
/// ```
///
/// [`KMC`]: https://github.com/julien-lange/kmc
///
/// *This macro is available only if MultiCrusty is built with
/// the `"checking"` feature.*
///
/// May have to be used with the [`checker_concat_impl`]! macro.
#[macro_export]
#[cfg_attr(doc_cfg, doc(cfg(feature = "checking")))]
macro_rules! checker_concat {
(
$name_file: expr,
$(
$sessiontype: ty
),+ $(,)?
) => {
{
let mut sessions = Vec::new();
$(
sessions.push(String::from(std::any::type_name::<$sessiontype>()));
)+
let state_branching_sessions = std::collections::hash_map::RandomState::new();
let branching_sessions: std::collections::HashMap<String, String> =
std::collections::HashMap::with_hasher(state_branching_sessions);
let state_group_branches = std::collections::hash_map::RandomState::new();
let group_branches: std::collections::HashMap<String, i32> =
std::collections::HashMap::with_hasher(state_group_branches);
let state_branches = std::collections::hash_map::RandomState::new();
let branches_receivers: std::collections::HashMap<String, std::collections::HashMap<String, String>> =
std::collections::HashMap::with_hasher(state_branches);
mpstthree::checking::checker(
$name_file,
sessions,
branches_receivers,
branching_sessions,
group_branches
)
}
};
(
$name_file: expr,
$(
$sessiontype: ty
),+ $(,)?
=>
$(
[
$branch_stack: ty,
$(
$choice: ty,
$branch: ident
),+ $(,)?
]
),+ $(,)?
) => {
{
// All the starting sessions, stringified
let mut sessions = Vec::new();
$(
sessions.push(String::from(std::any::type_name::<$sessiontype>()));
)+
// Each choice and branch: { choice_1 : { branch_1 : session_1 ; branch_2 : session_2 ; ... } ; ... }
let state_branching_sessions = std::collections::hash_map::RandomState::new();
let mut branching_sessions: std::collections::HashMap<String, String> =
std::collections::HashMap::with_hasher(state_branching_sessions);
// All branches, grouped by choice: { choice_1::branch_1 : 0 ; choice_1::branch_2 : 1 ; choice_2::branch_1 : 0 ; choice_2::branch_2 : 1 ; ... }
let state_group_branches = std::collections::hash_map::RandomState::new();
let mut group_branches: std::collections::HashMap<String, i32> =
std::collections::HashMap::with_hasher(state_group_branches);
// Start the index for group_branches
let mut index = 0;
$(
let temp_branch_stack = String::from(std::any::type_name::<$branch_stack>());
$(
branching_sessions.insert(
format!(
"{}::{}",
stringify!($choice).to_string(),
stringify!($branch).to_string(),
),
temp_branch_stack.clone()
);
group_branches.insert(
format!(
"{}::{}",
stringify!($choice).to_string(),
stringify!($branch).to_string(),
),
index
);
)+
index += 1;
)+
// Macro to implement Display for the `enum`
mpst_seq_proc::checking!(
$(
$(
{
$choice,
$branch,
}
)+
)+
);
// Create the graphs with the previous inputs
mpstthree::checking::checker(
$name_file,
sessions,
branches_receivers,
branching_sessions,
group_branches
)
}
};
}
/// *This macro is available only if MultiCrusty is built with
/// the `"checking"` feature.*
///
/// Must be used in pair with the [`checker_concat`]! macro
/// when there are choices/branches:
/// [`checker_concat_impl`]! must be used outside of any function
/// to create the functions generated by [`checker_concat`]!.
///
/// Compared with the [`checker_concat`]! macro,
/// here is an example:
///
/// ```ignore
/// mpstthree::checker_concat_impl!(
/// [
/// Branches0BtoA, Video,
/// Branches0CtoA, Video
/// ],
/// [
/// Branches0BtoA, End,
/// Branches0CtoA, End
/// ]
/// );
/// ```
///
/// Notice that there are only the name of the branches,
/// grouped by choice and role.
#[macro_export]
#[cfg_attr(doc_cfg, doc(cfg(feature = "checking")))]
macro_rules! checker_concat_impl {
(
$(
[
$(
$choice: ty,
$branch: ident
),+ $(,)?
]
),+ $(,)?
) => {
// Macro to implement Display for the `enum`
mpst_seq_proc::checking_impl!(
$(
$(
{
$choice,
$branch,
}
)+
)+
);
};
}
// Run the KMC command line
pub(crate) fn kmc_cli(name_file: &str, kmc_number: i32) -> Result<(bool, String), Box<dyn Error>> {
// Delete previous files
remove_file(format!(
"../mpst_rust_github/outputs/{name_file}_{kmc_number}_kmc.txt"
))
.unwrap_or(());
remove_file(format!(
"../mpst_rust_github/outputs/{name_file}-sync-0norm-system.dot"
))
.unwrap_or(());
remove_file(format!(
"../mpst_rust_github/outputs/{name_file}-sync-0norm-system.png"
))
.unwrap_or(());
remove_file(format!(
"../mpst_rust_github/outputs/{name_file}-ts-{kmc_number}.fsm"
))
.unwrap_or(());
// Run KMC tool, the outputs files of the tool are in the "outputs" folder
let kmc = Command::new("KMC")
.arg(format!("cfsm/{name_file}.txt"))
.arg(format!("{kmc_number:?}"))
.arg("--fsm")
.output()?;
let stdout = String::from(str::from_utf8(&kmc.stdout)?);
if stdout.contains("False") {
Ok((false, stdout))
} else {
// Write down the stdout of the previous command into
// a corresponding file in the "outputs" folder
let mut kmc_file = File::create(format!("outputs/{name_file}_{kmc_number}_kmc.txt"))?;
writeln!(kmc_file, "{stdout}")?;
Ok((true, stdout))
}
}
// The starting function for extracting the graphs
#[doc(hidden)]
pub fn checker(
name_file: &str,
sessions: Vec<String>,
branches_receivers: HashMap<String, HashMap<String, String>>,
branching_sessions: HashMap<String, String>,
group_branches: HashMap<String, i32>,
) -> Result<(HashGraph, Option<i32>), Box<dyn Error>> {
// Clean the input sessions and extract the roles
let (clean_sessions, roles) = clean_sessions(sessions.to_vec())?;
// The cleaned branches_receivers
let state_branches = RandomState::new();
let mut update_branches_receivers: HashMap<String, HashMap<String, Vec<String>>> =
HashMap::with_hasher(state_branches);
for (choice, branches) in branches_receivers {
let state_branch = RandomState::new();
let mut temp_branch: HashMap<String, Vec<String>> = HashMap::with_hasher(state_branch);
for (branch, session) in branches {
temp_branch.insert(branch, clean_session(&session)?);
}
update_branches_receivers.insert(choice, temp_branch);
}
// The cleaned branching_sessions
let state_branching_sessions = RandomState::new();
let mut update_branching_sessions: HashMap<String, Vec<String>> =
HashMap::with_hasher(state_branching_sessions);
for (branch, session) in branching_sessions {
let current_clean_session = clean_session(&session)?;
update_branching_sessions.insert(
branch.to_string(),
current_clean_session[..(current_clean_session.len() - 1)].to_vec(),
);
}
// The final result Hashmap
let state_result = RandomState::new();
let mut result: HashGraph = HashMap::with_hasher(state_result);
if !name_file.is_empty() {
// If a name file has been provided
// Create cfsm folder if missing
create_dir_all("cfsm")?;
// Create the file
let mut cfsm_file = File::create(format!("cfsm/{name_file}.txt"))?;
let mut cfsm_sort = vec![vec!["".to_string()]; roles.len()];
// Get all the graphs and add them to the result Hashmap
for (role, full_session) in clean_sessions {
// Get the graph and the cfsm for the current role
let (graph, cfsm) = get_graph_session(
&role,
full_session,
&roles,
update_branches_receivers.clone(),
update_branching_sessions.clone(),
group_branches.clone(),
)?;
// Insert the graph to the returned result
result.insert(role.to_string(), graph);
let index_role = roles.iter().position(|r| r == &role).unwrap();
cfsm_sort[index_role] = cfsm;
}
// Write the cfsm into the file
for elt_cfsm in cfsm_sort.iter() {
for elt in elt_cfsm.iter() {
writeln!(cfsm_file, "{elt}")?;
}
// Add a blank line
writeln!(cfsm_file)?;
}
let mut kmc_number = 1;
let mut kmc_result = kmc_cli(name_file, kmc_number)?;
while !kmc_result.0 && kmc_number < 50 {
kmc_number += 1;
kmc_result = kmc_cli(name_file, kmc_number)?;
}
if kmc_number == 50 {
println!(
"The protocol does not seem correct. Here is the last output: {:?}",
kmc_result.1
);
Ok((result, None))
} else {
Ok((result, Some(kmc_number)))
}
} else {
// Get all the graphs and add them to the result Hashmap
for (role, full_session) in clean_sessions {
// Get the graph and the cfsm for the current role
let (graph, _) = get_graph_session(
&role,
full_session,
&roles,
update_branches_receivers.clone(),
update_branching_sessions.clone(),
group_branches.clone(),
)?;
// Insert the graph to the returned result
result.insert(role.to_string(), graph);
}
Ok((result, None))
}
}