alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new

Browse source 
translation algorithm: Tauriainen/TAA.
This commit is contained in:
Damien Lefortier 2010-01-25 18:30:33 +01:00
parent d9b8fcddd6
commit 58d6b7912c
3 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2010-01-25 Damien Lefortier <dam@lrde.epita.fr>
* wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new
translation algorithm: Tauriainen/TAA.
2010-01-25 Damien Lefortier <dam@lrde.epita.fr> 2010-01-25 Damien Lefortier <dam@lrde.epita.fr>
* wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead * wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead

8
wrap/python/cgi/ltl2tgba.in
View file

@ -197,6 +197,7 @@ formula = form.getfirst('formula', '')
color_fm = "#DFC6F8" color_fm = "#DFC6F8"
color_lacim = "#F8C6DF" color_lacim = "#F8C6DF"
color_taa = "#D8C6FF"
options_common = [ options_common = [
('show_formula_png', 'draw the formula', 0), ('show_formula_png', 'draw the formula', 0),
@ -231,11 +232,16 @@ options_trans_lacim = [
('show_acceptance_png', ('show_acceptance_png',
'draw the acceptance relation', 0), 'draw the acceptance relation', 0),
] ]
options_trans_taa = [
('refined_rules',
'refined rules', 1)
]
default_translator = 'trans_fm'; default_translator = 'trans_fm';
translators = [ translators = [
('trans_fm', 'Couvreur/FM', color_fm), ('trans_fm', 'Couvreur/FM', color_fm),
('trans_lacim', 'Couvreur/LaCIM', color_lacim), ('trans_lacim', 'Couvreur/LaCIM', color_lacim),
('trans_taa', 'Tauriainen/TAA', color_taa),
] ]
options_accepting_run = [ options_accepting_run = [
@ -495,6 +501,8 @@ elif trans_fm:
automaton = spot.ltl_to_tgba_fm(f, dict, automaton = spot.ltl_to_tgba_fm(f, dict,
exprop, symb_merge, branching_postponement, exprop, symb_merge, branching_postponement,
fair_loop_approx) fair_loop_approx)
elif trans_taa:
automaton = spot.ltl_to_taa(f, dict, refined_rules)
print 'done.</p>' print 'done.</p>'
sys.stdout.flush() sys.stdout.flush()

5
wrap/python/spot.i
View file

@ -69,6 +69,7 @@
#include "tgba/succiter.hh" #include "tgba/succiter.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "tgba/statebdd.hh" #include "tgba/statebdd.hh"
#include "tgba/taatgba.hh"
#include "tgba/tgbabddcoredata.hh" #include "tgba/tgbabddcoredata.hh"
#include "tgba/succiterconcrete.hh" #include "tgba/succiterconcrete.hh"
#include "tgba/tgbabddconcrete.hh" #include "tgba/tgbabddconcrete.hh"
@ -78,6 +79,7 @@
#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/dottydec.hh" #include "tgbaalgos/dottydec.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/dupexp.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_lacim;
%feature("new") spot::ltl_to_tgba_fm; %feature("new") spot::ltl_to_tgba_fm;
%feature("new") spot::ltl_to_taa;
%feature("new") spot::tgba::get_init_state; %feature("new") spot::tgba::get_init_state;
%feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba::succ_iter;
%feature("new") spot::tgba_succ_iterator::current_state; %feature("new") spot::tgba_succ_iterator::current_state;
@ -156,6 +159,7 @@ using namespace spot;
%include "tgba/succiter.hh" %include "tgba/succiter.hh"
%include "tgba/tgba.hh" %include "tgba/tgba.hh"
%include "tgba/statebdd.hh" %include "tgba/statebdd.hh"
%include "tgba/taatgba.hh"
%include "tgba/tgbabddcoredata.hh" %include "tgba/tgbabddcoredata.hh"
%include "tgba/succiterconcrete.hh" %include "tgba/succiterconcrete.hh"
%include "tgba/tgbabddconcrete.hh" %include "tgba/tgbabddconcrete.hh"
@ -165,6 +169,7 @@ using namespace spot;
%include "tgbaalgos/ltl2tgba_lacim.hh" %include "tgbaalgos/ltl2tgba_lacim.hh"
%include "tgbaalgos/ltl2tgba_fm.hh" %include "tgbaalgos/ltl2tgba_fm.hh"
%include "tgbaalgos/ltl2taa.hh"
%include "tgbaalgos/dottydec.hh" %include "tgbaalgos/dottydec.hh"
%include "tgbaalgos/dotty.hh" %include "tgbaalgos/dotty.hh"
%include "tgbaalgos/dupexp.hh" %include "tgbaalgos/dupexp.hh"