machine_check_common/
property.rs

1//! Computation Tree Logic properties.
2use std::{collections::BTreeSet, fmt::Debug};
3
4use std::sync::Arc;
5
6use crate::ExecError;
7use serde::{Deserialize, Serialize};
8
9mod atomic;
10mod closed_form;
11mod parser;
12mod transition_depth;
13
14pub use atomic::{AtomicProperty, ComparisonType, ValueExpression};
15
16/// A Computation Tree Logic property.
17#[derive(Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
18pub struct Property {
19    arena: Arc<Vec<SubpropertyEntry>>,
20}
21
22impl Property {
23    pub fn root_subproperty(&self) -> Subproperty {
24        Subproperty {
25            property: self.clone(),
26            index: 0,
27        }
28    }
29
30    pub fn subproperty_entry(&self, index: usize) -> &SubpropertyEntry {
31        self.arena
32            .get(index)
33            .expect("Subproperty should be within property arena size")
34    }
35
36    pub fn affected_fixed_points(&self, index: usize) -> BTreeSet<usize> {
37        let ty = &self.get_by_index(index).ty;
38        match ty {
39            PropertyType::Const(_) | PropertyType::Atomic(_) => BTreeSet::new(),
40            PropertyType::Negation(inner) => self.affected_fixed_points(*inner),
41            PropertyType::BiLogic(bi_logic_operator) => BTreeSet::from_iter(
42                self.affected_fixed_points(bi_logic_operator.a)
43                    .union(&self.affected_fixed_points(bi_logic_operator.b))
44                    .copied(),
45            ),
46            PropertyType::Next(next_operator) => self.affected_fixed_points(next_operator.inner),
47            PropertyType::FixedPoint(fixed_point_operator) => {
48                let mut inner_affected = self.affected_fixed_points(fixed_point_operator.inner);
49                inner_affected.insert(index);
50                inner_affected
51            }
52            PropertyType::FixedVariable(inner) => BTreeSet::from([*inner]),
53        }
54    }
55
56    pub fn inherent() -> Self {
57        parser::inherent()
58    }
59
60    pub fn num_subproperties(&self) -> usize {
61        self.arena.len()
62    }
63}
64
65impl Debug for Property {
66    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
67        let mut builder = f.debug_struct("Property");
68        for (index, entry) in self.arena.iter().enumerate() {
69            let index_string = index.to_string();
70            builder.field(&index_string, entry);
71        }
72
73        builder.finish()
74    }
75}
76
77#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
78pub struct Subproperty {
79    property: Property,
80    index: usize,
81}
82
83impl Subproperty {
84    pub fn property(&self) -> &Property {
85        &self.property
86    }
87
88    pub fn index(&self) -> usize {
89        self.index
90    }
91
92    pub fn display_str(&self) -> Option<&str> {
93        self.property
94            .get_by_index(self.index)
95            .display_string
96            .as_deref()
97    }
98
99    pub fn is_visible(&self) -> bool {
100        self.property.get_by_index(self.index).visible
101    }
102}
103
104#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
105pub struct SubpropertyEntry {
106    pub ty: PropertyType,
107    display_string: Option<String>,
108    visible: bool,
109}
110
111#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
112pub enum PropertyType {
113    Const(bool),
114    Atomic(AtomicProperty),
115    Negation(usize),
116    BiLogic(BiLogicOperator),
117    Next(NextOperator),
118    FixedPoint(FixedPointOperator),
119    FixedVariable(usize),
120}
121
122#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
123pub struct BiLogicOperator {
124    pub is_and: bool,
125    pub a: usize,
126    pub b: usize,
127    pub reverse_display: bool,
128}
129
130#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
131pub struct NextOperator {
132    pub is_universal: bool,
133    pub inner: usize,
134}
135
136#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
137pub struct FixedPointOperator {
138    pub is_greatest: bool,
139    pub inner: usize,
140}
141
142impl Property {
143    pub fn parse(prop_str: &str) -> Result<Property, ExecError> {
144        parser::parse(prop_str)
145    }
146
147    fn get_by_index(&self, index: usize) -> &SubpropertyEntry {
148        self.arena
149            .get(index)
150            .expect("Subproperty index should be within property arena")
151    }
152}
153
154impl Subproperty {
155    fn new(property: Property, index: usize) -> Self {
156        assert!(index < property.arena.len());
157        Self { property, index }
158    }
159
160    pub fn displayed_children(&self) -> Vec<Subproperty> {
161        let ty = &self.property.get_by_index(self.index).ty;
162
163        let indices: Vec<usize> = match ty {
164            PropertyType::Const(_) => Vec::new(),
165            PropertyType::Atomic(_) => Vec::new(),
166            PropertyType::Negation(inner) => vec![*inner],
167            PropertyType::BiLogic(op) => {
168                if op.reverse_display {
169                    vec![op.b, op.a]
170                } else {
171                    vec![op.a, op.b]
172                }
173            }
174            PropertyType::Next(op) => vec![op.inner],
175            PropertyType::FixedPoint(op) => {
176                vec![op.inner]
177            }
178            PropertyType::FixedVariable(_) => Vec::new(),
179        };
180
181        indices
182            .into_iter()
183            .map(|index| Subproperty::new(self.property.clone(), index))
184            .collect()
185    }
186}
machine_check_common/property.rs

machine_check_common/
property.rs
