Create unique_ptr for Spot.
* src/misc/unique_ptr.hh: Create unique_ptr for Spot. * src/misc/Makefile.am: Register this new file. * src/tgbatest/ltl2tgba.cc: Replace two calls to delete by the utilisation of unique_ptr. * src/tgbaalgos/simulation.cc: Replace two calls to delete by the utilisation of unique_ptr.
This commit is contained in:
parent
b23296cf61
commit
f01d30eb91
4 changed files with 91 additions and 11 deletions
|
|
@ -52,6 +52,7 @@ misc_HEADERS = \
|
||||||
optionmap.hh \
|
optionmap.hh \
|
||||||
random.hh \
|
random.hh \
|
||||||
timer.hh \
|
timer.hh \
|
||||||
|
unique_ptr.hh \
|
||||||
version.hh
|
version.hh
|
||||||
|
|
||||||
noinst_LTLIBRARIES = libmisc.la
|
noinst_LTLIBRARIES = libmisc.la
|
||||||
|
|
|
||||||
83
src/misc/unique_ptr.hh
Normal file
83
src/misc/unique_ptr.hh
Normal file
|
|
@ -0,0 +1,83 @@
|
||||||
|
// -*- coding: utf-8 -*-
|
||||||
|
// Copyright (C) 2012 Laboratoire de Recherche et
|
||||||
|
// Développement de l'Epita (LRDE).
|
||||||
|
//
|
||||||
|
// This file is part of Spot, a model checking library.
|
||||||
|
//
|
||||||
|
// Spot is free software; you can redistribute it and/or modify it
|
||||||
|
// under the terms of the GNU General Public License as published by
|
||||||
|
// the Free Software Foundation; either version 2 of the License, or
|
||||||
|
// (at your option) any later version.
|
||||||
|
//
|
||||||
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||||
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||||
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||||
|
// License for more details.
|
||||||
|
//
|
||||||
|
// You should have received a copy of the GNU General Public License
|
||||||
|
// along with Spot; see the file COPYING. If not, write to the Free
|
||||||
|
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
|
// 02111-1307, USA.
|
||||||
|
|
||||||
|
#ifndef SPOT_MISC_UNIQUE_PTR_HH
|
||||||
|
# define SPOT_MISC_UNIQUE_PTR_HH
|
||||||
|
|
||||||
|
namespace spot
|
||||||
|
{
|
||||||
|
/// \brief Take ownership of a pointer at its construction, and
|
||||||
|
/// destroy it at the end of the scope.
|
||||||
|
template <typename T>
|
||||||
|
class unique_ptr
|
||||||
|
{
|
||||||
|
typedef T* pointer;
|
||||||
|
public:
|
||||||
|
unique_ptr(pointer ptr)
|
||||||
|
: ptr_(ptr)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
~unique_ptr()
|
||||||
|
{
|
||||||
|
delete ptr_;
|
||||||
|
}
|
||||||
|
|
||||||
|
operator pointer()
|
||||||
|
{
|
||||||
|
return ptr_;
|
||||||
|
}
|
||||||
|
|
||||||
|
pointer
|
||||||
|
operator->()
|
||||||
|
{
|
||||||
|
return ptr_;
|
||||||
|
}
|
||||||
|
|
||||||
|
private:
|
||||||
|
pointer ptr_;
|
||||||
|
|
||||||
|
// This copy gives the ownership of the pointer to the new copy.
|
||||||
|
// Can only be used by make_unique.
|
||||||
|
unique_ptr(const unique_ptr& up)
|
||||||
|
{
|
||||||
|
unique_ptr& non_const_up = const_cast<unique_ptr&>(up);
|
||||||
|
ptr_ = non_const_up.ptr_;
|
||||||
|
non_const_up.ptr_ = 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Allow `make_unique' to have an access to the private copy.
|
||||||
|
template <typename V> friend unique_ptr<V> make_unique(V* ptr);
|
||||||
|
|
||||||
|
unique_ptr& operator=(const unique_ptr&);
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
/// \brief Change a pointer into a unique_ptr.
|
||||||
|
template <typename T>
|
||||||
|
inline unique_ptr<T> make_unique(T* ptr)
|
||||||
|
{
|
||||||
|
return unique_ptr<T>(ptr);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
#endif // !SPOT_MISC_UNIQUE_PTR_HH
|
||||||
|
|
@ -26,6 +26,7 @@
|
||||||
#include "simulation.hh"
|
#include "simulation.hh"
|
||||||
#include "misc/acccompl.hh"
|
#include "misc/acccompl.hh"
|
||||||
#include "misc/minato.hh"
|
#include "misc/minato.hh"
|
||||||
|
#include "misc/unique_ptr.hh"
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
#include "tgbaalgos/reachiter.hh"
|
#include "tgbaalgos/reachiter.hh"
|
||||||
#include "tgbaalgos/sccfilter.hh"
|
#include "tgbaalgos/sccfilter.hh"
|
||||||
|
|
@ -702,7 +703,6 @@ namespace spot
|
||||||
state* initial_state;
|
state* initial_state;
|
||||||
|
|
||||||
automaton_size stat;
|
automaton_size stat;
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
} // End namespace anonymous.
|
} // End namespace anonymous.
|
||||||
|
|
@ -735,21 +735,18 @@ namespace spot
|
||||||
prev = next;
|
prev = next;
|
||||||
direct_simulation<false> simul(res);
|
direct_simulation<false> simul(res);
|
||||||
|
|
||||||
tgba* after_simulation = simul.run();
|
unique_ptr<tgba> after_simulation(simul.run());
|
||||||
|
|
||||||
if (res != t)
|
if (res != t)
|
||||||
delete res;
|
delete res;
|
||||||
|
|
||||||
direct_simulation<true> cosimul(after_simulation);
|
direct_simulation<true> cosimul(after_simulation);
|
||||||
|
|
||||||
tgba* after_cosimulation = cosimul.run();
|
unique_ptr<tgba> after_cosimulation(cosimul.run());
|
||||||
|
|
||||||
next = cosimul.get_stat();
|
next = cosimul.get_stat();
|
||||||
|
|
||||||
res = scc_filter(after_cosimulation, false);
|
res = scc_filter(after_cosimulation, false);
|
||||||
|
|
||||||
delete after_cosimulation;
|
|
||||||
delete after_simulation;
|
|
||||||
}
|
}
|
||||||
while (prev != next);
|
while (prev != next);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -59,6 +59,7 @@
|
||||||
#include "tgbaalgos/gtec/gtec.hh"
|
#include "tgbaalgos/gtec/gtec.hh"
|
||||||
#include "eltlparse/public.hh"
|
#include "eltlparse/public.hh"
|
||||||
#include "misc/timer.hh"
|
#include "misc/timer.hh"
|
||||||
|
#include "misc/unique_ptr.hh"
|
||||||
#include "tgbaalgos/stats.hh"
|
#include "tgbaalgos/stats.hh"
|
||||||
#include "tgbaalgos/scc.hh"
|
#include "tgbaalgos/scc.hh"
|
||||||
#include "tgbaalgos/emptiness_stats.hh"
|
#include "tgbaalgos/emptiness_stats.hh"
|
||||||
|
|
@ -1364,9 +1365,8 @@ main(int argc, char** argv)
|
||||||
// It is possible that we have applied other
|
// It is possible that we have applied other
|
||||||
// operations to the automaton since its initial
|
// operations to the automaton since its initial
|
||||||
// degeneralization. Let's degeneralize again!
|
// degeneralization. Let's degeneralize again!
|
||||||
spot::tgba* s = spot::degeneralize(a);
|
spot::unique_ptr<spot::tgba> s(spot::degeneralize(a));
|
||||||
spot::never_claim_reachable(std::cout, s, f, spin_comments);
|
spot::never_claim_reachable(std::cout, s, f, spin_comments);
|
||||||
delete s;
|
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
@ -1562,10 +1562,9 @@ main(int argc, char** argv)
|
||||||
}
|
}
|
||||||
else if (graph_run_tgba_opt)
|
else if (graph_run_tgba_opt)
|
||||||
{
|
{
|
||||||
spot::tgba* ar =
|
spot::unique_ptr<spot::tgba>
|
||||||
spot::tgba_run_to_tgba(a, run);
|
ar(spot::tgba_run_to_tgba(a, run));
|
||||||
spot::dotty_reachable(std::cout, ar, false);
|
spot::dotty_reachable(std::cout, ar, false);
|
||||||
delete ar;
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue