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

norentIfPaymentDenied to noRentIfPaymentUncertain

Browse Source
This commit is contained in:
Giulio De Pasquale 2017-01-22 16:42:03 +01:00
parent cf64a73bbf
commit 19dced1ec5
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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)
)
}