From 49701ca3bc4f4ff7c7027647a2ede18bea1c6a14 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 24 Jan 2015 11:54:39 +0100 Subject: [PATCH] dotty: get rid of the decorated version * src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh, src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: Delete. * src/tgbaalgos/Makefile.am, wrap/python/spot.i: Adjust. * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Remove the decorated version, and the related arguments. * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc: Adjust calls. * wrap/python/ajax/spot.in: Draw the accepting run as an automaton instead of painting it. * wrap/python/ajax/ltl2tgba.html: Update help text. --- src/bin/common_aoutput.cc | 5 +- src/bin/dstar2tgba.cc | 5 +- src/tgbaalgos/Makefile.am | 4 - src/tgbaalgos/dotty.cc | 140 +----------------------------- src/tgbaalgos/dotty.hh | 15 +--- src/tgbaalgos/dottydec.cc | 62 -------------- src/tgbaalgos/dottydec.hh | 98 --------------------- src/tgbaalgos/rundotdec.cc | 146 -------------------------------- src/tgbaalgos/rundotdec.hh | 64 -------------- src/tgbatest/complementation.cc | 2 +- src/tgbatest/emptchk.cc | 4 +- src/tgbatest/ltl2tgba.cc | 28 ++---- wrap/python/ajax/ltl2tgba.html | 2 +- wrap/python/ajax/spot.in | 30 ++----- wrap/python/spot.i | 4 - 15 files changed, 26 insertions(+), 583 deletions(-) delete mode 100644 src/tgbaalgos/dottydec.cc delete mode 100644 src/tgbaalgos/dottydec.hh delete mode 100644 src/tgbaalgos/rundotdec.cc delete mode 100644 src/tgbaalgos/rundotdec.hh diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index c64e7cb60..9038f2a14 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -236,10 +236,7 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut, // Do not output anything. break; case Dot: - spot::dotty_reachable(std::cout, aut, - (type == spot::postprocessor::BA) - || (type == spot::postprocessor::Monitor), - opt_dot); + spot::dotty_reachable(std::cout, aut, opt_dot); break; case Lbtt: spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index d22d7efde..be38c0e3b 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -353,10 +353,7 @@ namespace switch (format) { case Dot: - spot::dotty_reachable(std::cout, aut, - (type == spot::postprocessor::BA) - || (type == spot::postprocessor::Monitor), - opt_dot); + spot::dotty_reachable(std::cout, aut, opt_dot); break; case Lbtt: spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 4587115e2..7fb3d361d 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -36,7 +36,6 @@ tgbaalgos_HEADERS = \ cycles.hh \ dtgbacomp.hh \ degen.hh \ - dottydec.hh \ dotty.hh \ dtbasat.hh \ dtgbasat.hh \ @@ -62,7 +61,6 @@ tgbaalgos_HEADERS = \ reachiter.hh \ reducerun.hh \ replayrun.hh \ - rundotdec.hh \ safety.hh \ save.hh \ sccfilter.hh \ @@ -89,7 +87,6 @@ libtgbaalgos_la_SOURCES = \ dtgbacomp.cc \ degen.cc \ dotty.cc \ - dottydec.cc \ dtbasat.cc \ dtgbasat.cc \ dupexp.cc \ @@ -114,7 +111,6 @@ libtgbaalgos_la_SOURCES = \ reachiter.cc \ reducerun.cc \ replayrun.cc \ - rundotdec.cc \ safety.cc \ save.cc \ scc.cc \ diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index eb57bf5e8..927dc7b72 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -24,7 +24,6 @@ #include #include "tgba/tgbagraph.hh" #include "dotty.hh" -#include "dottydec.hh" #include "tgba/bddprint.hh" #include "reachiter.hh" #include "misc/escape.hh" @@ -168,147 +167,12 @@ namespace spot end(); } }; - - - class dotty_bfs : public tgba_reachable_iterator_breadth_first - { - public: - dotty_bfs(std::ostream& os, const_tgba_ptr a, bool mark_accepting_states, - const char* options, dotty_decorator* dd) - : tgba_reachable_iterator_breadth_first(a), os_(os), - mark_accepting_states_(mark_accepting_states), dd_(dd), - sba_(std::dynamic_pointer_cast(a)) - { - if (options) - while (char c = *options++) - switch (c) - { - case 'c': - opt_circles = true; - break; - case 'h': - opt_horizontal = true; - break; - case 'n': - opt_name = true; - break; - case 'N': - opt_name = false; - break; - case 'v': - opt_horizontal = false; - break; - case 't': - mark_accepting_states_ = false; - break; - default: - throw std::runtime_error - (std::string("unknown option for dotty(): ") + c); - } - } - - void - start() - { - os_ << "digraph G {\n"; - if (opt_horizontal) - os_ << " rankdir=LR\n"; - if (opt_name) - if (auto n = aut_->get_named_prop("automaton-name")) - escape_str(os_ << " label=\"", *n) << "\"\n labelloc=\"t\"\n"; - if (opt_circles) - os_ << " node [shape=\"circle\"]\n"; - os_ << " 0 [label=\"\", style=invis, "; - os_ << (opt_horizontal ? "width" : "height"); - os_ << "=0]\n 0 -> 1\n"; - } - - void - end() - { - os_ << '}' << std::endl; - } - - 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(); - auto a = si->current_acceptance_conditions(); - accepting = !si->done() && aut_->acc().accepting(a); - } - } - else - { - accepting = false; - } - - os_ << " " << n << ' ' - << dd_->state_decl(aut_, s, n, si, - escape_str(aut_->format_state(s)), - accepting) - << '\n'; - } - - void - process_link(const state* in_s, int in, - const state* out_s, int out, const tgba_succ_iterator* si) - { - std::string label = - bdd_format_formula(aut_->get_dict(), - si->current_condition()); - if (!mark_accepting_states_) - if (auto a = si->current_acceptance_conditions()) - { - label += "\n"; - label += aut_->acc().format(a); - } - - std::string s = aut_->transition_annotation(si); - if (!s.empty()) - { - if (*label.rbegin() != '\n') - label += '\n'; - label += s; - } - - os_ << " " << in << " -> " << out << ' ' - << dd_->link_decl(aut_, in_s, in, out_s, out, si, - escape_str(label)) - << '\n'; - } - - private: - std::ostream& os_; - bool mark_accepting_states_; - dotty_decorator* dd_; - const_tgba_digraph_ptr sba_; - bool opt_horizontal = true; - bool opt_name = true; - bool opt_circles = false; - }; - } + } // anonymous namespace std::ostream& dotty_reachable(std::ostream& os, const const_tgba_ptr& g, - bool assume_sba, const char* options, - dotty_decorator* dd) + const char* options) { - if (dd) - { - dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), options, dd); - d.run(); - return os; - } dotty_output d(os, options); auto aut = std::dynamic_pointer_cast(g); if (!aut) diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index 48c38b10a..20330fe91 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2012, 2013, 2014, 2015 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. @@ -29,19 +29,12 @@ namespace spot { - class dotty_decorator; - /// \ingroup tgba_io /// \brief Print reachable states in dot format. /// /// If \a 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. If no decorator is specified, the dotty_decorator - /// is used. - /// /// \param options an optional string of letters, each indicating a /// different option. Presently the following options are /// supported: 'v' for vertical output, 'h' for horizontal output, @@ -50,9 +43,7 @@ namespace spot SPOT_API std::ostream& dotty_reachable(std::ostream& os, const const_tgba_ptr& g, - bool assume_sba = false, - const char* options = nullptr, - dotty_decorator* dd = nullptr); + const char* options = nullptr); } #endif // SPOT_TGBAALGOS_DOTTY_HH diff --git a/src/tgbaalgos/dottydec.cc b/src/tgbaalgos/dottydec.cc deleted file mode 100644 index 337ab645e..000000000 --- a/src/tgbaalgos/dottydec.cc +++ /dev/null @@ -1,62 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 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. -// -// 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 3 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 this program. If not, see . - -#include "dottydec.hh" -#include "tgba/tgba.hh" - -namespace spot -{ - dotty_decorator::dotty_decorator() - { - } - - dotty_decorator::~dotty_decorator() - { - } - - std::string - dotty_decorator::state_decl(const const_tgba_ptr&, const state*, int, - tgba_succ_iterator*, const std::string& label, - bool accepting) - { - if (accepting) - return "[label=\"" + label + "\", peripheries=2]"; - else - return "[label=\"" + label + "\"]"; - } - - std::string - dotty_decorator::link_decl(const const_tgba_ptr&, 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 deleted file mode 100644 index eff5104c7..000000000 --- a/src/tgbaalgos/dottydec.hh +++ /dev/null @@ -1,98 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 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. -// -// 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBAALGOS_DOTTYDEC_HH -# define SPOT_TGBAALGOS_DOTTYDEC_HH - -# include "misc/common.hh" -# include -# include - -namespace spot -{ - class state; - class tgba_succ_iterator; - - /// \addtogroup tgba_dotty Decorating the dot output - /// \ingroup tgba_io - - /// \ingroup tgba_dotty - /// \brief Choose state and link styles for spot::dotty_reachable. - class SPOT_API 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 - /// \param accepting whether the state is accepting (it makes sense only - /// for state-acceptance automata) - virtual std::string state_decl(const const_tgba_ptr& a, - const state* s, int n, - tgba_succ_iterator* si, - const std::string& label, - bool accepting); - - /// \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 const_tgba_ptr& 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 deleted file mode 100644 index 17a604887..000000000 --- a/src/tgbaalgos/rundotdec.cc +++ /dev/null @@ -1,146 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). -// 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. -// -// 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 3 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 this program. If not, see . - -#include -#include "rundotdec.hh" - -namespace spot -{ - - tgba_run_dotty_decorator::tgba_run_dotty_decorator(const - const_tgba_run_ptr& 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.emplace_back(i, n); - for (tgba_run::steps::const_iterator i = run->cycle.begin(); - i != run->cycle.end(); ++i, ++n) - map_[i->s].second.emplace_back(i, n); - } - - tgba_run_dotty_decorator::~tgba_run_dotty_decorator() - { - } - - std::string - tgba_run_dotty_decorator::state_decl(const const_tgba_ptr&, - const state* s, int, - tgba_succ_iterator*, - 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 + acc + "\"]"; - - std::ostringstream os; - std::string sep = "("; - bool in_prefix = false; - bool in_cycle = false; - for (auto j: i->second.first) - { - os << sep << j.second; - sep = ", "; - in_prefix = true; - } - if (sep == ", ") - sep = "; "; - for (auto j: i->second.second) - { - 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 + acc + "]"; - } - - std::string - tgba_run_dotty_decorator::link_decl(const const_tgba_ptr&, - 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 deleted file mode 100644 index 433f30314..000000000 --- a/src/tgbaalgos/rundotdec.hh +++ /dev/null @@ -1,64 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 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. -// -// 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBAALGOS_RUNDOTDEC_HH -# define SPOT_TGBAALGOS_RUNDOTDEC_HH - -#include -#include -#include -#include "dottydec.hh" -#include "emptiness.hh" - -namespace spot -{ - /// \ingroup tgba_dotty - /// \brief Highlight a spot::tgba_run on a spot::tgba. - /// - /// An instance of this class can be passed to spot::dotty_reachable. - class SPOT_API tgba_run_dotty_decorator: public dotty_decorator - { - public: - tgba_run_dotty_decorator(const const_tgba_run_ptr& run); - virtual ~tgba_run_dotty_decorator(); - - virtual std::string state_decl(const const_tgba_ptr& a, - const state* s, int n, - tgba_succ_iterator* si, - const std::string& label, - bool accepting); - virtual std::string link_decl(const const_tgba_ptr& 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_ptr 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/complementation.cc b/src/tgbatest/complementation.cc index 970d069a7..6f3174d6c 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -251,7 +251,7 @@ int main(int argc, char* argv[]) return_value = 1; if (auto run = res->accepting_run()) { - spot::dotty_reachable(std::cout, ec->automaton(), false); + spot::dotty_reachable(std::cout, ec->automaton()); spot::print_tgba_run(std::cout, ec->automaton(), run); } } diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc index a9d1d5eac..af91044f4 100644 --- a/src/tgbatest/emptchk.cc +++ b/src/tgbatest/emptchk.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -163,7 +163,7 @@ main(int argc, char** argv) if (auto run = res->accepting_run()) { auto ar = spot::tgba_run_to_tgba(a, run); - spot::dotty_reachable(std::cout, ar, false); + spot::dotty_reachable(std::cout, ar); } std::cout << '\n'; if (runs == 0) diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1f664a445..cc93bf250 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -48,7 +48,6 @@ #include "taalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/replayrun.hh" -#include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/safety.hh" #include "tgbaalgos/gtec/gtec.hh" @@ -248,8 +247,6 @@ syntax(char* prog) << std::endl << " -CR compute and replay an accepting run (implies -C)" << std::endl - << " -g graph the accepting run on the automaton (requires -e)" - << std::endl << " -G graph the accepting run seen as an automaton " << " (requires -e)" << std::endl << " -m try to reduce accepting runs, in a second pass" @@ -364,7 +361,6 @@ checked_main(int argc, char** argv) bool display_reduced_form = false; bool post_branching = false; bool fair_loop_approx = false; - bool graph_run_opt = false; bool graph_run_tgba_opt = false; bool opt_reduce = false; bool opt_minimize = false; @@ -531,11 +527,6 @@ checked_main(int argc, char** argv) { file_opt = true; } - else if (!strcmp(argv[formula_index], "-g")) - { - accepting_run = true; - graph_run_opt = true; - } else if (!strcmp(argv[formula_index], "-G")) { accepting_run = true; @@ -927,10 +918,10 @@ checked_main(int argc, char** argv) } } - if ((graph_run_opt || graph_run_tgba_opt) + if ((graph_run_tgba_opt) && (!echeck_inst || !expect_counter_example)) { - std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl; + std::cerr << argv[0] << ": error: -G requires -e." << std::endl; exit(1); } @@ -1531,7 +1522,7 @@ checked_main(int argc, char** argv) switch (output) { case 0: - spot::dotty_reachable(std::cout, a, assume_sba); + spot::dotty_reachable(std::cout, a); break; case 5: a->get_dict()->dump(std::cout); @@ -1702,7 +1693,7 @@ checked_main(int argc, char** argv) } else { - if (!graph_run_opt && !graph_run_tgba_opt) + if (!graph_run_tgba_opt) ec->print_stats(std::cout); if (expect_counter_example != !!res && (!expect_counter_example || ec->safe())) @@ -1753,17 +1744,10 @@ checked_main(int argc, char** argv) else { tm.start("printing accepting run"); - if (graph_run_opt) - { - spot::tgba_run_dotty_decorator deco(run); - spot::dotty_reachable(std::cout, a, - assume_sba, nullptr, - &deco); - } - else if (graph_run_tgba_opt) + if (graph_run_tgba_opt) { auto ar = spot::tgba_run_to_tgba(a, run); - spot::dotty_reachable(std::cout, ar, false); + spot::dotty_reachable(std::cout, ar); } else { diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index e59c6e34c..f33efb628 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -551,7 +551,7 @@ an identifier: aUb is an atomic proposition, unlike

diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index a364f8c0b..dc6f98835 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -285,14 +285,14 @@ However you may download the Warning: The following result assumes the input formula is stuttering insensitive.
') # Should the automaton be displayed as a SBA? @@ -627,7 +627,7 @@ if output_type == 'm': unbufprint('
') dont_run_dot = print_stats(automaton) unbufprint('
') - render_automaton(automaton, dont_run_dot, issba) + render_automaton(automaton, dont_run_dot) automaton = 0 finish() @@ -685,7 +685,6 @@ if prune_scc: or direct_simul or reverse_simul or iterated_simul)) - issba = False if wdba_minimize: minimized = spot.minimize_obligation(automaton, f) @@ -693,20 +692,16 @@ if wdba_minimize: automaton = minimized minimized = 0 degen = False # No need to degeneralize anymore - issba = True direct_simul = False # No need to simulate anymore reverse_simul = False iterated_simul = False if direct_simul and not iterated_simul: automaton = spot.simulation(automaton) - issba = False if reverse_simul and not iterated_simul: automaton = spot.cosimulation(automaton) - issba = False if iterated_simul: automaton = spot.iterated_simulations(automaton) - issba = False if prune_scc and (direct_simul or reverse_simul): # Make a second pass after the simulation, since these might leave @@ -715,7 +710,6 @@ if prune_scc and (direct_simul or reverse_simul): if degen or neverclaim: degen = spot.degeneralize(automaton) - issba = True else: degen = automaton @@ -728,7 +722,7 @@ if output_type == 'a': del s else: # 't' or 's' dont_run_dot = print_stats(degen, True) - render_automaton(degen, dont_run_dot, issba) + render_automaton(degen, dont_run_dot) degen = 0 automaton = 0 finish() @@ -750,14 +744,13 @@ if output_type == 't': tautomaton = spot.tgba_to_tgta(degen, propset) if bisimulation: tautomaton = spot.minimize_tgta(tautomaton) - issba = False else: tautomaton = spot.tgba_to_ta(degen, propset, - issba, True, singlepass, livelock) + True, True, singlepass, livelock) if bisimulation: tautomaton = spot.minimize_ta(tautomaton) dont_run_dot = print_stats(tautomaton, ta = True) - render_automaton(tautomaton, dont_run_dot, issba) + render_automaton(tautomaton, dont_run_dot) tautomaton = 0 degen = 0 automaton = 0 @@ -767,14 +760,13 @@ if output_type == 't': if output_type == 'r': print_acc_run = False - draw_acc_run = False s = form.getfirst('rf', 'd') + draw_acc_run = False if s == 'p': print_acc_run = True elif s == 'd': draw_acc_run = True - err = "" opt = (form.getfirst('ec', 'Cou99') + "(" + form.getfirst('eo', '') + ")") @@ -823,12 +815,8 @@ if output_type == 'r': unbufprint('
%s
' % cgi.escape(s.str())) del s - if draw_acc_run: - deco = spot.tgba_run_dotty_decorator(ec_run) - dont_run_dot = print_stats(ec_a) - render_automaton(ec_a, dont_run_dot, issba, deco) - del deco + render_automaton(spot.tgba_run_to_tgba(ec_a, ec_run), False) del ec_run del ec_res unbufprint('
') diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 094b746fe..b7860451e 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -110,7 +110,6 @@ namespace std { #include "tgba/taatgba.hh" #include "tgba/tgbaproduct.hh" -#include "tgbaalgos/dottydec.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/degen.hh" #include "tgbaalgos/dupexp.hh" @@ -123,7 +122,6 @@ namespace std { #include "tgbaalgos/magic.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/safety.hh" #include "tgbaalgos/sccfilter.hh" @@ -244,7 +242,6 @@ namespace spot { %include "ltlvisit/apcollect.hh" %include "tgbaalgos/degen.hh" -%include "tgbaalgos/dottydec.hh" %include "tgbaalgos/dotty.hh" %include "tgbaalgos/dupexp.hh" %include "tgbaalgos/emptiness.hh" @@ -256,7 +253,6 @@ namespace spot { %include "tgbaalgos/magic.hh" %include "tgbaalgos/minimize.hh" %include "tgbaalgos/neverclaim.hh" -%include "tgbaalgos/rundotdec.hh" %include "tgbaalgos/save.hh" %include "tgbaalgos/safety.hh" %include "tgbaalgos/sccfilter.hh"