Commit 89592881 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: new example

Fixes #14.

* doc/org/tut22.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
parent 562a8d0f
......@@ -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 \
......
......@@ -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++]]
#+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
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