Enum Transition 

pub enum Transition {
    Delay {
        min: u32,
        max: Option<u32>,
    },
    Epsilon,
    Abort {
        leaf: LeafId,
        mode: AbortMode,
    },
    Match {
        actions: Vec<ActionId>,
    },
    LocalVarWrite {
        var: LocalVarId,
        value: LeafId,
    },
    LocalVarCopy {
        dst: LocalVarId,
        src: LocalVarId,
    },
    FirstMatchBegin {
        group: FirstMatchId,
    },
    FirstMatchEnd {
        group: FirstMatchId,
    },
    LocalVarStep {
        var: LocalVarId,
        delta: i64,
    },
    SubroutineCall {
        call: CallId,
        args: Vec<CallArg>,
    },
    EndPoint {
        point: EndPointId,
        flag: Option<LocalVarId>,
    },
    ClockSync {
        to: ClockId,
        strict: bool,
    },
}

One edge out of a ThreadStateId in a compiled automaton’s static transition table (plan §1.2/§1.4). This is the whole vocabulary a sequence/property tree compiles down to – every LRM operator (16.7’s concatenation, 16.9’s and/or/intersect/throughout/within/ first_match, 16.12’s property connectives, 17’s checker actions) is built from these shapes by a later task’s builder, not added as one of their own (T11’s first_match markers are the one exception: “earliest match” is a property of a whole evaluation attempt, which no path-local edge can express). Matched exhaustively wherever it is consumed (the first such site, Transition::kind_name below, exists precisely so a future variant added here without updating every consumer fails to compile, not silently mis-steps at runtime – ARCHITECTURE §7 item 9’s “every kind match shouts” discipline, applied to a workspace-local enum instead of a mirrored slang one).

Variants

Delay

A ##N/##[m:n] cycle delay (16.7) or a [*n:m]/[->n:m]/ [=n:m] repetition unrolled into a run of delay edges (16.9.2): this edge is only eligible once at least min ticks of the clock the thread is currently in (see ClockId) have elapsed since the automaton entered the state it leaves, and must be taken by max ticks (None = unbounded, the $ form) or the thread never gets another chance to – the engine (T9/T10) is the one enforcing that window, not this IR.

Fields

min: u32

max: Option<u32>

Epsilon

A same-tick edge: zero elapsed ticks, consumed instantly. Used unconditionally (a sequence concatenation boundary with a zero-width operand, 16.9.2.1’s empty-match rules, or any other place the builder needs to join two states with no delay and no condition) – but also, as of T9, paired with Edge::guard to model 16.9.1’s Boolean-leaf point-sample itself (“the expression is evaluated… over 1 clock tick”, which costs no ADDITIONAL elapsed time relative to the clock tick it is sampled on – the thing that advances time in a sequence is the ##/repetition operator between samples, not a sample’s own evaluation): see Edge’s own doc comment in vj-sim::sva::ir for why.

Abort

disable iff/property abort (16.12.14’s accept_on/reject_on/ sync_accept_on/sync_reject_on, and 16.6/16.15’s plain disable iff): evaluated every simulation time step against current (unsampled) values per 16.6, not gated on this edge’s own clock – the first tick leaf is true, the thread’s run is decided per mode without waiting for (or caring about) this edge’s own source/target states.

Fields

leaf: LeafId

mode: AbortMode

Match

This thread has reached its automaton’s accept state: schedule actions into the Reactive-region maturation queue (plan §1.4’s generalized MaturationQueue<ReportKind>, T2) rather than firing them inline – matches never fire synchronously with the Observed step that discovers them (16.4.1-style maturation, generalized).

Fields

actions: Vec<ActionId>

LocalVarWrite

A sequence match-item write (16.10/16.11): compute value (a compiled leaf, reused verbatim – 16.11 restricts match-item expressions to the same side-effect-free leaf shape 16.6 does, T5’s validation pass), cast it to var’s declared type (LocalVarDecl::cast) and store it into var’s slot of the thread’s frame before taking this edge. A compound assignment (v += e) is the same edge: its value leaf is the whole v + e, which reads v’s own slot (T13).

Fields

var: LocalVarId

value: LeafId

LocalVarCopy

A same-tick slot-to-slot copy (T13): dst takes src’s value, cast to dst‘s declared type, or becomes UNASSIGNED when src is. The edge exists for the two places 16.8.2/16.9 need a value to move between threads’ views of a variable without a leaf to compute it:

• an inout/output local formal argument, whose value is written back to the actual’s local variable when the instance’s match completes (16.8.2);
• the branching operators and/intersect (and their throughout/ within rewrites), whose second operand works on a SHADOW copy of every variable the first operand touches, copied in before the operands start and copied out afterwards for the variables that flow out only of the second operand (16.10, F.5.4). The two operands of the lockstep product share one frame, so without the shadow one operand’s write would be visible to the other.

Fields

dst: LocalVarId

src: LocalVarId

FirstMatchBegin

Start of a first_match(R) region (16.9.3, T11): zero elapsed ticks, like Epsilon, but the thread taking it is stamped with (group, current tick) – the tick R begins on.

first_match(R) keeps only R’s matches that END EARLIEST for a given beginning (Annex F.5.2: w |= first_match(R) iff w |= R and no proper prefix of w satisfies R). Whether a match is the earliest is a fact about EVERY thread of the region, not about one path, so it is decided against an attempt-wide table the engine keeps, keyed (group, begin tick) – see FirstMatchEnd. Nested and repeated regions carry one stamp each (every first_match in a tree has its own FirstMatchId, so stamps never collide).

Fields

group: FirstMatchId

FirstMatchEnd

End of a first_match(R) region: a thread reaching this edge has just produced a match of R that ended on the current tick. The engine looks (group, the tick this thread's group stamp holds) up in the attempt’s first-match table:

• absent: record the current tick as the earliest end, and take the edge;
• present and equal to the current tick: take the edge (several matches may end on that same earliest tick, and all of them are matches of first_match(R));
• present and EARLIER: the thread dies (a shorter match of R, from the same beginning, already exists).

The entry is recorded whether or not the thread’s continuation later succeeds: first_match(R) ##1 c discards the longer R matches even when the earliest one is followed by !c. Threads are stepped in tick order, so an earlier end tick is always seen before a later one. Taking this edge also drops the thread’s group stamp.

Fields

group: FirstMatchId

LocalVarStep

A sequence match-item increment/decrement (16.11, T14): var becomes var + delta (delta is +1 for x++/++x, -1 for x--/--x), cast to var’s declared type. It is a dedicated edge rather than a LocalVarWrite because the new value is a function of the variable alone: no compiled leaf is needed to compute it. A match item’s value is never observed (the statement form of x++ discards it), so pre- and post-forms are the same edge.

The variable must hold a value (16.10: an inc/dec reads it); the builder rejects every proof-of-unassigned and the interpreter fails the attempt with UnassignedRead for one it could not.

Fields

var: LocalVarId

delta: i64

SubroutineCall

A sequence match-item subroutine call (16.11, T14): at every nonempty end point of the sequence it is attached to, task or void function call is scheduled in the Reactive region (fire-and-forget: assertion evaluation neither waits on it nor receives anything back, and it runs even when a sequence this one is part of later fails). args is one entry per actual argument, in the formal order.

The edge is a same-tick, unguarded pass-through for the thread; its only effect is the call event the engine (T29) schedules. By-value arguments are the SAMPLED value of their leaf under the thread’s frame (consistent with the match that produced it); by-reference arguments are the actual itself, bound at call time. See CallArg.

Fields

call: CallId

args: Vec<CallArg>

EndPoint

The end point of another sequence instance (16.9.11, 16.13.5, 16.13.6): the value of inst.triggered / inst.matched for the instance Automaton::end_points[point].

The instance is evaluated INDEPENDENTLY of the thread that tests it: its automaton runs free, one attempt from every tick of its clock (“the result … does not depend upon the starting point of the match of its operand sequence”), and the instance has reached its end point on a tick when some attempt has a NONEMPTY match ending there (16.9.11: an empty match never activates the method). The runtime sets that status in the Observed region and it persists for the rest of the time step, so a thread reads a status that already includes the tick it is on. The edge takes no time.

• flag == None: the edge is a guard. A thread takes it only when the instance reached its end point, and forks once per DISTINCT frame an attempt matched with (16.10: “the thread evaluating the instance to which triggered is applied will fork”), copying the matching frame’s EndPoint::flow_out slots into its own. This is the application of the method as a whole maximal Boolean expression, the only one a local variable flows out of.
• flag == Some(slot): the application sits inside a larger expression (!s.triggered, a && s.triggered), so nothing flows out. The edge is not a guard: it stores 1/0 (the instance did / did not reach its end point on this tick) into the thread’s frame slot flag, and the leaf that holds the expression reads the slot where the application stands (a leaf reads its flags in the pre-order of the calls inside it, see the builder’s LeafLocals::end_flags).

For EndMethod::Matched the status is the instance’s own clock’s, held until the first tick of THIS automaton’s clock at or after the match: see EndMethod.

Fields

point: EndPointId

flag: Option<LocalVarId>

ClockSync

The clock change of a multiclocked sequence (16.13.1, sva T28): s1 ##1 s2 (strict) or s1 ##0 s2 (not strict) where s1 ends in one clock and s2 begins in another. The thread leaves the clock it is in and takes to:

• strict (##1): “the nearest strictly subsequent tick” of to – the first tick of to AFTER the instant the thread is at, even when the old clock’s tick is also one of to’s;
• not strict (##0): “the nearest possibly overlapping tick”: the first tick of to AT OR AFTER that instant, so no time passes when the two clocks tick together.

A fused edge pair would need the single-clock meaning of Delay{1,1} to be “one instant later”, which only holds when every instant is a tick; this edge is that statement made for the clocks involved. With no timeline (every instant a tick of every clock) it is a Delay{1,1} / Epsilon. The sequences either side must not admit the empty match (16.13.1: “a maximal singly clocked subsequence … shall admit only nonempty matches”), which the builder checks.

Fields

to: ClockId

strict: bool

Implementations

impl Transition

pub fn kind_name(&self) -> &'static str

A stable, short name per variant – this enum’s first exhaustive match site (module doc comment: no real consumer exists yet, so this is what keeps the “no wildcard arm” discipline load-bearing today instead of unchecked).

Trait Implementations

impl Clone for Transition

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Transition

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

Formats the value using the given formatter.

impl Eq for Transition

impl Hash for Transition

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Transition

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Transition