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
Hi Li, thank you for your questions. 2012/4/18 Jianwen Li <lijwen2748@gmail.com>:
1. Can I use your ltl parser source codes directly to implement my ideas?
That's code distributed under the GNU GPL, so as long as you are compatible with this licence you can use it for whatever you want.
2. Does SPOT integrate some ltl generators? Or, Are there any test suits available for me?
src/ltltest/genltl is a program that can generate LTL formulae from various parametered families. These families of formulae come from various papers (see the source code for references). src/ltltest/randltl is another program that can be used to generate random LTL formulae. lbtt/ is a tool that can be used to check (and benchmark) LTL translator. Spot uses it in the src/tgbatest/spotlbtt.test script to check all its LTL translator algorithms. In bench/ you should find various benchmarks related to LTL translation: - ltlclasses/ and ltlcounter/ build automata for formulas generated by genltl. - ltl2tgba/ use lbtt to compare spot with various other translator. There is a README in all these benchs/*/ directories.
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?
The ltl2tgba test program offer access to most of Spot's translations and reduction options. But it's not very user friendly (it was really meant to be used in the test suite).\ It work only with one formula at once. You can convert an LTL formula to a neverclaim with src/tgbatest/ltl2tgba -r4 -x -R3 -N 'X(a U b)' > out.never If you want to spend extra time to determinize and reduce obligation formula, try src/tgbatest/ltl2tgba -r4 -x -R3 -Rm -N 'X(a U b)' > out.never
I appreciate this function very much since I do want to compare my results with those from SPOT. ^^
I'd suggest to use LBTT for that. See how it is done in bench/ltl2tgba/
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 :)
Of course. In that case I'd suggest working off the "next" branch of the git repository (in which we are merging what will become Spot 0.9), and reading the file named HACKING about some of the conventions followed in Spot. Best regards, -- Alexandre Duret-Lutz
participants (2)
-
Alexandre Duret-Lutz -
Jianwen Li