SMV is one of the leading model checking tools existing today. It supports symbolic model checking using BDDs and bounded model checking using a reduction to satisfiability solving. The input language of SMV is (surprisingly enough) smv.
In order to be able to use both the strong BDD engine in SMV and the bounded model checking capabilities, we would like to be able to automatically translate reactive modules code into SMV. We would like to extend mocha so that one of its possible outputs would be an smv file.