From ad2f5524bb1da3b6162e67c4df6b8ca5293b4500 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jun 2019 20:56:39 +0200 Subject: [PATCH] doc: add tut90.org about bdd_dict Fixes #372. * doc/org/tut90.org: New file. * doc/Makefile.am, doc/org/tut.org: Add it. * NEWS: Mention it. * python/spot/__init__.py: Allow make_twa_graph with default bdd_dict. --- NEWS | 5 + doc/Makefile.am | 1 + doc/org/tut.org | 2 + doc/org/tut90.org | 447 ++++++++++++++++++++++++++++++++++++++++ python/spot/__init__.py | 6 + 5 files changed, 461 insertions(+) create mode 100644 doc/org/tut90.org diff --git a/NEWS b/NEWS index 46ad2a0d8..0fe750ac4 100644 --- a/NEWS +++ b/NEWS @@ -30,6 +30,11 @@ New in spot 2.7.5.dev (not yet released) amongst "Inf(0)", "t", or "f", and persistance properties have an acceptance condition among "Fin(0)", "t", or "f". + Documentation: + + - https://spot.lrde.epita.fr/tut90.html is a new file that explains + the purpose of the =spot::bdd_dict= object. + Library: - Add generic_accepting_run() as a variant of generic_emptiness_check() that diff --git a/doc/Makefile.am b/doc/Makefile.am index 79d437a28..1a295ed5d 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -115,6 +115,7 @@ ORG_FILES = \ org/tut50.org \ org/tut51.org \ org/tut52.org \ + org/tut90.org \ org/upgrade2.org \ org/satmin.org \ org/satmin.tex \ diff --git a/doc/org/tut.org b/doc/org/tut.org index d15063356..0ef6414bd 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -38,6 +38,8 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut23.org][Creating an alternating automaton by adding states and transitions]] - [[file:tut24.org][Iterating over alternating automata]] - [[file:tut52.org][Creating an explicit Kripke structure]] +- [[file:tut90.org][Using the =bdd_dict= to associate atomic proposition to BDD + variables, or allocate anonymous BDD variables (advanced)]] * Examples in C++ only diff --git a/doc/org/tut90.org b/doc/org/tut90.org new file mode 100644 index 000000000..963385b3a --- /dev/null +++ b/doc/org/tut90.org @@ -0,0 +1,447 @@ +# -*- coding: utf-8 -*- +#+TITLE: The bdd_dict interface (advanced topic) +#+DESCRIPTION: Description of the bdd_dict interface. +#+INCLUDE: setup.org +#+HTML_LINK_UP: tut.html +#+PROPERTY: header-args:C+++ :results verbatim :exports both +#+PROPERTY: header-args:python :results output :exports both + +Spot uses BDD for multiple purposes. + +The most common one is for labeling edges of automata: each edge +stores a BDD representing its guard (i.e., a Boolean function over +atomic propositions). Note that the automaton is still represented as +a graph (with a [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][vector of states and a vector of edges]]) and the BDD is +only used for the guard. This differs from symbolic representations +where the entire transition structure is represented as one large BDD. + +There are other algorithms where BDDs are used from different tasks. +For instance, our simulation-based reduction function computes a +*signature* of each state as a BDD that is essentially the disjunction +of all outgoing edges, represented by their guard, their acceptance +sets, and their destination *classes*. Also the translation of LTL +formulas to transition-based generalized Büchi automata is using an +intermediate representation of states that is similar to the +aforementioned signatures, excepts that classes are replaced by +subformulas. + +From the point of view of the BDD library, BDDs are just DAGs with +nodes labeled by BDD variables (numbered from 0). From the point of +view of Spot's algorithm, these BDD variables have a meaning. For +instance if we want to synchronize two automata that have guards over +the atomic propositions $a$ and $b$, we need to make sure that both +automata agree on the BDD variables used to represent $a$ and $b$. + +* The purpose of =bdd_dict= + +The =spot::bdd_dict= object is in charge of allocating BDD variables, +and ensuring that multiple users reuse the same variables for similar +purpose. When a =twa_graph= automaton is constructed, it takes a +=bdd_dict= as argument. Everytime an atomic proposition is +registered through the =twa::register_ap()= method, the =bdd_dict= +is queried. + +As an example, the following two automata share their =bdd_dict=, and +although they do not declare their atomic propositions in the same +order, they get compatible variable numbers. + +#+BEGIN_SRC C++ + #include + + int main() + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::twa_graph_ptr aut1 = spot::make_twa_graph(dict); + int ap1a = aut1->register_ap("a"); + int ap1b = aut1->register_ap("b"); + std::cout << "aut1: a=" << ap1a << " b=" << ap1b << '\n'; + + spot::twa_graph_ptr aut2 = spot::make_twa_graph(dict); + int ap2c = aut2->register_ap("c"); + int ap2b = aut2->register_ap("b"); + int ap2a = aut2->register_ap("a"); + std::cout << "aut2: a=" << ap2a << " b=" << ap2b << " c=" << ap2c << '\n'; + } +#+END_SRC + +#+RESULTS: +: aut1: a=0 b=1 +: aut2: a=0 b=1 b=2 + +Contrast the above result with the following example, where the two +automata use different =bdd_dict=: + + +#+BEGIN_SRC C++ + #include + + int main() + { + spot::bdd_dict_ptr dict1 = spot::make_bdd_dict(); + spot::twa_graph_ptr aut1 = spot::make_twa_graph(dict1); + int ap1a = aut1->register_ap("a"); + int ap1b = aut1->register_ap("b"); + std::cout << "aut1: a=" << ap1a << " b=" << ap1b << '\n'; + + spot::bdd_dict_ptr dict2 = spot::make_bdd_dict(); + spot::twa_graph_ptr aut2 = spot::make_twa_graph(dict2); + int ap2c = aut2->register_ap("c"); + int ap2b = aut2->register_ap("b"); + int ap2a = aut2->register_ap("a"); + std::cout << "aut2: a=" << ap2a << " b=" << ap2b << " c=" << ap2c << '\n'; + } +#+END_SRC + +#+RESULTS: +: aut1: a=0 b=1 +: aut2: a=2 b=1 c=0 + +For this reason, operations like ~spot::product(aut1, aut2)~ will +require that ~aut1->get_dict() == aut2->get_dict()~. + + +In Python, many functions that would take an explicit =bdd_dict= in C++ will +default to some global =bdd_dict= instead. So we can do: + +#+BEGIN_SRC python +import spot +aut1 = spot.make_twa_graph() +ap1a = aut1.register_ap("a") +ap1b = aut1.register_ap("b") +print("aut1: a={} b={}".format(ap1a, ap1b)) +aut2 = spot.make_twa_graph() +ap2c = aut2.register_ap("c") +ap2b = aut2.register_ap("b") +ap2a = aut2.register_ap("a") +print("aut1: a={} b={} c={}".format(ap2a, ap2b, ap2c)) +#+END_SRC + +#+RESULTS: +: aut1: a=0 b=1 +: aut1: a=0 b=1 c=2 + +In that case we did not mention any =bdd_dict=, but there is one that +is implicitly used in both cases. Similarly, when we call +=spot.translate()= the same global =bdd_dict= is used by default. + +What really confuses people, is that the association between an atomic +proposition (=a=, =b=, ...) and a BDD variable (=0=, =1=, ...) will +only be held by the =bdd_dict= for the lifetime of the objects (here the +automata) that registered this association to the =bdd_dict=. + +Here is a new C++ example where we use the =bdd_dict::dump()= method +to display the contents of the =bdd_dict= (this method is only meant +for debugging, please do not rely on its output). + +#+BEGIN_SRC C++ + #include + + int main() + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + + spot::twa_graph_ptr aut1 = spot::make_twa_graph(dict); + int ap1a = aut1->register_ap("a"); + int ap1b = aut1->register_ap("b"); + std::cout << "aut1@" << aut1 << ": a=" << ap1a << " b=" << ap1b << '\n'; + dict->dump(std::cout) << "---\n"; + + spot::twa_graph_ptr aut2 = spot::make_twa_graph(dict); + int ap2c = aut2->register_ap("c"); + int ap2b = aut2->register_ap("b"); + std::cout << "aut2@" << aut2 << ": b=" << ap2b << " c=" << ap2c << '\n'; + dict->dump(std::cout) << "---\n"; + + aut1 = nullptr; + std::cout << "aut1 destroyed\n"; + dict->dump(std::cout) << "---\n"; + + aut2 = nullptr; + std::cout << "aut2 destroyed\n"; + dict->dump(std::cout); + } +#+END_SRC + +#+RESULTS: +#+begin_example +aut1@0x55bff3d24340: a=0 b=1 +Variable Map: + 0 Var[a] x1 { 0x55bff3d24340 } + 1 Var[b] x1 { 0x55bff3d24340 } +Anonymous lists: + [0] +Free list: + +--- +aut2@0x55bff3d258d0: b=1 c=2 +Variable Map: + 0 Var[a] x1 { 0x55bff3d24340 } + 1 Var[b] x2 { 0x55bff3d24340 0x55bff3d258d0 } + 2 Var[c] x1 { 0x55bff3d258d0 } +Anonymous lists: + [0] +Free list: + +--- +aut1 destroyed +Variable Map: + 0 Free + 1 Var[b] x1 { 0x55bff3d258d0 } + 2 Var[c] x1 { 0x55bff3d258d0 } +Anonymous lists: + [0] +Free list: + (0, 1) +--- +aut2 destroyed +Variable Map: + 0 Free + 1 Free + 2 Free +Anonymous lists: + [0] +Free list: + (0, 3) +#+end_example + +For each BDD variable registered to the =bdd_dict=, we have one line +that gives: the variable number, its meaning (e.g. =Var[b]=), its +registration count (=x2=), and a list of pointers to the objects that +registered the association. + +Every time =twa::register_ap()= is called, it calls a similar function +in the =bdd_dict= to check for an existing association or register a +new one. When =aut1= is deleted, it unregisters all its variables, +causing variable =0= to become free. The free list is actually a list +of pairs representing ranges of free variables that can be reassigned +by the BDD dict when needed. (The *anonymous list* serves when +[[#anonymous][*anonymous BDD variables*]] are used.) + +Such a low-level registration is usually handled by the following +interface: + +#+BEGIN_SRC C++ :exports code + // return a BDD variable number for f + int bdd_dict::register_proposition(formula f, const void* for_me); + // release the BDD variable + void bdd_dict::unregister_variable(int var, const void* me); + // release all BDD variables registered by me + void bdd_dict::unregister_all_my_variables(const void* me); + // register the same variables as another object + void bdd_dict::register_all_variables_of(const void* from_other, + const void* for_me); +#+END_SRC + +The last function may be bit tricky to use, because we need to be sure +that another object has registered some variables. You can rely on +the fact that each =twa= automaton register its variables this way. + +Now, in most cases, there is no need to worry about the =bdd_dict=. +Automata will register and unregister variables as needed. Other +objects like =spot::twa_word= will do the same. + +There are at least two situations where one may need to deal with the +=bdd_dict=: +1. One case is when [[#ap][creating a derived object that store some BDD + representing a formula over atomic proposition]] (but without + reference to their original automaton). +2. Another case is when [[#anonymous][more BDD variables (maybe + unrelated to atomic propositions) are needed]]. + +These two cases are discussed in the next sections. + +* Prolonging the association between a BDD variable and an atomic proposition + :PROPERTIES: + :CUSTOM_ID: ap + :END: + +Let us implement an object representing a set of transitions of the +form $(src, guard, dest)$. This can for instance be used to store +all transition that belong to a certain acceptance set. + +#+NAME: trans_set +#+begin_src python :export code + import spot + + class trans_set: + def __init__(self, dict): + self.set = set() + self.dict = dict + def add_trans(self, src, guard, dst): + self.set.add((src, guard, dst)) + def str_trans(self, src, guard, dst): + f = spot.bdd_format_formula(self.dict, guard) + return "({},{},{})".format(src, f, dst) + def __str__(self): + return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' + + def accepting_set(aut, num): + ts = trans_set(aut.get_dict()) + for e in aut.edges(): + if e.acc.has(num): + ts.add_trans(e.src, e.cond, e.dst) + return ts +#+end_src + +The above code has two definitions. +1. The =trans_set= class is a set of transitions that can be printed. + It stores a =bdd_dict= so that it can print the guard of the + transition. +2. The =accepting_set= function iterates over an automaton, and saves + all transitions that belong to a given acceptance set number. + +For instance we can now translate an automaton, compute its acceptance +set 0, and print it as follows: + +#+begin_src python :noweb strip-export + <> + aut = spot.translate('GF(a <-> XXa)') + ts = accepting_set(aut, 0) + print(ts) +#+end_src +#+RESULTS: +: {(0,a,3),(1,a,1),(2,!a,2),(3,!a,0)} + +The code of =trans_set= is in fact bogus. The problem is that it +assumes the association between the atomic propositions and the BDD +variable is still available when the =str_trans= method is called. +However, that might not be the case. + +The following call sequence demonstrates the problem: + +#+begin_src python :noweb strip-export + <> + try: + ts = accepting_set(spot.translate('GF(a <-> XXa)'), 0) + print(ts) + except RuntimeError as e: + print("ERROR:", e) +#+end_src + +#+RESULTS: +: ERROR: bdd_to_formula() was passed a bdd with a variable that is not in the dictionary + +In this case, the temporary automaton constructed by +=spot.translate()= and passed to the =accepting_set()= function is +destroyed right after the =ts= object has been constructed. When the +automaton is destroyed, it removes all its associations from the +=bdd_dict=. This means that before the =print(ts)= the dictionary +that was used by the automaton, and that is still stored in the =ts= +objects is now empty: calling =bdd_format_formula()= raises an +exception. + +This can be fixed in a couple of ways. The easy way is to store the +automaton inside the =trans_set= object, to ensure that it will live +at least as long as the =trans_set= object. But maybe the automaton +is too big and we really want to get rid of it? In this case +=trans_set= should tell the =bdd_dict= that it want to retain the +associations. The easiest way in this case is to call the +=register_all_variables_of()= method, because we know that each +automaton registers its variables. + +#+begin_src python + import spot + + class trans_set: + def __init__(self, aut): + self.set = set() + self.dict = aut.get_dict() + self.dict.register_all_variables_of(aut, self) + def __del__(self): + self.dict.unregister_all_my_variables(self) + def add_trans(self, src, guard, dest): + self.set.add((src, guard, dest)) + def str_trans(self, src, guard, dest): + f = spot.bdd_format_formula(self.dict, guard) + return "({},{},{})".format(src, f, dest) + def __str__(self): + return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' + + def accepting_set(aut, num): + ts = trans_set(aut) + for e in aut.edges(): + if e.acc.has(num): + ts.add_trans(e.src, e.cond, e.dst) + return ts + + try: + ts = accepting_set(spot.translate('GF(a <-> XXa)'), 0) + print(ts) + except RuntimeError as e: + print("ERROR:", e) +#+end_src + +#+RESULTS: +: {(0,a,3),(1,a,1),(2,!a,2),(3,!a,0)} + +Notice that we have also added a destructor to =trans_set= to +unregister all the variables. + + +* Anonymous BDD variables + :PROPERTIES: + :CUSTOM_ID: anonymous + :END: + +Another scenario where working with a =bdd_dict= is needed is when one +needs to allocate *anonymous BDD variables*. These are variables that +are not attached to any atomic proposition, and that can be used by +one algorithm privately. If multiple algorithms (or objects) register +anonymous variables, the =bdd_dict= will reuse anonymous variables +allocated to other algorithms. One can allocate multiple anonymous +variables with the following =bdd_dict= method: + +#+begin_src c++ :export code +int bdd_dict::register_anonymous_variables(int n, const void* for_me); +#+end_src + +A range of =n= variables will be allocated starting at the returned +index. + +For instance, let's say the our =trans_set= should now store a +symbolic representation of a transition relation. For simplicity we +assume we just want to store set of pairs =(src,dst)=: each pair will +be a conjunction $v_{src}\land v'_{dst}$ between two BDD variables +taken from two ranges ($v_i$ representing a source state $i$ and $v'i$ +representing a destination state $i$), and the entire set will be a +disjunction of all these pairs. If the automaton has $n$ states, we +want to allocate $2n$ BDD variables for this purpose. We call these +variables *anonymous* because their meaning is unknown the the +=bdd_dict=. + +#+begin_src python + import spot + from buddy import * + + class trans_set: + def __init__(self, aut): + self.dict = d = aut.get_dict() + self.num_states = n = aut.num_states() + self.anonbase = b = d.register_anonymous_variables(2*n, self) + s = bddfalse + for e in aut.edges(): + s |= self.src(e.src) & self.dst(e.dst) + self.rel = s + def src(self, n): + return bdd_ithvar(self.anonbase + n) + def dst(self, n): + return bdd_ithvar(self.anonbase + n + self.num_states) + def __del__(self): + self.dict.unregister_all_my_variables(self) + def __str__(self): + isop = spot.minato_isop(self.rel) + i = isop.next() + res = [] + while i != bddfalse: + s = bdd_var(i) - self.anonbase + d = bdd_var(bdd_high(i)) - self.anonbase - self.num_states + res.append((s, d)) + i = isop.next() + return str(res) + + ts = trans_set(spot.translate('GF(a <-> XXa)')) + print(ts) +#+end_src + +#+RESULTS: +: [(0, 2), (0, 3), (1, 0), (1, 1), (2, 2), (2, 3), (3, 0), (3, 1)] diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 556a2bf04..c1bc8b229 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -200,6 +200,12 @@ class twa_graph: from IPython.display import SVG return SVG(_ostream_to_svg(ostr)) +def make_twa_graph(*args): + from spot.impl import make_twa_graph as mtg + if len(args) == 0: + return mtg(_bdd_dict) + return mtg(*args) + @_extend(formula) class formula: def __init__(self, str):