Crate mpstthree

  

Mpstthree (also called Multi-Crusty) 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

binary

The slightly modified binary session type library.

checking

This module is a beta feature that only works with RoleA, RoleB and RoleC. It also has various prerequisites that are shown in tests 06.

fork

This module contains the functions for forking the different endpoints.

functionmpst

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

macros

This module contains all the macros that are used for the parametrisation on the name and number of 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.

Macros

broadcast_cancel

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_impl

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

bundle_impl_with_enum

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_multi

Creates the structure MeshedChannels create_meshedchannels, the close_mpst and fork_mpst_multi.

bundle_struct_fork_close_multi_cancel

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.

checking

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_all

Create a macro that simplifies the usage of choose_mpst_multi_to_all.

choose_mpst_multi_cancel_to_all

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_all

Choose among different sessions that are provided.

choose_mpst_multi_to_all

Choose among different sessions that are provided.

choose_mpst_to_all

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

choose_tcp

Choose between many different sessions wrapped in an enum

close_mpst

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

close_mpst_cancel

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_cancel

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

create_broadcast_role

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_short

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_3

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_3

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_2

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_3

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_3

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_2

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_both

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_left

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_right

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_3

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_3

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_2

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_multi

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

create_fn_choose_mpst_cancel_multi_to_all_bundle

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

create_fn_choose_mpst_multi_to_all_bundle

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

create_meshedchannels

MeshedChannels Creates a MeshedChannels for more than 3 participants.

create_multiple_broadcast_role

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_short

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_role

Create multiple new Role and its dual.

create_multiple_normal_role_short

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

create_normal_role

Create a new Role and its dual.

create_normal_role_short

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

create_offer_mpst_session_1

OFFER 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_2

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_multi

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

create_offer_type_multi

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

create_recv_http_session

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

create_recv_http_session_bundle

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

create_recv_mpst_all_session

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

create_recv_mpst_session

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

create_recv_mpst_session_1

RECV 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_2

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_bundle

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

create_send_check_cancel

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_bundle

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

create_send_http_session

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

create_send_mpst_cancel

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_bundle

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

create_send_mpst_http_bundle

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

create_send_mpst_session

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

create_send_mpst_session_1

SEND 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_2

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_bundle

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

fork_mpst_multi

FORK 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_mpst

Offer a choice and send the session to the broadcaster

offer_http_mpst

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

offer_mpst

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_tcp

Offer a choice between many different sessions wrapped in an enum

recv_mpst

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

send_cancel

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

send_mpst

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