Automaton State Numbering¶
BoolMonitor exposes each LTLf automaton state as an integer id. The id is
appended to every agent's observation (RMConfig.temporally_extended), is part
of tabular Nash-Q state keys, and indexes counterfactual relabelling. A learned
policy is therefore only meaningful under the numbering it was trained with.
The hazard¶
flloat builds its DFA by iterating Python sets of formulas, so the integers it
assigns to states depend on the per-process hash seed (PYTHONHASHSEED, random
by default). The old id mapping sorted those integers, so for many formulas the
ids of non-initial states swap between processes. The initial state is always
id 0. Measured over 32 hash seeds:
| Formula | Numberings |
|---|---|
G !goal_reached, F guard_intruder_collision, G !guard_intruder_collision & G !collision_ever |
1 |
F goal_reached & G !collision_ever (Pursuit Classic intruders) |
2 |
Coins (!p_mismatched) U p_matched, Harvest (G !p_zapped) & (F p_apple), Territory role claim, Stag Hunt sustained stag |
2 per formula |
Training and evaluation inside one process always agreed, so every result
produced by a training job is self-consistent. The hazard appears only when a
checkpoint is evaluated in a new process: on 2026-09-30 re-evaluating Pursuit
Classic 2 hc_iql seed 0 gave guard successes 63 under hash seeds 0 and 1 and
84 (the training job's value) under hash seeds 2 and 3.
Canonical numbering¶
Monitors now number states breadth-first from the initial state, visiting
successors in the order of their printed guard expression
(monitor_state_numbering() == "canonical", the default). This does not
depend on the hash seed. numbering_fingerprint() returns a JSON-safe
signature (initial id, accepting ids, guarded transitions) and
BoolRewardWrapper.monitor_numbering_fingerprints() returns one per agent.
The legacy mapping remains available as "flloat", selected with
use_monitor_state_numbering("flloat") or the environment variable
PLTLF_MONITOR_STATE_NUMBERING=flloat (read at import). Checkpoint bundles
record monitor_state_numbering; bundles without the key predate the change
and were trained under a hash-seed-dependent flloat numbering.
Re-evaluating legacy checkpoints¶
A process-independent permutation mode reproduces any hash seed's flloat
numbering: flloat_numbering_permutations(formulas, hash_seed) runs a short
subprocess with that PYTHONHASHSEED and returns, per formula, the flloat id
of each canonical state; monitors built inside
use_monitor_state_numbering(permutation) then use exactly those ids
(state_numbering == "permutation"). Checkpoint re-evaluation uses this to
recover a legacy checkpoint's training numbering automatically, by replaying
the candidate classes on the training job's NashConv baseline rollouts; see
checkpoint re-evaluation.