[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification command
data specification 
   using exAgent
   command
   = Init-GetInputRequestData-TravelPlannerCmd with isInit-GetInputRequestData-TravelPlannerCmd | 
     GetFlightOffers-TravelPlannerCmd with isGetFlightOffers-TravelPlannerCmd | 
     RetFlightOffersstate1-TravelPlannerCmd with isRetFlightOffersstate1-TravelPlannerCmd | 
     BookSelectedstate2-TravelPlannerCmd with isBookSelectedstate2-TravelPlannerCmd | 
     DeclassifiedCCD-TravelPlannerCmd with isDeclassifiedCCD-TravelPlannerCmd | 
     OkConfirmBooking-TravelPlannerCmd with isOkConfirmBooking-TravelPlannerCmd comment: reply; | 
     GetFlightOffers-TravelAgencyCmd with isGetFlightOffers-TravelAgencyCmd | 
     RetFlightOffers-TravelAgencyCmd with isRetFlightOffers-TravelAgencyCmd comment: reply; | 
     PayCommission-TravelAgencyCmd with isPayCommission-TravelAgencyCmd | ReleaseCCD-CreditCardCenterCmd with isReleaseCCD-CreditCardCenterCmd | 
     GetDeclassifiedCCD-CreditCardCenterCmd with isGetDeclassifiedCCD-CreditCardCenterCmd | 
     GetFlightOffers-AirlineCmd with isGetFlightOffers-AirlineCmd | BookFlightOfferstate7-AirlineCmd with isBookFlightOfferstate7-AirlineCmd | 
     OkPayCommission-AirlineCmd with isOkPayCommission-AirlineCmd comment: reply; | GetInputRequestData-UserCmd-1 with isGetInputRequestData-UserCmd-1 | 
     GetSingleSelection-UserCmd-2 with isGetSingleSelection-UserCmd-2 | ConfirmRelease-UserCmd-3 with isConfirmRelease-UserCmd-3 | 
     Confirm-UserCmd-4 with isConfirm-UserCmd-4 | RetFlightOffers-TravelPlannerCmd with isRetFlightOffers-TravelPlannerCmd comment: reply; | 
     BookSelected-TravelPlannerCmd with isBookSelected-TravelPlannerCmd | 
     declassifyCCD4ASM-CreditCardCenterCmd with isdeclassifyCCD4ASM-CreditCardCenterCmd | 
     afterdeclassifyCCD4ASM-CreditCardCenterCmd with isafterdeclassifyCCD4ASM-CreditCardCenterCmd | 
     BookFlightOffer-AirlineCmd with isBookFlightOffer-AirlineCmd | BookFlightOfferstate6-AirlineCmd with isBookFlightOfferstate6-AirlineCmd | 
     Abort8-UserCmd with isAbort8-UserCmd | Abort9-UserCmd with isAbort9-UserCmd
   ;
   variables 
      cmd, cmd0, cmd1, cmd2 : command; 
end data specification