[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
# .	string-less	f	string → nat
. '	string-append	f	char → string
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic2	f	nat × nat → nat
. + .	string-append	f	string × string → string
. + .	string-data	f	char × string → string
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. .call	name	f	name → string
. .char1	string-data	f	string → char
. .cmd	name	f	name → command
. .cmd	action	f	action → command
. .from	action	f	action → Agent
. .id	Agent	f	Agent → nat
. .methodname	name	f	name → string
. .name	name	f	name → string
. .rstring	string-data	f	string → string
. .to	action	f	action → Agent
. < .	string-less	p	char × char
. < .	nat-basic1	p	nat × nat
. < .	string-less	p	string × string
. > .	nat	p	nat × nat
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
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
Airline-flightOffers	name	c	name
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
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
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
CreditCardCenter-ccd	name	c	name
DeclassifiedCCD-TravelPlannerCmd	command	c	command
declassify-count	name	f	string → name
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
isDeclassify-count	name	p	name
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
isLocVar	name	p	name
isMailbox	name	p	name
isOkConfirmBooking-TravelPlannerCmd	command	p	command
isOkPayCommission-AirlineCmd	command	p	command
isPayCommission-TravelAgencyCmd	command	p	command
isReadSourceCount	name	p	name
isReadSourceInputs	name	p	name
isReleaseCCD-CreditCardCenterCmd	command	p	command
isRetFlightOffers-TravelAgencyCmd	command	p	command
isRetFlightOffers-TravelPlannerCmd	command	p	command
isRetFlightOffersstate1-TravelPlannerCmd	command	p	command
isState	name	p	name
isTravelAgency	Agent	p	Agent
isTravelPlanner	Agent	p	Agent
isUser	Agent	p	Agent
isUser-Confirm	name	p	name
isUser-Confirm-count	name	p	name
isUser-ConfirmedRelease-count	name	p	name
isUser-ConfirmRelease	name	p	name
isUser-ConfirmRelease-count	name	p	name
isUser-ConfirmReleases	name	p	name
isUser-Confirms	name	p	name
isUser-GetInput	name	p	name
isUser-GetInput-count	name	p	name
isUser-GetInputs	name	p	name
isUser-GetMultipleSelection	name	p	name
isUser-GetMultipleSelection-count	name	p	name
isUser-GetMultipleSelections	name	p	name
isUser-GetSingleSelection	name	p	name
isUser-GetSingleSelection-count	name	p	name
isUser-GetSingleSelections	name	p	name
locVar	name	f	string → name
m	nat-basic2	v	nat
m0	Agent	v	nat
Mailbox	name	f	command → name
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
nam	name	v	name
nam0	name	v	name
nam1	name	v	name
name	name	s
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
okaction	okaction	p	action
OkConfirmBooking-TravelPlannerCmd	command	c	command
OkPayCommission-AirlineCmd	command	c	command
PayCommission-TravelAgencyCmd	command	c	command
pos	string-less	f	char × string → nat
ReadSourceCount	name	f	string × string → name
ReadSourceInputs	name	f	string × string → name
ReleaseCCD-CreditCardCenterCmd	command	c	command
RetFlightOffers-TravelAgencyCmd	command	c	command
RetFlightOffers-TravelPlannerCmd	command	c	command
RetFlightOffersstate1-TravelPlannerCmd	command	c	command
sortedchars	string-less	c	string
state	name	f	string → name
str	string-data	v	string
str0	string-data	v	string
str1	string-data	v	string
str2	string-data	v	string
str3	string-data	v	string
string	string-data	s
stringvar	string-append	v	string
stringvar0	string-append	v	string
stringvar1	name	v	string
stringvar2	name	v	string
TravelPlanner-flightOffer	name	c	name
usedName	namefuns	p	name × Agent
usedName	namefuns	p	name
User-Confirm	name	f	string → name
User-Confirm-count	name	f	string → name
User-ConfirmedRelease-count	name	f	string → name
User-ConfirmRelease	name	f	string → name
User-ConfirmRelease-count	name	f	string → name
User-ConfirmReleases	name	f	string → name
User-Confirms	name	f	string → name
User-GetInput	name	f	string → name
User-GetInput-count	name	f	string → name
User-GetInputs	name	f	string → name
User-GetMultipleSelection	name	f	string → name
User-GetMultipleSelection-count	name	f	string → name
User-GetMultipleSelections	name	f	string → name
User-GetSingleSelection	name	f	string → name
User-GetSingleSelection-count	name	f	string → name
User-GetSingleSelections	name	f	string → name