Dear Sir (Madam):

    Recently I am following your spot tool and try to use it to practice some of my ideas on ltl-to-Buchi translation.  After reading the manuals I appreciate if you

can answer me these questions:
1. Can I use your ltl parser source codes directly to implement my ideas?

2. Does SPOT integrate some ltl generators? Or, Are there any test suits available for me? 

3. Does SPOT provide any interface which can generate the Buchi automata from a list of formulas

        and output them with any format (e.g prolmea or xml ) back to a file?

   I appreciate this function very much since I do want to compare my results with those from SPOT. ^^

4. If I have some new idea to implement a new translation, is it possible for me to integrate it to SPOT? (I ask this since I thought SPOT is open :) )

 

Thank you very much and hope your reply!

 

Best

Jianwen Li