From ad3a7231e5db2f4c530e26f57616e7dadb164601 Mon Sep 17 00:00:00 2001
From: Giulio De Pasquale <giulio@depasquale.eu>
Date: Sun, 22 Jan 2017 16:21:50 +0100
Subject: [PATCH] noRentIfPaymentDenied and noPhantomResRent added

---
 1.RASD/res/alloy/AlloyPowerEnjoy.als | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy.als b/1.RASD/res/alloy/AlloyPowerEnjoy.als
index 7a25f90..ea403bc 100644
--- a/1.RASD/res/alloy/AlloyPowerEnjoy.als
+++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als
@@ -44,7 +44,7 @@ sig Car {
 abstract sig RMSS {
 		id : one Int,
 		startTime : one Int,
-		endTime : lone Int,
+		endTime : one Int,
 		cost : one Float,
 		status : one RequestStatus,
 		paymentStatus : one PaymentStatus,
@@ -194,7 +194,19 @@ fact noDuplicatedUser {
 		(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2) 
 }
 
+// A reservation and its associated rent have the same user
+fact noPhantomResRent {
+	(all c : Car |  c.status = INUSE implies
+		(no res : Reservation, ren : Rent | res.car = c and ren.car = c and res.user != ren.user)
+	)
+}
 
+// 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 ren : Rent | ren.car = c)
+	)
+}
 
 // No Users with NOTCONFIRMED Billing Information
 fact noUserWithNotConfirmedBilling {