Struct SessionTypeCompatibility 

pub struct SessionTypeCompatibility;

Checks compatibility (duality) between two session types.

Implementations

impl SessionTypeCompatibility

pub fn new() -> Self

Create a new compatibility checker.

pub fn dual(&self, s: &BinarySession) -> BinarySession

Compute the dual of a session type (swap sends↔receives, select↔offer).

pub fn are_dual(&self, s1: &BinarySession, s2: &BinarySession) -> bool

Check whether s1 and s2 are dual (i.e., compatible). A process holding s1 can communicate with one holding s2.

pub fn compatible(&self, s1: &BinarySession, s2: &BinarySession) -> bool

Check that a pair of sessions can reduce to End together (session progress). This is a simple syntactic check: both are End, or both are dual in one step.

Trait Implementations

impl Default for SessionTypeCompatibility

fn default() -> Self

Returns the “default value” for a type.