rename atomic propositions before calling ltl3ba

ltl3ba, like ltl2ba and spin, require atomic propositions to start with a lowercase letter. As a consequence, the ltl2tgba.html page fails to translate the formula F(A) with ltl3ba.

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 ltl3ba, ltl2ba, or spin, and allow these tools to take many formulas as input, and output the result in all the format we supports.