Commit 6f7f9ef8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

isdet: rewrite using the tgba_digraph interface

* src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh: Rewrite
using the tgba_digraph interface.
* src/tgbatest/ltl2tgba.cc: Adjust call.
parent c85ba787
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -28,66 +28,40 @@ namespace spot
template<bool count>
static
unsigned
count_nondet_states_aux(const const_tgba_ptr& aut)
count_nondet_states_aux(const const_tgba_digraph_ptr& aut)
{
unsigned res = 0;
typedef std::deque<const state*> todo_list;
state_set seen;
todo_list todo;
{
const state* s = aut->get_init_state();
seen.insert(s);
todo.push_back(s);
}
while (!todo.empty())
unsigned nondet_states = 0;
unsigned ns = aut->num_states();
for (unsigned src = 0; src < ns; ++src)
{
const state* src = todo.front();
todo.pop_front();
bool nondeterministic = false;
bdd available = bddtrue;
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
// the loop, because we still have to record the
// destination states.
if (!nondeterministic)
{
bdd label = i->current_condition();
if (!bdd_implies(label, available))
nondeterministic = true;
else
available -= label;
}
const state* dst = i->current_state();
if (seen.insert(dst).second)
todo.push_back(dst);
else
dst->destroy();
}
res += nondeterministic;
if (!count && nondeterministic)
for (auto& t: aut->out(src))
if (!bdd_implies(t.cond, available))
{
++nondet_states;
break;
}
else
{
available -= t.cond;
}
// If we are not counting non-deterministic states, abort as
// soon as possible.
if (!count && nondet_states)
break;
}
for (state_set::const_iterator i = seen.begin(); i != seen.end();)
{
const state* s = *i++;
s->destroy();
}
return res;
return nondet_states;
}
}
unsigned
count_nondet_states(const const_tgba_ptr& aut)
count_nondet_states(const const_tgba_digraph_ptr& aut)
{
return count_nondet_states_aux<true>(aut);
}
bool
is_deterministic(const const_tgba_ptr& aut)
is_deterministic(const const_tgba_digraph_ptr& aut)
{
if (aut->is_deterministic())
return true;
......@@ -95,43 +69,19 @@ namespace spot
}
bool
is_complete(const const_tgba_ptr& aut)
is_complete(const const_tgba_digraph_ptr& aut)
{
state_set seen;
typedef std::deque<const state*> todo_list;
todo_list todo;
bool complete = true;
{
const state* s = aut->get_init_state();
seen.insert(s);
todo.push_back(s);
}
while (!todo.empty())
unsigned ns = aut->num_states();
for (unsigned src = 0; src < ns; ++src)
{
const state* src = todo.front();
todo.pop_front();
bdd available = bddtrue;
for (auto i: aut->succ(src))
{
available -= i->current_condition();
const state* dst = i->current_state();
if (seen.insert(dst).second)
todo.push_back(dst);
else
dst->destroy();
}
for (auto& t: aut->out(src))
available -= t.cond;
if (available != bddfalse)
{
complete = false;
break;
}
}
for (state_set::const_iterator i = seen.begin(); i != seen.end();)
{
const state* s = *i++;
s->destroy();
return false;
}
return complete;
// The empty automaton is not complete since it does not have an
// initial state.
return ns > 0;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_ISDET_HH
# define SPOT_TGBAALGOS_ISDET_HH
# include "tgba/tgba.hh"
# include "tgba/tgbagraph.hh"
namespace spot
{
......@@ -33,7 +33,7 @@ namespace spot
/// but it is more efficient to call is_deterministic() if you do not
/// care about the number of nondeterministic states.
SPOT_API unsigned
count_nondet_states(const const_tgba_ptr& aut);
count_nondet_states(const const_tgba_digraph_ptr& aut);
/// \brief Return true iff \a aut is deterministic.
///
......@@ -41,14 +41,14 @@ namespace spot
/// the automaton is nondeterministic, because it can return before
/// the entire automaton has been explored.
SPOT_API bool
is_deterministic(const const_tgba_ptr& aut);
is_deterministic(const const_tgba_digraph_ptr& aut);
/// \brief Return true iff \a aut is complete.
///
/// An automaton is complete if its translation relation is total,
/// i.e., each state as a successor for any possible configuration.
SPOT_API bool
is_complete(const const_tgba_ptr& aut);
is_complete(const const_tgba_digraph_ptr& aut);
/// @}
}
......
......@@ -1638,7 +1638,7 @@ checked_main(int argc, char** argv)
case 13:
sub_stats_reachable(a).dump(std::cout);
std::cout << "nondeterministic states: "
<< count_nondet_states(a) << std::endl;
<< count_nondet_states(ensure_digraph(a)) << std::endl;
break;
case 14:
if (!wdba_minimization_is_success)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment