Como transformar LTL em automato em Promela - SPIN?
Como posso transformar, LTL rm em Automata no PROMELA? Eu sei que com o comando SPIN -f "ltl x" é possível transformar o LTL em uma reivindicação nunca, mas quero os autômatos do LTL e não o da negação. Está correto Se eu negar o LTL antes para gerar a reivindicação nunca. Alguém pode me ajudar?