Macro mpstthree::checker_concat [−][src]
macro_rules! checker_concat {
($($sessiontype : ty), + $(,) ?) => { ... };
($name_file : expr, $($sessiontype : ty), + $(,) ?) => { ... };
($($sessiontype : ty), + $(,) ? =>
$([$branch_stack : ty, $($choice : ty, $branch : ident), + $(,) ?]), + $(,)
?) => { ... };
($name_file : expr, $($sessiontype : ty), + $(,) ? =>
$([$branch_stack : ty, $($choice : ty, $branch : ident), + $(,) ?]), + $(,)
?) => { ... };
}
checking
only.Expand description
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 in the current repository folder.
/!\ The provided types and enum cannot be checked if they contain
a parameter, such as
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
mpstthree::checker_concat!(
EndpointAFull,
EndpointCFull,
EndpointBFull
=>
[
EndpointAVideo,
Branches0BtoA, Video,
Branches0CtoA, Video
],
[
EndpointAEnd,
Branches0BtoA, End,
Branches0CtoA, End
]
)
This macro is available only if MultiCrusty is built with
the "checking"
feature.