Module mpstthree::role

source ·
Expand description

The main trait used for representing an ordering 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.