Commit 314f51ac authored by martinez's avatar martinez
Browse files

* src/tgbatest/emptchk.test

src/tgbaalgos/tarjan_on_fly.hh,
src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh,
src/tgbaalgos/minimalce.cc: To correct a bug.
parent ad71da00
2004-09-14 Thomas Martinez <martinez@src.lip6.fr>
* src/tgbatest/emptchk.test
src/tgbaalgos/tarjan_on_fly.hh,
src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh,
src/tgbaalgos/minimalce.cc: To correct a bug.
* src/ltltest/reduc.test (FICH): bad file name.
2004-09-13 Thomas Martinez <martinez@src.lip6.fr>
......
......@@ -223,10 +223,321 @@ namespace spot
/////////////////////////////////////////////////////////////////////////////
// minimal_search
///////////////////////////////////////////////////////////////////
///////////////////////////////////////////////////////////////////
minimalce_search::minimalce_search(const tgba_tba_proxy* a,
int opt)
: a(a), x(0),
x_bis(0),
accepted_path_(false)
{
counter_ = 0;
nested_ = my_nested_ = false;
if (opt == nested)
nested_ = true;
if (opt == my_nested)
my_nested_ = true;
Maxsize = 0;
}
minimalce_search::~minimalce_search()
{
hash_type::const_iterator s = h.begin();
while (s != h.end())
{
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
}
if (x)
delete x;
// Release all iterators on the stack.
while (!stack.empty())
{
delete stack.front().second;
stack.pop_front();
}
for (std::list<ce::counter_example*>::iterator i = l_ce.begin();
i != l_ce.end(); ++i)
{
delete *i;
}
}
bool
minimalce_search::push(const state* s, bool m)
{
if ((Maxsize != 0) && // for minimize
(stack.size() + 1 > Maxsize))
return false;
tgba_succ_iterator* i = a->succ_iter(s);
i->first();
hash_type::iterator hi = h.find(s);
if (hi == h.end())
{
magic d = { !m, m, true, stack.size() + 1};
//magic d = { !m, m, true };
h[s] = d;
}
else
{
hi->second.seen_without |= !m;
hi->second.seen_with |= m;
hi->second.seen_path = true; // for nested search
if ((stack.size() + 1) < hi->second.depth) // for minimize
hi->second.depth = stack.size() + 1;
if (hi->first != s)
delete s;
s = hi->first;
}
magic_state ms = { s, m };
stack.push_front(state_iter_pair(ms, i));
return true;
}
bool
minimalce_search::has(const state* s, bool m) const
{
hash_type::const_iterator i = h.find(s);
if (i == h.end())
return false;
if (!m && i->second.seen_without)
return true;
if (m && i->second.seen_with)
return true;
return false;
}
bool
minimalce_search::exist_path(const state* s) const
{
hash_type::const_iterator hi = h.find(s);
if (hi == h.end())
return false;
if (hi->second.seen_with)
return false;
return hi->second.seen_path && hi->second.seen_without;
}
int
minimalce_search::depth_path(const state* s) const
{
int depth = 0;
stack_type::const_reverse_iterator i;
for (i = stack.rbegin(); i != stack.rend(); ++i, ++depth)
if (s->compare(i->first.s) == 0)
break;
if (i != stack.rend())
return depth;
else
return stack.size() + 1;
}
ce::counter_example*
minimalce_search::check()
{
if (my_nested_)
{
accepted_path_ = false;
accepted_depth_ = 0;
}
if (stack.empty())
// It's a new search.
push(a->get_init_state(), false);
else
// Remove the transition to the cycle root.
tstack.pop_front();
assert(stack.size() == 1 + tstack.size());
while (!stack.empty())
{
recurse:
//std::cout << "recurse : "<< stack.size() << std::endl;
minimalce_search::state_iter_pair& p = stack.front();
tgba_succ_iterator* i = p.second;
const bool magic = p.first.m;
while (!i->done())
{
const state* s_prime = i->current_state();
//std::cout << a->format_state(s_prime) << std::endl;
bdd c = i->current_condition();
i->next();
if ((magic && 0 == s_prime->compare(x)) ||
(magic && (nested_ || my_nested_) && exist_path(s_prime)) ||
(!magic && my_nested_ && accepted_path_ &&
exist_path(s_prime) && depth_path(s_prime) <= accepted_path_))
{
if (nested_ || my_nested)
{
if (x)
delete x;
x = s_prime->clone();
}
delete s_prime;
tstack.push_front(c);
assert(stack.size() == tstack.size());
build_counter();
Maxsize = stack.size();
counter_->build_cycle(x);
return counter_;
}
if (!has(s_prime, magic))
{
if (my_nested_ && a->state_is_accepting(s_prime))
{
accepted_path_ = true;
accepted_depth_ = stack.size();
}
if (push(s_prime, magic))
{
tstack.push_front(c);
goto recurse;
}
// for minimize
}
delete s_prime;
}
const state* s = p.first.s;
delete i;
if (nested_ || my_nested_)
{
hash_type::iterator hi = h.find(((stack.front()).first).s);
assert (hi != h.end());
hi->second.seen_path = false;
}
stack.pop_front();
if (!magic && a->state_is_accepting(s))
{
if (!has(s, true))
{
if (x)
delete x;
x = s->clone();
push(s, true);
continue;
}
}
if (!stack.empty())
tstack.pop_front();
}
std::cout << "END CHECK" << std::endl;
assert(tstack.empty());
return 0;
}
std::ostream&
minimalce_search::print_result(std::ostream& os, const tgba* restrict) const
{
stack_type::const_reverse_iterator i;
tstack_type::const_reverse_iterator ti;
os << "Prefix:" << std::endl;
const bdd_dict* d = a->get_dict();
for (i = stack.rbegin(), ti = tstack.rbegin();
i != stack.rend(); ++i, ++ti)
{
if (i->first.s->compare(x) == 0)
os <<"Cycle:" <<std::endl;
const state* s = i->first.s;
if (restrict)
{
s = a->project_state(s, restrict);
assert(s);
os << " " << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << " " << a->format_state(s) << std::endl;
}
os << " | " << bdd_format_set(d, *ti) << std::endl;
}
if (restrict)
{
const state* s = a->project_state(x, restrict);
assert(s);
os << " " << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << " " << a->format_state(x) << std::endl;
}
return os;
}
std::ostream&
minimalce_search::print_stat(std::ostream& os) const
{
int ce_size = 0;
if (counter_)
ce_size = counter_->size();
os << "Size of Counter Example : " << ce_size << std::endl
<< "States explored : " << h.size() << std::endl;
return os;
}
void
minimalce_search::build_counter()
{
if (counter_)
l_ce.push_front(counter_);
assert(stack.size() == tstack.size());
counter_ = new ce::counter_example(a);
stack_type::reverse_iterator i;
tstack_type::reverse_iterator ti;
for (i = stack.rbegin(), ti = tstack.rbegin();
i != stack.rend(); ++i, ++ti)
{
if (i->first.s->compare(x) == 0)
break;
ce::state_ce ce;
ce = ce::state_ce(i->first.s->clone(), *ti);
counter_->prefix.push_back(ce);
}
for (; i != stack.rend(); ++i, ++ti)
{
ce::state_ce ce;
ce = ce::state_ce(i->first.s->clone(), *ti);
counter_->cycle.push_back(ce);
}
//counter_->build_cycle(x);
}
///////////////////////////////////////////////////////////////////
///////////////////////////////////////////////////////////////////
/*
minimalce_search::minimalce_search(const tgba_tba_proxy *a,
bool mode)
: a(a), min_ce(0)
: a(a), min_ce(0),
x(0),
x_bis(0),
accepted_path_(false)
{
Maxsize = 0;
nested_ = my_nested_ = false;
mode_ = mode;
}
......@@ -245,13 +556,13 @@ namespace spot
i != l_ce.end();)
{
//std::cout << "delete a counter" << std::endl;
/*
if (*i == min_ce)
{
++i;
continue;
}
*/
//if (*i == min_ce)
//{
//++i;
//continue;
//}
ce::counter_example* ce = *i;
++i;
delete ce;
......@@ -345,10 +656,9 @@ namespace spot
{
recurse:
//std::cout << "recurse: " << a->format_state(s) << std::endl;
/*
if (iter)
delete iter;
*/
// if (iter)
// delete iter;
iter = stack.front().second;
while (!iter->done())
......@@ -495,10 +805,9 @@ namespace spot
std::ostringstream& os,
int mode)
{
/*
std::cout << os.str() << "recurse find : "
<< a->format_state(s) << std::endl;
*/
// std::cout << os.str() << "recurse find : "
// << a->format_state(s) << std::endl;
hash_type::iterator i = h_lenght.find(s);
if (i != h_lenght.end())
......@@ -606,18 +915,7 @@ namespace spot
break;
}
/*
if (depth <= last_depth)
std::cout << " : true => depth : "
<< depth << ", last_depth"
<< last_depth << std::endl;
else
std::cout << " : false => depth : "
<< depth << ", last_depth : "
<< last_depth << std::endl;
*/
return depth <= last_depth; // May be '<='
return depth <= last_depth;
}
int
......@@ -639,16 +937,6 @@ namespace spot
if (!return_value)
depth = -1;
/*
if (return_value)
std::cout << " : true" << std::endl;
else
{
depth = -1;
std::cout << " : false" << std::endl;
}
*/
return depth;
}
......@@ -713,5 +1001,6 @@ namespace spot
min_prefix = *i;
return min_prefix;
}
*/
}
......@@ -36,6 +36,13 @@
namespace spot
{
enum search_opt
{
magic = 0,
nested = 1,
my_nested = 2
};
namespace ce
{
......@@ -89,7 +96,8 @@ namespace spot
class minimalce_search: public emptyness_search
{
public:
minimalce_search(const tgba_tba_proxy *a, bool mode = false);
//minimalce_search(const tgba_tba_proxy *a, bool mode = false);
minimalce_search(const tgba_tba_proxy *a, int opt = nested);
virtual ~minimalce_search();
......@@ -97,18 +105,35 @@ namespace spot
virtual ce::counter_example* check();
/// \brief Find a counter example shorter than \a min_ce.
ce::counter_example* check(ce::counter_example* min_ce);
//ce::counter_example* check(ce::counter_example* min_ce);
ce::counter_example* find();
//ce::counter_example* find();
/// \brief Print Stat.
std::ostream& print_stat(std::ostream& os) const;
std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const;
ce::counter_example* get_minimal_cyle() const;
ce::counter_example* get_minimal_prefix() const;
//ce::counter_example* get_minimal_cyle() const;
//ce::counter_example* get_minimal_prefix() const;
private:
/// \brief Minimisation is implemented on the magic search algorithm.
struct magic
{
bool seen_without : 1;
bool seen_with : 1;
bool seen_path : 1;
unsigned int depth;
};
struct magic_state
{
const state* s;
bool m;
};
enum search_mode
{
normal = 0,
......@@ -116,6 +141,52 @@ namespace spot
};
//int mode;
typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
typedef std::list<state_iter_pair> stack_type;
stack_type stack; ///< Stack of visited states on the path.
typedef std::list<bdd> tstack_type;
/// \brief Stack of transitions.
///
/// This is an addition to the data from the paper.
tstack_type tstack;
typedef Sgi::hash_map<const state*, magic,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// Append a new state to the current path.
bool push(const state* s, bool m);
/// Check whether we already visited \a s with the Magic bit set to \a m.
bool has(const state* s, bool m) const;
/// Check if \a s is in the path.
bool exist_path(const state* s) const;
/// Return the depth of the state \a s in stack.
int depth_path(const state* s) const;
void build_counter();
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
const state* x;
/// \brief Active the nested search which produce a
/// smaller counter example.
bool nested_;
/// \brief Active the nested bis search which produce a
/// smaller counter example.
const state* x_bis;
bool my_nested_;
bool accepted_path_;
int accepted_depth_;
unsigned int Maxsize;
ce::counter_example* counter_;
std::list<ce::counter_example*> l_ce;
///////////////////////////////////////////////////////////////////
/*
//typedef std::pair<int, tgba_succ_iterator*> state_iter_pair;
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
......@@ -158,6 +229,7 @@ namespace spot
/// Save the current path in stack as a counter example.
/// this counter example is the minimal that we have found yet.
void save_counter(const state* s, std::ostringstream& os);
*/
};
}
......
......@@ -76,7 +76,7 @@ namespace spot
if (hi == h.end())
{
//magic d = { !m, m, true, stack.size() + 1};
magic d = { !m, m, true, };
magic d = { !m, m, true };
h[s] = d;
}
else
......
......@@ -32,12 +32,14 @@
namespace spot
{
/*
enum search_opt
{
magic = 0,
nested = 1,
my_nested = 2
};
*/
class nesteddfs_search: public emptyness_search
{
......
......@@ -36,10 +36,21 @@ namespace spot
i != stack.end(); ++i)
{
//if ((*i).s)
hash_type::iterator hi = h.find(i->s);
if (hi != h.end())
h.erase(hi);
delete (*i).s;
//if ((*i).lasttr)
delete (*i).lasttr;
}
for (hash_type::iterator i = h.begin();
i != h.end();)
{
const state *s = i->first;
++i;
delete s;
}
}
ce::counter_example*
......@@ -98,10 +109,10 @@ namespace spot
void
tarjan_on_fly::push(const state* s)
{
h[s] = 1;
h[s] = top;
top++;
struct_state ss = { s, 0, top, dftop, 0, 0 };
struct_state ss = { s, 0, top, dftop, 0 };
if (a->state_is_accepting(s))
{
......@@ -117,7 +128,12 @@ namespace spot
{
const state* sdel = stack[top].s;
tgba_succ_iterator* iter = stack[top].lasttr;
delete sdel;
if (h.find(sdel) == h.end())
{
assert(0);
delete sdel;
}
if (iter)
delete iter;
......@@ -135,6 +151,12 @@ namespace spot