| index c6f4f07a7..f46fe7b7b 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| @@ -21,6 +21,7 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start) |
| stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10) |
| strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10) |
| +create-choice-once missed no box-side effect precedes the serving CAS in this model, so a substituted executor leaves nothing behind; the rule's effect is the cancellation of a create whose box is gone (TestCreateNamesItsExecutorOnce fails under the mutation) |
| reloc-start-guard missed the chooser's §2 eligibility already excludes a target owing a park-local, a live source never owes one for the host it serves, and a whole-location chore cannot be pending in the region the host serves in (a move into it waits, CC11); TestRelocationStartGuardRefuses shows the refusal |
| reloc-exec-ack-barrier missed liveness in the sweep: without the barrier a target that never acknowledged is handed op.exec and the operation waits there instead; TestReplacementWithoutAcknowledgementHoldsEachTransition fails under the mutation (rev 4) |
| reloc-pin-reaches-release missed the release's step 2 already waits for the listing to show N, so in the sweep the pin's own check is never the first to see a short listing; TestPinNeverShortOfTheRelease hides the newest file after the release and fails under the mutation (rev 4) |
| @@ -33,6 +34,7 @@ reloc-drain-needs-writer missed liveness only (1b-next ruling 11): a never-woken |
| reloc-ack-before-pinning missed defence in depth (1b-next rev 4 N6): installing still waits for the barrier, so a replaced target that never acknowledged holds the operation at pinning instead of releasing; TestReplacedTargetAcknowledgesBeforePinning fails under the mutation |
| reloc-probe-attempts missed liveness only (ruling 19): uncounted attempts still end at the probe deadline; TestProbeAttemptsCountedBeforeTheyAreMade fails under the mutation |
| fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; TestStoppedBoxNeverFenced fails under the mutation |
| +reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does; TestL18NestedFailover fails under the mutation (no nested failover) |
| files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads; TestInstallAppliesThePinnedManifest lands the newer manifest between the pin and the install and fails under the mutation (rev 4) |
| reloc-abandoned-prepared missed the at-rest sweep, which 1b-next ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it; the operation's own park is the rule's effect, and TestAbandonedPreparedGenerationParked (both paths) fails under the mutation |
| reloc-stuck-refuses-admission missed the stuck operation's live source is still op.exec, so admitting its wake makes no second writer; the refusal keeps a stuck operation from running anything until the operator resolves it (ruling 9); TestStuckSourceRefusesAdmission fails under the mutation |
amadan