tut23.org 4.94 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
# -*- coding: utf-8 -*-
#+TITLE: Creating an alternating automaton by adding states and transitions
#+DESCRIPTION: Code example for constructing alternating ω-automata in Spot
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html

This example demonstrates how to create the following alternating
co-Büchi automaton (recognizing =GFa=) and then print it.

#+NAME: tut23-dot
#+BEGIN_SRC sh :results verbatim :exports none :var txt=tut23-cpp
12
autfilt --dot <<EOF
13
14
15
16
$txt
EOF
#+END_SRC

17
#+BEGIN_SRC dot :file tut23-aut.svg :var txt=tut23-dot :exports results
18
19
20
21
$txt
#+END_SRC

#+RESULTS:
22
[[file:tut23-aut.svg]]
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174


Note that the code is very similar to the [[file:tut22.org][previous example]]: in Spot an
alternating automaton is just an automaton that uses a mix of standard
edges (declared with =new_edge()=) and universal edges (declared with
=new_univ_edge()=).

* C++
  :PROPERTIES:
  :CUSTOM_ID: cpp
  :END:

#+NAME: tut23-cpp
#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
  #include <iostream>
  #include <spot/twaalgos/hoa.hh>
  #include <spot/twa/twagraph.hh>

  int main(void)
  {
    // The bdd_dict is used to maintain the correspondence between the
    // atomic propositions and the BDD variables that 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);

    // Since a BDD is associated to every atomic proposition, the
    // register_ap() function returns a BDD variable number that can be
    // converted into a BDD using bdd_ithvar().
    bdd a = bdd_ithvar(aut->register_ap("a"));

    // Set the acceptance condition of the automaton to co-Büchi
    aut->set_acceptance(1, "Fin(0)");

    // States are numbered from 0.
    aut->new_states(3);
    // The default initial state is 0, but it is always better to
    // specify it explicitely.
    aut->set_init_state(0U);

    // new_edge() takes 3 mandatory parameters: source state,
    // destination state, and label.  A last optional parameter can be
    // used to specify membership to acceptance sets.
    //
    // new_univ_edge() is similar, but the destination is a set of
    // states.
    aut->new_edge(0, 0, a);
    aut->new_univ_edge(0, {0, 1}, !a);
    aut->new_edge(1, 1, !a, {0});
    aut->new_edge(1, 2, a);
    aut->new_edge(2, 2, bddtrue);

    // Print the resulting automaton.
    print_hoa(std::cout, aut);
    return 0;
  }
#+END_SRC

#+RESULTS: tut23-cpp
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
#+END_SRC

* Python

#+BEGIN_SRC python :results output :exports both :wrap SRC hoa
  import spot
  import buddy

  # The bdd_dict is used to maintain the correspondence between the
  # atomic propositions and the BDD variables that label the edges of
  # the automaton.
  bdict = spot.make_bdd_dict();
  # This creates an empty automaton that we have yet to fill.
  aut = spot.make_twa_graph(bdict)

  # Since a BDD is associated to every atomic proposition, the register_ap()
  # function returns a BDD variable number that can be converted into a BDD
  # using bdd_ithvar() from the BuDDy library.
  a = buddy.bdd_ithvar(aut.register_ap("a"))

  # Set the acceptance condition of the automaton to co-Büchi
  aut.set_acceptance(1, "Fin(0)")

  # States are numbered from 0.
  aut.new_states(3)
  # The default initial state is 0, but it is always better to
  # specify it explicitely.
  aut.set_init_state(0);

  # new_edge() takes 3 mandatory parameters: source state, destination state,
  # and label.  A last optional parameter can be used to specify membership
  # to acceptance sets.  In the Python version, the list of acceptance sets
  # the transition belongs to should be specified as a list.
  #
  # new_univ_edge() is similar, but the destination is a list of states.
  aut.new_edge(0, 0, a);
  aut.new_univ_edge(0, [0, 1], -a);
  aut.new_edge(1, 1, -a, [0]);
  aut.new_edge(1, 2, a);
  aut.new_edge(2, 2, buddy.bddtrue);

  # Print the resulting automaton.
  print(aut.to_str('hoa'))
#+END_SRC

#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
#+END_SRC

* Additional comments

Alternating automata in Spot can also have a universal initial state:
e.g, an automaton may start in =0&1&2=.  Use =set_univ_init_state()=
to declare such as state.

175
We have a [[file:tut24.org][separate page]] describing how to explore the edges of an
176
177
178
alternating automaton.

Once you have built an alternating automaton, you can [[file:tut31.org][remove the
179
180
alternation]] to obtain a non-deterministic Büchi or generalized Büchi
automaton.