Enum ITreeNode 

pub enum ITreeNode<E, R> {
    Ret(R),
    Tau(Box<dyn FnOnce() -> ITreeNode<E, R>>),
    Vis(E, Box<dyn Fn(usize) -> ITreeNode<E, R>>),
}

An interaction tree node modelling one step of a potentially-infinite computation.

Based on the ITree structure used in verified concurrency frameworks.

Variants

Ret(R)

Pure return value.

Tau(Box<dyn FnOnce() -> ITreeNode<E, R>>)

Silent step (τ): delays computation by one tick.

Vis(E, Box<dyn Fn(usize) -> ITreeNode<E, R>>)

Visible event e followed by a continuation k.

Implementations

impl<E: Clone, R: Clone> ITreeNode<E, R>

pub fn ret(r: R) -> Self

Construct a pure return.

pub fn tau<F: FnOnce() -> ITreeNode<E, R> + 'static>(f: F) -> Self

Construct a tau step.

pub fn vis<K: Fn(usize) -> ITreeNode<E, R> + 'static>(e: E, k: K) -> Self

Construct a visible event step.

pub fn run(self, fuel: usize) -> Option<R>

Spin-up at most fuel tau steps and return the result if reached.