tgbabdddict.hh 1.06 KB
Newer Older
1
2
3
4
5
6
7
8
9
#ifndef SPOT_TGBA_TGBABDDDICT_H
# define SPOT_TGBA_TGBABDDDICT_H

#include <map>
#include <iostream>
#include "ltlast/formula.hh"

namespace spot
{
10
11

  /// Dictionary of BDD variables.
12
13
  struct tgba_bdd_dict
  {
14
    /// Formula-to-BDD-variable maps.
15
    typedef std::map<const ltl::formula*, int> fv_map;
16
    /// BDD-variable-to-formula maps.
17
18
    typedef std::map<int, const ltl::formula*> vf_map;

19
20
21
22
23
24
    fv_map now_map;		///< Maps formulae to "Now" BDD variables.
    vf_map now_formula_map;	///< Maps "Now" BDD variables to formulae.
    fv_map var_map;		///< Maps atomic propisitions to BDD variables
    vf_map var_formula_map;     ///< Maps BDD variables to atomic propisitions
    fv_map prom_map;		///< Maps promises to BDD variables.
    vf_map prom_formula_map;    ///< Maps BDD variables to promises.
25

26
27
    /// \brief Dump all variables for debugging.
    /// \param os The output stream.
28
    std::ostream& dump(std::ostream& os) const;
29
30
31

    /// Whether this dictionary contains \a other.
    bool contains(const tgba_bdd_dict& other) const;
32
33
34
35
  };
}

#endif // SPOT_TGBA_TGBABDDDICT_H