diff --git a/ChangeLog b/ChangeLog index 546bfa279..979871062 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,25 @@ +2011-03-05 Alexandre Duret-Lutz + + Using double borders for acceptance states in SBAs. + + * src/tgbaalgos/dotty.hh (dotty_reachable): Take a new + assume_sba argument. + * src/tgbaalgos/dotty.cc (dotty_bfs): Take a new + mark_accepting_states arguments. + (dotty_bfs::process_state): Check if a state is accepting using + the state_is_accepting() method for tgba_sba_proxies, or by + looking at the first outgoing transition of the state. Pass + the result to the dectorator. + (dotty_reachable): Adjust function. + * src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc, + src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc + (state_decl): Add an "accepting" argument, and use it to + decorate accepting states with a double border. + * src/tgbatest/ltl2tgba.cc: Keep track of whether the output + is an SBA or not, so that we can tell it to dotty(). + * wrap/python/ajax/spot.in: Likewise. + * wrap/python/cgi-bin/ltl2tgba.in: Likewise. + 2011-03-05 Alexandre Duret-Lutz * src/ltltest/genltl.cc (GF_n): Really use "op". diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 5a2f79f3e..76a9363ab 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -25,6 +27,7 @@ #include "tgba/bddprint.hh" #include "reachiter.hh" #include "misc/escape.hh" +#include "tgba/tgbatba.hh" namespace spot { @@ -33,8 +36,11 @@ namespace spot class dotty_bfs : public tgba_reachable_iterator_breadth_first { public: - dotty_bfs(std::ostream& os, const tgba* a, dotty_decorator* dd) - : tgba_reachable_iterator_breadth_first(a), os_(os), dd_(dd) + dotty_bfs(std::ostream& os, const tgba* a, bool mark_accepting_states, + dotty_decorator* dd) + : tgba_reachable_iterator_breadth_first(a), os_(os), + mark_accepting_states_(mark_accepting_states), dd_(dd), + sba_(dynamic_cast(a)) { } @@ -55,9 +61,31 @@ namespace spot void process_state(const state* s, int n, tgba_succ_iterator* si) { + bool accepting; + + if (mark_accepting_states_) + { + if (sba_) + { + accepting = sba_->state_is_accepting(s); + } + else + { + si->first(); + accepting = ((!si->done()) + && (si->current_acceptance_conditions() == + automata_->all_acceptance_conditions())); + } + } + else + { + accepting = false; + } + os_ << " " << n << " " << dd_->state_decl(automata_, s, n, si, - escape_str(automata_->format_state(s))) + escape_str(automata_->format_state(s)), + accepting) << std::endl; } @@ -80,14 +108,17 @@ namespace spot private: std::ostream& os_; + bool mark_accepting_states_; dotty_decorator* dd_; + const tgba_sba_proxy* sba_; }; } std::ostream& - dotty_reachable(std::ostream& os, const tgba* g, dotty_decorator* dd) + dotty_reachable(std::ostream& os, const tgba* g, + bool assume_sba, dotty_decorator* dd) { - dotty_bfs d(os, g, dd); + dotty_bfs d(os, g, assume_sba, dd); d.run(); return os; } diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index 28df1d03c..71901d0eb 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -31,12 +31,17 @@ namespace spot /// \brief Print reachable states in dot format. /// \ingroup tgba_io + /// + /// If assume_sba is set, this assumes that the automaton + /// is an SBA and use double elipse to mark accepting states. + /// /// The \a dd argument allows to customize the output in various /// ways. See \ref tgba_dotty "this page" for a list of available /// decorators. std::ostream& dotty_reachable(std::ostream& os, const tgba* g, + bool assume_sba = false, dotty_decorator* dd = dotty_decorator::instance()); } diff --git a/src/tgbaalgos/dottydec.cc b/src/tgbaalgos/dottydec.cc index 822304355..955b2410b 100644 --- a/src/tgbaalgos/dottydec.cc +++ b/src/tgbaalgos/dottydec.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -34,9 +36,13 @@ namespace spot std::string dotty_decorator::state_decl(const tgba*, const state*, int, - tgba_succ_iterator*, const std::string& label) + tgba_succ_iterator*, const std::string& label, + bool accepting) { - return "[label=\"" + label + "\"]"; + if (accepting) + return "[label=\"" + label + "\", peripheries=2]"; + else + return "[label=\"" + label + "\"]"; } std::string diff --git a/src/tgbaalgos/dottydec.hh b/src/tgbaalgos/dottydec.hh index bf7a0fd17..c3bdb4689 100644 --- a/src/tgbaalgos/dottydec.hh +++ b/src/tgbaalgos/dottydec.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -53,9 +53,12 @@ namespace spot /// \param si an iterator over the successors of this state (owned by the /// caller, but can be freely iterated) /// \param label the computed name of this state + /// \param accepting whether the state is accepting (it makes sense only + /// for state-acceptance automata) virtual std::string state_decl(const tgba* a, const state* s, int n, tgba_succ_iterator* si, - const std::string& label); + const std::string& label, + bool accepting); /// \brief Compute the style of a link. /// @@ -86,6 +89,7 @@ namespace spot protected: dotty_decorator(); }; + } #endif // SPOT_TGBAALGOS_DOTTYDEC_HH diff --git a/src/tgbaalgos/rundotdec.cc b/src/tgbaalgos/rundotdec.cc index e9bddf37c..340397ab5 100644 --- a/src/tgbaalgos/rundotdec.cc +++ b/src/tgbaalgos/rundotdec.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -45,11 +45,13 @@ namespace spot std::string tgba_run_dotty_decorator::state_decl(const tgba*, const state* s, int, tgba_succ_iterator*, - const std::string& label) + const std::string& label, + bool accepting) { step_map::const_iterator i = map_.find(s); + std::string acc = accepting ? ", peripheries=2" : ""; if (i == map_.end()) - return "[label=\"" + label + "\"]"; + return "[label=\"" + label + acc + "\"]"; std::ostringstream os; std::string sep = "("; @@ -74,7 +76,8 @@ namespace spot assert(in_cycle || in_prefix); os << ")\\n" << label; std::string color = in_prefix ? (in_cycle ? "violet" : "blue") : "red"; - return "[label=\"" + os.str() + "\", style=bold, color=" + color + "]"; + return "[label=\"" + os.str() + "\", style=bold, color=" + + color + acc + "]"; } std::string diff --git a/src/tgbaalgos/rundotdec.hh b/src/tgbaalgos/rundotdec.hh index 008d5bd71..bdabc791c 100644 --- a/src/tgbaalgos/rundotdec.hh +++ b/src/tgbaalgos/rundotdec.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -42,7 +44,8 @@ namespace spot virtual std::string state_decl(const tgba* a, const state* s, int n, tgba_succ_iterator* si, - const std::string& label); + const std::string& label, + bool accepting); virtual std::string link_decl(const tgba* a, const state* in_s, int in, const state* out_s, int out, diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 676b7148a..98ed72f38 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -336,6 +336,7 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); spot::timer_map tm; bool use_timer = false; + bool assume_sba = false; for (;;) { @@ -924,14 +925,20 @@ main(int argc, char** argv) && n_acc > 1 && echeck_inst->max_acceptance_conditions() < n_acc) degeneralize_opt = DegenTBA; + if (degeneralize_opt == DegenTBA) - a = degeneralized = new spot::tgba_tba_proxy(a); + { + a = degeneralized = new spot::tgba_tba_proxy(a); + } else if (degeneralize_opt == DegenSBA) - a = degeneralized = new spot::tgba_sba_proxy(a); + { + a = degeneralized = new spot::tgba_sba_proxy(a); + assume_sba = true; + } else if (labeling_opt == StateLabeled) - { - a = state_labeled = new spot::tgba_sgba_proxy(a); - } + { + a = state_labeled = new spot::tgba_sgba_proxy(a); + } const spot::tgba* minimized = 0; if (opt_minimize) @@ -957,6 +964,7 @@ main(int argc, char** argv) else { a = minimized; + assume_sba = true; } } @@ -965,6 +973,9 @@ main(int argc, char** argv) tm.start("Monitor minimization"); a = minimized = minimize_monitor(a); tm.stop("Monitor minimization"); + assume_sba = false; // All states are accepting, so double + // circles in the dot output are + // pointless. } spot::tgba_reduc* aut_red = 0; @@ -1045,6 +1056,8 @@ main(int argc, char** argv) { a = product = product_to_free = new spot::tgba_product(system, a); + assume_sba = false; + unsigned int n_acc = a->number_of_acceptance_conditions(); if (echeck_inst && degeneralize_opt == NoDegen @@ -1052,11 +1065,16 @@ main(int argc, char** argv) && echeck_inst->max_acceptance_conditions() < n_acc) degeneralize_opt = DegenTBA; if (degeneralize_opt == DegenTBA) - a = product = product_degeneralized = - new spot::tgba_tba_proxy(product); + { + a = product = product_degeneralized = + new spot::tgba_tba_proxy(product); + } else if (degeneralize_opt == DegenSBA) - a = product = product_degeneralized = - new spot::tgba_sba_proxy(product); + { + a = product = product_degeneralized = + new spot::tgba_sba_proxy(product); + assume_sba = true; + } } if (echeck_inst @@ -1088,7 +1106,7 @@ main(int argc, char** argv) switch (output) { case 0: - spot::dotty_reachable(std::cout, a); + spot::dotty_reachable(std::cout, a, assume_sba); break; case 1: if (concrete) @@ -1296,7 +1314,8 @@ main(int argc, char** argv) if (graph_run_opt) { spot::tgba_run_dotty_decorator deco(run); - spot::dotty_reachable(std::cout, a, &deco); + spot::dotty_reachable(std::cout, a, + assume_sba, &deco); } else if (graph_run_tgba_opt) { diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 6fda08063..3ca4999de 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -31,7 +31,7 @@ dot_bgcolor = '-Gbgcolor=#FFFFFF00' svg_output = False # FIXME: SVG output seems to be working well with # Firefox only. We have to figure out how - # to get the correct size and transparent + # to get the correct size and transparent # background in Chrome. from CGIHTTPServer import CGIHTTPRequestHandler @@ -124,12 +124,12 @@ def render_dot(basename): print '' sys.stdout.flush() -def render_automaton(basename, automata, dont_run_dot, deco = False): +def render_automaton(basename, automata, dont_run_dot, issba, deco = False): outfile = spot.ofstream(basename + '.txt') if not deco: - spot.dotty_reachable(outfile, automata) + spot.dotty_reachable(outfile, automata, issba) else: - spot.dotty_reachable(outfile, automata, deco) + spot.dotty_reachable(outfile, automata, issba, deco) del outfile if dont_run_dot: print ('

' + dont_run_dot + ''' to be rendered on-line. However @@ -182,7 +182,7 @@ imgprefix = imgdir + '/' + uid output_type = form.getfirst('o', 'v'); # Version requested. -if output_type == 'v': +if output_type == 'v': print 'Spot version ' + spot.version() exit(0) @@ -221,13 +221,13 @@ if opt != spot.Reduce_None: # Formula manipulation only. if output_type == 'f': - formula_format = form.getfirst('ff', 'o') + formula_format = form.getfirst('ff', 'o') # o = Spot, i = Spin, g = GraphViz - + if formula_format == 'o': print '

%s
' % f elif formula_format == 'i': - print ('
' + print ('
' + spot.to_spin_string(f) + '
') elif formula_format == 'g': outfile = spot.ofstream(imgprefix + '-f.txt') @@ -256,7 +256,7 @@ if translator == 'fm': elif fm == 'fl': fair_loop_approx = True automaton = spot.ltl_to_tgba_fm(f, dict, - exprop, symb_merge, + exprop, symb_merge, branching_postponement, fair_loop_approx) elif translator == 'la': automaton = spot.ltl_to_tgba_lacim(f, dict) @@ -268,6 +268,9 @@ elif translator == 'ta': refined_rules = True automaton = spot.ltl_to_taa(f, dict, refined_rules) +# Should it be displayed as a SBA? +issba = False + # Monitor output if output_type == 'm': automaton = spot.scc_filter(automaton) @@ -275,7 +278,7 @@ if output_type == 'm': print '
' dont_run_dot = print_stats(automaton) print '
' - render_automaton(imgprefix + '-a', automaton, dont_run_dot) + render_automaton(imgprefix + '-a', automaton, dont_run_dot, issba) automaton = 0 exit(0) @@ -317,9 +320,11 @@ if wdba_minimize: automaton = minimized minimized = 0 degen = False # No need to degeneralize anymore + issba = True if degen or neverclaim: degen = spot.tgba_sba_proxy(automaton) + issba = True else: degen = automaton @@ -332,7 +337,7 @@ if output_type == 'a': del s else: # 't' or 's' dont_run_dot = print_stats(degen) - render_automaton(imgprefix + '-a', degen, dont_run_dot) + render_automaton(imgprefix + '-a', degen, dont_run_dot, issba) degen = 0 automaton = 0 exit(0) @@ -391,13 +396,14 @@ if output_type == 'r': if draw_acc_run: deco = spot.tgba_run_dotty_decorator(ec_run) dont_run_dot = print_stats(ec_a) - render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco) + render_automaton(imgprefix + '-e', ec_a, dont_run_dot, + issba, deco) del deco del ec_run del ec_res print '
' del ec - del ec_a + del ec_a degen = 0 automaton = 0 exit(0) diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in index 32a6b9c76..cb53e670d 100755 --- a/wrap/python/cgi-bin/ltl2tgba.in +++ b/wrap/python/cgi-bin/ltl2tgba.in @@ -205,12 +205,12 @@ def render_dot(basename): + '.txt">dot source)') sys.stdout.flush() -def render_automaton(basename, automata, dont_run_dot, deco = False): +def render_automaton(basename, automata, dont_run_dot, issba, deco = False): outfile = spot.ofstream(basename + '.txt') if not deco: - spot.dotty_reachable(outfile, automata) + spot.dotty_reachable(outfile, automata, issba) else: - spot.dotty_reachable(outfile, automata, deco) + spot.dotty_reachable(outfile, automata, issba, deco) del outfile if dont_run_dot: print ('

' + dont_run_dot + ''' to be rendered on-line. However @@ -574,6 +574,8 @@ elif trans_fm: elif trans_taa: automaton = spot.ltl_to_taa(f, dict, refined_rules) +issba = False + if reduce_dmonitor: automaton = spot.minimize_monitor(automaton) elif reduce_wdba: @@ -581,6 +583,7 @@ elif reduce_wdba: if minimized: automaton = minimized minimized = 0 + issba = True elif reduce_scc: # Do not suppress all useless acceptance conditions if # degeneralization is requested: keeping those that lead to @@ -594,14 +597,14 @@ sys.stdout.flush() dont_run_dot = print_stats(automaton) if show_automaton_png: - render_automaton(imgprefix + '-a', automaton, dont_run_dot) + render_automaton(imgprefix + '-a', automaton, dont_run_dot, issba) if show_degen_png or show_never_claim: print '

Degeneralized automaton

' degen = spot.tgba_sba_proxy(automaton) dont_run_dot = print_stats(degen) if show_degen_png: - render_automaton(imgprefix + '-d', degen, dont_run_dot) + render_automaton(imgprefix + '-d', degen, dont_run_dot, True) else: degen = 0 @@ -627,7 +630,7 @@ if (type(automaton) == spot.tgba_bdd_concrete print '

Transition relation

' if show_relation_set: escaped_print_set(automaton.get_dict(), - automaton.get_core_data().relation) + automaton.get_core_data().relation) if show_relation_png: render_bdd(imgprefix + '-b', automaton.get_dict(), automaton.get_core_data().relation) @@ -637,7 +640,7 @@ if (type(automaton) == spot.tgba_bdd_concrete print '

Acceptance relation

' if show_acceptance_set: escaped_print_set(automaton.get_dict(), - automaton.get_core_data().acceptance_conditions) + automaton.get_core_data().acceptance_conditions) if show_acceptance_png: render_bdd(imgprefix + '-c', automaton.get_dict(), automaton.get_core_data().acceptance_conditions) @@ -681,6 +684,7 @@ if draw_acc_run or print_acc_run: if degen: ec_a = degen ec_msg += ' on degeneralized automaton' + issba = True else: print ('Cannot run ' + emptiness_check + ' on automata with more than ' + str(n_max) @@ -712,7 +716,8 @@ if draw_acc_run or print_acc_run: if draw_acc_run: deco = spot.tgba_run_dotty_decorator(ec_run) dont_run_dot = print_stats(ec_a) - render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco) + render_automaton(imgprefix + '-e', ec_a, dont_run_dot, + issba, deco) del deco del ec_run del ec_res