taco_zcs_model_checker/
lib.rs

1//! This module contains the different symbolic model checkers (ZCS model checkers)
2//! that operate on threshold automata and the 01-CS (ZCS).
3
4mod paths;
5pub mod smt_encoder_steady;
6pub mod zcs;
7pub mod zcs_error_graph;
8
9use taco_interval_ta::IntervalThresholdAutomaton;
10
11use log::info;
12
13use taco_model_checker::ModelCheckerContext;
14use taco_model_checker::reachability_specification::{
15    DisjunctionTargetConfig, ReachabilityProperty, TargetConfig,
16};
17use taco_threshold_automaton::lia_threshold_automaton::LIAVariableConstraint;
18
19use std::fmt::Display;
20use taco_model_checker::{ModelChecker, ModelCheckerResult, SMTBddContext};
21use taco_threshold_automaton::ThresholdAutomaton;
22use zcs::ZCS;
23use zcs::ZCSStates;
24use zcs::builder::ZCSBuilder;
25use zcs_error_graph::ZCSErrorGraph;
26use zcs_error_graph::builder::ZCSErrorGraphBuilder;
27
28/// This struct defines a symbolic model checker (ZCS model checker)
29/// It can be used to check reachability and coverability specifications
30/// Depending on the chosen search heuristics:
31/// - it can verify extended threshold automata with a semi-decision procedure
32/// - it can verify canonical threshold automata with a decision procedure
33#[derive(Debug, Clone)]
34pub struct ZCSModelChecker {
35    /// model checker context
36    ctx: SMTBddContext,
37    /// specifications to be checked
38    ta_spec: Vec<(DisjunctionTargetConfig, Vec<IntervalThresholdAutomaton>)>,
39    /// symbolic model checker heuristics
40    heuristics: ZCSModelCheckerHeuristics,
41}
42
43impl ZCSModelChecker {
44    /// constructs the symbolic 01-CS (ZCS) and initializes the bdd var manager
45    fn compute_zcs<'a>(&'a self, ta: &'a IntervalThresholdAutomaton) -> ZCS<'a> {
46        ZCSBuilder::new(self.ctx.bdd_manager(), ta).build()
47    }
48
49    /// construct the symbolic shared variable state that satisfies the interval
50    /// constraint of a target configuration
51    fn compute_enabled_shared_variable_states(
52        cs: &ZCS,
53        ta: &IntervalThresholdAutomaton,
54        target_config: &TargetConfig,
55    ) -> ZCSStates {
56        let var_constr = target_config.get_variable_constraint();
57        let interval_constr = ta
58            .get_interval_constraint(var_constr)
59            .expect("Failed to get target interval_constr");
60
61        ta.get_variables_constrained(&interval_constr)
62            .into_iter()
63            .map(|var| {
64                // union over all intervals allowed for a variable
65                ta.get_enabled_intervals(&interval_constr, var)
66                    .map(|interval| cs.get_sym_state_for_shared_interval(var, interval))
67                    .fold(cs.new_empty_sym_state(), |acc, x| acc.union(&x))
68            })
69            .fold(cs.new_full_sym_state(), |acc, x| acc.intersection(&x))
70    }
71
72    /// constructs the set of error states for a given spec and 01-CS (ZCS)
73    fn compute_error_states(
74        cs: &ZCS,
75        ta: &IntervalThresholdAutomaton,
76        specification: &DisjunctionTargetConfig,
77    ) -> Result<ZCSStates, ZCSModelCheckerError> {
78        let mut error_states = cs.new_empty_sym_state();
79
80        for target_config in specification.get_target_configs() {
81            let mut err_state = cs.new_full_sym_state();
82
83            for (loc, _) in target_config.get_locations_to_cover() {
84                err_state = err_state.intersection(&cs.get_sym_state_for_loc(loc));
85            }
86
87            for uncov in target_config.get_locations_to_uncover() {
88                err_state = err_state.intersection(&cs.get_sym_state_for_loc(uncov).complement());
89            }
90
91            // Variable constraints
92            if target_config.get_variable_constraint() != &LIAVariableConstraint::True {
93                let interval_err_state =
94                    Self::compute_enabled_shared_variable_states(cs, ta, target_config);
95                err_state = err_state.intersection(&interval_err_state);
96            }
97
98            error_states = error_states.union(&err_state);
99        }
100
101        Ok(error_states)
102    }
103
104    /// constructs the symbolic error graph (ZCS error graph) for the underlying 01-CS (ZCS)
105    fn compute_symbolic_error_graph<'a>(
106        &'a self,
107        ta: &'a IntervalThresholdAutomaton,
108        spec: &DisjunctionTargetConfig,
109    ) -> ZCSErrorGraph<'a> {
110        let cs = self.compute_zcs(ta);
111
112        let error_states = Self::compute_error_states(&cs, ta, spec)
113            .expect("The specification {} is not supported by the symbolic model checker");
114
115        ZCSErrorGraphBuilder::new(cs.clone(), error_states).build()
116    }
117}
118
119impl ModelChecker for ZCSModelChecker {
120    type ModelCheckerContext = SMTBddContext;
121
122    type ModelCheckerOptions = Option<ZCSModelCheckerHeuristics>;
123
124    type SpecType = ReachabilityProperty;
125
126    type ThresholdAutomatonType = IntervalThresholdAutomaton;
127
128    type InitializationError = ZCSModelCheckerInitializationError;
129
130    type ModelCheckingError = ZCSModelCheckerError;
131
132    fn initialize(
133        opts: Self::ModelCheckerOptions,
134        ta_spec: Vec<(DisjunctionTargetConfig, Vec<Self::ThresholdAutomatonType>)>,
135        ctx: Self::ModelCheckerContext,
136    ) -> Result<Self, Self::InitializationError> {
137        let heuristics;
138
139        match opts.clone() {
140            // No heuristics provided, use heuristics based on the given threshold automata
141            None => {
142                if ta_spec
143                    .iter()
144                    .any(|(_, tas)| tas.iter().any(|ta| ta.has_decrements_or_resets()))
145                {
146                    if ta_spec
147                        .iter()
148                        .any(|(_, tas)| tas.iter().any(|ta| ta.has_decrements()))
149                    {
150                        heuristics = ZCSModelCheckerHeuristics::DecrementAndIncrementHeuristics;
151                    } else {
152                        heuristics = ZCSModelCheckerHeuristics::ResetHeuristics;
153                    }
154                } else {
155                    heuristics = ZCSModelCheckerHeuristics::CanonicalHeuristics;
156                }
157            }
158            Some(h) => {
159                heuristics = h;
160            }
161        }
162
163        if opts == Some(ZCSModelCheckerHeuristics::CanonicalHeuristics)
164            && ta_spec
165                .iter()
166                .any(|(_, tas)| tas.iter().any(|ta| ta.has_decrements_or_resets()))
167        {
168            return Err(ZCSModelCheckerInitializationError::HeuristicsNotSuitable(
169                "Canonical heuristics".to_string(),
170            ));
171        }
172
173        Ok(Self {
174            ctx,
175            ta_spec,
176            heuristics,
177        })
178    }
179
180    fn verify(
181        self,
182        abort_on_violation: bool,
183    ) -> Result<ModelCheckerResult, Self::ModelCheckingError> {
184        let mut unsafe_prop = Vec::new();
185        let mut unknown_prop = Vec::new();
186
187        for (target, tas_to_check) in self.ta_spec.iter() {
188            info!(
189                "Starting to check property '{}', which requires {} model checker run(s).",
190                target.name(),
191                tas_to_check.len()
192            );
193            for ta in tas_to_check.iter() {
194                let error_graph = self.compute_symbolic_error_graph(ta, target);
195                if !error_graph.is_empty() {
196                    if self.heuristics == ZCSModelCheckerHeuristics::EmptyErrorGraphHeuristics {
197                        info!(
198                            "The error graph is not empty, but the chosen heuristics only checks for emptiness. Therefore, it is unknown whether the property holds."
199                        );
200                        unknown_prop.push(target.name().to_string());
201                        continue;
202                    }
203                    info!("The error graph is not empty, checking for non-spurious error paths.");
204                    let res =
205                        error_graph.contains_non_spurious_error_path(&ZCSModelCheckerContext::new(
206                            &self.ctx,
207                            self.heuristics.clone(),
208                            ta,
209                            target,
210                        ));
211
212                    if let Some(p) = res.non_spurious_path() {
213                        info!("Property {} is not satisfied!", target.name());
214
215                        unsafe_prop.push((target.name().to_string(), Box::new(p.clone())));
216
217                        if abort_on_violation {
218                            return Ok(ModelCheckerResult::UNSAFE(unsafe_prop));
219                        }
220
221                        break;
222                    }
223
224                    info!("All error paths are spurious.");
225                } else {
226                    info!("The error graph is empty.");
227                }
228            }
229        }
230
231        if !unsafe_prop.is_empty() {
232            return Ok(ModelCheckerResult::UNSAFE(unsafe_prop));
233        }
234
235        if self.heuristics == ZCSModelCheckerHeuristics::EmptyErrorGraphHeuristics {
236            if unknown_prop.is_empty() {
237                return Ok(ModelCheckerResult::SAFE);
238            } else {
239                return Ok(ModelCheckerResult::UNKNOWN(unknown_prop));
240            }
241        }
242
243        Ok(ModelCheckerResult::SAFE)
244    }
245}
246
247impl Default for ZCSModelChecker {
248    fn default() -> Self {
249        Self::new_mc(SMTBddContext::try_new(None).expect("Failed to create SMTBddContext"))
250    }
251}
252
253impl ZCSModelChecker {
254    /// new symbolic model checker with default settings
255    pub fn new_mc(ctx: SMTBddContext) -> Self {
256        Self {
257            ctx,
258            ta_spec: Vec::new(),
259            heuristics: ZCSModelCheckerHeuristics::CanonicalHeuristics,
260        }
261    }
262}
263
264/// Custom Error type to indicate an error
265/// when running a symbolic model checker (ZCS model checker)
266#[derive(Debug)]
267pub enum ZCSModelCheckerError {
268    /// Error indicating that the current specification is not supported by the current symbolic model checker
269    SpecNotSupported(String),
270}
271
272impl std::error::Error for ZCSModelCheckerError {}
273
274impl Display for ZCSModelCheckerError {
275    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
276        match self {
277            ZCSModelCheckerError::SpecNotSupported(spec) => write!(
278                f,
279                "This initialized symbolic model checker does not support the specification {spec}"
280            ),
281        }
282    }
283}
284
285/// Custom Error type to indicate an error
286/// when initializing a symbolic model checker (ZCS model checker)
287#[derive(Debug)]
288pub enum ZCSModelCheckerInitializationError {
289    /// Error indicating that the current heuristics does not support the given TA
290    HeuristicsNotSuitable(String),
291}
292
293impl std::error::Error for ZCSModelCheckerInitializationError {}
294
295impl Display for ZCSModelCheckerInitializationError {
296    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
297        match self {
298            ZCSModelCheckerInitializationError::HeuristicsNotSuitable(heur) => write!(
299                f,
300                "The chosen heuristics {heur} is not suitable for the given threshold automaton",
301            ),
302        }
303    }
304}
305
306/// This struct contains all the necessary configurations when using the symbolic model checker (ZCS model checker)
307pub struct ZCSModelCheckerContext<'a> {
308    /// used smt and bdd libraries
309    ctx: &'a SMTBddContext,
310    /// underlying heuristics
311    heuristics: ZCSModelCheckerHeuristics,
312    /// underlying TA
313    ta: &'a IntervalThresholdAutomaton,
314    /// underlying specification
315    spec: &'a DisjunctionTargetConfig,
316    /// indicates if the symbolic model checker should print spurious counterexamples
317    print_spurious_ce: bool,
318}
319impl<'a> ZCSModelCheckerContext<'a> {
320    /// creates a new symbolic model checker context
321    fn new(
322        ctx: &'a SMTBddContext,
323        heuristics: ZCSModelCheckerHeuristics,
324        ta: &'a IntervalThresholdAutomaton,
325        spec: &'a DisjunctionTargetConfig,
326    ) -> Self {
327        ZCSModelCheckerContext {
328            ctx,
329            heuristics,
330            ta,
331            spec,
332            print_spurious_ce: false,
333        }
334    }
335    /// returns the SMTBddContext
336    fn smt_bdd_context(&self) -> &SMTBddContext {
337        self.ctx
338    }
339    /// returns the heuristics
340    fn heuristics(&self) -> ZCSModelCheckerHeuristics {
341        self.heuristics.clone()
342    }
343    /// returns the underlying TA
344    fn ta(&self) -> &IntervalThresholdAutomaton {
345        self.ta
346    }
347    /// returns the underlying specification
348    fn spec(&self) -> &DisjunctionTargetConfig {
349        self.spec
350    }
351    /// returns if spurious counterexamples should be printed
352    fn print_spurious_ce(&self) -> bool {
353        self.print_spurious_ce
354    }
355}
356
357/// this enum defines SymbolicModelChecker Heuristics,
358/// such a heuristics defines which symbolic paths are ignored
359/// and which specifications and threshold automata can be checked
360///
361/// Additionally it describes a greedy heuristics which only checks if the symbolic error graph is empty.
362#[derive(PartialEq, Clone, Debug)]
363pub enum ZCSModelCheckerHeuristics {
364    /// this heuristics yields a semi-decision procedure
365    /// by unfolding cycles if the given `ta` contains resets
366    /// it can be used to verify extended threshold automata
367    /// for coverability or reachability specifications
368    ResetHeuristics,
369    /// this heuristics yields a semi-decision procedure
370    /// by unfolding cycles if the given `ta` contains increments and decrements
371    /// it can be used to verify extended threshold automata
372    /// for coverability or reachability specifications
373    DecrementAndIncrementHeuristics,
374    /// this heuristics yields a decision procedure
375    /// by only traversing cycles once
376    /// it can be used to verify canonical threshold automata (no resets/decrements)
377    /// for coverability or reachability specifications
378    CanonicalHeuristics,
379    /// this is a greedy heuristics that only checks if the symbolic error graph is empty
380    /// it is neither complete nor sound but guarantees termination
381    /// if the error graph is empty the property holds, otherwise no conclusion can be drawn
382    EmptyErrorGraphHeuristics,
383}
384impl ZCSModelCheckerHeuristics {
385    /// returns a new ResetHeuristics
386    pub fn new_reset_heuristics() -> Self {
387        ZCSModelCheckerHeuristics::ResetHeuristics
388    }
389    /// returns a new DecrementsAndIncrementHeuristics
390    pub fn new_decrement_and_increment_heuristics() -> Self {
391        ZCSModelCheckerHeuristics::DecrementAndIncrementHeuristics
392    }
393    /// returns a new CanonicalHeuristics
394    pub fn new_canonical_heuristics() -> Self {
395        ZCSModelCheckerHeuristics::CanonicalHeuristics
396    }
397    /// returns a new CanonicalHeuristics
398    pub fn new_empty_error_graph_heuristics() -> Self {
399        ZCSModelCheckerHeuristics::EmptyErrorGraphHeuristics
400    }
401    /// returns true iff the heuristics ensures that every steady path is monotonic
402    pub fn is_monotonic(&self) -> bool {
403        match self {
404            ZCSModelCheckerHeuristics::ResetHeuristics => true,
405            ZCSModelCheckerHeuristics::DecrementAndIncrementHeuristics => false,
406            ZCSModelCheckerHeuristics::CanonicalHeuristics => true,
407            ZCSModelCheckerHeuristics::EmptyErrorGraphHeuristics => false,
408        }
409    }
410}
411
412#[cfg(test)]
413mod tests {
414    use crate::ZCSModelChecker;
415    use crate::ZCSModelCheckerHeuristics;
416    use std::collections::HashMap;
417    use std::collections::HashSet;
418    use taco_bdd::BDDManagerConfig;
419    use taco_interval_ta::IntervalThresholdAutomaton;
420    use taco_interval_ta::builder::IntervalTABuilder;
421    use taco_interval_ta::interval::Interval;
422    use taco_model_checker::ModelChecker;
423    use taco_model_checker::ModelCheckerContext;
424    use taco_model_checker::ModelCheckerResult;
425    use taco_model_checker::SMTBddContext;
426    use taco_model_checker::reachability_specification::DisjunctionTargetConfig;
427    use taco_model_checker::reachability_specification::TargetConfig;
428    use taco_parser::ParseTAWithLTL;
429    use taco_parser::bymc::ByMCParser;
430    use taco_smt_encoder::SMTSolverBuilder;
431    use taco_smt_encoder::SMTSolverBuilderCfg;
432    use taco_threshold_automaton::ModifiableThresholdAutomaton;
433    use taco_threshold_automaton::expressions::BooleanExpression;
434    use taco_threshold_automaton::expressions::ComparisonOp;
435    use taco_threshold_automaton::expressions::IntegerExpression;
436    use taco_threshold_automaton::expressions::fraction::Fraction;
437    use taco_threshold_automaton::expressions::{Location, Parameter, Variable};
438    use taco_threshold_automaton::general_threshold_automaton::Action;
439    use taco_threshold_automaton::general_threshold_automaton::UpdateExpression;
440    use taco_threshold_automaton::general_threshold_automaton::builder::RuleBuilder;
441
442    use taco_threshold_automaton::BooleanVarConstraint;
443    use taco_threshold_automaton::LocationConstraint;
444    use taco_threshold_automaton::ParameterConstraint;
445    use taco_threshold_automaton::path::Configuration;
446    use taco_threshold_automaton::path::PathBuilder;
447    use taco_threshold_automaton::path::Transition;
448
449    impl ZCSModelChecker {
450        /// Create a new symbolic model checker (ZCS model checker)
451        fn new_test(ctx: SMTBddContext) -> Self {
452            ZCSModelChecker {
453                ctx,
454                ta_spec: Vec::new(),
455                heuristics: ZCSModelCheckerHeuristics::CanonicalHeuristics,
456            }
457        }
458    }
459
460    /// Construct the SymbolicErrorGraph for the following threshold automaton:
461    ///
462    /// Threshold Automaton:
463    /// Locations: {l0,l1,l2}
464    /// Initial location: l0
465    /// Parameter: {n,t}
466    /// Shared Variable: x
467    /// Initial location constraints: l0 = n - t & l1 = 0 & l2 = 0
468    /// Rules:
469    ///     r0: l0 -> l1, guard: true, action: x = x + 1
470    ///     r1: l0 -> l2, guard: x >= n - t, action: none
471    ///     r2: l1 -> l2, guard: x >= n - t, action: none
472    ///
473    /// Abstract Threshold Automaton:
474    /// Intervals for x: I_0 = [0,1), I_1 = [1,n-t), I_2 = [n-t, infty)
475    /// Interval Order: I_0 < I_1 < I_2
476    /// Abstract Rules:
477    ///     r0: l0 -> l1, guard: true, action: x = x + 1
478    ///     r1: l0 -> l1, guard: x = I_2, action: none
479    ///     r2: l1 -> l2, guard: x = I_2, action: none
480    fn get_test_ata() -> IntervalThresholdAutomaton {
481        let ta_builder =
482            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
483                .with_locations(vec![
484                    Location::new("l0"),
485                    Location::new("l1"),
486                    Location::new("l2"),
487                ])
488                .unwrap()
489                .with_variables(vec![Variable::new("x")])
490                .unwrap()
491                .with_parameters(vec![
492                    Parameter::new("n"),
493                    Parameter::new("t"),
494                    Parameter::new("f"),
495                ])
496                .unwrap()
497                .initialize()
498                .with_resilience_conditions(vec![
499                    ParameterConstraint::ComparisonExpression(
500                        Box::new(IntegerExpression::Atom(Parameter::new("n"))),
501                        ComparisonOp::Geq,
502                        Box::new(IntegerExpression::Const(0)),
503                    ),
504                    ParameterConstraint::ComparisonExpression(
505                        Box::new(IntegerExpression::Atom(Parameter::new("t"))),
506                        ComparisonOp::Geq,
507                        Box::new(IntegerExpression::Const(0)),
508                    ),
509                    ParameterConstraint::ComparisonExpression(
510                        Box::new(IntegerExpression::Atom(Parameter::new("f"))),
511                        ComparisonOp::Geq,
512                        Box::new(IntegerExpression::Const(0)),
513                    ),
514                    ParameterConstraint::ComparisonExpression(
515                        Box::new(IntegerExpression::Atom(Parameter::new("n")) - IntegerExpression::Atom(Parameter::new("t"))),
516                        ComparisonOp::Gt,
517                        Box::new(IntegerExpression::Const(1)),
518                    )
519                ]).unwrap()
520                .with_initial_location_constraints(vec![
521                    LocationConstraint::ComparisonExpression(
522                        Box::new(IntegerExpression::Atom(Location::new("l0"))),
523                        ComparisonOp::Eq,
524                        Box::new(
525                            IntegerExpression::Param(Parameter::new("n"))
526                                - IntegerExpression::Param(Parameter::new("t")),
527                        ),
528                    ),
529                    LocationConstraint::ComparisonExpression(
530                        Box::new(IntegerExpression::Atom(Location::new("l1"))),
531                        ComparisonOp::Eq,
532                        Box::new(IntegerExpression::Const(0)),
533                    ),
534                    LocationConstraint::ComparisonExpression(
535                        Box::new(IntegerExpression::Atom(Location::new("l2"))),
536                        ComparisonOp::Eq,
537                        Box::new(IntegerExpression::Const(0)),
538                    ),
539                ])
540                .unwrap()
541                .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
542                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
543                    ComparisonOp::Eq,
544                    Box::new(IntegerExpression::Const(0)),
545                )])
546                .unwrap()
547                .with_rules(vec![
548                    RuleBuilder::new(0, Location::new("l0"), Location::new("l1"))
549                        .with_action(
550                            Action::new(
551                                Variable::new("x"),
552                                IntegerExpression::Atom(Variable::new("x"))
553                                    + IntegerExpression::Const(1),
554                            )
555                            .unwrap(),
556                        )
557                        .build(),
558                    RuleBuilder::new(1, Location::new("l0"), Location::new("l2"))
559                        .with_guard(BooleanVarConstraint::ComparisonExpression(
560                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
561                            ComparisonOp::Geq,
562                            Box::new(
563                                IntegerExpression::Param(Parameter::new("n"))
564                                    - IntegerExpression::Param(Parameter::new("t")),
565                            ),
566                        ))
567                        .build(),
568                    RuleBuilder::new(2, Location::new("l1"), Location::new("l2"))
569                        .with_guard(BooleanVarConstraint::ComparisonExpression(
570                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
571                            ComparisonOp::Geq,
572                            Box::new(
573                                IntegerExpression::Param(Parameter::new("n"))
574                                    - IntegerExpression::Param(Parameter::new("t")),
575                            ),
576                        ))
577                        .build(),
578                ])
579                .unwrap();
580        let ta = ta_builder.build();
581        let lia =
582            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
583                ta.clone(),
584            )
585            .unwrap();
586
587        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
588            .build()
589            .unwrap();
590        let ata = interval_tas.next().unwrap();
591
592        let nxt = interval_tas.next();
593        assert!(nxt.is_none(), "Got additional ta {}", nxt.unwrap());
594        ata
595    }
596
597    #[test]
598    fn test_compute_symbolic_01_cs_no_bdd_mgr() {
599        let ctx = SMTBddContext::try_new(None).unwrap();
600
601        let smc = ZCSModelChecker::new_test(ctx);
602
603        let ata = get_test_ata();
604        let cs = smc.compute_zcs(&ata);
605
606        let initial_states = cs.initial_states();
607
608        let l_1 = cs.get_sym_state_for_loc(&Location::new("l1"));
609        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
610
611        // I_0 = [0,1)
612        let interval_0 =
613            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
614        let x_i_0 = cs.get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0.clone());
615
616        let correct_initial_states = l_1
617            .complement()
618            .intersection(&l_2.complement())
619            .intersection(&x_i_0);
620
621        assert!(initial_states.equal(&correct_initial_states));
622    }
623
624    #[test]
625    fn test_compute_symbolic_01_cs_some_bdd_mgr() {
626        let ctx = SMTBddContext::try_new(None).unwrap();
627
628        let smc = ZCSModelChecker::new_test(ctx);
629
630        let ata = get_test_ata();
631        let cs = smc.compute_zcs(&ata);
632
633        let initial_states = cs.initial_states();
634
635        let l_1 = cs.get_sym_state_for_loc(&Location::new("l1"));
636        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
637
638        // I_0 = [0,1)
639        let interval_0 =
640            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
641        let x_i_0 = cs.get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0.clone());
642
643        let correct_initial_states = l_1
644            .complement()
645            .intersection(&l_2.complement())
646            .intersection(&x_i_0);
647
648        assert!(initial_states.equal(&correct_initial_states));
649    }
650
651    #[test]
652    fn test_compute_error_states_cover() {
653        let ctx = SMTBddContext::try_new(None).unwrap();
654
655        let smc = ZCSModelChecker::new_test(ctx);
656
657        let spec = TargetConfig::new_cover([Location::new("l2")])
658            .unwrap()
659            .into_disjunct_with_name("test");
660
661        let ata = get_test_ata();
662        let cs = smc.compute_zcs(&ata);
663
664        let error_states = ZCSModelChecker::compute_error_states(&cs, &ata, &spec);
665
666        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
667
668        assert!(error_states.is_ok());
669        assert!(error_states.unwrap().equal(&l_2));
670    }
671
672    #[test]
673    fn test_compute_error_states_reachability() {
674        let ctx = SMTBddContext::try_new(None).unwrap();
675
676        let smc = ZCSModelChecker::new_test(ctx);
677
678        let spec = TargetConfig::new_reach(
679            HashSet::from([Location::new("l2")]),
680            HashSet::from([Location::new("l1")]),
681        )
682        .unwrap()
683        .into_disjunct_with_name("test");
684
685        let ata = get_test_ata();
686        let cs = smc.compute_zcs(&ata);
687
688        let error_states = ZCSModelChecker::compute_error_states(&cs, &ata, &spec);
689
690        let l_1 = cs.get_sym_state_for_loc(&Location::new("l1"));
691        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
692
693        assert!(error_states.is_ok());
694        assert!(
695            error_states
696                .unwrap()
697                .equal(&l_2.intersection(&l_1.complement()))
698        );
699    }
700
701    #[test]
702    fn test_compute_error_states_general_cover() {
703        let ctx = SMTBddContext::try_new(None).unwrap();
704
705        let smc = ZCSModelChecker::new_test(ctx);
706
707        let spec = TargetConfig::new_general_cover([(Location::new("l2"), 2)])
708            .unwrap()
709            .into_disjunct_with_name("test");
710
711        let ata = get_test_ata();
712        let cs = smc.compute_zcs(&ata);
713
714        let error_states = ZCSModelChecker::compute_error_states(&cs, &ata, &spec);
715
716        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
717
718        assert!(error_states.is_ok());
719        assert!(error_states.unwrap().equal(&l_2));
720    }
721
722    #[test]
723    fn test_compute_enabled_shared_variable_states() {
724        let ctx = SMTBddContext::try_new(None).unwrap();
725
726        let smc = ZCSModelChecker::new_test(ctx);
727
728        let spec = TargetConfig::new_reach_with_var_constr(
729            [(Location::new("l2"), 2)],
730            [],
731            BooleanExpression::ComparisonExpression(
732                Box::new(IntegerExpression::Atom(Variable::new("x"))),
733                ComparisonOp::Eq,
734                Box::new(IntegerExpression::Const(0)),
735            ),
736        )
737        .unwrap();
738
739        let ata = get_test_ata();
740        let cs = smc.compute_zcs(&ata);
741
742        let error_interval_state =
743            ZCSModelChecker::compute_enabled_shared_variable_states(&cs, &ata, &spec);
744
745        let i_1 = cs
746            .get_sym_state_for_shared_interval(&Variable::new("x"), &Interval::new_constant(0, 1));
747
748        assert!(error_interval_state.equal(&i_1));
749    }
750
751    #[test]
752    fn test_compute_error_states_reach_with_var_constr() {
753        let ctx = SMTBddContext::try_new(None).unwrap();
754
755        let smc = ZCSModelChecker::new_test(ctx);
756
757        let spec = TargetConfig::new_reach_with_var_constr(
758            [(Location::new("l2"), 2)],
759            [],
760            BooleanExpression::ComparisonExpression(
761                Box::new(IntegerExpression::Atom(Variable::new("x"))),
762                ComparisonOp::Eq,
763                Box::new(IntegerExpression::Const(0)),
764            ),
765        )
766        .unwrap()
767        .into_disjunct_with_name("test");
768
769        let ata = get_test_ata();
770        let cs = smc.compute_zcs(&ata);
771
772        let error_states = ZCSModelChecker::compute_error_states(&cs, &ata, &spec);
773
774        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
775        let i_1 = cs
776            .get_sym_state_for_shared_interval(&Variable::new("x"), &Interval::new_constant(0, 1));
777        let expected_err_state = l_2.intersection(&i_1);
778
779        assert!(error_states.is_ok());
780        assert!(error_states.unwrap().equal(&expected_err_state));
781    }
782
783    #[test]
784    fn test_compute_error_states_all_spec_types() {
785        let ctx = SMTBddContext::try_new(None).unwrap();
786
787        let smc = ZCSModelChecker::new_test(ctx);
788
789        let cover = TargetConfig::new_cover([Location::new("l2")]).unwrap();
790
791        let general_cover = TargetConfig::new_general_cover([(Location::new("l2"), 2)]).unwrap();
792
793        let reach = TargetConfig::new_general_reach(
794            HashMap::from([(Location::new("l2"), 2)]),
795            HashSet::new(),
796        )
797        .unwrap();
798
799        let spec = DisjunctionTargetConfig::new_from_targets(
800            "test".to_string(),
801            [cover, general_cover, reach],
802        );
803
804        let ata = get_test_ata();
805        let cs = smc.compute_zcs(&ata);
806
807        let error_states = ZCSModelChecker::compute_error_states(&cs, &ata, &spec);
808
809        let l_2 = cs.get_sym_state_for_loc(&Location::new("l2"));
810
811        assert!(error_states.is_ok());
812        assert!(error_states.unwrap().equal(&l_2));
813    }
814
815    #[test]
816    fn test_compute_symbolic_error_graph() {
817        let ctx = SMTBddContext::try_new(None).unwrap();
818
819        let smc = ZCSModelChecker::new_test(ctx);
820
821        let ata = get_test_ata();
822
823        let spec = TargetConfig::new_reach(
824            HashSet::from([Location::new("l2")]),
825            HashSet::from([Location::new("l0"), Location::new("l1")]),
826        )
827        .unwrap()
828        .into_disjunct_with_name("test");
829
830        let sym_err_graph = smc.compute_symbolic_error_graph(&ata, &spec);
831
832        assert!(!sym_err_graph.is_empty());
833    }
834
835    #[test]
836    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop() {
837        let test_spec = "
838            skel test_ta1 {
839                shared var1, var2, var3;
840                parameters n, f;
841                
842                assumptions (1) {
843                    n > 3 * f;
844                    n == 1;
845                    f == 0;
846                }
847
848                locations (2) {
849                    loc1 : [0];
850                    loc2 : [1];
851                    loc3 : [2];
852                }
853
854                inits (1) {
855                    loc1 == n - f;
856                    loc2 == 0;
857                    loc3 == 0;
858                    var1 == 0;
859                    var2 == 0;
860                    var3 == 0;
861                }
862
863                rules (4) {
864                    0: loc1 -> loc1
865                        when(true)
866                        do {var1' == var1 + 1};
867                    1: loc1 -> loc2
868                        when(true)
869                        do {};
870                    2: loc2 -> loc3
871                        when(var1 > 3 && var2 <= 0 && var1 <= 4)
872                        do {};
873                    
874                }
875
876                specifications (1) {
877                    test1:
878                        [](loc3 == 0)
879                }
880            }
881            ";
882
883        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
884
885        let mc = ZCSModelChecker::new(
886            Some((
887                Some(SMTSolverBuilderCfg::new_z3()),
888                Some(BDDManagerConfig::new_cudd()),
889            )),
890            Some(ZCSModelCheckerHeuristics::CanonicalHeuristics),
891            Vec::new(),
892            ta.clone(),
893            spec.into_iter(),
894        );
895        let mc = mc.unwrap();
896        let res = mc.verify(true).unwrap();
897
898        // Replicate spec ta that is created for ta builder
899        let mut spec_ta = ta.clone();
900        spec_ta.set_name("test_ta1-test1".into());
901
902        // Replicate interval ta for path builder
903
904        let path = PathBuilder::new(spec_ta)
905            .add_parameter_assignment(HashMap::from([
906                (Parameter::new("n"), 1),
907                (Parameter::new("f"), 0),
908            ]))
909            .unwrap()
910            .add_configuration(Configuration::new(
911                HashMap::from([
912                    (Variable::new("var1"), 0),
913                    (Variable::new("var2"), 0),
914                    (Variable::new("var3"), 0),
915                ]),
916                HashMap::from([
917                    (Location::new("loc1"), 1),
918                    (Location::new("loc2"), 0),
919                    (Location::new("loc3"), 0),
920                ]),
921            ))
922            .unwrap()
923            .add_transition(Transition::new(
924                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
925                    .with_action(Action::new_with_update(
926                        Variable::new("var1"),
927                        UpdateExpression::Inc(1),
928                    ))
929                    .build(),
930                1,
931            ))
932            .unwrap()
933            .add_configuration(Configuration::new(
934                HashMap::from([
935                    (Variable::new("var1"), 1),
936                    (Variable::new("var2"), 0),
937                    (Variable::new("var3"), 0),
938                ]),
939                HashMap::from([
940                    (Location::new("loc1"), 1),
941                    (Location::new("loc2"), 0),
942                    (Location::new("loc3"), 0),
943                ]),
944            ))
945            .unwrap()
946            .add_transition(Transition::new(
947                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
948                    .with_action(Action::new_with_update(
949                        Variable::new("var1"),
950                        UpdateExpression::Inc(1),
951                    ))
952                    .build(),
953                2,
954            ))
955            .unwrap()
956            .add_configuration(Configuration::new(
957                HashMap::from([
958                    (Variable::new("var1"), 3),
959                    (Variable::new("var2"), 0),
960                    (Variable::new("var3"), 0),
961                ]),
962                HashMap::from([
963                    (Location::new("loc1"), 1),
964                    (Location::new("loc2"), 0),
965                    (Location::new("loc3"), 0),
966                ]),
967            ))
968            .unwrap()
969            .add_transition(Transition::new(
970                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
971                    .with_action(Action::new_with_update(
972                        Variable::new("var1"),
973                        UpdateExpression::Inc(1),
974                    ))
975                    .build(),
976                1,
977            ))
978            .unwrap()
979            .add_configuration(Configuration::new(
980                HashMap::from([
981                    (Variable::new("var1"), 4),
982                    (Variable::new("var2"), 0),
983                    (Variable::new("var3"), 0),
984                ]),
985                HashMap::from([
986                    (Location::new("loc1"), 1),
987                    (Location::new("loc2"), 0),
988                    (Location::new("loc3"), 0),
989                ]),
990            ))
991            .unwrap()
992            .add_transition(Transition::new(
993                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
994                1,
995            ))
996            .unwrap()
997            .add_configuration(Configuration::new(
998                HashMap::from([
999                    (Variable::new("var1"), 4),
1000                    (Variable::new("var2"), 0),
1001                    (Variable::new("var3"), 0),
1002                ]),
1003                HashMap::from([
1004                    (Location::new("loc1"), 0),
1005                    (Location::new("loc2"), 1),
1006                    (Location::new("loc3"), 0),
1007                ]),
1008            ))
1009            .unwrap()
1010            .add_transition(Transition::new(
1011                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
1012                    .with_guard(
1013                        BooleanExpression::ComparisonExpression(
1014                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1015                            ComparisonOp::Gt,
1016                            Box::new(IntegerExpression::Const(3)),
1017                        ) & BooleanExpression::ComparisonExpression(
1018                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1019                            ComparisonOp::Leq,
1020                            Box::new(IntegerExpression::Const(0)),
1021                        ) & BooleanExpression::ComparisonExpression(
1022                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1023                            ComparisonOp::Leq,
1024                            Box::new(IntegerExpression::Const(4)),
1025                        ),
1026                    )
1027                    .build(),
1028                1,
1029            ))
1030            .unwrap()
1031            .add_configuration(Configuration::new(
1032                HashMap::from([
1033                    (Variable::new("var1"), 4),
1034                    (Variable::new("var2"), 0),
1035                    (Variable::new("var3"), 0),
1036                ]),
1037                HashMap::from([
1038                    (Location::new("loc1"), 0),
1039                    (Location::new("loc2"), 0),
1040                    (Location::new("loc3"), 1),
1041                ]),
1042            ))
1043            .unwrap()
1044            .build()
1045            .unwrap();
1046
1047        let res = match res {
1048            ModelCheckerResult::SAFE => unreachable!("checked above"),
1049            ModelCheckerResult::UNSAFE(v) => {
1050                assert_eq!(v.len(), 1);
1051                *v[0].1.clone()
1052            }
1053            ModelCheckerResult::UNKNOWN(_) => todo!(),
1054        };
1055
1056        assert_eq!(
1057            res,
1058            path.clone(),
1059            "Got:\n{}\n\nExpected:\n{}\n\n",
1060            res,
1061            path
1062        );
1063    }
1064
1065    #[test]
1066    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop_with_var_constr() {
1067        let test_spec = "
1068            skel test_ta1 {
1069                shared var1, var2, var3;
1070                parameters n, f;
1071                
1072                assumptions (1) {
1073                    n > 3 * f;
1074                    n == 1;
1075                    f == 0;
1076                }
1077
1078                locations (2) {
1079                    loc1 : [0];
1080                    loc2 : [1];
1081                    loc3 : [2];
1082                }
1083
1084                inits (1) {
1085                    loc1 == n - f;
1086                    loc2 == 0;
1087                    loc3 == 0;
1088                    var1 == 0;
1089                    var2 == 0;
1090                    var3 == 0;
1091                }
1092
1093                rules (4) {
1094                    0: loc1 -> loc1
1095                        when(true)
1096                        do {var1' == var1 + 1};
1097                    1: loc1 -> loc2
1098                        when(true)
1099                        do {};
1100                    2: loc2 -> loc3
1101                        when(var1 > 3 && var2 <= 0 && var1 < 6 )
1102                        do {};
1103                    
1104                }
1105
1106                specifications (1) {
1107                    test1:
1108                        []((loc3 == 0) || (var1 < 5))
1109                }
1110            }
1111            ";
1112
1113        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
1114
1115        let mc = ZCSModelChecker::new(
1116            Some((
1117                Some(SMTSolverBuilderCfg::new_z3()),
1118                Some(BDDManagerConfig::new_cudd()),
1119            )),
1120            Some(ZCSModelCheckerHeuristics::CanonicalHeuristics),
1121            Vec::new(),
1122            ta.clone(),
1123            spec.into_iter(),
1124        );
1125        let mc = mc.unwrap();
1126        let res = mc.verify(true).unwrap();
1127
1128        // Replicate spec ta that is created for ta builder
1129        let mut spec_ta = ta.clone();
1130        spec_ta.set_name("test_ta1-test1".into());
1131
1132        // Replicate interval ta for path builder
1133
1134        let path = PathBuilder::new(spec_ta)
1135            .add_parameter_assignment(HashMap::from([
1136                (Parameter::new("n"), 1),
1137                (Parameter::new("f"), 0),
1138            ]))
1139            .unwrap()
1140            .add_configuration(Configuration::new(
1141                HashMap::from([
1142                    (Variable::new("var1"), 0),
1143                    (Variable::new("var2"), 0),
1144                    (Variable::new("var3"), 0),
1145                ]),
1146                HashMap::from([
1147                    (Location::new("loc1"), 1),
1148                    (Location::new("loc2"), 0),
1149                    (Location::new("loc3"), 0),
1150                ]),
1151            ))
1152            .unwrap()
1153            .add_transition(Transition::new(
1154                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
1155                    .with_action(Action::new_with_update(
1156                        Variable::new("var1"),
1157                        UpdateExpression::Inc(1),
1158                    ))
1159                    .build(),
1160                5,
1161            ))
1162            .unwrap()
1163            .add_configuration(Configuration::new(
1164                HashMap::from([
1165                    (Variable::new("var1"), 5),
1166                    (Variable::new("var2"), 0),
1167                    (Variable::new("var3"), 0),
1168                ]),
1169                HashMap::from([
1170                    (Location::new("loc1"), 1),
1171                    (Location::new("loc2"), 0),
1172                    (Location::new("loc3"), 0),
1173                ]),
1174            ))
1175            .unwrap()
1176            .add_transition(Transition::new(
1177                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
1178                1,
1179            ))
1180            .unwrap()
1181            .add_configuration(Configuration::new(
1182                HashMap::from([
1183                    (Variable::new("var1"), 5),
1184                    (Variable::new("var2"), 0),
1185                    (Variable::new("var3"), 0),
1186                ]),
1187                HashMap::from([
1188                    (Location::new("loc1"), 0),
1189                    (Location::new("loc2"), 1),
1190                    (Location::new("loc3"), 0),
1191                ]),
1192            ))
1193            .unwrap()
1194            .add_transition(Transition::new(
1195                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
1196                    .with_guard(
1197                        BooleanExpression::ComparisonExpression(
1198                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1199                            ComparisonOp::Gt,
1200                            Box::new(IntegerExpression::Const(3)),
1201                        ) & BooleanExpression::ComparisonExpression(
1202                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1203                            ComparisonOp::Leq,
1204                            Box::new(IntegerExpression::Const(0)),
1205                        ) & BooleanExpression::ComparisonExpression(
1206                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1207                            ComparisonOp::Lt,
1208                            Box::new(IntegerExpression::Const(6)),
1209                        ),
1210                    )
1211                    .build(),
1212                1,
1213            ))
1214            .unwrap()
1215            .add_configuration(Configuration::new(
1216                HashMap::from([
1217                    (Variable::new("var1"), 5),
1218                    (Variable::new("var2"), 0),
1219                    (Variable::new("var3"), 0),
1220                ]),
1221                HashMap::from([
1222                    (Location::new("loc1"), 0),
1223                    (Location::new("loc2"), 0),
1224                    (Location::new("loc3"), 1),
1225                ]),
1226            ))
1227            .unwrap()
1228            .build()
1229            .unwrap();
1230
1231        let res = match res {
1232            ModelCheckerResult::SAFE => unreachable!("checked above"),
1233            ModelCheckerResult::UNSAFE(v) => {
1234                assert_eq!(v.len(), 1);
1235                *v[0].1.clone()
1236            }
1237            ModelCheckerResult::UNKNOWN(_) => todo!(),
1238        };
1239
1240        assert_eq!(
1241            res,
1242            path.clone(),
1243            "Got:\n{}\n\nExpected:\n{}\n\n",
1244            res,
1245            path
1246        );
1247    }
1248}
taco_zcs_model_checker/lib.rs

taco_zcs_model_checker/
lib.rs
