Standard priorities val P_HIGH = 100; val P_HIGH = 100; val P_NORMAL = 1000; val P_NORMAL = 1000; val P_LOW = 10000; val P_LOW = 10000; Standard declarations UNIT colset UNIT = unit; INT BOOL STRING AD2CPN colset declarations Name NameVal cont STRING colset NameVal = record cont: STRING; Order OrderID colset OrderID = int; OrderState orderer NameVal archived BOOL colset OrderState = record orderer: NameVal * archived: BOOL; Client ClientID colset ClientID = int; ClientControl Client0 colset ClientControl = with Client0; ClientState usingPaypal BOOL name NameVal control ClientControl colset ClientState = record usingPaypal: BOOL * name: NameVal * control: ClientControl; ECommerce ECommerceID colset ECommerceID = int; Names NameVal colset Names = list NameVal; ECommerceControl ECommerce0 colset ECommerceControl = with ECommerce0; ECommerceState cList Names control ECommerceControl colset ECommerceState = record cList: Names * control: ECommerceControl; Warehouse WarehouseID colset WarehouseID = int; WarehouseControl Warehouse0 colset WarehouseControl = with Warehouse0; WarehouseState control WarehouseControl colset WarehouseState = record control: WarehouseControl; Carrier CarrierID colset CarrierID = int; CarrierControl Carrier0 colset CarrierControl = with Carrier0; CarrierState control CarrierControl colset CarrierState = record control: CarrierControl; CreditCard CreditCardID colset CreditCardID = int; CreditCardControl CreditCard0 colset CreditCardControl = with CreditCard0; CreditCardState control CreditCardControl colset CreditCardState = record control: CreditCardControl; Paypal PaypalID colset PaypalID = int; PaypalControl Paypal0 colset PaypalControl = with Paypal0; PaypalState control PaypalControl colset PaypalState = record control: PaypalControl; Package PackageID colset PackageID = int; PackageControl Package0 colset PackageControl = with Package0; PackageState control PackageControl colset PackageState = record control: PackageControl; Clients CidCst ClientID ClientState colset CidCst = product ClientID * ClientState; Clients CidCst colset Clients = list CidCst; Ecommerces ProdECidECst ECommerceID ECommerceState colset ProdECidECst = product ECommerceID * ECommerceState; ECommerces ProdECidECst colset ECommerces = list ProdECidECst; Packages PackageIdSt PackageID PackageState colset PackageIdSt = product PackageID * PackageState; Packages PackageIdSt colset Packages = list PackageIdSt; Paypals prodPidPst PaypalID PaypalState colset prodPidPst = product PaypalID * PaypalState; Paypals prodPidPst colset Paypals = list prodPidPst; Warehouses prodWidWst WarehouseID WarehouseState colset prodWidWst = product WarehouseID * WarehouseState; Warehouses prodWidWst colset Warehouses = list prodWidWst; Carriers CarrierIdSt CarrierID CarrierState colset CarrierIdSt = product CarrierID * CarrierState; Carriers CarrierIdSt colset Carriers = list CarrierIdSt; CreditCards CreditCardIdSt CreditCardID CreditCardState colset CreditCardIdSt = product CreditCardID * CreditCardState; CreditCards CreditCardIdSt colset CreditCards = list CreditCardIdSt; Orders OrdersIdSt OrderID OrderState colset OrdersIdSt = product OrderID * OrderState; Orders OrdersIdSt colset Orders = list OrdersIdSt; State State set CLIENT ClientID EC ECommerceID WH WarehouseID CARRIER CarrierID CC CreditCardID PP PaypalID ORDER OrderID PACK PackageID ANS BOOL RES BOOL clients Clients eCommerces ECommerces warehouses Warehouses carriers Carriers creditCards CreditCards paypals Paypals orders Orders packages Packages colset State = record CLIENT: ClientID * EC: ECommerceID * WH: WarehouseID * CARRIER: CarrierID * CC: CreditCardID * PP: PaypalID * ORDER: OrderID * PACK: PackageID * ANS: BOOL * RES: BOOL * clients: Clients * eCommerces: ECommerces * warehouses: Warehouses * carriers: Carriers * creditCards: CreditCards * paypals: Paypals * orders: Orders * packages: Packages declare set; File inclusions "AD2CPN.sml" use "AD2CPN.sml"; Global variables test 0 globref test = 0; cs initState globref cs = initState; Local variables BOOL result var result : BOOL; Just for testing R i INT s STRING colset R = record i:INT * s:STRING; fun update2 s = R.set_s s "def"; fun update2 s = R.set_s s "def"; fun updateS st = State.set_EC st 3; fun updateS st = State.set_EC st 3; p1 UNIT 1`() p2 UNIT UNIT dec1 BOOL UNIT UNIT UNIT dec2 BOOL final1 UNIT UNIT UNIT UNIT UNIT UNIT BOOL UNIT UNIT UNIT UNIT UNIT UNIT UNIT UNIT UNIT final UNIT ORDER:=CLIENT.sendOrder(EC) input (); output (); action let val (s', oi) = sendOrder(!cs, #CLIENT(!cs), #EC(!cs)) in cs := State.set_ORDER s' oi end; init input() output() action cs := InitializeState (); RES = EC.checkRegistered(ORDER.orderer) input (); output (); action let val (s', b) = checkRegistered( !cs, #EC(!cs), get_orderer (!cs) (#ORDER(!cs)) ) in cs := State.set_RES s' b end; RES = true [result = true] RES = false [result = false] EC.proposeRegistration(CLIENT) input (); output (); action cs := proposeRegistration((!cs), #EC(!cs), #CLIENT(!cs)); ANS := CLIENT.answer() input (); output (); action let val (s', b) = answer(!cs, #CLIENT(!cs)) in cs := State.set_ANS s' b end; ANS=false [result = false] ANS=true [result = true] EC.register(CLIENT.name()) input (); output (); action cs := register (!cs , #EC(!cs), get_name (!cs) (#CLIENT(!cs))); merge merge merge fork PACK := WH.prepare(ORDER) input (); output (); action let val (s', pi) = prepare(!cs, #WH(!cs), #ORDER(!cs)) in cs := State.set_PACK s' pi end; CLIENT.usingPaypal() [result] not CLIENT.usingPaypal() [not result] CC.pay(ORDER) input (); output (); action cs := payByCC(!cs, #CC(!cs), #ORDER(!cs)); PP.pay(ORDER) input (); output (); action cs := payByPP(!cs , #PP(!cs), #ORDER(!cs)); merge merge join CARRIER.deliver(PACK) input (); output (); action cs := deliver(!cs, #CARRIER(!cs), #PACK(!cs)); CARRIER.informDelivered(PACK, EC) input (); output (); action cs := confirmDelivered(!cs, #CARRIER(!cs), #PACK(!cs), #EC(!cs)); EC.archive(ORDER) input (); output (); action cs := archive(!cs, #ORDER(!cs)); () () () () () #RES(!cs) result result () () () () () #ANS(!cs) result result () () () () () () () () () () () usingPaypal(!cs, #CLIENT(!cs)) () () result result () () () () () () () () () () () () () () () () () () () ()