Commit 5af687b2 authored by martinez's avatar martinez
Browse files

* src/tgbatest/spotlbtt.test,

src/tgbatest/reductgba.cc,
src/tgbatest/ltl2tgba.cc:
Add option for reduction of TGBA.

* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
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,
src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
Remove some bugs.

src/tgbaalgos/gtec/ce.cc:
Modification of construction of counter example.

* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim_del.cc,
src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
Modification for delayed simulation.


* src/tgbaalgos/gtec/ce.hh,
* src/tgbatest/ltl2tgba.cc,
parent 2d1151e0
2004-09-13 Thomas Martinez <martinez@src.lip6.fr>
* src/tgbatest/spotlbtt.test,
src/tgbatest/reductgba.cc,
src/tgbatest/ltl2tgba.cc:
Add option for reduction of TGBA.
* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
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,
src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
Remove some bugs.
src/tgbaalgos/gtec/ce.cc:
Modification of construction of counter example.
* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim_del.cc,
src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
Modification for delayed simulation.
2004-08-23 Thomas Martinez <martinez@src.lip6.fr>
* src/tgbaalgos/tarjan_on_fly.hh,
......@@ -9,11 +32,11 @@
src/tgbaalgos/colordfs.hh,
src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check.
src/tgbaalgos/gtec/ce.hh,
* src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
object in minimalce.hh.
src/tgbatest/ltl2tgba.cc,
* src/tgbatest/ltl2tgba.cc,
src/tgbatest/emptchk.test,
src/tgbaalgos/Makefile.am: Add files for emptyness-check.
......
......@@ -22,11 +22,12 @@
# Check for the reduc visitor.
. ./defs || exit 1
# . ./defs || exit 1
set -e
FICH=${1-$srcdir/formulae.txt}
#FICH=${1-$srcdir/formulae.txt}
FICH=${1-$srcdir/formules3.ltl}
for opt in 0 1 2 3; do
rm -f result.data
......
......@@ -35,7 +35,7 @@ namespace spot
tgba_reachable_iterator_breadth_first(a),
h_(nshf->build())
{
dict_->register_all_variables_of(a, this); // useful ??
dict_->register_all_variables_of(a, this);
run();
all_acceptance_conditions_ = a->all_acceptance_conditions();
......@@ -57,12 +57,12 @@ namespace spot
}
void
tgba_reduc::prune_automata(simulation_relation* rel)
tgba_reduc::quotient_state(direct_simulation_relation* rel)
{
// Remember that for each state couple (*i)->second
// simulate (*i)->first.
// Remember that for each state couple
// (*i)->second simulate (*i)->first.
for (simulation_relation::iterator i = rel->begin();
for (direct_simulation_relation::iterator i = rel->begin();
i != rel->end(); ++i)
{
......@@ -72,28 +72,29 @@ namespace spot
// We check if the two state are co-simulate.
bool recip = false;
for (spot::simulation_relation::iterator j = i;
for (direct_simulation_relation::iterator j = i;
j != rel->end(); ++j)
if ((((*i)->first)->compare((*j)->second) == 0) &&
(((*j)->first)->compare((*i)->second) == 0))
recip = true;
if (!recip)
this->redirect_transition((*i)->first, (*i)->second);
else
this->merge_state((*i)->first, (*i)->second);
if (recip)
//this->redirect_transition((*i)->first, (*i)->second);
this->merge_state((*i)->first, (*i)->second);
}
this->merge_transitions();
}
void
tgba_reduc::quotient_state(simulation_relation* rel)
tgba_reduc::quotient_state(delayed_simulation_relation* rel)
{
// Remember that for each state couple (*i)->second
// simulate (*i)->first.
if (nb_set_acc_cond() > 1)
return;
for (simulation_relation::iterator i = rel->begin();
//this->quotient_state(rel);
for (delayed_simulation_relation::iterator i = rel->begin();
i != rel->end(); ++i)
{
......@@ -103,7 +104,7 @@ namespace spot
// We check if the two state are co-simulate.
bool recip = false;
for (spot::simulation_relation::iterator j = i;
for (delayed_simulation_relation::iterator j = i;
j != rel->end(); ++j)
if ((((*i)->first)->compare((*j)->second) == 0) &&
(((*j)->first)->compare((*i)->second) == 0))
......@@ -116,6 +117,19 @@ namespace spot
this->merge_transitions();
}
void
tgba_reduc::delete_transitions(simulation_relation* rel)
{
for (simulation_relation::iterator i = rel->begin();
i != rel->end(); ++i)
{
if (((*i)->first)->compare((*i)->second) == 0)
continue;
this->redirect_transition((*i)->first, (*i)->second);
}
this->merge_transitions();
}
void
tgba_reduc::prune_scc()
{
......@@ -146,6 +160,7 @@ namespace spot
}
////////////////////////////////////////////
// for build tgba_reduc
void
tgba_reduc::start()
......@@ -430,10 +445,12 @@ namespace spot
tgba_reduc::merge_state_delayed(const spot::state*,
const spot::state*)
{
// TO DO
}
/////////////////////////////////////////
/////////////////////////////////////////
// Compute SCC
// From gtec.cc
void
......@@ -604,24 +621,24 @@ namespace spot
i != s1->end(); ++i)
(*i)->acceptance_conditions = bddfalse;
}
else
/*
else
{
// FIXME
/*
tgba_succ_iterator* si = this->succ_iter(sm->first);
spot::state* s2 = si->current_state();
seen_map::iterator sm2 = si_.find(s2);
if (sm2->second == n)
{
s1 = name_state_map_[tgba_explicit::format_state(sm2->first)];
for (state::iterator i = s1->begin();
i != s1->end(); ++i)
(*i)->acceptance_conditions = bddfalse;
}
delete s2;
delete si;
*/
// FIXME
tgba_succ_iterator* si = this->succ_iter(sm->first);
spot::state* s2 = si->current_state();
seen_map::iterator sm2 = si_.find(s2);
if (sm2->second == n)
{
s1 = name_state_map_[tgba_explicit::format_state(sm2->first)];
for (state::iterator i = s1->begin();
i != s1->end(); ++i)
(*i)->acceptance_conditions = bddfalse;
}
delete s2;
delete si;
}
*/
}
}
......@@ -825,6 +842,7 @@ namespace spot
}
/*
void
tgba_reduc::remove_scc_depth_first(spot::state* s, int n)
{
......@@ -853,7 +871,9 @@ namespace spot
seen_ = 0;
}
}
*/
/*
bool
tgba_reduc::is_alpha_ball(const spot::state* s, bdd label, int n)
{
......@@ -909,6 +929,21 @@ namespace spot
return ret;
}
*/
int
tgba_reduc::nb_set_acc_cond() const
{
bdd acc, all;
acc = all = this->all_acceptance_conditions();
int count = 0;
while (all != bddfalse)
{
all -= bdd_satone(all);
count++;
}
return count;
}
//////// JUST FOR DEBUG //////////
......
......@@ -34,6 +34,15 @@ namespace spot
typedef Sgi::pair<const spot::state*, const spot::state*> state_couple;
typedef Sgi::vector<state_couple*> simulation_relation;
/*
typedef Sgi::vector<state_couple*> direct_simulation_relation;
typedef Sgi::vector<state_couple*> delayed_simulation_relation;
*/
class direct_simulation_relation : public simulation_relation{};
class delayed_simulation_relation : public simulation_relation{};
class tgba_reduc: public tgba_explicit,
public tgba_reachable_iterator_breadth_first
{
......@@ -46,11 +55,15 @@ namespace spot
/// Reduce the automata using a relation simulation
/// Do not call this method with a delayed simulation relation.
void prune_automata(simulation_relation* rel);
void quotient_state(direct_simulation_relation* rel);
/// Build the quotient automata. Call this method
/// when use to a delayed simulation relation.
void quotient_state(simulation_relation* rel);
void quotient_state(delayed_simulation_relation* rel);
/// \brief Delete some transitions with help of a simulation
/// relation.
void delete_transitions(simulation_relation* rel);
/// Remove all state which not lead to an accepting cycle.
void prune_scc();
......@@ -144,9 +157,9 @@ namespace spot
/// publisher = {Springer-Verlag}
/// }
/// \endverbatim
bool is_alpha_ball(const spot::state* s,
bdd label = bddfalse,
int n = -1);
// bool is_alpha_ball(const spot::state* s,
// bdd label = bddfalse,
// int n = -1);
// Return true if we can't reach a state with
// an other value of scc.
......@@ -165,11 +178,13 @@ namespace spot
void remove_scc(spot::state* s);
/// Same as remove_scc but more efficient.
void remove_scc_depth_first(spot::state* s, int n = -1);
// void remove_scc_depth_first(spot::state* s, int n = -1);
/// For compute_scc.
void remove_component(const spot::state* from);
int tgba_reduc::nb_set_acc_cond() const;
};
}
......
......@@ -36,6 +36,7 @@ tgbaalgos_HEADERS = \
magic.hh \
minimalce.hh \
nesteddfs.hh \
nesteddfsgen.hh \
neverclaim.hh \
powerset.hh \
reachiter.hh \
......@@ -55,6 +56,7 @@ libtgbaalgos_la_SOURCES = \
magic.cc \
minimalce.cc \
nesteddfs.cc \
nesteddfsgen.cc \
neverclaim.cc \
powerset.cc \
reachiter.cc \
......
......@@ -30,6 +30,7 @@ namespace spot
colordfs_search::colordfs_search(const tgba_tba_proxy* a)
: a(a), x(0), counter_(0)
{
Maxdepth = -1;
}
colordfs_search::~colordfs_search()
......@@ -111,9 +112,7 @@ namespace spot
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
//std::cout << "iter : " << n << std::endl;
s2 = i->current_state();
//std::cout << a->format_state(s2) << std::endl;
hi = h.find(s2);
if (hi != h.end())
return_value &= (hi->second.c == black);
......@@ -123,8 +122,6 @@ namespace spot
}
delete i;
//std::cout << "End Loop" << std::endl;
hi = h.find(s);
assert(hi != h.end());
if (return_value)
......@@ -138,8 +135,8 @@ namespace spot
{
clock();
counter_ = new ce::counter_example(a);
const state* s = a->get_init_state();
if (dfs_blue(s))
const state *s = a->get_init_state();
if (dfs_blue_min(s))
counter_->build_cycle(x);
else
{
......@@ -154,49 +151,60 @@ namespace spot
bool
colordfs_search::dfs_blue(const state* s, bdd)
{
//std::cout << "dfs_blue : " << a->format_state(s) << std::endl;
if (!push(s, blue))
return false;
std::cout << "dfs_blue : " << std::endl;
hash_type::iterator hi;
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
if (stack.empty())
// It's a new search.
push(a->get_init_state(), blue);
else
tstack.pop_front();
while (!stack.empty())
{
const state* s2 = i->current_state();
//std::cout << "s2 : " << a->format_state(s2) << std::endl;
hi = h.find(s2);
if (a->state_is_accepting(s2) &&
(hi != h.end() && hi->second.is_in_cp))
{
ce::state_ce ce;
ce = ce::state_ce(s2, i->current_condition());
x = const_cast<state*>(s2);
delete i;
return true;// a counter example is found !!
}
else if (hi == h.end() || hi->second.c == white)
recurse:
tgba_succ_iterator *i = stack.front().second;
hash_type::iterator hi;
//std::cout << a->format_state(p.first) << std::endl;
while (!i->done())
{
int res = dfs_blue(s2, i->current_acceptance_conditions());
if (res == 1)
const state* s2 = i->current_state();
hi = h.find(s2);
if (a->state_is_accepting(s2) &&
(hi != h.end() && hi->second.is_in_cp))
{
delete i;
return true;
//ce::state_ce ce;
//ce = ce::state_ce(s2, i->current_condition());
x = const_cast<state*>(s2);
//push(s2, blue); //
//delete i;
return true;// a counter example is found !!
}
else if (hi == h.end() || hi->second.c == white)
{
push(s2, blue);
goto recurse;
}
else
delete s2;
i->next();
}
else
delete s2; // FIXME
}
delete i;
pop();
s = stack.front().first;
pop();
if (!all_succ_black(s) &&
a->state_is_accepting(s))
{
if (dfs_red(s))
return 1;
dfs_black(s);
if (!all_succ_black(s) &&
a->state_is_accepting(s))
{
if (dfs_red(s))
return true;
hash_type::iterator hi = h.find(s);
assert(hi == h.end());
hi->second.c = black;
}
delete s; //
}
return false;
......@@ -205,7 +213,7 @@ namespace spot
bool
colordfs_search::dfs_red(const state* s)
{
//std::cout << "dfs_red : " << a->format_state(s) << std::endl;
std::cout << "dfs_red : " << a->format_state(s) << std::endl;
if (!push(s, red))
return false;
......@@ -240,12 +248,143 @@ namespace spot
}
delete i;
hi = h.find(s);
assert(hi == h.end());
hi->second.c = black;
//std::cout << "dfs_red : pop" << std::endl;
pop();
return false;
}
///////////////////////////////////////////////////////////////////////
// for minimisation
bool
colordfs_search::dfs_blue_min(const state* s, bdd)
{
//std::cout << "dfs_blue : " << a->format_state(s) << std::endl;
if (!push(s, blue))
return false;
hash_type::iterator hi = h.find(s);
if (hi != h.end())
{
if (((int)stack.size() + 1) < hi->second.depth)
hi->second.depth = stack.size(); // for minimize
}
else
{
assert(0);
}
if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth))
{
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
const state* s2 = i->current_state();
//std::cout << "s2 : " << a->format_state(s2) << std::endl;
hi = h.find(s2);
if (a->state_is_accepting(s2) &&
(hi != h.end() && hi->second.is_in_cp))
{
Maxdepth = stack.size();
ce::state_ce ce;
ce = ce::state_ce(s2, i->current_condition());
x = const_cast<state*>(s2);
delete i;
return true;// a counter example is found !!
}
else if (hi == h.end() || hi->second.c == white)
{
int res = dfs_blue_min(s2, i->current_acceptance_conditions());
if (res == 1)
{
delete i;
return true;
}
}
else
delete s2; // FIXME
}
delete i;
pop();
if (!all_succ_black(s) &&
a->state_is_accepting(s))
{
if (dfs_red_min(s))
return 1;
dfs_black(s);
}
}
return false;
}
bool
colordfs_search::dfs_red_min(const state* s)
{
//std::cout << "dfs_red : " << a->format_state(s) << std::endl;
if (!push(s, red))
return false;
hash_type::iterator hi = h.find(s);
if (hi != h.end())
{
if (((int)stack.size() + 1) < hi->second.depth)
hi->second.depth = stack.size(); // for minimize
}
else
assert(0);
if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth))
{
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
const state* s2 = i->current_state();
hi = h.find(s2);
if (hi != h.end() && hi->second.is_in_cp &&
(a->state_is_accepting(s2) ||
(hi->second.c == blue)))
{
Maxdepth = stack.size();
ce::state_ce ce;
ce = ce::state_ce(s2->clone(), i->current_condition());
x = const_cast<state*>(s2);
delete i;
return true;// a counter example is found !!
}
if (hi != h.end() &&
(hi->second.c == blue))
// || ((int)stack.size() + 1) < hi->second.depth))
{
delete s2; // FIXME
if (dfs_red_min(hi->first))
{
delete i;
return true;
}
}
else
delete s2;
}
delete i;
//std::cout << "dfs_red : pop" << std::endl;
pop();
}
return false;
}
void
colordfs_search::dfs_black(const state* s)
{
......
......@@ -97,6 +97,8 @@ namespace spot
/// Pages = "92-108")
bool dfs_blue(const state* s, bdd acc = bddfalse);
bool dfs_red(const state* s);
bool dfs_blue_min(const state* s, bdd acc = bddfalse);
bool dfs_red_min(const state* s);
void dfs_black(const state* s);
/// Append a new state to the current path.
......@@ -110,6 +112,7 @@ namespace spot
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
const state* x;
int Maxdepth; ///< The size of the current counter example.
ce::counter_example* counter_;
clock_t tps_;
......
......@@ -35,7 +35,10 @@ namespace spot
eccf)