libpetri_verification/
result.rs

1use crate::marking_state::MarkingState;
2use crate::p_invariant::PInvariant;
3
4/// Verdict of a verification query.
5#[derive(Debug, Clone, PartialEq, Eq)]
6pub enum Verdict {
7    /// Property holds for all reachable states.
8    Proven {
9        /// The method that proved the property (e.g., "IC3/PDR" or "structural").
10        method: String,
11        /// Inductive invariant discovered by the solver, if available.
12        inductive_invariant: Option<String>,
13    },
14    /// Property is violated with a counterexample trace.
15    Violated,
16    /// Solver could not determine the result.
17    Unknown {
18        /// Reason for the unknown result.
19        reason: String,
20    },
21}
22
23impl Verdict {
24    pub fn is_proven(&self) -> bool {
25        matches!(self, Self::Proven { .. })
26    }
27
28    pub fn is_violated(&self) -> bool {
29        matches!(self, Self::Violated)
30    }
31}
32
33/// Statistics from the verification run.
34#[derive(Debug, Clone)]
35pub struct VerificationStatistics {
36    pub places: usize,
37    pub transitions: usize,
38    pub invariants_found: usize,
39    pub structural_result: String,
40}
41
42/// Result of an SMT verification query.
43#[derive(Debug, Clone)]
44pub struct VerificationResult {
45    pub verdict: Verdict,
46    pub report: String,
47    pub invariants: Vec<PInvariant>,
48    pub discovered_invariants: Vec<String>,
49    pub counterexample_trace: Vec<MarkingState>,
50    pub counterexample_transitions: Vec<String>,
51    pub elapsed_ms: u64,
52    pub statistics: VerificationStatistics,
53}
54
55impl VerificationResult {
56    pub fn is_proven(&self) -> bool {
57        self.verdict.is_proven()
58    }
59
60    pub fn is_violated(&self) -> bool {
61        self.verdict.is_violated()
62    }
63}
libpetri_verification/result.rs

libpetri_verification/
result.rs
