From 89592881c7f9df031b019ec8a7fcaf2b38b77301 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 12 Jun 2015 21:59:00 +0200
Subject: [PATCH] org: new example

Fixes #14.

* doc/org/tut22.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
---
 doc/Makefile.am   |  1 +
 doc/org/tut.org   |  1 +
 doc/org/tut22.org | 75 +++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 77 insertions(+)
 create mode 100644 doc/org/tut22.org

diff --git a/doc/Makefile.am b/doc/Makefile.am
index 2edd9150f..9ccfd919f 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -86,6 +86,7 @@ ORG_FILES = \
   org/tut10.org \
   org/tut20.org \
   org/tut21.org \
+  org/tut22.org \
   org/satmin.org \
   org/satmin.tex \
   org/setup.org \
diff --git a/doc/org/tut.org b/doc/org/tut.org
index 93d33b009..64cbee878 100644
--- a/doc/org/tut.org
+++ b/doc/org/tut.org
@@ -24,3 +24,4 @@ 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]]
+- [[file:tut22.org][Creating an automaton in C++]]
diff --git a/doc/org/tut22.org b/doc/org/tut22.org
new file mode 100644
index 000000000..573df4222
--- /dev/null
+++ b/doc/org/tut22.org
@@ -0,0 +1,75 @@
+#+TITLE: Creating an automaton in C++
+#+SETUPFILE: setup.org
+#+HTML_LINK_UP: tut.html
+
+This example demonstrates how to create an automaton in C++, and then print it.
+The interface
+
+#+BEGIN_SRC C++ :results verbatim :exports both
+  #include <iostream>
+  #include "twaalgos/hoa.hh"
+  #include "twa/twagraph.hh"
+
+  int main(void)
+  {
+    // The dict is used to maintain the correspondence between the
+    // atomic propositions and the BDD variables to label the edges of
+    // the automaton.
+    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
+    // This creates an empty automaton that we have yet to fill.
+    spot::twa_graph_ptr aut = make_twa_graph(dict);
+
+    // The current way to associate a BDD to an atomic proposition is
+    // not really nice, and should be improved in the future.  Currently
+    // the string first have to be converted into (LTL) formulas...
+    spot::ltl::environment& e = spot::ltl::default_environment::instance();
+    const spot::ltl::formula* f1 = e.require("p1");
+    const spot::ltl::formula* f2 = e.require("p2");
+    // ...and then those formula can be registered to the BDD dict.  The
+    // BDD dict wants to keep track of which automaton uses which BDD
+    // variable, so we supply that pointer to aut.  The
+    // register_proposition() function returns a BDD variable number
+    // that can be converted into a BDD using bdd_ithvar().
+    bdd p1 = bdd_ithvar(dict->register_proposition(f1, aut));
+    bdd p2 = bdd_ithvar(dict->register_proposition(f2, aut));
+
+    // Set the acceptance condition of the automaton to Inf(0)&Inf(1)
+    aut->set_generalized_buchi(2);
+
+    // States are numbered from 0.
+    aut->new_states(3);
+
+    // new_edge() takes 3 mandatory parameters:
+    // source state, destination state, label
+    // and a last optional parameter can be used
+    // to specify membership to acceptance sets.
+    aut->new_edge(0, 1, p1);
+    aut->new_edge(1, 1, p1 & p2, {0});
+    aut->new_edge(1, 2, p2, {1});
+    aut->new_edge(2, 1, p1 | p2, {0, 1});
+
+    // Print the resulting automaton.
+    print_hoa(std::cout, aut);
+    return 0;
+  }
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p1" "p2"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 1
+State: 1
+[0&1] 1 {0}
+[1] 2 {1}
+State: 2
+[0 | 1] 1 {0 1}
+--END--
+#+end_example