Skip to main content

TASpecification

taco_model_checker

Trait TASpecification 

Source 
pub trait TASpecification: Display {
    // Required methods
    fn locs_appearing(&self) -> impl IntoIterator<Item = &Location>;
    fn var_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint>;
}
Expand description

Common trait implemented by specifications

This trait is mostly used in preprocessing to inform the preprocessor which locations and variables appear in the specification, to ensure that they can be treated separately

Required Methods§

Source

fn locs_appearing(&self) -> impl IntoIterator<Item = &Location>

Get the locations that appear in the specification

This function can be used in the preprocessing to ensure no locations from the specification are removed

Source

fn var_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint>

Get the variable constraints that appear in target

This function can be used to get the interval constraints of variables in the target specification.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§