Compare commits
97 Commits
itpd-secti
...
master
Author | SHA1 | Date | |
---|---|---|---|
|
ae517b293f | ||
|
db795e81db | ||
|
c9e45969c9 | ||
|
473dd8c8e4 | ||
|
293f860395 | ||
|
a0373f4db7 | ||
|
43fc5f59a8 | ||
|
47cc41ad12 | ||
|
954edbbe93 | ||
|
9e3f19a05e | ||
|
f0272af803 | ||
|
989d54f8eb | ||
|
33fcc36efc | ||
|
2529915644 | ||
|
6ce2c4c470 | ||
|
47a25aebbf | ||
|
79249c9c69 | ||
|
31632f74a5 | ||
|
aa1a1c78e8 | ||
|
678359d03e | ||
|
df42f3fa07 | ||
|
2ffe2cb3f3 | ||
|
7c1ea13011 | ||
|
b7c8543be8 | ||
|
e71f30f0dd | ||
|
f5e8e0dc1e | ||
|
0e439963fd | ||
|
da7ee7b978 | ||
|
069f275869 | ||
|
1ebbecca39 | ||
|
77b4909bd2 | ||
|
3c020cf42f | ||
|
19dced1ec5 | ||
|
cf64a73bbf | ||
|
ad3a7231e5 | ||
|
b494e177c2 | ||
|
5ef9863bf3 | ||
|
7c7583dcd9 | ||
|
902be70754 | ||
|
ffd821485f | ||
|
70b920027e | ||
|
a90b7b3d94 | ||
|
fc763ff9f5 | ||
|
0f785226d8 | ||
|
327f88604e | ||
|
d3395aa7d0 | ||
|
dd856e15bb | ||
|
fdd84200af | ||
|
1399e522cd | ||
|
c26a47bcb2 | ||
|
5ca0f810f3 | ||
|
aec656ce6c | ||
|
e5faf0ea4b | ||
|
24cbd9af08 | ||
|
e4000b5632 | ||
|
bc5d95f2ec | ||
|
f569900fc7 | ||
|
d2e4e302de | ||
|
d984fbccae | ||
|
858923ab5a | ||
|
e61bed4c58 | ||
|
e396057410 | ||
|
5cbb48681b | ||
|
ab6a5f3af7 | ||
|
a57663442f | ||
|
690dced0cf | ||
|
5e086cbbd7 | ||
|
cdab03c1d5 | ||
|
2c8d990301 | ||
|
0bbd835a84 | ||
|
0db3108b9f | ||
|
3dee881ab7 | ||
|
d575cdbbf0 | ||
|
121d996d96 | ||
|
fd5fa91e9d | ||
|
75213e53e0 | ||
|
ade7a1f8b5 | ||
|
1630c38ceb | ||
|
1953b144f3 | ||
|
702fba3110 | ||
|
abb8093ded | ||
|
6381079e18 | ||
|
aaba835a99 | ||
|
6984c7d243 | ||
|
34184d3f9c | ||
|
a77b4d964b | ||
|
459aa638b1 | ||
|
873f1f0666 | ||
|
8b14797d0b | ||
|
3637220b3f | ||
|
5ede806c17 | ||
|
b254236c63 | ||
|
c930e1a581 | ||
|
d0b1ca541b | ||
|
bc978f0d29 | ||
daef56669d | |||
044c29c4ac |
273
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,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,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
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
@ -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,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
|
Before Width: | Height: | Size: 67 KiB After Width: | Height: | Size: 730 KiB |
BIN
1.RASD/res/img/world1.png
Normal file
After Width: | Height: | Size: 815 KiB |
BIN
1.RASD/res/img/world2.png
Normal file
After Width: | Height: | Size: 726 KiB |
BIN
1.RASD/res/img/world3.png
Normal file
After Width: | Height: | Size: 757 KiB |
Before Width: | Height: | Size: 751 KiB After Width: | Height: | Size: 474 KiB |
Before Width: | Height: | Size: 663 KiB |
Before Width: | Height: | Size: 420 KiB After Width: | Height: | Size: 422 KiB |
Before Width: | Height: | Size: 29 KiB After Width: | Height: | Size: 28 KiB |
Before Width: | Height: | Size: 33 KiB After Width: | Height: | Size: 32 KiB |
Before Width: | Height: | Size: 30 KiB After Width: | Height: | Size: 45 KiB |
Before Width: | Height: | Size: 47 KiB After Width: | Height: | Size: 48 KiB |
Before Width: | Height: | Size: 49 KiB After Width: | Height: | Size: 49 KiB |
Before Width: | Height: | Size: 49 KiB After Width: | Height: | Size: 49 KiB |
Before Width: | Height: | Size: 89 KiB |
Before Width: | Height: | Size: 52 KiB After Width: | Height: | Size: 84 KiB |
Before Width: | Height: | Size: 90 KiB |
Before Width: | Height: | Size: 52 KiB After Width: | Height: | Size: 84 KiB |
Before Width: | Height: | Size: 48 KiB After Width: | Height: | Size: 48 KiB |
Before Width: | Height: | Size: 47 KiB After Width: | Height: | Size: 47 KiB |
12677
4.Project Management/Planning.lyx
Normal file
BIN
4.Project Management/res/Dependencies.png
Normal file
After Width: | Height: | Size: 25 KiB |
BIN
4.Project Management/res/Dependencies.vsdx
Normal file
BIN
4.Project Management/res/GANTT.png
Normal file
After Width: | Height: | Size: 61 KiB |
BIN
4.Project Management/res/GANTT.vsdx
Normal file
5304
5.Code Inspection/CodeInspection.lyx
Normal file
BIN
5.Code Inspection/res/FreeMarker.png
Normal file
After Width: | Height: | Size: 24 KiB |
BIN
5.Code Inspection/res/Freemarker.vsdx
Normal file
BIN
5.Code Inspection/res/logopm.pdf
Normal file
200
5.Code Inspection/src/ProductConfigItemContentWrapper.java
Normal file
@ -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;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
189
5.Code Inspection/src/SeoTransform.java
Normal file
@ -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();
|
||||
}
|
||||
}
|
||||
}
|
231
5.Code Inspection/src/UrlRegexpTransform.java
Normal file
@ -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;
|
||||
}
|
||||
}
|
@ -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)
|
||||
|