Modeling
System Choreography
Global formal choreography specification and multi-line indented role projections for all 8 participants of ACME Mobility.
Choreography Participants
🚕
Rental Service
RS
👤
User
User
🏦
Bank Service
B
🚏
Station Service
S
🚗
Fleet Management
FM
📍
Tracking Service
TS
🔋
Battery Monitoring
BMS
🔧
Logistic Service
LS
Complete Global Formal Specification
The following formal algebra specification describes the complete message interaction sequence across all scenarios:
// INITIAL PHASE: Display available vehicles
map_opening: User -> RS;
return_vehicles: RS -> User;
(
// ========================================================================
// SCENARIO A: INSTANT RENTAL (QR Code Scan)
// ========================================================================
(
scanning: User -> RS;
// --- BANK DEPOSIT PRE-AUTHORIZATION ---
block_money: RS -> B;
(
// BRANCH A1: Pre-authorization Granted (Happy Path)
(
send_token: B -> RS;
// --- START FLEET MANAGEMENT MONITORING ---
start_monitoring: RS -> FM;
(
(
start_tracking: FM -> TS;
ack_start_tracking: TS -> FM
)
|
(
start_battery_monitoring: FM -> BMS;
ack_start_battery_monitoring: BMS -> FM
)
);
ack_monitoring: FM -> RS;
// --- UNLOCK PHYSICAL VEHICLE ---
unlock_vehicle: RS -> S;
vehicle_unlocked: S -> RS;
// --- CONFIRM RENTAL STARTED ---
ack_rental_started: RS -> User;
// --- TELEMETRY MONITORING LOOP DURING RIDE ---
(
request_update: User -> RS;
trigger_read: RS -> FM;
(
(
request_position: FM -> TS;
send_position_updated: TS -> FM
)
|
(
request_battery_status: FM -> BMS;
send_battery_status_updated: BMS -> FM
)
);
telemetry_update: FM -> RS;
vehicle_status_updated: RS -> User
)*;
// --- END RIDE ---
end_ride: User -> RS;
// --- LOCK VEHICLE ---
lock_vehicle: RS -> S;
vehicle_locked: S -> RS;
// --- STOP MONITORING ---
stop_monitoring: RS -> FM;
(
(
stop_tracking: FM -> TS;
ack_stop_tracking: TS -> FM
)
|
(
stop_battery_monitoring: FM -> BMS;
ack_stop_battery_monitoring: BMS -> FM
)
);
ack_stop_monitoring: FM -> RS;
// --- FINAL SETTLEMENT ---
request_final_payment: RS -> B;
(
ack_money_unlocked: B -> RS
|
ack_charge_sent: B -> RS
);
// --- RIDE SUMMARY ---
rental_summary: RS -> User;
// --- DAMAGE REPORTING & RECHARGING ---
(
// Option A: User Damage Report
(
send_report: User -> RS;
vehicle_in_queue: RS -> LS;
ack_vehicle_queued: LS -> RS;
ack_receive_report: RS -> User
)
+
// Option B: No Damage Report -> Recharging Evaluation
(
no_report_written: User -> RS;
(
(
recharge_request: RS -> S;
vehicle_recharged: S -> RS
)
+
(
no_recharge_needed: RS -> S;
ack_no_recharge: S -> RS
)
)
)
)
)
+
// BRANCH A2: Insufficient Funds Error
(
send_error: B -> RS;
send_error_message: RS -> User
)
)
)
+
// ========================================================================
// SCENARIO B: SHORT RESERVATION (30-minute booking window)
// ========================================================================
(
booking: User -> RS;
// --- BANK DEPOSIT PRE-AUTHORIZATION ---
block_money: RS -> B;
(
// BRANCH B1: Pre-authorization Granted
(
send_token: B -> RS;
// --- RESERVATION CONFIRMATION ---
ack_reservation: RS -> User;
(
// SCENARIO B1.1: EXPLICIT CANCELLATION
(
cancel_reservation: User -> RS;
(
(
unlock_money: RS -> B;
ack_money_unlocked: B -> RS
)
+
(
charge_money_block: RS -> B;
ack_charge_money_block: B -> RS
)
);
reservation_cancelled: RS -> User
)
+
// SCENARIO B1.2: TIMEOUT - NO SHOW (30 minutes expired)
(
timeout_message: RS -> User;
charge_money_block: RS -> B;
ack_charge_money_block: B -> RS;
reservation_cancelled: RS -> User
)
+
// SCENARIO B1.3: VEHICLE PICKUP (Happy Path)
(
scanning: User -> RS;
start_monitoring: RS -> FM;
(
(
start_tracking: FM -> TS;
ack_start_tracking: TS -> FM
)
|
(
start_battery_monitoring: FM -> BMS;
ack_start_battery_monitoring: BMS -> FM
)
);
ack_monitoring: FM -> RS;
unlock_vehicle: RS -> S;
vehicle_unlocked: S -> RS;
ack_rental_started: RS -> User;
(
request_update: User -> RS;
trigger_read: RS -> FM;
(
(
request_position: FM -> TS;
send_position_updated: TS -> FM
)
|
(
request_battery_status: FM -> BMS;
send_battery_status_updated: BMS -> FM
)
);
telemetry_update: FM -> RS;
vehicle_status_updated: RS -> User
)*;
end_ride: User -> RS;
lock_vehicle: RS -> S;
vehicle_locked: S -> RS;
stop_monitoring: RS -> FM;
(
(
stop_tracking: FM -> TS;
ack_stop_tracking: TS -> FM
)
|
(
stop_battery_monitoring: FM -> BMS;
ack_stop_battery_monitoring: BMS -> FM
)
);
ack_stop_monitoring: FM -> RS;
request_final_payment: RS -> B;
(
ack_money_unlocked: B -> RS
|
ack_charge_sent: B -> RS
);
rental_summary: RS -> User;
(
(
send_report: User -> RS;
vehicle_in_queue: RS -> LS;
ack_vehicle_queued: LS -> RS;
ack_receive_report: RS -> User
)
+
(
no_report_written: User -> RS;
(
(
recharge_request: RS -> S;
vehicle_recharged: S -> RS
)
+
(
no_recharge_needed: RS -> S;
ack_no_recharge: S -> RS
)
)
)
)
)
)
)
+
// BRANCH B2: Insufficient Funds Error (Booking)
(
send_error: B -> RS;
send_error_message: RS -> User
)
)
)
)
Indented Multi-line Role Projections
Expand each participant accordion below to view its complete, multi-line indented local projection:
// INITIAL PHASE
map_opening?User;
return_vehicles!User;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
scanning?User;
// Deposit Pre-authorization
block_money!B;
(
(
send_token?B;
// Start Monitoring
start_monitoring!FM;
1; 1; 1; 1; // Skip FM-TS/BMS internal interactions
ack_monitoring?FM;
// Unlock Vehicle
unlock_vehicle!S;
vehicle_unlocked?S;
ack_rental_started!User;
// Monitoring Loop
(
request_update?User;
trigger_read!FM;
1; // Skip FM-TS/BMS internal interactions
telemetry_update?FM;
vehicle_status_updated!User
)*;
// End Ride
end_ride?User;
lock_vehicle!S;
vehicle_locked?S;
// Stop Monitoring
stop_monitoring!FM;
1; 1; 1; 1; // Skip FM-TS/BMS internal interactions
ack_stop_monitoring?FM;
// Final Settlement
request_final_payment!B;
(ack_money_unlocked?B | ack_charge_sent?B);
rental_summary!User;
// Damage & Recharge Management
(
(
send_report?User;
vehicle_in_queue!LS;
ack_vehicle_queued?LS;
ack_receive_report!User
)
+
(
no_report_written?User;
(
(recharge_request!S; vehicle_recharged?S)
+
(no_recharge_needed!S; ack_no_recharge?S)
)
)
)
)
+
(
send_error?B;
send_error_message!User
)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
booking?User;
block_money!B;
(
(
send_token?B;
ack_reservation!User;
(
// B1: Cancellation
(
cancel_reservation?User;
(
(unlock_money!B; ack_money_unlocked?B)
+
(charge_money_block!B; ack_charge_money_block?B)
);
reservation_cancelled!User
)
+
// B2: Timeout
(
timeout_message!User;
charge_money_block!B;
ack_charge_money_block?B;
reservation_cancelled!User
)
+
// B3: Pickup
(
scanning?User;
start_monitoring!FM; 1; 1; 1; 1; ack_monitoring?FM;
unlock_vehicle!S; vehicle_unlocked?S;
ack_rental_started!User;
(request_update?User; trigger_read!FM; 1; telemetry_update?FM; vehicle_status_updated!User)*;
end_ride?User;
lock_vehicle!S; vehicle_locked?S;
stop_monitoring!FM; 1; 1; 1; 1; ack_stop_monitoring?FM;
request_final_payment!B;
(ack_money_unlocked?B | ack_charge_sent?B);
rental_summary!User;
(
(send_report?User; vehicle_in_queue!LS; ack_vehicle_queued?LS; ack_receive_report!User)
+
(no_report_written?User; ((recharge_request!S; vehicle_recharged?S) + (no_recharge_needed!S; ack_no_recharge?S)))
)
)
)
)
+
(
send_error?B;
send_error_message!User
)
)
)
)
// INITIAL PHASE
map_opening!RS;
return_vehicles?RS;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
scanning!RS;
1; // Skip block_money
(
(
1; // Skip send_token
1; 1; 1; 1; 1; 1; // Skip start_monitoring
1; 1; // Skip unlock
ack_rental_started?RS;
// Monitoring Loop
(
request_update!RS;
1; 1; 1;
vehicle_status_updated?RS
)*;
end_ride!RS;
1; 1; // Skip lock
1; 1; 1; 1; 1; 1; // Skip stop_monitoring
1; (1 | 1); // Skip final settlement
rental_summary?RS;
(
(send_report!RS; 1; 1; ack_receive_report?RS)
+
(no_report_written!RS; ((1; 1) + (1; 1)))
)
)
+
(
1; // Skip send_error
send_error_message?RS
)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
booking!RS;
1; // Skip block_money
(
(
1; // Skip send_token
ack_reservation?RS;
(
// B1: Cancellation
(
cancel_reservation!RS;
((1; 1) + (1; 1));
reservation_cancelled?RS
)
+
// B2: Timeout
(
timeout_message?RS;
1; 1;
reservation_cancelled?RS
)
+
// B3: Pickup
(
scanning!RS;
1; 1; 1; 1; 1; 1; // Skip start_monitoring
1; 1; // Skip unlock
ack_rental_started?RS;
(request_update!RS; 1; 1; 1; vehicle_status_updated?RS)*;
end_ride!RS;
1; 1; // Skip lock
1; 1; 1; 1; 1; 1; // Skip stop_monitoring
1; (1 | 1); // Skip final settlement
rental_summary?RS;
(
(send_report!RS; 1; 1; ack_receive_report?RS)
+
(no_report_written!RS; ((1; 1) + (1; 1)))
)
)
)
)
+
(
1; // Skip send_error
send_error_message?RS
)
)
)
)
// INITIAL PHASE
1; 1;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
1; // Skip scanning
block_money?RS;
(
(
send_token!RS;
1; 1; 1; 1; 1; 1; // Skip monitoring
1; 1; // Skip unlock
1; // Skip ack rental
(1; 1; 1; 1; 1)*; // Skip loop
1; // Skip end_ride
1; 1; // Skip lock
1; 1; 1; 1; 1; 1; // Skip stop monitoring
// Final Settlement
request_final_payment?RS;
(ack_money_unlocked!RS | ack_charge_sent!RS);
1; // Skip rental_summary
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
+
(
send_error!RS;
1 // Skip send_error_message
)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
1; // Skip booking
block_money?RS;
(
(
send_token!RS;
1; // Skip ack_reservation
(
// B1: Cancellation
(
1; // Skip cancel_reservation
(
(unlock_money?RS; ack_money_unlocked!RS)
+
(charge_money_block?RS; ack_charge_money_block!RS)
);
1 // Skip reservation_cancelled
)
+
// B2: Timeout
(
1; // Skip timeout_message
charge_money_block?RS;
ack_charge_money_block!RS;
1 // Skip reservation_cancelled
)
+
// B3: Pickup
(
1; // Skip scanning
1; 1; 1; 1; 1; 1; // Skip monitoring
1; 1; // Skip unlock
1; // Skip ack rental
(1; 1; 1; 1; 1)*; // Skip loop
1; // Skip end_ride
1; 1; // Skip lock
1; 1; 1; 1; 1; 1; // Skip stop monitoring
request_final_payment?RS;
(ack_money_unlocked!RS | ack_charge_sent!RS);
1; // Skip rental_summary
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
)
)
+
(
send_error!RS;
1 // Skip send_error_message
)
)
)
)
// INITIAL PHASE
1; 1;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
1; 1;
(
(
1; 1; 1; 1; 1; 1; 1;
unlock_vehicle?RS;
vehicle_unlocked!RS;
1;
(1; 1; 1; 1; 1)*;
1;
lock_vehicle?RS;
vehicle_locked!RS;
1; 1; 1; 1; 1; 1;
1; (1 | 1);
1;
(
(1; 1; 1; 1)
+
(
1;
(
(recharge_request?RS; vehicle_recharged!RS)
+
(no_recharge_needed?RS; ack_no_recharge!RS)
)
)
)
)
+
(1; 1)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
1; 1;
(
(
1; 1;
(
(1; ((1; 1) + (1; 1)); 1) + (1; 1; 1; 1)
+
(
1; 1; 1; 1; 1; 1; 1;
unlock_vehicle?RS; vehicle_unlocked!RS;
1; (1; 1; 1; 1; 1)*; 1;
lock_vehicle?RS; vehicle_locked!RS;
1; 1; 1; 1; 1; 1; 1; (1 | 1); 1;
(
(1; 1; 1; 1)
+
(1; ((recharge_request?RS; vehicle_recharged!RS) + (no_recharge_needed?RS; ack_no_recharge!RS)))
)
)
)
)
+
(1; 1)
)
)
)
// INITIAL PHASE
1; 1;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
1; 1;
(
(
1;
start_monitoring?RS;
(
(start_tracking!TS; ack_start_tracking?TS)
|
(start_battery_monitoring!BMS; ack_start_battery_monitoring?BMS)
);
ack_monitoring!RS;
1; 1; 1;
(
1; trigger_read?RS;
((request_position!TS; send_position_updated?TS) | (request_battery_status!BMS; send_battery_status_updated?BMS));
telemetry_update!RS;
1
)*;
1; 1; 1;
stop_monitoring?RS;
(
(stop_tracking!TS; ack_stop_tracking?TS)
|
(stop_battery_monitoring!BMS; ack_stop_battery_monitoring?BMS)
);
ack_stop_monitoring!RS;
1; (1 | 1); 1;
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
+
(1; 1)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
1; 1;
(
(
1; 1;
(
(1; ((1; 1) + (1; 1)); 1) + (1; 1; 1; 1)
+
(
1;
start_monitoring?RS;
(
(start_tracking!TS; ack_start_tracking?TS)
|
(start_battery_monitoring!BMS; ack_start_battery_monitoring?BMS)
);
ack_monitoring!RS;
1; 1; 1;
(1; trigger_read?RS; ((request_position!TS; send_position_updated?TS) | (request_battery_status!BMS; send_battery_status_updated?BMS)); telemetry_update!RS; 1)*;
1; 1; 1;
stop_monitoring?RS;
(
(stop_tracking!TS; ack_stop_tracking?TS)
|
(stop_battery_monitoring!BMS; ack_stop_battery_monitoring?BMS)
);
ack_stop_monitoring!RS;
1; (1 | 1); 1;
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
)
)
+
(1; 1)
)
)
)
// INITIAL PHASE
1; 1;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
1; 1;
(
(
1; 1;
((start_tracking?FM; ack_start_tracking!FM) | (1; 1));
1; 1; 1; 1;
(1; 1; ((request_position?FM; send_position_updated!FM) | (1; 1)); 1; 1)*;
1; 1; 1; 1;
((stop_tracking?FM; ack_stop_tracking!FM) | (1; 1));
1; 1; (1 | 1); 1;
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
+
(1; 1)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
1; 1;
(
(
1; 1;
(
(1; ((1; 1) + (1; 1)); 1) + (1; 1; 1; 1)
+
(
1; 1;
((start_tracking?FM; ack_start_tracking!FM) | (1; 1));
1; 1; 1;
(1; 1; ((request_position?FM; send_position_updated!FM) | (1; 1)); 1; 1)*;
1; 1; 1; 1;
((stop_tracking?FM; ack_stop_tracking!FM) | (1; 1));
1; 1; (1 | 1); 1;
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
)
)
+
(1; 1)
)
)
)
// INITIAL PHASE
1; 1;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
1; 1;
(
(
1; 1;
((1; 1) | (start_battery_monitoring?FM; ack_start_battery_monitoring!FM));
1; 1; 1; 1;
(1; 1; ((1; 1) | (request_battery_status?FM; send_battery_status_updated!FM)); 1; 1)*;
1; 1; 1; 1;
((1; 1) | (stop_battery_monitoring?FM; ack_stop_battery_monitoring!FM));
1; 1; (1 | 1); 1;
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
+
(1; 1)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
1; 1;
(
(
1; 1;
(
(1; ((1; 1) + (1; 1)); 1) + (1; 1; 1; 1)
+
(
1; 1;
((1; 1) | (start_battery_monitoring?FM; ack_start_battery_monitoring!FM));
1; 1; 1;
(1; 1; ((1; 1) | (request_battery_status?FM; send_battery_status_updated!FM)); 1; 1)*;
1; 1; 1; 1;
((1; 1) | (stop_battery_monitoring?FM; ack_stop_battery_monitoring!FM));
1; 1; (1 | 1); 1;
((1; 1; 1; 1) + (1; ((1; 1) + (1; 1))))
)
)
)
+
(1; 1)
)
)
)
// INITIAL PHASE
1; 1;
(
// ====== SCENARIO A: INSTANT RENTAL ======
(
1; 1;
(
(
1; 1; 1; 1; 1; 1; 1; 1; 1;
(1; 1; 1; 1; 1)*;
1; 1; 1; 1; 1; 1; 1; 1; 1; (1 | 1); 1;
(
(
1; // Skip send_report (User-RS)
vehicle_in_queue?RS;
ack_vehicle_queued!RS;
1 // Skip ack_receive_report (RS-User)
)
+
(
1; // Skip no_report_written
((1; 1) + (1; 1))
)
)
)
+
(1; 1)
)
)
+
// ====== SCENARIO B: SHORT RESERVATION ======
(
1; 1;
(
(
1; 1;
(
(1; ((1; 1) + (1; 1)); 1) + (1; 1; 1; 1)
+
(
1; 1; 1; 1; 1; 1; 1; 1; 1;
(1; 1; 1; 1; 1)*;
1; 1; 1; 1; 1; 1; 1; 1; 1; (1 | 1); 1;
(
(1; vehicle_in_queue?RS; ack_vehicle_queued!RS; 1)
+
(1; ((1; 1) + (1; 1)))
)
)
)
)
+
(1; 1)
)
)
)