in transition-pattern.mod . -- -- =========================== -- =========================== -- Specification of -- business process flow for -- saling and shipping -- =========================== -- =========================== mod* SALE-AND-SHIP { pr ( PATTERNS ) *[ SaleAndShip < State ]* -- ************** -- observations -- ************** -- observations are the same as ones defined in PATTERNS -- ************* -- transitions -- ************* -- ========================== -- regular events in client -- ========================== -- creating order with a carbon copy bop Create-cc-order : SaleAndShip SessionID DocumentID -> SaleAndShip -- sending order to sales bop Send-order : SaleAndShip DocumentID -> SaleAndShip -- creating receipt from invoice bop Create-receipt : SaleAndShip DocumentID DocumentID -> SaleAndShip -- sending receipt to sales bop Send-receipt : SaleAndShip DocumentID -> SaleAndShip -- -- ========================== -- control events in client -- ========================== -- checking ack with a carbon copy of order bop Check-ack : SaleAndShip DocumentID DocumentID -> SaleAndShip -- checking invoice with a carbon copy of order bop Check-invoice : SaleAndShip DocumentID DocumentID -> SaleAndShip -- -- ========================= -- regular events in sales -- ========================= -- creating ack from order bop Create-ack : SaleAndShip DocumentID DocumentID -> SaleAndShip -- sending ack to client bop Send-ack : SaleAndShip DocumentID -> SaleAndShip -- creating request from order bop Create-request : SaleAndShip DocumentID DocumentID -> SaleAndShip -- sending request to shipping bop Send-request : SaleAndShip DocumentID -> SaleAndShip -- -- ========================= -- control events in sales -- ========================= -- approving order bop Approve-order : SaleAndShip DocumentID -> SaleAndShip -- checking receipt with order -- which has an evidence apv(sales) bop Check-receipt : SaleAndShip DocumentID DocumentID -> SaleAndShip -- checking report with order -- which has an evidence apv(sales) bop Check-report : SaleAndShip DocumentID DocumentID -> SaleAndShip -- -- ============================ -- regular events in shipping -- ============================ -- creating invoice with a carbon copy from request bop Create-cc-invoice : SaleAndShip DocumentID DocumentID -> SaleAndShip -- sending invoice to client bop Send-invoice : SaleAndShip DocumentID -> SaleAndShip -- creating report from invoice bop Create-report : SaleAndShip DocumentID DocumentID -> SaleAndShip -- sending report to sales bop Send-report : SaleAndShip DocumentID -> SaleAndShip -- -- ================= -- irregular event -- ================= bop Forge-SaleAndShip : SaleAndShip DocumentID -> SaleAndShip bop ChangeSession-SaleAndShip : SaleAndShip DocumentID SessionID -> SaleAndShip -- -- -- variables var S : SaleAndShip var T : DocumentType var V : Division vars D D1 D2 D3 : DocumentID vars I I1 I2 : SessionID -- -- **************** -- initial states -- **************** op init : -> SaleAndShip op single : -> SessionID -- for single session eq (I1 = I2) = true . -- eq DocumentType(init, D) = noDocumentType . eq Place(init, D) = noDivision . eq Evidences(init, D) = emptyE . eq SessionID(init, D) = noSessionID . eq OriginalID(init, D) = noSessionID . eq Legal?(init, D) = true . eq DocumentIDList(init, I, T) = nillDID . -- eq UntrustedSet(init) = (sales shipping) . -- -- -- ****************** -- transition rules -- ****************** -- transition rules can be defined by -- using trasition rules in module PATTERN. -- ========================== -- regular events in client -- ========================== -- ----------------------- -- Create-cc-order(S, D) -- ----------------------- -- effective conditions op c-Create-cc-order : SaleAndShip SessionID DocumentID -> Bool -- the document whose type is order is not created -- in session I. eq c-Create-cc-order(S, I, D) = (S = init) . -- = c-Create-cc-1(S, I, client, D, order) and -- (DocumentIDList(S, I, order) = nillDID) . -- -- c-Create-cc-order(S, I, D) = true ceq Create-cc-order(S, I, D) = Create-cc-1(S, I, client, D, order) if c-Create-cc-order(S, I, D) . -- -- c-Create-cc-order(S, I, D) = false ceq Create-cc-order(S, I, D) = S if not(c-Create-cc-order(S, I, D)) . -- ------------------------------------------ -- -- ------------------ -- Send-order(S, D) -- ------------------ -- effective condition op c-Send-order : SaleAndShip DocumentID -> Bool -- there is no document except order in the cabinet. eq c-Send-order(S, D) = c-Send(S, client, D, sales) and (DocumentType(S, D) = order) . -- -- c-Send-order(S, D) = true ceq Send-order(S, D) = Send(S, client, D, sales) if c-Send-order(S, D) . -- -- c-Send-order(S, D) = false ceq Send-order(S, D) = S if not(c-Send-order(S, D)) . -- ------------------------------------------ -- -- --------------------------- -- Create-receipt(S, D1, D2) -- --------------------------- -- effective condition op c-Create-receipt : SaleAndShip DocumentID DocumentID -> Bool -- receipt is created from invoice. -- receipt is created after the check of invoice with -- a carbon copy of order. eq c-Create-receipt(S, D1, D2) = c-Create-2(S, client, D1, receipt, D2) and (DocumentIDList(S, SessionID(S, D2), receipt) = nillDID) and (DocumentType(S, D2) = invoice) and in?(ch(cc(order)), Evidences(S, D2)) . -- -- c-Create-receipt(S, D1, D2) = true ceq Create-receipt(S, D1, D2) = Create-2(S, client, D1, receipt, D2) if c-Create-receipt(S, D1, D2) . -- -- c-Create-receipt(S, D1, D2) = false ceq Create-receipt(S, D1, D2) = S if not(c-Create-receipt(S, D1, D2)) . -- ------------------------------------------ -- -- -------------------- -- Send-receipt(S, D) -- -------------------- -- effective condition op c-Send-receipt : SaleAndShip DocumentID -> Bool -- Document type of D is receipt. eq c-Send-receipt(S, D) = c-Send(S, client, D, sales) and (DocumentType(S, D) = receipt) . -- -- c-Send-receipt(S, D) = true ceq Send-receipt(S, D) = Send(S, client, D, sales) if c-Send-receipt(S, D) . -- -- c-Send-receipt(S, D) = false ceq Send-receipt(S, D) = S if not(c-Send-receipt(S, D)) . -- ------------------------------------------ -- -- ========================== -- control events in client -- ========================== -- ---------------------- -- Check-ack(S, D1, D2) -- ---------------------- -- effective condition op c-Check-ack : SaleAndShip DocumentID DocumentID -> Bool eq c-Check-ack(S, D1, D2) = c-Check-1(S, client, D1, D2) and (DocumentType(S, D1) = ack) and (DocumentType(S, D2) = cc(order)) . -- -- c-Check-ack(S, D1, D2) = true ceq Check-ack(S, D1, D2) = Check-1(S, client, D1, D2) if c-Check-ack(S, D1, D2) . -- -- c-Check-ack(S, D1, D2) = false ceq Check-ack(S, D1, D2) = S if not(c-Check-ack(S, D1, D2)) . -- ------------------------------------------ -- -- -------------------------- -- Check-invoice(S, D1, D2) -- -------------------------- -- effective condition op c-Check-invoice : SaleAndShip DocumentID DocumentID -> Bool -- checking invoice is done after checking ack -- with a carbon copy of order. eq c-Check-invoice(S, D1, D2) = c-Check-1(S, client, D1, D2) and (DocumentType(S, D1) = invoice) and (DocumentType(S, D2) = cc(order)) . -- -- c-Check-invoice(S, D1, D2) = true ceq Check-invoice(S, D1, D2) = Check-1(S, client, D1, D2) if c-Check-invoice(S, D1, D2) . -- -- c-Check-invoice(S, D1, D2) = false ceq Check-invoice(S, D1, D2) = S if not(c-Check-invoice(S, D1, D2)) . -- ------------------------------------------ -- -- ========================= -- regular events in sales -- ========================= -- ----------------------- -- Create-ack(S, D1, D2) -- ----------------------- -- effective condition op c-Create-ack : SaleAndShip DocumentID DocumentID -> Bool eq c-Create-ack(S, D1, D2) = c-Create-2(S, sales, D1, ack, D2) and (DocumentType(S, D2) = order) and (DocumentIDList(S, SessionID(S, D2), ack) = nillDID) and (Evidences(S, D2) = emptyE) . -- -- c-Create-ack(S, D1, D2) = true ceq Create-ack(S, D1, D2) = Create-2(S, sales, D1, ack, D2) if c-Create-ack(S, D1, D2) . -- -- c-Create-ack(S, D1, D2) = false ceq Create-ack(S, D1, D2) = S if not(c-Create-ack(S, D1, D2)) . -- ------------------------------------------ -- -- ---------------- -- Send-ack(S, D) -- ---------------- -- effective condition op c-Send-ack : SaleAndShip DocumentID -> Bool eq c-Send-ack(S, D) = c-Send(S, sales, D, client) and (DocumentType(S, D) = ack) . -- -- c-Send-ack(S, D) = true ceq Send-ack(S, D) = Send(S, sales, D, client) if c-Send-ack(S, D) . -- -- c-Send-ack(S, D) = false ceq Send-ack(S, D) = S if not(c-Send-ack(S, D)) . -- ------------------------------------------ -- -- --------------------------- -- Create-request(S, D1, D2) -- --------------------------- -- effective condition op c-Create-request : SaleAndShip DocumentID DocumentID -> Bool -- creating request is done after checking ack in client eq c-Create-request(S, D1, D2) = c-Create-2(S, sales, D1, request, D2) and (DocumentType(S, D2) = order) and (DocumentIDList(S, SessionID(S, D2), request) = nillDID) and in?(ch(cc(order)), Evidences(S, top(DocumentIDList(S, SessionID(S, D2), ack)))) . -- -- c-Create-request(S, D1, D2) = true ceq Create-request(S, D1, D2) = Create-2(S, sales, D1, request, D2) if c-Create-request(S, D1, D2) . -- -- c-Create-request(S, D1, D2) = false ceq Create-request(S, D1, D2) = S if not(c-Create-request(S, D1, D2)) . -- ------------------------------------------ -- -- -------------------- -- Send-request(S, D) -- -------------------- -- effective condition op c-Send-request : SaleAndShip DocumentID -> Bool eq c-Send-request(S, D) = c-Send(S, sales, D, shipping) and (DocumentType(S, D) = request) . -- -- c-Send-request(S, D) = true ceq Send-request(S, D) = Send(S, sales, D, shipping) if c-Send-request(S, D) . -- -- c-Send-request(S, D) = false ceq Send-request(S, D) = S if not(c-Send-request(S, D)) . -- ------------------------------------------ -- -- ========================= -- control events in sales -- ========================= -- --------------------- -- Approve-order(S, D) -- --------------------- -- effective condition op c-Approve-order : SaleAndShip DocumentID -> Bool -- approving order is done after sending request. eq c-Approve-order(S, D) = c-Approve-1(S, sales, D) and (DocumentType(S, D) = order) and (Evidences(S, D) = emptyE) and (Place(S, top(DocumentIDList(S, SessionID(S, D), ack))) = sales) . -- -- c-Approve-order(S, D) = true ceq Approve-order(S, D) = Approve-1(S, sales, D) if c-Approve-order(S, D) . -- -- c-Approve-order(S, D) = false ceq Approve-order(S, D) = S if not(c-Approve-order(S, D)) . -- ------------------------------------------ -- -- -------------------------- -- Check-receipt(S, D1, D2) -- -------------------------- -- effective condition op c-Check-receipt : SaleAndShip DocumentID DocumentID -> Bool eq c-Check-receipt(S, D1, D2) = c-Check-3(S, sales, D1, D2, apv(sales)) and (DocumentType(S, D1) = receipt) and (DocumentType(S, D2) = order) . -- -- c-Check-receipt(S, D1, D2) = true ceq Check-receipt(S, D1, D2) = Check-3(S, sales, D1, D2, apv(sales)) if c-Check-receipt(S, D1, D2) . -- -- c-Check-receipt(S, D1, D2) = false ceq Check-receipt(S, D1, D2) = S if not(c-Check-receipt(S, D1, D2)) . -- ------------------------------------------ -- -- ------------------------- -- Check-report(S, D1, D2) -- ------------------------- -- effective condition op c-Check-report : SaleAndShip DocumentID DocumentID -> Bool -- checking report is done after checking receipt. eq c-Check-report(S, D1, D2) = c-Check-3(S, sales, D1, D2, apv(sales)) and (DocumentType(S, D1) = report) and (DocumentType(S, D2) = order) and in?(ch(order), Evidences(S, top(DocumentIDList(S, SessionID(S, D1), receipt)))) . -- -- c-Check-report(S, D1, D2) = true ceq Check-report(S, D1, D2) = Check-3(S, sales, D1, D2, apv(sales)) if c-Check-report(S, D1, D2) . -- -- c-Check-report(S, D1, D2) = false ceq Check-report(S, D1, D2) = S if not(c-Check-report(S, D1, D2)) . -- ------------------------------------------ -- -- ============================ -- regular events in shipping -- ============================ -- ---------------------- -- Create-cc-invoice(S, D1, D2) -- ---------------------- -- effective conditions op c-Create-cc-invoice : SaleAndShip DocumentID DocumentID -> Bool eq c-Create-cc-invoice(S, D1, D2) = c-Create-cc-2(S, shipping, D1, invoice, D2) and (DocumentType(S, D2) = request) and (DocumentIDList(S, SessionID(S, D2), invoice) = nillDID) . -- -- c-Create-cc-invoice(S, D1, D2) = true ceq Create-cc-invoice(S, D1, D2) = Create-cc-2(S, shipping, D1, invoice, D2) if c-Create-cc-invoice(S, D1, D2) . -- -- c-Create-cc-invoice(S, D1, D2) = false ceq Create-cc-invoice(S, D1, D2) = S if not(c-Create-cc-invoice(S, D1, D2)) . -- ------------------------------------------ -- -- -------------------- -- Send-invoice(S, D) -- -------------------- -- effective conditions op c-Send-invoice : SaleAndShip DocumentID -> Bool eq c-Send-invoice(S, D) = c-Send(S, shipping, D, client) and (DocumentType(S, D) = invoice) . -- -- c-Send-invoice(S, D) = true ceq Send-invoice(S, D) = Send(S, shipping, D, client) if c-Send-invoice(S, D) . -- -- c-Send-invoice(S, D) = false ceq Send-invoice(S, D) = S if not(c-Send-invoice(S, D)) . -- ------------------------------------------ -- -- -------------------------- -- Create-report(S, D1, D2) -- -------------------------- -- effective conditions op c-Create-report : SaleAndShip DocumentID DocumentID -> Bool -- creating report is done -- after sending invoice to client. eq c-Create-report(S, D1, D2) = c-Create-2(S, shipping, D1, report, D2) and (DocumentType(S, D2) = cc(invoice)) and (DocumentIDList(S, SessionID(S, D2), report) = nillDID) and (Place(S, top(DocumentIDList(S, SessionID(S, D2), invoice))) = client) . -- -- c-Create-report(S, D1, D2) = true ceq Create-report(S, D1, D2) = Create-2(S, shipping, D1, report, D2) if c-Create-report(S, D1, D2) . -- -- c-Create-report(S, D1, D2) = false ceq Create-report(S, D1, D2) = S if not(c-Create-report(S, D1, D2)) . -- ------------------------------------------ -- -- ------------------- -- Send-report(S, D) -- ------------------- -- effective conditions op c-Send-report : SaleAndShip DocumentID -> Bool -- creating report is done -- after sending invoice to client. eq c-Send-report(S, D) = c-Send(S, shipping, D, sales) and (DocumentType(S, D) = report) . -- -- c-Send-report(S, D) = true ceq Send-report(S, D) = Send(S, shipping, D, sales) if c-Send-report(S, D) . -- -- c-Send-report(S, D) = false ceq Send-report(S, D) = S if not(c-Send-report(S, D)) . -- ------------------------------------------ -- -- ======================================= -- irregular event in sales and shipping -- ======================================= -- ---------------------------- -- Forge-SaleAndShip(S, D) -- ---------------------------- -- effective condition op c-Forge-SaleAndShip : SaleAndShip DocumentID -> Bool eq c-Forge-SaleAndShip(S, D) = c-Forge(S, D) . -- -- c-Forge-SaleAndShip(S, D) = true ceq Forge-SaleAndShip(S, D) = Forge(S, D) if c-Forge-SaleAndShip(S, D) . -- -- c-Forge-SaleAndShip(S, D) = false ceq Forge-SaleAndShip(S, D) = S if not(c-Forge-SaleAndShip(S, D)) . -- ------------------------------------------ -- -- --------------------------------- -- ChangeSession-SaleAndShip(S, D) -- --------------------------------- -- effective condition op c-ChangeSession-SaleAndShip : SaleAndShip DocumentID SessionID -> Bool eq c-ChangeSession-SaleAndShip(S, D, I) = c-ChangeSession(S, D, I) . -- -- c-ChangeSession-SaleAndShip(S, D, I) = true ceq ChangeSession-SaleAndShip(S, D, I) = ChangeSession(S, D, I) if c-ChangeSession-SaleAndShip(S, D, I) . -- -- c-ChangeSession-SaleAndShip(S, D, I) = false ceq ChangeSession-SaleAndShip(S, D, I) = S if not(c-ChangeSession-SaleAndShip(S, D, I)) . -- ------------------------------------------ -- } "[ -- test open SALE-AND-SHIP . op s : -> SaleAndShip . red Cabinet(Create-cc-order(init-SaleAndShip)) . red UntrustedSet(Create-cc-order(init-SaleAndShip)) . close ]" eof