TargetSpec

taco_model_checker

Trait TargetSpec 

Source 
pub trait TargetSpec: Display {
    // Required methods
    fn get_locations_in_target(&self) -> impl IntoIterator<Item = &Location>;
    fn get_variable_constraint(
        &self,
    ) -> impl IntoIterator<Item = &LIAVariableConstraint>;
}
Expand description

Common trait implemented by types that specify a target configuration in model checking

This trait is mostly used in preprocessing to ensure target locations are not removed by accident

Required Methods§

Source

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

Get the locations that appear in the target

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

Source

fn get_variable_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", so this trait is not object safe.

Implementors§