Struct ELTLSpecificationBuilder 

pub struct ELTLSpecificationBuilder<'a, T: ThresholdAutomaton> {
    ta: &'a T,
    properties: Vec<ELTLProperty>,
}

Builder for building an ELTLSpecification over a threshold automaton

Example

use taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder;
use taco_threshold_automaton::expressions::{IntegerExpression, ComparisonOp, Location, Variable};
use taco_model_checker::eltl::{ELTLExpression, ELTLSpecificationBuilder};

let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
    .with_variables(vec![
        Variable::new("var1"),
        Variable::new("var2"),
        Variable::new("var3"),
    ])
    .unwrap()
    .with_locations(vec![
        Location::new("loc1"),
        Location::new("loc2"),
    ])
    .unwrap()
    .initialize()
    .build();

let mut builder = ELTLSpecificationBuilder::new(&ta);

let expr1 = ELTLExpression::LocationExpr(
    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(2)),
);

let expr2 = ELTLExpression::LocationExpr(
    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(0)),
);

builder.add_expressions(vec![
    ("spec1".to_string(), expr1),
    ("spec2".to_string(), expr2),
]).unwrap();

let spec = builder.build();

assert_eq!(spec.expressions().len(), 2);
assert!(spec.expressions().iter().any(|(name, _)| name == "spec1"));
assert!(spec.expressions().iter().any(|(name, _)| name == "spec2"));

Fields

ta: &'a T

Threshold automaton associated with the expressions

properties: Vec<ELTLProperty>

Collection of tuples of expression names and the ELTL expression

Implementations

impl<T: ThresholdAutomaton> ELTLSpecificationBuilder<'_, T>

fn check_for_unknown_identifier<S>( &self, expr: &IntegerExpression<S>, ) -> Result<(), InternalELTLExpressionBuilderError>

where S: Atomic, Self: IsDeclared<S>,

Check if all identifiers in the expression are known

Returns () if no unknown identifier is found, otherwise the name of the unknown identifier

fn check_contains_parameter_expression( expr: &ELTLExpression, ) -> Result<(), InternalELTLExpressionBuilderError>

Check whether an ELTL expression contains a parameter expression

fn replace_trivial_expressions(expr: ELTLExpression) -> ELTLExpression

Replaces parameter expressions that do not contain parameters

fn validate_property( &self, expr: &ELTLExpression, ) -> Result<(), InternalELTLExpressionBuilderError>

Check if all atoms in the expression are known in the threshold automaton associated with the builder and that all location expressions are valid

pub fn add_expression( &mut self, name: String, expr: ELTLExpression, ) -> Result<(), ELTLExpressionBuilderError>

Add a new ELTL expression to the specification

This function checks if all atoms in the expression are known in the threshold automaton associated with the builder. If an unknown atom is found, an error is returned. Otherwise the expression is added to the specification.

This function also returns an error if the name of the expression is already used in the specification.

pub fn add_expressions( &mut self, expressions: impl IntoIterator<Item = ELTLProperty>, ) -> Result<(), ELTLExpressionBuilderError>

Add multiple ELTL expressions to the specification

This function checks if all atoms in the expression are known in the threshold automaton associated with the builder. If an unknown atom is found, an error is returned. Otherwise the expression is added to the specification.

This function also returns an error if the name of the expression is already used in the specification.

pub fn build(self) -> ELTLSpecification

Build the ELTL specification

Returns the ELTL specification containing all added expressions

impl<'a, T: ThresholdAutomaton> ELTLSpecificationBuilder<'a, T>

pub fn new(ta: &'a T) -> Self

Create a new empty ELTL specification builder

Trait Implementations

impl<T: ThresholdAutomaton> IsDeclared<Location> for ELTLSpecificationBuilder<'_, T>

fn is_declared(&self, obj: &Location) -> bool

Check if object of type T is declared

impl<T: ThresholdAutomaton> IsDeclared<Parameter> for ELTLSpecificationBuilder<'_, T>

fn is_declared(&self, obj: &Parameter) -> bool

Check if object of type T is declared

impl<T: ThresholdAutomaton> IsDeclared<Variable> for ELTLSpecificationBuilder<'_, T>

fn is_declared(&self, obj: &Variable) -> bool

Check if object of type T is declared