Paths added

1.RASD/RASD.lyx

@@ -509,33 +509,249 @@ setcounter{page}{1}
 \end_layout
 
 \begin_layout Section
-Correction to the RASD
+Introduction
 \end_layout
 
 \begin_layout Subsection
-Rasd Version 1.1
+Revision History
 \end_layout
 
 \begin_layout Standard
-While writing the Design Document, we found necessary to make some modifications
- to the RASD.
- This is why we wrote the second version of the document.
- Here there are the updates we did: 
+\align center
+\begin_inset Tabular
+<lyxtabular version="3" rows="5" columns="4">
+<features tabularvalignment="middle" tabularwidth="80page%">
+<column alignment="center" valignment="middle" width="0pt">
+<column alignment="center" valignment="middle" width="0pt">
+<column alignment="center" valignment="middle" width="30col%">
+<column alignment="center" valignment="middle" width="40col%">
+<row topspace="2pt" bottomspace="2pt">
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Version
 \end_layout
 
-\begin_layout Itemize
-In the previous RASD we didn't specify that the Customer Service is an outsource
-d service, and so in this document and in the following documents we won't
- implement it;
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Date
 \end_layout
 
-\begin_layout Itemize
-We introduced a new functional requirement: modify the profile information.
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
 
+\begin_layout Plain Layout
+Author(s)
 \end_layout
 
-\begin_layout Section
-Introduction
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Summary
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row topspace="2pt" bottomspace="2pt">
+<cell alignment="center" valignment="top" topline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+1.3
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+22/01/2017
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Giancarlo Colaci 
+\begin_inset Newline newline
+\end_inset
+
+Giulio De Pasquale
+\begin_inset Newline newline
+\end_inset
+
+Francesco Rinaldi
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Updated Alloy
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row topspace="2pt" bottomspace="2pt">
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+1.2
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+14/01/2017
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Giancarlo Colaci
+\begin_inset Newline newline
+\end_inset
+
+Giulio De Pasquale
+\begin_inset Newline newline
+\end_inset
+
+Francesco Rinaldi
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Name refactoring, updated Class Diagram
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row topspace="2pt" bottomspace="2pt">
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+1.1
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+12/12/2016
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Giancarlo Colaci
+\begin_inset Newline newline
+\end_inset
+
+Giulio De Pasquale
+\begin_inset Newline newline
+\end_inset
+
+Francesco Rinaldi
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Further details, new functional requirement
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row topspace="2pt" bottomspace="2pt">
+<cell alignment="center" valignment="top" bottomline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+1.0
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" bottomline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+14/11/2016
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" bottomline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Giancarlo Colaci
+\begin_inset Newline newline
+\end_inset
+
+Giulio De Pasquale
+\begin_inset Newline newline
+\end_inset
+
+Francesco Rinaldi
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" bottomline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Initial Release
+\end_layout
+
+\end_inset
+</cell>
+</row>
+</lyxtabular>
+
+\end_inset
+
+
 \end_layout
 
 \begin_layout Subsection
@@ -4322,6 +4538,14 @@ Here it is shown a class diagram in order to give a static sight of the
  in this picture.
 \end_layout
 
+\begin_layout Standard
+This diagram is intended as a starting draft to be expanded further in the
+ design phase: moreover, it doesn't represent the final class infrastructure
+ which will be used in our system.
+ Finally, this diagram doesn't include the classes that will be used in
+ the Mobile/Web applications.
+\end_layout
+
 \begin_layout Standard
 \begin_inset space \quad{}
 \end_inset
@@ -5253,9 +5477,10 @@ Here are presented three generated worlds, according to the model specified
 \end_layout
 
 \begin_layout Standard
-\begin_inset External
-	template PDFPages
-	filename res/img/alloy_mondo_1.pdf
+\align center
+\begin_inset Graphics
+	filename res/img/world1.png
+	height 100theight%
 	rotateAngle 90
 
 \end_inset
@@ -5271,9 +5496,10 @@ Here are presented three generated worlds, according to the model specified
 \end_layout
 
 \begin_layout Standard
-\begin_inset External
-	template PDFPages
-	filename res/img/alloy_mondo_3.pdf
+\align center
+\begin_inset Graphics
+	filename res/img/world2.png
+	height 100theight%
 	rotateAngle 90
 
 \end_inset
@@ -5289,9 +5515,10 @@ Here are presented three generated worlds, according to the model specified
 \end_layout
 
 \begin_layout Standard
-\begin_inset External
-	template PDFPages
-	filename res/img/alloy_mondo_2.pdf
+\align center
+\begin_inset Graphics
+	filename res/img/world3.png
+	height 100theight%
 	rotateAngle 90
 
 \end_inset

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

@@ -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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-

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

@@ -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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-

1.RASD/res/alloy/AlloyPowerEnjoy.als

@@ -8,8 +8,7 @@ sig Float {
 		leftPart : one Int,
 		rightPart : one Int
 } {
-		leftPart > 0
-		rightPart > 0
+		rightPart >= 0
 } 
 
 sig User {
@@ -27,25 +26,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
-		wCode > 0
+		id >= 0
+		wCode >= 0
 }
 
 abstract sig RMSS {
 		id : one Int,
 		startTime : one Int,
-		endTime : lone Int,
+		endTime : one Int,
 		cost : one Float,
 		status : one RequestStatus,
 		paymentStatus : one PaymentStatus,
@@ -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
@@ -188,13 +194,32 @@ 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
@@ -260,6 +285,12 @@ 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
@@ -267,7 +298,9 @@ fact  noMultipleUsersForTheSameRequest {
 
 // The same Request cannot be performed by two different User
 fact noDifferentUserForTheSameRequest {
-		all r : RMSS | r in r.user.request
+		(all u1, u2 : User | u1 != u2 implies
+			(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

@@ -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

5.Code Inspection/src/ProductConfigItemContentWrapper.java

@@ -0,0 +1,200 @@
+/*******************************************************************************
+ * 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

@@ -0,0 +1,189 @@
+/*******************************************************************************
+ * 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

@@ -0,0 +1,231 @@
+/*******************************************************************************
+ * 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 +1,8 @@
-https://etherpad.wikimedia.org/p/ingdaje2
+#PowerEnjoy
+----------------------------------------
+
+# 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)