| Nome | Sigla | Note |
|---|---|---|
| ACME | ACME | Indica l'azienda AcmeSky |
| Airline service | AIRk | Indica la k-esima compagnia aerea |
| Rent service | RENTt | Indica la t-esima compagnia di noleggio |
| Prontogram | PTG | Indica il servizio di messagistica |
| Bank service | BANK | Indica il servizio bancario |
| Geodistance service | GEO | Indica il servizio di calcolo distanze |
| User | USERx | Indica l'x-esimo utente |
( requestInterest: USERₓ -> ACME ; responseInterest: ACME -> USERₓ )*
|
( queryFlights: ACME -> AIRₖ ; responseFlights: AIRₖ -> ACME )*
|
( sendLastMinute: AIRₖ -> ACME ; responseLastMinute: ACME -> AIRₖ )*
|
( offerToken: ACME -> PTG ; notifyUser: PTG -> USERₓ ;
notifyResponse: USERₓ -> PTG ; messageSended: PTG -> ACME )*
|
(
confirmOffer: USERₓ -> ACME ;
(
(
responseOfferOk: ACME -> USERₓ ;
requestPaymentLink: USERₓ -> ACME ;
bookTickets: ACME -> AIRₖ ;
(
(
responseTickets: AIRₖ -> ACME ;
requestBankLink: ACME -> BANK ;
responselink: BANK -> ACME ;
paymentLink: ACME -> USERₓ ;
(
(
payment: USERₓ -> BANK ;
successPaymentBank: BANK -> ACME ;
(
// Richiesta a Geodistance se costo > 1000€
1
+
(
requestDistance: ACME -> GEO ;
responseDistance: GEO -> ACME ;
( // Richiesta a Rent service se distanza <30Km
1
+
(
(
requestDistanceRent: ACME -> GEO ;
responseDistanceRent: GEO -> ACME ;
)* ;
requestRent: ACME -> RENTₜ ;
responseRent: RENT ₜ-> ACME ;
)
)
)
) ;
SendJourneyReceipt: ACME -> USERₓ;
)
)
)
)
)
)
)*
( requestInterest: USERₓ -> ACME ; responseInterest: ACME -> USERₓ )*
|
( queryFlights: ACME -> AIRₖ ; responseFlights: AIRₖ -> ACME )*
|
( sendLastMinute: AIRₖ -> ACME ; responseLastMinute: ACME -> AIRₖ )*
|
( offerToken: ACME -> PTG ; notifyUser: PTG -> USERₓ ;
notifyResponse: USERₓ -> PTG ; messageSended: PTG -> ACME )*
|
(
confirmOffer: USERₓ -> ACME ;
(
(
responseOfferOk: ACME -> USERₓ ;
requestPaymentLink: USERₓ -> ACME ;
bookTickets: ACME -> AIRₖ ;
(
(
responseTickets: AIRₖ -> ACME ;
requestBankLink: ACME -> BANK ;
responselink: BANK -> ACME ;
paymentLink: ACME -> USERₓ ;
(
(
payment: USERₓ -> BANK ;
successPaymentBank: BANK -> ACME ;
(
// Richiesta a Geodistance se costo > 1000€
1
+
(
requestDistance: ACME -> GEO ;
responseDistance: GEO -> ACME ;
( // Richiesta a Rent service se distanza <30Km
1
+
(
(
requestDistanceRent: ACME -> GEO ;
responseDistanceRent: GEO -> ACME ;
)* ;
requestRent: ACME -> RENTₜ ;
responseRent: RENT ₜ-> ACME ;
)
)
)
) ;
SendJourneyInvoice: ACME -> USERₓ;
)
)
)
)
)
)
)*
Per verificare se la coreografia fornita verifica la proprietà di connessione, dobbiamo scomporla e analizzare ogni composizione, scelta e iterazione sequenziale. Di seguito un'analisi dettagliata della coreografia asincrona precedentemente rappresentata, passo dopo passo: Per quanto riguarda la prima parte della coreografia globale:
( requestInterest: USERₓ -> ACME ; responseInterest: ACME -> USERₓ )*
|
( queryFlights: ACME -> AIRₖ ; responseFlights: AIRₖ -> ACME )*
|
( sendLastMinute: AIRₖ -> ACME ; responseLastMinute: ACME -> AIRₖ )*
|
( offerToken: ACME -> PTG ; notifyUser: PTG -> USERₓ ;
notifyResponse: USERₓ -> PTG ; messageSended: PTG -> ACME )*
La proprietà di connectedness è verificata in quanto si tratta di operazioni parallele, in cui il mittente della prima operazione è il ricevente della seconda operazione e, viceversa, il ricevente della prima operazione è il mittente della seconda e i ruoli rimangono gli stessi.
Per quanto riguarda invece l'operazione confirmOffer:
confirmOffer: USERₓ -> ACME ;
(
// Confirmation of the offer
responseOfferOk: ACME -> USERₓ ;
requestPaymentLink: USERₓ -> ACME ;
bookTickets: ACME -> AIRₖ ;
(
// Booking tickets and payment link generation
responseTickets: AIRₖ -> ACME ;
requestBankLink: ACME -> BANK ;
responselink: BANK -> ACME ;
paymentLink: ACME -> USERₓ ;
(
// Payment process
payment: USERₓ -> BANK ;
successPaymentBank: BANK -> ACME ;
(
// Additional services based on payment amount
1
+
(
requestDistance: ACME -> GEO ;
responseDistance: GEO -> ACME ;
(
1
+
(
requestDistanceRent: ACME -> GEO ;
responseDistanceRent: GEO -> ACME ;
requestRent: ACME -> RENTₜ ;
responseRent: RENTₜ -> ACME ;
)
)
)
) ;
SendJourneyReceipt: ACME -> USERₓ;
)
)
)
confirmOffer: USERₓ -> ACME ;
(
// Confirmation of the offer
responseOfferOk: ACME -> USERₓ ;
requestPaymentLink: USERₓ -> ACME ;
bookTickets: ACME -> AIRₖ ;
(
// Booking tickets and payment link generation
responseTickets: AIRₖ -> ACME ;
requestBankLink: ACME -> BANK ;
responselink: BANK -> ACME ;
paymentLink: ACME -> USERₓ ;
(
// Payment process
payment: USERₓ -> BANK ;
successPaymentBank: BANK -> ACME ;
(
// Additional services based on payment amount
1
+
(
requestDistance: ACME -> GEO ;
responseDistance: GEO -> ACME ;
(
1
+
(
requestDistanceRent: ACME -> GEO ;
responseDistanceRent: GEO -> ACME ;
requestRent: ACME -> RENTₜ ;
responseRent: RENTₜ -> ACME ;
)
)
)
) ;
SendJourneyInvoice: ACME -> USERₓ;
)
)
)
Passo 1: confirmOffer: USERₓ -> ACME ; responseOfferOk: ACME -> USERₓ
Ogni composizione sequenziale si connette appropriatamente con almeno un ruolo condiviso. Ogni scelta assicura che gli stessi ruoli siano coinvolti inizialmente e non crea rami disconnessi. @@ -117,11 +117,11 @@
proj(ReceiveLastMinute, ACME) =
__________________
( sendLastMinute@AIRₖ ; responseLastMinute@AIRₖ )*
proj(RegisterInterest, ACME) =
________________
( requestInterest@USERₓ ; responseInterest@USERₓ )*
proj(SendOffer, ACME) =
__________
( offer@PTG ; 1 ; 1 ; messageSent@PTG )*
proj(confirmOffer, ACME) =
( confirmOffer@USERₓ ;
( _______________ ___________
(responseOfferOk@USERₓ ; requestPaymentLink@USERₓ ; bookTickets@AIRₖ
(
(
responseTickets@AIRₖ ;
______________
requestBankLink@BANK ; responselink@BANK ;
___________
paymentLink@USERₓ ; 1 ;
(
(
1; successPaymentBank@BANK ;
_______________
( 1 + ( requestDistance@GEO ; responseDistance@GEO ;
___________________
( 1 + ( ( requestDistanceRent@GEO ; responseDistanceRent@GEO )* ;
___________
requestRent@RENTₜ ; responseRent@RENTₜ ;
)
)
); __________________
) SendJourneyReceipt@USERₓ
)
)
)
)
)
)
)*
proj(confirmOffer, ACME) =
( confirmOffer@USERₓ ;
( _______________ ___________
(responseOfferOk@USERₓ ; requestPaymentLink@USERₓ ; bookTickets@AIRₖ
(
(
responseTickets@AIRₖ ;
______________
requestBankLink@BANK ; responselink@BANK ;
___________
paymentLink@USERₓ ; 1 ;
(
(
1; successPaymentBank@BANK ;
_______________
( 1 + ( requestDistance@GEO ; responseDistance@GEO ;
___________________
( 1 + ( ( requestDistanceRent@GEO ; responseDistanceRent@GEO )* ;
___________
requestRent@RENTₜ ; responseRent@RENTₜ ;
)
)
); __________________
) SendJourneyInvoice@USERₓ
)
)
)
)
)
)
)*
proj(RegisterInterest, USERₓ) =
_______________
( requestInterest@ACME ; responseInterest@ACME )*
proj(SendOffer, USERₓ) =
______________
( 1 ; notifyUser@PTG ; notifyResponse@PTG ; 1 )*
proj(confirmOffer, USERₓ) =
____________
( confirmOffer@ACME ;
( __________________
( responseOfferOk@ACME ; requestPaymentLink@ACME ; 1 ;
( _______
( 1 ; 1 ; 1 ; paymentLink@ACME ; payment@BANK ;
(
(
1 ; //successPaymentBank: BANK ->ACME
( 1 + ( 1 ; 1 ; //req distance
( 1 + (( 1 ; 1)* ; 1 ; 1 ;))
)
); SendJourneyReceipt@ACME
)
)
)
)
)
)
)*
proj(confirmOffer, USERₓ) =
____________
( confirmOffer@ACME ;
( __________________
( responseOfferOk@ACME ; requestPaymentLink@ACME ; 1 ;
( _______
( 1 ; 1 ; 1 ; paymentLink@ACME ; payment@BANK ;
(
(
1 ; //successPaymentBank: BANK ->ACME
( 1 + ( 1 ; 1 ; //req distance
( 1 + (( 1 ; 1)* ; 1 ; 1 ;))
)
); SendJourneyInvoice@ACME
)
)
)
)
)
)
)*
proj(QueryFlights, AIRₖ) =
_______________
( queryFlights@ACME ; responseFlights@ACME )*
proj(sendLastMinute, AIRₖ) =
______________
( sendLastMinute@ACME ; responseLastMinute@ACME )*