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
+3 -2
View File
@@ -2448,7 +2448,8 @@ class Controller:
"""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.
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:
return
live = set(self.live_units())
@@ -2457,7 +2458,7 @@ class Controller:
u = self.actuator_of("maintenance", inv)
if res.phase in now and u in live and not pre_resolve(
[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)
self._charge_ended |= self._charging_was - now[CHARGE]
self._charging_was = frozenset(now[CHARGE])