Skip to content

Plasmoid-Merger Petri Net

MIF-012 implements a one-safe stochastic Petri net for the local FRC plasmoid-merger control contract:

approach -> contact -> reconnection -> coalescence -> phase_locked

Unsafe tilt growth or density asymmetry routes the net to the terminal abort sink. Every normal transition consumes the single active token and produces one token in the next place, so the marking remains one-safe. The matching Lean proof surface records the finite one-token marking invariant, transition preservation, terminal stability, and nominal reachability to phase_locked.

Delay fields are discrete sampled tick counts, not continuous dwell times. Python rejects fractional or boolean delay values before coercion; Rust/PyO3 accepts only integer tick-count arguments. This keeps the Python reference, Rust runtime, and CONTROL topology export aligned on the same sampled Petri-net semantics.

Guards

From To Guard
approach contact axial separation at or below contact_separation_m and closing speed above threshold
contact reconnection normalised reconnection flux reaches reconnection_flux_min for the configured delay
reconnection coalescence density asymmetry is inside the coalescence window for the configured delay
coalescence phase_locked phase-lock error and axial separation are inside their tolerances for the configured delay
any non-terminal place abort tilt growth or density asymmetry exceeds the abort envelope

The SCPN-CONTROL export mirrors terminal stability by attaching both terminal places, phase_locked and abort, as inhibitor arcs to every transition. This keeps the CONTROL topology absorbing after either terminal sink is marked.

Python API

plasmoid_merger_petri_net

One-safe stochastic Petri net for FRC plasmoid merger dynamics.

MIF-012 models the control-state progression for a two-plasmoid FRC merge: approach, contact, reconnection, coalescence, and phase lock. The local carrier keeps the MIF-specific guard thresholds here while preserving a constructor shim for the pinned SCPN-CONTROL StochasticPetriNet surface.

MergerPlace

Bases: StrEnum

Places in the MIF FRC plasmoid-merger Petri net.

MergerTransition

Bases: StrEnum

Transitions in the MIF FRC plasmoid-merger Petri net.

PlasmoidMergerSpec(contact_separation_m=0.002, min_closing_speed_m_s=300000.0, reconnection_flux_min=0.72, coalescence_density_asymmetry_max=0.12, phase_lock_tolerance_rad=0.01, max_tilt_growth_rate_s=50000.0, contact_delay_ticks=1, reconnection_delay_ticks=2, coalescence_delay_ticks=2, phase_lock_delay_ticks=3, firing_probability=1.0, abort_density_asymmetry_max=0.35) dataclass

Guard thresholds and stochastic firing policy for MIF-012.

__post_init__()

Validate Petri-net thresholds and abort limits.

MergerObservation(separation_m, relative_velocity_m_s, phase_lock_error_rad, reconnection_flux_norm, density_asymmetry, tilt_growth_rate_s) dataclass

Single sampled observation driving the merger Petri-net guards.

__post_init__()

Validate observed plasmoid-merger state scalars.

MergerMarking(tokens, total_tokens) dataclass

Token marking for the one-safe merger net.

max_tokens_per_place property

Return the maximum token count held by any place.

MergerTransitionRecord(tick, transition, from_place, to_place, reason) dataclass

Audit record for a fired merger transition.

MergerStep(tick, place, transition, fired, reason, dwell_ticks, marking) dataclass

Result of evaluating one sampled observation.

MergerVerificationReport(passed, trials, steps_per_trial, failures, terminal_counts, max_tokens_per_place) dataclass

Boundedness or liveness verification summary.

PlasmoidMergerPetriNet(spec, seed=None)

Stateful one-safe stochastic Petri net for MIF FRC merger control.

audit_log property

Return immutable fired-transition audit entries.

reset(seed=None)

Reset to the initial approach marking.

copy()

Return a copy with identical state and an independently seeded RNG.

marking()

Return the current one-safe marking.

enabled_transition(observation)

Return the transition currently enabled by observation.

step(observation)

Evaluate one sampled observation and fire at most one transition.

build_control_petri_net(spec, net_factory=None)

Build the pinned SCPN-CONTROL StochasticPetriNet shape for MIF-012.

verify_merger_boundedness(spec=None, *, trials=100, steps_per_trial=500, seed=0)

Run the requested stochastic boundedness campaign.

verify_merger_liveness(spec=None, *, trials=1000, steps_per_trial=200, seed=0)

Run the requested liveness campaign against nominal merger stimuli.

Dispatch

Use scpn_mif_core.lifecycle.dispatched_plasmoid_merger_petri_net(...) for the fastest available measured runtime backend:

"lifecycle.plasmoid_merger_petri_net" = ["rust", "python"]

The Python reference remains available for deterministic debugging and tests.

Verification

The committed MIF-012 tests cover:

  • nominal collision-to-phase-lock progression;
  • deterministic transition-delay behaviour for reconnection, coalescence, and final phase lock;
  • reset semantics with and without stochastic reseeding;
  • fail-closed validation of discrete integer delay ticks;
  • abort routing for unsafe tilt or density asymmetry;
  • CONTROL topology export with both terminal inhibitor arcs and the default pinned import path;
  • the required boundedness campaign (100 × 500);
  • explicit broken-marking detection in the boundedness verifier;
  • the required liveness campaign (1 000 × 200);
  • property-based one-safe marking preservation;
  • Lean one-token marking and nominal reachability proofs;
  • Python/Rust parity and dispatch fallback.

Benchmarks

Measured on the local i5-11600K rig using Python 3.12.3 and Rust 1.85.0. The result is a non-isolated local comparison, not a production latency claim.

Group Backend Mean Result
campaign_8 Rust 3.43 us fastest
campaign_8 Python 45.51 us 13.3x slower than Rust
boundedness_100x500 Rust 4.18 ms fastest
boundedness_100x500 Python 421.38 ms 100.8x slower than Rust

Raw summary: bench/results/plasmoid_merger_petri_net.json.

Ownership

SYNC-STATE: upstream-pending applies to all MIF-012 implementation surfaces. SCPN-MIF-CORE owns the local MIF-specific Petri-net guards until SCPN-CONTROL receives the reusable Petri-net runtime and merger-control surface.