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

Adjust ltl2tgba.py to call scc_filter() with the "full" option as

Browse source 
appropriate.

* wrap/python/spot.i (spot::scc_filter): Make it available.
* wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
Use the "full" option unless the show_degen_png or
show_never_claim are set.  Also reduce_scc the default.
This commit is contained in:
Alexandre Duret-Lutz 2010-04-12 16:39:28 +02:00
parent ef3c82e1b0
commit 60dbeb1128
3 changed files with 19 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2010-04-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Adjust ltl2tgba.py to call scc_filter() with the "full" option as
appropriate.
* wrap/python/spot.i (spot::scc_filter): Make it available.
* wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
Use the "full" option unless the show_degen_png or
show_never_claim are set. Also reduce_scc the default.
2010-04-08 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-04-08 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/ltlvisit/basicreduce.cc: Typo in comment. * src/ltlvisit/basicreduce.cc: Typo in comment.

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

@ -258,7 +258,7 @@ options_reduce = [
('reduce_langcont', 'language containment' + new, 0), ('reduce_langcont', 'language containment' + new, 0),
] ]
options_aut_reduce = [ options_aut_reduce = [
('reduce_scc', 'prune unaccepting SCCs' + new, 0), ('reduce_scc', 'prune unaccepting SCCs' + new, 1),
] ]
options_debug = [ options_debug = [
('show_parse', 'show traces during parsing', 0), ('show_parse', 'show traces during parsing', 0),
@ -564,7 +564,11 @@ elif trans_taa:
automaton = spot.ltl_to_taa(f, dict, refined_rules) automaton = spot.ltl_to_taa(f, dict, refined_rules)
if reduce_scc: if reduce_scc:
automaton = spot.reduc_tgba_sim(automaton, spot.Reduce_Scc) # Do not suppress all useless acceptance conditions if
# degeneralization is requested: keeping those that lead to
# accepting states usually help.
automaton = spot.scc_filter(automaton, not (show_degen_png or
show_never_claim))
print 'done.</p>' print 'done.</p>'
sys.stdout.flush() sys.stdout.flush()

3
wrap/python/spot.i
View file

@ -91,6 +91,7 @@
#include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/reductgba_sim.hh"
#include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/rundotdec.hh"
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
using namespace spot::ltl; using namespace spot::ltl;
@ -151,6 +152,7 @@ using namespace spot;
%feature("new") spot::reduc_tgba_sim; %feature("new") spot::reduc_tgba_sim;
%feature("new") spot::emptiness_check_instantiator::construct; %feature("new") spot::emptiness_check_instantiator::construct;
%feature("new") spot::emptiness_check_instantiator::instanciate; %feature("new") spot::emptiness_check_instantiator::instanciate;
%feature("new") spot::scc_filter;
// Help SWIG with namespace lookups. // Help SWIG with namespace lookups.
#define ltl spot::ltl #define ltl spot::ltl
@ -182,6 +184,7 @@ using namespace spot;
%include "tgbaalgos/reductgba_sim.hh" %include "tgbaalgos/reductgba_sim.hh"
%include "tgbaalgos/rundotdec.hh" %include "tgbaalgos/rundotdec.hh"
%include "tgbaalgos/save.hh" %include "tgbaalgos/save.hh"
%include "tgbaalgos/sccfilter.hh"
%include "tgbaalgos/stats.hh" %include "tgbaalgos/stats.hh"
#undef ltl #undef ltl