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

taco_zcs_model_checker/
lib.rs
