bdddict.hh 5.37 KB
Newer Older
1
2
3
#ifndef SPOT_TGBA_BDDDICT_HH
# define SPOT_TGBA_BDDDICT_HH

4
#include "misc/hash.hh"
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
#include <list>
#include <set>
#include <iostream>
#include <bdd.h>
#include "ltlast/formula.hh"
#include "misc/bddalloc.hh"

namespace spot
{

  /// Map BDD variables to formulae.
  class bdd_dict: public bdd_allocator
  {
  public:

    bdd_dict();
    ~bdd_dict();

    /// Formula-to-BDD-variable maps.
24
25
    typedef Sgi::hash_map<const ltl::formula*, int,
			  ptr_hash<ltl::formula> > fv_map;
26
    /// BDD-variable-to-formula maps.
27
    typedef Sgi::hash_map<int, const ltl::formula*> vf_map;
28
29
30

    fv_map now_map;		///< Maps formulae to "Now" BDD variables
    vf_map now_formula_map;	///< Maps "Now" BDD variables to formulae
31
32
    fv_map var_map;		///< Maps atomic propositions to BDD variables
    vf_map var_formula_map;     ///< Maps BDD variables to atomic propositions
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
    fv_map acc_map;		///< Maps accepting conditions to BDD variables
    vf_map acc_formula_map;	///< Maps BDD variables to accepting conditions

    /// \brief Map Next variables to Now variables.
    ///
    /// Use with BuDDy's bdd_replace() function.
    bddPair* next_to_now;
    /// \brief Map Now variables to Next variables.
    ///
    /// Use with BuDDy's bdd_replace() function.
    bddPair* now_to_next;

    /// \brief Register an atomic proposition.
    ///
    /// Return (and maybe allocate) a BDD variable designating formula
    /// \a f.  The \a for_me argument should point to the object using
    /// this BDD variable, this is used for reference counting.  It is
    /// perfectly safe to call this function several time with the same
    /// arguments.
    ///
    /// \return The variable number.  Use bdd_ithvar() or bdd_nithvar()
    ///   to convert this to a BDD.
    int register_proposition(const ltl::formula* f, const void* for_me);

57
58
59
60
61
62
63
64
65
    /// \brief Register BDD variables as atomic propositions.
    ///
    /// Register all variables occurring in \a f as atomic propositions
    /// used by \a for_me.  This assumes that these atomic propositions
    /// are already known from the dictionary (i.e., they have already
    /// been registered by register_proposition() for another
    /// automaton).
    void register_propositions(bdd f, const void* for_me);

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
    /// \brief Register a couple of Now/Next variables
    ///
    /// Return (and maybe allocate) two BDD variables for a state
    /// associated to formula \a f.  The \a for_me argument should point
    /// to the object using this BDD variable, this is used for
    /// reference counting.  It is perfectly safe to call this
    /// function several time with the same arguments.
    ///
    /// \return The first variable number.  Add one to get the second
    /// variable.  Use bdd_ithvar() or bdd_nithvar() to convert this
    /// to a BDD.
    int register_state(const ltl::formula* f, const void* for_me);

    /// \brief Register an atomic proposition.
    ///
    /// Return (and maybe allocate) a BDD variable designating an
    /// accepting set associated to formula \a f.  The \a for_me
    /// argument should point to the object using this BDD variable,
    /// this is used for reference counting.  It is perfectly safe to
    /// call this function several time with the same arguments.
    ///
    /// \return The variable number.  Use bdd_ithvar() or bdd_nithvar()
    ///   to convert this to a BDD.
    int register_accepting_variable(const ltl::formula* f, const void* for_me);

91
92
93
94
95
96
97
98
99
    /// \brief Register BDD variables as accepting variables.
    ///
    /// Register all variables occurring in \a f as accepting variables
    /// used by \a for_me.  This assumes that these accepting variables
    /// are already known from the dictionary (i.e., they have already
    /// been registered by register_accepting_variable() for another
    /// automaton).
    void register_accepting_variables(bdd f, const void* for_me);

100
101
102
103
104
105
106
107
108
109
110
111
112
    /// \brief Duplicate the variable usage of another object.
    ///
    /// This tells this dictionary that the \a for_me object
    /// will be using the same BDD variables as the \a from_other objects.
    /// This ensure that the variables won't be freed when \a from_other
    /// is deleted if \a from_other is still alive.
    void register_all_variables_of(const void* from_other, const void* for_me);

    /// \brief Release the variables used by object.
    ///
    /// Usually called in the destructor if \a me.
    void unregister_all_my_variables(const void* me);

113
    /// @{
114
    /// Check whether formula \a f has already been registered by \a by_me.
115
116
117
118
119
    bool is_registered_proposition(const ltl::formula* f, const void* by_me);
    bool is_registered_state(const ltl::formula* f, const void* by_me);
    bool is_registered_accepting_variable(const ltl::formula* f,
					  const void* by_me);
    /// @}
120
121
122
123
124
125
126
127
128
129
130
131
132

    /// \brief Dump all variables for debugging.
    /// \param os The output stream.
    std::ostream& dump(std::ostream& os) const;

    /// \brief Make sure the dictionary is empty.
    ///
    /// This will print diagnostics and abort if the dictionary
    /// is not empty.  Use for debugging.
    void assert_emptiness() const;

  protected:
    /// BDD-variable reference counts.
133
134
    typedef Sgi::hash_set<const void*, ptr_hash<void> > ref_set;
    typedef Sgi::hash_map<int, ref_set> vr_map;
135
136
137
138
139
140
141
142
143
144
145
146
    vr_map var_refs;

  private:
    // Disallow copy.
    bdd_dict(const bdd_dict& other);
    bdd_dict& operator=(const bdd_dict& other);
  };


}

#endif // SPOT_TGBA_BDDDICT_HH