From cf64a73bbf06784c2758c811846ddbec991b317f Mon Sep 17 00:00:00 2001
From: Giulio De Pasquale <giulio@depasquale.eu>
Date: Sun, 22 Jan 2017 16:26:59 +0100
Subject: [PATCH] noEarlyRent added

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

diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy.als b/1.RASD/res/alloy/AlloyPowerEnjoy.als
index ea403bc..28b2a24 100644
--- a/1.RASD/res/alloy/AlloyPowerEnjoy.als
+++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als
@@ -213,6 +213,12 @@ fact noUserWithNotConfirmedBilling {
 		no u : User | u.billingInformation = NOTCONFIRMED
 }
 
+// Every rent starts after every reservation
+fact noEarlyRent {
+	(all c : Car, res : Reservation, ren : Rent | c.status = INUSE and res.car = c and ren.car = c implies
+		ren.startTime >= res.endTime 
+	)
+}
 // No Cities with the same ID
 fact noDuplicatedCities {
 		no c1 , c2 : City | c1.id = c2.id and c1 != c2