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

View long theorem info. View the proof. 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,

Theorem EXEC

EXEC (a; s) { if okaction(a) then { s := s ; let cmd = a .cmd in if isInit-GetInputRequestData-TravelPlannerCmd(cmd) then Init-GetInputRequestData-TravelPlannerCmd#(a; s) else if isGetFlightOffers-TravelPlannerCmd(cmd) then GetFlightOffers-TravelPlannerCmd#(a; s) else if isRetFlightOffersstate1-TravelPlannerCmd(cmd) then RetFlightOffersstate1-TravelPlannerCmd#(a; s) else if isBookSelectedstate2-TravelPlannerCmd(cmd) then BookSelectedstate2-TravelPlannerCmd#(a; s) else if isDeclassifiedCCD-TravelPlannerCmd(cmd) then DeclassifiedCCD-TravelPlannerCmd#(a; s) else if isOkConfirmBooking-TravelPlannerCmd(cmd) then OkConfirmBooking-TravelPlannerCmd#(a; s) else if isGetFlightOffers-TravelAgencyCmd(cmd) then GetFlightOffers-TravelAgencyCmd#(a; s) else if isRetFlightOffers-TravelAgencyCmd(cmd) then RetFlightOffers-TravelAgencyCmd#(a; s) else if isPayCommission-TravelAgencyCmd(cmd) then PayCommission-TravelAgencyCmd#(a; s) else if isReleaseCCD-CreditCardCenterCmd(cmd) then ReleaseCCD-CreditCardCenterCmd#(a; s) else if isGetDeclassifiedCCD-CreditCardCenterCmd(cmd) then GetDeclassifiedCCD-CreditCardCenterCmd#(a; s) else if isGetFlightOffers-AirlineCmd(cmd) then GetFlightOffers-AirlineCmd#(a; s) else if isBookFlightOfferstate7-AirlineCmd(cmd) then BookFlightOfferstate7-AirlineCmd#(a; s) else if isOkPayCommission-AirlineCmd(cmd) then OkPayCommission-AirlineCmd#(a; s) else if isGetInputRequestData-UserCmd-1(cmd) then GetInputRequestData-UserCmd-1#(a; s) else if isGetSingleSelection-UserCmd-2(cmd) then GetSingleSelection-UserCmd-2#(a; s) else if isConfirmRelease-UserCmd-3(cmd) then ConfirmRelease-UserCmd-3#(a; s) else if isConfirm-UserCmd-4(cmd) then Confirm-UserCmd-4#(a; s) else if isRetFlightOffers-TravelPlannerCmd(cmd) then RetFlightOffers-TravelPlannerCmd#(a; s) else if isBookSelected-TravelPlannerCmd(cmd) then BookSelected-TravelPlannerCmd#(a ; s ) else if isdeclassifyCCD4ASM-CreditCardCenterCmd (cmd) then declassifyCCD4ASM-CreditCardCenterCmd#(a ; s ) else if isafterdeclassifyCCD4ASM-CreditCardCenterCmd (cmd) then afterdeclassifyCCD4ASM-CreditCardCenterCmd#(a ; s ) else if isBookFlightOffer-AirlineCmd (cmd) then BookFlightOffer-AirlineCmd#(a ; s ) else if isBookFlightOfferstate6-AirlineCmd (cmd) then BookFlightOfferstate6-AirlineCmd#(a ; s ) else if isAbort8-UserCmd (cmd) then Abort8-UserCmd#(a ; s ) else if isAbort9-UserCmd (cmd) then Abort9-UserCmd#(a ; s ) } }