Commit bfd6d57a authored by Etienne Renault's avatar Etienne Renault
Browse files

Promote use of shared_ptr

* spot/kripke/kripke.hh, spot/ltsmin/ltsmin.cc,
spot/ltsmin/ltsmin.hh, spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/utils.hh, spot/twacube/Makefile.am,
spot/twacube/fwd.hh, spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc, tests/ltsmin/modelcheck.cc: here.
parent e4fb84b8
......@@ -21,6 +21,7 @@
#include <spot/kripke/fairkripke.hh>
#include <spot/twacube/cube.hh>
#include <memory>
namespace spot
{
......@@ -33,7 +34,8 @@ namespace spot
/// are provided by this template class. Specialisations
/// will handle it.
template<typename State, typename SuccIterator>
class SPOT_API kripkecube
class SPOT_API kripkecube:
public std::enable_shared_from_this<kripkecube<State, SuccIterator>>
{
public:
/// \brief Returns the initial State of the System
......
......@@ -1933,7 +1933,7 @@ namespace spot
throw std::runtime_error(err.str());
}
spot::kripkecube<spot::cspins_state, spot::cspins_iterator>*
ltsmin_kripkecube_ptr
ltsmin_model::kripkecube(const atomic_prop_set* to_observe,
const formula dead, int compress) const
{
......@@ -1970,7 +1970,8 @@ namespace spot
observed.push_back(dead_ap);
// Finally build the system.
return new spot::kripkecube<spot::cspins_state, spot::cspins_iterator>
return std::make_shared<spot::kripkecube<spot::cspins_state,
spot::cspins_iterator>>
(iface, compress, observed, selfloopize, dead_ap);
}
......@@ -2006,9 +2007,8 @@ namespace spot
}
std::tuple<bool, std::string, istats>
ltsmin_model::modelcheck(spot::kripkecube<spot::cspins_state,
spot::cspins_iterator>* sys,
spot::twacube* twa, bool compute_ctrx)
ltsmin_model::modelcheck(ltsmin_kripkecube_ptr sys,
spot::twacube_ptr twa, bool compute_ctrx)
{
ec_renault13lpar<cspins_state, cspins_iterator,
cspins_state_hash, cspins_state_equal> ec(*sys, twa);
......
......@@ -31,6 +31,10 @@ namespace spot
class cspins_iterator;
typedef int* cspins_state;
typedef std::shared_ptr<spot::kripkecube<spot::cspins_state,
spot::cspins_iterator>>
ltsmin_kripkecube_ptr;
class SPOT_API ltsmin_model final
{
public:
......@@ -79,7 +83,7 @@ namespace spot
// \brief The same as above but returns a kripkecube, i.e. a kripke
// that can be use in parallel. Moreover, it support more ellaborated
// atomic propositions such as "P.a == P.c"
spot::kripkecube<spot::cspins_state, spot::cspins_iterator>*
ltsmin_kripkecube_ptr
kripkecube(const atomic_prop_set* to_observe,
formula dead = formula::tt(),
int compress = 0) const;
......@@ -89,8 +93,8 @@ namespace spot
/// has been found and a string representing the counterexample if the
/// computation have been required
static std::tuple<bool, std::string, istats>
modelcheck(spot::kripkecube<spot::cspins_state, spot::cspins_iterator>* sys,
spot::twacube* twa, bool compute_ctrx = false);
modelcheck(ltsmin_kripkecube_ptr sys,
spot::twacube_ptr twa, bool compute_ctrx = false);
/// Number of variables in a state
int state_size() const;
......
......@@ -45,7 +45,7 @@ namespace spot
public:
ec_renault13lpar(kripkecube<State, SuccIterator>& sys,
twacube* twa)
twacube_ptr twa)
: intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
......
......@@ -59,7 +59,7 @@ namespace spot
{
public:
intersect(kripkecube<State, SuccIterator>& sys,
twacube* twa):
twacube_ptr twa):
sys_(sys), twa_(twa)
{
assert(is_a_kripkecube(sys));
......@@ -254,7 +254,7 @@ namespace spot
std::shared_ptr<trans_index> it_prop;
};
kripkecube<State, SuccIterator>& sys_;
twacube* twa_;
twacube_ptr twa_;
std::vector<todo_element> todo;
typedef std::unordered_map<const product_state, int,
product_state_hash,
......
......@@ -95,7 +95,6 @@ namespace spot
std::vector<std::string>* names_;
bdd_dict_ptr dict_;
std::unordered_map<int, int> reverse_binder_;
};
......@@ -116,7 +115,7 @@ namespace spot
public:
product_to_twa(kripkecube<State, SuccIterator>& sys,
twacube* twa)
twacube_ptr twa)
: intersect<State, SuccIterator, StateHash, StateEqual,
product_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys, twa)
......@@ -143,7 +142,6 @@ namespace spot
for (auto ap : this->twa_->get_ap())
{
auto idx = res_->register_ap(ap);
std::cout << ap << idx << std::endl;
reverse_binder_[i++] = idx;
}
}
......
......@@ -25,7 +25,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
twacubedir = $(pkgincludedir)/twacube
twacube_HEADERS = cube.hh twacube.hh
twacube_HEADERS = cube.hh twacube.hh fwd.hh
noinst_LTLIBRARIES = libtwacube.la
libtwacube_la_SOURCES = \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2016 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#pragma once
#include <memory>
namespace spot
{
class twacube;
typedef std::shared_ptr<twacube> twacube_ptr;
typedef std::shared_ptr<const twacube> const_twacube_ptr;
}
......@@ -24,6 +24,7 @@
#include <spot/graph/graph.hh>
#include <spot/twa/acc.hh>
#include <spot/twacube/cube.hh>
#include <spot/twacube/fwd.hh>
namespace spot
{
......@@ -101,7 +102,7 @@ namespace spot
const graph_t::state_storage_t& st_;
};
class SPOT_API twacube final
class SPOT_API twacube final: public std::enable_shared_from_this<twacube>
{
public:
twacube() = delete;
......@@ -150,4 +151,9 @@ namespace spot
graph_t theg_;
cubeset cubeset_;
};
inline twacube_ptr make_twacube(const std::vector<std::string> aps)
{
return std::make_shared<twacube>(aps);
}
}
......@@ -59,14 +59,14 @@ namespace spot
return result;
}
spot::twacube* twa_to_twacube(const spot::const_twa_graph_ptr aut)
spot::twacube_ptr twa_to_twacube(const spot::const_twa_graph_ptr aut)
{
// Compute the necessary binder and extract atomic propositions
std::unordered_map<int, int> ap_binder;
std::vector<std::string>* aps = extract_aps(aut, ap_binder);
// Declare the twa cube
spot::twacube* tg = new spot::twacube(*aps);
auto tg = spot::make_twacube(*aps);
// Fix acceptance
tg->acc() = aut->acc();
......@@ -135,7 +135,7 @@ namespace spot
}
spot::twa_graph_ptr
twacube_to_twa(spot::twacube* twacube)
twacube_to_twa(spot::twacube_ptr twacube)
{
// Grab necessary variables
auto& theg = twacube->get_graph();
......
......@@ -47,10 +47,10 @@ namespace spot
std::unordered_map<int, int>& ap_binder);
/// \brief Convert a twa into a twacube
SPOT_API spot::twacube*
SPOT_API twacube_ptr
twa_to_twacube(spot::const_twa_graph_ptr aut);
/// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube* twacube);
twacube_to_twa(spot::twacube_ptr twacube);
}
......@@ -47,7 +47,7 @@ int main()
tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1}));
// Test translation
auto* aut = twa_to_twacube(tg);
auto aut = twa_to_twacube(tg);
spot::print_dot(std::cout, tg);
std::cout << "-----------\n" << *aut << "-----------\n";
......@@ -62,7 +62,5 @@ int main()
<< ' ' << d.acc_
<< std::endl;
}
spot::print_dot(std::cout, spot::twacube_to_twa(aut));
delete aut;
}
......@@ -371,12 +371,11 @@ static int checked_main()
<< ". This could slow down parallel algorithms.\n";
tm.start("twa to twacube");
auto* propcube = spot::twa_to_twacube(prop);
auto propcube = spot::twa_to_twacube(prop);
tm.stop("twa to twacube");
tm.start("load kripkecube");
spot::kripkecube<spot::cspins_state,
spot::cspins_iterator>* modelcube = nullptr;
spot::ltsmin_kripkecube_ptr modelcube = nullptr;
try
{
modelcube = spot::ltsmin_model::load(mc_options.model)
......@@ -397,7 +396,6 @@ static int checked_main()
if (!modelcube)
{
delete propcube;
exit_code = 2;
goto safe_exit;
}
......@@ -423,8 +421,6 @@ static int checked_main()
else
std::cout << "an accepting run exists!\n" << std::get<1>(res)
<< std::endl;
delete modelcube;
delete propcube;
}
safe_exit:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment