spot  2.12
bdddict.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <list>
22 #include <set>
23 #include <map>
24 #include <iosfwd>
25 #include <bddx.h>
26 #include <vector>
27 #include <memory>
28 #include <spot/tl/formula.hh>
29 
30 namespace spot
31 {
33  class bdd_dict_priv;
34 
51  class SPOT_API bdd_dict
52  {
53  bdd_dict_priv* priv_;
54  public:
55 
56  bdd_dict();
57 
63 
65  typedef std::map<formula, int> fv_map;
67  typedef std::map<int, formula> vf_map;
68 
71 
73  typedef std::set<const void*> ref_set;
74 
75  enum var_type { anon = 0, var, acc };
76  struct bdd_info {
77  bdd_info() noexcept: type(anon) {}
78  var_type type;
79  formula f; // Used unless t==anon.
80  ref_set refs;
81  };
82  typedef std::vector<bdd_info> bdd_info_map;
83  // Map BDD variables to their meaning.
84  bdd_info_map bdd_map;
85 
97  int register_proposition(formula f, const void* for_me);
98 
99  template <typename T>
100  int register_proposition(formula f, std::shared_ptr<T> for_me)
101  {
102  return register_proposition(f, for_me.get());
103  }
105 
112  int has_registered_proposition(formula f, const void* me);
113 
114  template <typename T>
115  int has_registered_proposition(formula f, std::shared_ptr<T> for_me)
116  {
117  return has_registered_proposition(f, for_me.get());
118  }
120 
121  // \brief return the BDD variable associated to a registered
122  // proposition.
123  //
124  // Throws std::out_of_range if the \a is not a known proposition.
125  int varnum(formula f)
126  {
127  return var_map.at(f);
128  }
129 
141  int register_acceptance_variable(formula f, const void* for_me);
142 
143  template <typename T>
144  int register_acceptance_variable(formula f, std::shared_ptr<T> for_me)
145  {
146  return register_acceptance_variable(f, for_me.get());
147  }
149 
158  int register_anonymous_variables(int n, const void* for_me);
159 
160  template <typename T>
161  int register_anonymous_variables(int n, std::shared_ptr<T> for_me)
162  {
163  return register_anonymous_variables(n, for_me.get());
164  }
166 
174  void register_all_variables_of(const void* from_other, const void* for_me);
175 
176  template <typename T>
177  void register_all_variables_of(const void* from_other,
178  std::shared_ptr<T> for_me)
179  {
180  register_all_variables_of(from_other, for_me.get());
181  }
182 
183  template <typename T>
184  void register_all_variables_of(std::shared_ptr<T> from_other,
185  const void* for_me)
186  {
187  register_all_variables_of(from_other.get(), for_me);
188  }
189 
190  template <typename T, typename U>
191  void register_all_variables_of(std::shared_ptr<T> from_other,
192  std::shared_ptr<U> for_me)
193  {
194  register_all_variables_of(from_other.get(), for_me.get());
195  }
197 
201  void unregister_all_my_variables(const void* me);
202 
205  void unregister_variable(int var, const void* me);
206 
207  template <typename T>
208  void unregister_variable(int var, std::shared_ptr<T> me)
209  {
210  unregister_variable(var, me.get());
211  }
213 
216  std::ostream& dump(std::ostream& os) const;
217 
229  void assert_emptiness() const;
230 
231  private:
232  // Disallow copy.
233  bdd_dict(const bdd_dict& other) = delete;
234  bdd_dict& operator=(const bdd_dict& other) = delete;
235  };
236 
237  typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
238 
239  inline bdd_dict_ptr make_bdd_dict()
240  {
241  return std::make_shared<bdd_dict>();
242  }
243 }
Map BDD variables to formulae.
Definition: bdddict.hh:52
std::set< const void * > ref_set
BDD-variable reference counts.
Definition: bdddict.hh:73
int register_acceptance_variable(formula f, const void *for_me)
Register an acceptance variable.
void assert_emptiness() const
Make sure the dictionary is empty.
std::ostream & dump(std::ostream &os) const
Dump all variables for debugging.
void register_all_variables_of(std::shared_ptr< T > from_other, const void *for_me)
Duplicate the variable usage of another object.
Definition: bdddict.hh:184
std::map< int, formula > vf_map
BDD-variable-to-formula maps.
Definition: bdddict.hh:67
std::map< formula, int > fv_map
Formula-to-BDD-variable maps.
Definition: bdddict.hh:65
void unregister_variable(int var, std::shared_ptr< T > me)
Release a variable used by me.
Definition: bdddict.hh:208
int register_proposition(formula f, const void *for_me)
Register an atomic proposition.
void unregister_all_my_variables(const void *me)
Release all variables used by an object.
int register_proposition(formula f, std::shared_ptr< T > for_me)
Register an atomic proposition.
Definition: bdddict.hh:100
int register_anonymous_variables(int n, const void *for_me)
Register anonymous BDD variables.
int has_registered_proposition(formula f, std::shared_ptr< T > for_me)
whether a proposition has already been registered
Definition: bdddict.hh:115
void register_all_variables_of(const void *from_other, std::shared_ptr< T > for_me)
Duplicate the variable usage of another object.
Definition: bdddict.hh:177
int has_registered_proposition(formula f, const void *me)
whether a proposition has already been registered
fv_map var_map
Maps atomic propositions to BDD variables.
Definition: bdddict.hh:69
void unregister_variable(int var, const void *me)
Release a variable used by me.
int register_anonymous_variables(int n, std::shared_ptr< T > for_me)
Register anonymous BDD variables.
Definition: bdddict.hh:161
void register_all_variables_of(std::shared_ptr< T > from_other, std::shared_ptr< U > for_me)
Duplicate the variable usage of another object.
Definition: bdddict.hh:191
fv_map acc_map
Maps acceptance conditions to BDD variables.
Definition: bdddict.hh:70
int register_acceptance_variable(formula f, std::shared_ptr< T > for_me)
Register an acceptance variable.
Definition: bdddict.hh:144
~bdd_dict()
Destroy the BDD dict.
void register_all_variables_of(const void *from_other, const void *for_me)
Duplicate the variable usage of another object.
Main class for temporal logic formula.
Definition: formula.hh:732
LTL/PSL formula interface.
Definition: automata.hh:26
Definition: bdddict.hh:76

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1