This is version of BML is available for the sole purpose of its evaluation and testing.

It is the tool that was used for the paper "Backward Coverability with Pruning for Lossy Channel Systems" by Thomas Geffroy, Jérôme Leroux and Grégoire Sutre, published at SPIN 2017.

to compile: make main.native

usage:
./main.native file options
examples
./main.native paper_examples/simple_server.scm
./main.native paper_examples/pop3.scm -state-inequation
./main.native paper_examples/BAwCC.scm -mof
./main.native paper_examples/BAwCC_enh.scm -csre

to launch the same benchmarks as the paper:
./bench.sh ./main.native paper_examples invariant
with invariant equal to -mof, -csre or -state-inequation
