Re: [Spot] Creating bdds

Hi Miriam, Spot uses the BuDDy library for handling BDDs. Or rather, a modified version of BuDDy (with slightly modified internals, and additional public functions), but it should not really matter: the documentation of BuDDy you can find at http://buddy.sourceforge.net/manual/main.html still applies. Basically, variables are designated by integers. bdd_ithvar(1) creates a BDD representing the Boolean formula consisting of just variable #1, while bdd_nithvar(1) is its negation. Once you have BDDs, you can combine them using the usual & | ! - operators, and some other operators are available using the bdd_apply function. A simple C++ example can be found in buddy/examples/queen/queen.cxx, it follows the encoding given in section 6.1 of http://configit.com/configit_wordpress/wp-content/uploads/2013/07/bdd-eap.p… In Spot BDDs are used (among other things) to label the edges of automata using Boolean formulas over the atomic propositions. So for instance we can have an edge labeled by "a|b" and another one labeled by "!a&c", and if these two edges belong to different automata that we want to synchronize, we can easily compute that the conjunction of these two labels is "!a&b&c". Spot uses a bdd_dict object to associate an atomic proposition (an instance of the formula class created for instance using spot::formula::ap()) to a BDD variable number as used by BuDDy. The bdd_dict also wants to keep tracks of which automata use what BDD variable, so that BDD variables can be recycled for other purposes once they are not used anymore. The simplest way to register a new BDD variable from a named string is via the twa::register_ap() method, as illustrated here: https://spot.lrde.epita.fr/tut22.html This takes care of creating the atomic proposition and registering it to the bdd_dict if needed. If you print a BDD using "cout << bdd", you will see variable numbers, so that is not very nice for debugging. To print a BDD as a Boolean formula that uses the name of the atomic propositions, use bdd_print_formula(bdd_dict, bdd). HTH & happy new year to you too Alexandre