From c0d534ebf2fed6eb5a2cded18fbc576de6812d3e Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Wed, 21 Oct 2026 11:17:18 +0000 Subject: [PATCH] Require a positive floor count Signed-off-by: Qian-Cheng-nju --- specifications/MultiCarElevator/Elevator.tla | 2 ++ 1 file changed, 2 insertions(+) diff --git a/specifications/MultiCarElevator/Elevator.tla b/specifications/MultiCarElevator/Elevator.tla index 62389aa5..233264e8 100644 --- a/specifications/MultiCarElevator/Elevator.tla +++ b/specifications/MultiCarElevator/Elevator.tla @@ -16,6 +16,8 @@ CONSTANTS Person, \* The set of all people using the elevator system Elevator, \* The set of all elevators FloorCount \* The number of floors serviced by the elevator system +ASSUME FloorCountIsPositive == FloorCount \in (Nat \ {0}) + VARIABLES PersonState, \* The state of each person ActiveElevatorCalls, \* The set of all active elevator calls ElevatorState \* The state of each elevator