Enum PathOperation 

pub enum PathOperation<N: CfgState, D: ModelTransition<N::Model>> {
    Next(Rc<CtlFormula<N, D>>),
    Eventually(Rc<CtlFormula<N, D>>),
    Always(Rc<CtlFormula<N, D>>),
    Until(Rc<CtlFormula<N, D>>, Rc<CtlFormula<N, D>>),
}

Variants

Next(Rc<CtlFormula<N, D>>)

Eventually(Rc<CtlFormula<N, D>>)

Always(Rc<CtlFormula<N, D>>)

Until(Rc<CtlFormula<N, D>>, Rc<CtlFormula<N, D>>)

Implementations

impl<N: CfgState, D: ModelTransition<N::Model>> PathOperation<N, D>

pub fn next<T: Borrow<CtlFormula<N, D>>>(f: T) -> Self

pub fn eventually<T: Borrow<CtlFormula<N, D>>>(f: T) -> Self

pub fn always<T: Borrow<CtlFormula<N, D>>>(f: T) -> Self

pub fn until<T: Borrow<CtlFormula<N, D>>, U: Borrow<CtlFormula<N, D>>>( a: T, b: U, ) -> Self

Trait Implementations

impl<N: Clone + CfgState, D: Clone + ModelTransition<N::Model>> Clone for PathOperation<N, D>

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<N: CfgState, D: ModelTransition<N::Model>> Debug for PathOperation<N, D>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.