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

Use the degeneralization unicity_table in more places.

Browse source 
* src/tgbaalgos/degen.cc (unicity_table): Move and rename as...
* src/tgba/state.hh (state_unicity_table): ... this.
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/cycles.cc,
src/tgbaalgos/cycles.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/safety.cc: Use it to simplify existing code.
This commit is contained in:
Alexandre Duret-Lutz 2014-01-23 21:42:51 +01:00
parent c7b3148cb4
commit 2f71741575
9 changed files with 100 additions and 161 deletions
Download patch file Download diff file Expand all files Collapse all files

60
src/tgba/state.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
// Copyright (C) 2009, 2011, 2013, 2014 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é
@ -176,6 +176,64 @@ namespace spot
state_ptr_hash, state_ptr_equal> state_set;
/// \ingroup tgba_essentials
/// \brief Render state pointers unique via a hash table.
class SPOT_API state_unicity_table
{
state_set m;
public:
/// \brief Canonicalize state pointer.
///
/// If this is the first time a state is seen, this return the
/// state pointer as-is, otherwise it frees the state and returns
/// a point to the previously seen copy.
///
/// States are owned by the table and will be freed on
/// destruction.
const state* operator()(const state* s)
{
auto p = m.insert(s);
if (!p.second)
s->destroy();
return *p.first;
}
/// \brief Canonicalize state pointer.
///
/// Same as operator(), except that a nullptr
/// is returned if the state is not new.
const state* is_new(const state* s)
{
auto p = m.insert(s);
if (!p.second)
{
s->destroy();
return nullptr;
}
return *p.first;
}
~state_unicity_table()
{
for (state_set::iterator i = m.begin(); i != m.end();)
{
// Advance the iterator before destroying its key. This
// avoid issues with old g++ implementations.
state_set::iterator old = i++;
(*old)->destroy();
}
}
size_t
size()
{
return m.size();
}
};
// Functions related to shared_ptr.
//////////////////////////////////////////////////

31
src/tgbaalgos/cutscc.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -33,12 +33,10 @@ namespace spot
const std::set<unsigned>& s)
{
tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict());
state* cur = a->get_init_state();
std::queue<state*> tovisit;
typedef std::unordered_set<const state*,
state_ptr_hash, state_ptr_equal> hash_type;
const state* cur = a->get_init_state();
std::queue<const state*> tovisit;
// Setup
hash_type seen;
state_unicity_table seen;
unsigned scc_number;
std::string cur_format = a->format_state(cur);
std::set<unsigned>::iterator it;
@ -46,8 +44,7 @@ namespace spot
for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it)
continue;
assert(it != s.end());
tovisit.push(cur);
seen.insert(cur);
tovisit.push(seen(cur));
sub_a->add_state(cur_format);
sub_a->copy_acceptance_conditions_of(a);
// If the initial is not part of one of the desired SCC, exit
@ -68,15 +65,8 @@ namespace spot
// Is the successor included in one of the desired SCC ?
if (s.find(scc_number) != s.end())
{
if (seen.find(dst) == seen.end())
{
tovisit.push(dst);
seen.insert(dst); // has_state?
}
else
{
dst->destroy();
}
if (seen.is_new(dst))
tovisit.push(dst);
state_explicit_string::transition* t =
sub_a->create_transition(cur_format, dst_format);
sub_a->add_conditions(t, sit->current_condition());
@ -90,11 +80,6 @@ namespace spot
}
delete sit;
}
hash_type::iterator it2;
// Free visited states.
for (it2 = seen.begin(); it2 != seen.end(); ++it2)
(*it2)->destroy();
return sub_a;
}

9
src/tgbaalgos/cycles.cc
View file

@ -1,4 +1,5 @@
// Copyright (C) 2012 Laboratoire de Recherche et Developpement de
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -47,14 +48,12 @@ namespace spot
q.pop_back();
y->second.mark = false;
for (set_type::iterator i = y->second.b.begin();
i != y->second.b.end(); ++i)
for (auto s: y->second.b)
{
tagged_state x = tags_.find(*i);
tagged_state x = tags_.find(s);
assert(x != tags_.end());
// insert y in A(x)
x->second.del.erase(y->first);
// unmark x recursively if marked
if (x->second.mark)
q.push_back(x);

11
src/tgbaalgos/cycles.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -79,9 +79,6 @@ namespace spot
class SPOT_API enumerate_cycles
{
protected:
typedef std::unordered_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
// Extra information required for the algorithm for each state.
struct state_info
{
@ -98,10 +95,10 @@ namespace spot
// that a contributed to a contributed to a cycle.
bool mark;
// Deleted successors (in the paper, states deleted from A(x))
set_type del;
state_set del;
// Predecessors of the current states, that could not yet
// contribute to a cycle.
set_type b;
state_set b;
};
// Store the state_info for all visited states.

37
src/tgbaalgos/degen.cc
View file

@ -67,37 +67,6 @@ namespace spot
// Queue of state to be processed.
typedef std::deque<degen_state> queue_t;
// Memory management for the input states.
class unicity_table
{
state_set m;
public:
const state* operator()(const state* s)
{
auto p = m.insert(s);
if (!p.second)
s->destroy();
return *p.first;
}
~unicity_table()
{
for (state_set::iterator i = m.begin(); i != m.end();)
{
// Advance the iterator before destroying its key. This
// avoid issues with old g++ implementations.
state_set::iterator old = i++;
(*old)->destroy();
}
}
size_t
size()
{
return m.size();
}
};
// Acceptance set common to all outgoing transitions (of the same
// SCC -- we do not care about the other) of some state.
class outgoing_acc
@ -165,10 +134,10 @@ namespace spot
typedef std::unordered_map<const state*, bool,
state_ptr_hash, state_ptr_equal> cache_t;
cache_t cache_;
unicity_table& uniq_;
state_unicity_table& uniq_;
public:
has_acc_loop(const tgba* a, unicity_table& uniq):
has_acc_loop(const tgba* a, state_unicity_table& uniq):
a_(a),
uniq_(uniq)
{
@ -329,7 +298,7 @@ namespace spot
// Make sure we always use the same pointer for identical states
// from the input automaton.
unicity_table uniq;
state_unicity_table uniq;
// Accepting loop checker, for some heuristics.
has_acc_loop acc_loop(a, uniq);

35
src/tgbaalgos/minimize.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -52,6 +52,8 @@
namespace spot
{
// FIXME: do we really want to use unordered_set instead of set here?
// This calls for benchmarking.
typedef std::unordered_set<const state*,
state_ptr_hash, state_ptr_equal> hash_set;
typedef std::unordered_map<const state*, unsigned,
@ -184,36 +186,13 @@ namespace spot
power_map& pm, const state* dest)
: bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest)
{
seen.insert(dest);
}
virtual
~wdba_search_acc_loop()
{
hash_set::const_iterator i = seen.begin();
while (i != seen.end())
{
hash_set::const_iterator old = i;
++i;
(*old)->destroy();
}
seen(dest);
}
virtual const state*
filter(const state* s)
{
// Use the state from seen.
hash_set::const_iterator i = seen.find(s);
if (i == seen.end())
{
seen.insert(s);
}
else
{
s->destroy();
s = *i;
}
// Ignore states outside SCC #n.
s = seen(s);
if (sm.scc_of_state(s) != scc_n)
return 0;
return s;
@ -229,7 +208,7 @@ namespace spot
scc_map& sm;
power_map& pm;
const state* dest;
hash_set seen;
state_unicity_table seen;
};

12
src/tgbaalgos/powerset.cc
View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
@ -54,8 +55,7 @@ namespace spot
{
power_state ps;
state* s = aut->get_init_state();
pm.states.insert(s);
const state* s = pm.canonicalize(aut->get_init_state());
ps.insert(s);
todo.push_back(ps);
seen[ps] = 1;
@ -325,7 +325,7 @@ namespace spot
tgba_explicit_number* det = tgba_powerset(aut, pm, false);
if ((threshold_states > 0)
&& (pm.map_.size() > pm.states.size() * threshold_states))
&& (pm.map_.size() > pm.states_.size() * threshold_states))
{
delete det;
return 0;

33
src/tgbaalgos/powerset.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -34,21 +34,6 @@ namespace spot
{
typedef std::set<const state*, state_ptr_less_than> power_state;
typedef std::map<int, power_state> power_map_data;
typedef std::unordered_set<const state*, state_ptr_hash,
state_ptr_equal> state_set;
~power_map()
{
// Release all states.
state_set::const_iterator i = states.begin();
while (i != states.end())
{
// Advance the iterator before deleting the key.
const state* s = *i;
++i;
s->destroy();
}
}
const power_state&
states_of(int s) const
@ -59,21 +44,11 @@ namespace spot
const state*
canonicalize(const state* s)
{
state_set::const_iterator i = states.find(s);
if (i != states.end())
{
s->destroy();
s = *i;
}
else
{
states.insert(s);
}
return s;
return states_(s);
}
power_map_data map_;
state_set states;
state_unicity_table states_;
};

33
src/tgbaalgos/safety.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et
// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
@ -72,16 +72,10 @@ namespace spot
bool is_safety_mwdba(const tgba* aut)
{
typedef std::unordered_set<const state*,
state_ptr_hash, state_ptr_equal> seen_map;
seen_map seen; // States already seen.
state_unicity_table seen; // States already seen.
std::deque<const state*> todo; // A queue of states yet to explore.
{
state* s = aut->get_init_state();
todo.push_back(s);
seen.insert(s);
}
todo.push_back(seen(aut->get_init_state()));
bdd all_acc = aut->all_acceptance_conditions();
@ -100,28 +94,11 @@ namespace spot
all_accepting = false;
break;
}
state* d = it->current_state();
if (seen.find(d) != seen.end())
{
d->destroy();
}
else
{
seen.insert(d);
todo.push_back(d);
}
if (const state* d = seen.is_new(it->current_state()))
todo.push_back(d);
}
delete it;
}
seen_map::const_iterator it = seen.begin();
while (it != seen.end())
{
seen_map::const_iterator old = it;
++it;
(*old)->destroy();
}
return all_accepting;
}