Struct BacktrackingTraversal 

pub struct BacktrackingTraversal {
    pub branch_factor: u64,
    pub max_depth: usize,
    pub init_aux: u64,
    pub path: Vec<u64>,
    pub aux: u64,
    pub ledger: Vec<UndoToken>,
    pub visited: Vec<Vec<u64>>,
}

Reversible depth-first traversal owner.

Fields

branch_factor: u64

Number of admitted choices at each non-leaf depth.

max_depth: usize

Required depth of a complete leaf path.

init_aux: u64

Auxiliary value at the root.

path: Vec<u64>

Current branch-choice path.

aux: u64

Current auxiliary value.

ledger: Vec<UndoToken>

Undo tokens aligned with the current path.

visited: Vec<Vec<u64>>

A Vec is the executable representation of the TLA+ visited set; visited_unique and Visit’s freshness guard preserve set semantics.

Implementations

impl BacktrackingTraversal

pub fn mutate_exec(v: u64, d: u64) -> u64

Apply the modulo-three auxiliary mutation.

pub fn undo_exec(v: u64, d: u64) -> u64

Apply the inverse modulo-three auxiliary mutation.

pub fn new( branch_factor: u64, max_depth: usize, init_aux: u64, ) -> BacktrackingTraversal

Construct a traversal at its root with an empty visited set.

pub fn is_leaf_exec(&self) -> bool

Whether the current path has reached the configured leaf depth.

pub fn can_descend(&self, c: u64, d: u64) -> bool

Whether a choice and mutation delta enable another descent.

pub fn can_ascend(&self) -> bool

Whether an undo token is available for ascent.

pub fn has_visited(&self, p: &Vec<u64>) -> bool

Whether a path occurs in the visited-leaf ledger.

pub fn can_visit(&self) -> bool

Whether the current path is a fresh leaf that may be visited.

pub fn descend(&mut self, c: u64, d: u64)

Descend(c,d): record the undo token and apply its mutation atomically.

pub fn visit(&mut self)

Visit: append the current leaf only when it is fresh.

pub fn ascend(&mut self)

Ascend: apply the recorded inverse, then pop token and path.