[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
# .datafListOfData → nat
# .AgentsfAgents → nat
# .string-lessfstring → nat
# .AgentlistfAgentlist → nat
#ocAgentlistfAgent × Agentlist → nat
. 'string-appendfchar → string
. 'AgentlistfAgent → Agentlist
. * .nat-multfnat × nat → nat
. * .int-multfint × int → int
. + .datafunsfInteger × Integer → Integer
. + .nat-basic2fnat × nat → nat
. + .datafData × ListOfData → ListOfData
. + .datafGPSPos × ListOfGPSPos → ListOfGPSPos
. + .int-basic2fint × int → int
. + .datafFlightOffer × ListOfFlightOffer → ListOfFlightOffer
. + .string-datafchar × string → string
. + .AgentlistfAgent × Agent → Agentlist
. + .string-appendfstring × string → string
. + .AgentlistfAgentlist × Agent → Agentlist
. + .AgentlistfAgent × Agentlist → Agentlist
. + .AgentlistfAgentlist × Agentlist → Agentlist
. ++ .AgentsfAgents × Agent → Agents
. ++ .AgentlistfAgentlist × Agent → Agentlist
. +1nat-basic1fnat → nat
. +1int-basic1fint → int
. - .datafunsfInteger × Integer → Integer
. - .natfnat × nat → nat
. - .int-absfint × int → int
. -- .AgentsfAgents × Agent → Agents
. -1nat-basic1fnat → nat
. -1int-basic1fint → int
. -1l .AgentlistfAgentlist × nat → Agentlist
. -1l .AgentlistfAgentlist × Agent → Agentlist
. -l .AgentlistfAgentlist × Agent → Agentlist
. .1datafData → Data
. .2datafData → Data
. .AgentdatafData → Agent
. .agentlistdatafMessage → Agentlist
. .airlinedatafFlightOffer → String
. .BooleandatafData → Boolean
. .butlastAgentlistfAgentlist → Agentlist
. .callnamefname → string
. .ccddatafContent → CreditCardDetails
. .char1string-datafstring → char
. .cmdactionfaction → command
. .cmdnamefname → command
. .contentdatafMessage → Content
. .CreditCardDetailsdatafData → CreditCardDetails
. .datadatafContent → Data
. .datedatafRequestData → String
. .firstdatafListOfData → Data
. .firstdatafListOfGPSPos → GPSPos
. .firstAgentlistfAgentlist → Agent
. .firstdatafListOfFlightOffer → FlightOffer
. .flightOfferdatafContent → FlightOffer
. .FlightOfferdatafData → FlightOffer
. .flightOffersdatafContent → ListOfFlightOffer
. .fromactionfaction → Agent
. .GPSPosdatafData → GPSPos
. .idAgentfAgent → nat
. .iddatafContent → Integer
. .iddatafFlightOffer → Integer
. .IntegerdatafData → Integer
. .lastAgentlistfAgentlist → Agent
. .latitudedatafGPSPos → String
. .ListOfDatadatafData → ListOfData
. .ListOfFlightOfferdatafData → ListOfFlightOffer
. .ListOfGPSPosdatafData → ListOfGPSPos
. .longitudedatafGPSPos → String
. .methodnamenamefname → string
. .msgdatafData → Message
. .namenamefname → string
. .natdatafData → nat
. .receiverdatafContent → String
. .RequestDatadatafData → RequestData
. .requestDatadatafContent → RequestData
. .restdatafListOfData → ListOfData
. .restdatafListOfGPSPos → ListOfGPSPos
. .restdatafListOfFlightOffer → ListOfFlightOffer
. .restAgentlistfAgentlist → Agentlist
. .rstringstring-datafstring → string
. .selectiondatafContent → ListOfData
. .StringdatafData → String
. .toactionfaction → Agent
. .valuedatapBoolean
. .valuedatafString → string
. .valuedatafInteger → int
. .whatdatafContent → Data
. < .datapListOfData × ListOfData
. < .AgentlistpAgentlist × Agentlist
. < .string-lesspchar × char
. < .datafunsfInteger × Integer → Boolean
. < .string-lesspstring × string
. < .int-basic1pint × int
. < .nat-basic1pnat × nat
. <= .datafunsfInteger × Integer → Boolean
. > .int-abspint × int
. > .datafunsfInteger × Integer → Boolean
. > .natpnat × nat
. >= .datafunsfInteger × Integer → Boolean
. [ . ]AgentlistfAgentlist × nat → Agent
. [ . ]AgentlistfAgentlist × nat × Agent → Agentlist
. \ .AgentsfAgents × Agents → Agents
. \ .AgentlistfAgentlist × Agentlist → Agentlist
. ≤ .int-abspint × int
. ≤ .natpnat × nat
. ≥ .int-abspint × int
. ≥ .natpnat × nat
. ∈ .AgentlistpAgent × Agentlist
. ∈ .AgentspAgent × Agents
. ∪ .AgentsfAgents × Agents → Agents
. ∪ .AgentlistfAgentlist × Agentlist → Agentlist
. ∩ .AgentsfAgents × Agents → Agents
. ⊆ .AgentlistpAgentlist × Agentlist
. ⊆ .AgentspAgents × Agents
. ⊆m .AgentlistpAgentlist × Agentlist
. ⊑ .AgentlistpAgentlist × Agentlist
. ⊒ .AgentlistpAgentlist × Agentlist
[]AgentlistcAgentlist
[]datacListOfFlightOffer
[]datacListOfGPSPos
[]datacListOfData
{ . }AgentsfAgent → Agents
~ .int-absfint → int
∅AgentscAgents
aactionvaction
a_BooleandatavBoolean
a_Boolean0datavBoolean
a_Boolean1datavBoolean
a_Boolean2datavBoolean
a_CreditCardDetailsdatavCreditCardDetails
a_CreditCardDetails0datavCreditCardDetails
a_CreditCardDetails1datavCreditCardDetails
a_CreditCardDetails2datavCreditCardDetails
a_FlightOfferdatavFlightOffer
a_FlightOffer0datavFlightOffer
a_FlightOffer1datavFlightOffer
a_FlightOffer2datavFlightOffer
a_GPSPosdatavGPSPos
a_GPSPos0datavGPSPos
a_GPSPos1datavGPSPos
a_GPSPos2datavGPSPos
a_IntegerdatavInteger
a_Integer0datavInteger
a_Integer1datavInteger
a_Integer2datavInteger
a_ListOfDatadatavListOfData
a_ListOfData0datavListOfData
a_ListOfFlightOfferdatavListOfFlightOffer
a_ListOfFlightOffer0datavListOfFlightOffer
a_ListOfGPSPosdatavListOfGPSPos
a_ListOfGPSPos0datavListOfGPSPos
a_RequestDatadatavRequestData
a_RequestData0datavRequestData
a_RequestData1datavRequestData
a_RequestData2datavRequestData
a_StringdatavString
a_String0datavString
a_String1datavString
a_String2datavString
a0actionvaction
a1actionvaction
a2actionvaction
Abort8domaincdomain
Abort8-UserCmdcommandccommand
Abort9domaincdomain
Abort9-UserCmdcommandccommand
absint-absfint → int
actionactions
ActionactionfAgent × command × Agent → action
afterdeclassifyCCD4ASM-CreditCardCenterCmdcommandccommand
agAgentvAgent
ag0AgentvAgent
ag1AgentvAgent
ag2actionvAgent
ag3statevAgent
ag4statevAgent
ag5statevAgent
AgentAgents
AgentlistAgentlists
AgentsAgentss
aglAgentlistvAgentlist
agl0AgentlistvAgentlist
agl1AgentlistvAgentlist
agl10AgentlistvAgentlist
agl2AgentlistvAgentlist
agl3AgentlistvAgentlist
agl4AgentlistvAgentlist
agl5AgentlistvAgentlist
agl6AgentlistvAgentlist
agl7AgentlistvAgentlist
agl8AgentlistvAgentlist
agl9AgentlistvAgentlist
agsAgentsvAgents
ags0AgentsvAgents
ags1AgentsvAgents
ags2AgentsvAgents
Airline-flightOffersnamecname
allNullstatep(name × Agent → Data)
alterobserveAlterpdomain × name × Agent
BookFlightOffer-AirlineCmdcommandccommand
BookFlightOfferstate6-AirlineCmdcommandccommand
BookFlightOfferstate7-AirlineCmdcommandccommand
BookSelected-TravelPlannerCmdcommandccommand
BookSelectedstate2-TravelPlannerCmdcommandccommand
boolbools
Booleandatas
boolvarboolvbool
boolvar0boolvbool
butlastnAgentlistfnat × Agentlist → Agentlist
charchars
charcharvchar
char0charvchar
char1charvchar
char2charvchar
char3string-lessvchar
cmdcommandvcommand
cmd0commandvcommand
cmd1commandvcommand
cmd2commandvcommand
cntntdatavContent
cntnt0datavContent
cntnt1datavContent
commandcommands
Confirm-UserCmd-4commandccommand
ConfirmRelease-UserCmd-3commandccommand
Contentdatas
CreditCardCenter-ccdnamecname
CreditCardDetailsdatas
ddatavData
d0datavData
d1datavData
d2datavData
d4statevData
d5statevData
Datadatas
DeclassifiedCCD-TravelPlannerCmdcommandccommand
declassify-countnamefstring → name
declassifyCCD4ASM-CreditCardCenterCmdcommandccommand
disjAgentlistpAgentlist × Agentlist
dldatavListOfData
dl0datavListOfData
dl1datavListOfData
dl10datavListOfData
dl2datavListOfData
dl3datavListOfData
dl4datavListOfData
dl5datavListOfData
dl6datavListOfData
dl7datavListOfData
dl8datavListOfData
dl9datavListOfData
domaindomains
domvardomainvdomain
domvar0domainvdomain
domvar1domainvdomain
dupsAgentlistpAgentlist
exAgentexAgentpAgent
exAirlineexAgentpAgent
exCreditCardCenterexAgentpAgent
exTravelAgencyexAgentpAgent
exTravelPlannerexAgentpAgent
exUserexAgentpAgent
fillfirstAgentlistfnat × Agent × Agentlist → Agentlist
filterAgentlistfAgentlist × Agentlist → Agentlist
firstnAgentlistfnat × Agentlist → Agentlist
FlightOfferdatas
fromeAgentlistfAgentlist × Agent → Agentlist
getdatafunsfListOfData × nat → Data
GetDeclassifiedCCD-CreditCardCenterCmdcommandccommand
GetFlightOffers-AirlineCmdcommandccommand
GetFlightOffers-TravelAgencyCmdcommandccommand
GetFlightOffers-TravelPlannerCmdcommandccommand
GetInputRequestData-UserCmd-1commandccommand
GetSingleSelection-UserCmd-2commandccommand
GPSPosdatas
HighLow5domaincdomain
iint-basic1vint
i0int-basic1vint
incdatafunsfData → Data
initstatep(name × Agent → Data)
Init-GetInputRequestData-TravelPlannerCmdcommandccommand
intint-basic1s
Integerdatas
isAbort8domainpdomain
isAbort8-UserCmdcommandpcommand
isAbort9domainpdomain
isAbort9-UserCmdcommandpcommand
isafterdeclassifyCCD4ASM-CreditCardCenterCmdcommandpcommand
isAgentdatapData
isAirlineAgentpAgent
isBookFlightOfferdatapContent
isBookFlightOffer-AirlineCmdcommandpcommand
isBookFlightOfferstate6-AirlineCmdcommandpcommand
isBookFlightOfferstate7-AirlineCmdcommandpcommand
isBookSelecteddatapContent
isBookSelected-TravelPlannerCmdcommandpcommand
isBookSelectedstate2-TravelPlannerCmdcommandpcommand
isBooleandatapData
isConfirmdatapContent
isConfirm-UserCmd-4commandpcommand
isConfirmBookingdatapContent
isConfirmReleasedatapContent
isConfirmRelease-UserCmd-3commandpcommand
isCreditCardCenterAgentpAgent
isCreditCardDetailsdatapData
isDeclassifiedCCDdatapContent
isDeclassifiedCCD-TravelPlannerCmdcommandpcommand
isDeclassify-countnamepname
isdeclassifyCCD4ASM-CreditCardCenterCmdcommandpcommand
isFlightOfferdatapData
isGetDeclassifiedCCDdatapContent
isGetDeclassifiedCCD-CreditCardCenterCmdcommandpcommand
isGetFlightOffersdatapContent
isGetFlightOffers-AirlineCmdcommandpcommand
isGetFlightOffers-TravelAgencyCmdcommandpcommand
isGetFlightOffers-TravelPlannerCmdcommandpcommand
isGetInputAgentdatapContent
isGetInputAirlinedatapContent
isGetInputBooleandatapContent
isGetInputCreditCardCenterdatapContent
isGetInputCreditCardDetailsdatapContent
isGetInputDatadatapContent
isGetInputFlightOfferdatapContent
isGetInputGPSPosdatapContent
isGetInputIFlowUtildatapContent
isGetInputIntegerdatapContent
isGetInputRequestDatadatapContent
isGetInputRequestData-UserCmd-1commandpcommand
isGetInputStringdatapContent
isGetInputTravelAgencydatapContent
isGetInputTravelPlannerdatapContent
isGetMultipleSelectiondatapContent
isGetSingleSelectiondatapContent
isGetSingleSelection-UserCmd-2commandpcommand
isGPSPosdatapData
isHighLow5domainpdomain
isInit-GetInputRequestData-TravelPlannerCmdcommandpcommand
isIntegerdatapData
isListOfDatadatapData
isListOfFlightOfferdatapData
isListOfGPSPosdatapData
isLocVarnamepname
isMailboxnamepname
isMessagedatapData
isNatdatapData
isNull-IFlowUtildatafunsfData → Boolean
isOkConfirmBookingdatapContent
isOkConfirmBooking-TravelPlannerCmdcommandpcommand
isOkPayCommissiondatapContent
isOkPayCommission-AirlineCmdcommandpcommand
isPairdatapData
isPayCommissiondatapContent
isPayCommission-TravelAgencyCmdcommandpcommand
isReadSourceCountnamepname
isReadSourceInputsnamepname
isReleaseCCDdatapContent
isReleaseCCD-CreditCardCenterCmdcommandpcommand
isRequestDatadatapData
isRetFlightOffersdatapContent
isRetFlightOffers-TravelAgencyCmdcommandpcommand
isRetFlightOffers-TravelPlannerCmdcommandpcommand
isRetFlightOffersstate1-TravelPlannerCmdcommandpcommand
isShowdatapContent
isStartdatapContent
isStatenamepname
isStringdatapData
isTravelAgencyAgentpAgent
isTravelPlannerAgentpAgent
isTruedatafunspData
isUserAgentpAgent
isUserdomainpdomain
isUser->User_Airlinedomainpdomain
isUser-Confirmnamepname
isUser-Confirm-countnamepname
isUser-ConfirmedRelease-countnamepname
isUser-ConfirmReleasenamepname
isUser-ConfirmRelease-countnamepname
isUser-ConfirmReleasesnamepname
isUser-Confirmsnamepname
isUser-GetInputnamepname
isUser-GetInput-countnamepname
isUser-GetInputsnamepname
isUser-GetMultipleSelectionnamepname
isUser-GetMultipleSelection-countnamepname
isUser-GetMultipleSelectionsnamepname
isUser-GetSingleSelectionnamepname
isUser-GetSingleSelection-countnamepname
isUser-GetSingleSelectionsnamepname
isUser_Airlinedomainpdomain
isUser_TravelAgency_Airlinedomainpdomain
jint-basic1vint
j0int-basic1vint
lastnAgentlistfnat × Agentlist → Agentlist
ListOfDatadatas
ListOfData2ListOfFlightOfferdatafunsfListOfData → ListOfFlightOffer
ListOfData2ListOfGPSPosdatafunsfListOfData → ListOfGPSPos
ListOfFlightOfferdatas
ListOfFlightOffer2ListOfDatadatafunsfListOfFlightOffer → ListOfData
ListOfGPSPosdatas
ListOfGPSPos2ListOfDatadatafunsfListOfGPSPos → ListOfData
locVarnamefstring → name
mnat-basic2vnat
m0Agentvnat
Mailboxnamefcommand → name
mailboxNotNullstatep(name × Agent → Data)
maxOneNotNullstatep(name × Agent → Data)
Messagedatas
mkAirlineAgentfnat → Agent
mkBookFlightOfferdatafInteger × CreditCardDetails → Content
mkBookSelecteddatafFlightOffer → Content
mkBooleandatafbool → Boolean
mkConfirmdatacContent
mkConfirmBookingdatafInteger → Content
mkConfirmReleasedatafData × String → Content
mkCreditCardCenterAgentfnat → Agent
mkCreditCardDetailsdatacCreditCardDetails
mkDataPairdatafData × Data → Data
mkDeclassifiedCCDdatafCreditCardDetails → Content
mkFlightOfferdatafInteger × String → FlightOffer
mkGetDeclassifiedCCDdatacContent
mkGetFlightOffersdatafRequestData → Content
mkGetInputAgentdatacContent
mkGetInputAirlinedatacContent
mkGetInputBooleandatacContent
mkGetInputCreditCardCenterdatacContent
mkGetInputCreditCardDetailsdatacContent
mkGetInputDatadatacContent
mkGetInputFlightOfferdatacContent
mkGetInputGPSPosdatacContent
mkGetInputIFlowUtildatacContent
mkGetInputIntegerdatacContent
mkGetInputRequestDatadatacContent
mkGetInputStringdatacContent
mkGetInputTravelAgencydatacContent
mkGetInputTravelPlannerdatacContent
mkGetMultipleSelectiondatafListOfData → Content
mkGetSingleSelectiondatafListOfData → Content
mkGPSPosdatafString × String → GPSPos
mkIntegerdatafint → Integer
mklistAgentlistfAgent × nat → Agentlist
mkMessagedatafAgentlist × Content → Message
mkNatdatafnat → Data
mkOkConfirmBookingdatacContent
mkOkPayCommissiondatacContent
mkPayCommissiondatacContent
mkReleaseCCDdatafString → Content
mkRequestDatadatafString → RequestData
mkRetFlightOffersdatafListOfFlightOffer → Content
mkShowdatafData → Content
mkStartdatacContent
mkStringdatafstring → String
mkTravelAgencyAgentfnat → Agent
mkTravelPlannerAgentfnat → Agent
mkUserAgentfnat → Agent
msgdatavMessage
msg0datavMessage
nnat-basic1vnat
n0nat-basic1vnat
n1nat-basic1vnat
namnamevname
nam0namevname
nam1namevname
nam2statevname
nam3statevname
nam4statevname
nam5statevname
namenames
natnat-basic1s
nonNulldatafunspListOfData
nonNulldatafunspData
nulldatacData
NUMOFAirlineexAgentcnat
NUMOFAPPSANDUSERSexAgentcnat
NUMOFCreditCardCenterexAgentcnat
NUMOFTravelAgencyexAgentcnat
NUMOFTravelPlannerexAgentcnat
NUMOFUserexAgentcnat
obsobserveAlterf(name × Agent → Data) × domain → name × Agent → Data
observeobserveAlterpdomain × name × Agent
okactionokactionpaction
OkConfirmBooking-TravelPlannerCmdcommandccommand
OkPayCommission-AirlineCmdcommandccommand
PayCommission-TravelAgencyCmdcommandccommand
permAgentlistpAgentlist × Agentlist
posAgentlistfAgent × Agentlist → nat
posstring-lessfchar × string → nat
ReadSourceCountnamefstring × string → name
ReadSourceInputsnamefstring × string → name
ReleaseCCD-CreditCardCenterCmdcommandccommand
RequestDatadatas
restnAgentlistfnat × Agentlist → Agentlist
RetFlightOffers-TravelAgencyCmdcommandccommand
RetFlightOffers-TravelPlannerCmdcommandccommand
RetFlightOffersstate1-TravelPlannerCmdcommandccommand
revAgentlistfAgentlist → Agentlist
rmdupAgentlistfAgentlist → Agentlist
sstatevname × Agent → Data
s0statevname × Agent → Data
s1statevname × Agent → Data
s2statevname × Agent → Data
s3statevname × Agent → Data
set-airlinedatafunsfFlightOffer × String → FlightOffer
set-iddatafunsfFlightOffer × Integer → FlightOffer
set-latitudedatafunsfGPSPos × String → GPSPos
set-longitudedatafunsfGPSPos × String → GPSPos
sizedatafunsfData → nat
sortedcharsstring-lesscstring
statenamefstring → name
stateNotNullstatep(name × Agent → Data)
strstring-datavstring
str0string-datavstring
str1string-datavstring
str2string-datavstring
str3string-datavstring
stringstring-datas
Stringdatas
stringvarstring-appendvstring
stringvar0string-appendvstring
stringvar1namevstring
stringvar2namevstring
sublistAgentlistfnat × nat × Agentlist → Agentlist
TravelPlanner-flightOffernamecname
usedNamenamefunspname × Agent
usedNamenamefunspname
Userdomaincdomain
User->User_Airlinedomaincdomain
User-Confirmnamefstring → name
User-Confirm-countnamefstring → name
User-ConfirmedRelease-countnamefstring → name
User-ConfirmReleasenamefstring → name
User-ConfirmRelease-countnamefstring → name
User-ConfirmReleasesnamefstring → name
User-Confirmsnamefstring → name
User-GetInputnamefstring → name
User-GetInput-countnamefstring → name
User-GetInputsnamefstring → name
User-GetMultipleSelectionnamefstring → name
User-GetMultipleSelection-countnamefstring → name
User-GetMultipleSelectionsnamefstring → name
User-GetSingleSelectionnamefstring → name
User-GetSingleSelection-countnamefstring → name
User-GetSingleSelectionsnamefstring → name
User_Airlinedomaincdomain
User_TravelAgency_Airlinedomaincdomain
wrapAgent2DatadatafAgent → Data
wrapBoolean2DatadatafBoolean → Data
wrapCreditCardDetails2DatadatafCreditCardDetails → Data
wrapFlightOffer2DatadatafFlightOffer → Data
wrapGPSPos2DatadatafGPSPos → Data
wrapInteger2DatadatafInteger → Data
wrapListOfData2DatadatafListOfData → Data
wrapListOfFlightOffer2DatadatafListOfFlightOffer → Data
wrapListOfGPSPos2DatadatafListOfGPSPos → Data
wrapMessage2DatadatafMessage → Data
wrapRequestData2DatadatafRequestData → Data
wrapString2DatadatafString → Data