From 39b95474f83282954c4e7f3a81c0d6f794c14937 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Feb 2016 10:27:37 +0100 Subject: [PATCH] remove twa::transition_annotation Fixes #149. * spot/twa/twa.hh, spot/twa/twa.cc, spot/kripke/fairkripke.hh, spot/kripke/kripke.hh, spot/twa/twaproduct.cc, spot/twa/twaproduct.hh: Remove this method. * spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh, tests/ltsmin/finite.test: Adjust. * NEWS: Mention the removal. --- NEWS | 2 ++ spot/kripke/fairkripke.hh | 5 ++--- spot/kripke/kripke.hh | 5 ++--- spot/twa/twa.cc | 10 ++-------- spot/twa/twa.hh | 18 ------------------ spot/twa/twaproduct.cc | 15 --------------- spot/twa/twaproduct.hh | 7 ++----- spot/twaalgos/emptiness.cc | 23 ++--------------------- spot/twaalgos/emptiness.hh | 4 +--- tests/ltsmin/finite.test | 8 ++++---- 10 files changed, 17 insertions(+), 80 deletions(-) diff --git a/NEWS b/NEWS index 6a77bc885..62148aec3 100644 --- a/NEWS +++ b/NEWS @@ -82,6 +82,8 @@ New in spot 1.99.7a (not yet released) * The twa_safra_complement class has been removed. Use tgba_determinize() and dtwa_complement() instead. + * The twa::transition_annotation() method has been removed. + Python: * The ltsmin interface has been binded in Python. See diff --git a/spot/kripke/fairkripke.hh b/spot/kripke/fairkripke.hh index ad54faaa4..0542d6bea 100644 --- a/spot/kripke/fairkripke.hh +++ b/spot/kripke/fairkripke.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013, 2014, 2015 Laboratoire de Recherche et -// Developpement de l'Epita +// Copyright (C) 2009, 2010, 2013, 2014, 2015, 2016 Laboratoire de +// Recherche et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -79,7 +79,6 @@ namespace spot /// - kripke::state_condition() /// - kripke::state_acceptance_conditions() /// - kripke::format_state() - /// - and optionally kripke::transition_annotation() /// /// The other methods of the tgba interface are supplied by this /// class and need not be defined. diff --git a/spot/kripke/kripke.hh b/spot/kripke/kripke.hh index ae5391a1e..163e694b8 100644 --- a/spot/kripke/kripke.hh +++ b/spot/kripke/kripke.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita +// Copyright (C) 2009, 2010, 2013, 2014, 2016 Laboratoire de Recherche +// et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -81,7 +81,6 @@ namespace spot /// - kripke::succ_iter() /// - kripke::state_condition() /// - kripke::format_state() - /// - and optionally kripke::transition_annotation() /// /// The other methods of the tgba interface (like those dealing with /// acceptance conditions) are supplied by this kripke class and diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index cd34922c4..bcf3f85fa 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement de -// l'EPITA (LRDE). +// Copyright (C) 2011, 2014, 2015, 2016 Laboratoire de Recherche et +// Developpement de l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -69,12 +69,6 @@ namespace spot return nullptr; } - std::string - twa::transition_annotation(const twa_succ_iterator*) const - { - return ""; - } - bool twa::is_empty() const { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 1da7e3610..900bb0126 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -774,24 +774,6 @@ namespace spot /// data structure stored in the automaton. virtual std::string format_state(const state* s) const = 0; - /// \brief Return a possible annotation for the transition - /// pointed to by the iterator. - /// - /// You may decide to use annotations when building a tgba class - /// that represents the state space of a model, for instance to - /// indicate how the tgba transitions relate to the original model - /// (e.g. the annotation could be the name of a PetriNet - /// transition, or the line number of some textual formalism). - /// - /// Implementing this method is optional; the default annotation - /// is the empty string. - /// - /// This method is used for instance in replay_twa_run(). - /// - /// \param t a non-done twa_succ_iterator for this automaton - virtual std::string - transition_annotation(const twa_succ_iterator* t) const; - /// \brief Project a state on an automaton. /// /// This converts \a s, into that corresponding spot::state for \a diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index 657d3ba33..09df23a21 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -402,21 +402,6 @@ namespace spot return right_->project_state(s2->right(), t); } - std::string - twa_product::transition_annotation(const twa_succ_iterator* t) const - { - const twa_succ_iterator_product_common* i = - down_cast(t); - assert(i); - std::string left = left_->transition_annotation(i->left_); - std::string right = right_->transition_annotation(i->right_); - if (left == "") - return right; - if (right == "") - return left; - return "<" + left + ", " + right + ">"; - } - ////////////////////////////////////////////////////////////////////// // twa_product_init diff --git a/spot/twa/twaproduct.hh b/spot/twa/twaproduct.hh index 52591278d..6ec28040e 100644 --- a/spot/twa/twaproduct.hh +++ b/spot/twa/twaproduct.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -97,9 +97,6 @@ namespace spot virtual std::string format_state(const state* state) const; - virtual std::string - transition_annotation(const twa_succ_iterator* t) const; - virtual state* project_state(const state* s, const const_twa_ptr& t) const; const acc_cond& left_acc() const; diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 8e6b90e02..82b6599a9 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -434,20 +434,6 @@ namespace spot return res; } - namespace - { - static void - print_annotation(std::ostream& os, - const const_twa_ptr& a, - const twa_succ_iterator* i) - { - std::string s = a->transition_annotation(i); - if (s == "") - return; - os << ' ' << s; - } - } - bool twa_run::replay(std::ostream& os, bool debug) const { const state* s = aut->get_init_state(); @@ -579,9 +565,7 @@ namespace spot do { const state* s2 = j->dst(); - os << " *"; - print_annotation(os, aut, j); - os << " label=" + os << " * label=" << bdd_format_formula(aut->get_dict(), j->cond()) << " and acc=" @@ -598,9 +582,7 @@ namespace spot } if (debug) { - os << "transition"; - print_annotation(os, aut, j); - os << " with label=" + os << "transition with label=" << bdd_format_formula(aut->get_dict(), label) << " and acc=" << aut->acc().format(acc) << std::endl; @@ -608,7 +590,6 @@ namespace spot else { os << " | "; - print_annotation(os, aut, j); bdd_print_formula(os, aut->get_dict(), label); os << '\t'; aut->acc().format(acc); diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index a6f9ae193..0df56f129 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -302,9 +302,7 @@ namespace spot /// /// This is similar to os << run;, except that the /// run is actually replayed on the automaton while it is printed. - /// Doing so makes it possible to display transition annotations - /// (returned by spot::twa::transition_annotation()). The output - /// will stop if the run cannot be completed. + /// The output will stop if the run cannot be completed. /// /// \param os the stream on which the replay should be traced /// \param debug if set the output will be more verbose and extra diff --git a/tests/ltsmin/finite.test b/tests/ltsmin/finite.test index bede9bc0c..d9d1aee3e 100755 --- a/tests/ltsmin/finite.test +++ b/tests/ltsmin/finite.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -53,6 +53,6 @@ run 0 ../modelcheck -ddead -E $srcdir/finite.dve \ run 0 ../modelcheck -ddead -e $srcdir/finite.dve \ '!(G(dead -> ("P.a==2" | "P.b==3")))' -# This used to segfault because of a bug in -# twa_product::transition_annotation. +# This used to segfault because of a bug in a +# function that do not exist anymore. run 0 ../modelcheck -gp $srcdir/finite.dve true