Enum NonNegatedELTLExpression 

pub enum NonNegatedELTLExpression {
    Globally(Box<NonNegatedELTLExpression>),
    Eventually(Box<NonNegatedELTLExpression>),
    And(Box<NonNegatedELTLExpression>, Box<NonNegatedELTLExpression>),
    Or(Box<NonNegatedELTLExpression>, Box<NonNegatedELTLExpression>),
    LocationExpr(Box<IntegerExpression<Location>>, ComparisonOp, Box<IntegerExpression<Location>>),
    VariableExpr(Box<IntegerExpression<Variable>>, ComparisonOp, Box<IntegerExpression<Variable>>),
    ParameterExpr(Box<IntegerExpression<Parameter>>, ComparisonOp, Box<IntegerExpression<Parameter>>),
    True,
    False,
}

LTL Expression without negations and implications

Variants

Globally(Box<NonNegatedELTLExpression>)

Globally □

Eventually(Box<NonNegatedELTLExpression>)

Eventually ◇

And(Box<NonNegatedELTLExpression>, Box<NonNegatedELTLExpression>)

And ∧

Or(Box<NonNegatedELTLExpression>, Box<NonNegatedELTLExpression>)

Or ∨

LocationExpr(Box<IntegerExpression<Location>>, ComparisonOp, Box<IntegerExpression<Location>>)

Boolean constraint over the number of processes in a location

VariableExpr(Box<IntegerExpression<Variable>>, ComparisonOp, Box<IntegerExpression<Variable>>)

Boolean constraint over the value of a variable

ParameterExpr(Box<IntegerExpression<Parameter>>, ComparisonOp, Box<IntegerExpression<Parameter>>)

Boolean constraint over parameters

True

Always true

False

Always false

Trait Implementations

impl Clone for NonNegatedELTLExpression

fn clone(&self) -> NonNegatedELTLExpression

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NonNegatedELTLExpression

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

Formats the value using the given formatter.

impl From<ELTLExpression> for NonNegatedELTLExpression

fn from(value: ELTLExpression) -> Self

Converts to this type from the input type.

impl PartialEq for NonNegatedELTLExpression

fn eq(&self, other: &NonNegatedELTLExpression) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for NonNegatedELTLExpression