diff --git a/ChangeLog b/ChangeLog index bbcfe80fa..25f12436d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2010-01-25 Damien Lefortier + + * wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new + translation algorithm: Tauriainen/TAA. + 2010-01-25 Damien Lefortier * wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 83d4050bc..1f073ca04 100755 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -197,6 +197,7 @@ formula = form.getfirst('formula', '') color_fm = "#DFC6F8" color_lacim = "#F8C6DF" +color_taa = "#D8C6FF" options_common = [ ('show_formula_png', 'draw the formula', 0), @@ -231,11 +232,16 @@ options_trans_lacim = [ ('show_acceptance_png', 'draw the acceptance relation', 0), ] +options_trans_taa = [ + ('refined_rules', + 'refined rules', 1) + ] default_translator = 'trans_fm'; translators = [ ('trans_fm', 'Couvreur/FM', color_fm), ('trans_lacim', 'Couvreur/LaCIM', color_lacim), + ('trans_taa', 'Tauriainen/TAA', color_taa), ] options_accepting_run = [ @@ -495,6 +501,8 @@ elif trans_fm: automaton = spot.ltl_to_tgba_fm(f, dict, exprop, symb_merge, branching_postponement, fair_loop_approx) +elif trans_taa: + automaton = spot.ltl_to_taa(f, dict, refined_rules) print 'done.

' sys.stdout.flush() diff --git a/wrap/python/spot.i b/wrap/python/spot.i index bc7d43c1f..979b3eaad 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -69,6 +69,7 @@ #include "tgba/succiter.hh" #include "tgba/tgba.hh" #include "tgba/statebdd.hh" +#include "tgba/taatgba.hh" #include "tgba/tgbabddcoredata.hh" #include "tgba/succiterconcrete.hh" #include "tgba/tgbabddconcrete.hh" @@ -78,6 +79,7 @@ #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/ltl2taa.hh" #include "tgbaalgos/dottydec.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/dupexp.hh" @@ -135,6 +137,7 @@ using namespace spot; %feature("new") spot::ltl_to_tgba_lacim; %feature("new") spot::ltl_to_tgba_fm; +%feature("new") spot::ltl_to_taa; %feature("new") spot::tgba::get_init_state; %feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba_succ_iterator::current_state; @@ -156,6 +159,7 @@ using namespace spot; %include "tgba/succiter.hh" %include "tgba/tgba.hh" %include "tgba/statebdd.hh" +%include "tgba/taatgba.hh" %include "tgba/tgbabddcoredata.hh" %include "tgba/succiterconcrete.hh" %include "tgba/tgbabddconcrete.hh" @@ -165,6 +169,7 @@ using namespace spot; %include "tgbaalgos/ltl2tgba_lacim.hh" %include "tgbaalgos/ltl2tgba_fm.hh" +%include "tgbaalgos/ltl2taa.hh" %include "tgbaalgos/dottydec.hh" %include "tgbaalgos/dotty.hh" %include "tgbaalgos/dupexp.hh"