| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | Agents | f | Agents → nat |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic2 | f | nat × nat → nat |
| . ++ . | Agents | f | Agents × Agent → Agents |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -- . | Agents | f | Agents × Agent → Agents |
| . -1 | nat-basic1 | f | nat → nat |
| . .cmd | action | f | action → command |
| . .from | action | f | action → Agent |
| . .id | Agent | f | Agent → nat |
| . .to | action | f | action → Agent |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . \ . | Agents | f | Agents × Agents → Agents |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ∈ . | Agents | p | Agent × Agents |
| . ∪ . | Agents | f | Agents × Agents → Agents |
| . ∩ . | Agents | f | Agents × Agents → Agents |
| . ⊆ . | Agents | p | Agents × Agents |
| { . } | Agents | f | Agent → Agents |
| ∅ | Agents | c | Agents |
| a | action | v | action |
| a0 | action | v | action |
| a1 | action | v | action |
| a2 | action | v | action |
| Abort8-UserCmd | command | c | command |
| Abort9-UserCmd | command | c | command |
| action | action | s | |
| Action | action | f | Agent × command × Agent → action |
| afterdeclassifyCCD4ASM-CreditCardCenterCmd | command | c | command |
| ag | Agent | v | Agent |
| ag0 | Agent | v | Agent |
| ag1 | Agent | v | Agent |
| ag2 | action | v | Agent |
| Agent | Agent | s | |
| Agents | Agents | s | |
| ags | Agents | v | Agents |
| ags0 | Agents | v | Agents |
| ags1 | Agents | v | Agents |
| ags2 | Agents | v | Agents |
| BookFlightOffer-AirlineCmd | command | c | command |
| BookFlightOfferstate6-AirlineCmd | command | c | command |
| BookFlightOfferstate7-AirlineCmd | command | c | command |
| BookSelected-TravelPlannerCmd | command | c | command |
| BookSelectedstate2-TravelPlannerCmd | command | c | command |
| cmd | command | v | command |
| cmd0 | command | v | command |
| cmd1 | command | v | command |
| cmd2 | command | v | command |
| command | command | s | |
| Confirm-UserCmd-4 | command | c | command |
| ConfirmRelease-UserCmd-3 | command | c | command |
| DeclassifiedCCD-TravelPlannerCmd | command | c | command |
| declassifyCCD4ASM-CreditCardCenterCmd | command | c | command |
| exAgent | exAgent | p | Agent |
| exAirline | exAgent | p | Agent |
| exCreditCardCenter | exAgent | p | Agent |
| exTravelAgency | exAgent | p | Agent |
| exTravelPlanner | exAgent | p | Agent |
| exUser | exAgent | p | Agent |
| GetDeclassifiedCCD-CreditCardCenterCmd | command | c | command |
| GetFlightOffers-AirlineCmd | command | c | command |
| GetFlightOffers-TravelAgencyCmd | command | c | command |
| GetFlightOffers-TravelPlannerCmd | command | c | command |
| GetInputRequestData-UserCmd-1 | command | c | command |
| GetSingleSelection-UserCmd-2 | command | c | command |
| Init-GetInputRequestData-TravelPlannerCmd | command | c | command |
| isAbort8-UserCmd | command | p | command |
| isAbort9-UserCmd | command | p | command |
| isafterdeclassifyCCD4ASM-CreditCardCenterCmd | command | p | command |
| isAirline | Agent | p | Agent |
| isBookFlightOffer-AirlineCmd | command | p | command |
| isBookFlightOfferstate6-AirlineCmd | command | p | command |
| isBookFlightOfferstate7-AirlineCmd | command | p | command |
| isBookSelected-TravelPlannerCmd | command | p | command |
| isBookSelectedstate2-TravelPlannerCmd | command | p | command |
| isConfirm-UserCmd-4 | command | p | command |
| isConfirmRelease-UserCmd-3 | command | p | command |
| isCreditCardCenter | Agent | p | Agent |
| isDeclassifiedCCD-TravelPlannerCmd | command | p | command |
| isdeclassifyCCD4ASM-CreditCardCenterCmd | command | p | command |
| isGetDeclassifiedCCD-CreditCardCenterCmd | command | p | command |
| isGetFlightOffers-AirlineCmd | command | p | command |
| isGetFlightOffers-TravelAgencyCmd | command | p | command |
| isGetFlightOffers-TravelPlannerCmd | command | p | command |
| isGetInputRequestData-UserCmd-1 | command | p | command |
| isGetSingleSelection-UserCmd-2 | command | p | command |
| isInit-GetInputRequestData-TravelPlannerCmd | command | p | command |
| isOkConfirmBooking-TravelPlannerCmd | command | p | command |
| isOkPayCommission-AirlineCmd | command | p | command |
| isPayCommission-TravelAgencyCmd | command | p | command |
| isReleaseCCD-CreditCardCenterCmd | command | p | command |
| isRetFlightOffers-TravelAgencyCmd | command | p | command |
| isRetFlightOffers-TravelPlannerCmd | command | p | command |
| isRetFlightOffersstate1-TravelPlannerCmd | command | p | command |
| isTravelAgency | Agent | p | Agent |
| isTravelPlanner | Agent | p | Agent |
| isUser | Agent | p | Agent |
| m | nat-basic2 | v | nat |
| m0 | Agent | v | nat |
| mkAirline | Agent | f | nat → Agent |
| mkCreditCardCenter | Agent | f | nat → Agent |
| mkTravelAgency | Agent | f | nat → Agent |
| mkTravelPlanner | Agent | f | nat → Agent |
| mkUser | Agent | f | nat → Agent |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| NUMOFAirline | exAgent | c | nat |
| NUMOFAPPSANDUSERS | exAgent | c | nat |
| NUMOFCreditCardCenter | exAgent | c | nat |
| NUMOFTravelAgency | exAgent | c | nat |
| NUMOFTravelPlanner | exAgent | c | nat |
| NUMOFUser | exAgent | c | nat |
| OkConfirmBooking-TravelPlannerCmd | command | c | command |
| OkPayCommission-AirlineCmd | command | c | command |
| PayCommission-TravelAgencyCmd | command | c | command |
| ReleaseCCD-CreditCardCenterCmd | command | c | command |
| RetFlightOffers-TravelAgencyCmd | command | c | command |
| RetFlightOffers-TravelPlannerCmd | command | c | command |
| RetFlightOffersstate1-TravelPlannerCmd | command | c | command |