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

gtec: replace nsheap by a simple unordered_map

Browse source 
nsheap was an horror full of virtual functions required to
customize gtec to implement inclusion-based emptiness-check
in GreatSPN support.  Since this support has been removed, we
can remove the nsheap cruft as well.  Note that nsheap was
also used in emptinessta for no good reason (the code from
emptinessta was simply copied from gtec without cleanup).

* src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
Delete.
* src/tgbaalgos/gtec/Makefile.am: Adjust.
* src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
src/taalgos/tgba2ta.cc, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
Use a simple unordered_map.
This commit is contained in:
Alexandre Duret-Lutz 2014-01-30 15:02:52 +01:00
parent 46e4408a85
commit 393637f18a
11 changed files with 235 additions and 672 deletions
Download patch file Download diff file Expand all files Collapse all files

168
src/taalgos/emptinessta.cc
View file

@ -58,8 +58,7 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h = hash_type h;
numbered_state_heap_hash_map_factory::instance()->build();
// * num: the number of visited nodes. Used to set the order of each // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
@ -107,13 +106,13 @@ namespace spot
state_ta_product* init = new state_ta_product( state_ta_product* init = new state_ta_product(
(ta_init_it_->current_state()), kripke_init_state->clone()); (ta_init_it_->current_state()), kripke_init_state->clone());
numbered_state_heap::state_index_p h_init = h->find(init); if (!h.insert(std::make_pair(init, num + 1)).second)
{
if (h_init.first) init->destroy();
continue; continue;
}
h->insert(init, ++num); scc.push(++num);
scc.push(num);
arc.push(bddfalse); arc.push(bddfalse);
ta_succ_iterator_product* iter = a_->succ_iter(init); ta_succ_iterator_product* iter = a_->succ_iter(init);
@ -143,29 +142,25 @@ namespace spot
// Backtrack TODO. // Backtrack TODO.
todo.pop(); todo.pop();
dec_depth(); dec_depth();
trace trace << "PASS 1 : backtrack\n";
<< "PASS 1 : backtrack" << std::endl;
if (a_->is_livelock_accepting_state(curr) if (a_->is_livelock_accepting_state(curr)
&& !a_->is_accepting_state(curr)) && !a_->is_accepting_state(curr))
{ {
livelock_acceptance_states_not_found = false; livelock_acceptance_states_not_found = false;
trace trace << "PASS 1 : livelock accepting state found\n";
<< "PASS 1 : livelock accepting state found" << std::endl;
} }
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = auto i = h.find(curr);
h->index(curr->clone()); assert(i != h.end());
assert(spi.first);
scc.rem().push_front(curr); scc.rem().push_front(curr);
inc_depth(); inc_depth();
// set the h value of the Backtracked state to negative value. // set the h value of the Backtracked state to negative value.
// colour[curr] = BLUE; // colour[curr] = BLUE;
*spi.second = -std::abs(*spi.second); i->second = -std::abs(i->second);
// Backtrack livelock_roots. // Backtrack livelock_roots.
if (activate_heuristic && !livelock_roots.empty() if (activate_heuristic && !livelock_roots.empty()
@ -176,21 +171,11 @@ namespace spot
// remove that SSCC from the ROOT stacks. We must // remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC. // discard from H all reachable states from this SSCC.
assert(!scc.empty()); assert(!scc.empty());
if (scc.top().index == std::abs(*spi.second)) if (scc.top().index == std::abs(i->second))
{ {
// removing states // removing states
std::list<state*>::iterator i; for (auto j: scc.rem())
h[j] = -1; //colour[*i] = BLACK;
for (i = scc.rem().begin(); i != scc.rem().end(); ++i)
{
numbered_state_heap::state_index_p spi = h->index(
(*i)->clone());
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
//colour[*i] = BLACK;
}
dec_depth(scc.rem().size()); dec_depth(scc.rem().size());
scc.pop(); scc.pop();
assert(!arc.empty()); assert(!arc.empty());
@ -205,8 +190,7 @@ namespace spot
// We have a successor to look at. // We have a successor to look at.
inc_transitions(); inc_transitions();
trace trace << "PASS 1: transition\n";
<< "PASS 1: transition" << std::endl;
// Fetch the values destination state we are interested in... // Fetch the values destination state we are interested in...
state* dest = succ->current_state(); state* dest = succ->current_state();
@ -232,15 +216,12 @@ namespace spot
// We do not need SUCC from now on. // We do not need SUCC from now on.
// Are we going to a new state? // Are we going to a new state?
numbered_state_heap::state_index_p spi = h->find(dest); auto p = h.insert(std::make_pair(dest, num + 1));
if (p.second)
// Is this a new state?
if (!spi.first)
{ {
// Number it, stack it, and register its successors // Number it, stack it, and register its successors
// for later processing. // for later processing.
h->insert(dest, ++num); scc.push(++num);
scc.push(num);
arc.push(acc_cond); arc.push(acc_cond);
ta_succ_iterator_product* iter = a_->succ_iter(dest); ta_succ_iterator_product* iter = a_->succ_iter(dest);
@ -258,7 +239,7 @@ namespace spot
} }
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (p.first->second == -1)
continue; continue;
// Now this is the most interesting case. We have reached a // Now this is the most interesting case. We have reached a
@ -272,12 +253,11 @@ namespace spot
// ROOT is ascending: we just have to merge all SSCCs from the // ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold"). // the SSCC of S2 (called the "threshold").
int threshold = std::abs(*spi.second); int threshold = std::abs(p.first->second);
std::list<state*> rem; std::list<state*> rem;
bool acc = false; bool acc = false;
trace trace << "***PASS 1: CYCLE***\n";
<< "***PASS 1: CYCLE***" << std::endl;
while (threshold < scc.top().index) while (threshold < scc.top().index)
{ {
@ -311,14 +291,14 @@ namespace spot
{ {
trace trace
<< "PASS 1: SUCCESS: a_->is_livelock_accepting_state(curr): " << "PASS 1: SUCCESS: a_->is_livelock_accepting_state(curr): "
<< a_->is_livelock_accepting_state(curr) << std::endl; << a_->is_livelock_accepting_state(curr) << '\n';
trace trace
<< "PASS 1: scc.top().condition : " << "PASS 1: scc.top().condition : "
<< bdd_format_accset(a_->get_dict(), scc.top().condition) << bdd_format_accset(a_->get_dict(), scc.top().condition)
<< std::endl; << '\n';
trace trace
<< "PASS 1: a_->all_acceptance_conditions() : " << "PASS 1: a_->all_acceptance_conditions() : "
<< (a_->all_acceptance_conditions()) << std::endl; << (a_->all_acceptance_conditions()) << '\n';
trace trace
<< ("PASS 1 CYCLE and (scc.top().condition == " << ("PASS 1 CYCLE and (scc.top().condition == "
"a_->all_acceptance_conditions()) : ") "a_->all_acceptance_conditions()) : ")
@ -327,11 +307,11 @@ namespace spot
trace trace
<< "PASS 1: bddtrue: " << (a_->all_acceptance_conditions() << "PASS 1: bddtrue: " << (a_->all_acceptance_conditions()
== bddtrue) << std::endl; == bddtrue) << '\n';
trace trace
<< "PASS 1: bddfalse: " << (a_->all_acceptance_conditions() << "PASS 1: bddfalse: " << (a_->all_acceptance_conditions()
== bddfalse) << std::endl; == bddfalse) << '\n';
clear(h, todo, ta_init_it_); clear(h, todo, ta_init_it_);
return true; return true;
@ -341,9 +321,8 @@ namespace spot
if (activate_heuristic && a_->is_livelock_accepting_state(curr) if (activate_heuristic && a_->is_livelock_accepting_state(curr)
&& is_stuttering_transition) && is_stuttering_transition)
{ {
trace trace << "PASS 1: heuristic livelock detection \n";
<< "PASS 1: heuristic livelock detection " << std::endl; const state* dest = p.first->first;
const state* dest = spi.first;
std::set<const state*, state_ptr_less_than> liveset_dest = std::set<const state*, state_ptr_less_than> liveset_dest =
liveset[dest]; liveset[dest];
@ -352,7 +331,7 @@ namespace spot
int h_livelock_root = 0; int h_livelock_root = 0;
if (!livelock_roots.empty()) if (!livelock_roots.empty())
h_livelock_root = *(h->find((livelock_roots.top()))).second; h_livelock_root = h[livelock_roots.top()];
if (heuristic_livelock_detection(dest, h, h_livelock_root, if (heuristic_livelock_detection(dest, h, h_livelock_root,
liveset_curr)) liveset_curr))
@ -362,18 +341,13 @@ namespace spot
} }
std::set<const state*, state_ptr_less_than>::const_iterator it; std::set<const state*, state_ptr_less_than>::const_iterator it;
for (it = liveset_dest.begin(); it != liveset_dest.end(); ++it) for (const state* succ: liveset_dest)
{
const state* succ = (*it);
if (heuristic_livelock_detection(succ, h, h_livelock_root, if (heuristic_livelock_detection(succ, h, h_livelock_root,
liveset_curr)) liveset_curr))
{ {
clear(h, todo, ta_init_it_); clear(h, todo, ta_init_it_);
return true; return true;
} }
}
} }
} }
@ -389,26 +363,23 @@ namespace spot
bool bool
ta_check::heuristic_livelock_detection(const state * u, ta_check::heuristic_livelock_detection(const state * u,
numbered_state_heap* h, int h_livelock_root, std::set<const state*, hash_type& h, int h_livelock_root, std::set<const state*,
state_ptr_less_than> liveset_curr) state_ptr_less_than> liveset_curr)
{ {
numbered_state_heap::state_index_p hu = h->find(u); int hu = h[u];
if (*hu.second > 0) // colour[u] == GREY if (hu > 0) // colour[u] == GREY
{ {
if (*hu.second >= h_livelock_root) if (hu >= h_livelock_root)
{ {
trace trace << "PASS 1: heuristic livelock detection SUCCESS\n";
<< "PASS 1: heuristic livelock detection SUCCESS" << std::endl;
return true; return true;
} }
liveset_curr.insert(u); liveset_curr.insert(u);
} }
return false; return false;
} }
bool bool
@ -421,8 +392,7 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h = hash_type h;
numbered_state_heap_hash_map_factory::instance()->build();
// * num: the number of visited nodes. Used to set the order of each // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
@ -448,7 +418,6 @@ namespace spot
{ {
state* init_state = (*it); state* init_state = (*it);
ta_init_it_.push(init_state); ta_init_it_.push(init_state);
} }
while (!ta_init_it_.empty()) while (!ta_init_it_.empty())
@ -457,19 +426,19 @@ namespace spot
{ {
state* init = ta_init_it_.front(); state* init = ta_init_it_.front();
ta_init_it_.pop(); ta_init_it_.pop();
numbered_state_heap::state_index_p h_init = h->find(init);
if (h_init.first) if (!h.insert(std::make_pair(init, num + 1)).second)
{
init->destroy();
continue; continue;
}
h->insert(init, ++num);
sscc.push(num); sscc.push(num);
sscc.top().is_accepting = t->is_livelock_accepting_state(init); sscc.top().is_accepting = t->is_livelock_accepting_state(init);
ta_succ_iterator_product* iter = t->succ_iter(init); ta_succ_iterator_product* iter = t->succ_iter(init);
iter->first(); iter->first();
todo.emplace(init, iter); todo.emplace(init, iter);
inc_depth(); inc_depth();
} }
while (!todo.empty()) while (!todo.empty())
@ -488,13 +457,11 @@ namespace spot
// Backtrack TODO. // Backtrack TODO.
todo.pop(); todo.pop();
dec_depth(); dec_depth();
trace trace << "PASS 2 : backtrack\n";
<< "PASS 2 : backtrack" << std::endl;
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = auto i = h.find(curr);
h->index(curr->clone()); assert(i != h.end());
assert(spi.first);
sscc.rem().push_front(curr); sscc.rem().push_front(curr);
inc_depth(); inc_depth();
@ -503,19 +470,11 @@ namespace spot
// remove that SSCC from the ROOT stacks. We must // remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC. // discard from H all reachable states from this SSCC.
assert(!sscc.empty()); assert(!sscc.empty());
if (sscc.top().index == *spi.second) if (sscc.top().index == i->second)
{ {
// removing states // removing states
std::list<state*>::iterator i; for (auto j: sscc.rem())
h[j] = -1;
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{
numbered_state_heap::state_index_p spi = h->index(
(*i)->clone());
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
}
dec_depth(sscc.rem().size()); dec_depth(sscc.rem().size());
sscc.pop(); sscc.pop();
} }
@ -528,8 +487,7 @@ namespace spot
// We have a successor to look at. // We have a successor to look at.
inc_transitions(); inc_transitions();
trace trace << "PASS 2 : transition\n";
<< "PASS 2 : transition" << std::endl;
// Fetch the values destination state we are interested in... // Fetch the values destination state we are interested in...
state* dest = succ->current_state(); state* dest = succ->current_state();
@ -539,10 +497,10 @@ namespace spot
succ->next(); succ->next();
// We do not need SUCC from now on. // We do not need SUCC from now on.
numbered_state_heap::state_index_p spi = h->find(dest); auto i = h.find(dest);
// Is this a new state? // Is this a new state?
if (!spi.first) if (i == h.end())
{ {
// Are we going to a new state through a stuttering transition? // Are we going to a new state through a stuttering transition?
@ -555,7 +513,7 @@ namespace spot
// Number it, stack it, and register its successors // Number it, stack it, and register its successors
// for later processing. // for later processing.
h->insert(dest, ++num); h[dest] = ++num;
sscc.push(num); sscc.push(num);
sscc.top().is_accepting = t->is_livelock_accepting_state(dest); sscc.top().is_accepting = t->is_livelock_accepting_state(dest);
@ -565,24 +523,26 @@ namespace spot
inc_depth(); inc_depth();
continue; continue;
} }
else
{
dest->destroy();
}
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (i->second == -1)
continue; continue;
//self loop state //self loop state
if (!curr->compare(spi.first)) if (!curr->compare(i->first))
{ {
state * self_loop_state = (curr); state* self_loop_state = curr;
if (t->is_livelock_accepting_state(self_loop_state)) if (t->is_livelock_accepting_state(self_loop_state))
{ {
clear(h, todo, ta_init_it_); clear(h, todo, ta_init_it_);
trace trace << "PASS 2: SUCCESS\n";
<< "PASS 2: SUCCESS" << std::endl;
return true; return true;
} }
} }
// Now this is the most interesting case. We have reached a // Now this is the most interesting case. We have reached a
@ -596,7 +556,7 @@ namespace spot
// ROOT is ascending: we just have to merge all SSCCs from the // ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold"). // the SSCC of S2 (called the "threshold").
int threshold = *spi.second; int threshold = i->second;
std::list<state*> rem; std::list<state*> rem;
bool acc = false; bool acc = false;
@ -634,11 +594,11 @@ namespace spot
} }
void void
ta_check::clear(numbered_state_heap* h, std::stack<pair_state_iter> todo, ta_check::clear(hash_type& h, std::stack<pair_state_iter> todo,
std::queue<spot::state*> init_states) std::queue<spot::state*> init_states)
{ {
set_states(states() + h->size()); set_states(states() + h.size());
while (!init_states.empty()) while (!init_states.empty())
{ {
@ -653,15 +613,14 @@ namespace spot
todo.pop(); todo.pop();
dec_depth(); dec_depth();
} }
delete h;
} }
void void
ta_check::clear(numbered_state_heap* h, std::stack<pair_state_iter> todo, ta_check::clear(hash_type& h, std::stack<pair_state_iter> todo,
spot::ta_succ_iterator* init_states_it) spot::ta_succ_iterator* init_states_it)
{ {
set_states(states() + h->size()); set_states(states() + h.size());
delete init_states_it; delete init_states_it;
@ -672,7 +631,6 @@ namespace spot
todo.pop(); todo.pop();
dec_depth(); dec_depth();
} }
delete h;
} }
std::ostream& std::ostream&

11
src/taalgos/emptinessta.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2008, 2012, 2013, 2014 Laboratoire de Recherche et
// Dévelopment de l'Epita (LRDE). // Dévelopment de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -25,7 +25,6 @@
#include "ta/taproduct.hh" #include "ta/taproduct.hh"
#include "misc/optionmap.hh" #include "misc/optionmap.hh"
#include "tgbaalgos/gtec/nsheap.hh"
#include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/emptiness_stats.hh"
#include <stack> #include <stack>
#include <queue> #include <queue>
@ -87,6 +86,8 @@ namespace spot
/// See the paper cited above. /// See the paper cited above.
class SPOT_API ta_check : public ec_statistics class SPOT_API ta_check : public ec_statistics
{ {
typedef std::unordered_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
public: public:
ta_check(const ta_product* a, option_map o = option_map()); ta_check(const ta_product* a, option_map o = option_map());
virtual virtual
@ -126,18 +127,18 @@ namespace spot
protected: protected:
void void
clear(numbered_state_heap* h, std::stack<pair_state_iter> todo, std::queue< clear(hash_type& h, std::stack<pair_state_iter> todo, std::queue<
spot::state*> init_set); spot::state*> init_set);
void void
clear(numbered_state_heap* h, std::stack<pair_state_iter> todo, clear(hash_type& h, std::stack<pair_state_iter> todo,
spot::ta_succ_iterator* init_states_it); spot::ta_succ_iterator* init_states_it);
/// the heuristic for livelock-accepting runs detection, it's described /// the heuristic for livelock-accepting runs detection, it's described
/// in the paper cited above /// in the paper cited above
bool bool
heuristic_livelock_detection(const state * stuttering_succ, heuristic_livelock_detection(const state * stuttering_succ,
numbered_state_heap* h, int h_livelock_root, std::set<const state*, hash_type& h, int h_livelock_root, std::set<const state*,
state_ptr_less_than> liveset_curr); state_ptr_less_than> liveset_curr);
const ta_product* a_; ///< The automaton. const ta_product* a_; ///< The automaton.

78
src/taalgos/tgba2ta.cc
View file

@ -1,6 +1,6 @@
// -*- coding utf-8 -*- // -*- coding utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -35,7 +35,6 @@
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include <iostream> #include <iostream>
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "tgbaalgos/gtec/nsheap.hh"
#include <stack> #include <stack>
#include "tgba2ta.hh" #include "tgba2ta.hh"
#include "taalgos/statessetbuilder.hh" #include "taalgos/statessetbuilder.hh"
@ -164,9 +163,9 @@ namespace spot
// * h: a hash of all visited nodes, with their order, // * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper) // (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h = typedef std::unordered_map<const state*, int,
numbered_state_heap_hash_map_factory::instance()->build(); state_ptr_hash, state_ptr_equal> hash_type;
///< Heap of visited states. hash_type h; ///< Heap of visited states.
// * num: the number of visited nodes. Used to set the order of each // * num: the number of visited nodes. Used to set the order of each
// visited node, // visited node,
@ -182,13 +181,8 @@ namespace spot
// * init: the set of the depth-first search initial states // * init: the set of the depth-first search initial states
std::stack<state*> init_set; std::stack<state*> init_set;
ta::states_set_t::const_iterator it; for (state* s: testing_automata->get_initial_states_set())
ta::states_set_t init_states = testing_automata->get_initial_states_set(); init_set.push(s);
for (it = init_states.begin(); it != init_states.end(); ++it)
{
state* init_state = (*it);
init_set.push(init_state);
}
while (!init_set.empty()) while (!init_set.empty())
{ {
@ -198,29 +192,29 @@ namespace spot
state_ta_explicit* init = state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top()); down_cast<state_ta_explicit*> (init_set.top());
init_set.pop(); init_set.pop();
state_ta_explicit* init_clone = init;
numbered_state_heap::state_index_p h_init = h->find(init_clone);
if (h_init.first) if (!h.insert(std::make_pair(init, num + 1)).second)
{
init->destroy();
continue; continue;
}
h->insert(init_clone, ++num); sscc.push(++num);
sscc.push(num);
arc.push(bddfalse); arc.push(bddfalse);
sscc.top().is_accepting sscc.top().is_accepting
= testing_automata->is_accepting_state(init); = testing_automata->is_accepting_state(init);
tgba_succ_iterator* iter = testing_automata->succ_iter(init); tgba_succ_iterator* iter = testing_automata->succ_iter(init);
iter->first(); iter->first();
todo.push(pair_state_iter(init, iter)); todo.emplace(init, iter);
} }
while (!todo.empty()) while (!todo.empty())
{ {
state* curr = todo.top().first; state* curr = todo.top().first;
numbered_state_heap::state_index_p spi = h->find(curr); auto i = h.find(curr);
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (i != h.end() && i->second == -1)
{ {
todo.pop(); todo.pop();
continue; continue;
@ -238,16 +232,14 @@ namespace spot
todo.pop(); todo.pop();
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = h->index(curr); assert(i != h.end());
assert(spi.first);
sscc.rem().push_front(curr); sscc.rem().push_front(curr);
// When backtracking the root of an SSCC, we must also // When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must // remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC. // discard from H all reachable states from this SSCC.
assert(!sscc.empty()); assert(!sscc.empty());
if (sscc.top().index == *spi.second) if (sscc.top().index == i->second)
{ {
// removing states // removing states
std::list<state*>::iterator i; std::list<state*>::iterator i;
@ -256,25 +248,20 @@ namespace spot
|| (sscc.top().condition == || (sscc.top().condition ==
testing_automata->all_acceptance_conditions())); testing_automata->all_acceptance_conditions()));
trace << "*** sscc.size() = ***" trace << "*** sscc.size() = ***" << sscc.size() << '\n';
<< sscc.size() << std::endl; for (auto j: sscc.rem())
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{ {
numbered_state_heap::state_index_p spi = h[j] = -1;
h->index((*i));
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
if (is_livelock_accepting_sscc) if (is_livelock_accepting_sscc)
{ {
// if it is an accepting sscc add the state to // if it is an accepting sscc add the state to
// G (=the livelock-accepting states set) // G (=the livelock-accepting states set)
trace << "*** sscc.size() > 1: states: ***" trace << "*** sscc.size() > 1: states: ***"
<< testing_automata->format_state(*i) << testing_automata->format_state(j)
<< std::endl; << '\n';
state_ta_explicit* livelock_accepting_state = state_ta_explicit* livelock_accepting_state =
down_cast<state_ta_explicit*> (*i); down_cast<state_ta_explicit*>(j);
livelock_accepting_state-> livelock_accepting_state->
set_livelock_accepting_state(true); set_livelock_accepting_state(true);
@ -317,22 +304,21 @@ namespace spot
bool is_stuttering_transition = bool is_stuttering_transition =
testing_automata->get_state_condition(curr) testing_automata->get_state_condition(curr)
== testing_automata->get_state_condition(dest); == testing_automata->get_state_condition(dest);
state* dest_clone = dest; auto id = h.find(dest);
spi = h->find(dest_clone);
// Is this a new state? // Is this a new state?
if (!spi.first) if (id == h.end())
{ {
if (!is_stuttering_transition) if (!is_stuttering_transition)
{ {
init_set.push(dest); init_set.push(dest);
dest_clone->destroy(); dest->destroy();
continue; continue;
} }
// Number it, stack it, and register its successors // Number it, stack it, and register its successors
// for later processing. // for later processing.
h->insert(dest_clone, ++num); h[dest] = ++num;
sscc.push(num); sscc.push(num);
arc.push(acc_cond); arc.push(acc_cond);
sscc.top().is_accepting = sscc.top().is_accepting =
@ -340,17 +326,18 @@ namespace spot
tgba_succ_iterator* iter = testing_automata->succ_iter(dest); tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
iter->first(); iter->first();
todo.push(pair_state_iter(dest, iter)); todo.emplace(dest, iter);
continue; continue;
} }
dest->destroy();
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (id->second == -1)
continue; continue;
trace << "***compute_livelock_acceptance_states: CYCLE***\n"; trace << "***compute_livelock_acceptance_states: CYCLE***\n";
if (!curr->compare(dest)) if (!curr->compare(id->first))
{ {
state_ta_explicit * self_loop_state = state_ta_explicit * self_loop_state =
down_cast<state_ta_explicit*> (curr); down_cast<state_ta_explicit*> (curr);
@ -385,7 +372,7 @@ namespace spot
// ROOT is ascending: we just have to merge all SSCCs from the // ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold"). // the SSCC of S2 (called the "threshold").
int threshold = *spi.second; int threshold = id->second;
std::list<state*> rem; std::list<state*> rem;
bool acc = false; bool acc = false;
@ -415,7 +402,6 @@ namespace spot
} }
} }
delete h;
if ((artificial_livelock_acc_state != 0) if ((artificial_livelock_acc_state != 0)
|| single_pass_emptiness_check) || single_pass_emptiness_check)

4
src/tgbaalgos/gtec/Makefile.am
View file

@ -1,5 +1,5 @@
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement ## Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Developpement
## de l'Epita (LRDE). ## de l'Epita (LRDE).
## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## 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
@ -29,7 +29,6 @@ gtec_HEADERS = \
ce.hh \ ce.hh \
explscc.hh \ explscc.hh \
gtec.hh \ gtec.hh \
nsheap.hh \
sccstack.hh \ sccstack.hh \
status.hh status.hh
@ -38,6 +37,5 @@ libgtec_la_SOURCES = \
ce.cc \ ce.cc \
explscc.cc \ explscc.cc \
gtec.cc \ gtec.cc \
nsheap.cc \
sccstack.cc \ sccstack.cc \
status.cc status.cc

44
src/tgbaalgos/gtec/ce.cc
View file

@ -1,7 +1,8 @@
// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Développement de l'Epita (LRDE). // Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -47,17 +48,15 @@ namespace spot
filter(const state* s) filter(const state* s)
{ {
r->inc_ars_prefix_states(); r->inc_ars_prefix_states();
numbered_state_heap::state_index_p sip = ecs->h->find(s); auto i = ecs->h.find(s);
// Ignore unknown states ...
if (!sip.first)
{
s->destroy(); s->destroy();
return 0; // Ignore unknown states ...
} if (i == ecs->h.end())
return nullptr;
// ... as well as dead states. // ... as well as dead states.
if (*sip.second == -1) if (i->second == -1)
return 0; return nullptr;
return sip.first; return i->first;
} }
bool bool
@ -83,14 +82,11 @@ namespace spot
unsigned unsigned
couvreur99_check_result::acss_states() const couvreur99_check_result::acss_states() const
{ {
unsigned count = 0;
int scc_root = ecs_->root.top().index; int scc_root = ecs_->root.top().index;
unsigned count = 0;
numbered_state_heap_const_iterator* i = ecs_->h->iterator(); for (auto i: ecs_->h)
for (i->first(); !i->done(); i->next()) if (i.second >= scc_root)
if (i->get_index() >= scc_root)
++count; ++count;
delete i;
return count; return count;
} }
@ -190,18 +186,16 @@ namespace spot
virtual const state* virtual const state*
filter(const state* s) filter(const state* s)
{ {
numbered_state_heap::state_index_p sip = ecs->h->find(s); auto i = ecs->h.find(s);
// Ignore unknown states.
if (!sip.first)
{
s->destroy(); s->destroy();
// Ignore unknown states.
if (i == ecs->h.end())
return 0; return 0;
}
// Stay in the final SCC. // Stay in the final SCC.
if (*sip.second < scc_root) if (i->second < scc_root)
return 0; return 0;
r->inc_ars_cycle_states(); r->inc_ars_cycle_states();
return sip.first; return i->first;
} }
virtual bool virtual bool

164
src/tgbaalgos/gtec/gtec.cc
View file

@ -40,14 +40,12 @@ namespace spot
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter; typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
} }
couvreur99_check::couvreur99_check(const tgba* a, couvreur99_check::couvreur99_check(const tgba* a, option_map o)
option_map o,
const numbered_state_heap_factory* nshf)
: emptiness_check(a, o), : emptiness_check(a, o),
removed_components(0) removed_components(0)
{ {
poprem_ = o.get("poprem", 1); poprem_ = o.get("poprem", 1);
ecs_ = new couvreur99_check_status(a, nshf); ecs_ = new couvreur99_check_status(a);
stats["removed components"] = stats["removed components"] =
static_cast<spot::unsigned_statistics::unsigned_fun> static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check::get_removed_components); (&couvreur99_check::get_removed_components);
@ -85,14 +83,8 @@ namespace spot
{ {
assert(!ecs_->root.rem().empty()); assert(!ecs_->root.rem().empty());
dec_depth(ecs_->root.rem().size()); dec_depth(ecs_->root.rem().size());
std::list<const state*>::iterator i; for (auto i: ecs_->root.rem())
for (i = ecs_->root.rem().begin(); i != ecs_->root.rem().end(); ++i) ecs_->h[i] = -1;
{
numbered_state_heap::state_index_p spi = ecs_->h->index(*i);
assert(spi.first == *i);
assert(*spi.second != -1);
*spi.second = -1;
}
// ecs_->root.rem().clear(); // ecs_->root.rem().clear();
return; return;
} }
@ -106,10 +98,7 @@ namespace spot
// (FROM should be in H, otherwise it means all reachable // (FROM should be in H, otherwise it means all reachable
// states from FROM have already been removed and there is no // states from FROM have already been removed and there is no
// point in calling remove_component.) // point in calling remove_component.)
numbered_state_heap::state_index_p spi = ecs_->h->index(from); ecs_->h[from] = -1;
assert(spi.first == from);
assert(*spi.second != -1);
*spi.second = -1;
tgba_succ_iterator* i = ecs_->aut->succ_iter(from); tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
for (;;) for (;;)
@ -121,20 +110,14 @@ namespace spot
inc_transitions(); inc_transitions();
state* s = i->current_state(); state* s = i->current_state();
numbered_state_heap::state_index_p spi = ecs_->h->index(s); auto j = ecs_->h.find(s);
assert(j != ecs_->h.end());
s->destroy();
// This state is not necessary in H, because if we were if (j->second != -1)
// doing inclusion checking during the emptiness-check
// (redefining find()), the index `s' can be included in a
// larger state and will not be found by index(). We can
// safely ignore such states.
if (!spi.first)
continue;
if (*spi.second != -1)
{ {
*spi.second = -1; j->second = -1;
to_remove.push(ecs_->aut->succ_iter(spi.first)); to_remove.push(ecs_->aut->succ_iter(j->first));
} }
} }
while (i->next()); while (i->next());
@ -168,7 +151,7 @@ namespace spot
// Setup depth-first search from the initial state. // Setup depth-first search from the initial state.
{ {
state* init = ecs_->aut->get_init_state(); state* init = ecs_->aut->get_init_state();
ecs_->h->insert(init, 1); ecs_->h[init] = 1;
ecs_->root.push(1); ecs_->root.push(1);
arc.push(bddfalse); arc.push(bddfalse);
tgba_succ_iterator* iter = ecs_->aut->succ_iter(init); tgba_succ_iterator* iter = ecs_->aut->succ_iter(init);
@ -197,18 +180,18 @@ namespace spot
// If poprem is used, fill rem with any component removed, // If poprem is used, fill rem with any component removed,
// so that remove_component() does not have to traverse // so that remove_component() does not have to traverse
// the SCC again. // the SCC again.
numbered_state_heap::state_index_p spi = ecs_->h->index(curr); auto i = ecs_->h.find(curr);
assert(spi.first); assert(i != ecs_->h.end());
if (poprem_) if (poprem_)
{ {
ecs_->root.rem().push_front(spi.first); ecs_->root.rem().push_front(i->first);
inc_depth(); inc_depth();
} }
// When backtracking the root of an SCC, we must also // When backtracking the root of an SCC, we must also
// remove that SCC from the ARC/ROOT stacks. We must // remove that SCC from the ARC/ROOT stacks. We must
// discard from H all reachable states from this SCC. // discard from H all reachable states from this SCC.
assert(!ecs_->root.empty()); assert(!ecs_->root.empty());
if (ecs_->root.top().index == *spi.second) if (ecs_->root.top().index == i->second)
{ {
assert(!arc.empty()); assert(!arc.empty());
arc.pop(); arc.pop();
@ -232,13 +215,12 @@ namespace spot
// We do not need SUCC from now on. // We do not need SUCC from now on.
// Are we going to a new state? // Are we going to a new state?
numbered_state_heap::state_index_p spi = ecs_->h->find(dest); auto p = ecs_->h.insert(std::make_pair(dest, num + 1));
if (!spi.first) if (p.second)
{ {
// Yes. Number it, stack it, and register its successors // Yes. Bump number, stack the stack, and register its
// for later processing. // successors for later processing.
ecs_->h->insert(dest, ++num); ecs_->root.push(++num);
ecs_->root.push(num);
arc.push(acc); arc.push(acc);
tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest); tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest);
iter->first(); iter->first();
@ -246,9 +228,10 @@ namespace spot
inc_depth(); inc_depth();
continue; continue;
} }
dest->destroy();
// If we have reached a dead component, ignore it. // If we have reached a dead component, ignore it.
if (*spi.second == -1) if (p.first->second == -1)
continue; continue;
// Now this is the most interesting case. We have reached a // Now this is the most interesting case. We have reached a
@ -262,7 +245,7 @@ namespace spot
// ROOT is ascending: we just have to merge all SCCs from the // ROOT is ascending: we just have to merge all SCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SCC of S2 (called the "threshold"). // the SCC of S2 (called the "threshold").
int threshold = *spi.second; int threshold = p.first->second;
std::list<const state*> rem; std::list<const state*> rem;
while (threshold < ecs_->root.top().index) while (threshold < ecs_->root.top().index)
{ {
@ -296,7 +279,7 @@ namespace spot
} }
// Use this state to start the computation of an accepting // Use this state to start the computation of an accepting
// cycle. // cycle.
ecs_->cycle_seed = spi.first; ecs_->cycle_seed = p.first->first;
set_states(ecs_->states()); set_states(ecs_->states());
return new couvreur99_check_result(ecs_, options()); return new couvreur99_check_result(ecs_, options());
} }
@ -336,20 +319,16 @@ namespace spot
} }
} }
couvreur99_check_shy::couvreur99_check_shy(const tgba* a, couvreur99_check_shy::couvreur99_check_shy(const tgba* a, option_map o)
option_map o, : couvreur99_check(a, o), num(1)
const numbered_state_heap_factory*
nshf)
: couvreur99_check(a, o, nshf), num(1)
{ {
group_ = o.get("group", 1); group_ = o.get("group", 1);
group2_ = o.get("group2", 0); group2_ = o.get("group2", 0);
group_ |= group2_; group_ |= group2_;
onepass_ = o.get("onepass", 0);
// Setup depth-first search from the initial state. // Setup depth-first search from the initial state.
const state* i = ecs_->aut->get_init_state(); const state* i = ecs_->aut->get_init_state();
ecs_->h->insert(i, ++num); ecs_->h[i] = ++num;
ecs_->root.push(num); ecs_->root.push(num);
todo.emplace_back(i, num, this); todo.emplace_back(i, num, this);
inc_depth(1); inc_depth(1);
@ -367,15 +346,13 @@ namespace spot
while (!todo.empty()) while (!todo.empty())
{ {
succ_queue& queue = todo.back().q; succ_queue& queue = todo.back().q;
for (succ_queue::iterator q = queue.begin(); for (auto& q: queue)
q != queue.end(); ++q)
{ {
// Destroy the state if it is a clone of a // Destroy the state if it is a clone of a state in the
// state in the heap... // heap or if it is an unknown state.
numbered_state_heap::state_index_p spi = ecs_->h->index(q->s); auto i = ecs_->h.find(q.s);
// ... or if it is an unknown state. if (i == ecs_->h.end() || i->first != q.s)
if (spi.first == 0) q.s->destroy();
q->s->destroy();
} }
dec_depth(todo.back().q.size() + 1); dec_depth(todo.back().q.size() + 1);
todo.pop_back(); todo.pop_back();
@ -387,21 +364,21 @@ namespace spot
void void
couvreur99_check_shy::dump_queue(std::ostream& os) couvreur99_check_shy::dump_queue(std::ostream& os)
{ {
os << "--- TODO ---" << std::endl; os << "--- TODO ---\n";
unsigned pos = 0; unsigned pos = 0;
for (todo_list::const_iterator ti = todo.begin(); ti != todo.end(); ++ti) for (auto& ti: todo)
{ {
++pos; ++pos;
os << '#' << pos << " s:" << ti->s << " n:" << ti->n os << '#' << pos << " s:" << ti.s << " n:" << ti.n
<< " q:{"; << " q:{";
for (succ_queue::const_iterator qi = ti->q.begin(); qi != ti->q.end();) for (auto qi = ti.q.begin(); qi != ti.q.end();)
{ {
os << qi->s; os << qi->s;
++qi; ++qi;
if (qi != ti->q.end()) if (qi != ti.q.end())
os << ", "; os << ", ";
} }
os << '}' << std::endl; os << "}\n";
} }
} }
@ -450,9 +427,10 @@ namespace spot
// the SCC again. // the SCC again.
if (poprem_) if (poprem_)
{ {
numbered_state_heap::state_index_p spi = ecs_->h->index(curr); auto i = ecs_->h.find(curr);
assert(spi.first); assert(i != ecs_->h.end());
ecs_->root.rem().push_front(spi.first); assert(i->first == curr);
ecs_->root.rem().push_front(i->first);
inc_depth(); inc_depth();
} }
@ -479,35 +457,31 @@ namespace spot
// which state we are considering. Otherwise just pick the // which state we are considering. Otherwise just pick the
// first one. // first one.
succ_queue::iterator old; succ_queue::iterator old;
if (onepass_)
pos = queue.end();
if (pos == queue.end()) if (pos == queue.end())
old = queue.begin(); old = queue.begin();
else else
old = pos; old = pos;
successor succ = *old;
// Beware: the implementation of find_state in ifage/gspn/ssp.cc
// uses POS and modifies QUEUE.
numbered_state_heap::state_index_p sip = find_state(succ.s);
if (pos != queue.end()) if (pos != queue.end())
++pos; ++pos;
int* i = sip.second; //int* i = sip.second;
trace << "picked state " << succ.s << std::endl; successor succ = *old;
trace << "picked state " << succ.s << '\n';
auto i = ecs_->h.find(succ.s);
if (!i) if (i == ecs_->h.end())
{ {
// It's a new state. // It's a new state.
// If we are seeking known states, just skip it. // If we are seeking known states, just skip it.
if (pos != queue.end()) if (pos != queue.end())
continue; continue;
trace << "new state" << std::endl; trace << "new state\n";
// Otherwise, number it and stack it so we recurse. // Otherwise, number it and stack it so we recurse.
queue.erase(old); queue.erase(old);
dec_depth(); dec_depth();
ecs_->h->insert(succ.s, ++num); ecs_->h[succ.s] = ++num;
ecs_->root.push(num); ecs_->root.push(num);
arc.push(succ.acc); arc.push(succ.acc);
todo.emplace_back(succ.s, num, this); todo.emplace_back(succ.s, num, this);
@ -516,17 +490,20 @@ namespace spot
continue; continue;
} }
// It's an known state. Use i->first from now on.
succ.s->destroy();
queue.erase(old); queue.erase(old);
dec_depth(); dec_depth();
// Skip dead states. // Skip dead states.
if (*i == -1) if (i->second == -1)
{ {
trace << "dead state" << std::endl; trace << "dead state\n";
continue; continue;
} }
trace << "merging..." << std::endl; trace << "merging...\n";
// Now this is the most interesting case. We have // Now this is the most interesting case. We have
// reached a state S1 which is already part of a // reached a state S1 which is already part of a
@ -542,7 +519,7 @@ namespace spot
// merge all SCCs from the top of ROOT that have // merge all SCCs from the top of ROOT that have
// an index greater to the one of the SCC of S2 // an index greater to the one of the SCC of S2
// (called the "threshold"). // (called the "threshold").
int threshold = *i; int threshold = i->second;
std::list<const state*> rem; std::list<const state*> rem;
bdd acc = succ.acc; bdd acc = succ.acc;
while (threshold < ecs_->root.top().index) while (threshold < ecs_->root.top().index)
@ -571,7 +548,7 @@ namespace spot
{ {
// Use this state to start the computation of an accepting // Use this state to start the computation of an accepting
// cycle. // cycle.
ecs_->cycle_seed = sip.first; ecs_->cycle_seed = i->first;
// We have found an accepting SCC. Clean up TODO. // We have found an accepting SCC. Clean up TODO.
clear_todo(); clear_todo();
@ -595,10 +572,11 @@ namespace spot
if (poprem_) if (poprem_)
{ {
numbered_state_heap::state_index_p spi = const state* s = todo.back().s;
ecs_->h->index(todo.back().s); auto i = ecs_->h.find(s);
assert(spi.first); assert(i != ecs_->h.end());
ecs_->root.rem().push_front(spi.first); assert(i->first == s);
ecs_->root.rem().push_front(i->first);
// Don't change the stack depth, since // Don't change the stack depth, since
// we are just moving the state from TODO to REM. // we are just moving the state from TODO to REM.
} }
@ -613,20 +591,12 @@ namespace spot
} }
} }
numbered_state_heap::state_index_p
couvreur99_check_shy::find_state(const state* s)
{
return ecs_->h->find(s);
}
emptiness_check* emptiness_check*
couvreur99(const tgba* a, couvreur99(const tgba* a, option_map o)
option_map o,
const numbered_state_heap_factory* nshf)
{ {
if (o.get("shy")) if (o.get("shy"))
return new couvreur99_check_shy(a, o, nshf); return new couvreur99_check_shy(a, o);
return new couvreur99_check(a, o, nshf); return new couvreur99_check(a, o);
} }
} }

33
src/tgbaalgos/gtec/gtec.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement // Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -137,10 +137,7 @@ namespace spot
/// choosing a successor. Otherwise, only the successor of the /// choosing a successor. Otherwise, only the successor of the
/// topmost state on the DFS stack are considered. /// topmost state on the DFS stack are considered.
SPOT_API emptiness_check* SPOT_API emptiness_check*
couvreur99(const tgba* a, couvreur99(const tgba* a, option_map options = option_map());
option_map options = option_map(),
const numbered_state_heap_factory* nshf
= numbered_state_heap_hash_map_factory::instance());
/// \brief An implementation of the Couvreur99 emptiness-check algorithm. /// \brief An implementation of the Couvreur99 emptiness-check algorithm.
@ -149,10 +146,7 @@ namespace spot
class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics
{ {
public: public:
couvreur99_check(const tgba* a, couvreur99_check(const tgba* a, option_map o = option_map());
option_map o = option_map(),
const numbered_state_heap_factory* nshf
= numbered_state_heap_hash_map_factory::instance());
virtual ~couvreur99_check(); virtual ~couvreur99_check();
/// Check whether the automaton's language is empty. /// Check whether the automaton's language is empty.
@ -194,10 +188,7 @@ namespace spot
class SPOT_API couvreur99_check_shy : public couvreur99_check class SPOT_API couvreur99_check_shy : public couvreur99_check
{ {
public: public:
couvreur99_check_shy(const tgba* a, couvreur99_check_shy(const tgba* a, option_map o = option_map());
option_map o = option_map(),
const numbered_state_heap_factory* nshf
= numbered_state_heap_hash_map_factory::instance());
virtual ~couvreur99_check_shy(); virtual ~couvreur99_check_shy();
virtual emptiness_check_result* check(); virtual emptiness_check_result* check();
@ -247,20 +238,6 @@ namespace spot
// If the "group2" option is set (it implies "group"), we // If the "group2" option is set (it implies "group"), we
// reprocess the successor states of SCC that have been merged. // reprocess the successor states of SCC that have been merged.
bool group2_; bool group2_;
// If the onepass option is true, do only one pass. This cancels
// all the "shyness" of the algorithm, but we need the framework
// of the implementation when working with GreatSPN.
bool onepass_;
/// \brief find the SCC number of a unprocessed state.
///
/// Sometimes we want to modify some of the above structures when
/// looking up a new state. This happens for instance when find()
/// must perform inclusion checking and add new states to process
/// to TODO during this step. (Because TODO must be known,
/// sub-classing spot::numbered_state_heap is not enough.) Then
/// overriding this method is the way to go.
virtual numbered_state_heap::state_index_p find_state(const state* s);
}; };

182
src/tgbaalgos/gtec/nsheap.cc
View file

@ -1,182 +0,0 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2006 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 "nsheap.hh"
namespace spot
{
namespace
{
class numbered_state_heap_hash_map_const_iterator:
public numbered_state_heap_const_iterator
{
public:
numbered_state_heap_hash_map_const_iterator
(const numbered_state_heap_hash_map::hash_type& h)
: numbered_state_heap_const_iterator(), h(h)
{
}
~numbered_state_heap_hash_map_const_iterator()
{
}
virtual void
first()
{
i = h.begin();
}
virtual void
next()
{
++i;
}
virtual bool
done() const
{
return i == h.end();
}
virtual const state*
get_state() const
{
return i->first;
}
virtual int
get_index() const
{
return i->second;
}
private:
numbered_state_heap_hash_map::hash_type::const_iterator i;
const numbered_state_heap_hash_map::hash_type& h;
};
} // anonymous
numbered_state_heap_hash_map::~numbered_state_heap_hash_map()
{
// Free keys in H.
hash_type::iterator i = h.begin();
while (i != h.end())
{
// Advance the iterator before deleting the key.
const state* s = i->first;
++i;
s->destroy();
}
}
numbered_state_heap::state_index
numbered_state_heap_hash_map::find(const state* s) const
{
state_index res;
hash_type::const_iterator i = h.find(s);
if (i == h.end())
{
res.first = 0;
res.second = 0;
}
else
{
res.first = i->first;
res.second = i->second;
if (s != i->first)
s->destroy();
}
return res;
}
numbered_state_heap::state_index_p
numbered_state_heap_hash_map::find(const state* s)
{
state_index_p res;
hash_type::iterator i = h.find(s);
if (i == h.end())
{
res.first = 0;
res.second = 0;
}
else
{
res.first = i->first;
res.second = &i->second;
if (s != i->first)
s->destroy();
}
return res;
}
numbered_state_heap::state_index
numbered_state_heap_hash_map::index(const state* s) const
{
return this->numbered_state_heap_hash_map::find(s);
}
numbered_state_heap::state_index_p
numbered_state_heap_hash_map::index(const state* s)
{
return this->numbered_state_heap_hash_map::find(s);
}
void
numbered_state_heap_hash_map::insert(const state* s, int index)
{
h[s] = index;
}
int
numbered_state_heap_hash_map::size() const
{
return h.size();
}
numbered_state_heap_const_iterator*
numbered_state_heap_hash_map::iterator() const
{
return new numbered_state_heap_hash_map_const_iterator(h);
}
numbered_state_heap_hash_map_factory::numbered_state_heap_hash_map_factory()
: numbered_state_heap_factory()
{
}
numbered_state_heap_hash_map*
numbered_state_heap_hash_map_factory::build() const
{
return new numbered_state_heap_hash_map();
}
const numbered_state_heap_hash_map_factory*
numbered_state_heap_hash_map_factory::instance()
{
static numbered_state_heap_hash_map_factory f;
return &f;
}
}

148
src/tgbaalgos/gtec/nsheap.hh
View file

@ -1,148 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Development de
// l'Epita (LRDE).
// Copyright (C) 2004, 2006 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/>.
#ifndef SPOT_TGBAALGOS_GTEC_NSHEAP_HH
# define SPOT_TGBAALGOS_GTEC_NSHEAP_HH
# include "tgba/state.hh"
# include "misc/hash.hh"
namespace spot
{
/// Iterator on numbered_state_heap objects.
class SPOT_API numbered_state_heap_const_iterator
{
public:
virtual ~numbered_state_heap_const_iterator() {}
//@{
/// Iteration
virtual void first() = 0;
virtual void next() = 0;
virtual bool done() const = 0;
//@}
//@{
/// Inspection
virtual const state* get_state() const = 0;
virtual int get_index() const = 0;
//@}
};
/// Keep track of a large quantity of indexed states.
class SPOT_API numbered_state_heap
{
public:
typedef std::pair<const state*, int*> state_index_p;
typedef std::pair<const state*, int> state_index;
virtual ~numbered_state_heap() {}
//@{
/// \brief Is state in the heap?
///
/// Returns a pair (0,0) if \a s is not in the heap.
/// or a pair (p, i) if there is a clone \a p of \a s \a i
/// in the heap with index. If \a s is in the heap and is different
/// from \a p it will be freed.
///
/// These functions are called by the algorithm to check whether a
/// successor is a new state to explore or an already visited
/// state.
///
/// These functions can be redefined to search for more
/// than an equal match. For example we could redefine
/// it to check state inclusion.
virtual state_index find(const state* s) const = 0;
virtual state_index_p find(const state* s) = 0;
//@}
//@{
/// \brief Return the index of an existing state.
///
/// This is mostly similar to find(), except it will
/// be called for state which we know are already in
/// the heap, or for state which may not be in the
/// heap but for which it is always OK to do equality
/// checks.
virtual state_index index(const state* s) const = 0;
virtual state_index_p index(const state* s) = 0;
//@}
/// Add a new state \a s with index \a index
virtual void insert(const state* s, int index) = 0;
/// The number of stored states.
virtual int size() const = 0;
/// Return an iterator on the states/indexes pairs.
virtual numbered_state_heap_const_iterator* iterator() const = 0;
};
/// Abstract factory for numbered_state_heap
class SPOT_API numbered_state_heap_factory
{
public:
virtual ~numbered_state_heap_factory() {}
virtual numbered_state_heap* build() const = 0;
};
/// A straightforward implementation of numbered_state_heap with a hash map.
class SPOT_API numbered_state_heap_hash_map : public numbered_state_heap
{
public:
virtual ~numbered_state_heap_hash_map();
virtual state_index find(const state* s) const;
virtual state_index_p find(const state* s);
virtual state_index index(const state* s) const;
virtual state_index_p index(const state* s);
virtual void insert(const state* s, int index);
virtual int size() const;
virtual numbered_state_heap_const_iterator* iterator() const;
typedef std::unordered_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
protected:
hash_type h; ///< Map of visited states.
};
/// \brief Factory for numbered_state_heap_hash_map.
///
/// This class is a singleton. Retrieve the instance using instance().
class SPOT_API numbered_state_heap_hash_map_factory:
public numbered_state_heap_factory
{
public:
virtual numbered_state_heap_hash_map* build() const;
/// Get the unique instance of this class.
static const numbered_state_heap_hash_map_factory* instance();
protected:
virtual ~numbered_state_heap_hash_map_factory() {}
numbered_state_heap_hash_map_factory();
};
}
#endif // SPOT_TGBAALGOS_GTEC_NSHEAP_HH

28
src/tgbaalgos/gtec/status.cc
View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -22,31 +25,34 @@
namespace spot namespace spot
{ {
couvreur99_check_status::couvreur99_check_status couvreur99_check_status::couvreur99_check_status(const tgba* aut)
(const tgba* aut, : aut(aut)
const numbered_state_heap_factory* nshf)
: aut(aut),
h(nshf->build())
{ {
} }
couvreur99_check_status::~couvreur99_check_status() couvreur99_check_status::~couvreur99_check_status()
{ {
delete h; hash_type::iterator i = h.begin();
while (i != h.end())
{
// Advance the iterator before deleting the key.
const state* s = i->first;
++i;
s->destroy();
}
} }
void void
couvreur99_check_status::print_stats(std::ostream& os) const couvreur99_check_status::print_stats(std::ostream& os) const
{ {
os << h->size() << " unique states visited" << std::endl; os << h.size() << " unique states visited" << std::endl;
os << root.size() os << root.size()
<< " strongly connected components in search stack" << " strongly connected components in search stack\n";
<< std::endl;
} }
int int
couvreur99_check_status::states() const couvreur99_check_status::states() const
{ {
return h->size(); return h.size();
} }
} }

15
src/tgbaalgos/gtec/status.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement de // Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
@ -24,7 +24,6 @@
# define SPOT_TGBAALGOS_GTEC_STATUS_HH # define SPOT_TGBAALGOS_GTEC_STATUS_HH
#include "sccstack.hh" #include "sccstack.hh"
#include "nsheap.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include <iosfwd> #include <iosfwd>
@ -38,13 +37,17 @@ namespace spot
class SPOT_API couvreur99_check_status class SPOT_API couvreur99_check_status
{ {
public: public:
couvreur99_check_status(const tgba* aut, couvreur99_check_status(const tgba* aut);
const numbered_state_heap_factory* nshf);
~couvreur99_check_status(); ~couvreur99_check_status();
const tgba* aut; const tgba* aut;
scc_stack root; scc_stack root;
numbered_state_heap* h; ///< Heap of visited states.
typedef std::unordered_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h;
const state* cycle_seed; const state* cycle_seed;
/// Output statistics about this object. /// Output statistics about this object.