ctmc_memory_gate.h File Reference

Host-aware memory pre-gate for SolverCTMC. More...

#include <cmath>
#include <sstream>
#include <string>

Include dependency graph for ctmc_memory_gate.h:

Go to the source code of this file.

Classes
struct	line::mc::CtmcGateResult
	The gate verdict, plus the message the caller reports either way. More...

Namespaces
namespace	line
namespace	line::mc

Functions
double	line::mc::ctmc_available_memory_bytes ()
	Available physical memory in bytes.
CtmcGateResult	line::mc::ctmc_memory_gate (double log_nstates, bool force=false, double safety_fraction=CTMC_DEFAULT_SAFETY_FRACTION)
	Decide whether a state space of log-size log_nstates can be solved here.

Variables
constexpr double	line::mc::CTMC_BYTES_PER_NZ = 16.0
	8 bytes of value plus 8 amortized for the index, per stored nonzero.
constexpr double	line::mc::CTMC_DEFAULT_SAFETY_FRACTION = 0.6
	Fraction of available memory the solver may target.
constexpr double	line::mc::CTMC_FALLBACK_ALPHA = CTMC_BYTES_PER_NZ * 8.0
	Fallback power-law coefficients, identical to MATLAB and Python.
constexpr double	line::mc::CTMC_FALLBACK_BETA = 1.3
constexpr double	line::mc::CTMC_FALLBACK_AVAIL_BYTES = 1.0 * 1024.0 * 1024.0 * 1024.0
	Conservative available-memory default when the host probe fails.

Detailed Description

Host-aware memory pre-gate for SolverCTMC.

Port of matlab/src/api/mc/ctmc_memory_gate.m, mirrored by the JAR (MemoryGuard.gate) and native Python (ctmc_memory_gate).

THE POLICY IS REFUSAL, NOT A WARNING. When the predicted peak exceeds the safe budget the solve is REFUSED with an error naming the two numbers, and only an explicit force downgrades that to a warning. A warning the caller can walk past is the wrong contract here: the failure mode it precedes is the OOM killer taking the whole process, which produces no diagnostic at all and, observed on 2026-08-01, took down five sessions and the terminal hosting them. Refusing costs the caller a re-run with another solver; not refusing costs it everything running on the machine.

MDD AND CFTP ARE NEVER GATED. Both are served by their own analyzers and return before any explicit-generator path, so the gate is not on their route. That exemption is load-bearing rather than incidental: mdd holds the reachable set in a decision diagram whose size is governed by the diagram's compression, not by the state count, so it routinely solves models this estimator scores at exp(200). Gating on explicit size would clamp exactly the method that exists to beat it. Keep any new non-explicit method on the same side of the gate.

The predictor is the power law of the reference, bytes = alpha * N^beta, evaluated in log space. MATLAB and Python calibrate alpha/beta once per host by profiling a sparse LU and cache the fit; this port uses the reference's FALLBACK coefficients unconditionally, which is the same branch those two take when calibration cannot run. That is deliberate: the fallback is the conservative end of the fitted range, it is deterministic across hosts and runs, and a gate that silently changes its verdict after a background profiling step is worse than one that is slightly pessimistic.

Definition in file ctmc_memory_gate.h.