taco_smt_encoder/expression_encoding/
ctx_mgr.rs

1//! Manager for configurations that build a path
2
3use std::{cmp::min, collections::HashMap, rc::Rc};
4
5use log::debug;
6use taco_display_utils::join_iterator;
7use taco_threshold_automaton::{
8    RuleDefinition,
9    expressions::Parameter,
10    general_threshold_automaton::{GeneralThresholdAutomaton, Rule},
11    path::{Configuration, InitializedPathBuilder, Path, PathBuilder, Transition},
12};
13
14use crate::{
15    SMTExpr, SMTSolution, SMTSolver,
16    expression_encoding::{SMTVariableContext, config_ctx::ConfigFromSMT, step_ctx::StepSMT},
17};
18
19/// Manager of configurations for a threshold automaton
20pub struct SMTConfigMgr<CR, CC>
21where
22    CR: StepSMT,
23    CC: ConfigFromSMT,
24{
25    params: Rc<HashMap<Parameter, SMTExpr>>,
26    configs: Vec<Rc<CC>>,
27    configs_primed: Vec<Rc<CC>>,
28    step_steps: Vec<CR>,
29    steady_steps: Vec<CR>,
30}
31
32impl<CR, CC> SMTConfigMgr<CR, CC>
33where
34    CR: StepSMT,
35    CC: ConfigFromSMT,
36{
37    /// Create a new manager
38    pub fn new(params: Rc<HashMap<Parameter, SMTExpr>>) -> Self {
39        Self {
40            params,
41            configs: Vec::new(),
42            configs_primed: Vec::new(),
43            step_steps: Vec::new(),
44            steady_steps: Vec::new(),
45        }
46    }
47
48    /// Get a reference to the parameter variables
49    pub fn params(&self) -> &Rc<HashMap<Parameter, SMTExpr>> {
50        &self.params
51    }
52
53    /// Push a new steady configuration
54    pub fn push_steady(&mut self, step_ctx: CR) {
55        self.steady_steps.push(step_ctx);
56    }
57
58    /// Pop the last steady configuration
59    pub fn pop_steady(&mut self) {
60        self.steady_steps.pop();
61    }
62
63    /// Iterate over all steady steps
64    pub fn steady(&self) -> impl Iterator<Item = &CR> {
65        self.steady_steps.iter()
66    }
67
68    /// Push a new step
69    pub fn push_step(&mut self, step_ctx: CR) {
70        self.step_steps.push(step_ctx);
71    }
72
73    /// Pop a step
74    pub fn pop_step(&mut self) {
75        self.step_steps.pop();
76    }
77
78    /// Iterate over all steps
79    pub fn step(&self) -> impl Iterator<Item = &CR> {
80        self.step_steps.iter()
81    }
82
83    /// Push a new configuration
84    pub fn push_cfg(&mut self, cfg_ctx: Rc<CC>) {
85        self.configs.push(cfg_ctx);
86    }
87
88    /// Pop a configuration
89    pub fn pop_cfg(&mut self) {
90        self.configs.pop();
91    }
92
93    /// Iterate over all configurations
94    pub fn configs(&self) -> impl Iterator<Item = &Rc<CC>> {
95        self.configs.iter()
96    }
97
98    /// Iterate over all primed configurations
99    pub fn configs_primed(&self) -> impl Iterator<Item = &Rc<CC>> {
100        self.configs_primed.iter()
101    }
102
103    /// Push a new primed config
104    pub fn push_cfg_primed(&mut self, cfg_ctx: Rc<CC>) {
105        self.configs_primed.push(cfg_ctx);
106    }
107
108    /// Pop a primed config
109    pub fn pop_cfg_primed(&mut self) {
110        self.configs_primed.pop();
111    }
112
113    /// Extract the error path of the computed solution
114    pub fn extract_error_path(
115        &self,
116        res: SMTSolution,
117        solver: &mut SMTSolver,
118        ta: GeneralThresholdAutomaton,
119    ) -> Path {
120        let builder = PathBuilder::new(ta);
121
122        let param_assignment = self
123            .params
124            .get_solution(solver, res)
125            .expect("Failed to extract parameter assignment for error path");
126        let mut builder = builder
127            .add_parameter_assignment(param_assignment)
128            .expect("Parameter assignment returned by SMT solver invalid");
129
130        for (i, ((config, config_primed), steady_step)) in self
131            .configs
132            .iter()
133            .zip(self.configs_primed.iter())
134            .zip(self.steady_steps.iter())
135            .enumerate()
136        {
137            let config = config
138                .get_assigned_configuration(solver, res)
139                .expect("Failed to extract assigned configuration of config");
140
141            builder = builder
142                .add_configuration(config.clone())
143                .expect("Configuration config extracted from SMT solver is invalid");
144
145            builder = Self::add_transitions_steady_step_to_builder(
146                builder,
147                config,
148                steady_step,
149                solver,
150                res,
151            );
152
153            let primed_config = config_primed
154                .get_assigned_configuration(solver, res)
155                .expect("Failed to extract assigned configuration of primed_config");
156
157            builder = builder
158                .add_configuration(primed_config)
159                .expect("Configuration primed_config extracted from SMT solver is invalid");
160
161            // Extract rules from current step step
162            if i < self.step_steps.len() {
163                builder = Self::add_transition_step_step_to_builder(
164                    builder,
165                    &self.step_steps[i],
166                    solver,
167                    res,
168                );
169            }
170        }
171
172        builder.build().expect("Extracted path is invalid!")
173    }
174
175    /// Compute the transition defined by a steady step and add them to the error
176    /// path
177    fn add_transitions_steady_step_to_builder(
178        mut builder: InitializedPathBuilder,
179        config: Configuration,
180        steady_step: &CR,
181        solver: &mut SMTSolver,
182        res: SMTSolution,
183    ) -> InitializedPathBuilder {
184        let mut rules = steady_step
185            .get_rules_applied(solver, res)
186            .expect("Failed to extract rules used")
187            .filter(|(_, n)| *n > 0)
188            .collect::<Vec<_>>();
189
190        let mut curr_config = config.clone();
191
192        let old_rules = rules.clone();
193        let old_config = config;
194
195        // Try to order rules such that they are chainable
196        while !rules.is_empty() {
197            let mut n_apply = 0;
198
199            // Add enabled self-loops first
200            for (rule, n_to_apply) in rules.iter_mut().filter(|(r, _)| r.source() == r.target()) {
201                if curr_config.get_processes_in_location(rule.source()) > 0 {
202                    // if the transition is a self-loop apply it n_to_apply times
203                    n_apply = *n_to_apply;
204                    *n_to_apply = 0;
205
206                    (builder, curr_config) =
207                        Self::add_transition_to_builder_and_return_updated_config(
208                            builder,
209                            curr_config,
210                            rule.clone(),
211                            n_apply,
212                        );
213                }
214            }
215
216            for (rule, n_to_apply) in rules.iter_mut().filter(|(_, n)| *n > 0) {
217                // Check if rule can be applied
218                if curr_config.get_processes_in_location(rule.source()) > 0 {
219                    // compute the number of times it can be applied
220                    n_apply = min(
221                        curr_config.get_processes_in_location(rule.source()),
222                        *n_to_apply,
223                    );
224
225                    *n_to_apply -= n_apply;
226
227                    (builder, curr_config) =
228                        Self::add_transition_to_builder_and_return_updated_config(
229                            builder,
230                            curr_config,
231                            rule.clone(),
232                            n_apply,
233                        );
234
235                    // check if there are new self loops enabled after updating
236                    // the configuration
237                    break;
238                }
239            }
240
241            assert!(
242                n_apply > 0,
243                "Failed to order rules into chainable order! Configuration that rules must be applied on:\n{}\n\nRules left to apply:\n{}\n\nSet of rules to be ordered in this steady step:\n{}\n\nInitial configuration of the steady step:\n{}\n\n ",
244                curr_config,
245                join_iterator(rules.iter().map(|(r, i)| format!("{i} x {r}")), ",\n"),
246                join_iterator(old_rules.iter().map(|(r, i)| format!("{i} x {r}")), ",\n"),
247                old_config,
248            );
249
250            rules.retain(|(_, n)| *n > 0);
251        }
252
253        builder
254    }
255
256    /// Create the transition that applies rule `rule` `n` times, compute the
257    /// resulting configuration and add it to the path builder.
258    /// Returns the computed configuration and updated builder.
259    fn add_transition_to_builder_and_return_updated_config(
260        mut builder: InitializedPathBuilder,
261        config: Configuration,
262        rule: Rule,
263        n: u32,
264    ) -> (InitializedPathBuilder, Configuration) {
265        let transition = Transition::new(rule, n);
266        let curr_config = config
267            .apply_rule(&transition)
268            .expect("Constructed transition invalid!");
269
270        builder = builder
271            .add_transition(transition)
272            .expect("Failed to add transition to builder");
273        builder = builder
274            .add_configuration(curr_config.clone())
275            .expect("Failed to add configuration computed in steady step");
276
277        (builder, curr_config)
278    }
279
280    /// Compute the transition defined by a step step and add them to the error
281    /// path
282    fn add_transition_step_step_to_builder(
283        builder: InitializedPathBuilder,
284        step_step: &CR,
285        solver: &mut SMTSolver,
286        res: SMTSolution,
287    ) -> InitializedPathBuilder {
288        let mut rules_it = step_step
289            .get_rules_applied(solver, res)
290            .expect("Failed to extract rules applied");
291        let applied_rule = rules_it.next();
292
293        if applied_rule.is_none() {
294            // skip this configuration since we might have already
295            // reached an error
296            debug!("Found an empty step step. Skipping!");
297            return builder;
298        }
299        let (applied_rule, n) = applied_rule.unwrap();
300
301        debug_assert!(
302            rules_it.next().is_none(),
303            "Expected only one rule to be applied in step step!"
304        );
305
306        debug_assert!(
307            n == 1,
308            "Expected rule in step step to be applied only once !"
309        );
310
311        let transition = Transition::new(applied_rule, 1);
312
313        builder
314            .add_transition(transition)
315            .expect("Failed to add transition of step step to builder")
316    }
317}
taco_smt_encoder/expression_encoding/ctx_mgr.rs

taco_smt_encoder/expression_encoding/
ctx_mgr.rs
