1# -*- coding: utf-8 -*- 2#+TITLE: The bdd_dict interface (advanced topic) 3#+DESCRIPTION: Description of the bdd_dict interface. 4#+INCLUDE: setup.org 5#+HTML_LINK_UP: tut.html 6#+PROPERTY: header-args:C+++ :results verbatim :exports both 7#+PROPERTY: header-args:python :results output :exports both 8 9Spot uses BDD for multiple purposes. 10 11The most common one is for labeling edges of automata: each edge 12stores a BDD representing its guard (i.e., a Boolean function over 13atomic propositions). Note that the automaton is still represented as 14a graph (with a [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][vector of states and a vector of edges]]) and the BDD is 15only used for the guard. This differs from symbolic representations 16where the entire transition structure is represented as one large BDD. 17 18There are other algorithms where BDDs are used from different tasks. 19For instance, our simulation-based reduction function computes a 20*signature* of each state as a BDD that is essentially the disjunction 21of all outgoing edges, represented by their guard, their acceptance 22sets, and their destination *classes*. Also the translation of LTL 23formulas to transition-based generalized Büchi automata is using an 24intermediate representation of states that is similar to the 25aforementioned signatures, excepts that classes are replaced by 26subformulas. 27 28From the point of view of the BDD library, BDDs are just DAGs with 29nodes labeled by BDD variables (numbered from 0). From the point of 30view of Spot's algorithm, these BDD variables have a meaning. For 31instance if we want to synchronize two automata that have guards over 32the atomic propositions $a$ and $b$, we need to make sure that both 33automata agree on the BDD variables used to represent $a$ and $b$. 34 35* The purpose of =bdd_dict= 36 37The =spot::bdd_dict= object is in charge of allocating BDD variables, 38and ensuring that multiple users reuse the same variables for similar 39purpose. When a =twa_graph= automaton is constructed, it takes a 40=bdd_dict= as argument. Every time an atomic proposition is 41registered through the =twa::register_ap()= method, the =bdd_dict= 42is queried. 43 44As an example, the following two automata share their =bdd_dict=, and 45although they do not declare their atomic propositions in the same 46order, they get compatible variable numbers. 47 48#+BEGIN_SRC C++ 49 #include <spot/twa/twagraph.hh> 50 51 int main() 52 { 53 spot::bdd_dict_ptr dict = spot::make_bdd_dict(); 54 spot::twa_graph_ptr aut1 = spot::make_twa_graph(dict); 55 int ap1a = aut1->register_ap("a"); 56 int ap1b = aut1->register_ap("b"); 57 std::cout << "aut1: a=" << ap1a << " b=" << ap1b << '\n'; 58 59 spot::twa_graph_ptr aut2 = spot::make_twa_graph(dict); 60 int ap2c = aut2->register_ap("c"); 61 int ap2b = aut2->register_ap("b"); 62 int ap2a = aut2->register_ap("a"); 63 std::cout << "aut2: a=" << ap2a << " b=" << ap2b << " c=" << ap2c << '\n'; 64 } 65#+END_SRC 66 67#+RESULTS: 68: aut1: a=0 b=1 69: aut2: a=0 b=1 b=2 70 71Contrast the above result with the following example, where the two 72automata use different =bdd_dict=: 73 74 75#+BEGIN_SRC C++ 76 #include <spot/twa/twagraph.hh> 77 78 int main() 79 { 80 spot::bdd_dict_ptr dict1 = spot::make_bdd_dict(); 81 spot::twa_graph_ptr aut1 = spot::make_twa_graph(dict1); 82 int ap1a = aut1->register_ap("a"); 83 int ap1b = aut1->register_ap("b"); 84 std::cout << "aut1: a=" << ap1a << " b=" << ap1b << '\n'; 85 86 spot::bdd_dict_ptr dict2 = spot::make_bdd_dict(); 87 spot::twa_graph_ptr aut2 = spot::make_twa_graph(dict2); 88 int ap2c = aut2->register_ap("c"); 89 int ap2b = aut2->register_ap("b"); 90 int ap2a = aut2->register_ap("a"); 91 std::cout << "aut2: a=" << ap2a << " b=" << ap2b << " c=" << ap2c << '\n'; 92 } 93#+END_SRC 94 95#+RESULTS: 96: aut1: a=0 b=1 97: aut2: a=2 b=1 c=0 98 99For this reason, operations like ~spot::product(aut1, aut2)~ will 100require that ~aut1->get_dict() == aut2->get_dict()~. 101 102 103In Python, many functions that would take an explicit =bdd_dict= in C++ will 104default to some global =bdd_dict= instead. So we can do: 105 106#+BEGIN_SRC python 107import spot 108aut1 = spot.make_twa_graph() 109ap1a = aut1.register_ap("a") 110ap1b = aut1.register_ap("b") 111print("aut1: a={} b={}".format(ap1a, ap1b)) 112aut2 = spot.make_twa_graph() 113ap2c = aut2.register_ap("c") 114ap2b = aut2.register_ap("b") 115ap2a = aut2.register_ap("a") 116print("aut1: a={} b={} c={}".format(ap2a, ap2b, ap2c)) 117#+END_SRC 118 119#+RESULTS: 120: aut1: a=0 b=1 121: aut1: a=0 b=1 c=2 122 123In that case we did not mention any =bdd_dict=, but there is one that 124is implicitly used in both cases. Similarly, when we call 125=spot.translate()= the same global =bdd_dict= is used by default. 126 127What really confuses people, is that the association between an atomic 128proposition (=a=, =b=, ...) and a BDD variable (=0=, =1=, ...) will 129only be held by the =bdd_dict= for the lifetime of the objects (here the 130automata) that registered this association to the =bdd_dict=. 131 132Here is a new C++ example where we use the =bdd_dict::dump()= method 133to display the contents of the =bdd_dict= (this method is only meant 134for debugging, please do not rely on its output). 135 136#+BEGIN_SRC C++ 137 #include <spot/twa/twagraph.hh> 138 139 int main() 140 { 141 spot::bdd_dict_ptr dict = spot::make_bdd_dict(); 142 143 spot::twa_graph_ptr aut1 = spot::make_twa_graph(dict); 144 int ap1a = aut1->register_ap("a"); 145 int ap1b = aut1->register_ap("b"); 146 std::cout << "aut1@" << aut1 << ": a=" << ap1a << " b=" << ap1b << '\n'; 147 dict->dump(std::cout) << "---\n"; 148 149 spot::twa_graph_ptr aut2 = spot::make_twa_graph(dict); 150 int ap2c = aut2->register_ap("c"); 151 int ap2b = aut2->register_ap("b"); 152 std::cout << "aut2@" << aut2 << ": b=" << ap2b << " c=" << ap2c << '\n'; 153 dict->dump(std::cout) << "---\n"; 154 155 aut1 = nullptr; 156 std::cout << "aut1 destroyed\n"; 157 dict->dump(std::cout) << "---\n"; 158 159 aut2 = nullptr; 160 std::cout << "aut2 destroyed\n"; 161 dict->dump(std::cout); 162 } 163#+END_SRC 164 165#+RESULTS: 166#+begin_example 167aut1@0x55bff3d24340: a=0 b=1 168Variable Map: 169 0 Var[a] x1 { 0x55bff3d24340 } 170 1 Var[b] x1 { 0x55bff3d24340 } 171Anonymous lists: 172 [0] 173Free list: 174 175--- 176aut2@0x55bff3d258d0: b=1 c=2 177Variable Map: 178 0 Var[a] x1 { 0x55bff3d24340 } 179 1 Var[b] x2 { 0x55bff3d24340 0x55bff3d258d0 } 180 2 Var[c] x1 { 0x55bff3d258d0 } 181Anonymous lists: 182 [0] 183Free list: 184 185--- 186aut1 destroyed 187Variable Map: 188 0 Free 189 1 Var[b] x1 { 0x55bff3d258d0 } 190 2 Var[c] x1 { 0x55bff3d258d0 } 191Anonymous lists: 192 [0] 193Free list: 194 (0, 1) 195--- 196aut2 destroyed 197Variable Map: 198 0 Free 199 1 Free 200 2 Free 201Anonymous lists: 202 [0] 203Free list: 204 (0, 3) 205#+end_example 206 207For each BDD variable registered to the =bdd_dict=, we have one line 208that gives: the variable number, its meaning (e.g. =Var[b]=), its 209registration count (=x2=), and a list of pointers to the objects that 210registered the association. 211 212Every time =twa::register_ap()= is called, it calls a similar function 213in the =bdd_dict= to check for an existing association or register a 214new one. When =aut1= is deleted, it unregisters all its variables, 215causing variable =0= to become free. The free list is actually a list 216of pairs representing ranges of free variables that can be reassigned 217by the BDD dict when needed. (The *anonymous list* serves when 218[[#anonymous][*anonymous BDD variables*]] are used.) 219 220Such a low-level registration is usually handled by the following 221interface: 222 223#+BEGIN_SRC C++ :exports code 224 // return a BDD variable number for f 225 int bdd_dict::register_proposition(formula f, const void* for_me); 226 // release the BDD variable 227 void bdd_dict::unregister_variable(int var, const void* me); 228 // release all BDD variables registered by me 229 void bdd_dict::unregister_all_my_variables(const void* me); 230 // register the same variables as another object 231 void bdd_dict::register_all_variables_of(const void* from_other, 232 const void* for_me); 233#+END_SRC 234 235The last function may be bit tricky to use, because we need to be sure 236that another object has registered some variables. You can rely on 237the fact that each =twa= automaton register its variables this way. 238 239Now, in most cases, there is no need to worry about the =bdd_dict=. 240Automata will register and unregister variables as needed. Other 241objects like =spot::twa_word= will do the same. 242 243There are at least two situations where one may need to deal with the 244=bdd_dict=: 2451. One case is when [[#ap][creating a derived object that store some BDD 246 representing a formula over atomic proposition]] (but without 247 reference to their original automaton). 2482. Another case is when [[#anonymous][more BDD variables (maybe 249 unrelated to atomic propositions) are needed]]. 250 251These two cases are discussed in the next sections. 252 253* Prolonging the association between a BDD variable and an atomic proposition 254 :PROPERTIES: 255 :CUSTOM_ID: ap 256 :END: 257 258Let us implement an object representing a set of transitions of the 259form $(src, guard, dest)$. This can for instance be used to store 260all transition that belong to a certain acceptance set. 261 262#+NAME: trans_set 263#+begin_src python :export code 264 import spot 265 266 class trans_set: 267 def __init__(self, dict): 268 self.set = set() 269 self.dict = dict 270 def add_trans(self, src, guard, dst): 271 self.set.add((src, guard, dst)) 272 def str_trans(self, src, guard, dst): 273 f = spot.bdd_format_formula(self.dict, guard) 274 return "({},{},{})".format(src, f, dst) 275 def __str__(self): 276 return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' 277 278 def accepting_set(aut, num): 279 ts = trans_set(aut.get_dict()) 280 for e in aut.edges(): 281 if e.acc.has(num): 282 ts.add_trans(e.src, e.cond, e.dst) 283 return ts 284#+end_src 285 286The above code has two definitions. 2871. The =trans_set= class is a set of transitions that can be printed. 288 It stores a =bdd_dict= so that it can print the guard of the 289 transition. 2902. The =accepting_set= function iterates over an automaton, and saves 291 all transitions that belong to a given acceptance set number. 292 293For instance we can now translate an automaton, compute its acceptance 294set 0, and print it as follows: 295 296#+begin_src python :noweb strip-export 297 <<trans_set>> 298 aut = spot.translate('GF(a <-> XXa)') 299 ts = accepting_set(aut, 0) 300 print(ts) 301#+end_src 302#+RESULTS: 303: {(0,a,3),(1,a,1),(2,!a,2),(3,!a,0)} 304 305The code of =trans_set= is in fact bogus. The problem is that it 306assumes the association between the atomic propositions and the BDD 307variable is still available when the =str_trans= method is called. 308However, that might not be the case. 309 310The following call sequence demonstrates the problem: 311 312#+begin_src python :noweb strip-export 313 <<trans_set>> 314 try: 315 ts = accepting_set(spot.translate('GF(a <-> XXa)'), 0) 316 print(ts) 317 except RuntimeError as e: 318 print("ERROR:", e) 319#+end_src 320 321#+RESULTS: 322: ERROR: bdd_to_formula() was passed a bdd with a variable that is not in the dictionary 323 324In this case, the temporary automaton constructed by 325=spot.translate()= and passed to the =accepting_set()= function is 326destroyed right after the =ts= object has been constructed. When the 327automaton is destroyed, it removes all its associations from the 328=bdd_dict=. This means that before the =print(ts)= the dictionary 329that was used by the automaton, and that is still stored in the =ts= 330objects is now empty: calling =bdd_format_formula()= raises an 331exception. 332 333This can be fixed in a couple of ways. The easy way is to store the 334automaton inside the =trans_set= object, to ensure that it will live 335at least as long as the =trans_set= object. But maybe the automaton 336is too big and we really want to get rid of it? In this case 337=trans_set= should tell the =bdd_dict= that it want to retain the 338associations. The easiest way in this case is to call the 339=register_all_variables_of()= method, because we know that each 340automaton registers its variables. 341 342#+begin_src python 343 import spot 344 345 class trans_set: 346 def __init__(self, aut): 347 self.set = set() 348 self.dict = aut.get_dict() 349 self.dict.register_all_variables_of(aut, self) 350 def __del__(self): 351 self.dict.unregister_all_my_variables(self) 352 def add_trans(self, src, guard, dest): 353 self.set.add((src, guard, dest)) 354 def str_trans(self, src, guard, dest): 355 f = spot.bdd_format_formula(self.dict, guard) 356 return "({},{},{})".format(src, f, dest) 357 def __str__(self): 358 return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' 359 360 def accepting_set(aut, num): 361 ts = trans_set(aut) 362 for e in aut.edges(): 363 if e.acc.has(num): 364 ts.add_trans(e.src, e.cond, e.dst) 365 return ts 366 367 try: 368 ts = accepting_set(spot.translate('GF(a <-> XXa)'), 0) 369 print(ts) 370 except RuntimeError as e: 371 print("ERROR:", e) 372#+end_src 373 374#+RESULTS: 375: {(0,a,3),(1,a,1),(2,!a,2),(3,!a,0)} 376 377Notice that we have also added a destructor to =trans_set= to 378unregister all the variables. 379 380 381* Anonymous BDD variables 382 :PROPERTIES: 383 :CUSTOM_ID: anonymous 384 :END: 385 386Another scenario where working with a =bdd_dict= is needed is when one 387needs to allocate *anonymous BDD variables*. These are variables that 388are not attached to any atomic proposition, and that can be used by 389one algorithm privately. If multiple algorithms (or objects) register 390anonymous variables, the =bdd_dict= will reuse anonymous variables 391allocated to other algorithms. One can allocate multiple anonymous 392variables with the following =bdd_dict= method: 393 394#+begin_src c++ :export code 395int bdd_dict::register_anonymous_variables(int n, const void* for_me); 396#+end_src 397 398A range of =n= variables will be allocated starting at the returned 399index. 400 401For instance, let's say the our =trans_set= should now store a 402symbolic representation of a transition relation. For simplicity we 403assume we just want to store set of pairs =(src,dst)=: each pair will 404be a conjunction $v_{src}\land v'_{dst}$ between two BDD variables 405taken from two ranges ($v_i$ representing a source state $i$ and $v'i$ 406representing a destination state $i$), and the entire set will be a 407disjunction of all these pairs. If the automaton has $n$ states, we 408want to allocate $2n$ BDD variables for this purpose. We call these 409variables *anonymous* because their meaning is unknown the the 410=bdd_dict=. 411 412#+begin_src python 413 import spot 414 from buddy import * 415 416 class trans_set: 417 def __init__(self, aut): 418 self.dict = d = aut.get_dict() 419 self.num_states = n = aut.num_states() 420 self.anonbase = b = d.register_anonymous_variables(2*n, self) 421 s = bddfalse 422 for e in aut.edges(): 423 s |= self.src(e.src) & self.dst(e.dst) 424 self.rel = s 425 def src(self, n): 426 return bdd_ithvar(self.anonbase + n) 427 def dst(self, n): 428 return bdd_ithvar(self.anonbase + n + self.num_states) 429 def __del__(self): 430 self.dict.unregister_all_my_variables(self) 431 def __str__(self): 432 isop = spot.minato_isop(self.rel) 433 i = isop.next() 434 res = [] 435 while i != bddfalse: 436 s = bdd_var(i) - self.anonbase 437 d = bdd_var(bdd_high(i)) - self.anonbase - self.num_states 438 res.append((s, d)) 439 i = isop.next() 440 return str(res) 441 442 ts = trans_set(spot.translate('GF(a <-> XXa)')) 443 print(ts) 444#+end_src 445 446#+RESULTS: 447: [(0, 2), (0, 3), (1, 0), (1, 1), (2, 2), (2, 3), (3, 0), (3, 1)] 448 449# LocalWords: utf bdd html args BDDs DAGs twa SRC aut ap bff src 450# LocalWords: unregisters unregister dest init dst str num cond GF 451# LocalWords: noweb XXa RuntimeError del v'i anonbase bddfalse isop 452# LocalWords: ithvar 453