Module kernel 

The selection and entry/exit kernel of the W3C SCXML interpretation algorithm (Appendix D).

Every function here is a pure function over a CompiledChart, a configuration (StateSet) and the recorded History. The names follow Appendix D: select_transitions (selectTransitions and selectEventlessTransitions), remove_conflicting_transitions, compute_exit_set, compute_entry_set (computeEntrySet, addDescendantStatesToEnter, addAncestorStatesToEnter), transition_domain (getTransitionDomain), find_lcca, effective_targets (getEffectiveTargetStates), record_history (the history step of exitStates) and is_in_final_state.

Aeneas-friendly boundary

The kernel stays inside the Rust subset that Aeneas translates ([[constraints#Aeneas supports a Rust subset]]): it uses no trait objects, no interior mutability (Cell, RefCell), no unsafe, no async and no I/O. Data is plain vectors, bitsets of words and usize indices; iteration is over owned index vectors. The only abstraction is the generic condition oracle FnMut(TransIdx) -> bool taken by select_transitions, which is monomorphized, never dynamically dispatched.

Executable content and condition evaluation are outside the kernel: the session driver in crate::session calls the crate::datamodel::Datamodel trait object and applies the kernel’s plans (exit order, entry order, default entries, default history content) one state at a time, so the order of datamodel requests is fully determined by the kernel’s output. That order is what the datamodel tape (crate::tape) records for the Lean oracle.

Structs

EntryPlan

The result of computeEntrySet.

History

The history value table: for each history state, the states recorded when its parent was last exited, or None when it was never exited.

Functions

compute_domain

getTransitionDomain, computed from scratch.

compute_entry_set

computeEntrySet. domains are the transitions’ domains as compute_exit_set saw them, before exitStates recorded history (see transition_domains): Appendix D recomputes them here from the history just recorded, which can move a domain below a state the exit left (a deep history of a parallel state with one region), and that state was then never entered again.

compute_exit_set

computeExitSet: the active states that are proper descendants of the domains of the targeted transitions in ts.

descriptor_matches

Whether one event descriptor matches an event name (W3C SCXML 3.12.1): * matches every event; otherwise, after dropping a trailing .* or ., the descriptor must equal the name or be a prefix of it that ends at a . token boundary.

effective_targets

getEffectiveTargetStates: the targets of t with history states replaced by their recorded states, or by the effective targets of their default transition when nothing is recorded.

find_lcca

findLCCA: the nearest proper ancestor of head that is compound (or the root) and has every state of tail as a descendant.

is_atomic

Whether a state is atomic: it has no child states (history children do not count).

is_in_final_state

isInFinalState: a compound state with an active final child, or a parallel state all of whose regions are in a final state.

name_match

Whether any of a transition’s descriptors matches the event name.

proper_ancestors

The proper ancestors of s from its parent upward, stopping before stop; with no stop, up to and including the root.

record_history

The history step of exitStates: for every state in the exit set with history children, record the active atomic descendants (deep) or active children (shallow).

remove_conflicting_transitions

removeConflictingTransitions: keep a transition unless its exit set intersects that of a transition kept earlier; a transition whose source descends from the earlier one’s source replaces it, otherwise the earlier one wins.

select_transitions

selectTransitions (with Some(event)) and selectEventlessTransitions (with None): visit the active atomic states in document order and, for each, take the first transition in document order on the state or its nearest ancestor that matches the event and whose condition holds; then remove conflicts. cond is called, in this order, for each candidate transition that has a condition, and answers whether it holds.

transition_domain

getTransitionDomain, using the precomputed domain when it does not depend on history.

transition_domains

The domain of every transition in ts, in order, under the history recorded so far.