spot  2.8.1
bdddict.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011-2017 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
5 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
6 // Université Pierre et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // under the terms of the GNU General Public License as published by
12 // the Free Software Foundation; either version 3 of the License, or
13 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // You should have received a copy of the GNU General Public License
21 // along with this program. If not, see <http://www.gnu.org/licenses/>.
22 
23 #pragma once
24 
25 #include <list>
26 #include <set>
27 #include <map>
28 #include <iosfwd>
29 #include <bddx.h>
30 #include <vector>
31 #include <memory>
32 #include <spot/tl/formula.hh>
33 
34 namespace spot
35 {
37  class bdd_dict_priv;
38 
55  class SPOT_API bdd_dict
56  {
57  bdd_dict_priv* priv_;
58  public:
59 
60  bdd_dict();
61 
66  ~bdd_dict();
67 
69  typedef std::map<formula, int> fv_map;
71  typedef std::map<int, formula> vf_map;
72 
73  fv_map var_map;
74  fv_map acc_map;
75 
77  typedef std::set<const void*> ref_set;
78 
79  enum var_type { anon = 0, var, acc };
80  struct bdd_info {
81  bdd_info() : type(anon) {}
82  var_type type;
83  formula f; // Used unless t==anon.
84  ref_set refs;
85  };
86  typedef std::vector<bdd_info> bdd_info_map;
87  // Map BDD variables to their meaning.
88  bdd_info_map bdd_map;
89 
101  int register_proposition(formula f, const void* for_me);
102 
103  template <typename T>
104  int register_proposition(formula f, std::shared_ptr<T> for_me)
105  {
106  return register_proposition(f, for_me.get());
107  }
109 
116  int has_registered_proposition(formula f, const void* me);
117 
118  template <typename T>
119  int has_registered_proposition(formula f, std::shared_ptr<T> for_me)
120  {
121  return has_registered_proposition(f, for_me.get());
122  }
124 
125  // \brief return the BDD variable associated to a registered
126  // proposition.
127  //
128  // Throws std::out_of_range if the \a is not a known proposition.
129  int varnum(formula f)
130  {
131  return var_map.at(f);
132  }
133 
145  int register_acceptance_variable(formula f, const void* for_me);
146 
147  template <typename T>
148  int register_acceptance_variable(formula f, std::shared_ptr<T> for_me)
149  {
150  return register_acceptance_variable(f, for_me.get());
151  }
153 
162  int register_anonymous_variables(int n, const void* for_me);
163 
164  template <typename T>
165  int register_anonymous_variables(int n, std::shared_ptr<T> for_me)
166  {
167  return register_anonymous_variables(n, for_me.get());
168  }
170 
178  void register_all_variables_of(const void* from_other, const void* for_me);
179 
180  template <typename T>
181  void register_all_variables_of(const void* from_other,
182  std::shared_ptr<T> for_me)
183  {
184  register_all_variables_of(from_other, for_me.get());
185  }
186 
187  template <typename T>
188  void register_all_variables_of(std::shared_ptr<T> from_other,
189  const void* for_me)
190  {
191  register_all_variables_of(from_other.get(), for_me);
192  }
193 
194  template <typename T, typename U>
195  void register_all_variables_of(std::shared_ptr<T> from_other,
196  std::shared_ptr<U> for_me)
197  {
198  register_all_variables_of(from_other.get(), for_me.get());
199  }
201 
205  void unregister_all_my_variables(const void* me);
206 
209  void unregister_variable(int var, const void* me);
210 
211  template <typename T>
212  void unregister_variable(int var, std::shared_ptr<T> me)
213  {
214  unregister_variable(var, me.get());
215  }
217 
220  std::ostream& dump(std::ostream& os) const;
221 
233  void assert_emptiness() const;
234 
235  private:
236  // Disallow copy.
237  bdd_dict(const bdd_dict& other) = delete;
238  bdd_dict& operator=(const bdd_dict& other) = delete;
239  };
240 
241  typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
242 
243  inline bdd_dict_ptr make_bdd_dict()
244  {
245  return std::make_shared<bdd_dict>();
246  }
247 }
std::set< const void * > ref_set
BDD-variable reference counts.
Definition: bdddict.hh:77
Definition: automata.hh:26
std::map< int, formula > vf_map
BDD-variable-to-formula maps.
Definition: bdddict.hh:71
fv_map acc_map
Maps acceptance conditions to BDD variables.
Definition: bdddict.hh:74
std::map< formula, int > fv_map
Formula-to-BDD-variable maps.
Definition: bdddict.hh:69
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:188
LTL/PSL formula interface.
Main class for temporal logic formula.
Definition: formula.hh:686
Definition: bdddict.hh:80
Map BDD variables to formulae.
Definition: bdddict.hh:55
void unregister_variable(int var, std::shared_ptr< T > me)
Release a variable used by me.
Definition: bdddict.hh:212
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:195
int register_proposition(formula f, std::shared_ptr< T > for_me)
Register an atomic proposition.
Definition: bdddict.hh:104
int register_anonymous_variables(int n, std::shared_ptr< T > for_me)
Register anonymous BDD variables.
Definition: bdddict.hh:165
int register_acceptance_variable(formula f, std::shared_ptr< T > for_me)
Register an acceptance variable.
Definition: bdddict.hh:148
fv_map var_map
Maps atomic propositions to BDD variables.
Definition: bdddict.hh:73
int has_registered_proposition(formula f, std::shared_ptr< T > for_me)
whether a proposition has already been registered
Definition: bdddict.hh:119
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:181

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.8.13