sim: hostlife: declare-lost parks a return lane the lost target had begun (model 27)
Seed 96501 of 100,000: a target that had started its dirty return was declared lost; the rollback went on as a clean one and nothing parked moves/<host>/<rollback id>/ in the source's region.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+6
−0
internal/sim/hostlife/console_test.go+5 −0internal/sim/hostlife/rules_test.go+1 −0
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 5a37078bc..766382ad9 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -916,6 +916,11 @@ func (w *world) operator() { |
| keep = append(keep, o) |
| } |
| n.Obl = keep |
| + if owesReturn && n.Op.RollbackID != "" && on("lost-return-park") { |
| + // a return the lost target had begun: park its lane in the |
| + // source's region, after the lane's staging horizon (model 27) |
| + n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", w.now+stagingTTL+horizonH)) |
| + } |
| if owesEvidence { // a box that released already queued these |
| n.Obl = append(n.Obl, |
| w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", w.now+horizonH), |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 2cd9dbd42..f081a1b70 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -77,6 +77,7 @@ var allRules = []string{ |
| "revert-journal", // J-N11 |
| "rollback-journal", // R2-3 |
| "dirty-return", // INV-2 |
| + "lost-return-park", // rev 7 §7.10 (model 27): declare-lost parks a return lane the lost target had begun |
| "target-park", // R2-5/INV-10 |
| "abort-target-owner", // J-N13 |
| "timer-freeze", // J-N14 runner bookkeeping |