Struct LazyStepContext 

pub struct LazyStepContext<TA, C>
where
    TA: ThresholdAutomaton,
    C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,
{
    index: usize,
    rule_vars: BTreeMap<Rule, SMTExpr>,
    ta: Rc<TA>,
    prev_config: Rc<C>,
    curr_config: Rc<C>,
}

Context for rule applications in a path on a threshold automaton

This context creates SMT variables for rule applications for all rules that were supplied during the context creation.

It then allows to encode the possible paths using the LazyStepContext::encode_phi_step and LazyStepContext::encode_phi_steady functions.

Fields

index: usize

index of the configuration

rule_vars: BTreeMap<Rule, SMTExpr>

variables for rules

ta: Rc<TA>

threshold automaton

prev_config: Rc<C>

previous configuration

curr_config: Rc<C>

current configuration

Implementations

impl<TA, C> LazyStepContext<TA, C>

where TA: ThresholdAutomaton, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,

pub fn new( rules_to_appl: impl Iterator<Item = Rule>, ta: Rc<TA>, prev_config: Rc<C>, curr_config: Rc<C>, index: usize, solver: &mut SMTSolver, ) -> LazyStepContext<TA, C>

Create a new step context for encoding a step between two configurations σ and σ’

A step context stores the rule variables that are needed to specify the transition between two configurations of a threshold automaton.

fn encode_phi_base(&self, solver: &SMTSolver) -> SMTExpr

Encodes the ϕ_{base} of the step context

The encoding of phi base is slightly modified to require less parameters, the encoding does not include:

• the constraint σ.p = σ’.p for all parameters p
• the constraint RC(σ.p)
• the constraint N(σ.p) = N(σ’.p)

This is because we assume that the valuation of the parameters does not change during the execution. Therefore we instead only need to encode the resilience conditions once, which is done in the context manager. Afterwards, we can simply use the global parameter variables.

fn encode_phi_l(&self, solver: &SMTSolver) -> SMTExpr

Encodes the ϕ_L of the step context

fn encode_phi_gamma(&self, solver: &SMTSolver) -> SMTExpr

Encodes the ϕ_Γ of the step context

fn encode_phi_r(&self, solver: &SMTSolver) -> SMTExpr

Encodes the ϕ_R of the step context

fn exponential_encode_phi_appl(&self, solver: &SMTSolver) -> SMTExpr

(Exponential) Encode ϕ_{appl}

This function encodes an exponential version of the formula ϕ_{appl}, which includes all possibilities to fire a rule.

Compared to the version described in the main section of the paper, we statically filter the set S, to only include chains where for all i it holds that r_i.to = r_{i+1}.from and r_s = r therefore reducing the size of the set S and eliminating the need to encode ∧{1 < i ≤ s} r{i-1}.to = r_i.from ∧ r_s = r into the formula.

Note that we can therefore still have an exponentially big formula. To avoid this, non-deterministic guessing would need to be implemented.

fn encode_phi_chain(&self, solver: &SMTSolver, s: &[&Rule]) -> SMTExpr

Encode ϕ_chain for a single non-deterministic guess

This function encodes the ϕ_{chain} for set of rules s However, this function only encodes ∧_{r ∈ s} x_r > 0 ∧ σ.k(r_1.from) > 0 as all other constraints can be statically checked during the computation of S

Note: This function expects the sequence of rules to be reversed !

fn compute_s_for_r<'a>(&'a self, r: &'a Rule) -> Vec<Vec<&'a Rule>>

Compute all sets possible values of S for rule r

This function computes all possible sets S for all rules r, where S is the set of rules that can lead up to r. Additionally, this function ensures that these sets are chainable, meaning they satisfy the formula: ∧{1< i ≤ s} r{i-1}.to = r_i.from ∧ r_s = r

This function uses the helper compute_s_with_backtracking_recursive, to directly compute only chainable rule sequences.

Note: This function returns the sequences to apply in reversed order!. You can use .rev() to iterate in reversed order.

fn compute_s_with_backtracking_recursive<'a>( &'a self, loc: &'a Location, rules_applied: Vec<&'a Rule>, ) -> Vec<Vec<&'a Rule>>

Recursive helper function that returns a vector that contains:

• the current sequence of chainable rules
• the current sequence of rules extended with the incoming rules into loc
• the chainable extensions for these rule sequences

Note: Chains will be returned in reverse order !

pub fn encode_phi_steady(&self, solver: &SMTSolver) -> SMTExpr

Encode ϕ_{steady}

fn encode_appl_for_step_step(&self, solver: &SMTSolver) -> SMTExpr

Encode reduced version of ϕ_{appl}

That only requires that σ.k(r.source) > 0 for every self-loop if x_r > 0 For other rules, correctness is ensured by the encoding of ϕ_Γ

pub fn encode_phi_step(&self, solver: &SMTSolver) -> SMTExpr

Encode ϕ_{step}

Encodes the ϕ_{step} of the step context

Implementation

The paper does not (fully) specify the encoding of ϕ_{step}.

We decided to use the following formula:

• Introduce a new set of rule variables x_r’ for each rule r.
• Since we only want one rule to be applied when executing a step, we require that the sum of the rule variables is equal to 1, i.e.: ∑_{r ∈ R} x_r’ ≤ 1
• Then we can encode the validity of the rule application by simply using ϕ_R, ϕ_Γ and ϕ_L, with the new variables
• Important: Instead of using ϕ_{appl} with ϕ_{chain}, we use the encoding provided by encode_appl_for_step_step, which is specifically designed for step contexts and ensures the correct application of rules in this setting.

fn update_vec_to_smt(upd: &UpdateExpression, solver: &SMTSolver) -> SMTExpr

Encode the effect of an UpdateExpression into an SMT expression

This function encodes the effect of the update upd to a variable into an SMT expression.

Trait Implementations

impl<TA, C> Clone for LazyStepContext<TA, C>

where TA: ThresholdAutomaton + Clone, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable> + Clone,

fn clone(&self) -> LazyStepContext<TA, C>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<TA, C> Debug for LazyStepContext<TA, C>

where TA: ThresholdAutomaton + Debug, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable> + Debug,

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

Formats the value using the given formatter.

impl<TA, C> Display for LazyStepContext<TA, C>

where TA: ThresholdAutomaton, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,

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

Formats the value using the given formatter.

impl<TA, C> SMTVariableContext<Rule> for LazyStepContext<TA, C>

where TA: ThresholdAutomaton, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,

fn get_expr_for(&self, expr: &Rule) -> Result<SMTExpr, SMTSolverError>

Get the corresponding SMTExpr for the given expression of type T

fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a Rule>

where Rule: 'a,

Get all expressions for which the current context holds an assignment

fn get_solution<'a>( &'a self, solver: &mut SMTSolver, res: SMTSolution, ) -> Result<HashMap<Rule, u32>, SMTSolverError>

where Rule: 'a + Eq + Hash + Clone,

Get the solution assignment

impl<TA, C> StepSMT for LazyStepContext<TA, C>

where TA: ThresholdAutomaton, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,

fn get_rules_applied( &self, solver: &mut SMTSolver, res: SMTSolution, ) -> Result<impl Iterator<Item = (Rule, u32)>, SMTSolverError>

Returns the number of times a rule has been applied in the solution to this context