se cambio el condicional por dos senales continuas para evitar la explosion de estados en el model checker