NuSMV Version 2: BDD-based + SAT-based Symbolic ModelChecker.