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

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	gen-secdomain-set	function, secdomainset → nat
#	set-basic	function, set → nat
#	gen-command-list	function, commandlist → nat
#	list-data	function, list → nat
#	string-less	function, string → nat
#	Agentlist	function, Agentlist → nat
#	domains	function, domains → nat
#	data	function, ListOfData → nat
#	Agents	function, Agents → nat
#oc	list-perm	function, elem × list → nat
#oc	Agentlist	function, Agent × Agentlist → nat
'	gen-command-list	function, command → commandlist
'	list	function, elem → list
'	string-append	function, char → string
'	Agentlist	function, Agent → Agentlist
'	Instance	function, action → commandlist
*	int-mult	function, int × int → int
*	nat-mult	function, nat × nat → nat
+	gen-command-list	function, command × commandlist → commandlist
+	gen-command-list	function, commandlist × commandlist → commandlist
+	gen-command-list	function, commandlist × command → commandlist
+	gen-command-list	function, command × command → commandlist
+	list	function, list × list → list
+	list	function, list × elem → list
+	list	function, elem × elem → list
+	list-data	function, elem × list → list
+	string-append	function, string × string → string
+	string-data	function, char × string → string
+	int-basic2	function, int × int → int
+	nat-basic2	function, nat × nat → nat
+	Agentlist	function, Agent × Agentlist → Agentlist
+	Agentlist	function, Agentlist × Agentlist → Agentlist
+	Agentlist	function, Agentlist × Agent → Agentlist
+	Agentlist	function, Agent × Agent → Agentlist
+	Instance	function, action × commandlist → commandlist
+	Instance	function, commandlist × action → commandlist
+	Instance	function, action × action → commandlist
+	data	function, FlightOffer × ListOfFlightOffer → ListOfFlightOffer
+	data	function, GPSPos × ListOfGPSPos → ListOfGPSPos
+	data	function, Data × ListOfData → ListOfData
+	datafuns	function, Integer × Integer → Integer
++	gen-secdomain-set	function, secdomainset × secdomain → secdomainset
++	set-basic	function, set × elem → set
++	gen-command-list	function, commandlist × command → commandlist
++	list-dup	function, list × elem → list
++	Agentlist	function, Agentlist × Agent → Agentlist
++	Instance	function, commandlist × action → commandlist
++	Instance	function, secdomainset × domain → secdomainset
++	domains	function, domains × domain → domains
++	Agents	function, Agents × Agent → Agents
+1	int-basic1	function, int → int
+1	nat-basic1	function, nat → nat
-	int-abs	function, int × int → int
-	nat	function, nat × nat → nat
-	datafuns	function, Integer × Integer → Integer
--	gen-secdomain-set	function, secdomainset × secdomain → secdomainset
--	set-union	function, set × elem → set
--	Instance	function, secdomainset × domain → secdomainset
--	domains	function, domains × domain → domains
--	Agents	function, Agents × Agent → Agents
-1	int-basic1	function, int → int
-1	nat-basic1	function, nat → nat
-1l	list-del	function, list × elem → list
-1l	list-del	function, list × nat → list
-1l	Agentlist	function, Agentlist × Agent → Agentlist
-1l	Agentlist	function, Agentlist × nat → Agentlist
-l	list-del	function, list × elem → list
-l	Agentlist	function, Agentlist × Agent → Agentlist
.1	data	function, Data → Data
.2	data	function, Data → Data
.Agent	data	function, Data → Agent
.Boolean	data	function, Data → Boolean
.CreditCardDetails	data	function, Data → CreditCardDetails
.FlightOffer	data	function, Data → FlightOffer
.GPSPos	data	function, Data → GPSPos
.Integer	data	function, Data → Integer
.ListOfData	data	function, Data → ListOfData
.ListOfFlightOffer	data	function, Data → ListOfFlightOffer
.ListOfGPSPos	data	function, Data → ListOfGPSPos
.RequestData	data	function, Data → RequestData
.String	data	function, Data → String
.agentlist	data	function, Message → Agentlist
.airline	data	function, FlightOffer → String
.butlast	gen-command-list	function, commandlist → commandlist
.butlast	list-last	function, list → list
.butlast	Agentlist	function, Agentlist → Agentlist
.call	name	function, name → string
.ccd	data	function, Content → CreditCardDetails
.char1	string-data	function, string → char
.cmd	name	function, name → command
.cmd	action	function, action → command
.content	data	function, Message → Content
.data	data	function, Content → Data
.date	data	function, RequestData → String
.first	gen-command-list	function, commandlist → command
.first	list-data	function, list → elem
.first	Agentlist	function, Agentlist → Agent
.first	Instance	function, commandlist → action
.first	data	function, ListOfFlightOffer → FlightOffer
.first	data	function, ListOfGPSPos → GPSPos
.first	data	function, ListOfData → Data
.flightOffer	data	function, Content → FlightOffer
.flightOffers	data	function, Content → ListOfFlightOffer
.from	action	function, action → Agent
.id	Agent	function, Agent → nat
.id	data	function, Content → Integer
.id	data	function, FlightOffer → Integer
.last	gen-command-list	function, commandlist → command
.last	list-last	function, list → elem
.last	Agentlist	function, Agentlist → Agent
.last	Instance	function, commandlist → action
.latitude	data	function, GPSPos → String
.longitude	data	function, GPSPos → String
.methodname	name	function, name → string
.msg	data	function, Data → Message
.name	name	function, name → string
.nat	data	function, Data → nat
.receiver	data	function, Content → String
.requestData	data	function, Content → RequestData
.rest	gen-command-list	function, commandlist → commandlist
.rest	list-data	function, list → list
.rest	Agentlist	function, Agentlist → Agentlist
.rest	data	function, ListOfFlightOffer → ListOfFlightOffer
.rest	data	function, ListOfGPSPos → ListOfGPSPos
.rest	data	function, ListOfData → ListOfData
.rstring	string-data	function, string → string
.selection	data	function, Content → ListOfData
.to	action	function, action → Agent
.value	data	predicate, Boolean
.value	data	function, Integer → int
.value	data	function, String → string
.what	data	function, Content → Data
<	gen-command-list	predicate, commandlist × commandlist
<	list-data	predicate, list × list
<	string-less	predicate, string × string
<	string-less	predicate, char × char
<	int-basic1	predicate, int × int
<	nat-basic1	predicate, nat × nat
<	Agentlist	predicate, Agentlist × Agentlist
<	data	predicate, ListOfData × ListOfData
<	datafuns	function, Integer × Integer → Boolean
<=	datafuns	function, Integer × Integer → Boolean
>	int-abs	predicate, int × int
>	nat	predicate, nat × nat
>	datafuns	function, Integer × Integer → Boolean
>=	datafuns	function, Integer × Integer → Boolean
ASM#	ASM	procedure, : name × Agent → Data × bool
Abort8	domain	constant, domain
Abort8-UserCmd	command	constant, command
Abort8-UserCmd#	ASM	procedure, action : name × Agent → Data
Abort9	domain	constant, domain
Abort9-UserCmd	command	constant, command
Abort9-UserCmd#	ASM	procedure, action : name × Agent → Data
Action	action	function, Agent × command × Agent → action
Agent	Agent	sort,
Agentlist	Agentlist	sort,
Agents	Agents	sort,
Airline-flightOffers	name	constant, name
BookFlightOffer-AirlineCmd	command	constant, command
BookFlightOffer-AirlineCmd#	ASM	procedure, action : name × Agent → Data
BookFlightOfferstate6-AirlineCmd	command	constant, command
BookFlightOfferstate6-AirlineCmd#	ASM	procedure, action : name × Agent → Data
BookFlightOfferstate7-AirlineCmd	command	constant, command
BookFlightOfferstate7-AirlineCmd#	ASM	procedure, action : name × Agent → Data
BookSelected-TravelPlannerCmd	command	constant, command
BookSelected-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
BookSelectedstate2-TravelPlannerCmd	command	constant, command
BookSelectedstate2-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
Boolean	data	sort,
Boolvar	Instance	variable, bool,flexible
Confirm-UserCmd-4	command	constant, command
Confirm-UserCmd-4#	ASM	procedure, action : name × Agent → Data
ConfirmRelease-UserCmd-3	command	constant, command
ConfirmRelease-UserCmd-3#	ASM	procedure, action : name × Agent → Data
Content	data	sort,
CreditCardCenter-ccd	name	constant, name
CreditCardDetails	data	sort,
DONE	ASMAUX	procedure, command × Agent : name × Agent → Data
Data	data	sort,
DeclassifiedCCD-TravelPlannerCmd	command	constant, command
DeclassifiedCCD-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
EXEC	ASM	procedure, action : name × Agent → Data
FlightOffer	data	sort,
GPSPos	data	sort,
GetDeclassifiedCCD-CreditCardCenterCmd	command	constant, command
GetDeclassifiedCCD-CreditCardCenterCmd#	ASM	procedure, action : name × Agent → Data
GetFlightOffers-AirlineCmd	command	constant, command
GetFlightOffers-AirlineCmd#	ASM	procedure, action : name × Agent → Data
GetFlightOffers-TravelAgencyCmd	command	constant, command
GetFlightOffers-TravelAgencyCmd#	ASM	procedure, action : name × Agent → Data
GetFlightOffers-TravelPlannerCmd	command	constant, command
GetFlightOffers-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
GetInputRequestData-UserCmd-1	command	constant, command
GetInputRequestData-UserCmd-1#	ASM	procedure, action : name × Agent → Data
GetSingleSelection-UserCmd-2	command	constant, command
GetSingleSelection-UserCmd-2#	ASM	procedure, action : name × Agent → Data
HighLow5	domain	constant, domain
Init-GetInputRequestData-TravelPlannerCmd	command	constant, command
Init-GetInputRequestData-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
InitValue	userMethods	constant, Data
Integer	data	sort,
ListOfData	data	sort,
ListOfData2ListOfFlightOffer	datafuns	function, ListOfData → ListOfFlightOffer
ListOfData2ListOfGPSPos	datafuns	function, ListOfData → ListOfGPSPos
ListOfFlightOffer	data	sort,
ListOfFlightOffer2ListOfData	datafuns	function, ListOfFlightOffer → ListOfData
ListOfGPSPos	data	sort,
ListOfGPSPos2ListOfData	datafuns	function, ListOfGPSPos → ListOfData
Mailbox	name	function, command → name
Message	data	sort,
NUMOFAPPSANDUSERS	exAgent	constant, nat
NUMOFAirline	exAgent	constant, nat
NUMOFCreditCardCenter	exAgent	constant, nat
NUMOFTravelAgency	exAgent	constant, nat
NUMOFTravelPlanner	exAgent	constant, nat
NUMOFUser	exAgent	constant, nat
OkConfirmBooking-TravelPlannerCmd	command	constant, command
OkConfirmBooking-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
OkPayCommission-AirlineCmd	command	constant, command
OkPayCommission-AirlineCmd#	ASM	procedure, action : name × Agent → Data
PayCommission-TravelAgencyCmd	command	constant, command
PayCommission-TravelAgencyCmd#	ASM	procedure, action : name × Agent → Data
ReadSourceCount	name	function, string × string → name
ReadSourceInputs	name	function, string × string → name
ReleaseCCD-CreditCardCenterCmd	command	constant, command
ReleaseCCD-CreditCardCenterCmd#	ASM	procedure, action : name × Agent → Data
RequestData	data	sort,
RetFlightOffers-TravelAgencyCmd	command	constant, command
RetFlightOffers-TravelAgencyCmd#	ASM	procedure, action : name × Agent → Data
RetFlightOffers-TravelPlannerCmd	command	constant, command
RetFlightOffers-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
RetFlightOffersstate1-TravelPlannerCmd	command	constant, command
RetFlightOffersstate1-TravelPlannerCmd#	ASM	procedure, action : name × Agent → Data
STEP	ASM	procedure, : name × Agent → Data × bool
STEP#	Step	procedure, name × Agent → Data × action : name × Agent → Data
String	data	sort,
TravelPlanner-flightOffer	name	constant, name
User	domain	constant, domain
User->User_Airline	domain	constant, domain
User-Confirm	name	function, string → name
User-Confirm-count	name	function, string → name
User-ConfirmRelease	name	function, string → name
User-ConfirmRelease-count	name	function, string → name
User-ConfirmReleases	name	function, string → name
User-ConfirmedRelease-count	name	function, string → name
User-Confirms	name	function, string → name
User-GetInput	name	function, string → name
User-GetInput-count	name	function, string → name
User-GetInputs	name	function, string → name
User-GetMultipleSelection	name	function, string → name
User-GetMultipleSelection-count	name	function, string → name
User-GetMultipleSelections	name	function, string → name
User-GetSingleSelection	name	function, string → name
User-GetSingleSelection-count	name	function, string → name
User-GetSingleSelections	name	function, string → name
User_Airline	domain	constant, domain
User_TravelAgency_Airline	domain	constant, domain
[]	gen-command-list	constant, commandlist
[]	list-data	constant, list
[]	Agentlist	constant, Agentlist
[]	data	constant, ListOfFlightOffer
[]	data	constant, ListOfGPSPos
[]	data	constant, ListOfData
\	gen-secdomain-set	function, secdomainset × secdomainset → secdomainset
\	set-union	function, set × set → set
\	list-set	function, list × list → list
\	Agentlist	function, Agentlist × Agentlist → Agentlist
\	domains	function, domains × domains → domains
\	Agents	function, Agents × Agents → Agents
]	list-del	function, list × nat → elem
]	list-del	function, list × nat × elem → list
]	Agentlist	function, Agentlist × nat → Agent
]	Agentlist	function, Agentlist × nat × Agent → Agentlist
a	elem	variable, elem
a	action	variable, action
a0	list-data	variable, elem
a0	action	variable, action
a1	action	variable, action
a2	action	variable, action
a3	Instance	variable, action
a4	Instance	variable, action
a5	Instance	variable, action
a_Boolean	data	variable, Boolean
a_Boolean0	data	variable, Boolean
a_Boolean1	data	variable, Boolean
a_Boolean2	data	variable, Boolean
a_CreditCardDetails	data	variable, CreditCardDetails
a_CreditCardDetails0	data	variable, CreditCardDetails
a_CreditCardDetails1	data	variable, CreditCardDetails
a_CreditCardDetails2	data	variable, CreditCardDetails
a_FlightOffer	data	variable, FlightOffer
a_FlightOffer0	data	variable, FlightOffer
a_FlightOffer1	data	variable, FlightOffer
a_FlightOffer2	data	variable, FlightOffer
a_GPSPos	data	variable, GPSPos
a_GPSPos0	data	variable, GPSPos
a_GPSPos1	data	variable, GPSPos
a_GPSPos2	data	variable, GPSPos
a_Integer	data	variable, Integer
a_Integer0	data	variable, Integer
a_Integer1	data	variable, Integer
a_Integer2	data	variable, Integer
a_ListOfData	data	variable, ListOfData
a_ListOfData0	data	variable, ListOfData
a_ListOfFlightOffer	data	variable, ListOfFlightOffer
a_ListOfFlightOffer0	data	variable, ListOfFlightOffer
a_ListOfGPSPos	data	variable, ListOfGPSPos
a_ListOfGPSPos0	data	variable, ListOfGPSPos
a_RequestData	data	variable, RequestData
a_RequestData0	data	variable, RequestData
a_RequestData1	data	variable, RequestData
a_RequestData2	data	variable, RequestData
a_String	data	variable, String
a_String0	data	variable, String
a_String1	data	variable, String
a_String2	data	variable, String
abs	int-abs	function, int → int
action	action	sort,
afterdeclassifyCCD4ASM-CreditCardCenterCmd	command	constant, command
afterdeclassifyCCD4ASM-CreditCardCenterCmd#	ASM	procedure, action : name × Agent → Data
ag	Agent	variable, Agent
ag0	Agent	variable, Agent
ag1	Agent	variable, Agent
ag2	action	variable, Agent
ag3	state	variable, Agent
ag4	state	variable, Agent
ag5	state	variable, Agent
agl	Agentlist	variable, Agentlist
agl0	Agentlist	variable, Agentlist
agl1	Agentlist	variable, Agentlist
agl10	Agentlist	variable, Agentlist
agl2	Agentlist	variable, Agentlist
agl3	Agentlist	variable, Agentlist
agl4	Agentlist	variable, Agentlist
agl5	Agentlist	variable, Agentlist
agl6	Agentlist	variable, Agentlist
agl7	Agentlist	variable, Agentlist
agl8	Agentlist	variable, Agentlist
agl9	Agentlist	variable, Agentlist
ags	Agents	variable, Agents
ags0	Agents	variable, Agents
ags1	Agents	variable, Agents
ags2	Agents	variable, Agents
allNull	state	predicate, name × Agent → Data
alter	AccessControl	predicate, name × secdomain
alter	observeAlter	predicate, domain × name × Agent
b	elem	variable, elem
bool	bool	sort,
boolvar	bool	variable, bool
boolvar0	bool	variable, bool
boolvar1	Instance	variable, bool
butlastn	gen-command-list	function, nat × commandlist → commandlist
butlastn	list-last	function, nat × list → list
butlastn	Agentlist	function, nat × Agentlist → Agentlist
c	elem	variable, elem
cdom	AccessControl	function, command → secdomain
char	char	variable, char
char	char	sort,
char0	char	variable, char
char1	char	variable, char
char2	char	variable, char
char3	string-less	variable, char
cl	gen-command-list	variable, commandlist
cl0	gen-command-list	variable, commandlist
cl1	gen-command-list	variable, commandlist
cl10	gen-command-list	variable, commandlist
cl2	gen-command-list	variable, commandlist
cl3	gen-command-list	variable, commandlist
cl4	gen-command-list	variable, commandlist
cl5	gen-command-list	variable, commandlist
cl6	gen-command-list	variable, commandlist
cl7	gen-command-list	variable, commandlist
cl8	gen-command-list	variable, commandlist
cl9	gen-command-list	variable, commandlist
cmd	command	variable, command
cmd0	command	variable, command
cmd1	command	variable, command
cmd2	command	variable, command
cntnt	data	variable, Content
cntnt0	data	variable, Content
cntnt1	data	variable, Content
co	gen-commands	variable, command
co0	gen-command-list	variable, command
co1	gen-command-list	variable, command
co2	gen-command-list	variable, command
command	gen-commands	sort,
command	command	sort,
commandlist	gen-command-list	sort,
contents	AccessControl	function, systemstate × name → value
d	gen-secdomain	variable, secdomain
d	data	variable, Data
d0	gen-secdomain	variable, secdomain
d0	data	variable, Data
d1	gen-secdomain	variable, secdomain
d1	data	variable, Data
d2	data	variable, Data
d4	state	variable, Data
d5	state	variable, Data
declassify-count	name	function, string → name
declassifyCCD-CreditCardCenter	localMethods	function, CreditCardDetails → CreditCardDetails
declassifyCCD4ASM-CreditCardCenterCmd	command	constant, command
declassifyCCD4ASM-CreditCardCenterCmd#	ASM	procedure, action : name × Agent → Data
disj	gen-command-list	predicate, commandlist × commandlist
disj	list-dup	predicate, list × list
disj	Agentlist	predicate, Agentlist × Agentlist
dl	data	variable, ListOfData
dl0	data	variable, ListOfData
dl1	data	variable, ListOfData
dl10	data	variable, ListOfData
dl2	data	variable, ListOfData
dl3	data	variable, ListOfData
dl4	data	variable, ListOfData
dl5	data	variable, ListOfData
dl6	data	variable, ListOfData
dl7	data	variable, ListOfData
dl8	data	variable, ListOfData
dl9	data	variable, ListOfData
dom	domdefinitions	function, action → domain
dom	domdefinitions	function, name × Agent → domain
domain	domain	sort,
domains	domains	sort,
domsvar	domains	variable, domains
domsvar0	domains	variable, domains
domsvar1	domains	variable, domains
domsvar2	domains	variable, domains
domvar	domain	variable, domain
domvar0	domain	variable, domain
domvar1	domain	variable, domain
ds	gen-secdomain-set	variable, secdomainset
ds0	gen-secdomain-set	variable, secdomainset
ds1	gen-secdomain-set	variable, secdomainset
ds2	gen-secdomain-set	variable, secdomainset
dups	gen-command-list	predicate, commandlist
dups	list-dup	predicate, list
dups	Agentlist	predicate, Agentlist
elem	elem	sort,
eqd	AccessControl	predicate, systemstate × secdomain × systemstate
eqd	eqd	predicate, name × Agent → Data × domain × name × Agent → Data
eqdAirline	eqd	predicate, name × Agent → Data × name × name × Agent → Data
eqdCreditCardCenter	eqd	predicate, name × Agent → Data × name × name × Agent → Data
eqdTravelAgency	eqd	predicate, name × Agent → Data × name × name × Agent → Data
eqdTravelPlanner	eqd	predicate, name × Agent → Data × name × name × Agent → Data
eqdUser	eqd	predicate, name × Agent → Data × name × name × Agent → Data
eqds	MeydenIntrans	predicate, systemstate × secdomainset × systemstate
eqds	Instance	predicate, name × Agent → Data × secdomainset × name × Agent → Data
exAgent	exAgent	predicate, Agent
exAirline	exAgent	predicate, Agent
exCreditCardCenter	exAgent	predicate, Agent
exTravelAgency	exAgent	predicate, Agent
exTravelPlanner	exAgent	predicate, Agent
exUser	exAgent	predicate, Agent
fillfirst	gen-command-list	function, nat × command × commandlist → commandlist
fillfirst	list-last	function, nat × elem × list → list
fillfirst	Agentlist	function, nat × Agent × Agentlist → Agentlist
fillfirst	Instance	function, nat × action × commandlist → commandlist
filter	list-set	function, list × list → list
filter	Agentlist	function, Agentlist × Agentlist → Agentlist
filterOffers-Airline	localMethods	function, RequestData × ListOfFlightOffer → ListOfFlightOffer
firstn	list-del	function, nat × list → list
firstn	Agentlist	function, nat × Agentlist → Agentlist
frome	list-del	function, list × elem → list
frome	Agentlist	function, Agentlist × Agent → Agentlist
get	datafuns	function, ListOfData × nat → Data
getConfirmRelease	userMethods	predicate, nat
getMultipleSelection	userMethods	function, ListOfData × nat → ListOfData
getSingleSelection	userMethods	function, ListOfData × nat → Data
i	int-basic1	variable, int
i0	int-basic1	variable, int
inc	datafuns	function, Data → Data
init	state	predicate, name × Agent → Data
initialstate	gen-systemstate	constant, systemstate
int	int-basic1	sort,
ipurge	MeydenIntrans	function, commandlist × secdomain → commandlist
ipurge	Instance	function, commandlist × domain → commandlist
isAbort8	domain	predicate, domain
isAbort8-UserCmd	command	predicate, command
isAbort9	domain	predicate, domain
isAbort9-UserCmd	command	predicate, command
isAgent	data	predicate, Data
isAirline	Agent	predicate, Agent
isBookFlightOffer	data	predicate, Content
isBookFlightOffer-AirlineCmd	command	predicate, command
isBookFlightOfferstate6-AirlineCmd	command	predicate, command
isBookFlightOfferstate7-AirlineCmd	command	predicate, command
isBookSelected	data	predicate, Content
isBookSelected-TravelPlannerCmd	command	predicate, command
isBookSelectedstate2-TravelPlannerCmd	command	predicate, command
isBoolean	data	predicate, Data
isConfirm	data	predicate, Content
isConfirm-UserCmd-4	command	predicate, command
isConfirmBooking	data	predicate, Content
isConfirmRelease	data	predicate, Content
isConfirmRelease-UserCmd-3	command	predicate, command
isCreditCardCenter	Agent	predicate, Agent
isCreditCardDetails	data	predicate, Data
isDeclassDom	domdefinitions	predicate, domain
isDeclassifiedCCD	data	predicate, Content
isDeclassifiedCCD-TravelPlannerCmd	command	predicate, command
isDeclassify-count	name	predicate, name
isFlightOffer	data	predicate, Data
isGPSPos	data	predicate, Data
isGetDeclassifiedCCD	data	predicate, Content
isGetDeclassifiedCCD-CreditCardCenterCmd	command	predicate, command
isGetFlightOffers	data	predicate, Content
isGetFlightOffers-AirlineCmd	command	predicate, command
isGetFlightOffers-TravelAgencyCmd	command	predicate, command
isGetFlightOffers-TravelPlannerCmd	command	predicate, command
isGetInputAgent	data	predicate, Content
isGetInputAirline	data	predicate, Content
isGetInputBoolean	data	predicate, Content
isGetInputCreditCardCenter	data	predicate, Content
isGetInputCreditCardDetails	data	predicate, Content
isGetInputData	data	predicate, Content
isGetInputFlightOffer	data	predicate, Content
isGetInputGPSPos	data	predicate, Content
isGetInputIFlowUtil	data	predicate, Content
isGetInputInteger	data	predicate, Content
isGetInputRequestData	data	predicate, Content
isGetInputRequestData-UserCmd-1	command	predicate, command
isGetInputString	data	predicate, Content
isGetInputTravelAgency	data	predicate, Content
isGetInputTravelPlanner	data	predicate, Content
isGetMultipleSelection	data	predicate, Content
isGetSingleSelection	data	predicate, Content
isGetSingleSelection-UserCmd-2	command	predicate, command
isHighLow5	domain	predicate, domain
isInit-GetInputRequestData-TravelPlannerCmd	command	predicate, command
isInteger	data	predicate, Data
isListOfData	data	predicate, Data
isListOfFlightOffer	data	predicate, Data
isListOfGPSPos	data	predicate, Data
isLocVar	name	predicate, name
isMailbox	name	predicate, name
isMessage	data	predicate, Data
isNat	data	predicate, Data
isNull-IFlowUtil	datafuns	function, Data → Boolean
isOkConfirmBooking	data	predicate, Content
isOkConfirmBooking-TravelPlannerCmd	command	predicate, command
isOkPayCommission	data	predicate, Content
isOkPayCommission-AirlineCmd	command	predicate, command
isPair	data	predicate, Data
isPayCommission	data	predicate, Content
isPayCommission-TravelAgencyCmd	command	predicate, command
isReadSourceCount	name	predicate, name
isReadSourceInputs	name	predicate, name
isReleaseCCD	data	predicate, Content
isReleaseCCD-CreditCardCenterCmd	command	predicate, command
isRequestData	data	predicate, Data
isRetFlightOffers	data	predicate, Content
isRetFlightOffers-TravelAgencyCmd	command	predicate, command
isRetFlightOffers-TravelPlannerCmd	command	predicate, command
isRetFlightOffersstate1-TravelPlannerCmd	command	predicate, command
isShow	data	predicate, Content
isStart	data	predicate, Content
isState	name	predicate, name
isStateDom	domdefinitions	predicate, domain
isString	data	predicate, Data
isTravelAgency	Agent	predicate, Agent
isTravelPlanner	Agent	predicate, Agent
isTrue	datafuns	predicate, Data
isUser	Agent	predicate, Agent
isUser	domain	predicate, domain
isUser->User_Airline	domain	predicate, domain
isUser-Confirm	name	predicate, name
isUser-Confirm-count	name	predicate, name
isUser-ConfirmRelease	name	predicate, name
isUser-ConfirmRelease-count	name	predicate, name
isUser-ConfirmReleases	name	predicate, name
isUser-ConfirmedRelease-count	name	predicate, name
isUser-Confirms	name	predicate, name
isUser-GetInput	name	predicate, name
isUser-GetInput-count	name	predicate, name
isUser-GetInputs	name	predicate, name
isUser-GetMultipleSelection	name	predicate, name
isUser-GetMultipleSelection-count	name	predicate, name
isUser-GetMultipleSelections	name	predicate, name
isUser-GetSingleSelection	name	predicate, name
isUser-GetSingleSelection-count	name	predicate, name
isUser-GetSingleSelections	name	predicate, name
isUser_Airline	domain	predicate, domain
isUser_TravelAgency_Airline	domain	predicate, domain
isValidCCD-Airline	localMethods	constant, Data
isafterdeclassifyCCD4ASM-CreditCardCenterCmd	command	predicate, command
isdeclassifyCCD4ASM-CreditCardCenterCmd	command	predicate, command
j	int-basic1	variable, int
j0	int-basic1	variable, int
lastn	list-del	function, nat × list → list
lastn	Agentlist	function, nat × Agentlist → Agentlist
list	list-data	sort,
locVar	name	function, string → name
m	nat-basic2	variable, nat
m0	Agent	variable, nat
mailboxNotNull	state	predicate, name × Agent → Data
maxOneNotNull	state	predicate, name × Agent → Data
mkAirline	Agent	function, nat → Agent
mkBookFlightOffer	data	function, Integer × CreditCardDetails → Content
mkBookSelected	data	function, FlightOffer → Content
mkBoolean	data	function, bool → Boolean
mkConfirm	data	constant, Content
mkConfirmBooking	data	function, Integer → Content
mkConfirmRelease	data	function, Data × String → Content
mkCreditCardCenter	Agent	function, nat → Agent
mkCreditCardDetails	data	constant, CreditCardDetails
mkDataPair	data	function, Data × Data → Data
mkDeclassifiedCCD	data	function, CreditCardDetails → Content
mkFlightOffer	data	function, Integer × String → FlightOffer
mkGPSPos	data	function, String × String → GPSPos
mkGetDeclassifiedCCD	data	constant, Content
mkGetFlightOffers	data	function, RequestData → Content
mkGetInputAgent	data	constant, Content
mkGetInputAirline	data	constant, Content
mkGetInputBoolean	data	constant, Content
mkGetInputCreditCardCenter	data	constant, Content
mkGetInputCreditCardDetails	data	constant, Content
mkGetInputData	data	constant, Content
mkGetInputFlightOffer	data	constant, Content
mkGetInputGPSPos	data	constant, Content
mkGetInputIFlowUtil	data	constant, Content
mkGetInputInteger	data	constant, Content
mkGetInputRequestData	data	constant, Content
mkGetInputString	data	constant, Content
mkGetInputTravelAgency	data	constant, Content
mkGetInputTravelPlanner	data	constant, Content
mkGetMultipleSelection	data	function, ListOfData → Content
mkGetSingleSelection	data	function, ListOfData → Content
mkInteger	data	function, int → Integer
mkMessage	data	function, Agentlist × Content → Message
mkNat	data	function, nat → Data
mkOkConfirmBooking	data	constant, Content
mkOkPayCommission	data	constant, Content
mkPayCommission	data	constant, Content
mkReleaseCCD	data	function, String → Content
mkRequestData	data	function, String → RequestData
mkRetFlightOffers	data	function, ListOfFlightOffer → Content
mkShow	data	function, Data → Content
mkStart	data	constant, Content
mkString	data	function, string → String
mkTravelAgency	Agent	function, nat → Agent
mkTravelPlanner	Agent	function, nat → Agent
mkUser	Agent	function, nat → Agent
mklist	gen-command-list	function, command × nat → commandlist
mklist	list-last	function, elem × nat → list
mklist	Agentlist	function, Agent × nat → Agentlist
mklist	Instance	function, action × nat → commandlist
msg	data	variable, Message
msg0	data	variable, Message
n	nat-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
nam	gen-name	variable, name
nam	name	variable, name
nam0	name	variable, name
nam1	name	variable, name
nam2	state	variable, name
nam3	state	variable, name
nam4	state	variable, name
nam5	state	variable, name
name	gen-name	sort,
name	name	sort,
nat	nat-basic1	sort,
nonNull	datafuns	predicate, Data
nonNull	datafuns	predicate, ListOfData
null	gen-value	constant, value
null	data	constant, Data
obs	AccessControl	function, systemstate × secdomain → systemstate
obs	observeAlter	function, name × Agent → Data × domain → name × Agent → Data
observe	AccessControl	predicate, name × secdomain
observe	observeAlter	predicate, domain × name × Agent
okaction	okaction	predicate, action
perm	list-perm	predicate, list × list
perm	Agentlist	predicate, Agentlist × Agentlist
pos	list-del	function, elem × list → nat
pos	string-less	function, char × string → nat
pos	Agentlist	function, Agent × Agentlist → nat
processBooking-Airline	localMethods	function, Integer × CreditCardDetails → Data
restn	list-del	function, nat × list → list
restn	Agentlist	function, nat × Agentlist → Agentlist
rev	gen-command-list	function, commandlist → commandlist
rev	list-last	function, list → list
rev	Agentlist	function, Agentlist → Agentlist
rmdup	gen-command-list	function, commandlist → commandlist
rmdup	list-dup	function, list → list
rmdup	Agentlist	function, Agentlist → Agentlist
run	MeydenIntrans	function, systemstate × commandlist → systemstate
run	MeydenIntrans	function, commandlist → systemstate
run	Instance	function, name × Agent → Data × commandlist → name × Agent → Data
run	Instance	function, commandlist → name × Agent → Data
s	set-basic	variable, set
s	state	variable, name × Agent → Data
s0	set-basic	variable, set
s0	state	variable, name × Agent → Data
s1	set-basic	variable, set
s1	state	variable, name × Agent → Data
s2	set-basic	variable, set
s2	state	variable, name × Agent → Data
s3	state	variable, name × Agent → Data
secdomain	gen-secdomain	sort,
secdomainset	gen-secdomain-set	sort,
secure	MeydenIntrans	predicate, systemstate
secure	Instance	predicate, name × Agent → Data
set	set-basic	sort,
set-airline	datafuns	function, FlightOffer × String → FlightOffer
set-id	datafuns	function, FlightOffer × Integer → FlightOffer
set-latitude	datafuns	function, GPSPos × String → GPSPos
set-longitude	datafuns	function, GPSPos × String → GPSPos
size	datafuns	function, Data → nat
sortedchars	string-less	constant, string
sources	MeydenIntrans	function, commandlist × secdomain → secdomainset
sources	Instance	function, commandlist × domain → secdomainset
state	name	function, string → name
stateNotNull	state	predicate, name × Agent → Data
step	AccessControl	function, systemstate × command → systemstate
str	string-data	variable, string
str0	string-data	variable, string
str1	string-data	variable, string
str2	string-data	variable, string
str3	string-data	variable, string
string	string-data	sort,
stringvar	string-append	variable, string
stringvar0	string-append	variable, string
stringvar1	name	variable, string
stringvar2	name	variable, string
sublist	list-del	function, nat × nat × list → list
sublist	Agentlist	function, nat × nat × Agentlist → Agentlist
sys	gen-systemstate	variable, systemstate
sys0	gen-systemstate	variable, systemstate
sys1	gen-systemstate	variable, systemstate
systemstate	gen-systemstate	sort,
usedDom	domdefinitions	predicate, domain
usedName	namefuns	predicate, name
usedName	namefuns	predicate, name × Agent
v	gen-value	variable, value
v	Instance	variable, Data
v0	gen-value	variable, value
v0	Instance	variable, Data
v1	gen-value	variable, value
v1	Instance	variable, Data
value	gen-value	sort,
wrapAgent2Data	data	function, Agent → Data
wrapBoolean2Data	data	function, Boolean → Data
wrapCreditCardDetails2Data	data	function, CreditCardDetails → Data
wrapFlightOffer2Data	data	function, FlightOffer → Data
wrapGPSPos2Data	data	function, GPSPos → Data
wrapInteger2Data	data	function, Integer → Data
wrapListOfData2Data	data	function, ListOfData → Data
wrapListOfFlightOffer2Data	data	function, ListOfFlightOffer → Data
wrapListOfGPSPos2Data	data	function, ListOfGPSPos → Data
wrapMessage2Data	data	function, Message → Data
wrapRequestData2Data	data	function, RequestData → Data
wrapString2Data	data	function, String → Data
x	list-data	variable, list
x0	list-data	variable, list
x1	list-data	variable, list
x2	list-data	variable, list
y	list-data	variable, list
y0	list-data	variable, list
y1	list-data	variable, list
y2	list-data	variable, list
z	list-data	variable, list
z0	list-data	variable, list
z1	list-data	variable, list
z2	list-data	variable, list
}	gen-secdomain-set	function, secdomain → secdomainset
}	set-union	function, elem → set
}	Instance	function, domain → secdomainset
}	domains	function, domain → domains
}	Agents	function, Agent → Agents
~	int-abs	function, int → int
≤	int-abs	predicate, int × int
≤	nat	predicate, nat × nat
≥	int-abs	predicate, int × int
≥	nat	predicate, nat × nat
∈	gen-secdomain-set	predicate, secdomain × secdomainset
∈	set-basic	predicate, elem × set
∈	gen-command-list	predicate, command × commandlist
∈	list	predicate, elem × list
∈	Agentlist	predicate, Agent × Agentlist
∈	Instance	predicate, action × commandlist
∈	Instance	predicate, domain × secdomainset
∈	domains	predicate, domain × domains
∈	Agents	predicate, Agent × Agents
∪	gen-secdomain-set	function, secdomainset × secdomainset → secdomainset
∪	set-union	function, set × set → set
∪	list-set	function, list × list → list
∪	Agentlist	function, Agentlist × Agentlist → Agentlist
∪	domains	function, domains × domains → domains
∪	Agents	function, Agents × Agents → Agents
∩	gen-secdomain-set	function, secdomainset × secdomainset → secdomainset
∩	set-union	function, set × set → set
∩	domains	function, domains × domains → domains
∩	Agents	function, Agents × Agents → Agents
⇒	AccessControl	predicate, secdomain × secdomain
⇒	dominterference	predicate, domain × domain
⇒	dominterference	predicate, domains × domains
⇒1	Properties	predicate, domain × domain
⇒1	Properties	predicate, domains × domains
⇒2	Properties	predicate, domain × domain
⇒2	Properties	predicate, domains × domains
⊆	gen-secdomain-set	predicate, secdomainset × secdomainset
⊆	set-basic	predicate, set × set
⊆	list-set	predicate, list × list
⊆	Agentlist	predicate, Agentlist × Agentlist
⊆	domains	predicate, domains × domains
⊆	Agents	predicate, Agents × Agents
⊆m	list-perm	predicate, list × list
⊆m	Agentlist	predicate, Agentlist × Agentlist
⊑	gen-command-list	predicate, commandlist × commandlist
⊑	list-last	predicate, list × list
⊑	Agentlist	predicate, Agentlist × Agentlist
⊒	gen-command-list	predicate, commandlist × commandlist
⊒	list-last	predicate, list × list
⊒	Agentlist	predicate, Agentlist × Agentlist
∅	gen-secdomain-set	constant, secdomainset
∅	set-basic	constant, set
∅	domains	constant, domains
∅	Agents	constant, Agents