module PowerEnjoy //SIG sig Stringa {} sig Float { leftPart : one Int, rightPart : one Int } { leftPart > 0 rightPart > 0 } sig Car { id : one Int, plate : one Stringa, wCode : one Int, ecs : one ECS, ads : one ADS, status : one CarStatus, request : set RMSS } { id > 0 wCode > 0 } abstract sig RMSS { id : one Int, startTime : one Int, endTime : lone Int, cost : one Float, status : one RequestStatus, paymentStatus : one PaymentStatus, userID : one Int, carID : one Int, userPosition : one Stringa, carPosition : one Stringa, reservation : lone Reservation, rent : lone Rent } { id > 0 startTime > 0 endTime = none or endTime > 0 userID > 0 carID > 0 endTime > startTime } sig Reservation extends RMSS { countDown : one Int } { countDown >= 0 } sig Rent extends RMSS { mSavingOptionActived : one Bool } 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 } { id > 0 } sig DeactivatedUser extends User {} sig ECS { id : one Int, } { id > 0 } sig ADS { id : one Int } { id > 0 } sig ParkingArea { id : one Int, name : one Stringa, availableCars : one Int, car : set Car, rechargingArea : set RechargingArea } { id > 0 availableCars > 0 } sig City { id : one Int, name : one Stringa, parkingArea : set ParkingArea } { id > 0 } sig RechargingArea { id : one Int, plugs : one Int, address : one Stringa, isSpecial : one Bool } { id > 0 plugs > 0 } // 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 { #ParkingArea >= 1 } // In any parking area there could be zero or more recharging area fact presenceOfRechargingArea { #RechargingArea >= 0 } // In any parking area there could be zero or more cars fact presenceOfCars { #Car >= 0 } // Relation between users and active requests (reservation or rent) fact atMaxOneActiveRequestForUser { (all u : User | lone r : RMSS | (u.request = r) and (r.userID = u.id) and (r.status = ACTIVE)) // Each user has at maximum an active request at time } // Relation between RMSS and reservation or rent fact relationBetweenRequests { (all rm : RMSS | (one res : Reservation | rm.id = res.id) or (one ren : Rent | rm.id = ren.id)) } // R fact a { all rn : Rent | one rs : Reservation | (rn.userID = rs.userID) and (rn.carID = rs.carID) and (rn.startTime = rs.endTime) } fact b { all rn : Rent | no rs : Reservation | rn.id = rs.id } fact c { all rs : Reservation | no rn : Rent | rs.id = rn.id } // Relation between active requests (reservation or rent) and users fact exactelyOneUserForActiveRequest { (all r : RMSS | r.status = ACTIVE implies (one u : User | u.request = r)) // Each active request belongs exactely to one user } // Relation between cars and active requests (reservation or rent) fact atMaxOneActiveRequestForCar { (all c : Car | lone r : RMSS | (c.request = r) and (r.status = ACTIVE)) // Each car has at maximum an active request at time } // Relation between active requests (reservation or rent) and car fact exactelyOneCarForActiveRequest { (all r : RMSS | r.status = ACTIVE implies (one c : Car | c.request = r)) // Each active request refers exactely to one car } // Relation between deactivated users and active requests (reservation or rent) fact noActiveRequestForDeactivatedUser { (no dU : DeactivatedUser | one r : RMSS | (dU.request = r) and (r.status = ACTIVE)) // No deactivated users can have an active request } // Relation between active requests (reservation or rent) and deactivated users fact noDeactivatedUserForActiveRequest { (all r : RMSS | r.status = ACTIVE implies (no dU : DeactivatedUser | dU.request = r)) // Each active request does not belong to any deactivated user } // 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) } // No users with NOTCONFIRMED billing information fact noUserWithNotConfirmedBilling { no u : User | u.billingInformation = NOTCONFIRMED } // No duplicated deactivated users fact noDuplicatedDeactivatedUser { (no du1 , du2 : DeactivatedUser | du1.id = du2.id and du1 != du2) and (no du1 , du2 : DeactivatedUser | du1.email = du2.email and du1 != du2) and (no du1 , du2 : DeactivatedUser | du1.SSN = du2.SSN and du1 != du2) and (no du1 , du2 : DeactivatedUser | du1.drivingLicence = du2.drivingLicence and du1 != du2) } // 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.carID = req2.carID and req1.startTime = req2.startTime and req1.endTime = req2.endTime and req1 != req2)) } fact noDuplicatedReservation{ (no res1 , res2 : Reservation | res1.id = res2.id and res1 != res2) and (no res1 , res2 : Reservation | (res1.userID = res2.userID and res1.carID = res2.carID and res1.startTime = res2.startTime and res1.endTime = res2.endTime and res1 != res2)) } fact noDuplicatedRent{ (no ren1 , ren2 : Rent | ren1.id = ren2.id and ren1 != ren2) and (no ren1 , ren2 : Rent | (ren1.userID = ren2.userID and ren1.carID = ren2.carID and ren1.startTime = ren2.startTime and ren1.endTime = ren2.endTime and ren1 != ren2)) } // 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) } // No ECS with the same ID fact noDuplicatedECS { no ecs1 , ecs2 : ECS | ecs1.id = ecs2.id and ecs1 != ecs2 } // No ADS with the same ID fact noDuplicatedADS { no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2 } // AVAILABLE car // When a request is active the status of the payment is pending fact pendingPaymentForActiveRequest { (all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING) } //ASSERTION // 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 2 // 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 2 // Same number of requests assert equalityOfRequestsAsReservationOrRent { #{rm : RMSS} = (#{rs : Reservation} + #{rn : Rent}) } // //check equalityOfRequestsAsReservationOrRent for 1 pred show {} run show for 1 but exactly 1 User, exactly 2 RMSS, exactly 1 Rent, exactly 1 Car