Commit 3010d705 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Display transition annotations in dotty output.

* src/tgbaalgos/dotty.cc (process_link): Call
transition_annotation().  Reported by Nikos Gorogiannis.
* src/tgba/tgba.hh (transition_annotation): More documentation.
parent d573eb9b
2011-11-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Display transition annotations in dotty output.
* src/tgbaalgos/dotty.cc (process_link): Call
transition_annotation(). Reported by Nikos Gorogiannis.
* src/tgba/tgba.hh (transition_annotation): More documentation.
* NEWS: Mention this change.
2011-11-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Add an entry for the previous fix.
......
......@@ -16,6 +16,9 @@ New in spot 0.7.1a:
In that case, acceptance states are displayed with a double
circle. ltl2tgba (both command line and on-line) Use it to display
degeneralized automata.
- The dotty_reachable() function will also display transition
annotations (as returned by the tgba::transitition_annotation()).
This can be useful when displaying (small) state spaces.
- Identifiers used to name atomic proposition can contain dots.
E.g.: X.Y is now an atomic proposition, while it was understood
as X&Y in previous versions.
......
......@@ -157,10 +157,19 @@ namespace spot
/// \brief Return a possible annotation for the transition
/// pointed to by the iterator.
///
/// Implementing this function is optional; the default annotation
/// it the empty string.
/// 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).
///
/// \param t a non-done tgba_succ_iterator for this automata
/// Implementing this method is optional; the default annotation
/// is the empty string.
///
/// This method is used for instance in dotty_reachable(),
/// and replay_tgba_run().
///
/// \param t a non-done tgba_succ_iterator for this automaton
virtual std::string
transition_annotation(const tgba_succ_iterator* t) const;
......
......@@ -100,6 +100,14 @@ namespace spot
+ bdd_format_accset(automata_->get_dict(),
si->current_acceptance_conditions());
std::string s = automata_->transition_annotation(si);
if (!s.empty())
{
if (*label.rbegin() != '\n')
label += '\n';
label += s;
}
os_ << " " << in << " -> " << out << " "
<< dd_->link_decl(automata_, in_s, in, out_s, out, si,
escape_str(label))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment