This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| ok-Init-GetInputRequestData-TravelPlannerCmd | ⊦ okaction(Action(ag0, Init-GetInputRequestData-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isInit-GetInputRequestData-TravelPlannerCmd | ⊦ isInit-GetInputRequestData-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-GetFlightOffers-TravelPlannerCmd | ⊦ okaction(Action(ag0, GetFlightOffers-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isGetFlightOffers-TravelPlannerCmd | ⊦ isGetFlightOffers-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-RetFlightOffersstate1-TravelPlannerCmd | ⊦ okaction(Action(ag0, RetFlightOffersstate1-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isRetFlightOffersstate1-TravelPlannerCmd | ⊦ isRetFlightOffersstate1-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-BookSelectedstate2-TravelPlannerCmd | ⊦ okaction(Action(ag0, BookSelectedstate2-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isBookSelectedstate2-TravelPlannerCmd | ⊦ isBookSelectedstate2-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-DeclassifiedCCD-TravelPlannerCmd | ⊦ okaction(Action(ag0, DeclassifiedCCD-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isDeclassifiedCCD-TravelPlannerCmd | ⊦ isDeclassifiedCCD-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-OkConfirmBooking-TravelPlannerCmd | ⊦ okaction(Action(ag0, OkConfirmBooking-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isOkConfirmBooking-TravelPlannerCmd | ⊦ isOkConfirmBooking-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-GetFlightOffers-TravelAgencyCmd | ⊦ okaction(Action(ag0, GetFlightOffers-TravelAgencyCmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exTravelAgency(ag1)) | An Axiom |
| ok-isGetFlightOffers-TravelAgencyCmd | ⊦ isGetFlightOffers-TravelAgencyCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exTravelAgency(ag1))) | An Axiom |
| ok-RetFlightOffers-TravelAgencyCmd | ⊦ okaction(Action(ag0, RetFlightOffers-TravelAgencyCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1)) | An Axiom |
| ok-isRetFlightOffers-TravelAgencyCmd | ⊦ isRetFlightOffers-TravelAgencyCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1))) | An Axiom |
| ok-PayCommission-TravelAgencyCmd | ⊦ okaction(Action(ag0, PayCommission-TravelAgencyCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1)) | An Axiom |
| ok-isPayCommission-TravelAgencyCmd | ⊦ isPayCommission-TravelAgencyCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exTravelAgency(ag1))) | An Axiom |
| ok-ReleaseCCD-CreditCardCenterCmd | ⊦ okaction(Action(ag0, ReleaseCCD-CreditCardCenterCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exCreditCardCenter(ag1)) | An Axiom |
| ok-isReleaseCCD-CreditCardCenterCmd | ⊦ isReleaseCCD-CreditCardCenterCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exCreditCardCenter(ag1))) | An Axiom |
| ok-GetDeclassifiedCCD-CreditCardCenterCmd | ⊦ okaction(Action(ag0, GetDeclassifiedCCD-CreditCardCenterCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exCreditCardCenter(ag1)) | An Axiom |
| ok-isGetDeclassifiedCCD-CreditCardCenterCmd | ⊦ isGetDeclassifiedCCD-CreditCardCenterCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exCreditCardCenter(ag1))) | An Axiom |
| ok-GetFlightOffers-AirlineCmd | ⊦ okaction(Action(ag0, GetFlightOffers-AirlineCmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1)) | An Axiom |
| ok-isGetFlightOffers-AirlineCmd | ⊦ isGetFlightOffers-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1))) | An Axiom |
| ok-BookFlightOfferstate7-AirlineCmd | ⊦ okaction(Action(ag0, BookFlightOfferstate7-AirlineCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1)) | An Axiom |
| ok-isBookFlightOfferstate7-AirlineCmd | ⊦ isBookFlightOfferstate7-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1))) | An Axiom |
| ok-OkPayCommission-AirlineCmd | ⊦ okaction(Action(ag0, OkPayCommission-AirlineCmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1)) | An Axiom |
| ok-isOkPayCommission-AirlineCmd | ⊦ isOkPayCommission-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exAirline(ag1))) | An Axiom |
| ok-GetInputRequestData-UserCmd-1 | ⊦ okaction(Action(ag0, GetInputRequestData-UserCmd-1, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1)) | An Axiom |
| ok-isGetInputRequestData-UserCmd-1 | ⊦ isGetInputRequestData-UserCmd-1(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1))) | An Axiom |
| ok-GetSingleSelection-UserCmd-2 | ⊦ okaction(Action(ag0, GetSingleSelection-UserCmd-2, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1)) | An Axiom |
| ok-isGetSingleSelection-UserCmd-2 | ⊦ isGetSingleSelection-UserCmd-2(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1))) | An Axiom |
| ok-ConfirmRelease-UserCmd-3 | ⊦ okaction(Action(ag0, ConfirmRelease-UserCmd-3, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exUser(ag1)) | An Axiom |
| ok-isConfirmRelease-UserCmd-3 | ⊦ isConfirmRelease-UserCmd-3(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exUser(ag1))) | An Axiom |
| ok-Confirm-UserCmd-4 | ⊦ okaction(Action(ag0, Confirm-UserCmd-4, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1)) | An Axiom |
| ok-isConfirm-UserCmd-4 | ⊦ isConfirm-UserCmd-4(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exTravelPlanner(ag0) ∧ exUser(ag1))) | An Axiom |
| ok-RetFlightOffers-TravelPlannerCmd | ⊦ okaction(Action(ag0, RetFlightOffers-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isRetFlightOffers-TravelPlannerCmd | ⊦ isRetFlightOffers-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelAgency(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-BookSelected-TravelPlannerCmd | ⊦ okaction(Action(ag0, BookSelected-TravelPlannerCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1)) | An Axiom |
| ok-isBookSelected-TravelPlannerCmd | ⊦ isBookSelected-TravelPlannerCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exTravelPlanner(ag1))) | An Axiom |
| ok-declassifyCCD4ASM-CreditCardCenterCmd | ⊦ okaction(Action(ag0, declassifyCCD4ASM-CreditCardCenterCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1)) | An Axiom |
| ok-isdeclassifyCCD4ASM-CreditCardCenterCmd | ⊦ isdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1))) | An Axiom |
| ok-afterdeclassifyCCD4ASM-CreditCardCenterCmd | ⊦ okaction(Action(ag0, afterdeclassifyCCD4ASM-CreditCardCenterCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1)) | An Axiom |
| ok-isafterdeclassifyCCD4ASM-CreditCardCenterCmd | ⊦ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exCreditCardCenter(ag0) ∧ exCreditCardCenter(ag1))) | An Axiom |
| ok-BookFlightOffer-AirlineCmd | ⊦ okaction(Action(ag0, BookFlightOffer-AirlineCmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exAirline(ag1)) | An Axiom |
| ok-isBookFlightOffer-AirlineCmd | ⊦ isBookFlightOffer-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exTravelPlanner(ag0) ∧ exAirline(ag1))) | An Axiom |
| ok-BookFlightOfferstate6-AirlineCmd | ⊦ okaction(Action(ag0, BookFlightOfferstate6-AirlineCmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1)) | An Axiom |
| ok-isBookFlightOfferstate6-AirlineCmd | ⊦ isBookFlightOfferstate6-AirlineCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (exAirline(ag0) ∧ exAirline(ag1))) | An Axiom |
| ok-Abort8-UserCmd | ⊦ okaction(Action(ag0, Abort8-UserCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1)) | An Axiom |
| ok-isAbort8-UserCmd | ⊦ isAbort8-UserCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1))) | An Axiom |
| ok-Abort9-UserCmd | ⊦ okaction(Action(ag0, Abort9-UserCmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1)) | An Axiom |
| ok-isAbort9-UserCmd | ⊦ isAbort9-UserCmd(cmd) → (okaction(Action(ag0, cmd, ag1)) ↔ ¬ ¬ (ag0 .id = ag1 .id ∧ exUser(ag0) ∧ exUser(ag1))) | An Axiom |