libpetri_verification/
marking_state.rs

1use std::collections::HashMap;
2
3/// Immutable snapshot of a Petri net marking for state space analysis.
4///
5/// Maps places by name to integer token counts. Only stores places with count > 0.
6#[derive(Debug, Clone, PartialEq, Eq)]
7pub struct MarkingState {
8    tokens: HashMap<String, usize>,
9}
10
11impl MarkingState {
12    pub fn new() -> Self {
13        Self {
14            tokens: HashMap::new(),
15        }
16    }
17
18    pub fn from_map(tokens: HashMap<String, usize>) -> Self {
19        let tokens = tokens.into_iter().filter(|(_, c)| *c > 0).collect();
20        Self { tokens }
21    }
22
23    /// Returns the token count for a place.
24    pub fn count(&self, place: &str) -> usize {
25        self.tokens.get(place).copied().unwrap_or(0)
26    }
27
28    /// Returns all places with non-zero counts.
29    pub fn places(&self) -> impl Iterator<Item = (&str, usize)> {
30        self.tokens.iter().map(|(k, v)| (k.as_str(), *v))
31    }
32
33    /// Returns true if the marking is empty (no tokens anywhere).
34    pub fn is_empty(&self) -> bool {
35        self.tokens.is_empty()
36    }
37
38    /// Returns the total number of tokens across all places.
39    pub fn total_tokens(&self) -> usize {
40        self.tokens.values().sum()
41    }
42
43    /// Returns true if this marking has tokens in any of the named places.
44    pub fn has_tokens_in_any(&self, place_names: &[&str]) -> bool {
45        place_names.iter().any(|name| self.count(name) > 0)
46    }
47
48    /// Generates a canonical key for deduplication.
49    pub fn canonical_key(&self) -> String {
50        let mut entries: Vec<_> = self.tokens.iter().collect();
51        entries.sort_by_key(|(k, _)| k.as_str());
52        entries
53            .iter()
54            .map(|(k, v)| format!("{k}:{v}"))
55            .collect::<Vec<_>>()
56            .join(",")
57    }
58}
59
60impl Default for MarkingState {
61    fn default() -> Self {
62        Self::new()
63    }
64}
65
66/// Builder for constructing MarkingState instances.
67pub struct MarkingStateBuilder {
68    tokens: HashMap<String, usize>,
69}
70
71impl MarkingStateBuilder {
72    pub fn new() -> Self {
73        Self {
74            tokens: HashMap::new(),
75        }
76    }
77
78    pub fn tokens(mut self, place: impl Into<String>, count: usize) -> Self {
79        let key = place.into();
80        if count > 0 {
81            self.tokens.insert(key, count);
82        } else {
83            self.tokens.remove(&key);
84        }
85        self
86    }
87
88    pub fn add_tokens(mut self, place: impl Into<String>, count: usize) -> Self {
89        let entry = self.tokens.entry(place.into()).or_insert(0);
90        *entry += count;
91        self
92    }
93
94    pub fn build(self) -> MarkingState {
95        MarkingState::from_map(self.tokens)
96    }
97}
98
99impl Default for MarkingStateBuilder {
100    fn default() -> Self {
101        Self::new()
102    }
103}
104
105#[cfg(test)]
106mod tests {
107    use super::*;
108
109    #[test]
110    fn marking_state_basics() {
111        let ms = MarkingStateBuilder::new()
112            .tokens("p1", 2)
113            .tokens("p2", 1)
114            .build();
115
116        assert_eq!(ms.count("p1"), 2);
117        assert_eq!(ms.count("p2"), 1);
118        assert_eq!(ms.count("p3"), 0);
119        assert_eq!(ms.total_tokens(), 3);
120        assert!(!ms.is_empty());
121    }
122
123    #[test]
124    fn canonical_key_deterministic() {
125        let ms1 = MarkingStateBuilder::new()
126            .tokens("b", 1)
127            .tokens("a", 2)
128            .build();
129        let ms2 = MarkingStateBuilder::new()
130            .tokens("a", 2)
131            .tokens("b", 1)
132            .build();
133        assert_eq!(ms1.canonical_key(), ms2.canonical_key());
134    }
135
136    #[test]
137    fn empty_marking() {
138        let ms = MarkingState::new();
139        assert!(ms.is_empty());
140        assert_eq!(ms.total_tokens(), 0);
141        assert_eq!(ms.canonical_key(), "");
142    }
143
144    #[test]
145    fn zero_count_filtered() {
146        let ms = MarkingStateBuilder::new()
147            .tokens("p1", 0)
148            .tokens("p2", 1)
149            .build();
150        assert_eq!(ms.count("p1"), 0);
151        assert_eq!(ms.count("p2"), 1);
152        assert_eq!(ms.total_tokens(), 1);
153    }
154
155    #[test]
156    fn add_tokens_accumulates() {
157        let ms = MarkingStateBuilder::new()
158            .add_tokens("p1", 2)
159            .add_tokens("p1", 3)
160            .build();
161        assert_eq!(ms.count("p1"), 5);
162    }
163
164    #[test]
165    fn equality() {
166        let ms1 = MarkingStateBuilder::new().tokens("p", 2).build();
167        let ms2 = MarkingStateBuilder::new().tokens("p", 2).build();
168        assert_eq!(ms1, ms2);
169    }
170
171    #[test]
172    fn inequality_different_count() {
173        let ms1 = MarkingStateBuilder::new().tokens("p", 1).build();
174        let ms2 = MarkingStateBuilder::new().tokens("p", 2).build();
175        assert_ne!(ms1, ms2);
176    }
177}
libpetri_verification/marking_state.rs

libpetri_verification/
marking_state.rs
