taco_acs_model_checker/error_graph/
edge.rs

1//! Edge type for the error graph
2//!
3//! An edge in the [`super::ErrorGraph`] stores the ids of the rules that lead to the
4//! successor node.
5//!
6//! This module only borrows a `NodeRef` when creating a new edge.
7
8use std::collections::BTreeSet;
9
10use crate::{
11    acs_threshold_automaton::{CSRule, configuration::ACSTAConfig},
12    error_graph::NodeRef,
13};
14
15/// Edge in the error graph
16///
17/// An edge in the error graph consists of a rule id and a reference to a node.
18/// When inserted into a node `a` of the error graph, it means that we can
19/// derive the configuration of `node` by applying the rule with id `rule_id` to
20/// `a`.
21#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
22pub struct ErrorGraphEdge {
23    /// Ids of the rules used to derive this edge
24    rule_id: BTreeSet<u32>,
25    /// Config of the successor node
26    cfg: ACSTAConfig,
27    /// Successor node which configuration can be derived by applying the rule
28    /// with id `rule_id`
29    node: NodeRef,
30}
31
32impl ErrorGraphEdge {
33    /// Create a new [`ErrorGraphEdge`]
34    ///
35    /// Borrows `node` immutable during creation of the node
36    pub fn new(rule: &CSRule, node: NodeRef) -> Self {
37        let cfg = node.borrow().config().clone();
38
39        Self {
40            rule_id: BTreeSet::from([rule.id()]),
41            node,
42            cfg,
43        }
44    }
45
46    /// Returns the configuration of the successor node of this edge
47    pub fn get_successor_configuration(&self) -> &ACSTAConfig {
48        &self.cfg
49    }
50
51    /// Get the id of the rule that this edge has been derived from
52    pub fn get_ids_of_rules(&self) -> impl Iterator<Item = u32> {
53        self.rule_id.iter().cloned()
54    }
55
56    /// Get the node this edge leads to
57    pub fn node(&self) -> &NodeRef {
58        &self.node
59    }
60
61    /// Insert a new edge into a collection of error graph edges
62    pub fn insert_to_edge_collection(v: &mut Vec<ErrorGraphEdge>, e: ErrorGraphEdge) {
63        let found = v.iter_mut().fold(false, |acc, x| {
64            if !acc && x.get_successor_configuration() == e.get_successor_configuration() {
65                x.rule_id.extend(e.rule_id.clone());
66                return true;
67            }
68            acc
69        });
70
71        if !found {
72            v.push(e);
73        }
74    }
75}
76
77#[cfg(test)]
78mod new_mock {
79    use std::collections::BTreeSet;
80
81    use crate::error_graph::{NodeRef, edge::ErrorGraphEdge};
82
83    impl ErrorGraphEdge {
84        pub fn new_mock_with_id(r: u32, node: NodeRef) -> Self {
85            let cfg = node.borrow().config().clone();
86
87            Self {
88                rule_id: BTreeSet::from([r]),
89                node,
90                cfg,
91            }
92        }
93    }
94}
95
96#[cfg(test)]
97mod tests {
98
99    use std::collections::BTreeSet;
100
101    use crate::{
102        acs_threshold_automaton::{
103            ACSLocation, CSIntervalConstraint, CSRule, configuration::ACSTAConfig,
104        },
105        error_graph::{NodeRef, edge::ErrorGraphEdge, node::ErrorGraphNode},
106    };
107
108    #[test]
109    fn test_error_graph_edge() {
110        let node: NodeRef = ErrorGraphNode::new_mock(
111            0,
112            ACSTAConfig::new_mock_from_vecs(Vec::new(), Vec::new()),
113            Vec::new(),
114            Vec::new(),
115            Vec::new(),
116        )
117        .into();
118
119        let rule = CSRule::new_mock(
120            42,
121            ACSLocation::new_mock(0),
122            ACSLocation::new_mock(2),
123            CSIntervalConstraint::False,
124            Vec::new(),
125        );
126
127        let edge = ErrorGraphEdge::new(&rule, node.clone());
128
129        assert_eq!(
130            edge,
131            ErrorGraphEdge {
132                rule_id: BTreeSet::from([42]),
133                node: node.clone(),
134                cfg: node.borrow().config().clone(),
135            }
136        );
137
138        assert_eq!(edge.get_ids_of_rules().collect::<Vec<_>>(), vec![42]);
139        assert_eq!(edge.node(), &node);
140        assert_eq!(
141            edge.get_successor_configuration(),
142            &ACSTAConfig::new_mock_from_vecs(Vec::new(), Vec::new())
143        );
144    }
145}
taco_acs_model_checker/error_graph/edge.rs

taco_acs_model_checker/error_graph/
edge.rs
