tut22.org 2.36 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
23
24
25
26
27
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
69
70
71
72
73
74
75
76
#+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