Module mpstthree::role

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

Every structure that relies on this trait, such as RoleA and RoleB, contains at least a parameter, which is a Role itself. The only exception is RoleEnd, which represents the end of any ordering.

Modules

a

This module contains the required definitions and functions for the basic role A. Its dual is RoleADual.

a_dual

This module contains the required definitions and functions for the dual of the basic role A.

a_to_all

This module contains the required definitions and functions for the basic role A when it is making an internal choice. Its dual is RoleAlltoA.

all_to_a

This module contains the required definitions and functions for the basic role A when it is receiving an external choice. Its dual is RoleAtoAll.

all_to_b

This module contains the required definitions and functions for the basic role B when it is receiving an external choice. Its dual is RoleBtoAll.

all_to_c

This module contains the required definitions and functions for the basic role C when it is receiving an external choice. Its dual is RoleCtoAll.

b

This module contains the required definitions and functions for the basic role B. Its dual is RoleBDual.

b_dual

This module contains the required definitions and functions for the dual of the basic role B.

b_to_all

This module contains the required definitions and functions for the basic role B when it is making an internal choice. Its dual is RoleAlltoB.

broadcast

This module contains the required definitions and functions for a role to broadcast multiple choices. Its dual is it self.

c

This module contains the required definitions and functions for the basic role C. Its dual is RoleCDual.

c_dual

This module contains the required definitions and functions for the dual of the basic role C.

c_to_all

This module contains the required definitions and functions for the basic role C when it is making an internal choice. Its dual is RoleAlltoC.

end

This module contains the required definitions and functions for closing a stack. Its dual is it self.

Traits

Role

Trait for session types. Provides duality.