From 19dced1ec53a29caada6e36a93a5262c541b46df Mon Sep 17 00:00:00 2001 From: Giulio De Pasquale Date: Sun, 22 Jan 2017 16:42:03 +0100 Subject: [PATCH] norentIfPaymentDenied to noRentIfPaymentUncertain --- 1.RASD/res/alloy/AlloyPowerEnjoy.als | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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) ) }