43 changed files with 8983 additions and 27937 deletions
--- a/1.RASD/RASD.lyx
+++ b/1.RASD/RASD.lyx
@ -509,249 +509,33 @@ setcounter{page}{1}
 \end_layout
 \begin_layout Section
-Introduction
+Correction to the RASD
 \end_layout
 \begin_layout Subsection
-Revision History
+Rasd Version 1.1
 \end_layout
 \begin_layout Standard
-\align center
+While writing the Design Document, we found necessary to make some modiﬁcations
-\begin_inset Tabular
+ to the RASD.
-<lyxtabular version="3" rows="5" columns="4">
+ This is why we wrote the second version of the document.
-<features tabularvalignment="middle" tabularwidth="80page%">
+ Here there are the updates we did: 
 <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
-\end_inset
+\begin_layout Itemize
-</cell>
+In the previous RASD we didn't specify that the Customer Service is an outsource
-<cell alignment="center" valignment="top" usebox="none">
+d service, and so in this document and in the following documents we won't
-\begin_inset Text
+ implement it;
 \begin_layout Plain Layout
 Date
 \end_layout
-\end_inset
+\begin_layout Itemize
-</cell>
+We introduced a new functional requirement: modify the profile information.
 <cell alignment="center" valignment="top" usebox="none">
 \begin_inset Text
 \begin_layout Plain Layout
 Author(s)
 \end_layout
-\end_inset
+\begin_layout Section
-</cell>
+Introduction
 <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
@ -4538,14 +4322,6 @@ 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
@ -5477,10 +5253,9 @@ Here are presented three generated worlds, according to the model speciﬁed
 \end_layout
 \begin_layout Standard
-\align center
+\begin_inset External
-\begin_inset Graphics
+	template PDFPages
-	filename res/img/world1.png
+	filename res/img/alloy_mondo_1.pdf
 	height 100theight%
 	rotateAngle 90
 \end_inset
@ -5496,10 +5271,9 @@ Here are presented three generated worlds, according to the model speciﬁed
 \end_layout
 \begin_layout Standard
-\align center
+\begin_inset External
-\begin_inset Graphics
+	template PDFPages
-	filename res/img/world2.png
+	filename res/img/alloy_mondo_3.pdf
 	height 100theight%
 	rotateAngle 90
 \end_inset
@ -5515,10 +5289,9 @@ Here are presented three generated worlds, according to the model speciﬁed
 \end_layout
 \begin_layout Standard
-\align center
+\begin_inset External
-\begin_inset Graphics
+	template PDFPages
-	filename res/img/world3.png
+	filename res/img/alloy_mondo_2.pdf
 	height 100theight%
 	rotateAngle 90
 \end_inset
--- a/1.RASD/res/alloy/AlloyPowerEnjoy
+++ b/1.RASD/res/alloy/AlloyPowerEnjoy
@ -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
--- a/1.RASD/res/alloy/AlloyPowerEnjoy(DUPLICATO).als
+++ b/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
--- a/1.RASD/res/alloy/AlloyPowerEnjoy.als
+++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als
@ -8,7 +8,8 @@ sig Float {
 		leftPart : one Int,
 		rightPart : one Int
 } {
-		rightPart >= 0
+		leftPart > 0
 		rightPart > 0
 }
 sig User {
@ -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,
 	status: one Stringa,
 	rmss: one RMSS
 } {
 	id >= 0
 }
 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
 	latitude.leftPart >= 0
 	longitude.leftPart >= 0
 }
 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
+		car : set Car,
 		rechargingArea : set RechargingArea
 } {
-	availableCars >= 0
+		id > 0
 		availableCars > 0
 }
-sig RechargingArea extends Location {
+sig City {
 		id : one Int,
 		name : one Stringa,
 		parkingArea : set ParkingArea
 } {
 		id > 0
 }
 sig RechargingArea {
 		id : one Int,
 		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
--- a/1.RASD/res/alloy/seconda
+++ b/1.RASD/res/alloy/seconda
@ -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
--- a/1.RASD/res/img/ClassD.png
+++ b/1.RASD/res/img/ClassD.png
--- a/1.RASD/res/img/alloy_PROVA.pdf
+++ b/1.RASD/res/img/alloy_PROVA.pdf
--- a/1.RASD/res/img/alloy_mondo_1.pdf
+++ b/1.RASD/res/img/alloy_mondo_1.pdf
--- a/1.RASD/res/img/alloy_mondo_2.pdf
+++ b/1.RASD/res/img/alloy_mondo_2.pdf
--- a/1.RASD/res/img/alloy_mondo_3.pdf
+++ b/1.RASD/res/img/alloy_mondo_3.pdf
--- a/1.RASD/res/img/world1.png
+++ b/1.RASD/res/img/world1.png
--- a/1.RASD/res/img/world2.png
+++ b/1.RASD/res/img/world2.png
--- a/1.RASD/res/img/world3.png
+++ b/1.RASD/res/img/world3.png
--- a/Document/DD.lyx
+++ b/Document/DD.lyx
--- a/Document/res/img/ComponentView.png
+++ b/Document/res/img/ComponentView.png
--- a/Document/ITPD.lyx
+++ b/Document/ITPD.lyx
--- a/Document/res/img/2.4.2
+++ b/Document/res/img/2.4.2
--- a/Document/res/img/2.4.2.png
+++ b/Document/res/img/2.4.2.png
--- a/Document/res/img/Account
+++ b/Document/res/img/Account
--- a/Document/res/img/Account
+++ b/Document/res/img/Account
--- a/Document/res/img/Car
+++ b/Document/res/img/Car
--- a/Document/res/img/Car
+++ b/Document/res/img/Car
--- a/Document/res/img/Events
+++ b/Document/res/img/Events
--- a/Document/res/img/Events
+++ b/Document/res/img/Events
--- a/Document/res/img/Interfaces
+++ b/Document/res/img/Interfaces
--- a/Document/res/img/Interfaces
+++ b/Document/res/img/Interfaces
--- a/Document/res/img/Interfaces
+++ b/Document/res/img/Interfaces
--- a/Document/res/img/Interfaces
+++ b/Document/res/img/Interfaces
--- a/Document/res/img/Reservation
+++ b/Document/res/img/Reservation
--- a/Document/res/img/Reservation
+++ b/Document/res/img/Reservation
--- a/Management/Planning.lyx
+++ b/Management/Planning.lyx
--- a/Management/res/Dependencies.png
+++ b/Management/res/Dependencies.png
--- a/Management/res/Dependencies.vsdx
+++ b/Management/res/Dependencies.vsdx
--- a/Management/res/GANTT.png
+++ b/Management/res/GANTT.png
--- a/Management/res/GANTT.vsdx
+++ b/Management/res/GANTT.vsdx
--- a/Inspection/CodeInspection.lyx
+++ b/Inspection/CodeInspection.lyx
--- a/Inspection/res/FreeMarker.png
+++ b/Inspection/res/FreeMarker.png
--- a/Inspection/res/Freemarker.vsdx
+++ b/Inspection/res/Freemarker.vsdx
--- a/Inspection/res/logopm.pdf
+++ b/Inspection/res/logopm.pdf
--- a/Inspection/src/ProductConfigItemContentWrapper.java
+++ b/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;
                }
            }
        }
    }
 }
--- a/Inspection/src/SeoTransform.java
+++ b/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();
        }
    }
 }
--- a/Inspection/src/UrlRegexpTransform.java
+++ b/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;
    }
 }
--- a/README.md
+++ b/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)