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

c++11: introduce tgba::succ(s) to replace tgba::succ_iter(s).

Browse source 
| tgba_succ_iterator* i = aut->succ_iter(s);
| for (i->begin(); !i->done(); i->next())
|   {
|      // ...
|   }
| delete i;

becomes

| for (auto i: aut->succ(s))
|   {
|      // ...
|   }

hiding the begin()/done()/next() interface, taking care of the delete,
and allowing more optimization to come.

* src/tgba/succiter.hh, src/tgba/tgba.hh: Implement the above
new interface.
* iface/gspn/ssp.cc, src/dstarparse/nsa2tgba.cc,
src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbamask.cc, src/tgba/tgbasafracomplement.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/compsusp.cc, src/tgbaalgos/cutscc.cc,
src/tgbaalgos/degen.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/isdet.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/safety.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/tau03.cc, src/tgbatest/explicit2.cc: Update for
loops.
This commit is contained in:
Alexandre Duret-Lutz 2014-01-25 19:48:28 +01:00
parent f59773e3c7
commit 487cd01d9f
21 changed files with 418 additions and 522 deletions
Download patch file Download diff file Expand all files Collapse all files

8
iface/gspn/ssp.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011, 2013 Laboratoire de Recherche et
// Copyright (C) 2008, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
@ -365,9 +365,7 @@ namespace spot
state** state_array = 0;
size_t size_states = 0;
tgba_succ_iterator* i = data_->operand->succ_iter(s->right());
for (i->first(); !i->done(); i->next())
for (auto i: data_->operand->succ(s))
{
all_conds_ = i->current_condition();
outside_ = !all_conds_;
@ -454,8 +452,6 @@ namespace spot
free(props_[j].prop[conj]);
free(props_[j].prop);
}
delete i;
return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_,
bdd_array, state_array,
size_states, props_,

6
src/dstarparse/nsa2tgba.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2013 Laboratoire de Recherche et Développement de
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -153,8 +153,7 @@ namespace spot
todo.pop_front();
int src = bs2num[s];
tgba_succ_iterator* i = a->succ_iter(a->get_state(s.s));
for (i->first(); !i->done(); i->next())
for (auto i: a->succ(a->get_state(s.s)))
{
int dlabel = label(a, i->current_state());
@ -216,7 +215,6 @@ namespace spot
t->condition = i->current_condition();
}
}
delete i;
}

26
src/saba/sabacomplementtgba.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 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.
//
@ -208,17 +208,14 @@ namespace spot
{
// Get successors states.
bdd condition = it->first;
tgba_succ_iterator* iterator =
automaton_->succ_iter(origin_->get_state());
std::vector<shared_state> state_list;
for (iterator->first(); !iterator->done(); iterator->next())
{
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
state_list.push_back(shared_state(iterator->current_state(),
shared_state_deleter));
}
delete iterator;
for (auto iterator: automaton_->succ(origin_->get_state()))
{
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
state_list.push_back(shared_state(iterator->current_state(),
shared_state_deleter));
}
// Make the conjunction with ranks.
std::vector<int> current_ranks(state_list.size(), max_rank);
@ -292,14 +289,11 @@ namespace spot
std::set<int> atomics;
delete_condition_list();
tgba_succ_iterator* iterator =
automaton_->succ_iter(origin_->get_state());
for (iterator->first(); !iterator->done(); iterator->next())
for (auto iterator: automaton_->succ(origin_->get_state()))
{
bdd c = iterator->current_condition();
get_atomics(atomics, c);
}
delete iterator;
// Compute the conjunction of all those atomic properties.
unsigned atomics_size = atomics.size();

71
src/tgba/succiter.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -99,6 +99,73 @@ namespace spot
//@}
};
class tgba;
namespace internal
{
struct SPOT_API succ_iterator
{
protected:
tgba_succ_iterator* it_;
public:
succ_iterator(tgba_succ_iterator* it):
it_(it)
{
}
bool operator==(succ_iterator o) const
{
return it_ == o.it_;
}
bool operator!=(succ_iterator o) const
{
return it_ != o.it_;
}
const tgba_succ_iterator* operator*() const
{
return it_;
}
void operator++()
{
it_->next();
if (it_->done())
it_ = nullptr;
}
};
class SPOT_API succ_iterable
{
protected:
const tgba* aut_;
tgba_succ_iterator* it_;
public:
succ_iterable(const tgba* aut, tgba_succ_iterator* it)
: aut_(aut), it_(it)
{
}
~succ_iterable()
{
delete it_;
}
succ_iterator begin()
{
it_->first();
return it_->done() ? nullptr : it_;
}
succ_iterator end()
{
return nullptr;
}
};
}
}

37
src/tgba/tgba.hh
View file

@ -1,8 +1,9 @@
// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 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.
//
@ -23,12 +24,14 @@
# define SPOT_TGBA_TGBA_HH
#include "state.hh"
#include "succiter.hh"
#include "bdddict.hh"
#include "succiter.hh"
namespace spot
{
/// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata)
class tgba_succ_iterator;
/// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata)
///
/// Spot is centered around the spot::tgba type. This type and its
/// cousins are listed \ref tgba_essentials "here". This is an
@ -42,15 +45,15 @@ namespace spot
/// \ingroup tgba
/// \ingroup tgba_essentials
/// \brief A Transition-based Generalized Büchi Automaton.
/// \brief A Transition-based Generalized Büchi Automaton.
///
/// The acronym TGBA (Transition-based Generalized Büchi Automaton)
/// The acronym TGBA (Transition-based Generalized Büchi Automaton)
/// was coined by Dimitra Giannakopoulou and Flavio Lerda
/// in "From States to Transitions: Improving Translation of LTL
/// Formulae to Büchi Automata". (FORTE'02)
/// Formulae to Büchi Automata". (FORTE'02)
///
/// TGBAs are transition-based, meanings their labels are put
/// on arcs, not on nodes. They use Generalized Büchi acceptance
/// on arcs, not on nodes. They use Generalized Büchi acceptance
/// conditions: there are several acceptance sets (of
/// transitions), and a path can be accepted only if it traverses
/// at least one transition of each set infinitely often.
@ -105,8 +108,18 @@ namespace spot
/// product automaton. Otherwise, 0.
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const = 0;
const state* global_state = nullptr,
const tgba* global_automaton = nullptr) const = 0;
/// \brief Build an iterable over the successors of \a s.
///
/// This is meant to be used as
/// <code>for (auto i: aut->out(s)) { /* i->current_state() */ }</code>.
internal::succ_iterable
succ(const state* s) const
{
return {this, succ_iter(s)};
}
/// \brief Get a formula that must hold whatever successor is taken.
///

26
src/tgba/tgbakvcomplement.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -325,13 +325,11 @@ namespace spot
i != sr_map.end();
++i)
{
tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get());
for (iterator->first(); !iterator->done(); iterator->next())
for (auto iterator: automaton_->succ(i->first.get()))
{
bdd c = iterator->current_condition();
get_atomics(atomics, c);
}
delete iterator;
}
// Compute the conjunction of all those atomic properties.
@ -433,8 +431,7 @@ namespace spot
i != sr_map.end();
++i)
{
tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get());
for (iterator->first(); !iterator->done(); iterator->next())
for (auto iterator: automaton_->succ(i->first.get()))
{
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
@ -449,7 +446,6 @@ namespace spot
highest_current_ranks_[s] = i->second;
}
}
delete iterator;
}
// Highest $O$ set of the algorithm.
@ -460,8 +456,7 @@ namespace spot
i != s_set.end();
++i)
{
tgba_succ_iterator* iterator = automaton_->succ_iter(i->get());
for (iterator->first(); !iterator->done(); iterator->next())
for (auto iterator: automaton_->succ(i->get()))
{
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
@ -470,7 +465,6 @@ namespace spot
highest_state_set_.insert(s);
}
}
delete iterator;
}
current_ranks_ = highest_current_ranks_;
@ -683,22 +677,18 @@ namespace spot
bdd
tgba_kv_complement::compute_support_conditions(const state* state) const
{
tgba_succ_iterator* i = succ_iter(state);
bdd result = bddtrue;
for (i->first(); !i->done(); i->next())
bdd result = bddfalse;
for (auto i: succ(state))
result |= i->current_condition();
delete i;
return result;
}
bdd
tgba_kv_complement::compute_support_variables(const state* state) const
{
tgba_succ_iterator* i = succ_iter(state);
bdd result = bddtrue;
for (i->first(); !i->done(); i->next())
for (auto i: succ(state))
result &= bdd_support(i->current_condition());
delete i;
return result;
}

17
src/tgba/tgbamask.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -36,8 +36,8 @@ namespace spot
{
~succ_iter_filtered()
{
for (first(); !done(); next())
it_->dest->destroy();
for (auto& t: trans_)
t.dest->destroy();
}
void first()
@ -138,15 +138,11 @@ namespace spot
tgba_succ_iterator*
tgba_mask::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
const state*,
const tgba*) const
{
tgba_succ_iterator* it = original_->succ_iter(local_state,
global_state,
global_automaton);
succ_iter_filtered* res = new succ_iter_filtered;
for (it->first(); !it->done(); it->next())
for (auto it: original_->succ(local_state))
{
const state* s = it->current_state();
if (!wanted(s))
@ -159,7 +155,6 @@ namespace spot
it->current_acceptance_conditions() };
res->trans_.push_back(t);
}
delete it;
return res;
}

246
src/tgba/tgbasafracomplement.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 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.
//
@ -153,10 +153,9 @@ namespace spot
name = other.name;
parent = 0;
nodes = other.nodes;
for (child_list::const_iterator i = other.children.begin();
i != other.children.end(); ++i)
for (auto i: other.children)
{
safra_tree* c = new safra_tree(**i);
safra_tree* c = new safra_tree(*i);
c->parent = this;
children.push_back(c);
}
@ -170,11 +169,10 @@ namespace spot
safra_tree::~safra_tree()
{
for (child_list::iterator i = children.begin(); i != children.end(); ++i)
delete *i;
for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i)
(*i)->destroy();
for (auto c: children)
delete c;
for (auto n: nodes)
n->destroy();
}
safra_tree&
@ -237,13 +235,10 @@ namespace spot
hash ^= wang32_hash(name);
hash ^= wang32_hash(marked);
for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
hash ^= (*i)->hash();
for (child_list::const_iterator i = children.begin();
i != children.end();
++i)
hash ^= (*i)->hash();
for (auto n: nodes)
hash ^= n->hash();
for (auto c: children)
hash ^= c->hash();
return hash;
}
@ -262,13 +257,12 @@ namespace spot
safra_tree::max_name() const
{
int max_name = name;
for (child_list::const_iterator i = children.begin();
i != children.end(); ++i)
max_name = std::max(max_name, (*i)->max_name());
for (auto c: children)
max_name = std::max(max_name, c->max_name());
return max_name;
}
/// \brief Get an unused name in the tree for a new node.
/// \brief Get a unused name in the tree for a new node.
///
/// The root of the tree maintains a list of unused names.
/// When this list is empty, new names are computed.
@ -287,9 +281,8 @@ namespace spot
const safra_tree* current = queue.front();
queue.pop_front();
used_names.insert(current->name);
for (child_list::const_iterator i = current->children.begin();
i != current->children.end(); ++i)
queue.push_back(*i);
for (auto c: current->children)
queue.push_back(c);
}
int l = 0;
@ -325,13 +318,13 @@ namespace spot
safra_tree*
safra_tree::branch_accepting(const sba& a)
{
for (child_list::iterator i = children.begin(); i != children.end(); ++i)
(*i)->branch_accepting(a);
for (auto c: children)
c->branch_accepting(a);
subset_t subset;
for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
if (a.state_is_accepting(*i))
subset.insert(*i);
for (auto n: nodes)
if (a.state_is_accepting(n))
subset.insert(n);
if (!subset.empty())
children.push_back(new safra_tree(subset, this, get_new_name()));
@ -354,22 +347,20 @@ namespace spot
{
subset_t new_subset;
for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i)
for (auto n: nodes)
{
cache_t::const_iterator it = cache_transition.find(*i);
cache_t::const_iterator it = cache_transition.find(n);
if (it == cache_transition.end())
continue;
const tr_cache_t& transitions = it->second;
for (tr_cache_t::const_iterator t_it = transitions.begin();
t_it != transitions.end();
++t_it)
for (auto t: transitions)
{
if ((t_it->first & condition) != bddfalse)
if ((t.first & condition) != bddfalse)
{
if (new_subset.find(t_it->second) == new_subset.end())
if (new_subset.find(t.second) == new_subset.end())
{
const state* s = t_it->second->clone();
const state* s = t.second->clone();
new_subset.insert(s);
}
}
@ -377,8 +368,8 @@ namespace spot
}
nodes = new_subset;
for (child_list::iterator i = children.begin(); i != children.end(); ++i)
(*i)->succ_create(condition, cache_transition);
for (auto c: children)
c->succ_create(condition, cache_transition);
return this;
}
@ -391,18 +382,16 @@ namespace spot
safra_tree::normalize_siblings()
{
std::set<const state*, state_ptr_less_than> node_set;
for (child_list::iterator child_it = children.begin();
child_it != children.end();
++child_it)
for (auto c: children)
{
subset_t::iterator node_it = (*child_it)->nodes.begin();
while (node_it != (*child_it)->nodes.end())
subset_t::iterator node_it = c->nodes.begin();
while (node_it != c->nodes.end())
{
if (!node_set.insert(*node_it).second)
{
const state* s = *node_it;
(*child_it)->remove_node_from_children(*node_it);
(*child_it)->nodes.erase(node_it++);
c->remove_node_from_children(*node_it);
c->nodes.erase(node_it++);
s->destroy();
}
else
@ -411,7 +400,7 @@ namespace spot
}
}
(*child_it)->normalize_siblings();
c->normalize_siblings();
}
return this;
@ -421,18 +410,16 @@ namespace spot
void
safra_tree::remove_node_from_children(const state* state)
{
for (child_list::iterator child_it = children.begin();
child_it != children.end();
++child_it)
for (auto c: children)
{
subset_t::iterator it = (*child_it)->nodes.find(state);
if (it != (*child_it)->nodes.end())
subset_t::iterator it = c->nodes.find(state);
if (it != c->nodes.end())
{
const spot::state* s = *it;
(*child_it)->nodes.erase(it);
c->nodes.erase(it);
s->destroy();
}
(*child_it)->remove_node_from_children(state);
c->remove_node_from_children(state);
}
}
@ -470,12 +457,10 @@ namespace spot
safra_tree::mark()
{
std::set<const state*, state_ptr_less_than> node_set;
for (child_list::const_iterator child_it = children.begin();
child_it != children.end();
++child_it)
for (auto c: children)
{
node_set.insert((*child_it)->nodes.begin(), (*child_it)->nodes.end());
(*child_it)->mark();
node_set.insert(c->nodes.begin(), c->nodes.end());
c->mark();
}
char same = node_set.size() == nodes.size();
@ -500,10 +485,8 @@ namespace spot
if (same)
{
marked = true;
for (child_list::iterator i = children.begin();
i != children.end();
++i)
delete *i;
for (auto c: children)
delete c;
children = child_list();
}
@ -526,10 +509,8 @@ namespace spot
assert(bitset.size() > static_cast<unsigned>(name));
if (marked && !nodes.empty())
bitset.set(name);
for (child_list::const_iterator i = children.begin();
i != children.end();
++i)
(*i)->getL(bitset);
for (auto c: children)
c->getL(bitset);
}
/// Returns in which sets U (the semantic differs according to Rabin or
@ -544,10 +525,8 @@ namespace spot
assert(bitset.size() > static_cast<unsigned>(name));
if (!nodes.empty())
bitset.clear(name);
for (child_list::const_iterator i = children.begin();
i != children.end();
++i)
(*i)->getU(bitset);
for (auto c: children)
c->getU(bitset);
}
bool
@ -632,12 +611,11 @@ namespace spot
// Create successors of the Safra's tree.
safra_tree_automaton::transition_list transitions;
for (conjunction_list_t::const_iterator i = conjunction.begin();
i != conjunction.end(); ++i)
for (auto i: conjunction)
{
safra_tree* successor = new safra_tree(*current);
successor->branch_accepting(*sba_aut); // Step 2
successor->succ_create(*i, cache); // Step 3
successor->succ_create(i, cache); // Step 3
successor->normalize_siblings(); // Step 4
successor->remove_empty(); // Step 5
successor->mark(); // Step 6
@ -646,7 +624,7 @@ namespace spot
safra_tree_ptr_equal comparator(successor);
if (st->automaton.find(successor) != st->automaton.end())
{
transitions[*i] = st->automaton.find(successor)->first;
transitions[i] = st->automaton.find(successor)->first;
}
else
{
@ -654,12 +632,12 @@ namespace spot
std::find_if(queue.begin(), queue.end(), comparator);
if (item_in_queue != queue.end())
{
transitions[*i] = *item_in_queue;
transitions[i] = *item_in_queue;
}
else
{
delete_this_successor = false;
transitions[*i] = successor;
transitions[i] = successor;
queue.push_back(successor);
}
}
@ -672,13 +650,9 @@ namespace spot
queue.pop_front();
for (safra_tree::cache_t::iterator i = cache.begin();
i != cache.end();
++i)
for (safra_tree::tr_cache_t::iterator j = i->second.begin();
j != i->second.end();
++j)
j->second->destroy();
for (auto i: cache)
for (auto j: i.second)
j.second->destroy();
// delete node;
}
@ -694,21 +668,17 @@ namespace spot
safra_tree::cache_t& cache,
atomic_list_t& atomic_list)
{
for (safra_tree::subset_t::iterator it = node->nodes.begin();
it != node->nodes.end();
++it)
for (auto n: node->nodes)
{
safra_tree::tr_cache_t transitions;
tgba_succ_iterator* iterator = sba_aut->succ_iter(*it);
for (iterator->first(); !iterator->done(); iterator->next())
for (auto iterator: sba_aut->succ(n))
{
bdd condition = iterator->current_condition();
typedef std::pair<bdd, const state*> bdd_state;
transitions.insert(bdd_state(condition, iterator->current_state()));
set_atomic_list(atomic_list, condition);
}
delete iterator;
cache[*it] = transitions;
cache[n] = transitions;
}
}
@ -741,16 +711,15 @@ namespace spot
{
bdd result = bddtrue;
unsigned position = 1;
for (atomic_list_t::const_iterator a_it = atomics.begin();
a_it != atomics.end();
++a_it, position <<= 1)
for (auto a: atomics)
{
bdd this_atomic;
if (position & i)
this_atomic = bdd_ithvar(*a_it);
this_atomic = bdd_ithvar(a);
else
this_atomic = bdd_nithvar(*a_it);
result = bdd_apply(result, this_atomic, bddop_and);
this_atomic = bdd_nithvar(a);
result &= this_atomic;
position <<= 1;
}
list.insert(result);
}
@ -787,14 +756,12 @@ namespace spot
std::cout << "node" << this_node << "[label=\"";
std::cout << this_node->name << "|";
for (safra_tree::subset_t::const_iterator j = this_node->nodes.begin();
j != this_node->nodes.end();
++j)
for (auto j: this_node->nodes)
{
stnum_t::const_iterator it = node_names.find(*j);
stnum_t::const_iterator it = node_names.find(j);
int name;
if (it == node_names.end())
name = node_names[*j] = current_node++;
name = node_names[j] = current_node++;
else
name = it->second;
std::cout << name << ", ";
@ -820,8 +787,6 @@ namespace spot
{
typedef safra_tree_automaton::automaton_t::reverse_iterator
automaton_cit;
typedef safra_tree_automaton::transition_list::const_iterator
trans_cit;
stnum_t node_names;
int current_node = 0;
int nb_accepting_conditions = a->get_nb_acceptance_pairs();
@ -840,20 +805,19 @@ namespace spot
std::cout << "}" << std::endl;
// Successors.
for (trans_cit j = i->second.begin(); j != i->second.end(); ++j)
for (const auto& j: i->second)
std::cout << "node" << i->first << "->"
<< "node" << j->second <<
" [label=\"" << bddset << j->first << "\"];" << std::endl;
<< "node" << j.second <<
" [label=\"" << bddset << j.first << "\"];" << std::endl;
}
// Output the real name of all states.
std::cout << "{ rank=sink; legend [shape=none,margin=0,label=<\n"
<< "<TABLE BORDER='1' CELLBORDER='0' CELLSPACING='0'>\n";
for (stnum_t::const_iterator it = node_names.begin();
it != node_names.end(); ++it)
std::cout << "<TR><TD>" << it->second << "</TD><TD>"
<< a->get_sba()->format_state(it->first)
for (const auto& nn: node_names)
std::cout << "<TR><TD>" << nn.second << "</TD><TD>"
<< a->get_sba()->format_state(nn.first)
<< "</TD></TR>\n";
std::cout << "</TABLE>\n"
<< ">]}" << std::endl;
@ -1008,8 +972,8 @@ namespace spot
virtual
~tgba_safra_complement_succ_iterator()
{
for (succ_list_t::iterator i = list_.begin(); i != list_.end(); ++i)
delete i->second;
for (auto& p: list_)
delete p.second;
}
virtual void first();
@ -1076,12 +1040,8 @@ namespace spot
safra_tree_automaton::~safra_tree_automaton()
{
for (automaton_t::iterator i = automaton.begin();
i != automaton.end();
++i)
{
delete i->first;
}
for (auto& p: automaton)
delete p.first;
delete a_;
}
@ -1092,10 +1052,8 @@ namespace spot
return max_nb_pairs_;
int max = -1;
for (automaton_t::const_iterator i = automaton.begin();
i != automaton.end();
++i)
max = std::max(max, i->first->max_name());
for (auto& p: automaton)
max = std::max(max, p.first->max_name());
return max_nb_pairs_ = max + 1;
}
@ -1215,8 +1173,6 @@ namespace spot
safra_tree_automaton::automaton_t::const_iterator tr =
a->automaton.find(const_cast<safra_tree*>(s->get_safra()));
typedef safra_tree_automaton::transition_list::const_iterator trans_iter;
if (tr != a->automaton.end())
{
bdd condition = bddfalse;
@ -1226,14 +1182,14 @@ namespace spot
if (!s->get_use_bitset()) // if \delta'(q, a)
{
for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i)
for (auto& p: tr->second)
{
state_complement* s1 = new state_complement(e->clone(), e->clone(),
i->second, false);
p.second, false);
state_complement* s2 = new state_complement(e->clone(), e->clone(),
i->second, true);
succ_list.insert(std::make_pair(i->first, s1));
succ_list.insert(std::make_pair(i->first, s2));
p.second, true);
succ_list.insert(std::make_pair(p.first, s1));
succ_list.insert(std::make_pair(p.first, s2));
}
}
else
@ -1254,19 +1210,19 @@ namespace spot
// \delta'((q, I, J), a) if I'\subseteq J'
if (newI->is_subset_of(*newJ))
{
for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i)
for (auto& p: tr->second)
{
st = new state_complement(e->clone(), e->clone(), i->second, true);
succ_list.insert(std::make_pair(i->first, st));
st = new state_complement(e->clone(), e->clone(), p.second, true);
succ_list.insert(std::make_pair(p.first, st));
}
condition = the_acceptance_cond_;
}
else // \delta'((q, I, J), a)
{
for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i)
for (auto& p: tr->second)
{
st = new state_complement(newI, newJ, i->second, true);
succ_list.insert(std::make_pair(i->first, st));
st = new state_complement(newI, newJ, p.second, true);
succ_list.insert(std::make_pair(p.first, st));
}
}
delete newI;
@ -1277,11 +1233,11 @@ namespace spot
bitvect* pending = S.clone();
*pending |= *l;
*pending -= *u;
for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i)
for (auto& p: tr->second)
{
st = new state_complement(pending->clone(), e->clone(),
i->second, true);
succ_list.insert(std::make_pair(i->first, st));
p.second, true);
succ_list.insert(std::make_pair(p.first, st));
}
delete pending;
@ -1341,16 +1297,14 @@ namespace spot
const state_complement* s = down_cast<const state_complement*>(state);
assert(s);
typedef safra_tree_automaton::automaton_t::const_iterator auto_it;
typedef safra_tree_automaton::transition_list::const_iterator trans_it;
auto_it node(a->automaton.find(const_cast<safra_tree*>(s->get_safra())));
if (node == a->automaton.end())
return bddtrue;
bdd res = bddtrue;
trans_it i;
for (i = node->second.begin(); i != node->second.end(); ++i)
res |= i->first;
for (auto& i: node->second)
res |= i.first;
return res;
}
@ -1361,16 +1315,14 @@ namespace spot
const state_complement* s = down_cast<const state_complement*>(state);
assert(s);
typedef safra_tree_automaton::automaton_t::const_iterator auto_it;
typedef safra_tree_automaton::transition_list::const_iterator trans_it;
auto_it node(a->automaton.find(const_cast<safra_tree*>(s->get_safra())));
if (node == a->automaton.end())
return bddtrue;
bdd res = bddtrue;
trans_it i;
for (i = node->second.begin(); i != node->second.end(); ++i)
res &= bdd_support(i->first);
for (auto& i: node->second)
res &= bdd_support(i.first);
return res;
}

28
src/tgba/tgbatba.cc
View file

@ -1,8 +1,9 @@
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita.
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita.
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 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.
//
@ -517,10 +518,12 @@ namespace spot
return i->second;
bdd common = a_->all_acceptance_conditions();
tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done() && common != bddfalse; it->next())
common &= it->current_acceptance_conditions();
delete it;
for (auto it: a_->succ(s))
{
common &= it->current_acceptance_conditions();
if (common == bddfalse)
break;
}
// Populate cache
accmap_[s->clone()] = common;
@ -537,10 +540,8 @@ namespace spot
return i->second;
bdd common = bddfalse;
tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done(); it->next())
for (auto it: a_->succ(s))
common |= it->current_acceptance_conditions();
delete it;
// Populate cache
accmapu_[s->clone()] = common;
@ -618,8 +619,7 @@ namespace spot
bdd all = a->all_acceptance_conditions();
state* init = a->get_init_state();
tgba_succ_iterator* it = a->succ_iter(init);
for (it->first(); !it->done(); it->next())
for (auto it: a->succ(init))
{
// Look only for transitions that are accepting.
if (all != it->current_acceptance_conditions())
@ -635,13 +635,11 @@ namespace spot
// The cycle_start_ points to the right starting
// point already, so just return.
dest->destroy();
delete it;
init->destroy();
return;
}
dest->destroy();
}
delete it;
init->destroy();
}

7
src/tgbaalgos/compsusp.cc
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.
//
@ -277,8 +277,7 @@ namespace spot
const state* rs = p.second;
int src = seen[p];
tgba_succ_iterator* li = left->succ_iter(ls);
for (li->first(); !li->done(); li->next())
for (auto li: left->succ(ls))
{
state_pair d(li->current_state(), ris);
bdd lc = li->current_condition();

4
src/tgbaalgos/cutscc.cc
View file

@ -55,8 +55,7 @@ namespace spot
{
cur = tovisit.front();
tovisit.pop();
tgba_succ_iterator* sit = a->succ_iter(cur);
for (sit->first(); !sit->done(); sit->next())
for (auto sit: a->succ(cur))
{
cur_format = a->format_state(cur);
state* dst = sit->current_state();
@ -78,7 +77,6 @@ namespace spot
dst->destroy();
}
}
delete sit;
}
return sub_a;
}

12
src/tgbaalgos/degen.cc
View file

@ -88,8 +88,7 @@ namespace spot
unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0;
bdd common = a_->all_acceptance_conditions();
bdd union_ = bddfalse;
tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done(); it->next())
for (auto it: a_->succ(s))
{
// Ignore transitions that leave the SCC of s.
const state* d = it->current_state();
@ -102,7 +101,6 @@ namespace spot
common &= set;
union_ |= set;
}
delete it;
cache_entry e(common, union_);
return cache_.insert(std::make_pair(s, e)).first;
}
@ -150,8 +148,7 @@ namespace spot
if (p.second)
{
bdd all = a_->all_acceptance_conditions();
tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done(); it->next())
for (auto it: a_->succ(s))
{
// Look only for transitions that are accepting.
if (all != it->current_acceptance_conditions())
@ -164,7 +161,6 @@ namespace spot
break;
}
}
delete it;
}
return p.first->second;
}
@ -387,8 +383,7 @@ namespace spot
if (use_scc)
s_scc = m.scc_of_state(s.first);
tgba_succ_iterator* i = a->succ_iter(s.first);
for (i->first(); !i->done(); i->next())
for (auto i: a->succ(s.first))
{
degen_state d(uniq(i->current_state()), 0);
@ -576,7 +571,6 @@ namespace spot
t->condition |= i->current_condition();
}
}
delete i;
tr_cache.clear();
}

31
src/tgbaalgos/emptiness.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -345,29 +345,26 @@ namespace spot
next = l->begin()->s;
}
// browse the actual outgoing transitions
tgba_succ_iterator* j = a->succ_iter(s);
s->destroy(); // FIXME: is it always legitimate to destroy s before j?
for (j->first(); !j->done(); j->next())
// browse the actual outgoing transitions and
// look for next;
const state* the_next = nullptr;
for (auto j: a->succ(s))
{
if (j->current_condition() != label
|| j->current_acceptance_conditions() != acc)
continue;
const state* s2 = j->current_state();
if (s2->compare(next) != 0)
if (s2->compare(next) == 0)
{
s2->destroy();
continue;
}
else
{
s = s2;
break;
}
the_next = s2;
break;
}
s2->destroy();
}
assert(!j->done());
delete j;
assert(res);
s->destroy();
s = the_next;
state_map::const_iterator its = seen.find(next);
if (its == seen.end())

12
src/tgbaalgos/isdet.cc
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.
//
@ -44,10 +44,9 @@ namespace spot
const state* src = todo.front();
todo.pop_front();
tgba_succ_iterator* i = aut->succ_iter(src);
bool nondeterministic = false;
bdd available = bddtrue;
for (i->first(); !i->done(); i->next())
for (auto i: aut->succ(src))
{
// If we know the state is nondeterministic, just skip the
// test for the remaining transitions. But don't break
@ -67,7 +66,6 @@ namespace spot
else
dst->destroy();
}
delete i;
res += nondeterministic;
if (!count && nondeterministic)
break;
@ -110,9 +108,8 @@ namespace spot
const state* src = todo.front();
todo.pop_front();
tgba_succ_iterator* i = aut->succ_iter(src);
bdd available = bddtrue;
for (i->first(); !i->done(); i->next())
for (auto i: aut->succ(src))
{
available -= i->current_condition();
const state* dst = i->current_state();
@ -121,7 +118,6 @@ namespace spot
else
dst->destroy();
}
delete i;
if (available != bddfalse)
{
complete = false;

43
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
@ -152,8 +152,8 @@ namespace spot
~translate_dict()
{
fv_map::iterator i;
for (i = next_map.begin(); i != next_map.end(); ++i)
i->first->destroy();
for (auto& i: next_map)
i.first->destroy();
dict->unregister_all_my_variables(this);
flagged_formula_to_bdd_map::iterator j = ltl_bdd_.begin();
@ -306,10 +306,10 @@ namespace spot
{
fv_map::const_iterator fi;
os << "Next Variables:" << std::endl;
for (fi = next_map.begin(); fi != next_map.end(); ++fi)
for (auto& fi: next_map)
{
os << " " << fi->second << ": Next[";
to_string(fi->first, os) << "]" << std::endl;
os << " " << fi.second << ": Next[";
to_string(fi.first, os) << "]" << std::endl;
}
os << "Shared Dict:" << std::endl;
dict->dump(os);
@ -1005,9 +1005,8 @@ namespace spot
ratexp_to_dfa::~ratexp_to_dfa()
{
std::vector<tgba_explicit_formula*>::const_iterator it;
for (it = automata_.begin(); it != automata_.end(); ++it)
delete *it;
for (auto i: automata_)
delete i;
}
tgba_explicit_formula*
@ -1087,13 +1086,12 @@ namespace spot
// SCC are numbered in topological order
for (unsigned n = 0; n < scc_count; ++n)
{
bool coacc = false;
const std::list<const state*>& st = sm->states_of(n);
// The SCC is coaccessible if any of its states
// is final (i.e., it accepts [*0])...
std::list<const state*>::const_iterator it;
for (it = st.begin(); it != st.end(); ++it)
if (a->get_label(*it)->accepts_eword())
bool coacc = false;
const std::list<const state*>& st = sm->states_of(n);
for (auto l: st)
if (a->get_label(l)->accepts_eword())
{
coacc = true;
break;
@ -1101,10 +1099,8 @@ namespace spot
if (!coacc)
{
// ... or if any of its successors is coaccessible.
const scc_map::succ_type& succ = sm->succ(n);
for (scc_map::succ_type::const_iterator i = succ.begin();
i != succ.end(); ++i)
if (coaccessible[i->first])
for (auto& i: sm->succ(n))
if (coaccessible[i.first])
{
coacc = true;
break;
@ -1113,13 +1109,13 @@ namespace spot
if (!coacc)
{
// Mark all formulas of this SCC as useless.
for (it = st.begin(); it != st.end(); ++it)
f2a_[a->get_label(*it)] = 0;
for (auto f: st)
f2a_[a->get_label(f)] = nullptr;
}
else
{
for (it = st.begin(); it != st.end(); ++it)
f2a_[a->get_label(*it)] = a;
for (auto f: st)
f2a_[a->get_label(f)] = a;
}
coaccessible[n] = coacc;
}
@ -1136,6 +1132,7 @@ namespace spot
}
}
// FIXME: use the new tgba::succ() interface
tgba_succ_iterator*
ratexp_to_dfa::succ(const formula* f)
{

92
src/tgbaalgos/minimize.cc
View file

@ -93,26 +93,24 @@ namespace spot
tovisit.push(init);
seen->insert(init);
while (!tovisit.empty())
{
const state* src = tovisit.front();
tovisit.pop();
tgba_succ_iterator* sit = a->succ_iter(src);
for (sit->first(); !sit->done(); sit->next())
{
const state* dst = sit->current_state();
// Is it a new state ?
if (seen->find(dst) == seen->end())
const state* src = tovisit.front();
tovisit.pop();
for (auto sit: a->succ(src))
{
// Register the successor for later processing.
tovisit.push(dst);
seen->insert(dst);
const state* dst = sit->current_state();
// Is it a new state ?
if (seen->find(dst) == seen->end())
{
// Register the successor for later processing.
tovisit.push(dst);
seen->insert(dst);
}
else
dst->destroy();
}
else
dst->destroy();
}
delete sit;
}
}
// From the base automaton and the list of sets, build the minimal
@ -128,13 +126,13 @@ namespace spot
std::list<hash_set*>::iterator sit;
unsigned num = 0;
for (sit = sets.begin(); sit != sets.end(); ++sit)
{
hash_set::iterator hit;
hash_set* h = *sit;
for (hit = h->begin(); hit != h->end(); ++hit)
state_num[*hit] = num;
++num;
}
{
hash_set::iterator hit;
hash_set* h = *sit;
for (hit = h->begin(); hit != h->end(); ++hit)
state_num[*hit] = num;
++num;
}
typedef state_explicit_number::transition trs;
sba_explicit_number* res = new sba_explicit_number(a->get_dict());
// For each transition in the initial automaton, add the corresponding
@ -142,31 +140,29 @@ namespace spot
if (!final->empty())
res->declare_acceptance_condition(ltl::constant::true_instance());
for (sit = sets.begin(); sit != sets.end(); ++sit)
{
hash_set::iterator hit;
hash_set* h = *sit;
{
hash_set::iterator hit;
hash_set* h = *sit;
// Pick one state.
const state* src = *h->begin();
unsigned src_num = state_num[src];
bool accepting = (final->find(src) != final->end());
// Pick one state.
const state* src = *h->begin();
unsigned src_num = state_num[src];
bool accepting = (final->find(src) != final->end());
// Connect it to all destinations.
tgba_succ_iterator* succit = a->succ_iter(src);
for (succit->first(); !succit->done(); succit->next())
{
const state* dst = succit->current_state();
hash_map::const_iterator i = state_num.find(dst);
dst->destroy();
if (i == state_num.end()) // Ignore useless destinations.
continue;
trs* t = res->create_transition(src_num, i->second);
res->add_conditions(t, succit->current_condition());
if (accepting)
res->add_acceptance_condition(t, ltl::constant::true_instance());
}
delete succit;
}
// Connect it to all destinations.
for (auto succit: a->succ(src))
{
const state* dst = succit->current_state();
hash_map::const_iterator i = state_num.find(dst);
dst->destroy();
if (i == state_num.end()) // Ignore useless destinations.
continue;
trs* t = res->create_transition(src_num, i->second);
res->add_conditions(t, succit->current_condition());
if (accepting)
res->add_acceptance_condition(t, ltl::constant::true_instance());
}
}
res->merge_transitions();
const state* init_state = a->get_init_state();
unsigned init_num = state_num[init_state];
@ -362,8 +358,7 @@ namespace spot
{
const state* src = *hi;
bdd f = bddfalse;
tgba_succ_iterator* si = det_a->succ_iter(src);
for (si->first(); !si->done(); si->next())
for (auto si: det_a->succ(src))
{
const state* dst = si->current_state();
hash_map::const_iterator i = state_set_map.find(dst);
@ -378,7 +373,6 @@ namespace spot
continue;
f |= (bdd_ithvar(i->second) & si->current_condition());
}
delete si;
// Have we already seen this formula ?
bdd_states_map::iterator bsi = bdd_map.find(f);

51
src/tgbaalgos/powerset.cc
View file

@ -72,8 +72,8 @@ namespace spot
bdd all_vars = bddtrue;
power_state::const_iterator i;
for (i = src.begin(); i != src.end(); ++i)
all_vars &= aut->support_variables(*i);
for (auto s: src)
all_vars &= aut->support_variables(s);
// Compute all possible combinations of these variables.
bdd all_conds = bddtrue;
@ -84,17 +84,10 @@ namespace spot
// Construct the set of all states reachable via COND.
power_state dest;
for (i = src.begin(); i != src.end(); ++i)
{
tgba_succ_iterator *si = aut->succ_iter(*i);
for (si->first(); !si->done(); si->next())
if ((cond >> si->current_condition()) == bddtrue)
{
const state* s = pm.canonicalize(si->current_state());
dest.insert(s);
}
delete si;
}
for (auto s: src)
for (auto si: aut->succ(s))
if ((cond >> si->current_condition()) == bddtrue)
dest.insert(pm.canonicalize(si->current_state()));
if (dest.empty())
continue;
// Add that transition.
@ -177,10 +170,8 @@ namespace spot
// }
bdd acc = aut_->all_acceptance_conditions();
for (trans_set::iterator i = all_.begin(); i != all_.end(); ++i)
{
(*i)->acceptance_conditions = acc;
}
for (auto i: all_)
i->acceptance_conditions = acc;
return threshold_ != 0 && cycles_left_ == 0;
}
@ -213,17 +204,13 @@ namespace spot
// start of the loop in the determinized automaton.
const power_map::power_state& ps =
refmap_.states_of(a->get_label(begin->ts->first));
for (power_map::power_state::const_iterator it = ps.begin();
it != ps.end() && !accepting; ++it)
for (auto s: ps)
{
// Construct a product between
// LOOP_A, and ORIG_A starting in *IT.
tgba* p = new tgba_product_init(&loop_a, ref_,
loop_a_init, *it);
// LOOP_A, and ORIG_A starting in S.
tgba* p = new tgba_product_init(&loop_a, ref_, loop_a_init, s);
//spot::dotty_reachable(std::cout, p);
couvreur99_check* ec = down_cast<couvreur99_check*>(couvreur99(p));
assert(ec);
emptiness_check_result* res = ec->check();
@ -232,6 +219,8 @@ namespace spot
delete res;
delete ec;
delete p;
if (accepting)
break;
}
loop_a_init->destroy();
@ -242,8 +231,8 @@ namespace spot
print_set(std::ostream& o, const trans_set& s) const
{
o << "{ ";
for (trans_set::const_iterator i = s.begin(); i != s.end(); ++i)
o << *i << " ";
for (auto i: s)
o << i << " ";
o << "}";
return o;
}
@ -272,15 +261,11 @@ namespace spot
}
else
{
for (trans_set::const_iterator i = ts.begin(); i != ts.end(); ++i)
for (auto t: ts)
{
trans* t = *i;
reject_.insert(t);
for (set_set::iterator j = accept_.begin();
j != accept_.end(); ++j)
{
j->erase(t);
}
for (auto& j: accept_)
j.erase(t);
all_.erase(t);
}
}

4
src/tgbaalgos/safety.cc
View file

@ -85,8 +85,7 @@ namespace spot
const state* s = todo.front();
todo.pop_front();
tgba_succ_iterator* it = aut->succ_iter(s);
for (it->first(); !it->done(); it->next())
for (auto it: aut->succ(s))
{
bdd acc = it->current_acceptance_conditions();
if (acc != all_acc)
@ -97,7 +96,6 @@ namespace spot
if (const state* d = seen.is_new(it->current_state()))
todo.push_back(d);
}
delete it;
}
return all_accepting;
}

181
src/tgbaalgos/simulation.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// 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.
@ -156,12 +156,10 @@ namespace spot
void add_to_map(const std::list<constraint>& list,
map_constraint& feed_me)
{
for (std::list<constraint>::const_iterator it = list.begin();
it != list.end();
++it)
for (auto& p: list)
{
if (feed_me.find(it->first) == feed_me.end())
feed_me[it->first] = it->second;
if (feed_me.find(p.first) == feed_me.end())
feed_me[p.first] = p.second;
}
}
@ -434,13 +432,8 @@ namespace spot
// We fetch the result the run of acc_compl_automaton which
// has recorded all the state in a hash table, and we set all
// to init.
for (map_state_bdd::iterator it
= acc_compl.previous_class_.begin();
it != acc_compl.previous_class_.end();
++it)
{
previous_class_[it->first] = init;
}
for (auto& p: acc_compl.previous_class_)
previous_class_[p.first] = init;
// Put all the anonymous variable in a queue, and record all
// of these in a variable all_class_var_ which will be used
@ -481,26 +474,21 @@ namespace spot
// We run through the map bdd/list<state>, and we update
// the previous_class_ with the new data.
for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end();
++it)
for (auto& p: bdd_lstate_)
{
for (std::list<const state*>::iterator it_s = it->second.begin();
it_s != it->second.end();
++it_s)
{
// If the signature of a state is bddfalse (no
// transitions) the class of this state is bddfalse
// instead of an anonymous variable. It allows
// simplifications in the signature by removing a
// transition which has as a destination a state with
// no outgoing transition.
if (it->first == bddfalse)
previous_class_[*it_s] = bddfalse;
else
previous_class_[*it_s] = *it_bdd;
}
++it_bdd;
// If the signature of a state is bddfalse (no
// transitions) the class of this state is bddfalse
// instead of an anonymous variable. It allows
// simplifications in the signature by removing a
// transition which has as a destination a state with
// no outgoing transition.
if (p.first == bddfalse)
for (auto s: p.second)
previous_class_[s] = bddfalse;
else
for (auto s: p.second)
previous_class_[s] = *it_bdd;
++it_bdd;
}
}
@ -533,10 +521,9 @@ namespace spot
// Take a state and compute its signature.
bdd compute_sig(const state* src)
{
tgba_succ_iterator* sit = a_->succ_iter(src);
bdd res = bddfalse;
for (sit->first(); !sit->done(); sit->next())
for (auto sit: a_->succ(src))
{
const state* dst = sit->current_state();
bdd acc = bddtrue;
@ -574,7 +561,6 @@ namespace spot
if (Cosimulation && initial_state == src)
res |= bdd_initial;
delete sit;
return res;
}
@ -585,12 +571,9 @@ namespace spot
// all the reachable states of this automaton. We do not
// have to make (again) a traversal. We just have to run
// through this map.
for (std::list<const state*>::const_iterator it = order_.begin();
it != order_.end();
++it)
for (auto s: order_)
{
const state* src = previous_class_.find(*it)->first;
const state* src = previous_class_.find(s)->first;
bdd_lstate_[compute_sig(src)].push_back(src);
}
}
@ -636,22 +619,17 @@ namespace spot
std::list<bdd>::iterator it_bdd = used_var_.begin();
for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end();
++it)
for (auto& p: bdd_lstate_)
{
// If the signature of a state is bddfalse (which is
// roughly equivalent to no transition) the class of
// this state is bddfalse instead of an anonymous
// variable. It allows simplifications in the signature
// by removing a transition which has as a destination a
// state with no outgoing transition.
if (it->first == bddfalse)
now_to_next[it->first] = bddfalse;
else
now_to_next[it->first] = *it_bdd;
++it_bdd;
// If the signature of a state is bddfalse (no
// transitions) the class of this state is bddfalse
// instead of an anonymous variable. It allows
// simplifications in the signature by removing a
// transition which has as a destination a state with
// no outgoing transition.
now_to_next[p.first] =
(p.first == bddfalse) ? bddfalse : *it_bdd;
++it_bdd;
}
update_po(now_to_next, relation_);
@ -745,11 +723,10 @@ namespace spot
bdd nonapvars = sup_all_acc & bdd_support(all_class_var_);
// Create one state per partition.
for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end(); ++it)
for (auto& p: bdd_lstate_)
{
res->add_state(++current_max);
bdd part = previous_class_[*it->second.begin()];
bdd part = previous_class_[*p.second.begin()];
// The difference between the two next lines is:
// the first says "if you see A", the second "if you
@ -771,12 +748,10 @@ namespace spot
// For each partition, we will create
// all the transitions between the states.
for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end();
++it)
for (auto& p: bdd_lstate_)
{
// Get the signature.
bdd sig = compute_sig(*(it->second.begin()));
bdd sig = compute_sig(*(p.second.begin()));
if (Cosimulation)
sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));
@ -840,7 +815,7 @@ namespace spot
// know the source, we must take a random state in
// the list which is in the class we currently
// work on.
int src = bdd2state[previous_class_[*it->second.begin()]];
int src = bdd2state[previous_class_[*p.second.begin()]];
int dst = bdd2state[dest];
if (Cosimulation)
@ -875,15 +850,13 @@ namespace spot
for (unsigned snum = current_max; snum > 0; --snum)
{
const state* s = res->get_state(snum);
tgba_succ_iterator* it = res->succ_iter(s);
bdd acc = accst[snum];
for (it->first(); !it->done(); it->next())
for (auto it: res->succ(s))
{
tgba_explicit_number::transition* t =
res->get_transition(it);
t->acceptance_conditions = acc;
}
delete it;
}
res_is_deterministic = nb_minato == nb_satoneset;
@ -899,33 +872,23 @@ namespace spot
// where is the new class name.
void print_partition()
{
for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end();
++it)
for (auto& p: bdd_lstate_)
{
std::cerr << "partition: "
<< bdd_format_isop(a_->get_dict(), it->first)
<< bdd_format_isop(a_->get_dict(), p.first)
<< std::endl;
for (std::list<const state*>::iterator it_s = it->second.begin();
it_s != it->second.end();
++it_s)
{
std::cerr << " - "
<< a_->format_state(*it_s) << std::endl;
}
for (auto s: p.second)
std::cerr << " - " << a_->format_state(s) << '\n';
}
std::cerr << "\nPrevious iteration\n" << std::endl;
for (map_state_bdd::const_iterator it = previous_class_.begin();
it != previous_class_.end();
++it)
for (auto p: previous_class_)
{
std::cerr << a_->format_state(it->first)
std::cerr << a_->format_state(p.first)
<< " was in "
<< bdd_format_set(a_->get_dict(), it->second)
<< std::endl;
<< bdd_format_set(a_->get_dict(), p.second)
<< '\n';
}
}
@ -1039,13 +1002,12 @@ namespace spot
// signature later.
bdd dont_care_compute_sig(const state* src)
{
tgba_succ_iterator* sit = a_->succ_iter(src);
bdd res = bddfalse;
unsigned scc = scc_map_->scc_of_state(old_name_[src]);
bool sccacc = scc_map_->accepting(scc);
for (sit->first(); !sit->done(); sit->next())
for (auto sit: a_->succ(src))
{
const state* dst = sit->current_state();
bdd cl = previous_class_[dst];
@ -1061,8 +1023,6 @@ namespace spot
bdd to_add = acc & sit->current_condition() & relation_[cl];
res |= to_add;
}
delete sit;
return res;
}
@ -1315,22 +1275,15 @@ namespace spot
}
// Iterate over the transitions of both states.
for (map_bdd_bdd::const_iterator lit = sigl_map.begin();
lit != sigl_map.end(); ++lit)
for (map_bdd_bdd::iterator rit = sigr_map.begin();
rit != sigr_map.end(); ++rit)
{
// And create constraints if any of the transitions
// is out of the SCC and the left could imply the right.
if ((is_out_scc(lit->second) || is_out_scc(rit->second))
&& (bdd_exist(lit->first, on_cycle_) ==
bdd_exist(rit->first, on_cycle_)))
{
create_simple_constraint(lit->second, rit->second,
left, right, res);
}
}
for (auto lp: sigl_map)
for (auto rp: sigr_map)
// And create constraints if any of the transitions
// is out of the SCC and the left could imply the right.
if ((is_out_scc(lp.second) || is_out_scc(rp.second))
&& (bdd_exist(lp.first, on_cycle_) ==
bdd_exist(rp.first, on_cycle_)))
create_simple_constraint(lp.second, rp.second,
left, right, res);
return res;
}
@ -1358,11 +1311,9 @@ namespace spot
bdd_lstate_.clear();
// Compute the don't care signature for all the states.
for (std::list<const state*>::const_iterator my_it = order_.begin();
my_it != order_.end();
++my_it)
for (auto s: order_)
{
map_state_bdd::iterator it = previous_class_.find(*my_it);
map_state_bdd::iterator it = previous_class_.find(s);
const state* src = it->first;
bdd sig = dont_care_compute_sig(src);
@ -1384,12 +1335,8 @@ namespace spot
constraint_list cc;
for (map_bdd_bdd::iterator it = relation.begin();
it != relation.end();
++it)
{
revert_relation_[it->second] = class2state[it->first];
}
for (auto p: relation)
revert_relation_[p.second] = class2state[p.first];
int number_constraints = 0;
relation_ = relation;
@ -1397,11 +1344,9 @@ namespace spot
// order_ is here for the determinism. Here we make the diff
// between the two tables: imply and could_imply.
for (std::list<const state*>::const_iterator my_it = order_.begin();
my_it != order_.end();
++my_it)
for (auto s: order_)
{
map_state_bdd::iterator it = previous_class_.find(*my_it);
map_state_bdd::iterator it = previous_class_.find(s);
assert(relation.find(it->second) != relation.end());
assert(dont_care_relation.find(it->second)
!= dont_care_relation.end());

8
src/tgbaalgos/tau03.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -189,8 +189,7 @@ namespace spot
<< std::endl;
typename heap::color_ref c = h.get_color_ref(f.s);
assert(!c.is_white());
tgba_succ_iterator* i = a_->succ_iter(f.s);
for (i->first(); !i->done(); i->next())
for (auto i: a_->succ(f.s))
{
inc_transitions();
const state *s_prime = i->current_state();
@ -211,7 +210,6 @@ namespace spot
dfs_red(acu);
}
}
delete i;
if (c.get_acc() == all_cond)
{
trace << "DFS_BLUE propagation is successful, report a"

30
src/tgbatest/explicit2.cc
View file

@ -1,4 +1,5 @@
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -38,16 +39,13 @@ create_tgba_explicit_string(bdd_dict* d)
tgba->create_transition(s1, s2);
(void) t;
tgba_explicit_succ_iterator<state_explicit_string>* it
= tgba->succ_iter(tgba->get_init_state());
for (it->first(); !it->done(); it->next())
for (auto it: tgba->succ(tgba->get_init_state()))
{
state_explicit_string* se = it->current_state();
state_explicit_string* se =
down_cast<state_explicit_string*>(it->current_state());
std::cout << se->label() << std::endl;
se->destroy();
}
delete it;
delete tgba;
}
@ -63,16 +61,13 @@ create_tgba_explicit_number(bdd_dict* d)
tgba->create_transition(s1, s2);
(void) t;
tgba_explicit_succ_iterator<state_explicit_number>* it =
tgba->succ_iter(tgba->get_init_state());
for (it->first(); !it->done(); it->next())
for (auto it: tgba->succ(tgba->get_init_state()))
{
state_explicit_number* s = it->current_state();
state_explicit_number* s =
down_cast<state_explicit_number*>(it->current_state());
std::cout << s->label() << std::endl;
s->destroy();
}
delete it;
delete tgba;
}
@ -89,16 +84,13 @@ create_tgba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e)
tgba->create_transition(s1, s2);
(void) t;
tgba_explicit_succ_iterator<state_explicit_formula>* it =
tgba->succ_iter(tgba->get_init_state());
for (it->first(); !it->done(); it->next())
for (auto it: tgba->succ(tgba->get_init_state()))
{
state_explicit_formula* s = it->current_state();
state_explicit_formula* s =
down_cast<state_explicit_formula*>(it->current_state());
to_string(s->label(), std::cout) << std::endl;
s->destroy();
}
delete it;
delete tgba;
}