Automatic Translation of Reactive Modules to SMV

Reactive Modules is a modeling language designed to combine synchronous and asynchronous composition in a hierarchic and convenient way. The Mocha tool supports simulation and model checking of models written in this language.

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.