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: |
|---|---|---|
| obs-in-domain | ⊦ observe(domvar, nam, ag) → obs(s, domvar)(nam, ag) = s(nam, ag) | An Axiom |
| obs-other-domain | ⊦ ¬ observe(domvar, nam, ag) → obs(s, domvar)(nam, ag) = null | An Axiom |
| observe-User | ⊦ observe(User, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state2') ∧ exTravelPlanner(ag) ∨ nam = TravelPlanner-flightOffer ∧ exTravelPlanner(ag) ∨ nam = Mailbox(ReleaseCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag) ∨ nam = CreditCardCenter-ccd ∧ exCreditCardCenter(ag) ∨ nam = locVar(`airline') ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(ConfirmRelease-UserCmd-3) ∧ exUser(ag) ∨ nam = User-ConfirmRelease(`3') ∧ exUser(ag) ∨ nam = User-ConfirmRelease-count(`3') ∧ exUser(ag) ∨ nam = User-ConfirmReleases(`3') ∧ exUser(ag) ∨ nam = User-ConfirmedRelease-count(`3') ∧ exUser(ag)) | An Axiom |
| alter-User | ⊦ alter(User, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state2') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(ReleaseCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(ReleaseCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag) ∨ nam = locVar(`airline') ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(ConfirmRelease-UserCmd-3) ∧ exUser(ag) ∨ nam = Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag) ∨ nam = state(`state3') ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(ConfirmRelease-UserCmd-3) ∧ exUser(ag) ∨ nam = locVar(`ccd') ∧ exUser(ag) ∨ nam = locVar(`airline') ∧ exUser(ag) ∨ nam = User-ConfirmRelease(`3') ∧ exUser(ag) ∨ nam = User-ConfirmRelease-count(`3') ∧ exUser(ag) ∨ nam = User-ConfirmedRelease-count(`3') ∧ exUser(ag) ∨ nam = state(`pre9') ∧ exUser(ag) ∨ nam = Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag)) | An Axiom |
| observe-User_Airline | ⊦ observe(User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state1') ∧ exTravelPlanner(ag) ∨ nam = locVar(`flightOffers') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(DeclassifiedCCD-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = TravelPlanner-flightOffer ∧ exTravelPlanner(ag) ∨ nam = locVar(`ccd_decl') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(GetSingleSelection-UserCmd-2) ∧ exUser(ag) ∨ nam = User-GetSingleSelection(`2') ∧ exUser(ag) ∨ nam = User-GetSingleSelection-count(`2') ∧ exUser(ag) ∨ nam = User-GetSingleSelections(`2') ∧ exUser(ag) ∨ nam = Mailbox(BookSelected-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = state(`state4') ∧ exCreditCardCenter(ag) ∨ nam = locVar(`ccd_decl') ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(BookFlightOffer-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar(`id') ∧ exAirline(ag) ∨ nam = locVar(`ccd_decl') ∧ exAirline(ag)) | An Axiom |
| alter-User_Airline | ⊦ alter(User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state1') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(GetSingleSelection-UserCmd-2) ∧ exUser(ag) ∨ nam = Mailbox(DeclassifiedCCD-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar(`ccd_decl') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(BookFlightOffer-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox(GetSingleSelection-UserCmd-2) ∧ exUser(ag) ∨ nam = locVar(`flightOffers') ∧ exUser(ag) ∨ nam = User-GetSingleSelection(`2') ∧ exUser(ag) ∨ nam = User-GetSingleSelection-count(`2') ∧ exUser(ag) ∨ nam = state(`pre8') ∧ exUser(ag) ∨ nam = Mailbox(BookSelected-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(BookSelected-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = TravelPlanner-flightOffer ∧ exTravelPlanner(ag) ∨ nam = state(`state2') ∧ exTravelPlanner(ag) ∨ nam = state(`state4') ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(DeclassifiedCCD-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(BookFlightOffer-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar(`id') ∧ exAirline(ag) ∨ nam = locVar(`ccd_decl') ∧ exAirline(ag) ∨ nam = state(`state6') ∧ exAirline(ag)) | An Axiom |
| observe-User_TravelAgency_Airline | ⊦ observe(User_TravelAgency_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`init') ∧ exUser(ag) ∨ nam = Mailbox(GetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar(`requestData') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(OkConfirmBooking-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(GetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar(`requestData') ∧ exTravelAgency(ag) ∨ nam = Mailbox(RetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar(`flightOffers') ∧ exTravelAgency(ag) ∨ nam = Mailbox(PayCommission-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox(GetFlightOffers-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar(`requestData') ∧ exAirline(ag) ∨ nam = Airline-flightOffers ∧ exAirline(ag) ∨ nam = locVar(`filteredFlightOffers') ∧ exAirline(ag) ∨ nam = state(`state7') ∧ exAirline(ag) ∨ nam = Mailbox(OkPayCommission-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox(GetInputRequestData-UserCmd-1) ∧ exUser(ag) ∨ nam = User-GetInput(`1') ∧ exUser(ag) ∨ nam = User-GetInput-count(`1') ∧ exUser(ag) ∨ nam = User-GetInputs(`1') ∧ exUser(ag) ∨ nam = Mailbox(Confirm-UserCmd-4) ∧ exUser(ag) ∨ nam = User-Confirm(`4') ∧ exUser(ag) ∨ nam = User-Confirm-count(`4') ∧ exUser(ag) ∨ nam = User-Confirms(`4') ∧ exUser(ag) ∨ nam = Mailbox(RetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag)) | An Axiom |
| alter-User_TravelAgency_Airline | ⊦ alter(User_TravelAgency_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`init') ∧ exUser(ag) ∨ nam = Mailbox(GetInputRequestData-UserCmd-1) ∧ exUser(ag) ∨ nam = Mailbox(GetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar(`requestData') ∧ exTravelPlanner(ag) ∨ nam = Mailbox(GetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox(OkConfirmBooking-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(Confirm-UserCmd-4) ∧ exUser(ag) ∨ nam = Mailbox(GetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar(`requestData') ∧ exTravelAgency(ag) ∨ nam = Mailbox(GetFlightOffers-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox(RetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar(`flightOffers') ∧ exTravelAgency(ag) ∨ nam = Mailbox(RetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(PayCommission-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox(OkPayCommission-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox(GetFlightOffers-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar(`requestData') ∧ exAirline(ag) ∨ nam = locVar(`filteredFlightOffers') ∧ exAirline(ag) ∨ nam = Mailbox(RetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = state(`state7') ∧ exAirline(ag) ∨ nam = Mailbox(PayCommission-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox(OkPayCommission-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox(OkConfirmBooking-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(GetInputRequestData-UserCmd-1) ∧ exUser(ag) ∨ nam = User-GetInput(`1') ∧ exUser(ag) ∨ nam = User-GetInput-count(`1') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag) ∨ nam = Mailbox(GetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox(Confirm-UserCmd-4) ∧ exUser(ag) ∨ nam = User-Confirm(`4') ∧ exUser(ag) ∨ nam = User-Confirm-count(`4') ∧ exUser(ag) ∨ nam = Mailbox(RetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar(`flightOffers') ∧ exTravelPlanner(ag) ∨ nam = state(`state1') ∧ exTravelPlanner(ag)) | An Axiom |
| observe-User-User_Airline | ⊦ observe(User->User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state3') ∧ exCreditCardCenter(ag) ∨ nam = CreditCardCenter-ccd ∧ exCreditCardCenter(ag) ∨ nam = declassify-count(`declassifyCCD') ∧ exCreditCardCenter(ag)) | An Axiom |
| alter-User-User_Airline | ⊦ alter(User->User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state3') ∧ exCreditCardCenter(ag) ∨ nam = locVar(`ccd_decl') ∧ exCreditCardCenter(ag) ∨ nam = declassify-count(`declassifyCCD') ∧ exCreditCardCenter(ag) ∨ nam = state(`state4') ∧ exCreditCardCenter(ag)) | An Axiom |
| observe-HighLow5 | ⊦ observe(HighLow5, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`state6') ∧ exAirline(ag)) | An Axiom |
| alter-HighLow5 | ⊦ alter(HighLow5, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`state6') ∧ exAirline(ag) ∨ nam = state(`state7') ∧ exAirline(ag)) | An Axiom |
| observe-Abort8 | ⊦ observe(Abort8, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre8') ∧ exUser(ag)) | An Axiom |
| alter-Abort8 | ⊦ alter(Abort8, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre8') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag)) | An Axiom |
| observe-Abort9 | ⊦ observe(Abort9, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre9') ∧ exUser(ag)) | An Axiom |
| alter-Abort9 | ⊦ alter(Abort9, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre9') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag)) | An Axiom |