peperunas/swing2
1
0
Fork 0
Code Issues 3 Pull Requests Releases Wiki Activity

noEarlyRent added

Browse Source
This commit is contained in:
Giulio De Pasquale 2017-01-22 16:26:59 +01:00
parent ad3a7231e5
commit cf64a73bbf
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
1.RASD/res/alloy/AlloyPowerEnjoy.als
View File

@ -213,6 +213,12 @@ fact noUserWithNotConfirmedBilling {
no u : User | u.billingInformation = NOTCONFIRMED 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 // No Cities with the same ID
fact noDuplicatedCities { fact noDuplicatedCities {
no c1 , c2 : City | c1.id = c2.id and c1 != c2 no c1 , c2 : City | c1.id = c2.id and c1 != c2