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.
This commit is contained in:
Alexandre Duret-Lutz
parent
322e1a0179
commit
a4766f2f82
4 changed files with 42 additions and 9 deletions
11
ChangeLog
11
ChangeLog
|
|
@ -1,3 +1,14 @@
|
|||
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
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 <adl@lrde.epita.fr>
|
||||
|
||||
* src/evtgbatest/ltl2evtgba.test: Replace * by &.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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 '<TABLE>'
|
||||
|
|
@ -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.</p>'
|
||||
sys.stdout.flush()
|
||||
|
||||
|
|
@ -636,7 +647,7 @@ if draw_acc_run or print_acc_run:
|
|||
print ('<font color="red">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.</font>')
|
||||
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue