alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

remove twa::transition_annotation

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-15 10:27:37 +01:00
parent e1f5eb1fd6
commit 39b95474f8
10 changed files with 17 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -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

5
spot/kripke/fairkripke.hh
View file

@ -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.

5
spot/kripke/kripke.hh
View file

@ -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

10
spot/twa/twa.cc
View file

@ -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
{

18
spot/twa/twa.hh
View file

@ -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

15
spot/twa/twaproduct.cc
View file

@ -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<const twa_succ_iterator_product_common*>(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

7
spot/twa/twaproduct.hh
View file

@ -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;

23
spot/twaalgos/emptiness.cc
View file

@ -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);

4
spot/twaalgos/emptiness.hh
View file

@ -302,9 +302,7 @@ namespace spot
///
/// This is similar to <code>os << run;</code>, 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

8
tests/ltsmin/finite.test
View file

@ -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