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