vertep_core/
trace.rs

1//! Per-macrostep trace records.
2//!
3//! Every [`crate::session::start`] and [`crate::session::step`] call returns one
4//! [`MacrostepTrace`]: the input it processed, each event it consumed with the transitions that
5//! event (or an eventless selection) fired, the configuration afterwards and the effects it
6//! emitted. Rust and the Lean oracle produce these records independently and the differential
7//! tests compare them for equality. See [`crate::tape`] for the JSON Lines exchange format.
8
9use alloc::string::String;
10use alloc::vec::Vec;
11
12use crate::datamodel::Event;
13use crate::session::Effect;
14
15/// A declared transition, identified by its source state and its index in that state's
16/// transition list in the IR.
17#[derive(Clone, Debug, PartialEq, Eq, Hash)]
18#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
19pub struct TransitionRef {
20    /// The source state identifier.
21    pub source: String,
22    /// Index in the source's `transitions`.
23    pub index: usize,
24}
25
26/// What a macrostep was started by.
27#[derive(Clone, Debug, PartialEq)]
28#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
29pub enum TraceInput {
30    /// Session start, with the session identifier.
31    Start {
32        /// `_sessionid`.
33        sessionid: String,
34    },
35    /// An external event.
36    Event(Event),
37    /// A cancel request from the host or parent session.
38    Cancel,
39}
40
41/// One selection round inside a macrostep.
42#[derive(Clone, Debug, PartialEq, Eq)]
43#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
44pub struct MicrostepTrace {
45    /// The event consumed (`None` for an eventless selection).
46    pub event: Option<String>,
47    /// The transitions fired, in the order they were selected; empty when the event enabled
48    /// nothing.
49    pub transitions: Vec<TransitionRef>,
50}
51
52/// The record of one macrostep (one `start` or `step` call).
53#[derive(Clone, Debug, PartialEq)]
54#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
55pub struct MacrostepTrace {
56    /// 0 for the start macrostep, then 1, 2, ...
57    pub index: u64,
58    /// What started the macrostep.
59    pub input: TraceInput,
60    /// Events consumed and transitions fired, in order.
61    pub microsteps: Vec<MicrostepTrace>,
62    /// Active state identifiers after the macrostep, in document order.
63    pub configuration: Vec<String>,
64    /// Effects emitted, in order.
65    pub effects: Vec<Effect>,
66    /// Whether the session terminated in this macrostep.
67    pub terminated: bool,
68}
vertep_core/trace.rs

vertep_core/
trace.rs
