Struct Step 

#[non_exhaustive]
pub struct Step {
    pub action_taken: String,
    pub nondet_picks: Value,
    pub state: Value,
}

A single step from an Apalache-generated ITF trace.

Each ITF state record contains the TLA+ variables plus auxiliary MBT variables (action_taken, nondet_picks) that identify which action was taken and any nondeterministic choices.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

action_taken: String

The TLA+ action that was taken (e.g., “request_success”, “tick”).

nondet_picks: Value

Nondeterministic picks made by this step (ITF Value for proper type handling).

state: Value

Full TLA+ state after this step – an itf::Value::Record containing all state variables. Used for state comparison via State::from_spec.

Trait Implementations

impl Clone for Step

fn clone(&self) -> Step

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Step

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.