Commit 84f9be9e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

doc: show more metadata about automata

* src/twa/bdddict.hh (varnum): New method.
* doc/org/tut21.org: Show more metadata.
parent 51a75a31
......@@ -48,10 +48,16 @@ We now write some C++ to load this automaton [[file:tut20.org][as we did before]
iterating over it states and edges.
The only tricky part is to print the edge labels. Since they are
BDDs, printing them directly would just show the number of BDD
variables involved. Using =bdd_print_formula= and passing it the BDD
dictionary associated to the automaton is the way to print the edge
labels.
BDDs, printing them directly would just show the identifiers of BDDs
involved. Using =bdd_print_formula= and passing it the BDD dictionary
associated to the automaton is one way to print the edge labels.
Each automaton stores a vector the atomic propositions it uses. You
can iterate on that vector using the =ap()= member function. If you
want to convert an atomic proposition (represented by a =formula=)
into a BDD, use the =bdd_dict::varnum()= method to obtain the
corresponding BDD variable number, and then use for instance
=bdd_ithvar()= to convert this BDD variable number into an actual BDD.
#+BEGIN_SRC C++ :results verbatim :exports both
#include <string>
......@@ -83,15 +89,30 @@ labels.
void custom_print(std::ostream& out, spot::twa_graph_ptr& aut)
{
// We need the dictionary to print the BDD that labels the edge
const auto& dict = aut->get_dict();
// Print some meta-data
out << "Acceptance: " << aut->get_acceptance() << '\n';
out << "Number of sets: " << aut->num_sets() << '\n';
out << "Number of states: " << aut->num_states() << '\n';
out << "Number of edges: " << aut->num_edges() << '\n';
out << "Initial state: " << aut->get_init_state_number() << '\n';
// We need the dictionary to print the BDD that labels the edge
const auto& dict = aut->get_dict();
out << "Atomic propositions:";
for (spot::formula ap: aut->ap())
out << ' ' << ap << " (=" << dict->varnum(ap) << ')';
out << '\n';
// For these methods, true means "it's sure", false means "I don't
// know". These properties correspond to bits stored in the
// automaton, so they can be queried in constant time, and they are
// only set whenever they can be determined at a cheap cost.
out << "Deterministic: "
<< (aut->is_deterministic() ? "yes\n" : "maybe\n");
out << "StateBasedAcc: "
<< (aut->has_state_based_acc() ? "yes\n" : "maybe\n");
out << "Stutter Invariant: "
<< (aut->is_stutter_invariant() ? "yes\n" :
aut->is_stutter_sensitive() ? "no\n" : "maybe\n");
// States are numbered from 0 to n-1
unsigned n = aut->num_states();
......@@ -121,6 +142,10 @@ Number of sets: 2
Number of states: 4
Number of edges: 10
Initial state: 0
Atomic propositions: a (=0) b (=1) c (=2)
Deterministic: maybe
StateBasedAcc: maybe
Stutter Invariant: yes
State 0:
edge(0 -> 1)
label = a
......
......@@ -123,6 +123,15 @@ namespace spot
}
/// @}
// \brief return the BDD variable associated to a registered
// proposition.
//
// Throws std::out_of_range if the \a is not a known proposition.
int varnum(formula f)
{
return var_map.at(f);
}
/// \brief Register an acceptance variable.
///
/// Return (and maybe allocate) a BDD variable designating an
......
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