rename atomic propositions before calling ltl3ba
spin, require atomic propositions to start with a lowercase letter. As a consequence, the
ltl2tgba.html page fails to translate the formula
We could however relabel all the atomic propositions before calling
ltl3ba and then map the labels of the resulting automaton back to their original name before we display the automaton.
Rather than doing this in the CGI script, maybe this service could be provided by a command-line tool that can wrap
spin, and allow these tools to take many formulas as input, and output the result in all the format we supports.