bank17.cop

Copland Source

*rp, n:
  @us @ks [@hv [kim ks ker +~+ avm ks av] +<+ av us bmon]
      +<+ ((bmon us bser +~+ bmon us extmgr) +<+ extmgr us exts)

Pretty Printed Source

*rp, n:
  @us @ks [@hv [kim ks ker +~+ avm ks av] +<+ av us bmon]
      +<+ ((bmon us bser +~+ bmon us extmgr)
           +<+ extmgr us exts)

Abstract Syntax Tree

AST n0 kim ks ker n1 avm ks av n2 +~+ n2->n0 n2->n1 n3 @hv n3->n2 n4 av us bmon n5 +<+ n5->n3 n5->n4 n6 @ks n6->n5 n7 bmon us bser n8 bmon us extmgr n9 +~+ n9->n7 n9->n8 n10 extmgr us exts n11 +<+ n11->n9 n11->n10 n12 +<+ n12->n6 n12->n11 n13 @us n13->n12

Execution Semantics: bank17.gli

l(e6) = msp(hv, e5, kim, ks, ker) & l(e7) = msp(hv, e5, avm, ks, av)
  & l(e10) = msp(ks, e3, av, us, bmon)
  & l(e15) = msp(us, e14, bmon, us, bser)
  & l(e16) = msp(us, e14, bmon, us, extmgr)
  & l(e18) = msp(us, e13, extmgr, us, exts) & prec(e16, e18) & prec(e15, e18)
  & prec(e10, e15) & prec(e10, e18) & prec(e10, e16) & prec(e7, e10)
  & prec(e7, e18) & prec(e7, e16) & prec(e7, e15) & prec(e6, e10)
  & prec(e6, e18) & prec(e6, e16) & prec(e6, e15).

ms_evt(E) => E = e6 | E = e7 | E = e10 | E = e15 | E = e16 | E = e18.
G n10 msp(ks, e3, av, us, bmon) n16 msp(us, e14, bmon, us, extmgr) n10->n16 n15 msp(us, e14, bmon, us, bser) n10->n15 n18 msp(us, e13, extmgr, us, exts) n16->n18 n15->n18 n7 msp(hv, e5, avm, ks, av) n7->n10 n6 msp(hv, e5, kim, ks, ker) n6->n10

Problem Configuration

[ bound = 500, limit = 500000, input_order ]

m4_include(`bank17.gli')m4_dnl

m4_include(`bank17_supps.gli')m4_dnl

m4_include(`thy.gli')m4_dnl

Models