<?xml version='1.0' encoding='utf-8'?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>chan sellerchannel, customerchannel, carrierchannel;clock Clock1;int purchaseOrder, purchOrderAccp, NoStockAck;</declaration><template><name>Customer</name><declaration>int purchaseOrdercreatePOCustomer=1, purchOrderAccpcreatePOCustomer, NoStockAckcreatePOCustomer, purchaseOrderDeliverProductPOCustomer;</declaration><location id="id0" x="-88" y="80"><name x="-312" y="56">idhandlePurchaseOrderCustomer</name></location><location id="id1" x="528" y="80"><name x="544" y="56">identDeliverProductOrderCustomer</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="synchronisation" x="168" y="-104">sellerchannel!</label><label kind="assignment" x="56" y="-88">purchaseOrder=purchaseOrdercreatePOCustomer</label><nail x="-40" y="-56"/><nail x="472" y="-56"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="168" y="-32">sellerchannel?</label><label kind="assignment" x="48" y="-16">purchOrderAccpcreatePOCustomer=purchOrderAccp</label><nail x="480" y="16"/><nail x="-40" y="16"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="176" y="128">sellerchannel?</label><label kind="assignment" x="80" y="144">NoStockAckcreatePOCustomer=NoStockAck</label><nail x="464" y="120"/><nail x="-40" y="120"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="guard" x="192" y="240">Clock1&lt;24</label><label kind="synchronisation" x="168" y="208">customerchannel?</label><label kind="assignment" x="40" y="224">purchaseOrderDeliverProductPOCustomer=purchaseOrder</label><nail x="448" y="200"/><nail x="-32" y="200"/></transition></template><template><name>InternetSeller</name><declaration>int purchaseOrdercreatePOInternetSeller, purchOrderAccpcreatePOInternetSeller=1, NoStockAckcreatePOInternetSeller=1, purchaseOrderPickUpProductPOInternetSeller=1;</declaration><location id="id2" x="-32" y="80"><name x="-296" y="56">identhandlePurchaseOrderInternetSeller</name></location><location id="id3" x="504" y="80"><name x="520" y="56">idPickUpPurchaseOrderInternetSeller</name></location><init ref="id2"/><transition><source ref="id2"/><target ref="id3"/><label kind="synchronisation" x="200" y="-80">sellerchannel?</label><label kind="assignment" x="96" y="-64">purchaseOrdercreatePOInternetSeller=purchaseOrder</label><nail x="8" y="-40"/><nail x="456" y="-40"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="192" y="-24">sellerchannel!</label><label kind="assignment" x="80" y="-8">purchOrderAccp=purchOrderAccpcreatePOInternetSeller</label><nail x="456" y="16"/><nail x="16" y="16"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="200" y="128">sellerchannel!</label><label kind="assignment" x="88" y="144">NoStockAck=NoStockAckcreatePOInternetSeller</label><nail x="456" y="128"/><nail x="16" y="128"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="guard" x="200" y="232">Clock1&lt;02</label><label kind="synchronisation" x="192" y="200">carrierchannel!</label><label kind="assignment" x="48" y="216">purchaseOrder=purchaseOrderPickUpProductPOInternetSeller</label><nail x="464" y="192"/><nail x="16" y="192"/></transition></template><template><name>Carrier</name><declaration>int purchaseOrderPickUpProductPOCarrier, purchaseOrderDeliverProductPOCarrier=1;</declaration><location id="id4" x="-88" y="80"><name x="-320" y="56">identPickUpPurchaseOrderCarrier</name></location><location id="id5" x="552" y="80"><name x="568" y="56">idDeliverProductOrderCarrier</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="176" y="-16">Clock1&lt;02</label><label kind="synchronisation" x="168" y="-48">carrierchannel?</label><label kind="assignment" x="56" y="-32">purchaseOrderPickUpProductPOCarrier=purchaseOrder</label><nail x="-48" y="16"/><nail x="528" y="16"/></transition><transition><source ref="id5"/><target ref="id4"/><label kind="guard" x="176" y="184">Clock1&lt;24</label><label kind="synchronisation" x="160" y="152">customerchannel!</label><label kind="assignment" x="56" y="168">purchaseOrder=purchaseOrderDeliverProductPOCarrier</label><nail x="504" y="144"/><nail x="-48" y="144"/></transition></template><system>
system Customer, InternetSeller, Carrier;</system></nta>