alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Don't always delete the tgba used in ta_explicit.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-24 21:54:52 +02:00
parent be6071184e
commit 8e1438c98f
6 changed files with 35 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ta/taexplicit.cc
View file

@ -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,6 +380,7 @@ namespace spot
delete s;
}
get_dict()->unregister_all_my_variables(this);
if (own_tgba_)
delete tgba_;
}
@ -387,7 +391,6 @@ namespace spot
states_set_.insert(s);
return static_cast<state_ta_explicit*> (*add_state_to_ta.first);
}
void

9
src/ta/taexplicit.hh
View file

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

9
src/ta/tgtaexplicit.cc
View file

@ -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)
{
}

7
src/ta/tgtaexplicit.hh
View file

@ -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*

11
src/taalgos/minimize.cc
View file

@ -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<const tgta_explicit*> (tgta_);

4
src/tgbatest/ltl2tgba.cc
View file

@ -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;
}