peperunas/swing2
1
0
Fork 0
Code Issues 3 Pull Requests Releases Wiki Activity

Compare commits

base: peperunas:master
Branches Tags
peperunas:master
peperunas:itpd-section3
..
compare: peperunas:itpd-section3
Branches Tags
peperunas:master
peperunas:itpd-section3

No commits in common. "master" and "itpd-section3" have entirely different histories.
master ... itpd-secti

43 changed files with 8983 additions and 27937 deletions
Show Stats Expand all files Collapse all files

273
1.RASD/RASD.lyx
View File

@ -509,249 +509,33 @@ setcounter{page}{1}
\end_layout
\begin_layout Section
Introduction
Correction to the RASD
\end_layout
\begin_layout Subsection
Revision History
Rasd Version 1.1
\end_layout
\begin_layout Standard
\align center
\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
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:
\end_layout
\end_inset
</cell>
<cell alignment="center" valignment="top" usebox="none">
\begin_inset Text
\begin_layout Plain Layout
Date
\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_layout
\end_inset
</cell>
<cell alignment="center" valignment="top" usebox="none">
\begin_inset Text
\begin_layout Itemize
We introduced a new functional requirement: modify the profile information.
\begin_layout Plain Layout
Author(s)
\end_layout
\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
\begin_layout Section
Introduction
\end_layout
\begin_layout Subsection
@ -4538,14 +4322,6 @@ Here it is shown a class diagram in order to give a static sight of the
in this picture.
\end_layout
\begin_layout Standard
This diagram is intended as a starting draft to be expanded further in the
design phase: moreover, it doesn't represent the final class infrastructure
which will be used in our system.
Finally, this diagram doesn't include the classes that will be used in
the Mobile/Web applications.
\end_layout
\begin_layout Standard
\begin_inset space \quad{}
\end_inset
@ -5477,10 +5253,9 @@ Here are presented three generated worlds, according to the model specified
\end_layout
\begin_layout Standard
\align center
\begin_inset Graphics
filename res/img/world1.png
height 100theight%
\begin_inset External
template PDFPages
filename res/img/alloy_mondo_1.pdf
rotateAngle 90
\end_inset
@ -5496,10 +5271,9 @@ Here are presented three generated worlds, according to the model specified
\end_layout
\begin_layout Standard
\align center
\begin_inset Graphics
filename res/img/world2.png
height 100theight%
\begin_inset External
template PDFPages
filename res/img/alloy_mondo_3.pdf
rotateAngle 90
\end_inset
@ -5515,10 +5289,9 @@ Here are presented three generated worlds, according to the model specified
\end_layout
\begin_layout Standard
\align center
\begin_inset Graphics
filename res/img/world3.png
height 100theight%
\begin_inset External
template PDFPages
filename res/img/alloy_mondo_2.pdf
rotateAngle 90
\end_inset

364
1.RASD/res/alloy/AlloyPowerEnjoy (COPIA DI SICUREZZA).als Normal file
View File

@ -0,0 +1,364 @@
module PowerEnjoy
//SIG
sig Stringa {}
sig Float {
leftPart : one Int,
rightPart : one Int
} {
leftPart > 0
rightPart > 0
}
sig Car {
id : one Int,
plate : one Stringa,
wCode : one Int,
ecs : one ECS,
ads : one ADS,
status : one CarStatus,
request : set RMSS
} {
id > 0
wCode > 0
}
abstract sig RMSS {
id : one Int,
startTime : one Int,
endTime : lone Int,
cost : one Float,
status : one RequestStatus,
paymentStatus : one PaymentStatus,
userID : one Int,
carID : one Int,
userPosition : one Stringa,
carPosition : one Stringa,
reservation : lone Reservation,
rent : lone Rent
} {
id > 0
startTime > 0
endTime = none or endTime > 0
userID > 0
carID > 0
endTime > startTime
}
sig Reservation extends RMSS {
countDown : one Int
} {
countDown >= 0
}
sig Rent extends RMSS {
mSavingOptionActived : one Bool
}
sig User {
id : one Int,
name : one Stringa,
surname : one Stringa,
email : one Stringa,
password : one Stringa,
phone : one Stringa,
address : one Stringa,
SSN : one Stringa,
verificationCode : one Stringa,
drivingLicence : one Stringa,
billingInformation: one BillingInformation,
moneySavingOption : one Bool,
request : set RMSS
} {
id > 0
}
sig DeactivatedUser extends User {}
sig ECS {
id : one Int,
} {
id > 0
}
sig ADS {
id : one Int
} {
id > 0
}
sig ParkingArea {
id : one Int,
name : one Stringa,
availableCars : one Int,
car : set Car,
rechargingArea : set RechargingArea
} {
id > 0
availableCars > 0
}
sig City {
id : one Int,
name : one Stringa,
parkingArea : set ParkingArea
} {
id > 0
}
sig RechargingArea {
id : one Int,
plugs : one Int,
address : one Stringa,
isSpecial : one Bool
} {
id > 0
plugs > 0
}
// ENUMS
enum Bool {
TRUE,
FALSE
}
enum BillingInformation {
CONFIRMED,
NOTCONFIRMED
}
enum PaymentStatus {
ACCEPTED,
PENDING,
DENIED
}
enum CarStatus {
AVAILABLE,
RESERVED,
UNAVAILABLE,
INUSE
}
enum RequestStatus {
ACTIVE,
EXPIRED
}
// FACTS
// In any city there is at least a parking area
fact atLeastAParkingArea {
#ParkingArea >= 1
}
// In any parking area there could be zero or more recharging area
fact presenceOfRechargingArea {
#RechargingArea >= 0
}
// In any parking area there could be zero or more cars
fact presenceOfCars {
#Car >= 0
}
// Relation between users and active requests (reservation or rent)
fact atMaxOneActiveRequestForUser {
(all u : User | lone r : RMSS | (u.request = r) and (r.userID = u.id) and (r.status = ACTIVE))
// Each user has at maximum an active request at time
}
// Relation between RMSS and reservation or rent
fact relationBetweenRequests {
(all rm : RMSS | (one res : Reservation | rm.id = res.id) or
(one ren : Rent | rm.id = ren.id))
}
// R
fact a {
all rn : Rent | one rs : Reservation | (rn.userID = rs.userID) and
(rn.carID = rs.carID) and (rn.startTime = rs.endTime)
}
fact b {
all rn : Rent | no rs : Reservation | rn.id = rs.id
}
fact c {
all rs : Reservation | no rn : Rent | rs.id = rn.id
}
// Relation between active requests (reservation or rent) and users
fact exactelyOneUserForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies
(one u : User | u.request = r))
// Each active request belongs exactely to one user
}
// Relation between cars and active requests (reservation or rent)
fact atMaxOneActiveRequestForCar {
(all c : Car | lone r : RMSS | (c.request = r) and (r.status = ACTIVE))
// Each car has at maximum an active request at time
}
// Relation between active requests (reservation or rent) and car
fact exactelyOneCarForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies
(one c : Car | c.request = r))
// Each active request refers exactely to one car
}
// Relation between deactivated users and active requests (reservation or rent)
fact noActiveRequestForDeactivatedUser {
(no dU : DeactivatedUser | one r : RMSS | (dU.request = r) and (r.status = ACTIVE))
// No deactivated users can have an active request
}
// Relation between active requests (reservation or rent) and deactivated users
fact noDeactivatedUserForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies
(no dU : DeactivatedUser | dU.request = r))
// Each active request does not belong to any deactivated user
}
// No duplicated users
fact noDuplicatedUser {
(no u1 , u2 : User | u1.id = u2.id and u1 != u2) and
(no u1 , u2 : User | u1.email = u2.email and u1 != u2) and
(no u1 , u2 : User | u1.SSN = u2.SSN and u1 != u2) and
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2)
}
// No users with NOTCONFIRMED billing information
fact noUserWithNotConfirmedBilling {
no u : User | u.billingInformation = NOTCONFIRMED
}
// No duplicated deactivated users
fact noDuplicatedDeactivatedUser {
(no du1 , du2 : DeactivatedUser | du1.id = du2.id and du1 != du2) and
(no du1 , du2 : DeactivatedUser | du1.email = du2.email and du1 != du2) and
(no du1 , du2 : DeactivatedUser | du1.SSN = du2.SSN and du1 != du2) and
(no du1 , du2 : DeactivatedUser | du1.drivingLicence = du2.drivingLicence and du1 != du2)
}
// No cities with the same ID
fact noDuplicatedCities {
no c1 , c2 : City | c1.id = c2.id and c1 != c2
}
// No Parking Areas with the same ID
fact noDuplicatedParkingAreas {
no pa1 , pa2 : ParkingArea | pa1.id = pa2.id and pa1 != pa2
}
// No Recharging Areas with the same ID
fact noDuplicatedRechargingAreas {
no ra1 , ra2 : RechargingArea | ra1.id = ra2.id and ra1 != ra2
}
// No duplicated requests
fact noDuplicatedRMSS{
(no req1 , req2 : RMSS | req1.id = req2.id and req1 != req2) and
(no req1 , req2 : RMSS | (req1.userID = req2.userID and
req1.carID = req2.carID and req1.startTime = req2.startTime and
req1.endTime = req2.endTime and req1 != req2))
}
fact noDuplicatedReservation{
(no res1 , res2 : Reservation | res1.id = res2.id and res1 != res2) and
(no res1 , res2 : Reservation | (res1.userID = res2.userID and
res1.carID = res2.carID and res1.startTime = res2.startTime and
res1.endTime = res2.endTime and res1 != res2))
}
fact noDuplicatedRent{
(no ren1 , ren2 : Rent | ren1.id = ren2.id and ren1 != ren2) and
(no ren1 , ren2 : Rent | (ren1.userID = ren2.userID and
ren1.carID = ren2.carID and ren1.startTime = ren2.startTime and
ren1.endTime = ren2.endTime and ren1 != ren2))
}
// No duplicated cars
fact noDuplicatedCars {
(no c1 , c2 : Car | c1.id = c2.id and c1 != c2) and
(no c1 , c2 : Car | c1.plate = c2.plate and c1 != c2) and
(no c1 , c2 : Car | c1.wCode = c2.wCode and c1 != c2)
}
// No ECS with the same ID
fact noDuplicatedECS {
no ecs1 , ecs2 : ECS | ecs1.id = ecs2.id and ecs1 != ecs2
}
// No ADS with the same ID
fact noDuplicatedADS {
no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2
}
// AVAILABLE car
// When a request is active the status of the payment is pending
fact pendingPaymentForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
}
//ASSERTION
// The number of active rents is equal to the number of cars in use
assert equalityOfRentedCarsAndActiveRents {
#{r : Rent | r.status = ACTIVE} = #{c : Car | c.status = INUSE}
}
//
//check equalityOfRentedCarsAndActiveRents for 2
// The number of active reservations is equal to the number of cars reserved
assert equalityOfReservedCarsAndActiveReservations {
#{r : Reservation | r.status = ACTIVE} = #{c : Car | c.status = RESERVED}
}
//
//check equalityOfReservedCarsAndActiveReservations for 2
// Same number of requests
assert equalityOfRequestsAsReservationOrRent {
#{rm : RMSS} = (#{rs : Reservation} + #{rn : Rent})
}
//
//check equalityOfRequestsAsReservationOrRent for 1
pred show {}
run show for 1 but exactly 1 User, exactly 2 RMSS, exactly 1 Rent, exactly 1 Car

480
1.RASD/res/alloy/AlloyPowerEnjoy(DUPLICATO).als Normal file
View File

@ -0,0 +1,480 @@
module PowerEnjoy
//SIG
sig Stringa {}
sig Float {
leftPart : one Int,
rightPart : one Int
} {
leftPart > 0
rightPart > 0
}
sig Car {
id : one Int,
plate : one Stringa,
wCode : one Int,
ecs : one ECS,
ads : one ADS,
status : one CarStatus//,
//request : set RMSS
} {
id > 0
wCode > 0
}
abstract sig RMSS {
id : one Int,
startTime : one Int,
endTime : lone Int,
cost : one Float,
status : one RequestStatus,
paymentStatus : one PaymentStatus,
userID : one Int,
carID : one Int,
userPosition : one Stringa,
carPosition : one Stringa,
car : one Car
//reservation : lone Reservation,
//rent : lone Rent
} {
id > 0
startTime > 0
endTime = none or endTime > 0
userID > 0
carID > 0
endTime > startTime
}
sig Reservation extends RMSS {
countDown : one Int
} {
countDown >= 0
}
sig Rent extends RMSS {
mSavingOptionActived : one Bool
}
sig User {
id : one Int,
name : one Stringa,
surname : one Stringa,
email : one Stringa,
password : one Stringa,
phone : one Stringa,
address : one Stringa,
SSN : one Stringa,
verificationCode : one Stringa,
drivingLicence : one Stringa,
billingInformation: one BillingInformation,
moneySavingOption : one Bool,
request : set RMSS
} {
id > 0
}
sig DeactivatedUser extends User {}
sig ECS {
id : one Int,
} {
id > 0
}
sig ADS {
id : one Int
} {
id > 0
}
sig ParkingArea {
id : one Int,
name : one Stringa,
availableCars : one Int,
car : set Car,
rechargingArea : set RechargingArea
} {
id > 0
availableCars > 0
}
sig City {
id : one Int,
name : one Stringa,
parkingArea : set ParkingArea
} {
id > 0
}
sig RechargingArea {
id : one Int,
plugs : one Int,
address : one Stringa,
isSpecial : one Bool
} {
id > 0
plugs > 0
}
// ENUMS
enum Bool {
TRUE,
FALSE
}
enum BillingInformation {
CONFIRMED,
NOTCONFIRMED
}
enum PaymentStatus {
ACCEPTED,
PENDING,
DENIED
}
enum CarStatus {
AVAILABLE,
RESERVED,
UNAVAILABLE,
INUSE
}
enum RequestStatus {
ACTIVE,
EXPIRED
}
// FACTS
// In any city there is at least a parking area
fact atLeastAParkingArea {
#ParkingArea >= 1
}
// In any parking area there could be zero or more recharging area
fact presenceOfRechargingArea {
#RechargingArea >= 0
}
// In any parking area there could be zero or more cars
fact presenceOfCars {
#Car >= 0
}
// Relation between users and active requests (reservation or rent)
fact atMaxOneActiveRequestForUser {
(all u : User | lone r : RMSS | (u.request = r) and (r.userID = u.id) and (r.status = ACTIVE))
// Each user has at maximum an active request at time
}
// Relation between Rent and Reservations
fact a {
all ren : Rent | one res : Reservation | ( (ren.userID = res.userID) and
(ren.carID = res.carID) and (ren.startTime = res.endTime) )
}
// Relation between RMSS and Reservation or Rent
fact relationBetweenRequests {
(all rm : RMSS |
(
one res : Reservation | ( (rm.id = res.id) and (rm.userID = res.userID)
and (rm.carID = res.carID) and (rm.startTime = res.startTime) and
(rm.endTime = res.endTime) )
)
or
(
one ren : Rent | ( (rm.id = ren.id) and (rm.userID = ren.userID)
and (rm.carID = ren.carID) and (rm.startTime = ren.startTime) and
(rm.endTime = ren.endTime) )
)
)
}
fact b {
all ren : Rent | no res : Reservation | ren.id = res.id
}
fact c {
all res : Reservation | no ren : Rent | res.id = ren.id
}
// Relation between active requests (reservations or rents) and users
fact exactelyOneUserForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies
(one u : User | u.request = r))
// Each active request belongs exactely to one user
}
// Each user can have multiple expired requests (reservations or rents)
fact multipleExpiredRequests {
(all r : RMSS | r.status = EXPIRED implies
(one u : User | u.request = r))
}
// Relation between cars and active requests (reservations or rents)
fact atMaxOneActiveRequestForCar {
(all c : Car | lone r : RMSS | (c.request = r) and (r.status = ACTIVE))
// Each car has at maximum an active request at time
}
// Relation between active requests (reservation or rent) and car
fact exactelyOneCarForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies
(one c : Car | c.request = r))
// Each active request refers exactely to one car
}
// Relation between deactivated users and active requests (reservation or rent)
fact noActiveRequestForDeactivatedUser {
(no dU : DeactivatedUser | one r : RMSS | (dU.request = r) and (r.status = ACTIVE))
// No deactivated users can have an active request
}
// Relation between active requests (reservation or rent) and deactivated users
fact noDeactivatedUserForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies
(no dU : DeactivatedUser | dU.request = r))
// Each active request does not belong to any deactivated user
}
// No duplicated users
fact noDuplicatedUser {
(no u1 , u2 : User | u1.id = u2.id and u1 != u2) and
(no u1 , u2 : User | u1.email = u2.email and u1 != u2) and
(no u1 , u2 : User | u1.SSN = u2.SSN and u1 != u2) and
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2)
}
// No users with NOTCONFIRMED billing information
fact noUserWithNotConfirmedBilling {
no u : User | u.billingInformation = NOTCONFIRMED
}
// No duplicated deactivated users
fact noDuplicatedDeactivatedUser {
(no du1 , du2 : DeactivatedUser | du1.id = du2.id and du1 != du2) and
(no du1 , du2 : DeactivatedUser | du1.email = du2.email and du1 != du2) and
(no du1 , du2 : DeactivatedUser | du1.SSN = du2.SSN and du1 != du2) and
(no du1 , du2 : DeactivatedUser | du1.drivingLicence = du2.drivingLicence and du1 != du2)
}
// No cities with the same ID
fact noDuplicatedCities {
no c1 , c2 : City | c1.id = c2.id and c1 != c2
}
// No Parking Areas with the same ID
fact noDuplicatedParkingAreas {
no pa1 , pa2 : ParkingArea | pa1.id = pa2.id and pa1 != pa2
}
// No Recharging Areas with the same ID
fact noDuplicatedRechargingAreas {
no ra1 , ra2 : RechargingArea | ra1.id = ra2.id and ra1 != ra2
}
// No duplicated requests
fact noDuplicatedRMSS{
(no req1 , req2 : RMSS | req1.id = req2.id and req1 != req2) and
(no req1, req2 : RMSS | req1.userID = req2.userID and
req1.carID = req2.carID and req1.startTime = req2.startTime
and req1.endTime = req2.endTime and req1 != req2)
}
fact noDuplicatedReservation{
(no res1 , res2 : Reservation | res1.id = res2.id and res1 != res2) and
(no res1, res2 : Reservation | res1.userID = res2.userID and
res1.carID = res2.carID and res1.startTime = res2.startTime
and res1.endTime = res2.endTime and res1 != res2)
}
fact noDuplicatedRent{
(no ren1 , ren2 : Rent | ren1.id = ren2.id and ren1 != ren2) and
(no ren1, ren2: Rent | ren1.userID = ren2.userID
and ren1.carID = ren2.carID and ren1.startTime = ren2.startTime
and ren1.endTime = ren2.endTime and ren1 != ren2)
}
// Users cannot hold the same reservation
// fact noDifferentUsersForTheSameReservation{
// (all r : RMSS | no u1, u2 : User | u1 !)
//}
// USER -- > RENT : SAME MONEY SAVING OPTION
// No duplicated cars
fact noDuplicatedCars {
(no c1 , c2 : Car | c1.id = c2.id and c1 != c2) and
(no c1 , c2 : Car | c1.plate = c2.plate and c1 != c2) and
(no c1 , c2 : Car | c1.wCode = c2.wCode and c1 != c2)
}
// No ECS with the same ID
fact noDuplicatedECS {
no ecs1 , ecs2 : ECS | ecs1.id = ecs2.id and ecs1 != ecs2
}
// No ADS with the same ID
fact noDuplicatedADS {
no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2
}
// AVAILABLE car
// When a request is active the status of the payment is pending
fact pendingPaymentForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
}
// When a car is RENTED the related RENT is ACTIVE
fact aRentedCarIsRelatedToAnActiveRent {
(all c : Car | c.status = INUSE implies
(one ren : Rent | c.id = ren.carID and ren.status = ACTIVE) and
(no res : Reservation | c.id = res.carID and res.status = ACTIVE)
)
}
fact anActiveRentIsRelatedToARentedCar {
(all ren : Rent | ren.status = ACTIVE implies
(one c : Car | ren.carID = c.id and c.status = INUSE)
)
}
// When a car is RESERVED the related RESERVATION is ACTIVE
fact aReservedCarIsRelatedToAnActiveReservation {
(all c : Car | c.status = RESERVED implies
(one res : Reservation | c.id = res.carID and res.status = ACTIVE) and
(no ren : Rent | c.id = ren.carID and ren.status = ACTIVE)
)
}
fact anActiveReservationIsRelatedToAReservedCar {
(all res : Reservation | res.status = ACTIVE implies
(one c : Car | res.carID = c.id and c.status = RESERVED)
)
}
// When a car is UNAVAILABLE, it cannot be RESERVED
fact noUnavailableReservedCar {
all c : Car | c.status = UNAVAILABLE implies
(no res : Reservation | res.status = ACTIVE and res.carID = c.id)
}
// When a car is AVAILABLE, it cannot be RENTED
fact noUnavailableRentedCar {
all c : Car | c.status = UNAVAILABLE implies
(no ren : Rent | ren.status = ACTIVE and ren.carID = c.id)
}
// When a reservation is EXPIRED, it still remembers the reserved car
fact consistencyOfReservation {
(all res : Reservation | res.status = EXPIRED implies
(one c : Car | res.carID = c.id)
)
}
// When a rent is EXPIRED, it still remembers the rented car
fact consistencyOfRent {
(all ren : Rent | ren.status = EXPIRED implies
(one c : Car | ren.carID = c.id)
)
}
// When a car is INUSE the related RENT is ACTIVE
// When a car is AVAILABLE
// When a car is UNAVAILABLE
//ASSERTION
// The number of active rents is equal to the number of cars in use
assert equalityOfRentedCarsAndActiveRents {
#{r : Rent | r.status = ACTIVE} = #{c : Car | c.status = INUSE}
}
// check equalityOfRentedCarsAndActiveRents for 8 [no counterexamplefound]
// The number of active reservations is equal to the number of cars reserved
assert equalityOfReservedCarsAndActiveReservations {
#{r : Reservation | r.status = ACTIVE} = #{c : Car | c.status = RESERVED}
}
// check equalityOfReservedCarsAndActiveReservations for 8 [no counterexamplefound]
// The number of the Reservation is greater or equal to the number of Rent
assert noRentWithoutReservation{
all u : User |
#{res: Reservation | res.userID = u.id } >= #{ren : Rent | ren.userID = u.id}
}
//check noRentWithoutReservation for 3
assert z{
#{rm : RMSS} >= #{res : Reservation}
}
//check z for 8
assert zz{
#{rm : RMSS} >= #{rn : Rent}
}
//check zz for 3
assert zzz{
#{res : Reservation} < #{req : RMSS}
}
//check zzz for 2
pred show {}
run show for 4 but exactly 1 User, exactly 1 RMSS, exactly 2 Car

141
1.RASD/res/alloy/AlloyPowerEnjoy.als
View File

@ -8,7 +8,8 @@ sig Float {
leftPart : one Int,
rightPart : one Int
} {
rightPart >= 0
leftPart > 0
rightPart > 0
}
sig User {
@ -26,25 +27,25 @@ sig User {
moneySavingOption : one Bool,
request : set RMSS
} {
id >= 0
id > 0
}
sig Car {
id : one Int,
plate : one Stringa,
wCode : one Int,
ecs : one ECS,
ads : one ADS,
location: one Location,
status : one CarStatus
} {
id >= 0
wCode >= 0
id > 0
wCode > 0
}
abstract sig RMSS {
id : one Int,
startTime : one Int,
endTime : one Int,
endTime : lone Int,
cost : one Float,
status : one RequestStatus,
paymentStatus : one PaymentStatus,
@ -53,15 +54,14 @@ abstract sig RMSS {
carPosition : one Stringa,
mSavingOption : one Bool,
car : one Car,
user : one User,
events : set Event
user : one User
} {
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,61 +70,45 @@ sig Rent extends RMSS {}
sig DeactivatedUser extends User {}
sig ECS {
id : one Int,
} {
id > 0
}
sig ADS {
id : one Int
} {
id >= 0
id > 0
}
abstract sig Event {
sig ParkingArea {
id : one Int,
status: one Stringa,
rmss: one RMSS
} {
id >= 0
}
sig Payment extends Event {}
sig Notification extends Event {
message: one Stringa
}
abstract sig Location {
id : one Int,
boundaries : set Int,
latitude : one Float,
longitude : one Float
} {
id >= 0
latitude.leftPart >= 0
longitude.leftPart >= 0
}
sig City extends Location {
name : one Stringa,
zipCode : one Int,
parArea : set ParkingArea
} {
zipCode > 0
}
sig ParkingArea extends Location {
availableCars : one Int,
rechargingArea : one RechargingArea
car : set Car,
rechargingArea : set RechargingArea
} {
availableCars >= 0
id > 0
availableCars > 0
}
sig RechargingArea extends Location {
sig City {
id : one Int,
name : one Stringa,
parkingArea : set ParkingArea
} {
id > 0
}
sig RechargingArea {
id : one Int,
plugs : one Int,
ranking : one Int,
maxRadius : one Int,
address : one Stringa,
isSpecial : one Bool
} {
plugs >= 0
ranking >= 0
maxRadius >= 0
id > 0
plugs > 0
}
// ENUMS
@ -161,18 +145,24 @@ enum RequestStatus {
// In any city there is at least a parking area
fact atLeastAParkingArea {
(all c : City | #c.parArea >= 1)
#ParkingArea >= 1
}
// In any parking area there could be zero or more recharging area
fact presenceOfRechargingArea {
(all p : ParkingArea | #p.rechargingArea >= 0)
#RechargingArea >= 0
}
// In any parking area there could be zero or more cars
fact presenceOfCars {
(all p : ParkingArea | #p.availableCars >= 0)
#Car >= 0
}
// No ECS with the same ID
fact noDuplicatedECS {
(no ecs1 , ecs2 : ECS | ecs1.id = ecs2.id and ecs1 != ecs2)
}
// No ADS with the same ID
@ -180,10 +170,14 @@ fact noDuplicatedADS {
(no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2)
}
// The same ECS cannot be used by two different Cars
fact theSameECSCannotBeUsedByDifferentCars {
no disj c1, c2 : Car | c1.ecs = c2.ecs
}
// The same ADS cannot be used by two different Cars
fact theSameADSCannotBeUsedByDifferentCars {
(no disj c1, c2 : Car | c1.ads = c2.ads)
no disj c1, c2 : Car | c1.ads = c2.ads
}
// No Duplicated Users
@ -194,32 +188,13 @@ fact noDuplicatedUser {
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2)
}
// A reservation and its associated rent have the same user
fact noPhantomResRent {
(all c : Car | c.status = INUSE implies
(no res : Reservation, ren : Rent | res.car = c and ren.car = c and res.user != ren.user)
)
}
// No rent is possible if the reservation payment was denied or pending
fact noRentIfPaymentUncertain {
(all c : Car, res : Reservation| c.status = INUSE and res.car = c and (res.paymentStatus = DENIED or res.paymentStatus = PENDING) implies
(no ren : Rent | ren.car = c)
)
}
// No Users with NOTCONFIRMED Billing Information
fact noUserWithNotConfirmedBilling {
no u : User | u.billingInformation = NOTCONFIRMED
}
// Every rent starts after every reservation
fact noEarlyRent {
(all c : Car, res : Reservation, ren : Rent | c.status = INUSE and res.car = c and ren.car = c implies
ren.startTime >= res.endTime
)
}
// No Cities with the same ID
fact noDuplicatedCities {
no c1 , c2 : City | c1.id = c2.id and c1 != c2
@ -285,12 +260,6 @@ fact pendingPaymentForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
}
// There are no duplicate payments
fact noDuplicatePayments {
(all r1, r2 : RMSS | r1 != r2 and r1.paymentStatus = PENDING and r2.paymentStatus = PENDING implies
(all p1, p2 : Payment | p1 != p2 and p1 in r1.events and p2 in r2.events)
)
}
// No Multiple Users for the same Request
fact noMultipleUsersForTheSameRequest {
no disj u1, u2 : User | u1.request & u2.request != none
@ -298,9 +267,7 @@ fact noMultipleUsersForTheSameRequest {
// The same Request cannot be performed by two different User
fact noDifferentUserForTheSameRequest {
(all u1, u2 : User | u1 != u2 implies
(no r : RMSS | r in u1.request and r in u2.request)
)
all r : RMSS | r in r.user.request
}
// The same User cannot have two ACTIVE Requests

340
1.RASD/res/alloy/seconda prova.als Normal file
View File

@ -0,0 +1,340 @@
module PowerEnjoy
//SIG
sig Stringa {}
sig Float {
leftPart : one Int,
rightPart : one Int
} {
leftPart > 0
rightPart > 0
}
sig User {
id : one Int,
name : one Stringa,
surname : one Stringa,
email : one Stringa,
password : one Stringa,
phone : one Stringa,
address : one Stringa,
SSN : one Stringa,
verificationCode : one Stringa,
drivingLicence : one Stringa,
billingInformation: one BillingInformation,
moneySavingOption : one Bool,
request : set RMSS
} {
id > 0
}
sig Car {
id : one Int,
plate : one Stringa,
wCode : one Int,
ecs : one ECS,
ads : one ADS,
status : one CarStatus
} {
id > 0
wCode > 0
}
abstract sig RMSS {
id : one Int,
startTime : one Int,
endTime : lone Int,
cost : one Float,
status : one RequestStatus,
paymentStatus : one PaymentStatus,
userID : one Int,
userPosition : one Stringa,
carPosition : one Stringa,
mSavingOption : one Bool,
car : one Car,
user : one User
} {
id > 0
startTime > 0
endTime > 0
endTime = none or endTime > 0
userID > 0
endTime > startTime
}
sig Reservation extends RMSS {}
sig Rent extends RMSS {}
sig DeactivatedUser extends User {}
sig ECS {
id : one Int,
} {
id > 0
}
sig ADS {
id : one Int
} {
id > 0
}
sig ParkingArea {
id : one Int,
name : one Stringa,
availableCars : one Int,
car : set Car,
rechargingArea : set RechargingArea
} {
id > 0
availableCars > 0
}
sig City {
id : one Int,
name : one Stringa,
parkingArea : set ParkingArea
} {
id > 0
}
sig RechargingArea {
id : one Int,
plugs : one Int,
address : one Stringa,
isSpecial : one Bool
} {
id > 0
plugs > 0
}
// ENUMS
enum Bool {
TRUE,
FALSE
}
enum BillingInformation {
CONFIRMED,
NOTCONFIRMED
}
enum PaymentStatus {
ACCEPTED,
PENDING,
DENIED
}
enum CarStatus {
AVAILABLE,
RESERVED,
UNAVAILABLE,
INUSE
}
enum RequestStatus {
ACTIVE,
EXPIRED
}
// FACTS
// In any city there is at least a parking area
fact atLeastAParkingArea {
#ParkingArea >= 1
}
// In any parking area there could be zero or more recharging area
fact presenceOfRechargingArea {
#RechargingArea >= 0
}
// In any parking area there could be zero or more cars
fact presenceOfCars {
#Car >= 0
}
// No ECS with the same ID
fact noDuplicatedECS {
(no ecs1 , ecs2 : ECS | ecs1.id = ecs2.id and ecs1 != ecs2)
}
// No ADS with the same ID
fact noDuplicatedADS {
(no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2)
}
// The same ECS cannot be used by two different Cars
fact theSameECSCannotBeUsedByDifferentCars {
no disj c1, c2 : Car | c1.ecs = c2.ecs
}
// The same ADS cannot be used by two different Cars
fact theSameADSCannotBeUsedByDifferentCars {
no disj c1, c2 : Car | c1.ads = c2.ads
}
// No Duplicated Users
fact noDuplicatedUser {
(no u1 , u2 : User | u1.id = u2.id and u1 != u2) and
(no u1 , u2 : User | u1.email = u2.email and u1 != u2) and
(no u1 , u2 : User | u1.SSN = u2.SSN and u1 != u2) and
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2)
}
// No Users with NOTCONFIRMED Billing Information
fact noUserWithNotConfirmedBilling {
no u : User | u.billingInformation = NOTCONFIRMED
}
// No Cities with the same ID
fact noDuplicatedCities {
no c1 , c2 : City | c1.id = c2.id and c1 != c2
}
// No Parking Areas with the same ID
fact noDuplicatedParkingAreas {
no pa1 , pa2 : ParkingArea | pa1.id = pa2.id and pa1 != pa2
}
// No Recharging Areas with the same ID
fact noDuplicatedRechargingAreas {
no ra1 , ra2 : RechargingArea | ra1.id = ra2.id and ra1 != ra2
}
// No Duplicated Requests
fact noDuplicatedRMSS {
(no req1 , req2 : RMSS | req1.id = req2.id and req1 != req2) and
(no req1, req2 : RMSS | req1.userID = req2.userID and
req1.car = req2.car and req1.startTime = req2.startTime
and req1.endTime = req2.endTime and req1 != req2)
}
// No Duplicated Cars
fact noDuplicatedCars {
(no c1 , c2 : Car | c1.id = c2.id and c1 != c2) and
(no c1 , c2 : Car | c1.plate = c2.plate and c1 != c2) and
(no c1 , c2 : Car | c1.wCode = c2.wCode and c1 != c2)
}
// When a car is RENTED the related RENT is ACTIVE and viceversa
fact aRentedCarIsRelatedToAnActiveRent {
(all c : Car | c.status = INUSE implies
(one ren : Rent | ren.car = c and ren.status = ACTIVE) and
(no res : Reservation | res.car = c and res.status = ACTIVE)
) and
(all ren : Rent | ren.status = ACTIVE implies
(one c : Car | ren.car = c and c.status = INUSE)
)
}
// When a car is RESERVED the related RESERVATION is ACTIVE and viceversa
fact aReservedCarIsRelatedToAnActiveReservation {
(all c : Car | c.status = RESERVED implies
(one res : Reservation | res.car = c and res.status = ACTIVE) and
(no ren : Rent | ren.car = c and ren.status = ACTIVE)
) and
(all res : Reservation | res.status = ACTIVE implies
(one c : Car | res.car = c and c.status = RESERVED)
)
}
// When a car is UNAVAILABLE, it cannot be RESERVED nor RENTED
fact noUnavailableReservedCar {
all c : Car | c.status = UNAVAILABLE implies (
(no res : Reservation | res.status = ACTIVE and res.car = c) and
(no ren : Rent | ren.status = ACTIVE and ren.car = c)
)
}
// When a request is ACTIVE the status of the payment is PENDING
fact pendingPaymentForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
}
// NONCANCELLAREOTIUCCIDO
fact noMultipleUserForTheSameRequest {
no disj u1, u2 : User | u1.request & u2.request != none
}
// The same Request cannot be performed by two different User
fact noDifferentUserForTheSameRequest {
all r : RMSS | r in r.user.request
}
// The same User cannot have two ACTIVE Requests
fact theSameUserCannotPerformTwoActiveRequests {
no disj r1, r2 : RMSS | r1.user = r2.user and r1.status = ACTIVE and r2.status = ACTIVE
}
// The same User cannot start two Request contemporary
fact noSimultaneousActions {
no disj r1, r2 : RMSS | r1.user = r2.user and r1.startTime = r2.startTime
}
// Relation between deactivated users and active requests (reservation or rent)
fact noActiveRequestForDeactivatedUser {
(all dU : DeactivatedUser | no r : dU.request | (r.status = ACTIVE))
// No deactivated users can have an active request
}
//Consistency of the MoneySavingOption for the ACTIVE Requests
fact consistencyOfMoneySavingOptionForActiveRequests {
(all u : User | u.request.status = ACTIVE implies u.moneySavingOption = u.request.mSavingOption)
}
// A Rent is possible only as a consequence of a Reservation
fact rentIsAPossibleConsequenceOfReservation{
(all r : Rent | one res : Reservation | res in r.user.request and r.startTime = res.endTime and r.car = res.car)
}
// ASSERTIONS
/******* WORKING *******/
// The number of active rents is equal to the number of cars in use
assert equalityOfRentedCarsAndActiveRents {
#{r : Rent | r.status = ACTIVE} = #{c : Car | c.status = INUSE}
}
// check equalityOfRentedCarsAndActiveRents for 10 [no counterexamplefound]
/******* WORKING *******/
// The number of active reservations is equal to the number of cars reserved
assert equalityOfReservedCarsAndActiveReservations {
#{r : Reservation | r.status = ACTIVE} = #{c : Car | c.status = RESERVED}
}
// check equalityOfReservedCarsAndActiveReservations for 10 //[no counterexamplefound]
/******* WORKING *******/
//The number of the Reservation is greater or equal to the number of Rent
assert noRentWithoutReservation {
all u : User |
#{res: Reservation | res.user = u } >= #{ren : Rent | ren.user = u}
}
// check noRentWithoutReservation for 10 //[no counterexamplefound]
/******* WORKING *******/
//If there is an end time for a Reservation, that must be after the start
assert requestTimeConsistency {
all r : RMSS | r.endTime > 0 implies r.endTime > r.startTime
}
// check requestTimeConsistency for 10 //[no counterexamplefound]
pred show {
#User = 3
#DeactivatedUser = 0
#RMSS = 3
#Car = 2
#{ r : RMSS | r.status = ACTIVE} >= 2
#{ r : Rent | r.status = ACTIVE} >= 1
}
run show for 3

BIN
1.RASD/res/img/ClassD.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 730 KiB

After

Width:  |  Height:  |  Size: 67 KiB

BIN
1.RASD/res/img/alloy_PROVA.pdf Normal file
View File

Binary file not shown.

BIN
1.RASD/res/img/alloy_mondo_1.pdf Normal file
View File

Binary file not shown.

BIN
1.RASD/res/img/alloy_mondo_2.pdf Normal file
View File

Binary file not shown.

BIN
1.RASD/res/img/alloy_mondo_3.pdf Normal file
View File

Binary file not shown.

BIN
1.RASD/res/img/world1.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 815 KiB

BIN
1.RASD/res/img/world2.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 726 KiB

BIN
1.RASD/res/img/world3.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 757 KiB

1682
2.Design Document/DD.lyx
View File

File diff suppressed because it is too large Load Diff

BIN
2.Design Document/res/img/ComponentView.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 474 KiB

After

Width:  |  Height:  |  Size: 751 KiB

4120
3.Integration Test Plan Document/ITPD.lyx
View File

File diff suppressed because it is too large Load Diff

BIN
3.Integration Test Plan Document/res/img/2.4.2 [OLD].png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 663 KiB

BIN
3.Integration Test Plan Document/res/img/2.4.2.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 422 KiB

After

Width:  |  Height:  |  Size: 420 KiB

BIN
3.Integration Test Plan Document/res/img/Account Management 1.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 28 KiB

After

Width:  |  Height:  |  Size: 29 KiB

BIN
3.Integration Test Plan Document/res/img/Account Management 2.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 32 KiB

After

Width:  |  Height:  |  Size: 33 KiB

BIN
3.Integration Test Plan Document/res/img/Car Management 1.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 45 KiB

After

Width:  |  Height:  |  Size: 30 KiB

BIN
3.Integration Test Plan Document/res/img/Car Management 2.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 48 KiB

After

Width:  |  Height:  |  Size: 47 KiB

BIN
3.Integration Test Plan Document/res/img/Events Handler 1.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 49 KiB

After

Width:  |  Height:  |  Size: 49 KiB

BIN
3.Integration Test Plan Document/res/img/Events Handler 2.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 49 KiB

After

Width:  |  Height:  |  Size: 49 KiB

BIN
3.Integration Test Plan Document/res/img/Interfaces 1 bis.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 89 KiB

BIN
3.Integration Test Plan Document/res/img/Interfaces 1.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 84 KiB

After

Width:  |  Height:  |  Size: 52 KiB

BIN
3.Integration Test Plan Document/res/img/Interfaces 2 bis.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 90 KiB

BIN
3.Integration Test Plan Document/res/img/Interfaces 2.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 84 KiB

After

Width:  |  Height:  |  Size: 52 KiB

BIN
3.Integration Test Plan Document/res/img/Reservation Management 1.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 48 KiB

After

Width:  |  Height:  |  Size: 48 KiB

BIN
3.Integration Test Plan Document/res/img/Reservation Management 2.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 47 KiB

After

Width:  |  Height:  |  Size: 47 KiB

12677
4.Project Management/Planning.lyx
View File

File diff suppressed because it is too large Load Diff

BIN
4.Project Management/res/Dependencies.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 25 KiB

BIN
4.Project Management/res/Dependencies.vsdx
View File

Binary file not shown.

BIN
4.Project Management/res/GANTT.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 61 KiB

BIN
4.Project Management/res/GANTT.vsdx
View File

Binary file not shown.

5304
5.Code Inspection/CodeInspection.lyx
View File

File diff suppressed because it is too large Load Diff

BIN
5.Code Inspection/res/FreeMarker.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 24 KiB

BIN
5.Code Inspection/res/Freemarker.vsdx
View File

Binary file not shown.

BIN
5.Code Inspection/res/logopm.pdf
View File

Binary file not shown.

200
5.Code Inspection/src/ProductConfigItemContentWrapper.java
View File

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

189
5.Code Inspection/src/SeoTransform.java
View File

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

231
5.Code Inspection/src/UrlRegexpTransform.java
View File

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

9
README.md
View File

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