[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,
asm specification
ASM#
using ASMAUX
target
procedures
ASM# : (name × Agent → Data) × bool nonfunctional nondeterministic;
STEP : (name × Agent → Data) × bool nonfunctional nondeterministic;
EXEC action : (name × Agent → Data) nonfunctional;
Init-GetInputRequestData-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
GetFlightOffers-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
RetFlightOffersstate1-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
BookSelectedstate2-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
DeclassifiedCCD-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
OkConfirmBooking-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
GetFlightOffers-TravelAgencyCmd# action : (name × Agent → Data) nonfunctional;
RetFlightOffers-TravelAgencyCmd# action : (name × Agent → Data) nonfunctional;
PayCommission-TravelAgencyCmd# action : (name × Agent → Data) nonfunctional;
ReleaseCCD-CreditCardCenterCmd# action : (name × Agent → Data) nonfunctional;
GetDeclassifiedCCD-CreditCardCenterCmd# action : (name × Agent → Data) nonfunctional;
GetFlightOffers-AirlineCmd# action : (name × Agent → Data) nonfunctional;
BookFlightOfferstate7-AirlineCmd# action : (name × Agent → Data) nonfunctional;
OkPayCommission-AirlineCmd# action : (name × Agent → Data) nonfunctional;
GetInputRequestData-UserCmd-1# action : (name × Agent → Data) nonfunctional;
GetSingleSelection-UserCmd-2# action : (name × Agent → Data) nonfunctional;
ConfirmRelease-UserCmd-3# action : (name × Agent → Data) nonfunctional;
Confirm-UserCmd-4# action : (name × Agent → Data) nonfunctional;
RetFlightOffers-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
BookSelected-TravelPlannerCmd# action : (name × Agent → Data) nonfunctional;
declassifyCCD4ASM-CreditCardCenterCmd# action : (name × Agent → Data) nonfunctional;
afterdeclassifyCCD4ASM-CreditCardCenterCmd# action : (name × Agent → Data) nonfunctional;
BookFlightOffer-AirlineCmd# action : (name × Agent → Data) nonfunctional;
BookFlightOfferstate6-AirlineCmd# action : (name × Agent → Data) nonfunctional;
Abort8-UserCmd# action : (name × Agent → Data) nonfunctional;
Abort9-UserCmd# action : (name × Agent → Data) nonfunctional;
input variables ;
state variables s, boolvar;
initial state init(s)
final state boolvar
asm rule STEP
declaration
asm : ASM# (;s, boolvar)
{
while ¬ boolvar do STEP
};, STEP : STEP (;s, boolvar)
{
choose a with true in EXEC ; boolvar := [?]
};,
EXEC
: EXEC (a; s)
{
if okaction(a)
then {
s := s ;
let cmd = a .cmd
in if isInit-GetInputRequestData-TravelPlannerCmd(cmd)
then Init-GetInputRequestData-TravelPlannerCmd#
else if isGetFlightOffers-TravelPlannerCmd(cmd)
then GetFlightOffers-TravelPlannerCmd#
else if isRetFlightOffersstate1-TravelPlannerCmd(cmd)
then RetFlightOffersstate1-TravelPlannerCmd#
else if isBookSelectedstate2-TravelPlannerCmd(cmd)
then BookSelectedstate2-TravelPlannerCmd#
else if isDeclassifiedCCD-TravelPlannerCmd(cmd)
then DeclassifiedCCD-TravelPlannerCmd#
else if isOkConfirmBooking-TravelPlannerCmd(cmd)
then OkConfirmBooking-TravelPlannerCmd#
else if isGetFlightOffers-TravelAgencyCmd(cmd)
then GetFlightOffers-TravelAgencyCmd#
else if isRetFlightOffers-TravelAgencyCmd(cmd)
then RetFlightOffers-TravelAgencyCmd#
else if isPayCommission-TravelAgencyCmd(cmd)
then PayCommission-TravelAgencyCmd#
else if isReleaseCCD-CreditCardCenterCmd(cmd)
then ReleaseCCD-CreditCardCenterCmd#
else if isGetDeclassifiedCCD-CreditCardCenterCmd(cmd)
then GetDeclassifiedCCD-CreditCardCenterCmd#
else if isGetFlightOffers-AirlineCmd(cmd)
then GetFlightOffers-AirlineCmd#
else if isBookFlightOfferstate7-AirlineCmd(cmd)
then BookFlightOfferstate7-AirlineCmd#
else if isOkPayCommission-AirlineCmd(cmd)
then OkPayCommission-AirlineCmd#
else if isGetInputRequestData-UserCmd-1(cmd)
then GetInputRequestData-UserCmd-1#
else if isGetSingleSelection-UserCmd-2(cmd)
then GetSingleSelection-UserCmd-2#
else if isConfirmRelease-UserCmd-3(cmd)
then ConfirmRelease-UserCmd-3#
else if isConfirm-UserCmd-4(cmd)
then Confirm-UserCmd-4#
else if isRetFlightOffers-TravelPlannerCmd
(cmd)
then RetFlightOffers-TravelPlannerCmd#
else if isBookSelected-TravelPlannerCmd
(cmd)
then BookSelected-TravelPlannerCmd#
else if isdeclassifyCCD4ASM-CreditCardCenterCmd
(cmd)
then declassifyCCD4ASM-CreditCardCenterCmd#
else if isafterdeclassifyCCD4ASM-CreditCardCenterCmd
(cmd)
then afterdeclassifyCCD4ASM-CreditCardCenterCmd#
else if isBookFlightOffer-AirlineCmd
(cmd)
then BookFlightOffer-AirlineCmd#
else if isBookFlightOfferstate6-AirlineCmd
(cmd)
then BookFlightOfferstate6-AirlineCmd#
else if isAbort8-UserCmd
(cmd)
then Abort8-UserCmd#
else if isAbort9-UserCmd
(cmd)
then Abort9-UserCmd#
}
};,
Init-GetInputRequestData-TravelPlannerCmd#
: Init-GetInputRequestData-TravelPlannerCmd# (a; s)
{
if s(state(`init'), mkUser(a .to .id)) ≠ null
then let agl = s(state(`init'), mkUser(a .to .id)) .msg .agentlist
in {
s(state(`init'), mkUser(a .to .id)) := null ;
s(Mailbox(GetInputRequestData-UserCmd-1), mkUser(a .to .id)) := wrapMessage2Data(mkMessage(agl, mkGetInputRequestData))
}
};,
GetFlightOffers-TravelPlannerCmd#
: GetFlightOffers-TravelPlannerCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isGetFlightOffers(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`requestData'), a .to) := wrapRequestData2Data(d .msg .content .requestData) ;
s(Mailbox(GetFlightOffers-TravelAgencyCmd), mkTravelAgency(0)) := wrapMessage2Data
(mkMessage
(a .to + agl,
mkGetFlightOffers
(s(locVar(`requestData'), a .to) .RequestData)))
}
};,
RetFlightOffersstate1-TravelPlannerCmd#
: RetFlightOffersstate1-TravelPlannerCmd# (a; s)
{
if s(state(`state1'), a .to) ≠ null
then let agl = s(state(`state1'), a .to) .msg .agentlist
in {
s(state(`state1'), a .to) := null ;
s(Mailbox(GetSingleSelection-UserCmd-2), mkUser(a .to .id)) := wrapMessage2Data
(mkMessage
(agl,
mkGetSingleSelection
(ListOfFlightOffer2ListOfData
(s(locVar(`flightOffers'), a .to) .ListOfFlightOffer))))
}
};,
BookSelectedstate2-TravelPlannerCmd#
: BookSelectedstate2-TravelPlannerCmd# (a; s)
{
if s(state(`state2'), a .to) ≠ null
then let agl = s(state(`state2'), a .to) .msg .agentlist
in {
s(state(`state2'), a .to) := null ;
s(Mailbox(ReleaseCCD-CreditCardCenterCmd), mkCreditCardCenter(a .to .id)) := wrapMessage2Data
(mkMessage
(agl,
mkReleaseCCD
(s(TravelPlanner-flightOffer, a .to)
.FlightOffer
.airline)))
}
};,
DeclassifiedCCD-TravelPlannerCmd#
: DeclassifiedCCD-TravelPlannerCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isDeclassifiedCCD(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`ccd_decl'), a .to) := wrapCreditCardDetails2Data(d .msg .content .ccd) ;
s(Mailbox(BookFlightOffer-AirlineCmd), mkAirline(0)) := wrapMessage2Data
(mkMessage
(a .to + agl,
mkBookFlightOffer
(s(TravelPlanner-flightOffer, a .to) .FlightOffer .id,
s(locVar(`ccd_decl'), a .to) .CreditCardDetails)))
}
};,
OkConfirmBooking-TravelPlannerCmd#
: OkConfirmBooking-TravelPlannerCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isOkConfirmBooking(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(Mailbox(Confirm-UserCmd-4), mkUser(a .to .id)) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
GetFlightOffers-TravelAgencyCmd#
: GetFlightOffers-TravelAgencyCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isGetFlightOffers(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`requestData'), a .to) := wrapRequestData2Data(d .msg .content .requestData) ;
s(Mailbox(GetFlightOffers-AirlineCmd), mkAirline(0)) := wrapMessage2Data
(mkMessage
(a .to + agl,
mkGetFlightOffers(s(locVar(`requestData'), a .to) .RequestData)))
}
};,
RetFlightOffers-TravelAgencyCmd#
: RetFlightOffers-TravelAgencyCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isRetFlightOffers(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`flightOffers'), a .to) := wrapListOfFlightOffer2Data(d .msg .content .flightOffers) ;
if agl ≠ [] ∧ exTravelPlanner(agl .first)
then s(Mailbox(RetFlightOffers-TravelPlannerCmd), agl .first) := wrapMessage2Data
(mkMessage
(agl .rest,
mkRetFlightOffers
(s(locVar(`flightOffers'), a .to) .ListOfFlightOffer)))
}
};,
PayCommission-TravelAgencyCmd#
: PayCommission-TravelAgencyCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isPayCommission(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
if agl ≠ [] ∧ exAirline(agl .first)
then s(Mailbox(OkPayCommission-AirlineCmd), agl .first) := wrapMessage2Data(mkMessage(agl .rest, mkOkPayCommission))
}
};,
ReleaseCCD-CreditCardCenterCmd#
: ReleaseCCD-CreditCardCenterCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isReleaseCCD(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`airline'), a .to) := wrapString2Data(d .msg .content .receiver) ;
s(Mailbox(ConfirmRelease-UserCmd-3), mkUser(a .to .id)) := wrapMessage2Data
(mkMessage
(agl,
mkConfirmRelease
(wrapCreditCardDetails2Data
(s(CreditCardCenter-ccd, a .to) .CreditCardDetails),
s(locVar(`airline'), a .to) .String)))
}
};,
GetDeclassifiedCCD-CreditCardCenterCmd#
: GetDeclassifiedCCD-CreditCardCenterCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isGetDeclassifiedCCD(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ; s(state(`state3'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
GetFlightOffers-AirlineCmd#
: GetFlightOffers-AirlineCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isGetFlightOffers(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`requestData'), a .to) := wrapRequestData2Data(d .msg .content .requestData) ;
s(locVar(`filteredFlightOffers'), a .to) := wrapListOfFlightOffer2Data
(filterOffers-Airline
(s(locVar(`requestData'), a .to) .RequestData,
s(Airline-flightOffers, a .to) .ListOfFlightOffer)) ;
if agl ≠ [] ∧ exTravelAgency(agl .first)
then s(Mailbox(RetFlightOffers-TravelAgencyCmd), agl .first) := wrapMessage2Data
(mkMessage
(agl .rest,
mkRetFlightOffers
(s(locVar(`filteredFlightOffers'), a .to)
.ListOfFlightOffer)))
}
};,
BookFlightOfferstate7-AirlineCmd#
: BookFlightOfferstate7-AirlineCmd# (a; s)
{
if s(state(`state7'), a .to) ≠ null
then let agl = s(state(`state7'), a .to) .msg .agentlist
in {
s(state(`state7'), a .to) := null ;
s(Mailbox(PayCommission-TravelAgencyCmd), mkTravelAgency(0)) := wrapMessage2Data(mkMessage(a .to + agl, mkPayCommission))
}
};,
OkPayCommission-AirlineCmd#
: OkPayCommission-AirlineCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isOkPayCommission(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
if agl ≠ [] ∧ exTravelPlanner(agl .first)
then s(Mailbox(OkConfirmBooking-TravelPlannerCmd), agl .first) := wrapMessage2Data
(mkMessage(agl .rest, mkOkConfirmBooking))
}
};,
GetInputRequestData-UserCmd-1#
: GetInputRequestData-UserCmd-1# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isGetInputRequestData(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(User-GetInput(`1'), a .to) := get(s(User-GetInputs(`1'), a .to) .ListOfData, s(User-GetInput-count(`1'), a .to) .nat) ;
s(User-GetInput-count(`1'), a .to) := inc(s(User-GetInput-count(`1'), a .to)) ;
if isNull-IFlowUtil(s(User-GetInput(`1'), a .to)) .value
then s(state(`init'), mkUser(a .to .id)) := wrapMessage2Data(mkMessage(agl, mkConfirm))
else s(Mailbox(GetFlightOffers-TravelPlannerCmd), mkTravelPlanner(a .to .id)) := wrapMessage2Data
(mkMessage
(agl,
mkGetFlightOffers
(s(User-GetInput(`1'), a .to)
.RequestData)))
}
};,
GetSingleSelection-UserCmd-2#
: GetSingleSelection-UserCmd-2# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isGetSingleSelection(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`flightOffers'), a .to) := wrapListOfFlightOffer2Data(ListOfData2ListOfFlightOffer(d .msg .content .selection)) ;
s(User-GetSingleSelection(`2'), a .to) := getSingleSelection
(d .msg .content .selection,
get
(s(User-GetSingleSelections(`2'), a .to) .ListOfData,
s(User-GetSingleSelection-count(`2'), a .to) .nat)
.nat) ;
s(User-GetSingleSelection-count(`2'), a .to) := inc(s(User-GetSingleSelection-count(`2'), a .to)) ;
if isNull-IFlowUtil(s(User-GetSingleSelection(`2'), a .to)) .value
then s(state(`pre8'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
else s(Mailbox(BookSelected-TravelPlannerCmd), mkTravelPlanner(a .to .id)) := wrapMessage2Data
(mkMessage
(agl,
mkBookSelected
(s(User-GetSingleSelection(`2'), a .to)
.FlightOffer)))
}
};,
ConfirmRelease-UserCmd-3#
: ConfirmRelease-UserCmd-3# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isConfirmRelease(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`ccd'), a .to) := wrapCreditCardDetails2Data(d .msg .content .what .CreditCardDetails) ;
s(locVar(`airline'), a .to) := wrapString2Data(d .msg .content .receiver) ;
s(User-ConfirmRelease(`3'), a .to) := get
(s(User-ConfirmReleases(`3'), a .to) .ListOfData,
s(User-ConfirmRelease-count(`3'), a .to) .nat) ;
s(User-ConfirmRelease-count(`3'), a .to) := inc(s(User-ConfirmRelease-count(`3'), a .to)) ;
if ¬ isNull-IFlowUtil(s(User-ConfirmRelease(`3'), a .to)) .value
then s(User-ConfirmedRelease-count(`3'), a .to) := inc(s(User-ConfirmedRelease-count(`3'), a .to)) ;
if isNull-IFlowUtil(s(User-ConfirmRelease(`3'), a .to)) .value
then s(state(`pre9'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
else s(Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd), mkCreditCardCenter(a .to .id)) := wrapMessage2Data
(mkMessage
(agl, mkGetDeclassifiedCCD))
}
};,
Confirm-UserCmd-4#
: Confirm-UserCmd-4# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isConfirm(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(User-Confirm(`4'), a .to) := get(s(User-Confirms(`4'), a .to) .ListOfData, s(User-Confirm-count(`4'), a .to) .nat) ;
s(User-Confirm-count(`4'), a .to) := inc(s(User-Confirm-count(`4'), a .to))
}
};,
RetFlightOffers-TravelPlannerCmd#
: RetFlightOffers-TravelPlannerCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isRetFlightOffers(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`flightOffers'), a .to) := wrapListOfFlightOffer2Data(d .msg .content .flightOffers) ;
s(state(`state1'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
BookSelected-TravelPlannerCmd#
: BookSelected-TravelPlannerCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isBookSelected(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(TravelPlanner-flightOffer, a .to) := wrapFlightOffer2Data(d .msg .content .flightOffer) ;
s(state(`state2'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
declassifyCCD4ASM-CreditCardCenterCmd#
: declassifyCCD4ASM-CreditCardCenterCmd# (a; s)
{
if s(state(`state3'), a .to) ≠ null
then let agl = s(state(`state3'), a .to) .msg .agentlist
in {
s(state(`state3'), a .to) := null ;
s(locVar(`ccd_decl'), a .to) := wrapCreditCardDetails2Data
(declassifyCCD-CreditCardCenter(s(CreditCardCenter-ccd, a .to) .CreditCardDetails)) ;
s(declassify-count(`declassifyCCD'), a .to) := inc(s(declassify-count(`declassifyCCD'), a .to)) ;
s(state(`state4'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
afterdeclassifyCCD4ASM-CreditCardCenterCmd#
: afterdeclassifyCCD4ASM-CreditCardCenterCmd# (a; s)
{
if s(state(`state4'), a .to) ≠ null
then let agl = s(state(`state4'), a .to) .msg .agentlist
in {
s(state(`state4'), a .to) := null ;
s(Mailbox(DeclassifiedCCD-TravelPlannerCmd), mkTravelPlanner(a .to .id)) := wrapMessage2Data
(mkMessage
(agl,
mkDeclassifiedCCD
(s(locVar(`ccd_decl'), a .to) .CreditCardDetails)))
}
};,
BookFlightOffer-AirlineCmd#
: BookFlightOffer-AirlineCmd# (a; s)
{
let d = s(Mailbox(a .cmd), a .to)
in if isMessage(d) ∧ isBookFlightOffer(d .msg .content)
then let agl = d .msg .agentlist
in {
s(Mailbox(a .cmd), a .to) := null ;
s(locVar(`id'), a .to) := wrapInteger2Data(d .msg .content .id) ;
s(locVar(`ccd_decl'), a .to) := wrapCreditCardDetails2Data(d .msg .content .ccd) ;
let d0 = processBooking-Airline(s(locVar(`id'), a .to) .Integer, s(locVar(`ccd_decl'), a .to) .CreditCardDetails) in skip ;
s(state(`state6'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
BookFlightOfferstate6-AirlineCmd#
: BookFlightOfferstate6-AirlineCmd# (a; s)
{
if s(state(`state6'), a .to) ≠ null
then let agl = s(state(`state6'), a .to) .msg .agentlist
in {
s(state(`state6'), a .to) := null ; s(state(`state7'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
Abort8-UserCmd#
: Abort8-UserCmd# (a; s)
{
if s(state(`pre8'), a .to) ≠ null
then let agl = s(state(`pre8'), a .to) .msg .agentlist
in {
s(state(`pre8'), a .to) := null ; s(state(`init'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};,
Abort9-UserCmd#
: Abort9-UserCmd# (a; s)
{
if s(state(`pre9'), a .to) ≠ null
then let agl = s(state(`pre9'), a .to) .msg .agentlist
in {
s(state(`pre9'), a .to) := null ; s(state(`init'), a .to) := wrapMessage2Data(mkMessage(agl, mkConfirm))
}
};
end asm specification