Crate mpstthree

  

Mpstthree (also called MultiCrusty) is a library to write and check communication protocols based on Multiparty Session Types.

Currently this library is geared toward use with Scribble and New Scribble for full checking of protocols.

Modules

bakingbaking

This module contains the macros for creating the different structures and associated functions for any number of participants to simplify send/recv.

binary

The slightly modified binary session type library.

checkingchecking

This module contains the macros and the functions for checking wether a protocol is well written or not, according to a bottom-up method.

functionmpst

This module contains all the functions that are used for consuming MeshedChannels.

macros_multiplemacros_multiple

This module contains all the macros that are used for the parametrisation on the number of participants.

macros_simplemacros_simple

This module contains all the macros that are used for the parametrisation on the name of the participants.

meshedchannels

The main structure used for representing a participant, also named a party, within a protocol.

role

The main trait used for representing an ordering or the name of a participant.

transporttransport

The module for interacting with different modes of transport such as HTTP or TCP

Macros

broadcast_cancelmacros_multiple

Indefinitely loops to check all sessions if there is a Cancel signal and broadcast if it present. Will also close correctly if a Stop signal is received.

bundle_implbaking

Create a new SessionMST structure, new roles and the baking environment.

bundle_impl_with_enumbaking

Create a new SessionMST structuren, new roles and the baking environment. Also create the macros needed for choosing branches. Each macro is linked to a role X and are called as followed: choose_mpst_x_to_all!( s, # the current session enum_1::variant_1, # the first branch for the first passive role enum_2::variant_2, # the first branch for the second passive role … enum_n::variant_n, # the first branch for the n-th passive role )

bundle_struct_fork_close_multimacros_multiple

Creates the structure MeshedChannels create_meshedchannels, the close_mpst and fork_mpst_multi.

bundle_struct_fork_close_multi_cancelmacros_multiple

Creates the structure MeshedChannels create_meshedchannels, the close_mpst_cancel and fork_mpst_multi functions to be used with more than 2 participants. It checks the send sides of the channels along the recv sides.

checker_concatchecking

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. The KMC repository must be installed next to the current one.

choose

Choose between many different sessions wrapped in an enum

choose_mpst_a_to_all

Choose, for A, among two different sessions

choose_mpst_b_to_all

Choose, for B, among two different sessions

choose_mpst_c_to_all

Choose, for C, among two different sessions

choose_mpst_create_multi_to_allmacros_multiple

Create a macro that simplifies the usage of choose_mpst_multi_to_all.

choose_mpst_multi_cancel_to_allmacros_multiple

Choose among different sessions that are provided, may fail because of a canceled session. Need to exclude the first participant

choose_mpst_multi_http_to_allmacros_multiple

Choose among different sessions that are provided.

choose_mpst_multi_to_allmacros_multiple

Choose among different sessions that are provided.

choose_mpst_to_allmacros_simple

Choose among two different sessions. Must be used with MeshedChannels.

choose_tcptransport

Choose between many different sessions wrapped in an enum

close_mpstmacros_multiple

Create the close function to be used with more than 3 participants.

close_mpst_cancelmacros_multiple

Create the close function to be used with more than 3 participants. It is used for checking the send sides upon closing.

close_mpst_check_cancelmacros_multiple

Create the close function to be used with more than 3 participants.

create_broadcast_rolemacros_simple

Create a new broadcast Role and its dual. A broadcast Role is used for sending a choice. Its dual is used for receving this choice.

create_broadcast_role_shortmacros_simple

Create a new broadcast Role and its dual. A broadcast Role is used for sending a choice. Its dual is used for receving this choice. When a name X is given, the Roles created are

create_choose_both_from_1_to_2_and_3macros_simple

Call both create_choose_right_from_1_to_2_and_3 and create_choose_left_from_1_to_2_and_3. Must be used with MeshedChannels.

create_choose_both_from_2_to_1_and_3macros_simple

Call both create_choose_right_from_2_to_1_and_3 and create_choose_left_from_2_to_1_and_3. Must be used with MeshedChannels.

create_choose_both_from_3_to_1_and_2macros_simple

Call both create_choose_right_from_3_to_1_and_2 and create_choose_left_from_3_to_1_and_2. Must be used with MeshedChannels.

create_choose_left_from_1_to_2_and_3macros_simple

Create the ChooseMpst function to send a Choose left branch from the first role to the others. Must be used with MeshedChannels.

create_choose_left_from_2_to_1_and_3macros_simple

Create the ChooseMpst function to send a Choose left branch from the second role to the others. Must be used with MeshedChannels.

create_choose_left_from_3_to_1_and_2macros_simple

Create the ChooseMpst function to send a Choose left branch from the third role to the others. Must be used with MeshedChannels.

create_choose_mpst_session_multi_bothmacros_multiple

Create the two ChooseMpst functions to send a Choose on each branch to be used with more than 3 participants. Only works when active role is the last one (TODO: adapt to any index role).

create_choose_mpst_session_multi_leftmacros_multiple

Create the ChooseMpst function to send a Choose left branch to be used with more than 3 participants. Only works when active role is the last one (TODO: adapt to any index role).

create_choose_mpst_session_multi_rightmacros_multiple

Create the ChooseMpst function to send a Choose right branch to be used with more than 3 participants. Only works when active role is the last one (TODO: adapt to any index role).

create_choose_right_from_1_to_2_and_3macros_simple

Create the ChooseMpst function to send a Choose right branch from the first role to the others. Must be used with MeshedChannels.

create_choose_right_from_2_to_1_and_3macros_simple

Create the ChooseMpst function to send a Choose right branch from the second role to the others. Must be used with MeshedChannels.

create_choose_right_from_3_to_1_and_2macros_simple

Create the ChooseMpst function to send a Choose right branch from the third role to the others. Must be used with MeshedChannels.

create_choose_type_multimacros_multiple

Create the ChooseMpst type to be used with more than 3 participants.

create_fn_choose_mpst_cancel_multi_to_all_bundlemacros_multiple

Create choose fuunctions, to choose among different sessions that are provided.

create_fn_choose_mpst_multi_to_all_bundlemacros_multiple

Create choose fuunctions, to choose among different sessions that are provided.

create_meshedchannelsmacros_multiple

Creates a MeshedChannels for more than 3 participants.

create_multiple_broadcast_rolemacros_simple

Create multiple new broadcast Role and its dual. A broadcast Role is used for sending a choice. Its dual is used for receving this choice.

create_multiple_broadcast_role_shortmacros_simple

Create multiple new broadcast Role and its dual. A broadcast Role is used for sending a choice. Its dual is used for receving this choice. When a name X is given, the Roles created are

create_multiple_normal_rolemacros_simple

Create multiple new Role and its dual.

create_multiple_normal_role_shortmacros_simple

Create multiple new Role and its dual. When a name X is given, the Roles created are

create_normal_rolemacros_simple

Create a new Role and its dual.

create_normal_role_shortmacros_simple

Create a new Role and its dual. When a name X is given, the Roles created are

create_offer_mpst_session_1macros_simple

Create an offer function to recv on the first binary session from any kind of role. Must be used with MeshedChannels.

create_offer_mpst_session_2macros_simple

Create an offer function to recv on the second binary session from any kind of role. Must be used with MeshedChannels.

create_offer_mpst_session_multimacros_multiple

Creates an OfferMpst function to receive an offer on a given binary session type of a MeshedChannels.

create_offer_type_multimacros_multiple

Create the OfferMpst type to be used with more than 3 participants.

create_recv_http_sessiontransport

Creates a recv function to receive from a simple role on a given binary session type of a MeshedChannels.

create_recv_http_session_bundletransport

Creates multiple recv functions to receive from a simple role on a given binary session type of a MeshedChannels.

create_recv_mpst_sessionmacros_multiple

Creates a recv function to receive from a simple role on a given binary session type of a MeshedChannels.

create_recv_mpst_session_1macros_simple

Create a recv function to recv on the first binary session from any kind of role. Must be used with MeshedChannels.

create_recv_mpst_session_2macros_simple

Create a recv function to recv on the second binary session from any kind of role. Must be used with MeshedChannels.

create_recv_mpst_session_bundlemacros_multiple

Creates multiple recv functions to receive from a simple role on a given binary session type of a MeshedChannels.

create_send_check_cancelmacros_multiple

Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants. Checks if the first binary session has a “cancel” signal and panic if yes. The send function will try to send and panic if not possible (canceled session).

create_send_check_cancel_bundlemacros_multiple

Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.

create_send_http_sessiontransport

Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants.

create_send_mpst_cancelmacros_multiple

Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants. The send function will try to send and panic if not possible (canceled session).

create_send_mpst_cancel_bundlemacros_multiple

Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.

create_send_mpst_http_bundletransport

Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.

create_send_mpst_sessionmacros_multiple

Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants.

create_send_mpst_session_1macros_simple

Create a send function to send on the first binary session from any kind of role. Must be used with MeshedChannels.

create_send_mpst_session_2macros_simple

Create a send function to send on the second binary session from any kind of role. Must be used with MeshedChannels.

create_send_mpst_session_bundlemacros_multiple

Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.

fork_mpst_multimacros_multiple

Creates the fork function to be used with more than 3 participants.

offer

Offer a choice between many different sessions wrapped in an enum

offer_cancel_mpstmacros_multiple

Offer a choice and send the session to the broadcaster

offer_http_mpstmacros_multiple

Offer a choice between many different sessions wrapped in an enum. Used with http functions

offer_mpstmacros_multiple

Offer a choice between many different sessions wrapped in an enum

offer_mpst_a_to_b

Offer a choice to A from B between many different sessions wrapped in an enum

offer_mpst_a_to_c

Offer a choice to A from C between many different sessions wrapped in an enum

offer_mpst_b_to_a

Offer a choice to B from A between many different sessions wrapped in an enum

offer_mpst_b_to_c

Offer a choice to B from C between many different sessions wrapped in an enum

offer_mpst_c_to_a

Offer a choice to C from A between many different sessions wrapped in an enum

offer_mpst_c_to_b

Offer a choice to C from B between many different sessions wrapped in an enum

offer_tcptransport

Offer a choice between many different sessions wrapped in an enum

recv_mpstmacros_multiple

Shorter way to call the code within the recv function instead of having to create the function itself.

send_cancelmacros_multiple

Creates a function that will cancel a session and send a Cancel signal to the broadcasting role.

send_mpstmacros_multiple

Shorter way to call the code within the send function instead of having to create the function itself.