Struct SMTConfigMgr 

pub struct SMTConfigMgr<CR, CC>
where
    CR: StepSMT,
    CC: ConfigFromSMT,
{
    params: Rc<HashMap<Parameter, SMTExpr>>,
    configs: Vec<Rc<CC>>,
    configs_primed: Vec<Rc<CC>>,
    step_steps: Vec<CR>,
    steady_steps: Vec<CR>,
}

Manager of configurations for a threshold automaton

Fields

params: Rc<HashMap<Parameter, SMTExpr>>

configs: Vec<Rc<CC>>

configs_primed: Vec<Rc<CC>>

step_steps: Vec<CR>

steady_steps: Vec<CR>

Implementations

impl<CR, CC> SMTConfigMgr<CR, CC>

where CR: StepSMT, CC: ConfigFromSMT,

pub fn new(params: Rc<HashMap<Parameter, SMTExpr>>) -> Self

Create a new manager

pub fn params(&self) -> &Rc<HashMap<Parameter, SMTExpr>>

Get a reference to the parameter variables

pub fn push_steady(&mut self, step_ctx: CR)

Push a new steady configuration

pub fn pop_steady(&mut self)

Pop the last steady configuration

pub fn steady(&self) -> impl Iterator<Item = &CR>

Iterate over all steady steps

pub fn push_step(&mut self, step_ctx: CR)

Push a new step

pub fn pop_step(&mut self)

Pop a step

pub fn step(&self) -> impl Iterator<Item = &CR>

Iterate over all steps

pub fn push_cfg(&mut self, cfg_ctx: Rc<CC>)

Push a new configuration

pub fn pop_cfg(&mut self)

Pop a configuration

pub fn configs(&self) -> impl Iterator<Item = &Rc<CC>>

Iterate over all configurations

pub fn configs_primed(&self) -> impl Iterator<Item = &Rc<CC>>

Iterate over all primed configurations

pub fn push_cfg_primed(&mut self, cfg_ctx: Rc<CC>)

Push a new primed config

pub fn pop_cfg_primed(&mut self)

Pop a primed config

pub fn extract_error_path( &self, res: SMTSolution, solver: &mut SMTSolver, ta: GeneralThresholdAutomaton, ) -> Path

Extract the error path of the computed solution

fn add_transitions_steady_step_to_builder( builder: InitializedPathBuilder, config: Configuration, steady_step: &CR, solver: &mut SMTSolver, res: SMTSolution, ) -> InitializedPathBuilder

Compute the transition defined by a steady step and add them to the error path

fn add_transition_to_builder_and_return_updated_config( builder: InitializedPathBuilder, config: Configuration, rule: Rule, n: u32, ) -> (InitializedPathBuilder, Configuration)

Create the transition that applies rule rule n times, compute the resulting configuration and add it to the path builder. Returns the computed configuration and updated builder.

fn add_transition_step_step_to_builder( builder: InitializedPathBuilder, step_step: &CR, solver: &mut SMTSolver, res: SMTSolution, ) -> InitializedPathBuilder

Compute the transition defined by a step step and add them to the error path