bank1.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

Execution Semantics: bank1.gli

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

ms_evt(E) => E = e2 | E = e5.
    

Problem Configuration

[ bound = 500, input_order ]

m4_include(`bank1.gli')m4_dnl

m4_include(`bank1_supps.gli')m4_dnl

m4_include(`thy.gli')m4_dnl

    

Models

Model 1