Struct SMTEncoderSteady 

pub struct SMTEncoderSteady<'a> {
    ta: &'a IntervalThresholdAutomaton,
    rule_counter_to_smt: Vec<(Rule, SMTExpr)>,
    ctx: IndexedSMTContext,
    steady_error_path: &'a SteadyErrorPath<'a>,
}

Type representing an SMT Encoder which is used to encode a steady error path and checking it for spuriousness.

Fields

ta: &'a IntervalThresholdAutomaton

underlying Threshold Automaton

rule_counter_to_smt: Vec<(Rule, SMTExpr)>

vector of smt variables for each rule counter (counts how often this rule is applied)

ctx: IndexedSMTContext

indexed parameter context which stores the smt solver and manages all smt variables

steady_error_path: &'a SteadyErrorPath<'a>

underlying steady error path

Implementations

impl<'a> SMTEncoderSteady<'a>

pub fn new( smt: SMTSolverBuilder, aut: &'a IntervalThresholdAutomaton, steady_error_path: &'a SteadyErrorPath<'a>, ) -> Self

Creates a new SMTEncoder for a given smt solver smt, a given threshold automaton aut and a steady_error_path that is checked for spuriousness. It automatically adds assertions for the resilience condition and the initial location and variable constraints to the smt solver.

fn initialize_rule_counters<'b, I>(&mut self, rules_it: I)

where I: Iterator<Item = &'b Rule>,

creates and stores an smt variable for every Rule rule with its index in the iterator which counts how often rule is applied

fn encode_resilience_conditions<'b, I>(&mut self, rc: I) -> SMTExpr

where I: Iterator<Item = &'b BooleanExpression<Parameter>>,

encodes and returns the resilience condition as an smt constraint

fn encode_loc_conditions<'b, I>(&mut self, cond: I) -> SMTExpr

where I: Iterator<Item = &'b BooleanExpression<Location>>,

encodes and stores the initial location conditions into an smt constraint

fn encode_var_conditions<'b, I>(&mut self, cond: I) -> SMTExpr

where I: Iterator<Item = &'b BooleanExpression<Variable>>,

encodes and stores the initial shared variable conditions into an smt constraint

pub fn steady_is_non_spurious( &mut self, spec: Option<&DisjunctionTargetConfig>, ) -> SpuriousResult

checks if the steady error path is non-spurious

returns additionally Some(path) if a non-spurious error state is reached

if the last state of the steady error path is an error state, the specification needs to be provided to ensure that the corresponding concrete state is also an error state

1. each indexed location, parameter, rule counter is non-negative
2. encode steady error path
3. encode that each steady path fragment is valid
4. encode error states if the last state of the steady error path is an error state
5. run smt solver

pub fn encode_step_transition( &self, from_index: u32, rule_index: u32, ) -> SMTExpr

encodes that the step transition is valid

by checking that the configuration after the steady path \sigma_i leads to the configuration of the next steady path \sigma_{i+1} by applying the transition r exactly once

fn encode_update_shared_var( &self, shared_smt: &SMTExpr, next_shared_smt: &SMTExpr, rule_smt: SMTExpr, update: &UpdateExpression, ) -> SMTExpr

encodes that shared variable ‘x_i’ is updated according to the update or reset of rule r_i = (from, to, uv, τ, ϕ) where c_i counts the number of times r_i is applied

Encoding:

• uv(x) != 0 => σ_{i+1}.g(x) = σ_i.g(x) + c_i * uv(x)
• x ∈ τ => σ_{i+1}.g(x) = 0
• uv(x) = 0 ∧ x ∉ τ => σ_{i+1}.g(x) = σ_i.g(x)

fn encode_steady_error_path(&mut self) -> SMTExpr

encodes the interval constraints for an steady path

i.e., it is checked if for each step, the shared variables are in the respective interval

fn encode_shared_interval<S>(&self, shared: S, interval: Interval) -> SMTExpr

where S: IntoNoDivBooleanExpr<Variable> + Clone,

encodes that the value of an indexed shared variable ‘x_i’ is in the given interval, e.g., if ‘x_i ∈ [t1,t2)’ then: x_i ≥ t1 ∧ x_i < t2

fn encode_error_states(&self, spec: &DisjunctionTargetConfig) -> SMTExpr

encodes the set of error states for the last configuration in the path

This function works for any disjunction of Coverability, General Coverability and Reachability Specifications, For every other specification, smt.false is returned

fn encode_steady_path( &self, from_index: u32, rule_index: u32, steady_path: &SteadyPath, ) -> SMTExpr

encodes that the steady path with rules R = {r_0,…,r_k} is valid from = σ_{from_index} is the configuration at the beginning of the steady path to = σ’_{from_index+1} is the configuration at the end of the steady path

rule_index indicates the first rule of the steady path in the rule_counter_to_smt vector

1. Processes move according to the steady path
2. Update shared variables ‘x_0,…,x_n’ according to the updates (resets or decrements are not allowed)
3. Make sure that for every rule in the steady path there is a fireable chain
4. If the error paths contains increments and decrements, ensure that monotonicity is preserved

fn encode_steady_path_move_processes( &self, from_index: u32, rule_index: u32, steady_path: &SteadyPath, ) -> SMTExpr

encodes that the processes in the ‘steady path’ with rules R = {r_0,…,r_k} move accordingly from = σ_{from_index} is the configuration starting at the steady path to = σ’_{from_index+1} is the configuration ending at the steady path

rule_index indicates the first rule of the steady path in the rule_counter_to_smt vector

encoding: ∀{l_j ∈ L} σ’.k[l_j] = σ.k[l_j] + ∑{r_i ∈ R with r_i.to = l_j} c_i - ∑_{r_i ∈ R with r_i.from = l_j} c_i

fn encode_steady_path_update_shared_variables( &self, from_index: u32, rule_index: u32, steady_path: &SteadyPath, ) -> SMTExpr

encodes that the shared variables in the steady path with rules R = {r_0,…,r_k} are updated accordingly from = σ_{from_index} is the configuration at the beginning of the steady path to = σ’_{from_index+1} is the configuration at the end of the steady path

rule_index indicates the first rule of the steady path in the rule_counter_to_smt vector

returns an error if the steady path contains a reset or decrement update

encoding: ∀ x: σ’.g[x] = σ.g[x] + ∑_{r_i ∈ R} c_i * uv_i[x] if x is not reset ∀ x: σ’.g[x] = 0 if x is reset

fn encode_steady_path_fireable_chain( &self, from_index: u32, rule_index: u32, steady_path: &SteadyPath, ) -> SMTExpr

encodes that all the rules in the steady path with rules R = {r_0,…,r_k} lead to a fireable chain from = σ_{from_index} is the configuration at the beginning of steady path

rule_index indicates the first rule of the steady path in the rule_counter_to_smt vector

Compared to the version described in the main section of the paper, we statically filter the set S, to only include chains from R where for all i it holds that r_i.to = r_{i+1}.from and r_s = r TODO add more tests

fn encode_monotonicity_constraints( &self, rule_index: u32, steady_path: &SteadyPath, ) -> SMTExpr

encodes that the rules applied in the steady path with rules R = {r_0,…,r_k} guarantee mononotonicity for the guards

i.e., it ensures that no rule r_i which decrements a shared variable x is applied when a rule r_j which increments x is applied as well and vice versa

rule_index indicates the first rule of the steady path in the rule_counter_to_smt vector

encoding: ∀{x ∈ Γ} (∑{r_i ∈ R with uv_i[x] > 0} c_i = 0) ∨ (∑_{r_i ∈ R with uv_i[x] < 0} c_i = 0) TODO: add more tests

fn encode_phi_chain_for_steady_path( &self, from_index: u32, s: &[(&Rule, &SMTExpr)], ) -> SMTExpr

Encode ϕ_chain for a single non-deterministic guess for steady paths

from_index indicates the index of the configuration at the beginning of the steady path

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 TODO: add more tests

fn compute_s_for_r_for_steady_path( &'a self, vector_rules: &'a Vec<(&'a Rule, &'a SMTExpr)>, r: &'a Rule, rule_smt: &'a SMTExpr, ) -> Vec<Vec<(&'a Rule, &'a SMTExpr)>>

Compute all sets possible values of S for rule r and ‘steady path’ with rules R = {r_0,…,r_k}

This function computes all possible sets S for all rules r, where S is the set of rules from R 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_for_steady_path, 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. TODO: add more tests

fn compute_s_with_backtracking_recursive_for_steady_path( loc: &'a Location, vector_rules: &[(&'a Rule, &'a SMTExpr)], rules_applied: Vec<(&'a Rule, &'a SMTExpr)>, ) -> Vec<Vec<(&'a Rule, &'a SMTExpr)>>

Recursive helper function that extends the 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 ! TODO: add more tests

fn extract_non_spurious_concrete_path( &mut self, res: SMTSolution, ) -> Result<Path, SMTEncoderError>

extract a non-spurious counterexample trace reaching an error state from the smt solver

fn extract_step_path( &mut self, res: SMTSolution, configurations: &[Configuration], config_index: u32, rule_index: u32, ) -> Result<(Configuration, Transition), SMTEncoderError>

extracts the concrete step between two steady transitions

fn extract_steady_path( &mut self, res: SMTSolution, steady_path: &SteadyPath, configurations: &[Configuration], last_config: Configuration, config_index: u32, rule_index: u32, ) -> Result<(Vec<Transition>, Vec<Configuration>), SMTEncoderError>

extracts the concrete path from a steady path

fn extract_transition_and_updated_config( config: Configuration, rule: Rule, n: u32, ) -> (Transition, Configuration)

Create the transition that applies rule rule n times and compute the resulting configuration

fn get_rule_counter_assignment( &mut self, res: SMTSolution, expr: &SMTExpr, ) -> Result<Option<u64>, SMTSolverError>

returns a satisying assignment for a given rule counter given as SMTExpr