feat(modelchecker): next_states() builtin for one-step ENABLED assert…

[jp-fizzbee]

…ions

Adds one-step lookahead to always assertions: next_states() returns the list of successor transitions from the state under check. Each entry is a struct:

transition(name, kind, role_ref, role_id, action_name, state)

• name: flat label ("Customer#0.PlaceOrder", "thread-0", "channel-0-message-1")
• kind: "action" | "thread" | "channel"
• role_ref: role instance label ("Customer#0"), None for non-role transitions
• role_id: the role's identity value (same as id) — compares by VALUE, so n.role_id == w.id scopes a check to a role instance. Role objects themselves compare by pointer and never match across clones, so the Role object is deliberately not exposed.
• action_name: bare action name. Named action_name/role_ref (not action/role) because those are fizz keywords and cannot appear in attribute position.
• state: successor heap vars at the first yield point — same struct shape as before/after in transition assertions.

This expresses TLA+ ENABLED-style safety properties with arbitrary quantifier nesting — e.g. "every item in the trash is restorable":

always assertion EveryTrashItemRestorable:
    for k in items:
        if items[k] == "trash":
            if len([n for n in next_states() if n.state.items[k] == "active"]) == 0:
                return False
    return True

The forall-item-exists-successor shape is not expressible with transition assertions, and a global-reachability exists formulation cannot catch ordering-restricted designs (stack-like trash where only the most recent deletion is restorable) — pinned by the 09-07 example.

Semantics:

• The probe (probeNextStates) IGNORES exploration bounds — max_actions depth, max_concurrent_actions, per-action caps. Enabledness is a property of the state, not the exploration schedule; without this, assertions would false-fail at the depth frontier and at states where in-flight non-atomic actions exhaust the concurrency cap (pinned by 09-08).
• Probe forks are throwaway: never attached, queued, or invariant-checked (no recursion). lib-level allocation counters (role refs, channel ids) are snapshotted/restored so discarded probe execution cannot shift ref numbering of real exploration.
• Crash variants are excluded from the successor set.
• Non-atomic actions: successor is the FIRST yield point; use name filtering for "can this serial action start".
• Intermediate-fork dedup happens AFTER Execute (mirrors processNode): sibling oneof forks share the parent's state until the choice binding runs; deduping at push time would collapse them (pinned by 09-06).
• Lazy + memoized; zero cost for specs that don't call it. Verified BFS, DFS, --experimental_processed_queue, --experimental_no_graph, and simulation. Unavailable in composition joins.

Also exposes id components to specs via new attrs on ModelValue (inherited by SymmetricValue): id.name -> "Worker", id.index -> 0. Previously the only option was parsing str(id) ("Worker0").

Docs: LANGUAGE_REFERENCE next_states() section; GOTCHAS #14 (role objects compare by pointer across states — compare id values; also applies to transition assertions' before/after) and #15 (keywords cannot be attribute names; multi-line comprehensions do not parse).

Reference examples: 09-06 (unrestricted restore, PASSES), 09-07 (stack trash, FAILS with assertion name), 09-08 (concurrency-cap false positive guard), 09-09 (role_id discrimination + id attrs).