Compare commits

...

97 Commits

Author SHA1 Message Date
Giulio De Pasquale
ae517b293f Paths added 2017-02-05 18:04:46 +01:00
Giulio De Pasquale
db795e81db 2.1.2 done 2017-02-05 17:56:50 +01:00
Giulio De Pasquale
c9e45969c9 2.1.1 done 2017-02-05 17:42:18 +01:00
Giancarlo Colaci
473dd8c8e4 Aggiunta file 2017-02-05 17:35:41 +01:00
Giulio De Pasquale
293f860395 Hyperref fixed 2017-02-04 21:17:14 +01:00
Giulio De Pasquale
a0373f4db7 Section 2.0 done 2017-02-04 20:43:45 +01:00
Giulio De Pasquale
43fc5f59a8 Table fixes 2017-02-04 20:32:40 +01:00
Giancarlo Colaci
47cc41ad12 Aggiunto qualcosa all'introduzione 2017-02-03 16:57:28 +01:00
Giancarlo Colaci
954edbbe93 Finita la modifica delle tabelle 2017-02-03 16:02:38 +01:00
Giancarlo Colaci
9e3f19a05e Modifiche sparse 2017-02-03 11:36:19 +01:00
Giulio De Pasquale
f0272af803 logo relative path fix 2017-02-03 11:34:02 +01:00
Giulio De Pasquale
989d54f8eb logo relative path fix 2017-02-03 11:26:25 +01:00
Giulio De Pasquale
33fcc36efc 2.1 done 2017-02-03 11:22:11 +01:00
Giancarlo Colaci
2529915644 Modifiche fino 24 2017-02-03 10:38:29 +01:00
Giulio De Pasquale
6ce2c4c470 LOL full stub now 2017-02-01 18:54:52 +01:00
Giulio De Pasquale
47a25aebbf LOL full stub now 2017-02-01 18:49:15 +01:00
Giulio De Pasquale
79249c9c69 Full stub 2017-02-01 18:44:25 +01:00
Giulio De Pasquale
31632f74a5 CodeInspection stub 2017-02-01 17:00:42 +01:00
Giulio De Pasquale
aa1a1c78e8 Added CI src files 2017-02-01 16:33:24 +01:00
Giulio De Pasquale
678359d03e Last fixes, GANTT 2017-01-22 23:32:53 +01:00
Giulio De Pasquale
df42f3fa07 Last fixes, GANTT 2017-01-22 23:32:45 +01:00
Giulio De Pasquale
2ffe2cb3f3 ITPD done 2017-01-22 23:11:50 +01:00
Giulio De Pasquale
7c1ea13011 Planning done 2017-01-22 23:10:48 +01:00
Giulio De Pasquale
b7c8543be8 DD done 2017-01-22 23:06:27 +01:00
Giulio De Pasquale
e71f30f0dd RASD done 2017-01-22 23:01:25 +01:00
Giulio De Pasquale
f5e8e0dc1e Merge branch 'master' of ssh://giugl.io:10022/peperunas/swing2 2017-01-22 23:00:46 +01:00
Giulio De Pasquale
0e439963fd RASD done 2017-01-22 23:00:37 +01:00
Francesco Rinaldi
da7ee7b978 better style for the document 2017-01-22 22:49:39 +01:00
Francesco Rinaldi
069f275869 fixed 3.2 style 2017-01-22 22:42:12 +01:00
Francesco Rinaldi
1ebbecca39 fixed unknown bug 2017-01-22 22:37:30 +01:00
Francesco Rinaldi
77b4909bd2 Planning document completed 2017-01-22 22:23:04 +01:00
Giulio De Pasquale
3c020cf42f noDifferentUserForTheSameRequest fixed 2017-01-22 16:55:06 +01:00
Giulio De Pasquale
19dced1ec5 norentIfPaymentDenied to noRentIfPaymentUncertain 2017-01-22 16:42:03 +01:00
Giulio De Pasquale
cf64a73bbf noEarlyRent added 2017-01-22 16:26:59 +01:00
Giulio De Pasquale
ad3a7231e5 noRentIfPaymentDenied and noPhantomResRent added 2017-01-22 16:21:50 +01:00
Giulio De Pasquale
b494e177c2 No duplicate payments, alloy 2017-01-22 13:45:37 +01:00
Francesco Rinaldi
5ef9863bf3 Updated Class Diagram 2017-01-22 12:30:43 +01:00
Giulio De Pasquale
7c7583dcd9 Fixed alloy to reflect new class diagram, removed useless als 2017-01-22 12:19:00 +01:00
Giancarlo Colaci
902be70754 Modifica delle ore 2017-01-22 11:23:06 +01:00
Giulio De Pasquale
ffd821485f Section 6.3 done 2017-01-20 20:24:33 +01:00
Giulio De Pasquale
70b920027e Section 6.2 done 2017-01-20 20:08:16 +01:00
Giancarlo Colaci
a90b7b3d94 Added folder res with graphs 2017-01-20 20:03:33 +01:00
Giulio De Pasquale
fc763ff9f5 Section 6.1 fixes 2017-01-20 19:37:19 +01:00
Giulio De Pasquale
0f785226d8 Section 6.1 done 2017-01-20 19:35:20 +01:00
Giulio De Pasquale
327f88604e Section 6 scrambling 2017-01-20 19:25:13 +01:00
Giulio De Pasquale
d3395aa7d0 Section 5 table 26 week fix 2017-01-20 19:08:08 +01:00
Giulio De Pasquale
dd856e15bb Merge branch 'master' of ssh://giugl.io:10022/peperunas/swing2 2017-01-20 19:04:03 +01:00
Giulio De Pasquale
fdd84200af Section 6 tables stubs 2017-01-20 19:04:01 +01:00
Francesco Rinaldi
1399e522cd RELY cost drivers table 2017-01-20 19:01:34 +01:00
Giulio De Pasquale
c26a47bcb2 Section 6.1, section 4 layout 2017-01-20 18:36:48 +01:00
Giulio De Pasquale
5ca0f810f3 Table stub in section 3 2017-01-20 18:28:24 +01:00
Francesco Rinaldi
aec656ce6c now 3.2 is finished sorrynotsorry 2017-01-20 18:10:38 +01:00
Francesco Rinaldi
e5faf0ea4b name 4 giul 2017-01-20 18:03:28 +01:00
Giulio De Pasquale
24cbd9af08 3.2 table fix 2 2017-01-20 18:01:51 +01:00
Giulio De Pasquale
e4000b5632 3.2 pedici 2017-01-20 17:59:01 +01:00
Giulio De Pasquale
bc5d95f2ec 3.2 table fix 2017-01-20 17:56:17 +01:00
Francesco Rinaldi
f569900fc7 sorrynotsorry 2017-01-20 17:47:41 +01:00
Giulio De Pasquale
d2e4e302de PORCODIOFRANCESCO 2017-01-20 17:45:51 +01:00
Francesco Rinaldi
d984fbccae 3.2 finished 2017-01-20 17:19:10 +01:00
Giulio De Pasquale
858923ab5a Section 5 2017-01-20 17:18:25 +01:00
Francesco Rinaldi
e61bed4c58 3.2 finished 2017-01-20 17:17:37 +01:00
Francesco Rinaldi
e396057410 3.2 finished 2017-01-20 17:16:33 +01:00
Giulio De Pasquale
5cbb48681b Section 5 stub 2017-01-20 16:53:26 +01:00
Giulio De Pasquale
ab6a5f3af7 Section 5 stub 2017-01-20 16:53:13 +01:00
Francesco Rinaldi
a57663442f uff 2017-01-20 16:39:45 +01:00
Francesco Rinaldi
690dced0cf changes 2017-01-20 16:37:39 +01:00
Francesco Rinaldi
5e086cbbd7 scale factors modified 2017-01-20 16:36:53 +01:00
Giancarlo Colaci
cdab03c1d5 Table numbers 2017-01-20 16:35:18 +01:00
Francesco Rinaldi
2c8d990301 scale factors added 2017-01-20 16:31:33 +01:00
Giulio De Pasquale
0bbd835a84 Section 4 done. Formatting fixes 2017-01-19 17:30:25 +01:00
Giulio De Pasquale
0db3108b9f Section 2 completed 2017-01-19 17:02:27 +01:00
Giulio De Pasquale
3dee881ab7 2.1 completed 2017-01-19 15:52:46 +01:00
Giulio De Pasquale
d575cdbbf0 Complexity tables 2017-01-19 15:32:01 +01:00
Giulio De Pasquale
121d996d96 Chap 4 stub 2017-01-19 12:47:58 +01:00
Francesco Rinaldi
fd5fa91e9d Class Diagram Updated 2017-01-15 13:00:03 +01:00
Giulio De Pasquale
75213e53e0 Added CD description in RASD 2017-01-14 11:40:15 +01:00
Giulio De Pasquale
ade7a1f8b5 Removed OLD pngs 2017-01-14 11:34:03 +01:00
Giulio De Pasquale
1630c38ceb Fixed table width RASD 1.1 | #14 2017-01-14 11:33:10 +01:00
Francesco Rinaldi
1953b144f3 ITPD is DONE for me. I think it is ready to be PUSHED into the public repository. We just need to remove OLD png whenever we approve this version. 2017-01-14 00:41:29 +01:00
Francesco Rinaldi
702fba3110 Merge branch 'master' of http://giugl.io:10000/peperunas/swing2 2017-01-14 00:39:50 +01:00
Francesco Rinaldi
abb8093ded ITPD is DONE for me. I think it is ready to be PUSHED into the public repository. 2017-01-14 00:39:10 +01:00
Giulio De Pasquale
6381079e18 Removed Core Data dep from interfaces 2017-01-13 23:03:27 +01:00
Giulio De Pasquale
aaba835a99 Fixes here and there 2017-01-13 22:56:59 +01:00
Giulio De Pasquale
6984c7d243 #12, #13 | Finished section 1,4,5,6 2017-01-12 18:14:00 +01:00
Giulio De Pasquale
34184d3f9c #8 | Changelogs, introductions restyled 2017-01-12 12:58:17 +01:00
Francesco Rinaldi
a77b4d964b E anche oggi si dorme domani. Solved #2 & #4 MI PARE EH POI BOH C'HO SONNO 2017-01-12 01:53:25 +01:00
Francesco Rinaldi
459aa638b1 Section 3 RE-FORMATTED gesù bambino 2017-01-12 00:28:20 +01:00
Francesco Rinaldi
873f1f0666 Minor fixes + Interfaces graphs in ITPD 2017-01-11 22:52:08 +01:00
Francesco Rinaldi
8b14797d0b Request Management 2.4.2 changed 2017-01-11 20:24:57 +01:00
Giulio De Pasquale
3637220b3f RMSS comeback 2017-01-11 20:23:52 +01:00
Giulio De Pasquale
5ede806c17 RMSS comeback 2017-01-11 20:23:31 +01:00
Giulio De Pasquale
b254236c63 Fixes in section 3, ITPD 2017-01-11 20:08:42 +01:00
Giulio De Pasquale
c930e1a581 Fixes in 3.1 descriptions 2017-01-11 19:51:09 +01:00
Giulio De Pasquale
d0b1ca541b Fixes in 3.1 descriptions 2017-01-11 19:50:31 +01:00
Francesco Rinaldi
bc978f0d29 test 2017-01-11 19:50:09 +01:00
daef56669d Merge branch 'itpd-section3' of peperunas/swing2 into master 2017-01-11 18:44:54 +00:00
044c29c4ac Merge branch 'itpd-section3' of peperunas/swing2 into master 2017-01-11 18:35:38 +00:00
43 changed files with 27707 additions and 8753 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

Binary file not shown.

Before

Width:  |  Height:  |  Size: 67 KiB

After

Width:  |  Height:  |  Size: 730 KiB

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

BIN
1.RASD/res/img/world1.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 815 KiB

BIN
1.RASD/res/img/world2.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 726 KiB

BIN
1.RASD/res/img/world3.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 757 KiB

File diff suppressed because it is too large Load Diff

Binary file not shown.

Before

Width:  |  Height:  |  Size: 751 KiB

After

Width:  |  Height:  |  Size: 474 KiB

File diff suppressed because it is too large Load Diff

Binary file not shown.

Before

Width:  |  Height:  |  Size: 663 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 420 KiB

After

Width:  |  Height:  |  Size: 422 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 29 KiB

After

Width:  |  Height:  |  Size: 28 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 33 KiB

After

Width:  |  Height:  |  Size: 32 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 30 KiB

After

Width:  |  Height:  |  Size: 45 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 47 KiB

After

Width:  |  Height:  |  Size: 48 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 49 KiB

After

Width:  |  Height:  |  Size: 49 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 49 KiB

After

Width:  |  Height:  |  Size: 49 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 89 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 52 KiB

After

Width:  |  Height:  |  Size: 84 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 90 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 52 KiB

After

Width:  |  Height:  |  Size: 84 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 48 KiB

After

Width:  |  Height:  |  Size: 48 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 47 KiB

After

Width:  |  Height:  |  Size: 47 KiB

File diff suppressed because it is too large Load Diff

Binary file not shown.

After

Width:  |  Height:  |  Size: 25 KiB

Binary file not shown.

Binary file not shown.

After

Width:  |  Height:  |  Size: 61 KiB

Binary file not shown.

File diff suppressed because it is too large Load Diff

Binary file not shown.

After

Width:  |  Height:  |  Size: 24 KiB

Binary file not shown.

Binary file not shown.

View 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;
}
}
}
}
}

View 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();
}
}
}

View 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;
}
}

View File

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