machine_check_common/property/
transition_depth.rs

1use crate::{check::Property, property::PropertyType};
2
3impl Property {
4    pub fn transition_depth(&self) -> usize {
5        self.transition_depth_inner(0)
6    }
7
8    fn transition_depth_inner(&self, subproperty_index: usize) -> usize {
9        let subproperty_entry = self.subproperty_entry(subproperty_index);
10
11        match &subproperty_entry.ty {
12            PropertyType::Const(_) | PropertyType::Atomic(_) | PropertyType::FixedVariable(_) => 0,
13            PropertyType::Negation(inner) => self.transition_depth_inner(*inner),
14            PropertyType::BiLogic(bi_logic_operator) => self
15                .transition_depth_inner(bi_logic_operator.a)
16                .max(self.transition_depth_inner(bi_logic_operator.b)),
17            PropertyType::Next(next_operator) => {
18                // increment the transition depth
19                self.transition_depth_inner(next_operator.inner) + 1
20            }
21            PropertyType::FixedPoint(fixed_point_operator) => {
22                self.transition_depth_inner(fixed_point_operator.inner)
23            }
24        }
25    }
26}