SAFETY-95 review: test the stale-link and contradiction legs; refusal +1 only
checks / unit (pull_request) Successful in 32m34s
infra-pin / fresh (pull_request) Successful in 1s

F1: test_safety95 checks that a dropped draining battery is this rule's
(stale link, N=3, 4000 W: grid import 676 W vs base 786 W); kills R2.
F2: _charge_track tested directly with a contradicting drain (SAFETY-91's
pin as a floor against a closed pack); kills R3. Today a drain contradicts
only through a refusal; the clause stays, as a contradiction sends 0 W.
F3: a drain ends on a refusal only when the battery will not give
(refused > 0, as _held_back()); one that will not take still drains.
Tested both signs; kills R8.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
glenn schrooyen
2026-10-07 16:41:16 +02:00
co-authored by Claude Opus 5.5
parent 9c0314a826
commit 4707d37019
3 changed files with 47 additions and 4 deletions
@@ -28,8 +28,11 @@ only). On the cycle a drain ends:
4. Then the loop moves one slew step a cycle. 4. Then the loop moves one slew step a cycle.
A drain ends when its battery leaves DRAIN, is not live, its claims A drain ends when its battery leaves DRAIN, is not live, its claims
contradict, or it refuses (SAFETY-73's limit outranks the pin without a contradict, or it will not give (SAFETY-73's limit outranks the pin
contradiction, so the refusal is read from the battery). The end is kept without a contradiction, so the refusal is read from the battery; +1 only,
as `_held_back()`). Today a contradiction on a drain only arises through
a refusal; the clause stays because a contradiction sends A 0 W, which is
an end (tested directly). The end is kept
until the loop runs (a missed poll). A dropped draining battery is this until the loop runs (a missed poll). A dropped draining battery is this
rule's, not `_reseed_drop()`'s. Order in one cycle: drop/rejoin rule's, not `_reseed_drop()`'s. Order in one cycle: drop/rejoin
(SAFETY-96), charge end (SAFETY-93), drain end (this) last; each moves the (SAFETY-96), charge end (SAFETY-93), drain end (this) last; each moves the
+3 -2
View File
@@ -2448,7 +2448,8 @@ class Controller:
"""SAFETY-93, N>=2: a charge ends when its battery leaves CHARGE or can """SAFETY-93, N>=2: a charge ends when its battery leaves CHARGE or can
no longer be placed (stale link, refusal). Kept until the loop runs. no longer be placed (stale link, refusal). Kept until the loop runs.
SAFETY-95: a drain likewise; its refusal (SAFETY-73) outranks the pin SAFETY-95: a drain likewise; its refusal (SAFETY-73) outranks the pin
without a contradiction, so it is read from the battery.""" without a contradiction, so it is read from the battery (+1, will not
give; a battery that will not take still drains)."""
if len(self.inverters) < 2: if len(self.inverters) < 2:
return return
live = set(self.live_units()) live = set(self.live_units())
@@ -2457,7 +2458,7 @@ class Controller:
u = self.actuator_of("maintenance", inv) u = self.actuator_of("maintenance", inv)
if res.phase in now and u in live and not pre_resolve( if res.phase in now and u in live and not pre_resolve(
[c for c in claims if c.actuator == u]).contradiction \ [c for c in claims if c.actuator == u]).contradiction \
and not (res.phase == DRAIN and inv.refused): and not (res.phase == DRAIN and (inv.refused or 0) > 0):
now[res.phase].add(inv.name) now[res.phase].add(inv.name)
self._charge_ended |= self._charging_was - now[CHARGE] self._charge_ended |= self._charging_was - now[CHARGE]
self._charging_was = frozenset(now[CHARGE]) self._charging_was = frozenset(now[CHARGE])
+39
View File
@@ -37,6 +37,7 @@ logging.disable(logging.WARNING)
import opt11_identity as rig # noqa: E402 import opt11_identity as rig # noqa: E402
import safety79_identity as s79 # noqa: E402 import safety79_identity as s79 # noqa: E402
from app import main as app_main, packmode # noqa: E402 from app import main as app_main, packmode # noqa: E402
from app.arbiter import Claim, P_MAINTENANCE, P_SAFETY # noqa: E402
from app.main import Controller # noqa: E402 from app.main import Controller # noqa: E402
from app.maintenance import (CHARGE, DRAIN, DRAIN_TIMEOUT_MIN, # noqa: E402 from app.maintenance import (CHARGE, DRAIN, DRAIN_TIMEOUT_MIN, # noqa: E402
HOLD, IDLE, MaintResult) HOLD, IDLE, MaintResult)
@@ -332,6 +333,11 @@ _now, _old = _by[("complete", 3, 4000.0)]
check("N=3 at 4000 W: the others take A's share at once, as before (the " check("N=3 at 4000 W: the others take A's share at once, as before (the "
"site does not drop), so the grid does not import", "site does not drop), so the grid does not import",
_now["imp"] <= 50.0 and abs(_now["imp"] - _old["imp"]) <= 50.0) _now["imp"] <= 50.0 and abs(_now["imp"] - _old["imp"]) <= 50.0)
_now, _old = _by[("stale link", 3, 4000.0)]
check(f"⭐ stale link, N=3, 4000 W: a dropped draining battery is this "
f"rule's, not the link-drop reseed's, so the grid imports at least "
f"50 W less than base ({_now['imp']:.0f} W, base {_old['imp']:.0f})",
_now["imp"] <= _old["imp"] - 50.0)
# ============================================================================ # # ============================================================================ #
print("\n2. the peak guard still binds across a drain end") print("\n2. the peak guard still binds across a drain end")
@@ -498,6 +504,39 @@ check("no drain ended: nothing moves (the integrator either)",
_c._drain_tail, _c._settle, _c.grid = {A}, {}, -800.0 _c._drain_tail, _c._settle, _c.grid = {A}, {}, -800.0
check("the tail ends with A's settling (SAFETY-96's window)", check("the tail ends with A's settling (SAFETY-96's window)",
_c._drain_grid_w(AB) == -800.0 and _c._drain_tail == set()) _c._drain_grid_w(AB) == -800.0 and _c._drain_tail == set())
_UA, _UB = (_c.actuator_of("maintenance", i) for i in _c.inverters)
_drain = MaintResult(DRAIN, True, 2000.0, False, [])
def drain_ends(extra, refused=0):
"""`_charge_track` with A draining last cycle, its drain SET and the
claims `extra` on A: which drains it ends."""
_c._draining_was, _c._drain_ended = frozenset({A}), frozenset()
_c._charging_was, _c._charge_ended = frozenset(), frozenset()
_c.live_units = lambda: (_UA, _UB)
_c.inverters[0].refused = refused
try:
_c._charge_track([Claim.set("maintenance", P_MAINTENANCE, 2000.0,
actuator=_UA)] + extra, [_drain, _b])
finally:
del _c.live_units
_c.inverters[0].refused = 0
return set(_c._drain_ended)
_rating = [Claim.limit("device", P_SAFETY, -2500.0, 2500.0, actuator=_UA)]
check("a drain that still stands does not end (its rating binds, no "
"contradiction, no refusal)", drain_ends(_rating) == set())
check("a drain whose limits contradict ends: A is sent 0 W (SAFETY-91's "
"pin as a floor against a closed pack)",
drain_ends(_rating + [
Claim.limit("maintenance", P_MAINTENANCE, lo=2000.0, actuator=_UA),
Claim.limit("pack", P_SAFETY, hi=0.0, actuator=_UA)]) == {A})
check("a refusal ends a drain only if A will not give (+1); one that will "
"not take (-1) leaves the drain standing",
drain_ends(_rating, refused=1) == {A}
and drain_ends(_rating, refused=-1) == set())
_n1c = run(1, 1200.0, store=store(1), dur=4.0)[1] _n1c = run(1, 1200.0, store=store(1), dur=4.0)[1]
_n1c.target, _n1c.i_w, _n1c._drain_ended = 2000.0, 5.0, frozenset({A}) _n1c.target, _n1c.i_w, _n1c._drain_ended = 2000.0, 5.0, frozenset({A})
_n1c._reseed_drain_end([_pin], {A}) _n1c._reseed_drain_end([_pin], {A})