diff --git a/ChangeLog b/ChangeLog index 53b2b1791..5f86e078a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,17 @@ 2004-11-03 Alexandre Duret-Lutz + * src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh, + src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files. + * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, + libtgbaalgos_la_SOURCES): Add them. + * src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator + as third parameter. + * src/tgbaalgos/dotty.cc (dotty_bfs::process_state, + dotty_bfs::process_link): Use the decorator. + * src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option + is given. + * src/tgbatest/emptchk.test: Exercize -g. + * src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl. * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index c82498942..d3282e906 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -28,6 +28,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ dotty.hh \ + dottydec.hh \ dupexp.hh \ emptiness.hh \ lbtt.hh \ @@ -39,6 +40,7 @@ tgbaalgos_HEADERS = \ projrun.hh \ reachiter.hh \ replayrun.hh \ + rundotdec.hh \ save.hh \ stats.hh \ reductgba_sim.hh @@ -46,6 +48,7 @@ tgbaalgos_HEADERS = \ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ dotty.cc \ + dottydec.cc \ dupexp.cc \ emptiness.cc \ lbtt.cc \ @@ -57,6 +60,7 @@ libtgbaalgos_la_SOURCES = \ projrun.cc \ reachiter.cc \ replayrun.cc \ + rundotdec.cc \ save.cc \ stats.cc \ reductgba_sim.cc \ diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 0f0c50f96..5a2f79f3e 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -33,8 +33,8 @@ namespace spot class dotty_bfs : public tgba_reachable_iterator_breadth_first { public: - dotty_bfs(const tgba* a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), os_(os) + dotty_bfs(std::ostream& os, const tgba* a, dotty_decorator* dd) + : tgba_reachable_iterator_breadth_first(a), os_(os), dd_(dd) { } @@ -53,34 +53,41 @@ namespace spot } void - process_state(const state* s, int n, tgba_succ_iterator*) + process_state(const state* s, int n, tgba_succ_iterator* si) { - os_ << " " << n << " [label=\""; - escape_str(os_, automata_->format_state(s)) << "\"]" << std::endl; + os_ << " " << n << " " + << dd_->state_decl(automata_, s, n, si, + escape_str(automata_->format_state(s))) + << std::endl; } void - process_link(const state*, int in, - const state*, int out, const tgba_succ_iterator* si) + process_link(const state* in_s, int in, + const state* out_s, int out, const tgba_succ_iterator* si) { - os_ << " " << in << " -> " << out << " [label=\""; - escape_str(os_, bdd_format_formula(automata_->get_dict(), - si->current_condition())) << "\\n"; - escape_str(os_, - bdd_format_accset(automata_->get_dict(), - si->current_acceptance_conditions())) - << "\"]" << std::endl; + std::string label = + bdd_format_formula(automata_->get_dict(), + si->current_condition()) + + "\n" + + bdd_format_accset(automata_->get_dict(), + si->current_acceptance_conditions()); + + os_ << " " << in << " -> " << out << " " + << dd_->link_decl(automata_, in_s, in, out_s, out, si, + escape_str(label)) + << std::endl; } private: std::ostream& os_; + dotty_decorator* dd_; }; } std::ostream& - dotty_reachable(std::ostream& os, const tgba* g) + dotty_reachable(std::ostream& os, const tgba* g, dotty_decorator* dd) { - dotty_bfs d(g, os); + dotty_bfs d(os, g, dd); d.run(); return os; } diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index f5143a32c..f1c05ed40 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -22,13 +22,18 @@ #ifndef SPOT_TGBAALGOS_DOTTY_HH # define SPOT_TGBAALGOS_DOTTY_HH -#include "tgba/tgba.hh" +#include "dottydec.hh" #include namespace spot { + class tgba; + /// \brief Print reachable states in dot format. - std::ostream& dotty_reachable(std::ostream& os, const tgba* g); + std::ostream& + dotty_reachable(std::ostream& os, + const tgba* g, + dotty_decorator* dd = dotty_decorator::instance()); } #endif // SPOT_TGBAALGOS_DOTTY_HH diff --git a/src/tgbaalgos/dottydec.cc b/src/tgbaalgos/dottydec.cc new file mode 100644 index 000000000..822304355 --- /dev/null +++ b/src/tgbaalgos/dottydec.cc @@ -0,0 +1,56 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "dottydec.hh" +#include "tgba/tgba.hh" + +namespace spot +{ + dotty_decorator::dotty_decorator() + { + } + + dotty_decorator::~dotty_decorator() + { + } + + std::string + dotty_decorator::state_decl(const tgba*, const state*, int, + tgba_succ_iterator*, const std::string& label) + { + return "[label=\"" + label + "\"]"; + } + + std::string + dotty_decorator::link_decl(const tgba*, const state*, int, const state*, int, + const tgba_succ_iterator*, + const std::string& label) + { + return "[label=\"" + label + "\"]"; + } + + dotty_decorator* + dotty_decorator::instance() + { + static dotty_decorator d; + return &d; + } +} diff --git a/src/tgbaalgos/dottydec.hh b/src/tgbaalgos/dottydec.hh new file mode 100644 index 000000000..fb7fb08b0 --- /dev/null +++ b/src/tgbaalgos/dottydec.hh @@ -0,0 +1,87 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_DOTTYDEC_HH +# define SPOT_TGBAALGOS_DOTTYDEC_HH + +#include + +namespace spot +{ + class state; + class tgba; + class tgba_succ_iterator; + + /// Choose state and link styles for spot::dotty_reachable. + class dotty_decorator + { + public: + virtual ~dotty_decorator(); + + /// \brief Compute the style of a state. + /// + /// This function should output a string of the form + /// [label="foo", style=bar, ...]. The + /// default implementation will simply output [label="LABEL"] + /// with LABEL replaced by the value of \a label. + /// + /// \param a the automaton being drawn + /// \param s the state being drawn (owned by the caller) + /// \param n a unique number for this state + /// \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 + virtual std::string state_decl(const tgba* a, const state* s, int n, + tgba_succ_iterator* si, + const std::string& label); + + /// \brief Compute the style of a link. + /// + /// This function should output a string of the form + /// [label="foo", style=bar, ...]. The + /// default implementation will simply output [label="LABEL"] + /// with LABEL replaced by the value of \a label. + /// + /// \param a the automaton being drawn + /// \param in_s the source state of the transition being drawn + /// (owned by the caller) + /// \param in the unique number associated to \a in_s + /// \param out_s the destination state of the transition being drawn + /// (owned by the caller) + /// \param out the unique number associated to \a out_s + /// \param si an iterator over the successors of \a in_s, pointing to + /// the current transition (owned by the caller and cannot + /// be iterated) + /// \param label the computed name of this state + virtual std::string link_decl(const tgba* a, + const state* in_s, int in, + const state* out_s, int out, + const tgba_succ_iterator* si, + const std::string& label); + + /// Get the unique instance of the default dotty_decorator. + static dotty_decorator* instance(); + protected: + dotty_decorator(); + }; +} + +#endif // SPOT_TGBAALGOS_DOTTYDEC_HH diff --git a/src/tgbaalgos/rundotdec.cc b/src/tgbaalgos/rundotdec.cc new file mode 100644 index 000000000..e61801e2f --- /dev/null +++ b/src/tgbaalgos/rundotdec.cc @@ -0,0 +1,143 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "rundotdec.hh" +#include "tgba/succiter.hh" + +namespace spot +{ + + tgba_run_dotty_decorator::tgba_run_dotty_decorator(const tgba_run* run) + : run_(run) + { + int n = 1; + for (tgba_run::steps::const_iterator i = run->prefix.begin(); + i != run->prefix.end(); ++i, ++n) + map_[i->s].first.push_back(step_num(i, n)); + for (tgba_run::steps::const_iterator i = run->cycle.begin(); + i != run->cycle.end(); ++i, ++n) + map_[i->s].second.push_back(step_num(i, n)); + } + + tgba_run_dotty_decorator::~tgba_run_dotty_decorator() + { + } + + std::string + tgba_run_dotty_decorator::state_decl(const tgba*, const state* s, int, + tgba_succ_iterator*, + const std::string& label) + { + step_map::const_iterator i = map_.find(s); + if (i == map_.end()) + return "[label=\"" + label + "\"]"; + + std::ostringstream os; + std::string sep = "("; + bool in_prefix = false; + bool in_cycle = false; + for (step_set::const_iterator j = i->second.first.begin(); + j != i->second.first.end(); ++j) + { + os << sep << j->second; + sep = ", "; + in_prefix = true; + } + if (sep == ", ") + sep = "; "; + for (step_set::const_iterator j = i->second.second.begin(); + j != i->second.second.end(); ++j) + { + os << sep << j->second; + sep = ", "; + in_cycle = true; + } + 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 + "]"; + } + + std::string + tgba_run_dotty_decorator::link_decl(const tgba*, + const state* in_s, int, + const state* out_s, int, + const tgba_succ_iterator* si, + const std::string& label) + { + step_map::const_iterator i = map_.find(in_s); + if (i != map_.end()) + { + std::ostringstream os; + std::string sep = "("; + bool in_prefix = false; + bool in_cycle = false; + for (step_set::const_iterator j = i->second.first.begin(); + j != i->second.first.end(); ++j) + if (j->first->label == si->current_condition() + && j->first->acc == si->current_acceptance_conditions()) + { + tgba_run::steps::const_iterator j2 = j->first; + ++j2; + if (j2 == run_->prefix.end()) + j2 = run_->cycle.begin(); + if (out_s->compare(j2->s)) + continue; + + os << sep << j->second; + sep = ", "; + in_prefix = true; + } + if (sep == ", ") + sep = "; "; + for (step_set::const_iterator j = i->second.second.begin(); + j != i->second.second.end(); ++j) + if (j->first->label == si->current_condition() + && j->first->acc == si->current_acceptance_conditions()) + { + tgba_run::steps::const_iterator j2 = j->first; + ++j2; + if (j2 == run_->cycle.end()) + j2 = run_->cycle.begin(); + if (out_s->compare(j2->s)) + continue; + + os << sep << j->second; + sep = ", "; + in_cycle = true; + } + os << ")\\n"; + if (in_prefix || in_cycle) + { + std::string + color = in_prefix ? (in_cycle ? "violet" : "blue" ) : "red"; + return ("[label=\"" + os.str() + label + + "\", style=bold, color=" + color + "]"); + + } + } + return "[label=\"" + label + "\"]"; + } + + + +} diff --git a/src/tgbaalgos/rundotdec.hh b/src/tgbaalgos/rundotdec.hh new file mode 100644 index 000000000..fb0237231 --- /dev/null +++ b/src/tgbaalgos/rundotdec.hh @@ -0,0 +1,60 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_RUNDOTDEC_HH +# define SPOT_TGBAALGOS_RUNDOTDEC_HH + +#include +#include +#include +#include "dottydec.hh" +#include "emptiness.hh" + +namespace spot +{ + /// \brief Highlight a spot::tgba_run on a spot::tgba. + /// + /// An instance of this class can be passed to spot::dotty_reachable. + class tgba_run_dotty_decorator: public dotty_decorator + { + public: + tgba_run_dotty_decorator(const tgba_run* run); + virtual ~tgba_run_dotty_decorator(); + + virtual std::string state_decl(const tgba* a, const state* s, int n, + tgba_succ_iterator* si, + const std::string& label); + virtual std::string link_decl(const tgba* a, + const state* in_s, int in, + const state* out_s, int out, + const tgba_succ_iterator* si, + const std::string& label); + private: + const tgba_run* run_; + typedef std::pair step_num; + typedef std::list step_set; + typedef std::map, + spot::state_ptr_less_than> step_map; + step_map map_; + }; +} + +#endif // SPOT_TGBAALGOS_RUNDOTDEC_HH diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index b4136b09f..4f4e78f1d 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -25,18 +25,24 @@ set -e +expect_ce_do() +{ + run 0 ./ltl2tgba "$@" + run 0 ./ltl2tgba -g "$@" +} + expect_ce() { - run 0 ./ltl2tgba -e "$1" - run 0 ./ltl2tgba -e -D "$1" - run 0 ./ltl2tgba -e -f "$1" - run 0 ./ltl2tgba -e -f -D "$1" - run 0 ./ltl2tgba -ecouvreur99_shy "$1" - run 0 ./ltl2tgba -ecouvreur99_shy -D "$1" - run 0 ./ltl2tgba -ecouvreur99_shy -f "$1" - run 0 ./ltl2tgba -ecouvreur99_shy -f -D "$1" - run 0 ./ltl2tgba -emagic_search "$1" - run 0 ./ltl2tgba -emagic_search -f "$1" + expect_ce_do -e "$1" + expect_ce_do -e -D "$1" + expect_ce_do -e -f "$1" + expect_ce_do -e -f -D "$1" + expect_ce_do -ecouvreur99_shy "$1" + expect_ce_do -ecouvreur99_shy -D "$1" + expect_ce_do -ecouvreur99_shy -f "$1" + expect_ce_do -ecouvreur99_shy -f -D "$1" + expect_ce_do -emagic_search "$1" + expect_ce_do -emagic_search -f "$1" } expect_no() diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index b5ef9d7d5..d08cedeff 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -43,6 +43,7 @@ #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/replayrun.hh" +#include "tgbaalgos/rundotdec.hh" void syntax(char* prog) @@ -65,6 +66,7 @@ syntax(char* prog) << " -f use Couvreur's FM algorithm for translation" << std::endl << " -F read the formula from the file" << std::endl + << " -g graph the accepting run on the automaton (requires -e)" << " -L fair-loop approximation (implies -f)" << std::endl << " -N display the never clain for Spin " << "(implies -D)" << std::endl @@ -147,6 +149,7 @@ main(int argc, char** argv) bool display_parity_game = false; bool post_branching = false; bool fair_loop_approx = false; + bool graph_run_opt = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; @@ -199,6 +202,10 @@ main(int argc, char** argv) { file_opt = true; } + else if (!strcmp(argv[formula_index], "-g")) + { + graph_run_opt = true; + } else if (!strcmp(argv[formula_index], "-L")) { fair_loop_approx = true; @@ -347,6 +354,12 @@ main(int argc, char** argv) } } + if (graph_run_opt && (echeck_algo == "" || !expect_counter_example)) + { + std::cerr << argv[0] << ": error: -g requires -e." << std::endl; + exit(1); + } + std::string input; if (file_opt) @@ -561,7 +574,8 @@ main(int argc, char** argv) do { spot::emptiness_check_result* res = ec->check(); - ec->print_stats(std::cout); + if (!graph_run_opt) + ec->print_stats(std::cout); if (expect_counter_example != !!res) exit_code = 1; @@ -580,9 +594,17 @@ main(int argc, char** argv) } else { - spot::print_tgba_run(std::cout, ec_a, run); - if (!spot::replay_tgba_run(std::cout, ec_a, run)) - exit_code = 1; + if (graph_run_opt) + { + spot::tgba_run_dotty_decorator deco(run); + spot::dotty_reachable(std::cout, ec_a, &deco); + } + else + { + spot::print_tgba_run(std::cout, ec_a, run); + if (!spot::replay_tgba_run(std::cout, ec_a, run)) + exit_code = 1; + } delete run; } }