Rebeca to SMV translator, is a tool for automatic translation of Rebeca models into SMV codesl, so that the model can be verified with NuSMV model checker. The tool has been developed using Java language, so it is portable and can be run on any platform that has a Java Runtime Environment. The current version of this tool supports the following features in Rebeca model: