Commit e1ef47d9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 2c5bae3d
2011-03-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2011-03-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/ltltest/genltl.cc (GF_n): Really use "op". * src/ltltest/genltl.cc (GF_n): Really use "op".
......
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre // dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie. // et Marie Curie.
...@@ -25,6 +27,7 @@ ...@@ -25,6 +27,7 @@
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "reachiter.hh" #include "reachiter.hh"
#include "misc/escape.hh" #include "misc/escape.hh"
#include "tgba/tgbatba.hh"
namespace spot namespace spot
{ {
...@@ -33,8 +36,11 @@ namespace spot ...@@ -33,8 +36,11 @@ namespace spot
class dotty_bfs : public tgba_reachable_iterator_breadth_first class dotty_bfs : public tgba_reachable_iterator_breadth_first
{ {
public: public:
dotty_bfs(std::ostream& os, const tgba* a, dotty_decorator* dd) dotty_bfs(std::ostream& os, const tgba* a, bool mark_accepting_states,
: tgba_reachable_iterator_breadth_first(a), os_(os), dd_(dd) dotty_decorator* dd)
: tgba_reachable_iterator_breadth_first(a), os_(os),
mark_accepting_states_(mark_accepting_states), dd_(dd),
sba_(dynamic_cast<const tgba_sba_proxy*>(a))
{ {
} }
...@@ -55,9 +61,31 @@ namespace spot ...@@ -55,9 +61,31 @@ namespace spot
void void
process_state(const state* s, int n, tgba_succ_iterator* si) 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 << " " os_ << " " << n << " "
<< dd_->state_decl(automata_, s, n, si, << dd_->state_decl(automata_, s, n, si,
escape_str(automata_->format_state(s))) escape_str(automata_->format_state(s)),
accepting)
<< std::endl; << std::endl;
} }
...@@ -80,14 +108,17 @@ namespace spot ...@@ -80,14 +108,17 @@ namespace spot
private: private:
std::ostream& os_; std::ostream& os_;
bool mark_accepting_states_;
dotty_decorator* dd_; dotty_decorator* dd_;
const tgba_sba_proxy* sba_;
}; };
} }
std::ostream& 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(); d.run();
return os; return os;
} }
......
// 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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
...@@ -31,12 +31,17 @@ namespace spot ...@@ -31,12 +31,17 @@ namespace spot
/// \brief Print reachable states in dot format. /// \brief Print reachable states in dot format.
/// \ingroup tgba_io /// \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 /// The \a dd argument allows to customize the output in various
/// ways. See \ref tgba_dotty "this page" for a list of available /// ways. See \ref tgba_dotty "this page" for a list of available
/// decorators. /// decorators.
std::ostream& std::ostream&
dotty_reachable(std::ostream& os, dotty_reachable(std::ostream& os,
const tgba* g, const tgba* g,
bool assume_sba = false,
dotty_decorator* dd = dotty_decorator::instance()); dotty_decorator* dd = dotty_decorator::instance());
} }
......
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
...@@ -34,9 +36,13 @@ namespace spot ...@@ -34,9 +36,13 @@ namespace spot
std::string std::string
dotty_decorator::state_decl(const tgba*, const state*, int, 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 std::string
......
// 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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
...@@ -53,9 +53,12 @@ namespace spot ...@@ -53,9 +53,12 @@ namespace spot
/// \param si an iterator over the successors of this state (owned by the /// \param si an iterator over the successors of this state (owned by the
/// caller, but can be freely iterated) /// caller, but can be freely iterated)
/// \param label the computed name of this state /// \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, virtual std::string state_decl(const tgba* a, const state* s, int n,
tgba_succ_iterator* si, tgba_succ_iterator* si,
const std::string& label); const std::string& label,
bool accepting);
/// \brief Compute the style of a link. /// \brief Compute the style of a link.
/// ///
...@@ -86,6 +89,7 @@ namespace spot ...@@ -86,6 +89,7 @@ namespace spot
protected: protected:
dotty_decorator(); dotty_decorator();
}; };
} }
#endif // SPOT_TGBAALGOS_DOTTYDEC_HH #endif // SPOT_TGBAALGOS_DOTTYDEC_HH
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre // dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie. // et Marie Curie.
// //
...@@ -45,11 +45,13 @@ namespace spot ...@@ -45,11 +45,13 @@ namespace spot
std::string std::string
tgba_run_dotty_decorator::state_decl(const tgba*, const state* s, int, tgba_run_dotty_decorator::state_decl(const tgba*, const state* s, int,
tgba_succ_iterator*, tgba_succ_iterator*,
const std::string& label) const std::string& label,
bool accepting)
{ {
step_map::const_iterator i = map_.find(s); step_map::const_iterator i = map_.find(s);
std::string acc = accepting ? ", peripheries=2" : "";
if (i == map_.end()) if (i == map_.end())
return "[label=\"" + label + "\"]"; return "[label=\"" + label + acc + "\"]";
std::ostringstream os; std::ostringstream os;
std::string sep = "("; std::string sep = "(";
...@@ -74,7 +76,8 @@ namespace spot ...@@ -74,7 +76,8 @@ namespace spot
assert(in_cycle || in_prefix); assert(in_cycle || in_prefix);
os << ")\\n" << label; os << ")\\n" << label;
std::string color = in_prefix ? (in_cycle ? "violet" : "blue") : "red"; 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 std::string
......
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre // dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie. // et Marie Curie.
...@@ -42,7 +44,8 @@ namespace spot ...@@ -42,7 +44,8 @@ namespace spot
virtual std::string state_decl(const tgba* a, const state* s, int n, virtual std::string state_decl(const tgba* a, const state* s, int n,
tgba_succ_iterator* si, tgba_succ_iterator* si,
const std::string& label); const std::string& label,
bool accepting);
virtual std::string link_decl(const tgba* a, virtual std::string link_decl(const tgba* a,
const state* in_s, int in, const state* in_s, int in,
const state* out_s, int out, const state* out_s, int out,
......
...@@ -336,6 +336,7 @@ main(int argc, char** argv) ...@@ -336,6 +336,7 @@ main(int argc, char** argv)
spot::bdd_dict* dict = new spot::bdd_dict(); spot::bdd_dict* dict = new spot::bdd_dict();
spot::timer_map tm; spot::timer_map tm;
bool use_timer = false; bool use_timer = false;
bool assume_sba = false;
for (;;) for (;;)
{ {
...@@ -924,14 +925,20 @@ main(int argc, char** argv) ...@@ -924,14 +925,20 @@ main(int argc, char** argv)
&& n_acc > 1 && n_acc > 1
&& echeck_inst->max_acceptance_conditions() < n_acc) && echeck_inst->max_acceptance_conditions() < n_acc)
degeneralize_opt = DegenTBA; degeneralize_opt = DegenTBA;
if (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) 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) 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; const spot::tgba* minimized = 0;
if (opt_minimize) if (opt_minimize)
...@@ -957,6 +964,7 @@ main(int argc, char** argv) ...@@ -957,6 +964,7 @@ main(int argc, char** argv)
else else
{ {
a = minimized; a = minimized;
assume_sba = true;
} }
} }
...@@ -965,6 +973,9 @@ main(int argc, char** argv) ...@@ -965,6 +973,9 @@ main(int argc, char** argv)
tm.start("Monitor minimization"); tm.start("Monitor minimization");
a = minimized = minimize_monitor(a); a = minimized = minimize_monitor(a);
tm.stop("Monitor minimization"); 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; spot::tgba_reduc* aut_red = 0;
...@@ -1045,6 +1056,8 @@ main(int argc, char** argv) ...@@ -1045,6 +1056,8 @@ main(int argc, char** argv)
{ {
a = product = product_to_free = new spot::tgba_product(system, a); a = product = product_to_free = new spot::tgba_product(system, a);
assume_sba = false;
unsigned int n_acc = a->number_of_acceptance_conditions(); unsigned int n_acc = a->number_of_acceptance_conditions();
if (echeck_inst if (echeck_inst
&& degeneralize_opt == NoDegen && degeneralize_opt == NoDegen
...@@ -1052,11 +1065,16 @@ main(int argc, char** argv) ...@@ -1052,11 +1065,16 @@ main(int argc, char** argv)
&& echeck_inst->max_acceptance_conditions() < n_acc) && echeck_inst->max_acceptance_conditions() < n_acc)
degeneralize_opt = DegenTBA; degeneralize_opt = DegenTBA;
if (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) 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 if (echeck_inst
...@@ -1088,7 +1106,7 @@ main(int argc, char** argv) ...@@ -1088,7 +1106,7 @@ main(int argc, char** argv)
switch (output) switch (output)
{ {
case 0: case 0:
spot::dotty_reachable(std::cout, a); spot::dotty_reachable(std::cout, a, assume_sba);
break; break;
case 1: case 1:
if (concrete) if (concrete)
...@@ -1296,7 +1314,8 @@ main(int argc, char** argv) ...@@ -1296,7 +1314,8 @@ main(int argc, char** argv)
if (graph_run_opt) if (graph_run_opt)
{ {
spot::tgba_run_dotty_decorator deco(run); 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) else if (graph_run_tgba_opt)
{ {
......
...@@ -31,7 +31,7 @@ dot_bgcolor = '-Gbgcolor=#FFFFFF00' ...@@ -31,7 +31,7 @@ dot_bgcolor = '-Gbgcolor=#FFFFFF00'
svg_output = False # FIXME: SVG output seems to be working well with svg_output = False # FIXME: SVG output seems to be working well with
# Firefox only. We have to figure out how # 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. # background in Chrome.
from CGIHTTPServer import CGIHTTPRequestHandler from CGIHTTPServer import CGIHTTPRequestHandler
...@@ -124,12 +124,12 @@ def render_dot(basename): ...@@ -124,12 +124,12 @@ def render_dot(basename):
print '</div>' print '</div>'
sys.stdout.flush() 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') outfile = spot.ofstream(basename + '.txt')
if not deco: if not deco:
spot.dotty_reachable(outfile, automata) spot.dotty_reachable(outfile, automata, issba)
else: else:
spot.dotty_reachable(outfile, automata, deco) spot.dotty_reachable(outfile, automata, issba, deco)
del outfile del outfile
if dont_run_dot: if dont_run_dot:
print ('<p>' + dont_run_dot + ''' to be rendered on-line. However print ('<p>' + dont_run_dot + ''' to be rendered on-line. However
...@@ -182,7 +182,7 @@ imgprefix = imgdir + '/' + uid ...@@ -182,7 +182,7 @@ imgprefix = imgdir + '/' + uid
output_type = form.getfirst('o', 'v'); output_type = form.getfirst('o', 'v');
# Version requested. # Version requested.
if output_type == 'v': if output_type == 'v':
print 'Spot version ' + spot.version() print 'Spot version ' + spot.version()
exit(0) exit(0)
...@@ -221,13 +221,13 @@ if opt != spot.Reduce_None: ...@@ -221,13 +221,13 @@ if opt != spot.Reduce_None:
# Formula manipulation only. # Formula manipulation only.
if output_type == 'f': if output_type == 'f':
formula_format = form.getfirst('ff', 'o') formula_format = form.getfirst('ff', 'o')
# o = Spot, i = Spin, g = GraphViz # o = Spot, i = Spin, g = GraphViz
if formula_format == 'o': if formula_format == 'o':
print '<div class="formula spot-format">%s</div>' % f print '<div class="formula spot-format">%s</div>' % f
elif formula_format == 'i': elif formula_format == 'i':
print ('<div class="formula spin-format">' print ('<div class="formula spin-format">'
+ spot.to_spin_string(f) + '</div>') + spot.to_spin_string(f) + '</div>')
elif formula_format == 'g': elif formula_format == 'g':
outfile = spot.ofstream(imgprefix + '-f.txt') outfile = spot.ofstream(imgprefix + '-f.txt')
...@@ -256,7 +256,7 @@ if translator == 'fm': ...@@ -256,7 +256,7 @@ if translator == 'fm':
elif fm == 'fl': elif fm == 'fl':
fair_loop_approx = True fair_loop_approx = True
automaton = spot.ltl_to_tgba_fm(f, dict, automaton = spot.ltl_to_tgba_fm(f, dict,
exprop, symb_merge, exprop, symb_merge,
branching_postponement, fair_loop_approx) branching_postponement, fair_loop_approx)
elif translator == 'la': elif translator == 'la':
automaton = spot.ltl_to_tgba_lacim(f, dict) automaton = spot.ltl_to_tgba_lacim(f, dict)
...@@ -268,6 +268,9 @@ elif translator == 'ta': ...@@ -268,6 +268,9 @@ elif translator == 'ta':
refined_rules = True refined_rules = True
automaton = spot.ltl_to_taa(f, dict, refined_rules) automaton = spot.ltl_to_taa(f, dict, refined_rules)
# Should it be displayed as a SBA?
issba = False
# Monitor output # Monitor output
if output_type == 'm': if output_type == 'm':
automaton = spot.scc_filter(automaton) automaton = spot.scc_filter(automaton)
...@@ -275,7 +278,7 @@ if output_type == 'm': ...@@ -275,7 +278,7 @@ if output_type == 'm':
print '<div class="automata-stats">' print '<div class="automata-stats">'
dont_run_dot = print_stats(automaton) dont_run_dot = print_stats(automaton)
print '</div>' print '</div>'
render_automaton(imgprefix + '-a', automaton, dont_run_dot) render_automaton(imgprefix + '-a', automaton, dont_run_dot, issba)
automaton = 0 automaton = 0
exit(0) exit(0)
...@@ -317,9 +320,11 @@ if wdba_minimize: ...@@ -317,9 +320,11 @@ if wdba_minimize:
automaton = minimized automaton = minimized
minimized = 0 minimized = 0
degen = False # No need to degeneralize anymore degen = False # No need to degeneralize anymore
issba = True
if degen or neverclaim: if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton) degen = spot.tgba_sba_proxy(automaton)
issba = True
else: else:
degen = automaton degen = automaton
...@@ -332,7 +337,7 @@ if output_type == 'a': ...@@ -332,7 +337,7 @@ if output_type == 'a':
del s del s
else: # 't' or 's' else: # 't' or 's'
dont_run_dot = print_stats(degen) 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 degen = 0
automaton = 0 automaton = 0
exit(0) exit(0)
...@@ -391,13 +396,14 @@ if output_type == 'r': ...@@ -391,13 +396,14 @@ if output_type == 'r':
if draw_acc_run: if draw_acc_run:
deco = spot.tgba_run_dotty_decorator(ec_run) deco = spot.tgba_run_dotty_decorator(ec_run)
dont_run_dot = print_stats(ec_a) 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 deco
del ec_run del ec_run
del ec_res del ec_res
print '</div>' print '</div>'
del ec del ec
del ec_a del ec_a
degen = 0 degen = 0
automaton = 0 automaton = 0
exit(0) exit(0)
...@@ -205,12 +205,12 @@ def render_dot(basename): ...@@ -205,12 +205,12 @@ def render_dot(basename):
+ '.txt">dot source</a>)') + '.txt">dot source</a>)')