diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy.als b/1.RASD/res/alloy/AlloyPowerEnjoy.als index 28b2a24..933172e 100644 --- a/1.RASD/res/alloy/AlloyPowerEnjoy.als +++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als @@ -201,9 +201,9 @@ fact noPhantomResRent { ) } -// No rent is possible if the reservation payment was denied -fact noRentIfPaymentDenied { - (all c : Car, res : Reservation| c.status = INUSE and res.car = c and res.paymentStatus = DENIED implies +// No rent is possible if the reservation payment was denied or pending +fact noRentIfPaymentUncertain { + (all c : Car, res : Reservation| c.status = INUSE and res.car = c and (res.paymentStatus = DENIED or res.paymentStatus = PENDING) implies (no ren : Rent | ren.car = c) ) }