From 241ba112d68245e8e04682b8e25464d3bddd6ea3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 26 Dec 2010 19:30:36 +0100 Subject: [PATCH] Make minimization of obligation properties and deterministic monitor available in the CGI script. * wrap/python/spot.i: Declare the minimize() interface. * wrap/python/cgi-bin/ltl2tgba.in: Add reduce_dmonitor and reduce_wdba options. --- ChangeLog | 9 ++++++++ wrap/python/cgi-bin/ltl2tgba.in | 8 ++++++- wrap/python/spot.i | 39 ++++++++++++++++++--------------- 3 files changed, 37 insertions(+), 19 deletions(-) diff --git a/ChangeLog b/ChangeLog index ffefb5ebb..3bffad152 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-12-26 Alexandre Duret-Lutz + + Make minimization of obligation properties and deterministic + monitor available in the CGI script. + + * wrap/python/spot.i: Declare the minimize() interface. + * wrap/python/cgi-bin/ltl2tgba.in: Add reduce_dmonitor and + reduce_wdba options. + 2010-12-14 Alexandre Duret-Lutz Add a WDBA benchmark. diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in index b02781f64..badae049b 100755 --- a/wrap/python/cgi-bin/ltl2tgba.in +++ b/wrap/python/cgi-bin/ltl2tgba.in @@ -260,6 +260,8 @@ options_reduce = [ ] options_aut_reduce = [ ('reduce_scc', 'prune unaccepting SCCs', 1), + ('reduce_wdba', 'minimize obligation properties' + new, 0), + ('reduce_dmonitor', 'build deterministic monitor' + new, 0), ] options_debug = [ ('show_parse', 'show traces during parsing', 0), @@ -569,7 +571,11 @@ elif trans_fm: elif trans_taa: automaton = spot.ltl_to_taa(f, dict, refined_rules) -if reduce_scc: +if reduce_dmonitor: + automaton = spot.minimize(automaton, True) +elif reduce_wdba: + automaton = spot.minimize(automaton, False) +elif reduce_scc: # Do not suppress all useless acceptance conditions if # degeneralization is requested: keeping those that lead to # accepting states usually help. diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 249052837..514ad0441 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -77,16 +77,17 @@ #include "tgba/tgbaproduct.hh" #include "tgba/tgbatba.hh" -#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" -#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/emptiness.hh" #include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/ltl2taa.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/magic.hh" +#include "tgbaalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/rundotdec.hh" @@ -137,22 +138,23 @@ using namespace spot; %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" -%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; -%feature("new") spot::tgba_dupexp_bfs; -%feature("new") spot::tgba_dupexp_dfs; %feature("new") spot::emptiness_check::check; +%feature("new") spot::emptiness_check_instantiator::construct; +%feature("new") spot::emptiness_check_instantiator::instanciate; %feature("new") spot::emptiness_check_result::accepting_run; %feature("new") spot::explicit_magic_search; %feature("new") spot::explicit_se05_search; +%feature("new") spot::ltl_to_taa; +%feature("new") spot::ltl_to_tgba_fm; +%feature("new") spot::ltl_to_tgba_lacim; +%feature("new") spot::minimize; %feature("new") spot::reduc_tgba_sim; -%feature("new") spot::emptiness_check_instantiator::construct; -%feature("new") spot::emptiness_check_instantiator::instanciate; %feature("new") spot::scc_filter; +%feature("new") spot::tgba_dupexp_bfs; +%feature("new") spot::tgba_dupexp_dfs; +%feature("new") spot::tgba::get_init_state; +%feature("new") spot::tgba::succ_iter; +%feature("new") spot::tgba_succ_iterator::current_state; // Help SWIG with namespace lookups. #define ltl spot::ltl @@ -170,16 +172,17 @@ using namespace spot; %include "tgba/tgbaproduct.hh" %include "tgba/tgbatba.hh" -%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" -%include "tgbaalgos/lbtt.hh" %include "tgbaalgos/emptiness.hh" %include "tgbaalgos/gtec/gtec.hh" +%include "tgbaalgos/lbtt.hh" +%include "tgbaalgos/ltl2taa.hh" +%include "tgbaalgos/ltl2tgba_fm.hh" +%include "tgbaalgos/ltl2tgba_lacim.hh" %include "tgbaalgos/magic.hh" +%include "tgbaalgos/minimize.hh" %include "tgbaalgos/neverclaim.hh" %include "tgbaalgos/reductgba_sim.hh" %include "tgbaalgos/rundotdec.hh"