diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy (COPIA DI SICUREZZA).als b/1.RASD/res/alloy/AlloyPowerEnjoy (COPIA DI SICUREZZA).als deleted file mode 100644 index d664f6c..0000000 --- a/1.RASD/res/alloy/AlloyPowerEnjoy (COPIA DI SICUREZZA).als +++ /dev/null @@ -1,364 +0,0 @@ -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 - - - - - - - - - - - - - - - - - - - - - diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy(DUPLICATO).als b/1.RASD/res/alloy/AlloyPowerEnjoy(DUPLICATO).als deleted file mode 100644 index bc09fc1..0000000 --- a/1.RASD/res/alloy/AlloyPowerEnjoy(DUPLICATO).als +++ /dev/null @@ -1,480 +0,0 @@ -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, - car : one Car - //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 Rent and Reservations -fact a { - all ren : Rent | one res : Reservation | ( (ren.userID = res.userID) and - (ren.carID = res.carID) and (ren.startTime = res.endTime) ) -} - -// Relation between RMSS and Reservation or Rent -fact relationBetweenRequests { - (all rm : RMSS | - ( - one res : Reservation | ( (rm.id = res.id) and (rm.userID = res.userID) - and (rm.carID = res.carID) and (rm.startTime = res.startTime) and - (rm.endTime = res.endTime) ) - ) - or - ( - one ren : Rent | ( (rm.id = ren.id) and (rm.userID = ren.userID) - and (rm.carID = ren.carID) and (rm.startTime = ren.startTime) and - (rm.endTime = ren.endTime) ) - ) - ) -} - - - - -fact b { - all ren : Rent | no res : Reservation | ren.id = res.id -} - - -fact c { - all res : Reservation | no ren : Rent | res.id = ren.id -} - - -// Relation between active requests (reservations or rents) 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 -} - -// Each user can have multiple expired requests (reservations or rents) -fact multipleExpiredRequests { - (all r : RMSS | r.status = EXPIRED implies - (one u : User | u.request = r)) -} - -// Relation between cars and active requests (reservations or rents) -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) -} - -// Users cannot hold the same reservation -// fact noDifferentUsersForTheSameReservation{ -// (all r : RMSS | no u1, u2 : User | u1 !) -//} - - -// USER -- > RENT : SAME MONEY SAVING OPTION - -// 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) -} -// When a car is RENTED the related RENT is ACTIVE -fact aRentedCarIsRelatedToAnActiveRent { - (all c : Car | c.status = INUSE implies - (one ren : Rent | c.id = ren.carID and ren.status = ACTIVE) and - (no res : Reservation | c.id = res.carID and res.status = ACTIVE) - ) -} - -fact anActiveRentIsRelatedToARentedCar { - (all ren : Rent | ren.status = ACTIVE implies - (one c : Car | ren.carID = c.id and c.status = INUSE) - ) -} - -// When a car is RESERVED the related RESERVATION is ACTIVE -fact aReservedCarIsRelatedToAnActiveReservation { - (all c : Car | c.status = RESERVED implies - (one res : Reservation | c.id = res.carID and res.status = ACTIVE) and - (no ren : Rent | c.id = ren.carID and ren.status = ACTIVE) - ) -} - -fact anActiveReservationIsRelatedToAReservedCar { - (all res : Reservation | res.status = ACTIVE implies - (one c : Car | res.carID = c.id and c.status = RESERVED) - ) -} - -// When a car is UNAVAILABLE, it cannot be RESERVED -fact noUnavailableReservedCar { - all c : Car | c.status = UNAVAILABLE implies - (no res : Reservation | res.status = ACTIVE and res.carID = c.id) -} - - -// When a car is AVAILABLE, it cannot be RENTED -fact noUnavailableRentedCar { - all c : Car | c.status = UNAVAILABLE implies - (no ren : Rent | ren.status = ACTIVE and ren.carID = c.id) -} - -// When a reservation is EXPIRED, it still remembers the reserved car -fact consistencyOfReservation { - (all res : Reservation | res.status = EXPIRED implies - (one c : Car | res.carID = c.id) - ) -} - -// When a rent is EXPIRED, it still remembers the rented car -fact consistencyOfRent { - (all ren : Rent | ren.status = EXPIRED implies - (one c : Car | ren.carID = c.id) - ) -} - - - - - - - - - - - - -// When a car is INUSE the related RENT is ACTIVE -// When a car is AVAILABLE -// When a car is UNAVAILABLE - - - - -//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 8 [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 8 [no counterexamplefound] - -// The number of the Reservation is greater or equal to the number of Rent -assert noRentWithoutReservation{ - all u : User | - #{res: Reservation | res.userID = u.id } >= #{ren : Rent | ren.userID = u.id} -} -//check noRentWithoutReservation for 3 - -assert z{ - #{rm : RMSS} >= #{res : Reservation} -} - -//check z for 8 - -assert zz{ - #{rm : RMSS} >= #{rn : Rent} -} - -//check zz for 3 - -assert zzz{ - #{res : Reservation} < #{req : RMSS} -} - -//check zzz for 2 - - - pred show {} - -run show for 4 but exactly 1 User, exactly 1 RMSS, exactly 2 Car - - - - - - - - - - - - - - - - - - - - - diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy.als b/1.RASD/res/alloy/AlloyPowerEnjoy.als index e13371d..deecc3d 100644 --- a/1.RASD/res/alloy/AlloyPowerEnjoy.als +++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als @@ -8,9 +8,8 @@ sig Float { leftPart : one Int, rightPart : one Int } { - leftPart > 0 - rightPart > 0 -} + rightPart >= 0 +} sig User { id : one Int, @@ -27,19 +26,19 @@ sig User { moneySavingOption : one Bool, request : set RMSS } { - id > 0 + id >= 0 } sig Car { id : one Int, plate : one Stringa, wCode : one Int, - ecs : one ECS, ads : one ADS, + location: one Location, status : one CarStatus } { - id > 0 - wCode > 0 + id >= 0 + wCode >= 0 } abstract sig RMSS { @@ -54,14 +53,15 @@ abstract sig RMSS { carPosition : one Stringa, mSavingOption : one Bool, car : one Car, - user : one User + user : one User, + events : set Event } { - id > 0 - startTime > 0 - endTime > 0 - endTime = none or endTime > 0 - userID > 0 - endTime > startTime + id >= 0 + startTime >= 0 + endTime >= 0 + endTime = none or endTime >= 0 + userID >= 0 + endTime >= startTime } sig Reservation extends RMSS {} @@ -70,45 +70,61 @@ sig Rent extends RMSS {} sig DeactivatedUser extends User {} -sig ECS { - id : one Int, -} { - id > 0 -} - sig ADS { id : one Int } { - id > 0 + id >= 0 } -sig ParkingArea { - id : one Int, - name : one Stringa, - availableCars : one Int, - car : set Car, - rechargingArea : set RechargingArea +abstract sig Event { + id : one Int, + status: one Stringa, + rmss: one RMSS } { - id > 0 - availableCars > 0 + id >= 0 } -sig City { - id : one Int, - name : one Stringa, - parkingArea : set ParkingArea +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 } { - id > 0 + id >= 0 + latitude.leftPart >= 0 + longitude.leftPart >= 0 } -sig RechargingArea { - id : one Int, +sig City extends Location { + name : one Stringa, + zipCode : one Int, + parArea : set ParkingArea +} { + zipCode > 0 +} + +sig ParkingArea extends Location { + availableCars : one Int, + rechargingArea : one RechargingArea +} { + availableCars >= 0 +} + +sig RechargingArea extends Location { plugs : one Int, - address : one Stringa, + ranking : one Int, + maxRadius : one Int, isSpecial : one Bool } { - id > 0 - plugs > 0 + plugs >= 0 + ranking >= 0 + maxRadius >= 0 } // ENUMS @@ -145,24 +161,18 @@ enum RequestStatus { // In any city there is at least a parking area fact atLeastAParkingArea { - #ParkingArea >= 1 + (all c : City | #c.parArea >= 1) } - // In any parking area there could be zero or more recharging area fact presenceOfRechargingArea { - #RechargingArea >= 0 + (all p : ParkingArea | #p.rechargingArea >= 0) } // In any parking area there could be zero or more cars fact presenceOfCars { - #Car >= 0 -} - -// No ECS with the same ID -fact noDuplicatedECS { - (no ecs1 , ecs2 : ECS | ecs1.id = ecs2.id and ecs1 != ecs2) + (all p : ParkingArea | #p.availableCars >= 0) } // No ADS with the same ID @@ -170,14 +180,10 @@ fact noDuplicatedADS { (no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2) } -// The same ECS cannot be used by two different Cars -fact theSameECSCannotBeUsedByDifferentCars { - no disj c1, c2 : Car | c1.ecs = c2.ecs -} // The same ADS cannot be used by two different Cars fact theSameADSCannotBeUsedByDifferentCars { - no disj c1, c2 : Car | c1.ads = c2.ads + (no disj c1, c2 : Car | c1.ads = c2.ads) } // No Duplicated Users diff --git a/1.RASD/res/alloy/seconda prova.als b/1.RASD/res/alloy/seconda prova.als deleted file mode 100644 index 5602701..0000000 --- a/1.RASD/res/alloy/seconda prova.als +++ /dev/null @@ -1,340 +0,0 @@ -module PowerEnjoy - -//SIG - -sig Stringa {} - -sig Float { - leftPart : one Int, - rightPart : one Int -} { - leftPart > 0 - rightPart > 0 -} - -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 Car { - id : one Int, - plate : one Stringa, - wCode : one Int, - ecs : one ECS, - ads : one ADS, - status : one CarStatus -} { - 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, - userPosition : one Stringa, - carPosition : one Stringa, - mSavingOption : one Bool, - car : one Car, - user : one User -} { - id > 0 - startTime > 0 - endTime > 0 - endTime = none or endTime > 0 - userID > 0 - endTime > startTime -} - -sig Reservation extends RMSS {} - -sig Rent extends RMSS {} - -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 -} - -// 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) -} - -// The same ECS cannot be used by two different Cars -fact theSameECSCannotBeUsedByDifferentCars { - no disj c1, c2 : Car | c1.ecs = c2.ecs -} - -// The same ADS cannot be used by two different Cars -fact theSameADSCannotBeUsedByDifferentCars { - no disj c1, c2 : Car | c1.ads = c2.ads -} - -// 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 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) -} - -// NONCANCELLAREOTIUCCIDO -fact noMultipleUserForTheSameRequest { - no disj u1, u2 : User | u1.request & u2.request != none -} - -// The same Request cannot be performed by two different User -fact noDifferentUserForTheSameRequest { - all r : RMSS | r in r.user.request -} - -// 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 *******/ -// 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 [no counterexamplefound] - -/******* WORKING *******/ -// 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 //[no counterexamplefound] - -/******* WORKING *******/ -//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 //[no counterexamplefound] - -/******* WORKING *******/ -//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 //[no counterexamplefound] - - - -pred show { - #User = 3 - #DeactivatedUser = 0 - #RMSS = 3 - #Car = 2 - #{ r : RMSS | r.status = ACTIVE} >= 2 - #{ r : Rent | r.status = ACTIVE} >= 1 -} - -run show for 3