From 8e1438c98f9f2bc083b562496a59045e0484377f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Jun 2012 21:54:52 +0200 Subject: [PATCH] Don't always delete the tgba used in ta_explicit. * src/ta/taexplicit.hh (ta_explicit): Take a boolean to tell whether the tgba is owned. * src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh: Likewise. * src/ta/taexplicit.cc (~ta_explicit): Adjust destruction. * src/tgbatest/ltl2tgba.cc: Adjust usage. * src/taalgos/minimize.cc: Likewise. --- src/ta/taexplicit.cc | 19 +++++++++++-------- src/ta/taexplicit.hh | 9 +++++---- src/ta/tgtaexplicit.cc | 9 +++++---- src/ta/tgtaexplicit.hh | 7 ++++--- src/taalgos/minimize.cc | 11 ++++++----- src/tgbatest/ltl2tgba.cc | 4 ++++ 6 files changed, 35 insertions(+), 24 deletions(-) diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 240697e77..018edd660 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// DĂ©veloppement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -352,9 +353,12 @@ namespace spot ta_explicit::ta_explicit(const tgba* tgba, bdd all_acceptance_conditions, - state_ta_explicit* artificial_initial_state) : - tgba_(tgba), all_acceptance_conditions_(all_acceptance_conditions), - artificial_initial_state_(artificial_initial_state) + state_ta_explicit* artificial_initial_state, + bool own_tgba) : + tgba_(tgba), + all_acceptance_conditions_(all_acceptance_conditions), + artificial_initial_state_(artificial_initial_state), + own_tgba_(own_tgba) { get_dict()->register_all_variables_of(&tgba_, this); if (artificial_initial_state != 0) @@ -362,7 +366,6 @@ namespace spot state_ta_explicit* is = add_state(artificial_initial_state); assert(is == artificial_initial_state); } - } ta_explicit::~ta_explicit() @@ -377,7 +380,8 @@ namespace spot delete s; } get_dict()->unregister_all_my_variables(this); - delete tgba_; + if (own_tgba_) + delete tgba_; } state_ta_explicit* @@ -387,7 +391,6 @@ namespace spot states_set_.insert(s); return static_cast (*add_state_to_ta.first); - } void diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index 5e68a0812..790203c90 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita_explicit (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Developpement de l Epita_explicit (LRDE). // // This file is part of Spot, a model checking library. // @@ -43,7 +43,8 @@ namespace spot { public: ta_explicit(const tgba* tgba, bdd all_acceptance_conditions, - state_ta_explicit* artificial_initial_state = 0); + state_ta_explicit* artificial_initial_state = 0, + bool own_tgba = false); const tgba* get_tgba() const; @@ -141,7 +142,7 @@ namespace spot state_ta_explicit* artificial_initial_state_; ta::states_set_t states_set_; ta::states_set_t initial_states_set_; - + bool own_tgba_; }; /// states used by spot::ta_explicit. diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 6d6465a91..102b7aaac 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -31,8 +31,9 @@ namespace spot { tgta_explicit::tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, - state_ta_explicit* artificial_initial_state) : - ta_explicit(tgba, all_acceptance_conditions, artificial_initial_state) + state_ta_explicit* artificial_initial_state, + bool own_tgba) : + ta_explicit(tgba, all_acceptance_conditions, artificial_initial_state, own_tgba) { } diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 366e8686e..86a9a5f6b 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita_explicit (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// DĂ©veloppement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -40,7 +40,8 @@ namespace spot { public: tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, - state_ta_explicit* artificial_initial_state); + state_ta_explicit* artificial_initial_state, + bool own_tgba = false); // tgba interface virtual spot::state* diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 7e2415196..7de54cf76 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -502,7 +502,8 @@ namespace spot tgba_explicit_number* tgba = new tgba_explicit_number(ta_->get_dict()); - ta_explicit* res = new ta_explicit(tgba, ta_->all_acceptance_conditions()); + ta_explicit* res = new ta_explicit(tgba, ta_->all_acceptance_conditions(), + 0, /* own_tgba = */ true); partition_t partition = build_partition(ta_); @@ -524,8 +525,8 @@ namespace spot tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict()); - tgta_explicit* res = new tgta_explicit(tgba, - tgta_->all_acceptance_conditions(), 0); + tgta_explicit* res = new tgta_explicit(tgba, tgta_->all_acceptance_conditions(), + 0, /* own_tgba = */ true); //TODO copier le tgta_ dans un tgta_explicit au lieu de faire un cast... const ta_explicit* tgta = dynamic_cast (tgta_); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 2a3664c77..a8138027b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -845,6 +845,7 @@ main(int argc, char** argv) { spot::tgba_bdd_concrete* concrete = 0; const spot::tgba* to_free = 0; + const spot::tgba* to_free2 = 0; spot::tgba* a = 0; if (from_file) @@ -1149,6 +1150,7 @@ main(int argc, char** argv) delete testing_automata_nm; delete testing_automata; + delete a; a = 0; degeneralized = 0; if (degeneralize_opt != DegenSBA) @@ -1157,6 +1159,7 @@ main(int argc, char** argv) } if (tgta_opt) { + to_free2 = a; spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd); if (opt_bisim_ta) { @@ -1485,6 +1488,7 @@ main(int argc, char** argv) delete degeneralized; delete aut_scc; delete to_free; + delete to_free2; delete echeck_inst; delete temp_dir_sim; }