From 4d848e988ce27809169ddaa1e8c1f2b7993c130e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Jun 2015 00:28:53 +0200 Subject: [PATCH] org: new example * doc/org/tut21.org: New file. * doc/Makefile.am, doc/org/tut.org: Add it. --- doc/Makefile.am | 1 + doc/org/tut.org | 7 ++ doc/org/tut21.org | 160 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 168 insertions(+) create mode 100644 doc/org/tut21.org diff --git a/doc/Makefile.am b/doc/Makefile.am index a0bee2a96..2edd9150f 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -85,6 +85,7 @@ ORG_FILES = \ org/tut02.org \ org/tut10.org \ org/tut20.org \ + org/tut21.org \ org/satmin.org \ org/satmin.tex \ org/setup.org \ diff --git a/doc/org/tut.org b/doc/org/tut.org index 23e01556a..93d33b009 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -17,3 +17,10 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut02.org][Relabeling Formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] - [[file:tut20.org][Converting a never claim into HOA]] + +* Examples in C++ only + +The following examples are too low-level to be implemented in shell or +Python (at least at the moment), so they are purely C++ so far. + +- [[file:tut21.org][Custom print of an automaton]] diff --git a/doc/org/tut21.org b/doc/org/tut21.org new file mode 100644 index 000000000..9364afdff --- /dev/null +++ b/doc/org/tut21.org @@ -0,0 +1,160 @@ +#+TITLE: Custom print of an automaton +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +This example demonstrates how to iterate over an automaton. We will +only show how to do this in C++: the Python bindings for the automata +are not yet supporting these low-level iterations, and the shell +commands aren't up to the task either. + +First let's create an example automaton in HOA format. + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba 'Fa | G(Fb&Fc)' -H | tee tut21.hoa +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +name: "Fa | G(Fb & Fc)" +States: 4 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc complete +properties: stutter-invariant +--BODY-- +State: 0 +[0] 1 +[!0] 2 +[!0] 3 +State: 1 +[t] 1 {0 1} +State: 2 +[0] 1 +[!0] 2 +State: 3 +[1&2] 3 {0 1} +[1&!2] 3 {0} +[!1&2] 3 {1} +[!1&!2] 3 +--END-- +#+end_example + +We now write some C++ to load this automaton [[file:tut20.org][as we did before]], and in +=custom_print()= we print it out in a custom way by explicitly +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. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include "parseaut/public.hh" + #include "twaalgos/hoa.hh" + #include "twa/bddprint.hh" + + void custom_print(std::ostream& out, spot::twa_graph_ptr& aut); + + int main() + { + std::string input = "tut21.hoa"; + spot::parse_aut_error_list pel; + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::parsed_aut_ptr pa = parse_aut(input, pel, dict); + if (spot::format_parse_aut_errors(std::cerr, input, pel)) + return 1; + // This cannot occur when reading a never claim, but + // it could while reading a HOA file. + if (pa->aborted) + { + std::cerr << "--ABORT-- read\n"; + return 1; + } + custom_print(std::cout, pa->aut); + return 0; + } + + void custom_print(std::ostream& out, spot::twa_graph_ptr& aut) + { + // 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'; + + // We need the dictionary to print the BDD that labels the edge + const auto& dict = aut->get_dict(); + + // States are numbered from 0 to n-1 + unsigned n = aut->num_states(); + for (unsigned s = 0; s < n; ++s) + { + out << "State " << s << ":\n"; + + // The out(s) method returns a fake container that can be + // iterated over as if the contents was the edges going + // out of s. Each of these edge is a quadruplet + // (src,dst,cond,acc). Note that because this returns + // a reference, the edge can also be modified. + for (auto& t: aut->out(s)) + { + out << " edge(" << t.src << " -> " << t.dst << ")\n label = "; + spot::bdd_print_formula(out, dict, t.cond); + out << "\n acc sets = " << t.acc << '\n'; + } + } + } +#+END_SRC + +#+RESULTS: +#+begin_example +Acceptance: Inf(0)&Inf(1) +Number of sets: 2 +Number of states: 4 +Number of edges: 10 +State 0: + edge(0 -> 1) + label = a + acc sets = {} + edge(0 -> 2) + label = !a + acc sets = {} + edge(0 -> 3) + label = !a + acc sets = {} +State 1: + edge(1 -> 1) + label = 1 + acc sets = {0,1} +State 2: + edge(2 -> 1) + label = a + acc sets = {} + edge(2 -> 2) + label = !a + acc sets = {} +State 3: + edge(3 -> 3) + label = b & c + acc sets = {0,1} + edge(3 -> 3) + label = b & !c + acc sets = {0} + edge(3 -> 3) + label = !b & c + acc sets = {1} + edge(3 -> 3) + label = !b & !c + acc sets = {} +#+end_example + + +#+BEGIN_SRC sh :results verbatim :exports none +rm -f tut21.hoa +#+END_SRC