Enum ELTLExpression 

pub enum ELTLExpression {
    Implies(Box<ELTLExpression>, Box<ELTLExpression>),
    Globally(Box<ELTLExpression>),
    Eventually(Box<ELTLExpression>),
    And(Box<ELTLExpression>, Box<ELTLExpression>),
    Or(Box<ELTLExpression>, Box<ELTLExpression>),
    Not(Box<ELTLExpression>),
    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,
}

ELTL (LTL without next) expressions for threshold automata

This module provides the types defining ELTL expressions without a next operator for threshold automata. In the literature these formulas are also called ELTL or fault-tolerant temporal logic.

Example

use taco_threshold_automaton::expressions::{IntegerExpression, ComparisonOp, Location};
use taco_model_checker::eltl::ELTLExpression;

// loc1 = 0 => □(loc_agree_1 = 0)
let _ = ELTLExpression::Implies(
 Box::new(ELTLExpression::LocationExpr(
    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(0)),
 )),
 Box::new(ELTLExpression::Globally(
    Box::new(ELTLExpression::LocationExpr(
        Box::new(IntegerExpression::Atom(Location::new("loc_agree_1"))),
        ComparisonOp::Eq,
        Box::new(IntegerExpression::Const(0)),
    )),
 )));

Variants

Implies(Box<ELTLExpression>, Box<ELTLExpression>)

Implication ⟹

Globally(Box<ELTLExpression>)

Globally □

Eventually(Box<ELTLExpression>)

Eventually ◇

And(Box<ELTLExpression>, Box<ELTLExpression>)

And ∧

Or(Box<ELTLExpression>, Box<ELTLExpression>)

Or ∨

Not(Box<ELTLExpression>)

Not ¬

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>>)

Expression over the value of parameters

True

Always true

False

Always false

Implementations

impl ELTLExpression

pub fn remove_negations(&self) -> NonNegatedELTLExpression

Remove boolean negations from an expression, transforming the expression into a NonNegatedELTLExpression expression.

This method is used to remove negations and implications from an LTL expression. Implications are simply transformed into disjunctions, and negations are pushed down to the atomic expressions.

Example

use taco_model_checker::eltl::ELTLExpression;
use taco_threshold_automaton::expressions::{ComparisonOp, Variable, IntegerExpression};
use taco_model_checker::eltl::remove_negations::NonNegatedELTLExpression;

// (1 = 2) => (x = 1)
let ltl = ELTLExpression::Implies(
    Box::new(ELTLExpression::LocationExpr(
        Box::new(IntegerExpression::Const(1)),
        ComparisonOp::Eq,
        Box::new(IntegerExpression::Const(2)),
    )),
    Box::new(ELTLExpression::VariableExpr(
        Box::new(IntegerExpression::Atom(Variable::new("x"))),
        ComparisonOp::Eq,
        Box::new(IntegerExpression::Const(1)),
    )),
);

let non_negated_ltl = ltl.remove_negations();

// (1 != 2) ∨ (x = 1)
let expected = NonNegatedELTLExpression::Or(
    Box::new(NonNegatedELTLExpression::LocationExpr(
        Box::new(IntegerExpression::Const(1)),
        ComparisonOp::Neq,
        Box::new(IntegerExpression::Const(2)),
    )),
    Box::new(NonNegatedELTLExpression::VariableExpr(
        Box::new(IntegerExpression::Atom(Variable::new("x"))),
        ComparisonOp::Eq,
        Box::new(IntegerExpression::Const(1)),
   )),
);

assert_eq!(non_negated_ltl, expected);

fn negate_expression(&self) -> NonNegatedELTLExpression

impl ELTLExpression

pub fn contains_temporal_operator(&self) -> bool

Check if the expression contains a temporal operator

Returns true if the expression contains a temporal operator, otherwise false

Example

use taco_threshold_automaton::expressions::{IntegerExpression, ComparisonOp, Location};
use taco_model_checker::eltl::ELTLExpression;

let expression = ELTLExpression::LocationExpr(
    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
);
assert!(!expression.contains_temporal_operator());

let expression = ELTLExpression::Globally(Box::new(ELTLExpression::LocationExpr(
    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
)));
assert!(expression.contains_temporal_operator());

Trait Implementations

impl BitAnd for ELTLExpression

type Output = ELTLExpression

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self::Output

Performs the & operation.

impl BitOr for ELTLExpression

type Output = ELTLExpression

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self::Output

Performs the | operation.

impl Clone for ELTLExpression

fn clone(&self) -> ELTLExpression

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ELTLExpression

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

Formats the value using the given formatter.

impl Display for ELTLExpression

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 Hash for ELTLExpression

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Not for ELTLExpression

type Output = ELTLExpression

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl PartialEq for ELTLExpression

fn eq(&self, other: &ELTLExpression) -> 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 ELTLExpression