pool PaymentOrg {PaymentOrg,PStart,SendInvoice,PEnd}
pool Customer {Customer,ReceiveInvoice,ReceiveProduct,CAndJ,CStart,Order,CAndS,CEnd}
pool Manufacturer {Manufacturer,SendProduct,MStart,MEnd}
pool Reseller {Reseller,RAndJ,RAndS,REnd,PlaceInvoiceRequest,RStart,PlaceProductRequest}

agent PStart(p1,p) = p(info,c_a).t.'p1<c_a>.0
agent SendInvoice(p1,p2) = (^invoice)p1(c_a).t.'c_a<invoice>.'p2.0
agent PEnd(p2) = p2.t.0
exec agent PaymentOrg(payChan) = (^p1,p2)(PStart(p1,payChan) | SendInvoice(p1,p2) | PEnd(p2))

agent MStart(m1,m) = m(i,c_a).t.'m1<c_a>.0
agent SendProduct(m1,m2) = (^product)m1(c_a).t.'c_a<product>.'m2.0
agent MEnd(m2) = m2.t.0
exec agent Manufacturer(manChan) = (^m1,m2)(SendProduct(m1,m2) | MEnd(m2) | MStart(m1,manChan))

agent ReceiveInvoice(c4,c5) = c4(invAddr).invAddr(invoice).t.'c5.0 
agent ReceiveProduct(c3,c6) = c3(itemAddr).itemAddr(product).t.'c6.0
agent CAndJ(c6,c5,c7) = c6.c5.t.'c7.0 
agent CStart(c1) = t.'c1.0
agent Order(c1,c2,order) = (^item,itemAddr,invAddr)c1.t.'order<item,itemAddr,invAddr>.'c2<itemAddr,invAddr>.0
agent CAndS(c2,c4,c3) = c2(itemAddr,invAddr).t.('c4<invAddr>.0 | 'c3<itemAddr>.0 )
agent CEnd(c7) = c7.t.0
exec agent Customer(order) = (^c1,c2,c3,c4,c5,c6,c7)(ReceiveInvoice(c4,c5) | ReceiveProduct(c3,c6) | CAndJ(c6,c5,c7) | CStart(c1) | Order(c1,c2,order) | CAndS(c2,c4,c3) | CEnd(c7))

agent RAndJ(r5,r4,r6) = r5.r4.t.'r6.0
agent RAndS(r1,r3,r2) = r1(it,it_a,in_a).t.('r3<it,it_a>.0 | 'r2<it,in_a>.0 )
agent REnd(r6) = r6.t.0
agent PlaceInvoiceRequest(r2,r4,p) = r2(it,in_a).t.'p<it,in_a>.'r4.0
agent RStart(r1,o) = o(it,it_a,in_a).t.'r1<it,it_a,in_a>.0
agent PlaceProductRequest(r3,r5,m) = r3(it,it_a).t.'m<it,it_a>.'r5.0
exec agent Reseller(payChan,order,manChan) = (^r6,r1,r2,r3,r4,r5)(RAndJ(r5,r4,r6) | RAndS(r1,r3,r2) | REnd(r6) | PlaceInvoiceRequest(r2,r4,payChan) | RStart(r1,order) | PlaceProductRequest(r3,r5,manChan))
