2.2 KiB
D05 原7領域の有限判断ケース（未承認）
全7領域の比較用入力と期待関係を整理する。試験実施・合格・正式独立レビュー・原成果完了を意味しない。fixture値を本番値に転記しない。閉店/勤務/EVの選択は保留する。
1 closing
入力: At the boundary, an active service has one minute remaining.
候補・不変条件: Choice A permits completion only if power/staff/related-facility guards hold; B preserves progress and reservation without completion payment. Manual and scheduled closure scope must be specified.
2 power
入力: A service and boarded elevator pair exist when reserve reaches zero.
候補・不変条件: No work completion or sale caused by the stopped interval; preserve identity. Owner chooses safe landing exception versus cabin holding; no fabricated teleport destination.
3 destruction
入力: A scheduled destruction precedes the final service interval.
候補・不変条件: Destroyed instance cannot complete service; release owned reservation at most once; later power recovery must not undo destruction.
4 departure
入力: Departure and service final interval occur in one tick.
候補・不変条件: Define eligible active versus queued departure. One reservation has one consume or release result, no orphan and no double payment; do not invent a new paid-refund policy.
5 charging
入力: The same completion ID is replayed after save/resume.
候補・不変条件: Same payment identity must not add a second ledger transaction, wallet debit, consumed inventory or completion notification.
6 shift
入力: Day staff leaves at 18:00 and night staff is not yet physically present.
候補・不変条件: Choice A settles the actual preceding interval then forbids new work without night attendance; B applies shift removal first and holds progress. No stale daytime attendance may start new work.
7 midnight
入力: A paid service reaches completion at 00:00 after the daily-close phase.
候補・不変条件: Under observed ordering, closed period excludes the sale timestamp and next-day ledger contains it once. Any changed ordering needs explicit approval; same daily-close ID may not settle payroll/upkeep twice.