Commit 8e685e00 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

deprecate copy() in favor of make_twa_graph()

Fixes #258.

* spot/twaalgos/copy.cc: Delete, and move the code...
* spot/twa/twagraph.cc: ... in some anonymous namespace here.
* spot/twa/twagraph.hh: Adjust the make_twa_graph() overload.
* spot/twaalgos/copy.hh, NEWS: Mark copy() as deprecated and redirect
to make_twa_graph().
* doc/org/upgrade2.org, doc/org/tut51.org, python/spot/impl.i,
spot/twaalgos/dot.cc, spot/twaalgos/langmap.cc, tests/core/ikwiad.cc:
Adjust callers.
* spot/twaalgos/Makefile.am: Remove copy.cc.
parent 1e9daa73
...@@ -196,6 +196,9 @@ New in spot 2.3.5.dev (not yet released) ...@@ -196,6 +196,9 @@ New in spot 2.3.5.dev (not yet released)
spot::twa::prop_deterministic() as a deprecated synonym for spot::twa::prop_deterministic() as a deprecated synonym for
spot::twa::prop_universal() to help backward compatibility. spot::twa::prop_universal() to help backward compatibility.
- The spot::copy() function is deprecated. Use
spot::make_twa_graph() instead.
New in spot 2.3.5 (2017-06-22) New in spot 2.3.5 (2017-06-22)
Bugs fixed: Bugs fixed:
......
...@@ -471,7 +471,7 @@ With a small variant of the above code, we could also display the ...@@ -471,7 +471,7 @@ With a small variant of the above code, we could also display the
counterexample on the state space, but only because our state space is counterexample on the state space, but only because our state space is
so small: displaying large state spaces is not sensible. Besides, highlighting so small: displaying large state spaces is not sensible. Besides, highlighting
a run only works on =twa_graph= automata, so we need to convert the a run only works on =twa_graph= automata, so we need to convert the
Kripke structure to a =twa_graph=: this can be done with =copy()=. But Kripke structure to a =twa_graph=: this can be done with =make_twa_graph()=. But
now =k= is no longer a Kripke structure (also not generated now =k= is no longer a Kripke structure (also not generated
on-the-fly anymore), so the =print_dot()= function will display it as on-the-fly anymore), so the =print_dot()= function will display it as
a classical automaton with conditions on edges rather than state: a classical automaton with conditions on edges rather than state:
...@@ -493,7 +493,6 @@ passing the option "~k~" to =print_dot()= will fix that. ...@@ -493,7 +493,6 @@ passing the option "~k~" to =print_dot()= will fix that.
#include <spot/twaalgos/translate.hh> #include <spot/twaalgos/translate.hh>
#include <spot/twa/twaproduct.hh> #include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/emptiness.hh> #include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/copy.hh>
<<demo-3-aux>> <<demo-3-aux>>
int main() int main()
{ {
...@@ -509,8 +508,9 @@ passing the option "~k~" to =print_dot()= will fix that. ...@@ -509,8 +508,9 @@ passing the option "~k~" to =print_dot()= will fix that.
spot::twa_graph_ptr af = spot::translator(d).run(f); spot::twa_graph_ptr af = spot::translator(d).run(f);
// Convert demo_kripke into an explicit graph // Convert demo_kripke into an explicit graph
spot::twa_graph_ptr k = spot::copy(std::make_shared<demo_kripke>(d), spot::twa_graph_ptr k =
spot::twa::prop_set::all(), true); spot::make_twa_graph(std::make_shared<demo_kripke>(d),
spot::twa::prop_set::all(), true);
// Find a run of or demo_kripke that intersects af. // Find a run of or demo_kripke that intersects af.
if (auto run = k->intersecting_run(af)) if (auto run = k->intersecting_run(af))
{ {
...@@ -518,14 +518,14 @@ passing the option "~k~" to =print_dot()= will fix that. ...@@ -518,14 +518,14 @@ passing the option "~k~" to =print_dot()= will fix that.
spot::print_dot(std::cout, k, ".k"); spot::print_dot(std::cout, k, ".k");
} }
} }
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results #+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results
$txt $txt
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
[[file:kripke-3.png]] [[file:kripke-3.png]]
* Possible improvements * Possible improvements
......
...@@ -263,7 +263,7 @@ that provide a function with a similar service. ...@@ -263,7 +263,7 @@ that provide a function with a similar service.
| ~tgbaalgos/dtbasat.hh~ | ~spot/twaalgos/dtbasat.hh~ | | | ~tgbaalgos/dtbasat.hh~ | ~spot/twaalgos/dtbasat.hh~ | |
| ~tgbaalgos/dtgbacomp.hh~ | ~spot/twaalgos/complement.hh~ | | | ~tgbaalgos/dtgbacomp.hh~ | ~spot/twaalgos/complement.hh~ | |
| ~tgbaalgos/dtgbasat.hh~ | ~spot/twaalgos/dtwasat.hh~ | | | ~tgbaalgos/dtgbasat.hh~ | ~spot/twaalgos/dtwasat.hh~ | |
| ~tgbaalgos/dupexp.hh~ | ~spot/twaalgos/copy.hh~ | also a copy constructor of twa | | ~tgbaalgos/dupexp.hh~ | ~spot/twaalgos/twagraph.hh~ | constructor of twa_graph |
| ~tgbaalgos/eltl2tgba_lacim.hh~ | | not supported anymore | | ~tgbaalgos/eltl2tgba_lacim.hh~ | | not supported anymore |
| ~tgbaalgos/emptiness.hh~ | ~spot/twaalgos/emptiness.hh~ | | | ~tgbaalgos/emptiness.hh~ | ~spot/twaalgos/emptiness.hh~ | |
| ~tgbaalgos/emptiness_stats.hh~ | ~spot/twaalgos/emptiness_stats.hh~ | | | ~tgbaalgos/emptiness_stats.hh~ | ~spot/twaalgos/emptiness_stats.hh~ | |
...@@ -615,7 +615,7 @@ for (auto i: aut->succ(s)) ...@@ -615,7 +615,7 @@ for (auto i: aut->succ(s))
| ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata | | ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata |
| ~dtgba_complement()~ | ~dtwa_complement()~ | | | ~dtgba_complement()~ | ~dtwa_complement()~ | |
| ~dupexp_bfs()~ | | deleted | | ~dupexp_bfs()~ | | deleted |
| ~dupexp_dfs()~ | ~copy()~ | | | ~dupexp_dfs()~ | ~make_twa_graph()~ | |
| ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | | | ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | |
| ~emptiness_check_instantiator::construct()~ | ~make_emptiness_check_instantiator()~ | | | ~emptiness_check_instantiator::construct()~ | ~make_emptiness_check_instantiator()~ | |
| ~emptiness_check_instantiator::max_acceptance_conditions()~ | ~emptiness_check_instantiator::max_sets()~ | | | ~emptiness_check_instantiator::max_acceptance_conditions()~ | ~emptiness_check_instantiator::max_sets()~ | |
......
...@@ -121,7 +121,6 @@ ...@@ -121,7 +121,6 @@
#include <spot/twaalgos/degen.hh> #include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/dot.hh> #include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/dualize.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/complete.hh> #include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/emptiness.hh> #include <spot/twaalgos/emptiness.hh>
...@@ -537,7 +536,6 @@ def state_is_accepting(self, src) -> "bool": ...@@ -537,7 +536,6 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/cleanacc.hh> %include <spot/twaalgos/cleanacc.hh>
%include <spot/twaalgos/degen.hh> %include <spot/twaalgos/degen.hh>
%include <spot/twaalgos/dot.hh> %include <spot/twaalgos/dot.hh>
%include <spot/twaalgos/copy.hh>
%include <spot/twaalgos/complete.hh> %include <spot/twaalgos/complete.hh>
%feature("flatnested") spot::twa_run::step; %feature("flatnested") spot::twa_run::step;
%include <spot/twaalgos/emptiness.hh> %include <spot/twaalgos/emptiness.hh>
......
...@@ -20,6 +20,7 @@ ...@@ -20,6 +20,7 @@
#include <spot/twa/twagraph.hh> #include <spot/twa/twagraph.hh>
#include <spot/tl/print.hh> #include <spot/tl/print.hh>
#include <vector> #include <vector>
#include <deque>
namespace spot namespace spot
{ {
...@@ -715,4 +716,136 @@ namespace spot ...@@ -715,4 +716,136 @@ namespace spot
set_named_prop("state-names", names.release()); set_named_prop("state-names", names.release());
} }
namespace
{
twa_graph_ptr
copy(const const_twa_ptr& aut, twa::prop_set p,
bool preserve_names, unsigned max_states)
{
twa_graph_ptr out = make_twa_graph(aut->get_dict());
out->copy_acceptance_of(aut);
out->copy_ap_of(aut);
out->prop_copy(aut, p);
std::vector<std::string>* names = nullptr;
std::set<unsigned>* incomplete = nullptr;
// Old highlighting maps
typedef std::map<unsigned, unsigned> hmap;
hmap* ohstates = nullptr;
hmap* ohedges = nullptr;
const_twa_graph_ptr aut_g = nullptr;
// New highlighting maps
hmap* nhstates = nullptr;
hmap* nhedges = nullptr;
if (preserve_names)
{
names = new std::vector<std::string>;
out->set_named_prop("state-names", names);
// If the input is a twa_graph and we were asked to preserve
// names, also preserve highlights.
aut_g = std::dynamic_pointer_cast<const twa_graph>(aut);
if (aut_g)
{
ohstates = aut->get_named_prop<hmap>("highlight-states");
if (ohstates)
nhstates = out->get_or_set_named_prop<hmap>("highlight-states");
ohedges = aut->get_named_prop<hmap>("highlight-edges");
if (ohedges)
nhedges = out->get_or_set_named_prop<hmap>("highlight-edges");
}
}
// States already seen.
state_map<unsigned> seen;
// States to process
std::deque<state_map<unsigned>::const_iterator> todo;
auto new_state = [&](const state* s) -> unsigned
{
auto p = seen.emplace(s, 0);
if (p.second)
{
p.first->second = out->new_state();
todo.emplace_back(p.first);
if (names)
names->emplace_back(aut->format_state(s));
if (ohstates)
{
auto q = ohstates->find(aut_g->state_number(s));
if (q != ohstates->end())
nhstates->emplace(p.first->second, q->second);
}
}
else
{
s->destroy();
}
return p.first->second;
};
out->set_init_state(new_state(aut->get_init_state()));
while (!todo.empty())
{
const state* src1;
unsigned src2;
std::tie(src1, src2) = *todo.front();
todo.pop_front();
for (auto* t: aut->succ(src1))
{
unsigned edgenum = 0;
if (SPOT_UNLIKELY(max_states < out->num_states()))
{
// If we have reached the max number of state, never try
// to create a new one.
auto i = seen.find(t->dst());
if (i == seen.end())
{
if (!incomplete)
incomplete = new std::set<unsigned>;
incomplete->insert(src2);
continue;
}
edgenum = out->new_edge(src2, i->second, t->cond(), t->acc());
}
else
{
edgenum = out->new_edge(src2, new_state(t->dst()),
t->cond(), t->acc());
}
if (ohedges)
{
auto q = ohedges->find(aut_g->edge_number(t));
if (q != ohedges->end())
nhedges->emplace(edgenum, q->second);
}
}
}
auto s = seen.begin();
while (s != seen.end())
{
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
ptr->destroy();
}
if (incomplete)
out->set_named_prop("incomplete-states", incomplete);
return out;
}
}
twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, twa::prop_set p,
bool preserve_names, unsigned max_states)
{
if (max_states == -1U && !preserve_names)
if (auto a = std::dynamic_pointer_cast<const twa_graph>(aut))
return std::make_shared<twa_graph>(a, p);
return copy(aut, p, preserve_names, max_states);
}
} }
...@@ -23,7 +23,6 @@ ...@@ -23,7 +23,6 @@
#include <spot/graph/ngraph.hh> #include <spot/graph/ngraph.hh>
#include <spot/twa/bdddict.hh> #include <spot/twa/bdddict.hh>
#include <spot/twa/twa.hh> #include <spot/twa/twa.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/tl/formula.hh> #include <spot/tl/formula.hh>
#include <sstream> #include <sstream>
...@@ -612,30 +611,42 @@ namespace spot ...@@ -612,30 +611,42 @@ namespace spot
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states); void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
}; };
/// \ingroup twa
/// \brief Build an explicit automaton from all states of \a aut,
inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict) inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict)
{ {
return std::make_shared<twa_graph>(dict); return std::make_shared<twa_graph>(dict);
} }
/// \ingroup twa
/// \brief Build an explicit automaton from all states of \a aut,
inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut, inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut,
twa::prop_set p) twa::prop_set p)
{ {
return std::make_shared<twa_graph>(aut, p); return std::make_shared<twa_graph>(aut, p);
} }
/// \ingroup twa
/// \brief Build an explicit automaton from all states of \a aut,
inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut, inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut,
twa::prop_set p) twa::prop_set p)
{ {
return std::make_shared<twa_graph>(aut, p); return std::make_shared<twa_graph>(aut, p);
} }
inline twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, /// \ingroup twa
twa::prop_set p) /// \brief Build an explicit automaton from all states of \a aut,
{ ///
auto a = std::dynamic_pointer_cast<const twa_graph>(aut); /// This overload works using the abstract interface for automata.
if (a) ///
return std::make_shared<twa_graph>(a, p); /// Set \a preserve_names to preserve state names, and set \a max_states
else /// to a maximum number of states to keep. States with successors that
return copy(aut, p); /// have not been kept will be marked as incomplete; this is mostly useful
} /// to display a subset of a large state space.
SPOT_API twa_graph_ptr
make_twa_graph(const const_twa_ptr& aut, twa::prop_set p,
bool preserve_names = false,
// parentheses for SWIG, see
// https://github.com/swig/swig/issues/993
unsigned max_states = -(1U));
} }
...@@ -98,7 +98,6 @@ libtwaalgos_la_SOURCES = \ ...@@ -98,7 +98,6 @@ libtwaalgos_la_SOURCES = \
complete.cc \ complete.cc \
complement.cc \ complement.cc \
compsusp.cc \ compsusp.cc \
copy.cc \
cycles.cc \ cycles.cc \
degen.cc \ degen.cc \
determinize.cc \ determinize.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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/>.
#include <spot/twaalgos/copy.hh>
#include <spot/twa/twagraph.hh>
#include <deque>
namespace spot
{
twa_graph_ptr
copy(const const_twa_ptr& aut, twa::prop_set p,
bool preserve_names, unsigned max_states)
{
twa_graph_ptr out = make_twa_graph(aut->get_dict());
out->copy_acceptance_of(aut);
out->copy_ap_of(aut);
out->prop_copy(aut, p);
std::vector<std::string>* names = nullptr;
std::set<unsigned>* incomplete = nullptr;
// Old highlighting maps
typedef std::map<unsigned, unsigned> hmap;
hmap* ohstates = nullptr;
hmap* ohedges = nullptr;
const_twa_graph_ptr aut_g = nullptr;
// New highlighting maps
hmap* nhstates = nullptr;
hmap* nhedges = nullptr;
if (preserve_names)
{
names = new std::vector<std::string>;
out->set_named_prop("state-names", names);
// If the input is a twa_graph and we were asked to preserve
// names, also preserve highlights.
aut_g = std::dynamic_pointer_cast<const twa_graph>(aut);
if (aut_g)
{
ohstates = aut->get_named_prop<hmap>("highlight-states");
if (ohstates)
nhstates = out->get_or_set_named_prop<hmap>("highlight-states");
ohedges = aut->get_named_prop<hmap>("highlight-edges");
if (ohedges)
nhedges = out->get_or_set_named_prop<hmap>("highlight-edges");
}
}
// States already seen.
state_map<unsigned> seen;
// States to process
std::deque<state_map<unsigned>::const_iterator> todo;
auto new_state = [&](const state* s) -> unsigned
{
auto p = seen.emplace(s, 0);
if (p.second)
{
p.first->second = out->new_state();
todo.emplace_back(p.first);
if (names)
names->emplace_back(aut->format_state(s));
if (ohstates)
{
auto q = ohstates->find(aut_g->state_number(s));
if (q != ohstates->end())
nhstates->emplace(p.first->second, q->second);
}
}
else
{
s->destroy();
}
return p.first->second;
};
out->set_init_state(new_state(aut->get_init_state()));
while (!todo.empty())
{
const state* src1;
unsigned src2;
std::tie(src1, src2) = *todo.front();
todo.pop_front();
for (auto* t: aut->succ(src1))
{
unsigned edgenum = 0;
if (SPOT_UNLIKELY(max_states < out->num_states()))
{
// If we have reached the max number of state, never try
// to create a new one.
auto i = seen.find(t->dst());
if (i == seen.end())
{
if (!incomplete)
incomplete = new std::set<unsigned>;
incomplete->insert(src2);
continue;
}
edgenum = out->new_edge(src2, i->second, t->cond(), t->acc());
}
else
{
edgenum =
out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc());
}
if (ohedges)
{
auto q = ohedges->find(aut_g->edge_number(t));
if (q != ohedges->end())
nhedges->emplace(edgenum, q->second);
}
}
}
auto s = seen.begin();
while (s != seen.end())
{
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
ptr->destroy();
}
if (incomplete)
out->set_named_prop("incomplete-states", incomplete);
return out;
}
}
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Copyright (C) 2012-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
...@@ -23,18 +23,20 @@ ...@@ -23,18 +23,20 @@
#pragma once #pragma once
#include <spot/misc/common.hh> #include <spot/misc/common.hh>
#include <spot/twa/fwd.hh> #include <spot/twa/twagraph.hh>
#include <spot/twa/twa.hh>
namespace spot namespace spot
{ {
/// \ingroup twa_misc /// \ingroup twa_misc
/// \brief Build an explicit automaton from all states of \a aut, /// \brief Build an explicit automaton from all states of \a aut,
/// ///
/// This works using the abstract interface for automata. If you /// This function was deprecated in Spot 2.4. Use the
/// have a twa_graph that you want to copy, it is more efficient /// function make_twa_graph() instead.
/// to call make_twa_graph() instead. SPOT_DEPRECATED("use make_twa_graph() instead")
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
copy(const const_twa_ptr& aut, twa::prop_set p, inline copy(const const_twa_ptr& aut, twa::prop_set p,
bool preserve_names = false, unsigned max_states = -1U); bool preserve_names = false, unsigned max_states = -1U)
{
return make_twa_graph(aut, p, preserve_names, max_states);
}
} }
...@@ -30,7 +30,6 @@ ...@@ -30,7 +30,6 @@
#include <spot/misc/escape.hh> #include <spot/misc/escape.hh>
#include <spot/twa/twagraph.hh> #include <spot/twa/twagraph.hh>
#include <spot/twa/formula2bdd.hh> #include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
#include <spot/kripke/fairkripke.hh> #include <spot/kripke/fairkripke.hh>
#include <cstdlib> #include <cstdlib>
...@@ -833,7 +832,7 @@ namespace spot ...@@ -833,7 +832,7 @@ namespace spot
d.parse_opts("k"); d.parse_opts("k");
auto aut = std::dynamic_pointer_cast<const twa_graph>(g); auto aut = std::dynamic_pointer_cast<const twa_graph>(g);
if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states())) if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states()))
aut = copy(g, twa::prop_set::all(), true, d.max_states() - 1); aut = make_twa_graph(g, twa::prop_set::all(), true, d.max_states() - 1);
d.print(aut); d.print(aut);
return os; return os;
} }
......
...@@ -19,7 +19,6 @@ ...@@ -19,7 +19,6 @@
#include <numeric> #include <numeric>
#include <spot/twa/twa.hh>