diff --git a/ChangeLog b/ChangeLog index eec8f555a..74bdf8af7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-01-30 Alexandre Duret-Lutz + + Add SCC pruning options to the CGI script. + + * wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically + prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting + SCCs in all algorithms. + * src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to + SWIG. + * wrap/python/spot.i: Include reductgba_sim.hh. + 2010-01-30 Alexandre Duret-Lutz * src/evtgbatest/ltl2evtgba.test: Replace * by &. diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index ac53d8843..3e15348b8 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -40,8 +40,12 @@ namespace spot /// Options for reduce. enum reduce_tgba_options { + // Reduce_None and Reduce_All clash with the definitions in ltl::reduce + // for Swig because Swig does not handle namespaces. +#ifndef SWIG /// No reduction. Reduce_None = 0, +#endif /// Reduction of state using direct simulation relation. Reduce_quotient_Dir_Sim = 1, /// Reduction of transitions using direct simulation relation. @@ -52,8 +56,10 @@ namespace spot Reduce_transition_Del_Sim = 8, /// Reduction using SCC. Reduce_Scc = 16, +#ifndef SWIG /// All reductions. Reduce_All = -1U +#endif }; /// \brief Remove some node of the automata using a simulation @@ -65,6 +71,8 @@ namespace spot /// \return the reduced automata. const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); +#ifndef SWIG + /// \brief Compute a direct simulation relation on state of tgba \a f. direct_simulation_relation* get_direct_relation_simulation(const tgba* a, std::ostream& os, @@ -328,9 +336,10 @@ namespace spot /// \brief The Jurdzinski's lifting algorithm. virtual void lift(); - }; +#endif // SWIG + /// @} } diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in index 40f9bfc0c..ca0f50bd3 100755 --- a/wrap/python/cgi-bin/ltl2tgba.in +++ b/wrap/python/cgi-bin/ltl2tgba.in @@ -234,12 +234,12 @@ formula = form.getfirst('formula', '') color_fm = "#DFC6F8" color_lacim = "#F8C6DF" -color_taa = "#D8C6FF" +color_taa = "#F8DFC6" options_common = [ ('show_formula_png', 'draw the formula', 0), - ('show_automaton_png', 'draw Büchi automaton', 1), - ('show_degen_png', 'draw degeneralized Büchi automaton', 0), + ('show_automaton_png', 'draw Büchi automaton', 1), + ('show_degen_png', 'draw degeneralized Büchi automaton', 0), ('show_never_claim', 'output Spin never claim', 0), ('show_lbtt', 'convert automaton for LBTT', 0), ] @@ -248,6 +248,9 @@ options_reduce = [ ('reduce_syntimpl', 'syntactic implication', 1), ('reduce_eventuniv', 'eventuality and universality', 1), ] +options_aut_reduce = [ + ('reduce_scc', 'prune unaccepting SCCs', 0), + ] options_debug = [ ('show_parse', 'show traces during parsing', 0), ('show_dictionnary', 'print BDD dictionary', 0), @@ -260,6 +263,8 @@ options_trans_fm = [ ('opt_fair_loop_approx','fair-loop approximations', 0), ] options_trans_lacim = [ + ('symbolically_prune_scc', + 'symbolically prune unaccepting SCCs', 1), ('show_relation_set', 'print the transition relation as a BDD set', 0), ('show_relation_png', @@ -429,8 +434,9 @@ for opt, desc, color in translators: add_options('', 0, color, globals()['options_' + opt]) add_options("Search accepting run?", 0, '', options_accepting_run) -add_options("Common Options", 1, '', options_common) +add_options("Common Output Options", 1, '', options_common) add_options("Formula Simplications", 1, '', options_reduce) +add_options("Automata Simplifications", 1, '', options_aut_reduce) add_options("Debugging Options", 1, '', options_debug) print '' @@ -533,6 +539,8 @@ else: if trans_lacim: automaton = spot.ltl_to_tgba_lacim(f, dict) + if symbolically_prune_scc: + automaton.delete_unaccepting_scc() elif trans_fm: automaton = spot.ltl_to_tgba_fm(f, dict, exprop, symb_merge, branching_postponement, @@ -540,6 +548,9 @@ elif trans_fm: elif trans_taa: automaton = spot.ltl_to_taa(f, dict, refined_rules) +if reduce_scc: + automaton = spot.reduc_tgba_sim(automaton, spot.Reduce_Scc) + print 'done.

' sys.stdout.flush() @@ -636,7 +647,7 @@ if draw_acc_run or print_acc_run: print ('Cannot run ' + emptiness_check + ' on automata with more than ' + n_max + ' acceptance ' + 'conditions. Please select "draw degeneralized ' - + 'Büchi automaton" if you want to try this' + + 'Büchi automaton" if you want to try this' + ' algorithm on the degeneralized version of the' + ' automaton.') diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 979b3eaad..cebfa02b5 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique // de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -88,6 +88,7 @@ #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/magic.hh" #include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" @@ -147,7 +148,7 @@ using namespace spot; %feature("new") spot::emptiness_check_result::accepting_run; %feature("new") spot::explicit_magic_search; %feature("new") spot::explicit_se05_search; - +%feature("new") spot::reduc_tgba_sim; %feature("new") spot::emptiness_check_instantiator::construct; %feature("new") spot::emptiness_check_instantiator::instanciate; @@ -178,6 +179,7 @@ using namespace spot; %include "tgbaalgos/gtec/gtec.hh" %include "tgbaalgos/magic.hh" %include "tgbaalgos/neverclaim.hh" +%include "tgbaalgos/reductgba_sim.hh" %include "tgbaalgos/rundotdec.hh" %include "tgbaalgos/save.hh" %include "tgbaalgos/stats.hh"