tut22.org 1.81 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
#+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);

23
24
    // Since a BDD is associated to every atomic proposition, the
    // register_ap() function returns a BDD variable number
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
25
    // that can be converted into a BDD using bdd_ithvar().
26
27
    bdd p1 = bdd_ithvar(aut->register_ap("p1"));
    bdd p2 = bdd_ithvar(aut->register_ap("p2"));
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

    // 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