enrich action with
   predicates 
      okaction : action;
   
   axioms 
      ok-Init-GetInputRequestData-TravelPlannerCmd
      : ⊦ 
        okaction(Action(ag0, Init-GetInputRequestData-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isInit-GetInputRequestData-TravelPlannerCmd
      : ⊦ 
          isInit-GetInputRequestData-TravelPlannerCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-GetFlightOffers-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, GetFlightOffers-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isGetFlightOffers-TravelPlannerCmd
      :  ⊦ isGetFlightOffers-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-RetFlightOffersstate1-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, RetFlightOffersstate1-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isRetFlightOffersstate1-TravelPlannerCmd
      : ⊦ 
          isRetFlightOffersstate1-TravelPlannerCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-BookSelectedstate2-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, BookSelectedstate2-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isBookSelectedstate2-TravelPlannerCmd
      : ⊦ 
          isBookSelectedstate2-TravelPlannerCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-DeclassifiedCCD-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, DeclassifiedCCD-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isDeclassifiedCCD-TravelPlannerCmd
      : ⊦ 
          isDeclassifiedCCD-TravelPlannerCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-OkConfirmBooking-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, OkConfirmBooking-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isOkConfirmBooking-TravelPlannerCmd
      :  ⊦ isOkConfirmBooking-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-GetFlightOffers-TravelAgencyCmd
      :  ⊦ okaction(Action(ag0, GetFlightOffers-TravelAgencyCmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exTravelAgency(ag1));
      used for : s, ls;
       
      ok-isGetFlightOffers-TravelAgencyCmd
      :  ⊦ isGetFlightOffers-TravelAgencyCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exTravelAgency(ag1)));
      used for : s, ls, generated;
       
      ok-RetFlightOffers-TravelAgencyCmd :  ⊦ okaction(Action(ag0, RetFlightOffers-TravelAgencyCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1));
      used for : s, ls;
       
      ok-isRetFlightOffers-TravelAgencyCmd
      :  ⊦ isRetFlightOffers-TravelAgencyCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1)));
      used for : s, ls, generated;
       
      ok-PayCommission-TravelAgencyCmd :  ⊦ okaction(Action(ag0, PayCommission-TravelAgencyCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1));
      used for : s, ls;
       
      ok-isPayCommission-TravelAgencyCmd
      :  ⊦ isPayCommission-TravelAgencyCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1)));
      used for : s, ls, generated;
       
      ok-ReleaseCCD-CreditCardCenterCmd
      :  ⊦ okaction(Action(ag0, ReleaseCCD-CreditCardCenterCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exCreditCardCenter(ag1));
      used for : s, ls;
       
      ok-isReleaseCCD-CreditCardCenterCmd
      : ⊦ 
          isReleaseCCD-CreditCardCenterCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exCreditCardCenter(ag1)));
      used for : s, ls, generated;
       
      ok-GetDeclassifiedCCD-CreditCardCenterCmd
      :  ⊦ okaction(Action(ag0, GetDeclassifiedCCD-CreditCardCenterCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exCreditCardCenter(ag1));
      used for : s, ls;
       
      ok-isGetDeclassifiedCCD-CreditCardCenterCmd
      : ⊦ 
          isGetDeclassifiedCCD-CreditCardCenterCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exCreditCardCenter(ag1)));
      used for : s, ls, generated;
       
      ok-GetFlightOffers-AirlineCmd :  ⊦ okaction(Action(ag0, GetFlightOffers-AirlineCmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1));
      used for : s, ls;
       
      ok-isGetFlightOffers-AirlineCmd
      :  ⊦ isGetFlightOffers-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1)));
      used for : s, ls, generated;
       
      ok-BookFlightOfferstate7-AirlineCmd :  ⊦ okaction(Action(ag0, BookFlightOfferstate7-AirlineCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1));
      used for : s, ls;
       
      ok-isBookFlightOfferstate7-AirlineCmd
      :  ⊦ isBookFlightOfferstate7-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1)));
      used for : s, ls, generated;
       
      ok-OkPayCommission-AirlineCmd :  ⊦ okaction(Action(ag0, OkPayCommission-AirlineCmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1));
      used for : s, ls;
       
      ok-isOkPayCommission-AirlineCmd
      :  ⊦ isOkPayCommission-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1)));
      used for : s, ls, generated;
       
      ok-GetInputRequestData-UserCmd-1
      :  ⊦ okaction(Action(ag0, GetInputRequestData-UserCmd-1, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1));
      used for : s, ls;
       
      ok-isGetInputRequestData-UserCmd-1
      :  ⊦ isGetInputRequestData-UserCmd-1(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1)));
      used for : s, ls, generated;
       
      ok-GetSingleSelection-UserCmd-2
      :  ⊦ okaction(Action(ag0, GetSingleSelection-UserCmd-2, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1));
      used for : s, ls;
       
      ok-isGetSingleSelection-UserCmd-2
      :  ⊦ isGetSingleSelection-UserCmd-2(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1)));
      used for : s, ls, generated;
       
      ok-ConfirmRelease-UserCmd-3
      :  ⊦ okaction(Action(ag0, ConfirmRelease-UserCmd-3, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exUser(ag1));
      used for : s, ls;
       
      ok-isConfirmRelease-UserCmd-3
      :  ⊦ isConfirmRelease-UserCmd-3(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exUser(ag1)));
      used for : s, ls, generated;
       
      ok-Confirm-UserCmd-4 :  ⊦ okaction(Action(ag0, Confirm-UserCmd-4, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1));
      used for : s, ls;
       
      ok-isConfirm-UserCmd-4
      :  ⊦ isConfirm-UserCmd-4(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1)));
      used for : s, ls, generated;
       
      ok-RetFlightOffers-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, RetFlightOffers-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isRetFlightOffers-TravelPlannerCmd
      :  ⊦ isRetFlightOffers-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-BookSelected-TravelPlannerCmd
      :  ⊦ okaction(Action(ag0, BookSelected-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1));
      used for : s, ls;
       
      ok-isBookSelected-TravelPlannerCmd
      :  ⊦ isBookSelected-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1)));
      used for : s, ls, generated;
       
      ok-declassifyCCD4ASM-CreditCardCenterCmd
      : ⊦ 
          okaction(Action(ag0, declassifyCCD4ASM-CreditCardCenterCmd, ag1))
        ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1));
      used for : s, ls;
       
      ok-isdeclassifyCCD4ASM-CreditCardCenterCmd
      : ⊦ 
          isdeclassifyCCD4ASM-CreditCardCenterCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1)));
      used for : s, ls, generated;
       
      ok-afterdeclassifyCCD4ASM-CreditCardCenterCmd
      : ⊦ 
          okaction(Action(ag0, afterdeclassifyCCD4ASM-CreditCardCenterCmd, ag1))
        ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1));
      used for : s, ls;
       
      ok-isafterdeclassifyCCD4ASM-CreditCardCenterCmd
      : ⊦ 
          isafterdeclassifyCCD4ASM-CreditCardCenterCmd(cmd)
        → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1)));
      used for : s, ls, generated;
       
      ok-BookFlightOffer-AirlineCmd :  ⊦ okaction(Action(ag0, BookFlightOffer-AirlineCmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exAirline(ag1));
      used for : s, ls;
       
      ok-isBookFlightOffer-AirlineCmd
      :  ⊦ isBookFlightOffer-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exAirline(ag1)));
      used for : s, ls, generated;
       
      ok-BookFlightOfferstate6-AirlineCmd :  ⊦ okaction(Action(ag0, BookFlightOfferstate6-AirlineCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1));
      used for : s, ls;
       
      ok-isBookFlightOfferstate6-AirlineCmd
      :  ⊦ isBookFlightOfferstate6-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1)));
      used for : s, ls, generated;
       
      ok-Abort8-UserCmd :  ⊦ okaction(Action(ag0, Abort8-UserCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1));
      used for : s, ls;
       
      ok-isAbort8-UserCmd :  ⊦ isAbort8-UserCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1)));
      used for : s, ls, generated;
       
      ok-Abort9-UserCmd :  ⊦ okaction(Action(ag0, Abort9-UserCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1));
      used for : s, ls;
       
      ok-isAbort9-UserCmd :  ⊦ isAbort9-UserCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1)));
      used for : s, ls, generated;
       
end enrich