spot 2.11.6.dev
Loading...
Searching...
No Matches
bdddict.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2011-2017, 2022 Laboratoire de Recherche et
3// Développement 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
34namespace 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
67
69 typedef std::map<formula, int> fv_map;
71 typedef std::map<int, formula> vf_map;
72
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() noexcept: 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}
Map BDD variables to formulae.
Definition bdddict.hh:56
std::set< const void * > ref_set
BDD-variable reference counts.
Definition bdddict.hh:77
std::ostream & dump(std::ostream &os) const
Dump all variables for debugging.
int register_acceptance_variable(formula f, const void *for_me)
Register an acceptance variable.
void assert_emptiness() const
Make sure the dictionary is empty.
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
std::map< int, formula > vf_map
BDD-variable-to-formula maps.
Definition bdddict.hh:71
std::map< formula, int > fv_map
Formula-to-BDD-variable maps.
Definition bdddict.hh:69
void unregister_variable(int var, std::shared_ptr< T > me)
Release a variable used by me.
Definition bdddict.hh:212
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:104
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: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
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:73
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:165
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
fv_map acc_map
Maps acceptance conditions to BDD variables.
Definition bdddict.hh:74
int register_acceptance_variable(formula f, std::shared_ptr< T > for_me)
Register an acceptance variable.
Definition bdddict.hh:148
~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:733
LTL/PSL formula interface.
Definition automata.hh:27
Definition bdddict.hh:80

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