Commit dc5ad78b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Make bdd_dict a shared pointer.

* src/tgba/bdddict.hh (bdd_dict_ptr): New type.
(make_bdd_dict): New function.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
src/dstarparse/dstarparse.yy, src/dstarparse/public.hh,
src/graphtest/tgbagraph.cc, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/neverparse/neverclaimparse.yy, src/neverparse/public.hh,
src/priv/accmap.hh, src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/sabatest/sabacomplementtgba.cc,
src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/taalgos/dotty.cc, src/tgba/bddprint.cc,
src/tgba/bddprint.hh, src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh,
src/tgba/tgbagraph.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh,
src/tgba/wdbacomp.cc, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbaalgos/word.cc, src/tgbaalgos/word.hh, src/tgbaparse/public.hh,
src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/maskacc.cc,
src/tgbatest/powerset.cc, src/tgbatest/randtgba.cc,
src/tgbatest/taatgba.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
wrap/python/tests/alarm.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/parsetgba.py: Update to use bdd_dict_ptr and
make_bdd_dict().
parent 10e5c623
......@@ -328,7 +328,7 @@ namespace spot
int
convert_aps(const ltl::atomic_prop_set* aps,
const dve2_interface* d,
bdd_dict* dict,
bdd_dict_ptr dict,
const ltl::formula* dead,
prop_set& out)
{
......@@ -604,8 +604,8 @@ namespace spot
{
public:
dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps,
const ltl::formula* dead, int compress)
dve2_kripke(const dve2_interface* d, bdd_dict_ptr dict,
const prop_set* ps, const ltl::formula* dead, int compress)
: d_(d),
state_size_(d_->get_state_variable_count()),
dict_(dict), ps_(ps),
......@@ -913,7 +913,7 @@ namespace spot
}
virtual
spot::bdd_dict* get_dict() const
spot::bdd_dict_ptr get_dict() const
{
return dict_;
}
......@@ -921,7 +921,7 @@ namespace spot
private:
const dve2_interface* d_;
int state_size_;
bdd_dict* dict_;
bdd_dict_ptr dict_;
const char** vname_;
bool* format_filter_;
const prop_set* ps_;
......@@ -998,7 +998,7 @@ namespace spot
kripke*
load_dve2(const std::string& file_arg, bdd_dict* dict,
load_dve2(const std::string& file_arg, bdd_dict_ptr dict,
const ltl::atomic_prop_set* to_observe,
const ltl::formula* dead,
int compress,
......
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE)
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
......@@ -56,7 +57,7 @@ namespace spot
// dead states
// \a verbose whether to output verbose messages
SPOT_API kripke*
load_dve2(const std::string& file, bdd_dict* dict,
load_dve2(const std::string& file, bdd_dict_ptr dict,
const ltl::atomic_prop_set* to_observe,
const ltl::formula* dead = ltl::constant::true_instance(),
int compress = 0, bool verbose = true);
......
......@@ -156,7 +156,7 @@ main(int argc, char **argv)
spot::ltl::atomic_prop_set ap;
spot::bdd_dict* dict = new spot::bdd_dict();
auto dict = spot::make_bdd_dict();
spot::kripke* model = 0;
const spot::tgba* prop = 0;
spot::tgba* product = 0;
......@@ -367,7 +367,6 @@ main(int argc, char **argv)
delete model;
if (f)
f->destroy();
delete dict;
deadf->destroy();
......
......@@ -293,8 +293,7 @@ namespace
{
spot::dstar_parse_error_list pel;
spot::dstar_aut* daut;
spot::bdd_dict dict;
daut = spot::dstar_parse(filename, pel, &dict);
daut = spot::dstar_parse(filename, pel, spot::make_bdd_dict());
if (spot::format_dstar_parse_errors(std::cerr, filename, pel))
{
delete daut;
......
......@@ -739,7 +739,7 @@ namespace
class translator_runner: protected spot::formater
{
private:
spot::bdd_dict& dict;
spot::bdd_dict_ptr dict;
// Round-specific variables
quoted_string string_ltl_spot;
quoted_string string_ltl_spin;
......@@ -754,7 +754,7 @@ namespace
public:
using spot::formater::has;
translator_runner(spot::bdd_dict& dict)
translator_runner(spot::bdd_dict_ptr dict)
: dict(dict)
{
declare('f', &string_ltl_spot);
......@@ -902,7 +902,7 @@ namespace
{
spot::neverclaim_parse_error_list pel;
std::string filename = output.val()->name();
res = spot::neverclaim_parse(filename, pel, &dict);
res = spot::neverclaim_parse(filename, pel, dict);
if (!pel.empty())
{
status_str = "parse error";
......@@ -930,7 +930,7 @@ namespace
}
else
{
res = spot::lbtt_parse(f, error, &dict);
res = spot::lbtt_parse(f, error, dict);
if (!res)
{
status_str = "parse error";
......@@ -948,7 +948,7 @@ namespace
spot::dstar_parse_error_list pel;
std::string filename = output.val()->name();
spot::dstar_aut* aut;
aut = spot::dstar_parse(filename, pel, &dict);
aut = spot::dstar_parse(filename, pel, dict);
if (!pel.empty())
{
status_str = "parse error";
......@@ -1191,12 +1191,12 @@ namespace
class processor: public job_processor
{
spot::bdd_dict dict;
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
translator_runner runner;
fset_t unique_set;
public:
processor()
: runner(dict)
processor():
runner(dict)
{
}
......@@ -1401,7 +1401,7 @@ namespace
// build a random state-space.
spot::srand(seed);
spot::tgba* statespace = spot::random_graph(states, density,
ap, &dict);
ap, dict);
// Products of the state space with the positive automata.
std::vector<spot::tgba*> pos_prod(m);
......
......@@ -279,7 +279,7 @@ states:
static void fill_guards(result_& r)
{
spot::bdd_dict* d = r.d->aut->get_dict();
spot::bdd_dict_ptr d = r.d->aut->get_dict();
size_t nap = r.aps.size();
int* vars = new int[nap];
......@@ -316,7 +316,7 @@ namespace spot
dstar_aut*
dstar_parse(const std::string& name,
dstar_parse_error_list& error_list,
bdd_dict* dict,
bdd_dict_ptr dict,
ltl::environment& env,
bool debug)
{
......
......@@ -88,7 +88,7 @@ namespace spot
SPOT_API dstar_aut*
dstar_parse(const std::string& filename,
dstar_parse_error_list& error_list,
bdd_dict* dict,
bdd_dict_ptr dict,
ltl::environment& env = ltl::default_environment::instance(),
bool debug = false);
......
......@@ -25,18 +25,18 @@
void f1()
{
spot::bdd_dict d;
auto d = spot::make_bdd_dict();
auto& e = spot::ltl::default_environment::instance();
spot::tgba_digraph tg(&d);
spot::tgba_digraph tg(d);
auto* f1 = e.require("p1");
auto* f2 = e.require("p2");
bdd p1 = bdd_ithvar(d.register_proposition(f1, &tg));
bdd p2 = bdd_ithvar(d.register_proposition(f2, &tg));
bdd a1 = bdd_ithvar(d.register_acceptance_variable(f1, &tg));
bdd a2 = bdd_ithvar(d.register_acceptance_variable(f2, &tg));
bdd p1 = bdd_ithvar(d->register_proposition(f1, &tg));
bdd p2 = bdd_ithvar(d->register_proposition(f2, &tg));
bdd a1 = bdd_ithvar(d->register_acceptance_variable(f1, &tg));
bdd a2 = bdd_ithvar(d->register_acceptance_variable(f2, &tg));
f1->destroy();
f2->destroy();
......
......@@ -126,13 +126,13 @@ namespace spot
// kripke_explicit
kripke_explicit::kripke_explicit(bdd_dict* dict)
kripke_explicit::kripke_explicit(bdd_dict_ptr dict)
: dict_(dict),
init_(0)
{
}
kripke_explicit::kripke_explicit(bdd_dict* dict,
kripke_explicit::kripke_explicit(bdd_dict_ptr dict,
state_kripke* init)
: dict_(dict),
init_ (init)
......@@ -169,7 +169,7 @@ namespace spot
return init_;
}
bdd_dict*
bdd_dict_ptr
kripke_explicit::get_dict() const
{
return dict_;
......
......@@ -114,11 +114,11 @@ namespace spot
class SPOT_API kripke_explicit : public kripke
{
public:
kripke_explicit(bdd_dict*);
kripke_explicit(bdd_dict*, state_kripke*);
kripke_explicit(bdd_dict_ptr);
kripke_explicit(bdd_dict_ptr, state_kripke*);
~kripke_explicit();
bdd_dict* get_dict() const;
bdd_dict_ptr get_dict() const;
state_kripke* get_init_state() const;
/// \brief Allow to get an iterator on the state we passed in
......@@ -175,7 +175,7 @@ namespace spot
void add_transition(state_kripke* source,
const state_kripke* dest);
bdd_dict* dict_;
bdd_dict_ptr dict_;
state_kripke* init_;
std::map<const std::string, state_kripke*> ns_nodes_;
std::map<const state_kripke*, std::string> sn_nodes_;
......
......@@ -41,7 +41,7 @@ namespace spot
void process_state(const state* s, int, tgba_succ_iterator* si)
{
const bdd_dict* d = aut_->get_dict();
const bdd_dict_ptr d = aut_->get_dict();
os_ << '"';
escape_str(os_, aut_->format_state(s));
os_ << "\", \"";
......@@ -88,7 +88,7 @@ namespace spot
else
notfirst = true;
const bdd_dict* d = aut_->get_dict();
const bdd_dict_ptr d = aut_->get_dict();
os_ << 'S' << in_s << ", \"";
const kripke* automata = down_cast<const kripke*>(aut_);
assert(automata);
......
......@@ -198,7 +198,7 @@ namespace spot
kripke_explicit*
kripke_parse(const std::string& name,
kripke_parse_error_list& error_list,
bdd_dict* dict,
bdd_dict_ptr dict,
environment& env,
bool debug)
{
......
......@@ -41,7 +41,7 @@ namespace spot
SPOT_API kripke_explicit*
kripke_parse(const std::string& name,
kripke_parse_error_list& error_list,
bdd_dict* dict,
bdd_dict_ptr dict,
ltl::environment& env
= ltl::default_environment::instance(),
bool debug = false);
......
// Copyright (C) 2011 Laboratoire de Recherche et Developpement
// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -28,9 +28,8 @@ int main(int argc, char** argv)
{
int return_value = 0;
kripke_parse_error_list pel;
bdd_dict* dict = new bdd_dict;
kripke_explicit* k = kripke_parse(argv[1], pel, dict);
kripke_explicit* k = kripke_parse(argv[1], pel, make_bdd_dict());
if (!pel.empty())
{
format_kripke_parse_errors(std::cerr, argv[1], pel);
......@@ -41,7 +40,6 @@ int main(int argc, char** argv)
kripke_save_reachable(std::cout, k);
delete k;
delete dict;
assert(ltl::atomic_prop::instance_count() == 0);
assert(ltl::unop::instance_count() == 0);
assert(ltl::binop::instance_count() == 0);
......
......@@ -76,7 +76,7 @@ namespace spot
{
spot::ltl::atomic_prop_set aps;
atomic_prop_collect(f, &aps);
bdd_dict* d = a->get_dict();
auto d = a->get_dict();
bdd res = bddtrue;
for (atomic_prop_set::const_iterator i = aps.begin();
i != aps.end(); ++i)
......
......@@ -37,7 +37,7 @@ namespace spot
{
language_containment_checker::language_containment_checker
(bdd_dict* dict, bool exprop, bool symb_merge,
(bdd_dict_ptr dict, bool exprop, bool symb_merge,
bool branching_postponement, bool fair_loop_approx)
: dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
branching_postponement_(branching_postponement),
......
......@@ -46,7 +46,7 @@ namespace spot
public:
/// This class uses spot::ltl_to_tgba_fm to translate LTL
/// formulae. See that function for the meaning of these options.
language_containment_checker(bdd_dict* dict, bool exprop,
language_containment_checker(bdd_dict_ptr dict, bool exprop,
bool symb_merge,
bool branching_postponement,
bool fair_loop_approx);
......@@ -72,7 +72,7 @@ namespace spot
record_* register_formula_(const formula* f);
/* Translation options */
bdd_dict* dict_;
bdd_dict_ptr dict_;
bool exprop_;
bool symb_merge_;
bool branching_postponement_;
......
......@@ -51,7 +51,7 @@ namespace spot
typedef std::pair<const formula*, const formula*> pairf;
typedef std::map<pairf, bool> syntimpl_cache_t;
public:
bdd_dict* dict;
bdd_dict_ptr dict;
ltl_simplifier_options options;
language_containment_checker lcc;
......@@ -130,12 +130,12 @@ namespace spot
dict->unregister_all_my_variables(this);
}
ltl_simplifier_cache(bdd_dict* d)
ltl_simplifier_cache(bdd_dict_ptr d)
: dict(d), lcc(d, true, true, false, false)
{
}
ltl_simplifier_cache(bdd_dict* d, const ltl_simplifier_options& opt)
ltl_simplifier_cache(bdd_dict_ptr d, const ltl_simplifier_options& opt)
: dict(d), options(opt), lcc(d, true, true, false, false)
{
options.containment_checks |= options.containment_checks_stronger;
......@@ -4694,43 +4694,20 @@ namespace spot
/////////////////////////////////////////////////////////////////////
// ltl_simplifier
ltl_simplifier::ltl_simplifier(bdd_dict* d)
ltl_simplifier::ltl_simplifier(bdd_dict_ptr d)
{
if (!d)
{
d = new bdd_dict;
owndict = true;
}
else
{
owndict = false;
}
cache_ = new ltl_simplifier_cache(d);
}
ltl_simplifier::ltl_simplifier(const ltl_simplifier_options& opt,
bdd_dict* d)
bdd_dict_ptr d)
{
if (!d)
{
d = new bdd_dict;
owndict = true;
}
else
{
owndict = false;
}
cache_ = new ltl_simplifier_cache(d, opt);
}
ltl_simplifier::~ltl_simplifier()
{
bdd_dict* todelete = 0;
if (owndict)
todelete = cache_->dict;
delete cache_;
// It has to be deleted after the cache.
delete todelete;
}
const formula*
......@@ -4794,7 +4771,7 @@ namespace spot
return cache_->boolean_to_isop(f);
}
bdd_dict*
bdd_dict_ptr
ltl_simplifier::get_dict() const
{
return cache_->dict;
......
// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -78,8 +79,9 @@ namespace spot
class SPOT_API ltl_simplifier
{
public:
ltl_simplifier(bdd_dict* dict = 0);
ltl_simplifier(const ltl_simplifier_options& opt, bdd_dict* dict = 0);
ltl_simplifier(bdd_dict_ptr dict = make_bdd_dict());
ltl_simplifier(const ltl_simplifier_options& opt,
bdd_dict_ptr dict = make_bdd_dict());
~ltl_simplifier();
/// Simplify the formula \a f (using options supplied to the
......@@ -157,7 +159,7 @@ namespace spot
void clear_as_bdd_cache();
/// Return the bdd_dict used.
bdd_dict* get_dict() const;
bdd_dict_ptr get_dict() const;
/// Cached version of spot::ltl::star_normal_form().
const formula* star_normal_form(const formula* f);
......@@ -177,8 +179,6 @@ namespace spot
// Copy disallowed.
ltl_simplifier(const ltl_simplifier&) SPOT_DELETED;
void operator=(const ltl_simplifier&) SPOT_DELETED;
bool owndict;
};
}
......
......@@ -289,7 +289,7 @@ namespace spot
tgba_digraph*
neverclaim_parse(const std::string& name,
neverclaim_parse_error_list& error_list,
bdd_dict* dict,
bdd_dict_ptr dict,
environment& env,
bool debug)
{
......
......@@ -59,7 +59,7 @@ namespace spot
neverclaim_parse(const std::string& filename,
neverclaim_parse_error_list&
error_list,
bdd_dict* dict,
bdd_dict_ptr dict,
ltl::environment& env = ltl::default_environment::instance(),
bool debug = false);
......
......@@ -31,7 +31,7 @@ namespace spot
class acc_mapper_common
{
protected:
bdd_dict* dict_;
bdd_dict_ptr dict_;
tgba_digraph* aut_;
ltl::environment& env_;
bdd neg_;
......
......@@ -85,7 +85,7 @@ namespace spot
/// This is useful when dealing with several automata (which
/// may use the same BDD variable for different formula),
/// or simply when printing.
virtual bdd_dict* get_dict() const = 0;
virtual bdd_dict_ptr get_dict() const = 0;
/// \brief Format the state as a string for printing.
///
......
......@@ -415,7 +415,7 @@ namespace spot
state);
}
bdd_dict*
bdd_dict_ptr
saba_complement_tgba::get_dict() const
{
return automaton_->get_dict();
......
......@@ -63,7 +63,7 @@ namespace spot
virtual saba_succ_iterator*
succ_iter(const saba_state* local_state) const;
virtual bdd_dict* get_dict() const;
virtual bdd_dict_ptr get_dict() const;
virtual std::string format_state(const saba_state* state) const;
virtual bdd all_acceptance_conditions() const;
private:
......
......@@ -64,15 +64,12 @@ int main(int argc, char* argv[])
return 1;
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba* a;
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse(formula, p1);
if (spot::ltl::format_parse_errors(std::cerr, formula, p1))
return 2;
a = spot::ltl_to_tgba_fm(f1, dict);
auto a = spot::ltl_to_tgba_fm(f1, spot::make_bdd_dict());
spot::saba_complement_tgba* complement =
new spot::saba_complement_tgba(a);
......@@ -82,5 +79,4 @@ int main(int argc, char* argv[])
delete complement;
delete a;
f1->destroy();
delete dict;
}
......@@ -129,7 +129,7 @@ namespace spot
/// This is useful when dealing with several automata (which
/// may use the same BDD variable for different formula),
/// or simply when printing.
virtual bdd_dict*
virtual bdd_dict_ptr
get_dict() const = 0;
/// \brief Format the state as a string for printing.
......
......@@ -490,7 +490,7 @@ namespace spot
return new ta_explicit_succ_iterator(s, condition);
}
bdd_dict*
bdd_dict_ptr
ta_explicit::get_dict() const
{
return tgba_->get_dict();
......
......@@ -73,7 +73,7 @@ namespace spot
virtual ta_succ_iterator*
succ_iter(const spot::state* s, bdd condition) const;
virtual bdd_dict*
virtual bdd_dict_ptr
get_dict() const;
virtual std::string
......
......@@ -328,7 +328,7 @@ namespace spot
}