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

Fix constness of minimize_wdba() return.

Browse source 
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc:
Return a tgba*, not a const tgba*.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-29 00:44:38 +02:00
parent df1785f526
commit f082700fb2
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgbaalgos/minimize.cc
View file

@ -619,7 +619,7 @@ namespace spot
return minimize_dfa(det_a, final, non_final); return minimize_dfa(det_a, final, non_final);
} }
const tgba* tgba*
minimize_obligation(const tgba* aut_f, minimize_obligation(const tgba* aut_f,
const ltl::formula* f, const tgba* aut_neg_f) const ltl::formula* f, const tgba* aut_neg_f)
{ {
@ -706,6 +706,6 @@ namespace spot
if (ok) if (ok)
return min_aut_f; return min_aut_f;
delete min_aut_f; delete min_aut_f;
return aut_f; return const_cast<tgba*>(aut_f);
} }
} }

8
src/tgbaalgos/minimize.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -140,9 +140,9 @@ namespace spot
/// product(aut_neg_f,minize(aut))</code> are both empty. If they /// product(aut_neg_f,minize(aut))</code> are both empty. If they
/// are, the the minimization was sound. (See the paper for full /// are, the the minimization was sound. (See the paper for full
/// details.) /// details.)
const tgba* minimize_obligation(const tgba* aut_f, tgba* minimize_obligation(const tgba* aut_f,
const ltl::formula* f = 0, const ltl::formula* f = 0,
const tgba* aut_neg_f = 0); const tgba* aut_neg_f = 0);
/// @} /// @}
} }