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

emptiness: Upgrade to tgba_digraph.

Browse source 
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: Use
tgba_digraph instead of tgba_explicit_string.
This commit is contained in:
Alexandre Duret-Lutz 2014-07-04 01:23:24 +02:00
parent 97e3eb7655
commit ee087b5996
2 changed files with 23 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/tgbaalgos/emptiness.cc
View file

@ -24,7 +24,6 @@
#include "emptiness.hh"
#include "tgba/tgba.hh"
#include "tgba/bddprint.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gv04.hh"
#include "tgbaalgos/magic.hh"
@ -283,30 +282,21 @@ namespace spot
// tgba_run_to_tgba
//////////////////////////////////////////////////////////////////////
namespace
{
std::string format_state(const tgba* a, const state* s, int n)
{
std::ostringstream os;
os << a->format_state(s) << " (" << n << ')';
return os.str();
}
}
tgba*
tgba_digraph*
tgba_run_to_tgba(const tgba* a, const tgba_run* run)
{
tgba_explicit_string* res = new tgba_explicit_string(a->get_dict());
res->copy_acceptance_conditions_of(a);
auto d = a->get_dict();
auto res = new tgba_digraph(d);
auto& g = res->get_graph();
d->register_all_variables_of(a, res);
const state* s = a->get_init_state();
int number = 1;
state_explicit_string* source;
state_explicit_string* dest;
unsigned src;
unsigned dst;
const tgba_run::steps* l;
bdd seen_acc = bddfalse;
typedef std::unordered_map<const state*, state_explicit_string*,
typedef std::unordered_map<const state*, unsigned,
state_ptr_hash, state_ptr_equal> state_map;
state_map seen;
@ -318,9 +308,8 @@ namespace spot
tgba_run::steps::const_iterator i = l->begin();
assert(s->compare(i->s) == 0);
source = res->set_init_state(format_state(a, i->s, number));
++number;
seen.insert(std::make_pair(i->s, source));
src = g.new_state();
seen.insert(std::make_pair(i->s, src));
for (; i != l->end();)
{
@ -366,32 +355,23 @@ namespace spot
s->destroy();
s = the_next;
state_map::const_iterator its = seen.find(next);
if (its == seen.end())
{
dest = res->add_state(format_state(a, next, number));
++number;
seen.insert(std::make_pair(next, dest));
}
else
dest = its->second;
state_explicit_string::transition* t =
res->create_transition(source, dest);
res->add_conditions(t, label);
res->add_acceptance_conditions(t, acc);
source = dest;
auto p = seen.insert(std::make_pair(next, 0));
if (p.second)
p.first->second = g.new_state();
dst = p.first->second;
g.new_transition(src, dst, label, acc);
src = dst;
// Sum acceptance conditions.
if (l == &run->cycle && i != l->begin())
seen_acc |= acc;
seen_acc |= acc;
}
s->destroy();
assert(seen_acc == a->all_acceptance_conditions());
res->merge_transitions();
return res;
}

7
src/tgbaalgos/emptiness.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
// 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.
@ -29,6 +29,7 @@
#include <bdd.h>
#include "misc/optionmap.hh"
#include "tgba/state.hh"
#include "tgba/tgbagraph.hh"
#include "emptiness_stats.hh"
namespace spot
@ -293,7 +294,7 @@ namespace spot
/// states are merged).
///
/// \pre \a run must correspond to an actual run of the automaton \a a.
SPOT_API tgba*
SPOT_API tgba_digraph*
tgba_run_to_tgba(const tgba* a, const tgba_run* run);
/// @}