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

noRentIfPaymentDenied and noPhantomResRent added

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

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

@ -44,7 +44,7 @@ sig Car {
abstract sig RMSS { abstract sig RMSS {
id : one Int, id : one Int,
startTime : one Int, startTime : one Int,
endTime : lone Int, endTime : one Int,
cost : one Float, cost : one Float,
status : one RequestStatus, status : one RequestStatus,
paymentStatus : one PaymentStatus, paymentStatus : one PaymentStatus,
@ -194,7 +194,19 @@ fact noDuplicatedUser {
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2) (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 // No Users with NOTCONFIRMED Billing Information
fact noUserWithNotConfirmedBilling { fact noUserWithNotConfirmedBilling {