snappea 0.1.0

The P modeling language in Rust: emit events from your application and check them against P specs in tests, plus the `snappea` checker
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142

//! Coverage of monitor executions over observed logs. This measures states entered and
//! declared state/event handlers exercised, not P model paths or scheduler coverage.
//! Transition hits are reported without a denominator: action bodies can jump dynamically.

use std::collections::BTreeSet;

use crate::sema::{HandlerAction, MachineId, Program, StateId};

use crate::checker::coverage::{CoverageInfo, CoverageTables};

/// Stable state/event identity, suitable for union across processes or test cases.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
pub struct HandlerCoverage {
    pub state: String,
    pub event: String,
}

/// A transition actually taken, including transitions from action bodies.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
pub struct TransitionCoverage {
    pub source: String,
    pub target: String,
}

/// Mergeable coverage for selected monitor declarations, with compilation source identity.
/// Use `try_merge` for validated same-source union; `merge` is a low-level unchecked union.
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct ObserveCoverage {
    /// SHA-256 identity of all compilation source contents.
    pub source_fingerprint: Option<String>,
    pub declared_states: BTreeSet<String>,
    pub visited_states: BTreeSet<String>,
    /// Explicit do, goto and ignore handlers. Deferred events are not Java handlers.
    pub declared_handlers: BTreeSet<HandlerCoverage>,
    /// Includes the handler attempted when an assertion fails.
    pub visited_handlers: BTreeSet<HandlerCoverage>,
    pub transitions: BTreeSet<TransitionCoverage>,
}

fn state_name(prog: &Program, state: StateId) -> String {
    let s = prog.state(state);
    format!("{}.{}", prog.machine(s.machine).name, s.name)
}

impl ObserveCoverage {
    pub fn new(prog: &Program, spec: MachineId) -> Self {
        let mut result = Self { source_fingerprint: prog.source_fingerprint.clone(), ..Self::default() };
        for &state in &prog.machine(spec).states {
            let name = state_name(prog, state);
            result.declared_states.insert(name.clone());
            for handler in &prog.state(state).handlers {
                if !matches!(handler.action, HandlerAction::Defer) {
                    result
                        .declared_handlers
                        .insert(HandlerCoverage { state: name.clone(), event: prog.event(handler.event).name.clone() });
                }
            }
        }
        result
    }

    /// Unchecked union of hit sets and declarations, without summing duplicate hits.
    /// Callers must ensure source compatibility; portable reports use `try_merge` instead.
    pub fn merge(&mut self, other: &Self) {
        self.declared_states.extend(other.declared_states.iter().cloned());
        self.visited_states.extend(other.visited_states.iter().cloned());
        self.declared_handlers.extend(other.declared_handlers.iter().cloned());
        self.visited_handlers.extend(other.visited_handlers.iter().cloned());
        self.transitions.extend(other.transitions.iter().cloned());
    }

    pub(crate) fn record(&mut self, prog: &Program, tables: &CoverageTables, info: &CoverageInfo) {
        self.visited_states.extend(info.monitor_states.iter().map(|&s| state_name(prog, s)));
        for h in &self.declared_handlers {
            let hit = prog.states.iter().enumerate().any(|(i, s)| {
                state_name(prog, StateId(i as u32)) == h.state
                    && s.handlers.iter().any(|handler| {
                        prog.event(handler.event).name == h.event
                            && info.received.contains(&(tables.plain(StateId(i as u32)), handler.event.0))
                    })
            });
            if hit {
                self.visited_handlers.insert(h.clone());
            }
        }
        self.transitions.extend(
            info.monitor_transitions
                .iter()
                .map(|&(a, b)| TransitionCoverage { source: state_name(prog, a), target: state_name(prog, b) }),
        );
    }

    /// Stable machine-readable representation shared with `observe --json-report`.
    pub fn to_json(&self) -> serde_json::Value {
        let handlers = |items: &BTreeSet<HandlerCoverage>| {
            items.iter().map(|h| serde_json::json!({"state": h.state, "event": h.event})).collect::<Vec<_>>()
        };
        serde_json::json!({
            "schema_version": 1,
            "scope": "observed_monitor",
            "source_fingerprint": self.source_fingerprint,
            "states": {"total": self.declared_states.len(), "covered": self.visited_states.len(), "declared": self.declared_states, "visited": self.visited_states},
            "handlers": {"total": self.declared_handlers.len(), "covered": self.visited_handlers.len(), "declared": handlers(&self.declared_handlers), "visited": handlers(&self.visited_handlers)},
            "transitions": self.transitions.iter().map(|t| serde_json::json!({"source": t.source, "target": t.target})).collect::<Vec<_>>()
        })
    }

    /// Human-readable summary with every missing state and handler listed.
    pub fn render_text(&self) -> String {
        let mut out = format!(
            "Observed monitor coverage (not full model or schedule coverage)\nStates: {}/{}\nHandlers: {}/{}\nTransitions observed: {}\n",
            self.visited_states.len(), self.declared_states.len(), self.visited_handlers.len(),
            self.declared_handlers.len(), self.transitions.len()
        );
        for state in self.declared_states.difference(&self.visited_states) {
            out.push_str(&format!("  Unvisited state: {state}\n"));
        }
        for h in self.declared_handlers.difference(&self.visited_handlers) {
            out.push_str(&format!("  Uncovered handler: {} / {}\n", h.state, h.event));
        }
        out
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn suite_union_keeps_missing_declarations_and_deduplicates_hits() {
        let mut first = ObserveCoverage::default();
        first.declared_states.extend(["Spec.A".into(), "Spec.B".into(), "Spec.Unseen".into()]);
        first.visited_states.insert("Spec.A".into());
        let mut second = first.clone();
        second.visited_states.insert("Spec.B".into());
        first.merge(&second);
        first.merge(&second);
        assert_eq!(first.to_json()["states"]["covered"], 2);
        assert_eq!(first.to_json()["states"]["total"], 3);
        assert!(first.render_text().contains("Unvisited state: Spec.Unseen"));
    }
}