Compare commits

..

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

43 changed files with 8983 additions and 27937 deletions

File diff suppressed because it is too large Load Diff

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

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

View File

@ -8,8 +8,9 @@ sig Float {
leftPart : one Int, leftPart : one Int,
rightPart : one Int rightPart : one Int
} { } {
rightPart >= 0 leftPart > 0
} rightPart > 0
}
sig User { sig User {
id : one Int, id : one Int,
@ -26,25 +27,25 @@ sig User {
moneySavingOption : one Bool, moneySavingOption : one Bool,
request : set RMSS request : set RMSS
} { } {
id >= 0 id > 0
} }
sig Car { sig Car {
id : one Int, id : one Int,
plate : one Stringa, plate : one Stringa,
wCode : one Int, wCode : one Int,
ecs : one ECS,
ads : one ADS, ads : one ADS,
location: one Location,
status : one CarStatus status : one CarStatus
} { } {
id >= 0 id > 0
wCode >= 0 wCode > 0
} }
abstract sig RMSS { abstract sig RMSS {
id : one Int, id : one Int,
startTime : one Int, startTime : one Int,
endTime : one Int, endTime : lone Int,
cost : one Float, cost : one Float,
status : one RequestStatus, status : one RequestStatus,
paymentStatus : one PaymentStatus, paymentStatus : one PaymentStatus,
@ -53,15 +54,14 @@ abstract sig RMSS {
carPosition : one Stringa, carPosition : one Stringa,
mSavingOption : one Bool, mSavingOption : one Bool,
car : one Car, car : one Car,
user : one User, user : one User
events : set Event
} { } {
id >= 0 id > 0
startTime >= 0 startTime > 0
endTime >= 0 endTime > 0
endTime = none or endTime >= 0 endTime = none or endTime > 0
userID >= 0 userID > 0
endTime >= startTime endTime > startTime
} }
sig Reservation extends RMSS {} sig Reservation extends RMSS {}
@ -70,61 +70,45 @@ sig Rent extends RMSS {}
sig DeactivatedUser extends User {} sig DeactivatedUser extends User {}
sig ECS {
id : one Int,
} {
id > 0
}
sig ADS { sig ADS {
id : one Int id : one Int
} { } {
id >= 0 id > 0
} }
abstract sig Event { sig ParkingArea {
id : one Int, id : one Int,
status: one Stringa, name : one Stringa,
rmss: one RMSS availableCars : one Int,
car : set Car,
rechargingArea : set RechargingArea
} { } {
id >= 0 id > 0
availableCars > 0
} }
sig Payment extends Event {} sig City {
id : one Int,
sig Notification extends Event { name : one Stringa,
message: one Stringa parkingArea : set ParkingArea
}
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 City extends Location { sig RechargingArea {
name : one Stringa, id : one Int,
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, plugs : one Int,
ranking : one Int, address : one Stringa,
maxRadius : one Int,
isSpecial : one Bool isSpecial : one Bool
} { } {
plugs >= 0 id > 0
ranking >= 0 plugs > 0
maxRadius >= 0
} }
// ENUMS // ENUMS
@ -161,18 +145,24 @@ enum RequestStatus {
// In any city there is at least a parking area // In any city there is at least a parking area
fact atLeastAParkingArea { fact atLeastAParkingArea {
(all c : City | #c.parArea >= 1) #ParkingArea >= 1
} }
// In any parking area there could be zero or more recharging area // In any parking area there could be zero or more recharging area
fact presenceOfRechargingArea { fact presenceOfRechargingArea {
(all p : ParkingArea | #p.rechargingArea >= 0) #RechargingArea >= 0
} }
// In any parking area there could be zero or more cars // In any parking area there could be zero or more cars
fact presenceOfCars { 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 // No ADS with the same ID
@ -180,10 +170,14 @@ fact noDuplicatedADS {
(no ads1 , ads2 : ADS | ads1.id = ads2.id and ads1 != ads2) (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 // The same ADS cannot be used by two different Cars
fact theSameADSCannotBeUsedByDifferentCars { fact theSameADSCannotBeUsedByDifferentCars {
(no disj c1, c2 : Car | c1.ads = c2.ads) no disj c1, c2 : Car | c1.ads = c2.ads
} }
// No Duplicated Users // No Duplicated Users
@ -194,32 +188,13 @@ fact noDuplicatedUser {
(no u1 , u2 : User | u1.drivingLicence = u2.drivingLicence and u1 != u2) (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 // No Users with NOTCONFIRMED Billing Information
fact noUserWithNotConfirmedBilling { fact noUserWithNotConfirmedBilling {
no u : User | u.billingInformation = NOTCONFIRMED 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 // No Cities with the same ID
fact noDuplicatedCities { fact noDuplicatedCities {
no c1 , c2 : City | c1.id = c2.id and c1 != c2 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) (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 // No Multiple Users for the same Request
fact noMultipleUsersForTheSameRequest { fact noMultipleUsersForTheSameRequest {
no disj u1, u2 : User | u1.request & u2.request != none 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 // The same Request cannot be performed by two different User
fact noDifferentUserForTheSameRequest { fact noDifferentUserForTheSameRequest {
(all u1, u2 : User | u1 != u2 implies all r : RMSS | r in r.user.request
(no r : RMSS | r in u1.request and r in u2.request)
)
} }
// The same User cannot have two ACTIVE Requests // The same User cannot have two ACTIVE Requests

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

Binary file not shown.

Before

Width:  |  Height:  |  Size: 730 KiB

After

Width:  |  Height:  |  Size: 67 KiB

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Before

Width:  |  Height:  |  Size: 815 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 726 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 757 KiB

File diff suppressed because it is too large Load Diff

Binary file not shown.

Before

Width:  |  Height:  |  Size: 474 KiB

After

Width:  |  Height:  |  Size: 751 KiB

File diff suppressed because it is too large Load Diff

Binary file not shown.

After

Width:  |  Height:  |  Size: 663 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 422 KiB

After

Width:  |  Height:  |  Size: 420 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 28 KiB

After

Width:  |  Height:  |  Size: 29 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 32 KiB

After

Width:  |  Height:  |  Size: 33 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 45 KiB

After

Width:  |  Height:  |  Size: 30 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 48 KiB

After

Width:  |  Height:  |  Size: 47 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.

After

Width:  |  Height:  |  Size: 89 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 84 KiB

After

Width:  |  Height:  |  Size: 52 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 90 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 84 KiB

After

Width:  |  Height:  |  Size: 52 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.

Before

Width:  |  Height:  |  Size: 25 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 61 KiB

Binary file not shown.

File diff suppressed because it is too large Load Diff

Binary file not shown.

Before

Width:  |  Height:  |  Size: 24 KiB

Binary file not shown.

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

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

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

View File

@ -1,8 +1 @@
#PowerEnjoy https://etherpad.wikimedia.org/p/ingdaje2
----------------------------------------
# PDF
I PDF generati nelle cartelle delle consegne vengono automaticamente ignorati. Per avere dei PDF pronti, bisogna inserirli nella cartella `Deliveries` nella root.
# Pad Idee
Link [qui](https://etherpad.wikimedia.org/p/ingdaje2)