¿Cómo puedo transformar, rm LTL en Automata en PROMELA? Sé que con el comando SPIN -f "ltl x" es posible transformar el LTL en un reclamo ininterrumpido, pero quiero los autómatas del LTL y no el de negación. Es correcto si niego el LTL antes para generar el reclamo nunca. ¿Alguien puede ayudarme?