Macro mpstthree::checker_concat

macro_rules! checker_concat {
    (
        $name_file: expr,
        $(
            $sessiontype: ty
        ),+ $(,)?
    ) => { ... };
    (
        $name_file: expr,
        $(
            $sessiontype: ty
        ),+ $(,)?
        =>
        $(
            [
                $branch_stack: ty,
                $(
                    $choice: ty,
                    $branch: ident
                ),+ $(,)?
            ]
        ),+ $(,)?
    ) => { ... };
}

Available on crate feature checking only.

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 , 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

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
    ]
)

This macro is available only if MultiCrusty is built with the "checking" feature.

May have to be used with the [checker_concat_impl]! macro.