data specification 
   using bool , 
         int-mult
 , 
         namefuns , 
         Agentlist
   Message = mkMessage( . .agentlist : Agentlist;  . .content : Content); comment: agents are senders (from) for (standard) commands,
                   and receivers (to) for reply commands;
   Content
   = mkBookFlightOffer( . .id : Integer;  . .ccd : CreditCardDetails) with isBookFlightOffer | 
     mkBookSelected( . .flightOffer : FlightOffer) with isBookSelected | mkConfirm with isConfirm | 
     mkConfirmBooking( . .id : Integer) with isConfirmBooking | mkConfirmRelease( . .what : Data;  . .receiver : String) with isConfirmRelease | 
     mkDeclassifiedCCD( . .ccd : CreditCardDetails) with isDeclassifiedCCD | mkGetDeclassifiedCCD with isGetDeclassifiedCCD | 
     mkGetFlightOffers( . .requestData : RequestData) with isGetFlightOffers | mkGetInputAgent with isGetInputAgent | 
     mkGetInputAirline with isGetInputAirline | mkGetInputBoolean with isGetInputBoolean | mkGetInputCreditCardCenter with isGetInputCreditCardCenter | 
     mkGetInputCreditCardDetails with isGetInputCreditCardDetails | mkGetInputData with isGetInputData | 
     mkGetInputFlightOffer with isGetInputFlightOffer | mkGetInputGPSPos with isGetInputGPSPos | mkGetInputIFlowUtil with isGetInputIFlowUtil | 
     mkGetInputInteger with isGetInputInteger | mkGetInputRequestData with isGetInputRequestData | mkGetInputString with isGetInputString | 
     mkGetInputTravelAgency with isGetInputTravelAgency | mkGetInputTravelPlanner with isGetInputTravelPlanner | 
     mkGetMultipleSelection( . .selection : ListOfData) with isGetMultipleSelection | 
     mkGetSingleSelection( . .selection : ListOfData) with isGetSingleSelection | mkOkConfirmBooking with isOkConfirmBooking | 
     mkOkPayCommission with isOkPayCommission | mkPayCommission with isPayCommission | mkReleaseCCD( . .receiver : String) with isReleaseCCD | 
     mkRetFlightOffers( . .flightOffers : ListOfFlightOffer) with isRetFlightOffers | mkShow( . .data : Data) with isShow | mkStart with isStart
   ;
   Boolean = mkBoolean( . .value : bool);
   CreditCardDetails = mkCreditCardDetails;
   FlightOffer = mkFlightOffer( . .id : Integer;  . .airline : String);
   GPSPos = mkGPSPos( . .latitude : String;  . .longitude : String);
   Integer = mkInteger( . .value : int);
   RequestData = mkRequestData( . .date : String);
   String = mkString( . .value : string);
   Data
   = wrapMessage2Data( . .msg : Message) with isMessage | wrapBoolean2Data( . .Boolean : Boolean) with isBoolean | 
     wrapCreditCardDetails2Data( . .CreditCardDetails : CreditCardDetails) with isCreditCardDetails | 
     wrapFlightOffer2Data( . .FlightOffer : FlightOffer) with isFlightOffer | wrapGPSPos2Data( . .GPSPos : GPSPos) with isGPSPos | 
     wrapInteger2Data( . .Integer : Integer) with isInteger | wrapRequestData2Data( . .RequestData : RequestData) with isRequestData | 
     wrapString2Data( . .String : String) with isString | 
     wrapListOfFlightOffer2Data( . .ListOfFlightOffer : ListOfFlightOffer) with isListOfFlightOffer | 
     wrapListOfGPSPos2Data( . .ListOfGPSPos : ListOfGPSPos) with isListOfGPSPos | wrapListOfData2Data( . .ListOfData : ListOfData) with isListOfData | 
     wrapAgent2Data( . .Agent : Agent) with isAgent | mkNat( . .nat : nat) with isNat | mkDataPair( . .1 : Data;  . .2 : Data) with isPair | null
   ;
   ListOfFlightOffer = [] |  . + . ( . .first : FlightOffer;  . .rest : ListOfFlightOffer) prio 9;
   ListOfGPSPos = [] |  . + . ( . .first : GPSPos;  . .rest : ListOfGPSPos) prio 9;
   ListOfData = [] |  . + . ( . .first : Data;  . .rest : ListOfData) prio 9;
   variables 
      d, d0, d1 : Data; 
      dl, dl0, dl1, dl2, dl3, dl4, dl5, dl6, dl7, dl8, dl9, dl10 : ListOfData; 
      msg : Message; 
      cntnt, cntnt0, cntnt1 : Content; 
      a_Boolean, a_Boolean0, a_Boolean1, a_Boolean2 : Boolean; 
      a_CreditCardDetails, a_CreditCardDetails0, a_CreditCardDetails1, a_CreditCardDetails2 : CreditCardDetails; 
      a_FlightOffer, a_FlightOffer0, a_FlightOffer1, a_FlightOffer2 : FlightOffer; 
      a_GPSPos, a_GPSPos0, a_GPSPos1, a_GPSPos2 : GPSPos; 
      a_Integer, a_Integer0, a_Integer1, a_Integer2 : Integer; 
      a_RequestData, a_RequestData0, a_RequestData1, a_RequestData2 : RequestData; 
      a_String, a_String0, a_String1, a_String2 : String; 
      a_ListOfFlightOffer, a_ListOfFlightOffer0 : ListOfFlightOffer; 
      a_ListOfGPSPos, a_ListOfGPSPos0 : ListOfGPSPos; 
      a_ListOfData, a_ListOfData0 : ListOfData; 
   size functions # . : ListOfData → nat;
   order predicates  . < . : ListOfData × ListOfData;
end data specification