libpetri_verification/
counterexample.rs

1use crate::marking_state::MarkingState;
2#[allow(unused_imports)]
3use crate::marking_state::MarkingStateBuilder;
4#[allow(unused_imports)]
5use crate::net_flattener::FlatNet;
6
7/// A decoded counterexample trace from Z3.
8#[derive(Debug, Clone)]
9pub struct DecodedTrace {
10    pub trace: Vec<MarkingState>,
11    pub transitions: Vec<String>,
12}
13
14impl DecodedTrace {
15    pub fn empty() -> Self {
16        Self {
17            trace: Vec::new(),
18            transitions: Vec::new(),
19        }
20    }
21
22    pub fn is_empty(&self) -> bool {
23        self.trace.is_empty()
24    }
25}
26
27/// Decodes a Z3 proof answer into a counterexample trace.
28///
29/// Extracts marking states from `Reachable(m0, m1, ..., mP-1)` applications
30/// and transition names from rule applications prefixed with `t_`.
31///
32/// This is a best-effort decoder that gracefully degrades if the Z3 answer
33/// format varies — returns an empty trace rather than failing.
34#[cfg(feature = "z3")]
35pub fn decode(answer_str: &str, flat: &FlatNet) -> DecodedTrace {
36    let mut trace = Vec::new();
37    let mut transitions = Vec::new();
38
39    // Parse the answer string looking for Reachable applications and transition names.
40    // Z3 Spacer returns the answer as an S-expression tree.
41    // We look for patterns like (Reachable 0 1 0 ...) and (t_name ...)
42    for line in answer_str.lines() {
43        let trimmed = line.trim();
44
45        // Look for transition names (prefixed with t_)
46        if let Some(name) = extract_transition_name(trimmed) {
47            if let Some(original) = flat.transitions.iter().find(|ft| ft.name == name) {
48                transitions.push(original.name.clone());
49            } else {
50                transitions.push(name);
51            }
52        }
53
54        // Look for Reachable applications with integer arguments
55        if let Some(marking) = extract_marking(trimmed, flat) {
56            trace.push(marking);
57        }
58    }
59
60    DecodedTrace { trace, transitions }
61}
62
63/// Extracts a transition name from a Z3 S-expression fragment.
64#[allow(dead_code)]
65fn extract_transition_name(s: &str) -> Option<String> {
66    // Look for patterns like (t_name or |t_name|
67    let s = s.trim_start_matches('(').trim();
68    if s.starts_with("t_") || s.starts_with("|t_") {
69        let name = s
70            .trim_start_matches('|')
71            .split_whitespace()
72            .next()?
73            .trim_end_matches('|')
74            .trim_end_matches(')');
75        Some(name.to_string())
76    } else {
77        None
78    }
79}
80
81/// Extracts a MarkingState from a Reachable application in S-expression format.
82#[allow(dead_code)]
83fn extract_marking(s: &str, flat: &FlatNet) -> Option<MarkingState> {
84    // Pattern: (Reachable 0 1 0 ...) or (|Reachable| 0 1 0 ...)
85    let content = s.trim_start_matches('(').trim();
86    let prefix = if content.starts_with("|Reachable|") {
87        "|Reachable|"
88    } else if content.starts_with("Reachable") {
89        "Reachable"
90    } else {
91        return None;
92    };
93
94    let args = content[prefix.len()..].trim().trim_end_matches(')');
95    let values: Vec<i64> = args
96        .split_whitespace()
97        .filter_map(|tok| {
98            tok.trim_matches(|c: char| !c.is_ascii_digit() && c != '-')
99                .parse()
100                .ok()
101        })
102        .collect();
103
104    if values.len() != flat.place_count {
105        return None;
106    }
107
108    let mut builder = MarkingStateBuilder::new();
109    for (i, &count) in values.iter().enumerate() {
110        if count > 0 {
111            builder = builder.tokens(&flat.places[i], count as usize);
112        }
113    }
114    Some(builder.build())
115}
116
117#[cfg(test)]
118mod tests {
119    use super::*;
120
121    #[test]
122    fn empty_trace() {
123        let trace = DecodedTrace::empty();
124        assert!(trace.is_empty());
125        assert!(trace.transitions.is_empty());
126    }
127
128    #[cfg(feature = "z3")]
129    #[test]
130    fn extract_transition_name_basic() {
131        assert_eq!(
132            extract_transition_name("(t_fire_a 1 2 3)"),
133            Some("t_fire_a".into())
134        );
135        assert_eq!(
136            extract_transition_name("(|t_fire_b| 1 2)"),
137            Some("t_fire_b".into())
138        );
139        assert_eq!(extract_transition_name("(Reachable 1 2)"), None);
140    }
141
142    #[cfg(feature = "z3")]
143    #[test]
144    fn extract_marking_basic() {
145        use std::collections::HashMap;
146
147        let flat = FlatNet {
148            places: vec!["p1".into(), "p2".into()],
149            place_index: HashMap::from([("p1".into(), 0), ("p2".into(), 1)]),
150            place_count: 2,
151            transitions: Vec::new(),
152        };
153
154        let m = extract_marking("(Reachable 1 0)", &flat);
155        assert!(m.is_some());
156        let marking = m.unwrap();
157        assert_eq!(marking.count("p1"), 1);
158        assert_eq!(marking.count("p2"), 0);
159    }
160}
libpetri_verification/counterexample.rs

libpetri_verification/
counterexample.rs
