[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	domains	f	domains → nat
# .	Agents	f	Agents → nat
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic2	f	nat × nat → nat
. ++ .	domains	f	domains × domain → domains
. ++ .	Agents	f	Agents × Agent → Agents
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	domains	f	domains × domain → domains
. -- .	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
. \ .	domains	f	domains × domains → domains
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ∈ .	domains	p	domain × domains
. ∈ .	Agents	p	Agent × Agents
. ∪ .	Agents	f	Agents × Agents → Agents
. ∪ .	domains	f	domains × domains → domains
. ∩ .	domains	f	domains × domains → domains
. ∩ .	Agents	f	Agents × Agents → Agents
. ⊆ .	domains	p	domains × domains
. ⊆ .	Agents	p	Agents × Agents
{ . }	Agents	f	Agent → Agents
{ . }	domains	f	domain → domains
∅	Agents	c	Agents
∅	domains	c	domains
a	action	v	action
a0	action	v	action
a1	action	v	action
a2	action	v	action
Abort8	domain	c	domain
Abort8-UserCmd	command	c	command
Abort9	domain	c	domain
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
domain	domain	s
domains	domains	s
domsvar	domains	v	domains
domsvar0	domains	v	domains
domsvar1	domains	v	domains
domsvar2	domains	v	domains
domvar	domain	v	domain
domvar0	domain	v	domain
domvar1	domain	v	domain
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
HighLow5	domain	c	domain
Init-GetInputRequestData-TravelPlannerCmd	command	c	command
isAbort8	domain	p	domain
isAbort8-UserCmd	command	p	command
isAbort9	domain	p	domain
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
isHighLow5	domain	p	domain
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	domain	p	domain
isUser	Agent	p	Agent
isUser->User_Airline	domain	p	domain
isUser_Airline	domain	p	domain
isUser_TravelAgency_Airline	domain	p	domain
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
User	domain	c	domain
User->User_Airline	domain	c	domain
User_Airline	domain	c	domain
User_TravelAgency_Airline	domain	c	domain