bank2.cop

Copland Source

*rp, n: @ks [av us bmon]
  +<+ @us bmon us exts

Pretty Printed Source

*rp, n: @ks [av us bmon] +<+ @us bmon us exts

Abstract Syntax Tree

AST n0 av us bmon n1 @ks n1->n0 n2 bmon us exts n3 @us n3->n2 n4 +<+ n4->n1 n4->n3

Execution Semantics: bank2.gli

l(e2) = msp(ks, e1, av, us, bmon) & l(e5) = msp(us, e4, bmon, us, exts)
  & prec(e2, e5).

ms_evt(E) => E = e2 | E = e5.
G n2 msp(ks, e1, av, us, bmon) n5 msp(us, e4, bmon, us, exts) n2->n5

Problem Configuration

[ bound = 500, input_order ]

m4_include(`bank2.gli')m4_dnl

m4_include(`bank2_supps.gli')m4_dnl

m4_include(`thy.gli')m4_dnl

Models