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