libpetri_verification/
state_class.rs

1use crate::dbm::Dbm;
2use crate::marking_state::MarkingState;
3
4/// A state class: pair of (M: marking, D: firing domain DBM).
5///
6/// Provides a finite abstraction of the infinite Time Petri Net state space.
7#[derive(Debug, Clone)]
8pub struct StateClass {
9    pub marking: MarkingState,
10    pub dbm: Dbm,
11    pub enabled_transitions: Vec<String>,
12}
13
14impl StateClass {
15    pub fn new(marking: MarkingState, dbm: Dbm, enabled_transitions: Vec<String>) -> Self {
16        Self {
17            marking,
18            dbm,
19            enabled_transitions,
20        }
21    }
22
23    /// Returns true if the firing domain is empty.
24    pub fn is_empty(&self) -> bool {
25        self.dbm.is_empty()
26    }
27
28    /// Returns whether transition at the given clock index can fire.
29    pub fn can_fire(&self, clock_idx: usize) -> bool {
30        self.dbm.can_fire(clock_idx)
31    }
32
33    /// Looks up a transition clock index by name.
34    pub fn transition_index(&self, name: &str) -> Option<usize> {
35        self.enabled_transitions.iter().position(|n| n == name)
36    }
37
38    /// Generates a canonical key for deduplication.
39    pub fn canonical_key(&self) -> String {
40        format!(
41            "{}|{}",
42            self.marking.canonical_key(),
43            self.dbm.canonical_string()
44        )
45    }
46}
47
48impl PartialEq for StateClass {
49    fn eq(&self, other: &Self) -> bool {
50        self.marking == other.marking && self.dbm == other.dbm
51    }
52}
53
54impl Eq for StateClass {}
55
56#[cfg(test)]
57mod tests {
58    use super::*;
59    use crate::marking_state::MarkingStateBuilder;
60
61    #[test]
62    fn state_class_basic() {
63        let marking = MarkingStateBuilder::new().tokens("p1", 1).build();
64        let dbm = Dbm::create(vec!["t1".to_string()], &[0.0], &[f64::INFINITY]);
65        let sc = StateClass::new(marking, dbm, vec!["t1".to_string()]);
66
67        assert!(!sc.is_empty());
68        assert_eq!(sc.transition_index("t1"), Some(0));
69        assert_eq!(sc.transition_index("nonexistent"), None);
70    }
71
72    #[test]
73    fn state_class_canonical_key() {
74        let marking = MarkingStateBuilder::new().tokens("p1", 1).build();
75        let dbm = Dbm::create(vec!["t1".to_string()], &[0.0], &[10.0]);
76        let sc = StateClass::new(marking, dbm, vec!["t1".to_string()]);
77
78        let key = sc.canonical_key();
79        assert!(!key.is_empty());
80    }
81
82    #[test]
83    fn state_class_equality() {
84        let m1 = MarkingStateBuilder::new().tokens("p1", 1).build();
85        let m2 = MarkingStateBuilder::new().tokens("p1", 1).build();
86        let d1 = Dbm::create(vec!["t1".to_string()], &[0.0], &[10.0]);
87        let d2 = Dbm::create(vec!["t1".to_string()], &[0.0], &[10.0]);
88
89        let sc1 = StateClass::new(m1, d1, vec!["t1".to_string()]);
90        let sc2 = StateClass::new(m2, d2, vec!["t1".to_string()]);
91
92        assert_eq!(sc1, sc2);
93    }
94}
libpetri_verification/state_class.rs

libpetri_verification/
state_class.rs
