1.RASD/res/alloy/AlloyPowerEnjoy (COPIA DI SICUREZZA).als

@@ -0,0 +1,364 @@
+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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

1.RASD/res/alloy/AlloyPowerEnjoy(DUPLICATO).als

@@ -0,0 +1,480 @@
+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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

1.RASD/res/alloy/AlloyPowerEnjoy.als

@@ -8,8 +8,9 @@ sig Float {
 		leftPart : one Int,
 		rightPart : one Int
 } {
-		rightPart >= 0
+		leftPart > 0
-} 
+		rightPart > 0
+}
 
 sig User {
 		id : one Int,
@@ -26,25 +27,25 @@ 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
+		id > 0
-		wCode >= 0
+		wCode > 0
 }
 
 abstract sig RMSS {
 		id : one Int,
 		startTime : one Int,
-		endTime : one Int,
+		endTime : lone Int,
 		cost : one Float,
 		status : one RequestStatus,
 		paymentStatus : one PaymentStatus,
@@ -53,15 +54,14 @@ abstract sig RMSS {
 		carPosition : one Stringa,
 		mSavingOption : one Bool,
 		car : one Car,
-		user : one User,
+		user : one User
-		events : set Event
 } {
-		id >= 0
+		id > 0
-		startTime >= 0
+		startTime > 0
-		endTime >= 0
+		endTime > 0
-		endTime = none or endTime >= 0
+		endTime = none or endTime > 0
-		userID >= 0
+		userID > 0
-		endTime >= startTime
+		endTime > startTime
 }
 
 sig Reservation extends RMSS {}
@@ -70,61 +70,45 @@ sig Rent extends RMSS {}
 
 sig DeactivatedUser extends User {}
 
+sig ECS {
+		id : one Int,
+} {
+		id > 0
+}
+
 sig ADS {
 		id : one Int
 } {
-		id >= 0
+		id > 0
 }
 
-abstract sig Event {
+sig ParkingArea {
-	id : one Int,
+		id : one Int,
-	status: one Stringa,
+		name : one Stringa,
-	rmss: one RMSS
+		availableCars : one Int,
+		car : set Car,
+		rechargingArea : set RechargingArea
 } {
-	id >= 0
+		id > 0
+		availableCars > 0
 }
 
-sig Payment extends Event {}
+sig City {
-
+		id : one Int,
-sig Notification extends Event {
+		name : one Stringa,
-	message: one Stringa
+		parkingArea : set ParkingArea
-}
-
-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 City extends Location {
+sig RechargingArea {
-	name : one Stringa,
+		id : one Int,
-	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,
-		ranking : one Int,
+		address : one Stringa,
-		maxRadius : one Int,
 		isSpecial : one Bool
 } {
-		plugs >= 0
+		id > 0
-		ranking >= 0
+		plugs > 0
-		maxRadius >= 0
 }
 
 // ENUMS
@@ -161,18 +145,24 @@ enum RequestStatus {
 
 //  In any city there is at least a parking area
 fact atLeastAParkingArea {
-		(all c : City | #c.parArea >=  1)
+		#ParkingArea >=  1
 }
 
 
+
 //  In any parking area there could be zero or more recharging area
 fact presenceOfRechargingArea {
-		(all p : ParkingArea | #p.rechargingArea >=  0)
+		#RechargingArea >=  0
 }
 
 //  In any parking area there could be zero or more cars
 fact presenceOfCars {
-		(all p : ParkingArea | #p.availableCars >= 0)
+		#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
@@ -180,10 +170,14 @@ 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
@@ -194,32 +188,13 @@ fact noDuplicatedUser {
 		(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 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 
-		(no ren : Rent | ren.car = c)
-	)
-}
 
 // No Users with NOTCONFIRMED Billing Information
 fact noUserWithNotConfirmedBilling {
 		no u : User | u.billingInformation = NOTCONFIRMED
 }
 
-// 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 
-	)
-}
-
 // No Cities with the same ID
 fact noDuplicatedCities {
 		no c1 , c2 : City | c1.id = c2.id and c1 != c2
@@ -285,12 +260,6 @@ fact pendingPaymentForActiveRequest {
 		(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
 }
 
-// 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)	
-	)
-}
 // No Multiple Users for the same Request
 fact  noMultipleUsersForTheSameRequest {
 		 no disj u1, u2 : User | u1.request & u2.request != none
@@ -298,9 +267,7 @@ fact  noMultipleUsersForTheSameRequest {
 
 // The same Request cannot be performed by two different User
 fact noDifferentUserForTheSameRequest {
-		(all u1, u2 : User | u1 != u2 implies
+		all r : RMSS | r in r.user.request
-			(no r : RMSS | r in u1.request and r in u2.request)
-		)
 }
 
 // The same User cannot have two ACTIVE Requests

1.RASD/res/alloy/seconda prova.als

@@ -0,0 +1,340 @@
+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

5.Code Inspection/src/ProductConfigItemContentWrapper.java

@@ -1,200 +0,0 @@
-/*******************************************************************************
- * Licensed to the Apache Software Foundation (ASF) under one
- * or more contributor license agreements.  See the NOTICE file
- * distributed with this work for additional information
- * regarding copyright ownership.  The ASF licenses this file
- * to you under the Apache License, Version 2.0 (the
- * "License"); you may not use this file except in compliance
- * with the License.  You may obtain a copy of the License at
- *
- * http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing,
- * software distributed under the License is distributed on an
- * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
- * KIND, either express or implied.  See the License for the
- * specific language governing permissions and limitations
- * under the License.
- *******************************************************************************/
-package org.apache.ofbiz.product.config;
-
-import java.io.IOException;
-import java.io.StringWriter;
-import java.io.Writer;
-import java.util.HashMap;
-import java.util.Locale;
-import java.util.Map;
-
-import javax.servlet.http.HttpServletRequest;
-
-import org.apache.ofbiz.base.util.Debug;
-import org.apache.ofbiz.base.util.GeneralException;
-import org.apache.ofbiz.base.util.StringUtil;
-import org.apache.ofbiz.base.util.StringUtil.StringWrapper;
-import org.apache.ofbiz.base.util.UtilCodec;
-import org.apache.ofbiz.base.util.UtilHttp;
-import org.apache.ofbiz.base.util.UtilValidate;
-import org.apache.ofbiz.base.util.cache.UtilCache;
-import org.apache.ofbiz.content.content.ContentWorker;
-import org.apache.ofbiz.content.content.ContentWrapper;
-import org.apache.ofbiz.entity.Delegator;
-import org.apache.ofbiz.entity.DelegatorFactory;
-import org.apache.ofbiz.entity.GenericValue;
-import org.apache.ofbiz.entity.model.ModelEntity;
-import org.apache.ofbiz.entity.model.ModelUtil;
-import org.apache.ofbiz.entity.util.EntityQuery;
-import org.apache.ofbiz.entity.util.EntityUtilProperties;
-import org.apache.ofbiz.service.LocalDispatcher;
-import org.apache.ofbiz.service.ServiceContainer;
-
-/**
- * Product Config Item Content Worker: gets product content to display
- */
-public class ProductConfigItemContentWrapper implements ContentWrapper {
-
-    public static final String module = ProductConfigItemContentWrapper.class.getName();
-    public static final String SEPARATOR = "::";    // cache key separator
-    private static final UtilCache<String, String> configItemContentCache = UtilCache.createUtilCache("configItem.content", true); // use soft reference to free up memory if needed
-
-    protected transient LocalDispatcher dispatcher;
-    protected String dispatcherName;
-    protected transient Delegator delegator;
-    protected String delegatorName;
-    protected GenericValue productConfigItem;
-    protected Locale locale;
-    protected String mimeTypeId;
-
-
-    public static ProductConfigItemContentWrapper makeProductConfigItemContentWrapper(GenericValue productConfigItem, HttpServletRequest request) {
-        return new ProductConfigItemContentWrapper(productConfigItem, request);
-    }
-
-    public ProductConfigItemContentWrapper(LocalDispatcher dispatcher, GenericValue productConfigItem, Locale locale, String mimeTypeId) {
-        this.dispatcher = dispatcher;
-        this.dispatcherName = dispatcher.getName();
-        this.delegator = productConfigItem.getDelegator();
-        this.delegatorName = delegator.getDelegatorName();
-        this.productConfigItem = productConfigItem;
-        this.locale = locale;
-        this.mimeTypeId = mimeTypeId;
-    }
-
-    public ProductConfigItemContentWrapper(GenericValue productConfigItem, HttpServletRequest request) {
-        this.dispatcher = (LocalDispatcher) request.getAttribute("dispatcher");
-        this.dispatcherName = dispatcher.getName();
-        this.delegator = (Delegator) request.getAttribute("delegator");
-        this.delegatorName = delegator.getDelegatorName();
-        this.productConfigItem = productConfigItem;
-        this.locale = UtilHttp.getLocale(request);
-        this.mimeTypeId = EntityUtilProperties.getPropertyValue("content", "defaultMimeType", "text/html; charset=utf-8", this.delegator);
-    }
-
-    public StringWrapper get(String confItemContentTypeId, String encoderType) {
-        return StringUtil.makeStringWrapper(getProductConfigItemContentAsText(productConfigItem, confItemContentTypeId, locale, mimeTypeId, getDelegator(), getDispatcher(), encoderType));
-    }
-
-    public Delegator getDelegator() {
-        if (delegator == null) {
-            delegator = DelegatorFactory.getDelegator(delegatorName);
-        }
-        return delegator;
-    }
-
-    public LocalDispatcher getDispatcher() {
-        if (dispatcher == null) {
-            dispatcher = ServiceContainer.getLocalDispatcher(dispatcherName, this.getDelegator());
-        }
-        return dispatcher;
-    }
-
-    public static String getProductConfigItemContentAsText(GenericValue productConfigItem, String confItemContentTypeId, HttpServletRequest request, String encoderType) {
-        LocalDispatcher dispatcher = (LocalDispatcher) request.getAttribute("dispatcher");
-        String mimeTypeId = EntityUtilProperties.getPropertyValue("content", "defaultMimeType", "text/html; charset=utf-8", productConfigItem.getDelegator());
-        return getProductConfigItemContentAsText(productConfigItem, confItemContentTypeId, UtilHttp.getLocale(request), mimeTypeId, productConfigItem.getDelegator(), dispatcher, encoderType);
-    }
-
-    public static String getProductConfigItemContentAsText(GenericValue productConfigItem, String confItemContentTypeId, Locale locale, LocalDispatcher dispatcher, String encoderType) {
-        return getProductConfigItemContentAsText(productConfigItem, confItemContentTypeId, locale, null, null, dispatcher, encoderType);
-    }
-
-    public static String getProductConfigItemContentAsText(GenericValue productConfigItem, String confItemContentTypeId, Locale locale, String mimeTypeId, Delegator delegator, LocalDispatcher dispatcher, String encoderType) {
-        UtilCodec.SimpleEncoder encoder = UtilCodec.getEncoder(encoderType);
-        String candidateFieldName = ModelUtil.dbNameToVarName(confItemContentTypeId);
-        String cacheKey = confItemContentTypeId + SEPARATOR + locale + SEPARATOR + mimeTypeId + SEPARATOR + productConfigItem.get("configItemId") + SEPARATOR + encoderType + SEPARATOR + delegator;
-        try {
-            String cachedValue = configItemContentCache.get(cacheKey);
-            if (cachedValue != null) {
-                return cachedValue;
-            }
-            Writer outWriter = new StringWriter();
-            getProductConfigItemContentAsText(null, productConfigItem, confItemContentTypeId, locale, mimeTypeId, delegator, dispatcher, outWriter, false);
-            String outString = outWriter.toString();
-            if (UtilValidate.isEmpty(outString)) {
-                outString = productConfigItem.getModelEntity().isField(candidateFieldName) ? productConfigItem.getString(candidateFieldName): "";
-                outString = outString == null? "" : outString;
-            }
-            outString = encoder.sanitize(outString);
-            if (configItemContentCache != null) {
-                configItemContentCache.put(cacheKey, outString);
-            }
-            return outString;
-        } catch (GeneralException e) {
-            Debug.logError(e, "Error rendering ProdConfItemContent, inserting empty String", module);
-            String candidateOut = productConfigItem.getModelEntity().isField(candidateFieldName) ? productConfigItem.getString(candidateFieldName): "";
-            return candidateOut == null? "" : encoder.sanitize(candidateOut);
-        } catch (IOException e) {
-            Debug.logError(e, "Error rendering ProdConfItemContent, inserting empty String", module);
-            String candidateOut = productConfigItem.getModelEntity().isField(candidateFieldName) ? productConfigItem.getString(candidateFieldName): "";
-            return candidateOut == null? "" : encoder.sanitize(candidateOut);
-        }
-    }
-
-    public static void getProductConfigItemContentAsText(String configItemId, GenericValue productConfigItem, String confItemContentTypeId, Locale locale, String mimeTypeId, Delegator delegator, LocalDispatcher dispatcher, Writer outWriter) throws GeneralException, IOException {
-        getProductConfigItemContentAsText(configItemId, productConfigItem, confItemContentTypeId, locale, mimeTypeId, delegator, dispatcher, outWriter, true);
-    }
-
-    public static void getProductConfigItemContentAsText(String configItemId, GenericValue productConfigItem, String confItemContentTypeId, Locale locale, String mimeTypeId, Delegator delegator, LocalDispatcher dispatcher, Writer outWriter, boolean cache) throws GeneralException, IOException {
-        if (configItemId == null && productConfigItem != null) {
-            configItemId = productConfigItem.getString("configItemId");
-        }
-
-        if (delegator == null && productConfigItem != null) {
-            delegator = productConfigItem.getDelegator();
-        }
-
-        if (UtilValidate.isEmpty(mimeTypeId)) {
-            mimeTypeId = EntityUtilProperties.getPropertyValue("content", "defaultMimeType", "text/html; charset=utf-8", delegator);
-        }
-
-        GenericValue productConfigItemContent = EntityQuery.use(delegator).from("ProdConfItemContent")
-                .where("configItemId", configItemId, "confItemContentTypeId", confItemContentTypeId)
-                .orderBy("-fromDate")
-                .cache(cache)
-                .filterByDate()
-                .queryFirst();
-        if (productConfigItemContent != null) {
-            // when rendering the product config item content, always include the ProductConfigItem and ProdConfItemContent records that this comes from
-            Map<String, Object> inContext = new HashMap<String, Object>();
-            inContext.put("productConfigItem", productConfigItem);
-            inContext.put("productConfigItemContent", productConfigItemContent);
-            ContentWorker.renderContentAsText(dispatcher, delegator, productConfigItemContent.getString("contentId"), outWriter, inContext, locale, mimeTypeId, null, null, cache);
-            return;
-        }
-        
-        String candidateFieldName = ModelUtil.dbNameToVarName(confItemContentTypeId);
-        ModelEntity productConfigItemModel = delegator.getModelEntity("ProductConfigItem");
-        if (productConfigItemModel.isField(candidateFieldName)) {
-            if (productConfigItem == null) {
-                productConfigItem = EntityQuery.use(delegator).from("ProductConfigItem").where("configItemId", configItemId).cache().queryOne();
-            }
-            if (productConfigItem != null) {
-                String candidateValue = productConfigItem.getString(candidateFieldName);
-                if (UtilValidate.isNotEmpty(candidateValue)) {
-                    outWriter.write(candidateValue);
-                    return;
-                }
-            }
-        }
-    }
-}
-

5.Code Inspection/src/SeoTransform.java

@@ -1,189 +0,0 @@
-/*******************************************************************************
- * Licensed to the Apache Software Foundation (ASF) under one
- * or more contributor license agreements.  See the NOTICE file
- * distributed with this work for additional information
- * regarding copyright ownership.  The ASF licenses this file
- * to you under the Apache License, Version 2.0 (the
- * "License"); you may not use this file except in compliance
- * with the License.  You may obtain a copy of the License at
- *
- * http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing,
- * software distributed under the License is distributed on an
- * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
- * KIND, either express or implied.  See the License for the
- * specific language governing permissions and limitations
- * under the License.
- *******************************************************************************/
-package org.apache.ofbiz.product.category.ftl;
-
-import java.io.IOException;
-import java.io.Writer;
-import java.util.Iterator;
-import java.util.Map;
-
-import javax.servlet.ServletContext;
-import javax.servlet.http.HttpServletRequest;
-import javax.servlet.http.HttpServletResponse;
-import javax.servlet.http.HttpSession;
-
-import org.apache.oro.text.regex.Pattern;
-import org.apache.oro.text.regex.Perl5Matcher;
-import org.apache.ofbiz.base.util.Debug;
-import org.apache.ofbiz.entity.GenericValue;
-import org.apache.ofbiz.product.category.SeoConfigUtil;
-import org.apache.ofbiz.webapp.control.RequestHandler;
-
-import freemarker.core.Environment;
-import freemarker.ext.beans.BeanModel;
-import freemarker.template.SimpleScalar;
-import freemarker.template.TemplateScalarModel;
-import freemarker.template.TemplateTransformModel;
-
-/**
- * SeoTransform - Freemarker Transform for URLs (links)
- * 
- */
-public class SeoTransform implements TemplateTransformModel {
-
-    private static final String module = SeoTransform.class.getName();
-
-    public boolean checkArg(Map args, String key, boolean defaultValue) {
-        if (!args.containsKey(key)) {
-            return defaultValue;
-        } else {
-            Object o = args.get(key);
-            if (o instanceof SimpleScalar) {
-                SimpleScalar s = (SimpleScalar) o;
-                return "true".equalsIgnoreCase(s.getAsString());
-            }
-            return defaultValue;
-        }
-    }
-
-    public Writer getWriter(final Writer out, Map args) {
-        final StringBuffer buf = new StringBuffer();
-        final boolean fullPath = checkArg(args, "fullPath", false);
-        final boolean secure = checkArg(args, "secure", false);
-        final boolean encode = checkArg(args, "encode", true);
-
-        return new Writer(out) {
-
-            public void write(char cbuf[], int off, int len) {
-                buf.append(cbuf, off, len);
-            }
-
-            public void flush() throws IOException {
-                out.flush();
-            }
-
-            public void close() throws IOException {
-                try {
-                    Environment env = Environment.getCurrentEnvironment();
-                    BeanModel req = (BeanModel) env.getVariable("request");
-                    BeanModel res = (BeanModel) env.getVariable("response");
-                    Object prefix = env.getVariable("urlPrefix");
-                    if (req != null) {
-                        HttpServletRequest request = (HttpServletRequest) req.getWrappedObject();
-                        ServletContext ctx = (ServletContext) request.getAttribute("servletContext");
-                        HttpServletResponse response = null;
-                        if (res != null) {
-                            response = (HttpServletResponse) res.getWrappedObject();
-                        }
-                        HttpSession session = request.getSession();
-                        GenericValue userLogin = (GenericValue) session.getAttribute("userLogin");
-
-                        // anonymous shoppers are not logged in
-                        if (userLogin != null && "anonymous".equals(userLogin.getString("userLoginId"))) {
-                            userLogin = null;
-                        }
-
-                        RequestHandler rh = (RequestHandler) ctx.getAttribute("_REQUEST_HANDLER_");
-                        out.write(seoUrl(rh.makeLink(request, response, buf.toString(), fullPath, secure, encode), userLogin == null));
-                    } else if (prefix != null) {
-                        if (prefix instanceof TemplateScalarModel) {
-                            TemplateScalarModel s = (TemplateScalarModel) prefix;
-                            String prefixString = s.getAsString();
-                            String bufString = buf.toString();
-                            boolean prefixSlash = prefixString.endsWith("/");
-                            boolean bufSlash = bufString.startsWith("/");
-                            if (prefixSlash && bufSlash) {
-                                bufString = bufString.substring(1);
-                            } else if (!prefixSlash && !bufSlash) {
-                                bufString = "/" + bufString;
-                            }
-                            out.write(prefixString + bufString);
-                        }
-                    } else {
-                        out.write(buf.toString());
-                    }
-                } catch (Exception e) {
-                    throw new IOException(e.getMessage());
-                }
-            }
-        };
-    }
-
-    /**
-     * Transform a url according to seo pattern regular expressions.
-     * 
-     * @param url , String to do the seo transform
-     * @param isAnon , boolean to indicate whether it's an anonymous visit.
-     * 
-     * @return String, the transformed url.
-     */
-    public static String seoUrl(String url, boolean isAnon) {
-        Perl5Matcher matcher = new Perl5Matcher();
-        if (SeoConfigUtil.checkUseUrlRegexp() && matcher.matches(url, SeoConfigUtil.getGeneralRegexpPattern())) {
-            Iterator<String> keys = SeoConfigUtil.getSeoPatterns().keySet().iterator();
-            boolean foundMatch = false;
-            while (keys.hasNext()) {
-                String key = keys.next();
-                Pattern pattern = SeoConfigUtil.getSeoPatterns().get(key);
-                if (pattern.getPattern().contains(";jsessionid=")) {
-                    if (isAnon) {
-                        if (SeoConfigUtil.isJSessionIdAnonEnabled()) {
-                            continue;
-                        }
-                    } else {
-                        if (SeoConfigUtil.isJSessionIdUserEnabled()) {
-                            continue;
-                        } else {
-                            boolean foundException = false;
-                            for (int i = 0; i < SeoConfigUtil.getUserExceptionPatterns().size(); i++) {
-                                if (matcher.matches(url, SeoConfigUtil.getUserExceptionPatterns().get(i))) {
-                                    foundException = true;
-                                    break;
-                                }
-                            }
-                            if (foundException) {
-                                continue;
-                            }
-                        }
-                    }
-                }
-                String replacement = SeoConfigUtil.getSeoReplacements().get(key);
-                if (matcher.matches(url, pattern)) {
-                    for (int i = 1; i < matcher.getMatch().groups(); i++) {
-                        replacement = replacement.replaceAll("\\$" + i, matcher.getMatch().group(i));
-                    }
-                    // break if found any matcher
-                    url = replacement;
-                    foundMatch = true;
-                    break;
-                }
-            }
-            if (!foundMatch) {
-                Debug.logVerbose("Can NOT find a seo transform pattern for this url: " + url, module);
-            }
-        }
-        return url;
-    }
-
-    static {
-        if (!SeoConfigUtil.isInitialed()) {
-            SeoConfigUtil.init();
-        }
-    }
-}

5.Code Inspection/src/UrlRegexpTransform.java

@@ -1,231 +0,0 @@
-/*******************************************************************************
- * Licensed to the Apache Software Foundation (ASF) under one
- * or more contributor license agreements.  See the NOTICE file
- * distributed with this work for additional information
- * regarding copyright ownership.  The ASF licenses this file
- * to you under the Apache License, Version 2.0 (the
- * "License"); you may not use this file except in compliance
- * with the License.  You may obtain a copy of the License at
- *
- * http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing,
- * software distributed under the License is distributed on an
- * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
- * KIND, either express or implied.  See the License for the
- * specific language governing permissions and limitations
- * under the License.
- *******************************************************************************/
-package org.apache.ofbiz.product.category.ftl;
-
-import java.io.IOException;
-import java.io.Writer;
-import java.util.Iterator;
-import java.util.Map;
-
-import javax.servlet.ServletContext;
-import javax.servlet.http.HttpServletRequest;
-import javax.servlet.http.HttpServletResponse;
-import javax.servlet.http.HttpSession;
-
-import org.apache.oro.text.regex.Pattern;
-import org.apache.oro.text.regex.Perl5Matcher;
-import org.apache.ofbiz.base.util.Debug;
-import org.apache.ofbiz.entity.GenericValue;
-import org.apache.ofbiz.product.category.SeoConfigUtil;
-import org.apache.ofbiz.webapp.control.RequestHandler;
-
-import freemarker.core.Environment;
-import freemarker.ext.beans.BeanModel;
-import freemarker.template.SimpleScalar;
-import freemarker.template.TemplateScalarModel;
-import freemarker.template.TemplateTransformModel;
-
-/**
- * UrlRegexpTransform - Freemarker Transform for Products URLs (links)
- * 
- */
-public class UrlRegexpTransform implements TemplateTransformModel {
-
-    private static final String module = UrlRegexpTransform.class.getName();
-
-    public boolean checkArg(Map args, String key, boolean defaultValue) {
-        if (!args.containsKey(key)) {
-            return defaultValue;
-        } else {
-            Object o = args.get(key);
-            if (o instanceof SimpleScalar) {
-                SimpleScalar s = (SimpleScalar) o;
-                return "true".equalsIgnoreCase(s.getAsString());
-            }
-            return defaultValue;
-        }
-    }
-
-    public Writer getWriter(final Writer out, Map args) {
-        final StringBuffer buf = new StringBuffer();
-        final boolean fullPath = checkArg(args, "fullPath", false);
-        final boolean secure = checkArg(args, "secure", false);
-        final boolean encode = checkArg(args, "encode", true);
-
-        return new Writer(out) {
-
-            public void write(char cbuf[], int off, int len) {
-                buf.append(cbuf, off, len);
-            }
-
-            public void flush() throws IOException {
-                out.flush();
-            }
-
-            public void close() throws IOException {
-                try {
-                    Environment env = Environment.getCurrentEnvironment();
-                    BeanModel req = (BeanModel) env.getVariable("request");
-                    BeanModel res = (BeanModel) env.getVariable("response");
-                    Object prefix = env.getVariable("urlPrefix");
-                    if (req != null) {
-                        HttpServletRequest request = (HttpServletRequest) req.getWrappedObject();
-                        ServletContext ctx = (ServletContext) request.getAttribute("servletContext");
-                        HttpServletResponse response = null;
-                        if (res != null) {
-                            response = (HttpServletResponse) res.getWrappedObject();
-                        }
-                        HttpSession session = request.getSession();
-                        GenericValue userLogin = (GenericValue) session.getAttribute("userLogin");
-
-                        // anonymous shoppers are not logged in
-                        if (userLogin != null && "anonymous".equals(userLogin.getString("userLoginId"))) {
-                            userLogin = null;
-                        }
-
-                        RequestHandler rh = (RequestHandler) ctx.getAttribute("_REQUEST_HANDLER_");
-                        out.write(seoUrl(rh.makeLink(request, response, buf.toString(), fullPath, secure || request.isSecure() , encode), userLogin == null));
-                    } else if (prefix != null) {
-                        if (prefix instanceof TemplateScalarModel) {
-                            TemplateScalarModel s = (TemplateScalarModel) prefix;
-                            String prefixString = s.getAsString();
-                            String bufString = buf.toString();
-                            boolean prefixSlash = prefixString.endsWith("/");
-                            boolean bufSlash = bufString.startsWith("/");
-                            if (prefixSlash && bufSlash) {
-                                bufString = bufString.substring(1);
-                            } else if (!prefixSlash && !bufSlash) {
-                                bufString = "/" + bufString;
-                            }
-                            out.write(prefixString + bufString);
-                        }
-                    } else {
-                        out.write(buf.toString());
-                    }
-                } catch (Exception e) {
-                    throw new IOException(e.getMessage());
-                }
-            }
-        };
-    }
-
-    /**
-     * Transform a url according to seo pattern regular expressions.
-     * 
-     * @param url
-     *            , String to do the seo transform
-     * @param isAnon
-     *            , boolean to indicate whether it's an anonymous visit.
-     * 
-     * @return String, the transformed url.
-     */
-    public static String seoUrl(String url, boolean isAnon) {
-        Perl5Matcher matcher = new Perl5Matcher();
-        if (SeoConfigUtil.checkUseUrlRegexp() && matcher.matches(url, SeoConfigUtil.getGeneralRegexpPattern())) {
-            Iterator<String> keys = SeoConfigUtil.getSeoPatterns().keySet().iterator();
-            boolean foundMatch = false;
-            while (keys.hasNext()) {
-                String key = keys.next();
-                Pattern pattern = SeoConfigUtil.getSeoPatterns().get(key);
-                if (pattern.getPattern().contains(";jsessionid=")) {
-                    if (isAnon) {
-                        if (SeoConfigUtil.isJSessionIdAnonEnabled()) {
-                            continue;
-                        }
-                    } else {
-                        if (SeoConfigUtil.isJSessionIdUserEnabled()) {
-                            continue;
-                        } else {
-                            boolean foundException = false;
-                            for (int i = 0; i < SeoConfigUtil.getUserExceptionPatterns().size(); i++) {
-                                if (matcher.matches(url, SeoConfigUtil.getUserExceptionPatterns().get(i))) {
-                                    foundException = true;
-                                    break;
-                                }
-                            }
-                            if (foundException) {
-                                continue;
-                            }
-                        }
-                    }
-                }
-                String replacement = SeoConfigUtil.getSeoReplacements().get(key);
-                if (matcher.matches(url, pattern)) {
-                    for (int i = 1; i < matcher.getMatch().groups(); i++) {
-                        replacement = replacement.replaceAll("\\$" + i, matcher.getMatch().group(i));
-                    }
-                    // break if found any matcher
-                    url = replacement;
-                    foundMatch = true;
-                    break;
-                }
-            }
-            if (!foundMatch) {
-                Debug.logVerbose("Can NOT find a seo transform pattern for this url: " + url, module);
-            }
-        }
-        return url;
-    }
-
-    static {
-        SeoConfigUtil.init();
-    }
-
-    /**
-     * Forward a uri according to forward pattern regular expressions. Note: this is developed for Filter usage.
-     * 
-     * @param uri
-     *            String to reverse transform
-     * @return String
-     */
-    public static boolean forwardUri(HttpServletResponse response, String uri) {
-        Perl5Matcher matcher = new Perl5Matcher();
-        boolean foundMatch = false;
-        Integer responseCodeInt = null;
-        if (SeoConfigUtil.checkUseUrlRegexp() && SeoConfigUtil.getSeoPatterns() != null && SeoConfigUtil.getForwardReplacements() != null) {
-            Iterator<String> keys = SeoConfigUtil.getSeoPatterns().keySet().iterator();
-            while (keys.hasNext()) {
-                String key = keys.next();
-                Pattern pattern = SeoConfigUtil.getSeoPatterns().get(key);
-                String replacement = SeoConfigUtil.getForwardReplacements().get(key);
-                if (matcher.matches(uri, pattern)) {
-                    for (int i = 1; i < matcher.getMatch().groups(); i++) {
-                        replacement = replacement.replaceAll("\\$" + i, matcher.getMatch().group(i));
-                    }
-                    // break if found any matcher
-                    uri = replacement;
-                    responseCodeInt = SeoConfigUtil.getForwardResponseCodes().get(key);
-                    foundMatch = true;
-                    break;
-                }
-            }
-        }
-        if (foundMatch) {
-            if (responseCodeInt == null) {
-                response.setStatus(SeoConfigUtil.getDefaultResponseCode());
-            } else {
-                response.setStatus(responseCodeInt.intValue());
-            }
-            response.setHeader("Location", uri);
-        } else {
-            Debug.logInfo("Can NOT forward this url: " + uri, module);
-        }
-        return foundMatch;
-    }
-}

README.md

@@ -1,8 +1 @@
-#PowerEnjoy
+https://etherpad.wikimedia.org/p/ingdaje2
-----------------------------------------
-
-# PDF
-I PDF generati nelle cartelle delle consegne vengono automaticamente ignorati. Per avere dei PDF pronti, bisogna inserirli nella cartella `Deliveries` nella root.
-
-# Pad Idee
-Link [qui](https://etherpad.wikimedia.org/p/ingdaje2)