18 Apr
2012
18 Apr
'12
7:46 a.m.
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
18 Apr
18 Apr
10:44 a.m.
Hi Li, thank you for your questions.
2012/4/18 Jianwen Li <lijwen2748(a)gmail.com>om>:
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
4711
days inactive
4711
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Jianwen Li