2017-01-11 11:27:49 +00:00
|
|
|
module PowerEnjoy
|
|
|
|
|
|
|
|
//SIG
|
|
|
|
|
|
|
|
sig Stringa {}
|
|
|
|
|
|
|
|
sig Float {
|
|
|
|
leftPart : one Int,
|
|
|
|
rightPart : one Int
|
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
rightPart >= 0
|
|
|
|
}
|
2017-01-11 11:27:49 +00:00
|
|
|
|
|
|
|
sig User {
|
|
|
|
id : one Int,
|
|
|
|
name : one Stringa,
|
|
|
|
surname : one Stringa,
|
|
|
|
email : one Stringa,
|
|
|
|
password : one Stringa,
|
|
|
|
phone : one Stringa,
|
|
|
|
address : one Stringa,
|
|
|
|
SSN : one Stringa,
|
|
|
|
verificationCode : one Stringa,
|
|
|
|
drivingLicence : one Stringa,
|
|
|
|
billingInformation: one BillingInformation,
|
|
|
|
moneySavingOption : one Bool,
|
|
|
|
request : set RMSS
|
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
id >= 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
sig Car {
|
|
|
|
id : one Int,
|
|
|
|
plate : one Stringa,
|
|
|
|
wCode : one Int,
|
|
|
|
ads : one ADS,
|
2017-01-22 11:19:00 +00:00
|
|
|
location: one Location,
|
2017-01-11 11:27:49 +00:00
|
|
|
status : one CarStatus
|
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
id >= 0
|
|
|
|
wCode >= 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
abstract sig RMSS {
|
|
|
|
id : one Int,
|
|
|
|
startTime : one Int,
|
2017-01-22 15:21:50 +00:00
|
|
|
endTime : one Int,
|
2017-01-11 11:27:49 +00:00
|
|
|
cost : one Float,
|
|
|
|
status : one RequestStatus,
|
|
|
|
paymentStatus : one PaymentStatus,
|
|
|
|
userID : one Int,
|
|
|
|
userPosition : one Stringa,
|
|
|
|
carPosition : one Stringa,
|
|
|
|
mSavingOption : one Bool,
|
|
|
|
car : one Car,
|
2017-01-22 11:19:00 +00:00
|
|
|
user : one User,
|
|
|
|
events : set Event
|
2017-01-11 11:27:49 +00:00
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
id >= 0
|
|
|
|
startTime >= 0
|
|
|
|
endTime >= 0
|
|
|
|
endTime = none or endTime >= 0
|
|
|
|
userID >= 0
|
|
|
|
endTime >= startTime
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
sig Reservation extends RMSS {}
|
|
|
|
|
|
|
|
sig Rent extends RMSS {}
|
|
|
|
|
|
|
|
sig DeactivatedUser extends User {}
|
|
|
|
|
2017-01-22 11:19:00 +00:00
|
|
|
sig ADS {
|
|
|
|
id : one Int
|
2017-01-11 11:27:49 +00:00
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
id >= 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
2017-01-22 11:19:00 +00:00
|
|
|
abstract sig Event {
|
|
|
|
id : one Int,
|
|
|
|
status: one Stringa,
|
|
|
|
rmss: one RMSS
|
2017-01-11 11:27:49 +00:00
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
id >= 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
2017-01-22 11:19:00 +00:00
|
|
|
sig Payment extends Event {}
|
|
|
|
|
|
|
|
sig Notification extends Event {
|
|
|
|
message: one Stringa
|
|
|
|
}
|
|
|
|
|
|
|
|
abstract sig Location {
|
|
|
|
id : one Int,
|
|
|
|
boundaries : set Int,
|
|
|
|
latitude : one Float,
|
|
|
|
longitude : one Float
|
2017-01-11 11:27:49 +00:00
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
id >= 0
|
|
|
|
latitude.leftPart >= 0
|
|
|
|
longitude.leftPart >= 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
2017-01-22 11:19:00 +00:00
|
|
|
sig City extends Location {
|
|
|
|
name : one Stringa,
|
|
|
|
zipCode : one Int,
|
|
|
|
parArea : set ParkingArea
|
2017-01-11 11:27:49 +00:00
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
zipCode > 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
2017-01-22 11:19:00 +00:00
|
|
|
sig ParkingArea extends Location {
|
|
|
|
availableCars : one Int,
|
|
|
|
rechargingArea : one RechargingArea
|
|
|
|
} {
|
|
|
|
availableCars >= 0
|
|
|
|
}
|
|
|
|
|
|
|
|
sig RechargingArea extends Location {
|
2017-01-11 11:27:49 +00:00
|
|
|
plugs : one Int,
|
2017-01-22 11:19:00 +00:00
|
|
|
ranking : one Int,
|
|
|
|
maxRadius : one Int,
|
2017-01-11 11:27:49 +00:00
|
|
|
isSpecial : one Bool
|
|
|
|
} {
|
2017-01-22 11:19:00 +00:00
|
|
|
plugs >= 0
|
|
|
|
ranking >= 0
|
|
|
|
maxRadius >= 0
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
// ENUMS
|
|
|
|
|
|
|
|
enum Bool {
|
|
|
|
TRUE,
|
|
|
|
FALSE
|
|
|
|
}
|
|
|
|
|
|
|
|
enum BillingInformation {
|
|
|
|
CONFIRMED,
|
|
|
|
NOTCONFIRMED
|
|
|
|
}
|
|
|
|
|
|
|
|
enum PaymentStatus {
|
|
|
|
ACCEPTED,
|
|
|
|
PENDING,
|
|
|
|
DENIED
|
|
|
|
}
|
|
|
|
|
|
|
|
enum CarStatus {
|
|
|
|
AVAILABLE,
|
|
|
|
RESERVED,
|
|
|
|
UNAVAILABLE,
|
|
|
|
INUSE
|
|
|
|
}
|
|
|
|
|
|
|
|
enum RequestStatus {
|
|
|
|
ACTIVE,
|
|
|
|
EXPIRED
|
|
|
|
}
|
|
|
|
|
|
|
|
// FACTS
|
|
|
|
|
|
|
|
// In any city there is at least a parking area
|
|
|
|
fact atLeastAParkingArea {
|
2017-01-22 11:19:00 +00:00
|
|
|
(all c : City | #c.parArea >= 1)
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
// In any parking area there could be zero or more recharging area
|
|
|
|
fact presenceOfRechargingArea {
|
2017-01-22 11:19:00 +00:00
|
|
|
(all p : ParkingArea | #p.rechargingArea >= 0)
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
// In any parking area there could be zero or more cars
|
|
|
|
fact presenceOfCars {
|
2017-01-22 11:19:00 +00:00
|
|
|
(all p : ParkingArea | #p.availableCars >= 0)
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
// No ADS with the same ID
|
|
|
|
fact noDuplicatedADS {
|
|
|
|
(no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2)
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
// The same ADS cannot be used by two different Cars
|
|
|
|
fact theSameADSCannotBeUsedByDifferentCars {
|
2017-01-22 11:19:00 +00:00
|
|
|
(no disj c1, c2 : Car | c1.ads = c2.ads)
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
// No Duplicated Users
|
|
|
|
fact noDuplicatedUser {
|
|
|
|
(no u1 , u2 : User | u1.id = u2.id and u1 != u2) and
|
|
|
|
(no u1 , u2 : User | u1.email = u2.email and u1 != u2) and
|
|
|
|
(no u1 , u2 : User | u1.SSN = u2.SSN and u1 != u2) and
|
|
|
|
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2)
|
|
|
|
}
|
|
|
|
|
2017-01-22 15:21:50 +00:00
|
|
|
// 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)
|
|
|
|
)
|
|
|
|
}
|
2017-01-11 11:27:49 +00:00
|
|
|
|
2017-01-22 15:42:03 +00:00
|
|
|
// 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
|
2017-01-22 15:21:50 +00:00
|
|
|
(no ren : Rent | ren.car = c)
|
|
|
|
)
|
|
|
|
}
|
2017-01-11 11:27:49 +00:00
|
|
|
|
|
|
|
// No Users with NOTCONFIRMED Billing Information
|
|
|
|
fact noUserWithNotConfirmedBilling {
|
|
|
|
no u : User | u.billingInformation = NOTCONFIRMED
|
|
|
|
}
|
|
|
|
|
2017-01-22 15:26:59 +00:00
|
|
|
// 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
|
|
|
|
)
|
|
|
|
}
|
2017-01-22 22:00:37 +00:00
|
|
|
|
2017-01-11 11:27:49 +00:00
|
|
|
// No Cities with the same ID
|
|
|
|
fact noDuplicatedCities {
|
|
|
|
no c1 , c2 : City | c1.id = c2.id and c1 != c2
|
|
|
|
}
|
|
|
|
|
|
|
|
// No Parking Areas with the same ID
|
|
|
|
fact noDuplicatedParkingAreas {
|
|
|
|
no pa1 , pa2 : ParkingArea | pa1.id = pa2.id and pa1 != pa2
|
|
|
|
}
|
|
|
|
|
|
|
|
// No Recharging Areas with the same ID
|
|
|
|
fact noDuplicatedRechargingAreas {
|
|
|
|
no ra1 , ra2 : RechargingArea | ra1.id = ra2.id and ra1 != ra2
|
|
|
|
}
|
|
|
|
|
|
|
|
// No Duplicated Requests
|
|
|
|
fact noDuplicatedRMSS {
|
|
|
|
(no req1 , req2 : RMSS | req1.id = req2.id and req1 != req2) and
|
|
|
|
(no req1, req2 : RMSS | req1.userID = req2.userID and
|
|
|
|
req1.car = req2.car and req1.startTime = req2.startTime
|
|
|
|
and req1.endTime = req2.endTime and req1 != req2)
|
|
|
|
}
|
|
|
|
|
|
|
|
// No Duplicated Cars
|
|
|
|
fact noDuplicatedCars {
|
|
|
|
(no c1 , c2 : Car | c1.id = c2.id and c1 != c2) and
|
|
|
|
(no c1 , c2 : Car | c1.plate = c2.plate and c1 != c2) and
|
|
|
|
(no c1 , c2 : Car | c1.wCode = c2.wCode and c1 != c2)
|
|
|
|
}
|
|
|
|
|
|
|
|
// When a car is RENTED the related RENT is ACTIVE and viceversa
|
|
|
|
fact aRentedCarIsRelatedToAnActiveRent {
|
|
|
|
(all c : Car | c.status = INUSE implies
|
|
|
|
(one ren : Rent | ren.car = c and ren.status = ACTIVE) and
|
|
|
|
(no res : Reservation | res.car = c and res.status = ACTIVE) )
|
|
|
|
and
|
|
|
|
(all ren : Rent | ren.status = ACTIVE implies
|
|
|
|
(one c : Car | ren.car = c and c.status = INUSE)
|
|
|
|
)
|
|
|
|
}
|
|
|
|
|
|
|
|
// When a car is RESERVED the related RESERVATION is ACTIVE and viceversa
|
|
|
|
fact aReservedCarIsRelatedToAnActiveReservation {
|
|
|
|
(all c : Car | c.status = RESERVED implies
|
|
|
|
(one res : Reservation | res.car = c and res.status = ACTIVE) and
|
|
|
|
(no ren : Rent | ren.car = c and ren.status = ACTIVE)
|
|
|
|
) and
|
|
|
|
(all res : Reservation | res.status = ACTIVE implies
|
|
|
|
(one c : Car | res.car = c and c.status = RESERVED)
|
|
|
|
)
|
|
|
|
}
|
|
|
|
|
|
|
|
// When a car is UNAVAILABLE, it cannot be RESERVED nor RENTED
|
|
|
|
fact noUnavailableReservedCar {
|
|
|
|
all c : Car | c.status = UNAVAILABLE implies (
|
|
|
|
(no res : Reservation | res.status = ACTIVE and res.car = c) and
|
|
|
|
(no ren : Rent | ren.status = ACTIVE and ren.car = c)
|
|
|
|
)
|
|
|
|
}
|
|
|
|
|
|
|
|
// When a request is ACTIVE the status of the payment is PENDING
|
|
|
|
fact pendingPaymentForActiveRequest {
|
|
|
|
(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
|
|
|
|
}
|
|
|
|
|
2017-01-22 12:45:37 +00:00
|
|
|
// There are no duplicate payments
|
|
|
|
fact noDuplicatePayments {
|
|
|
|
(all r1, r2 : RMSS | r1 != r2 and r1.paymentStatus = PENDING and r2.paymentStatus = PENDING implies
|
|
|
|
(all p1, p2 : Payment | p1 != p2 and p1 in r1.events and p2 in r2.events)
|
|
|
|
)
|
|
|
|
}
|
2017-01-11 11:27:49 +00:00
|
|
|
// No Multiple Users for the same Request
|
|
|
|
fact noMultipleUsersForTheSameRequest {
|
|
|
|
no disj u1, u2 : User | u1.request & u2.request != none
|
|
|
|
}
|
|
|
|
|
|
|
|
// The same Request cannot be performed by two different User
|
|
|
|
fact noDifferentUserForTheSameRequest {
|
2017-01-22 15:55:06 +00:00
|
|
|
(all u1, u2 : User | u1 != u2 implies
|
|
|
|
(no r : RMSS | r in u1.request and r in u2.request)
|
|
|
|
)
|
2017-01-11 11:27:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
// The same User cannot have two ACTIVE Requests
|
|
|
|
fact theSameUserCannotPerformTwoActiveRequests {
|
|
|
|
no disj r1, r2 : RMSS | r1.user = r2.user and
|
|
|
|
r1.status = ACTIVE and r2.status = ACTIVE
|
|
|
|
}
|
|
|
|
|
|
|
|
// The same User cannot start two Request contemporary
|
|
|
|
fact noSimultaneousActions {
|
|
|
|
no disj r1, r2 : RMSS | r1.user = r2.user and r1.startTime = r2.startTime
|
|
|
|
}
|
|
|
|
|
|
|
|
// Relation between deactivated users and active requests (reservation or rent)
|
|
|
|
fact noActiveRequestForDeactivatedUser {
|
|
|
|
(all dU : DeactivatedUser | no r : dU.request | (r.status = ACTIVE))
|
|
|
|
// No deactivated users can have an active request
|
|
|
|
}
|
|
|
|
|
|
|
|
//Consistency of the MoneySavingOption for the ACTIVE Requests
|
|
|
|
fact consistencyOfMoneySavingOptionForActiveRequests {
|
|
|
|
(all u : User | u.request.status = ACTIVE implies
|
|
|
|
u.moneySavingOption = u.request.mSavingOption)
|
|
|
|
}
|
|
|
|
|
|
|
|
// A Rent is possible only as a consequence of a Reservation
|
|
|
|
fact rentIsAPossibleConsequenceOfReservation{
|
|
|
|
(all r : Rent | one res : Reservation | res in r.user.request and
|
|
|
|
r.startTime = res.endTime and r.car = res.car)
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// ASSERTIONS
|
|
|
|
|
|
|
|
/******* WORKING *******/ //[no counterexamplefound]
|
|
|
|
// The number of active rents is equal to the number of cars in use
|
|
|
|
assert equalityOfRentedCarsAndActiveRents {
|
|
|
|
#{r : Rent | r.status = ACTIVE} = #{c : Car | c.status = INUSE}
|
|
|
|
}
|
|
|
|
// check equalityOfRentedCarsAndActiveRents for 10
|
|
|
|
|
|
|
|
/******* WORKING *******/ //[no counterexamplefound]
|
|
|
|
// The number of active reservations is equal to the number of cars reserved
|
|
|
|
assert equalityOfReservedCarsAndActiveReservations {
|
|
|
|
#{r : Reservation | r.status = ACTIVE} = #{c : Car | c.status = RESERVED}
|
|
|
|
}
|
|
|
|
// check equalityOfReservedCarsAndActiveReservations for 10
|
|
|
|
|
|
|
|
/******* WORKING *******/ //[no counterexamplefound]
|
|
|
|
//The number of the Reservation is greater or equal to the number of Rent
|
|
|
|
assert noRentWithoutReservation {
|
|
|
|
all u : User |
|
|
|
|
#{res: Reservation | res.user = u } >= #{ren : Rent | ren.user = u}
|
|
|
|
}
|
|
|
|
// check noRentWithoutReservation for 10
|
|
|
|
|
|
|
|
/******* WORKING *******/ //[no counterexamplefound]
|
|
|
|
//If there is an end time for a Reservation, that must be after the start
|
|
|
|
assert requestTimeConsistency {
|
|
|
|
all r : RMSS | r.endTime > 0 implies r.endTime > r.startTime
|
|
|
|
}
|
|
|
|
// check requestTimeConsistency for 10
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
pred show {
|
|
|
|
#User >= 2
|
|
|
|
#DeactivatedUser = 1
|
|
|
|
#RMSS >= 2
|
|
|
|
#Car = 3
|
|
|
|
#{ r : RMSS | r.status = ACTIVE} >= 1
|
|
|
|
#{ r : Rent | r.status = ACTIVE} >= 1
|
|
|
|
}
|
|
|
|
|
|
|
|
run show for 3
|