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

* src/tgbatest/spotlbtt.test: We don't check the post-reduction

Browse source 
with scc and delayed simulation.

* src/tgbatest/ltl2tgba.cc: Adjust parameters.
* src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
* src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
Remove some useless comments.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.

* src/ltlvisit/reducform.cc: Correct some bug for multop.
* src/ltltest/reduccmp.test: More Test.
* src/ltltest/reduc.cc: Thinko
* src/ltltest/equals.cc: Reduction compare
This commit is contained in:
martinez 2004-06-17 16:27:36 +00:00
parent 84e72c8764
commit c769f74750
16 changed files with 429 additions and 250 deletions
Download patch file Download diff file Expand all files Collapse all files

17
ChangeLog
View file

@ -1,3 +1,20 @@
2004-06-17 Thomas Martinez <martinez@src.lip6.fr>
* src/tgbatest/spotlbtt.test: We don't check the post-reduction
with scc and delayed simulation.
* src/tgbatest/ltl2tgba.cc: Adjust parameters.
* src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
* src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
Remove some useless comments.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.
* src/ltlvisit/reducform.cc: Correct some bug for multop.
* src/ltltest/reduccmp.test: More Test.
* src/ltltest/reduc.cc: Thinko
* src/ltltest/equals.cc: Reduction compare
2004-06-17 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-06-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s. * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s.

3
src/ltltest/equals.cc
View file

@ -84,11 +84,8 @@ main(int argc, char** argv)
spot::ltl::formula* tmp; spot::ltl::formula* tmp;
tmp = f1; tmp = f1;
f1 = spot::ltl::reduce(f1); f1 = spot::ltl::reduce(f1);
//std::string f2s = spot::ltl::to_string(f2);
//std::string f1s = spot::ltl::to_string(f1);
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
spot::ltl::dump(std::cout, f1); spot::ltl::dump(std::cout, f1);
//std::cout << f1s << " // " << f2s << std::endl;
#endif #endif
int exit_code = f1 != f2; int exit_code = f1 != f2;

3
src/ltltest/reduc.cc
View file

@ -179,6 +179,5 @@ main(int argc, char** argv)
assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0);
//return exit_code; return exit_code;
return 0;
} }

37
src/ltltest/reduccmp.test
View file

@ -25,6 +25,38 @@
. ./defs || exit 1 . ./defs || exit 1
# No reduction
run 0 ./reduccmp 'a U b' 'a U b'
run 0 ./reduccmp 'a R b' 'a R b'
run 0 ./reduccmp 'a & b' 'a & b'
run 0 ./reduccmp 'a | b' 'a | b'
run 0 ./reduccmp 'a & (a U b)' 'a & (a U b)'
run 0 ./reduccmp 'a | (a U b)' 'a | (a U b)'
# Syntactic reduction
run 0 ./reduccmp 'a & (!b R !a)' 'false'
run 0 ./reduccmp '(!b R !a) & a' 'false'
run 0 ./reduccmp '(!b R !a) | a' 'true'
run 0 ./reduccmp 'a | (!b R !a)' 'true'
run 0 ./reduccmp 'a & (!b R !a) & c' 'false'
run 0 ./reduccmp 'c & (!b R !a) & a' 'false'
run 0 ./reduccmp 'a | (!b R !a) | c' 'true'
run 0 ./reduccmp 'c | (!b R !a) | a' 'true'
run 0 ./reduccmp 'a & (b U a)' 'a'
run 0 ./reduccmp '(b U a) & a' 'a'
run 0 ./reduccmp 'a | (b U a)' '(b U a)'
run 0 ./reduccmp '(b U a) | a' '(b U a)'
run 0 ./reduccmp 'a U (b U a)' '(b U a)'
run 0 ./reduccmp 'a & (b U a) & a' 'a'
run 0 ./reduccmp 'a & (b U a) & a' 'a'
run 0 ./reduccmp 'a | (b U a) | a' '(b U a)'
run 0 ./reduccmp 'a | (b U a) | a' '(b U a)'
run 0 ./reduccmp 'a U (b U a)' '(b U a)'
# Basics reduction # Basics reduction
run 0 ./reduccmp 'X(true)' 'true' run 0 ./reduccmp 'X(true)' 'true'
run 0 ./reduccmp 'X(false)' 'false' run 0 ./reduccmp 'X(false)' 'false'
@ -67,8 +99,3 @@ run 0 ./reduccmp 'Ga' 'Ga'
run 0 ./reduccmp 'GFGa' 'FGa' run 0 ./reduccmp 'GFGa' 'FGa'
run 0 ./reduccmp 'b R Ga' 'Ga' run 0 ./reduccmp 'b R Ga' 'Ga'
run 0 ./reduccmp 'b R FGa' 'FGa' run 0 ./reduccmp 'b R FGa' 'FGa'
# Syntactic reduction
run 0 ./reduccmp 'a & (b U a)' 'a'
run 0 ./reduccmp 'a | (b U a)' '(b U a)'
run 0 ./reduccmp 'a U (b U a)' '(b U a)'

33
src/ltltest/syntimpl.test
View file

@ -33,21 +33,6 @@ run 1 ./syntimpl 0 '(e R f)' '(g U f)'
run 1 ./syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))' run 1 ./syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
run 1 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)' run 1 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
run 0 ./syntimpl 0 'Xa' 'XX(b U a)'
run 0 ./syntimpl 0 'XXa' 'X(b U a)'
run 0 ./syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
run 0 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
run 0 ./syntimpl 0 'a' 'b'
run 0 ./syntimpl 0 'a' 'b + c'
run 0 ./syntimpl 0 'a + b' 'a'
run 0 ./syntimpl 0 'a' 'a * c'
run 0 ./syntimpl 0 'a * b' 'c'
run 0 ./syntimpl 0 'a' 'a U b'
run 0 ./syntimpl 0 'a' 'a R b'
run 0 ./syntimpl 0 'a R b' 'a'
run 1 ./syntimpl 0 '1' '1' run 1 ./syntimpl 0 '1' '1'
run 1 ./syntimpl 0 '0' '0' run 1 ./syntimpl 0 '0' '0'
@ -81,3 +66,21 @@ run 1 ./syntimpl 0 'a R b' '1 R b'
run 1 ./syntimpl 0 'b * (a U b)' 'a U b' run 1 ./syntimpl 0 'b * (a U b)' 'a U b'
run 1 ./syntimpl 0 'a U b' 'c + (a U b)' run 1 ./syntimpl 0 'a U b' 'c + (a U b)'
run 0 ./syntimpl 0 'Xa' 'XX(b U a)'
run 0 ./syntimpl 0 'XXa' 'X(b U a)'
run 0 ./syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
run 0 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
run 0 ./syntimpl 0 'a' 'b'
run 0 ./syntimpl 0 'a' 'b + c'
run 0 ./syntimpl 0 'a + b' 'a'
run 0 ./syntimpl 0 'a' 'a * c'
run 0 ./syntimpl 0 'a * b' 'c'
run 0 ./syntimpl 0 'a' 'a U b'
run 0 ./syntimpl 0 'a' 'a R b'
run 0 ./syntimpl 0 'a R b' 'a'
run 0 ./syntimpl 0 'p2' 'p3 || G(p2 && p5)'
run 0 ./syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'

98
src/ltlvisit/reducform.cc
View file

@ -201,81 +201,71 @@ namespace spot
if (opt_ & Reduce_Syntactic_Implications) if (opt_ & Reduce_Syntactic_Implications)
{ {
formula* f1;
formula* f2;
multop::vec::iterator index = res->begin();
multop::vec::iterator indextmp = index;
switch (mo->op())
{
case multop::Or:
if (index != res->end())
break;
f1 = *index++;
for (; index != res->end(); index++)
{
f2 = *index;
/* a < b => a + b = b */
if (syntactic_implication(f1, f2)) // f1 < f2
{
f1 = f2;
destroy(*indextmp);
res->erase(indextmp);
indextmp = index;
index--;
}
else if (syntactic_implication(f2, f1)) // f2 < f1
{
destroy(*index);
res->erase(index);
index--;
}
}
break;
case multop::And: bool removed = true;;
if (index != res->end()) multop::vec::iterator f1;
multop::vec::iterator f2;
while (removed)
{
removed = false;
f2 = f1 = res->begin();
++f1;
while (f1 != res->end())
{
assert(f1 != f2);
// a < b => a + b = b
// a < b => a & b = a
if ((syntactic_implication(*f1, *f2) && // f1 < f2
(mo->op() == multop::Or)) ||
((syntactic_implication(*f2, *f1)) && // f2 < f1
(mo->op() == multop::And)))
{
// We keep f2
destroy(*f1);
res->erase(f1);
removed = true;
break; break;
f1 = *index++;
for (; index != res->end(); index++)
{
f2 = *index;
/* a < b => a & b = a */
if (syntactic_implication(f1, f2)) // f1 < f2
{
destroy(*index);
res->erase(index);
index--;
} }
else if (syntactic_implication(f2, f1)) // f2 < f1 else if ((syntactic_implication(*f2, *f1) && // f2 < f1
(mo->op() == multop::Or)) ||
((syntactic_implication(*f1,* f2)) && // f1 < f2
(mo->op() == multop::And)))
{ {
f1 = f2; // We keep f1
destroy(*indextmp); destroy(*f2);
res->erase(indextmp); res->erase(f2);
indextmp = index; removed = true;
index--;
}
}
break; break;
} }
else
++f1;
}
}
// FIXME
/* f1 < !f2 => f1 & f2 = false /* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */ !f1 < f2 => f1 | f2 = true */
for (index = res->begin(); index != res->end(); index++) for (f1 = res->begin(); f1 != res->end(); f1++)
for (indextmp = res->begin(); indextmp != res->end(); indextmp++) for (f2 = res->begin(); f2 != res->end(); f2++)
if (index != indextmp if (f1 != f2 &&
&& syntactic_implication_neg(*index, *indextmp, syntactic_implication_neg(*f1, *f2,
mo->op() != multop::Or)) mo->op() != multop::Or))
{ {
for (multop::vec::iterator j = res->begin(); for (multop::vec::iterator j = res->begin();
j != res->end(); j++) j != res->end(); j++)
destroy(*j); destroy(*j);
res->clear();
delete res;
if (mo->op() == multop::Or) if (mo->op() == multop::Or)
result_ = constant::true_instance(); result_ = constant::true_instance();
else else
result_ = constant::false_instance(); result_ = constant::false_instance();
return; return;
} }
} }
if (res->size()) if (res->size())
{ {
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);

179
src/tgba/tgbareduc.cc
View file

@ -131,16 +131,14 @@ namespace spot
const state_explicit* se = dynamic_cast<const state_explicit*>(s); const state_explicit* se = dynamic_cast<const state_explicit*>(s);
assert(se); assert(se);
sn_map::const_iterator i = state_name_map_.find(se->get_state()); sn_map::const_iterator i = state_name_map_.find(se->get_state());
//seen_map::const_iterator j = si_.find(s); seen_map::const_iterator j = si_.find(s);
assert(i != state_name_map_.end()); assert(i != state_name_map_.end());
/*
if (j != si_.end()) // SCC have been computed if (j != si_.end()) // SCC have been computed
{ {
os << ", SCC " << j->second; os << ", SCC " << j->second;
return i->second + std::string(os.str()); return i->second + std::string(os.str());
} }
else else
*/
return i->second; return i->second;
} }
@ -244,8 +242,10 @@ namespace spot
bdd cond_simul; bdd cond_simul;
bdd acc_simul; bdd acc_simul;
std::list<state*> ltmp; std::list<state*> ltmp;
const tgba_explicit::state* s1 = name_state_map_[this->format_state(s)]; const tgba_explicit::state* s1 =
const tgba_explicit::state* s2 = name_state_map_[this->format_state(simul)]; name_state_map_[tgba_explicit::format_state(s)];
const tgba_explicit::state* s2 =
name_state_map_[tgba_explicit::format_state(simul)];
sp_map::iterator i = state_predecessor_map_.find(s1); sp_map::iterator i = state_predecessor_map_.find(s1);
if (i == state_predecessor_map_.end()) // 0 predecessor if (i == state_predecessor_map_.end()) // 0 predecessor
@ -325,11 +325,13 @@ namespace spot
// But it can be have some predecessor in state_predecessor_map_ !! // But it can be have some predecessor in state_predecessor_map_ !!
// So, we remove from it. // So, we remove from it.
ns_map::iterator k = name_state_map_.find(format_state(s)); ns_map::iterator k =
name_state_map_.find(tgba_explicit::format_state(s));
if (k == name_state_map_.end()) // 0 predecessor if (k == name_state_map_.end()) // 0 predecessor
return; return;
tgba_explicit::state* st = name_state_map_[format_state(s)]; tgba_explicit::state* st =
name_state_map_[tgba_explicit::format_state(s)];
// for all successor q of s, we remove s of the predecessor of q. // for all successor q of s, we remove s of the predecessor of q.
@ -370,8 +372,10 @@ namespace spot
void void
tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2) tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2)
{ {
const tgba_explicit::state* s1 = name_state_map_[this->format_state(sim1)]; const tgba_explicit::state* s1 =
const tgba_explicit::state* s2 = name_state_map_[this->format_state(sim2)]; name_state_map_[tgba_explicit::format_state(sim1)];
const tgba_explicit::state* s2 =
name_state_map_[tgba_explicit::format_state(sim2)];
const tgba_explicit::state* stmp = s1; const tgba_explicit::state* stmp = s1;
const spot::state* simtmp = sim1; const spot::state* simtmp = sim1;
@ -424,6 +428,7 @@ namespace spot
///////////////////////////////////////// /////////////////////////////////////////
// From gtec.cc
void void
tgba_reduc::remove_component(const spot::state* from) tgba_reduc::remove_component(const spot::state* from)
{ {
@ -459,6 +464,7 @@ namespace spot
} }
} }
// From gtec.cc
void void
tgba_reduc::compute_scc() tgba_reduc::compute_scc()
{ {
@ -558,6 +564,8 @@ namespace spot
void void
tgba_reduc::delete_scc() tgba_reduc::delete_scc()
{ {
std::cout << "delete_scc" << std::endl;
bool change = true; bool change = true;
Sgi::hash_map<int, const spot::state*>::iterator i; Sgi::hash_map<int, const spot::state*>::iterator i;
Sgi::hash_map<int, const spot::state*>::iterator itmp; Sgi::hash_map<int, const spot::state*>::iterator itmp;
@ -570,76 +578,22 @@ namespace spot
change = false; change = false;
for (i = state_scc_v_.begin(); i != state_scc_v_.end();) for (i = state_scc_v_.begin(); i != state_scc_v_.end();)
{ {
//std::cout << "Is terminal ? : " << std::endl; std::cout << "delete_scc : ["
<< this->format_state(i->second)
<< "]"
<< "is_terminal ??" << std::endl;
if (is_terminal(i->second)) if (is_terminal(i->second))
{ {
//std::cout << " YES" << std::endl; //change = true;
change = true; change = false;
this->remove_scc(const_cast<spot::state*>(i->second)); //this->remove_scc(const_cast<spot::state*>(i->second));
itmp = i; itmp = i;
//state_scc_v_.erase(itmp);
}
++i; ++i;
state_scc_v_.erase(itmp);
}
else
{
++i;
//std::cout << " NO "<< std::endl;
} }
} }
} }
}
bool
tgba_reduc::is_alpha_ball(const spot::state* s, int n)
{
/// FIXME
bool b = false;
seen_map::const_iterator i;
if (n == -1)
{
acc_ == bddfalse;
b = true;
assert(seen_ == NULL);
seen_ = new seen_map();
i = si_.find(s);
assert(i->first != NULL);
n = i->second;
}
seen_map::const_iterator sm = seen_->find(s);
if (sm == seen_->end())
{
seen_->insert(std::pair<const spot::state*, int>(s, 1));
i = si_.find(s);
assert(i->first != 0);
if (n != i->second)
return false;
}
else
{
return true;
}
bool ret = true;
tgba_succ_iterator* j = this->succ_iter(s);
for (j->first(); !j->done(); j->next())
{
acc_ |= j->current_acceptance_conditions();
ret &= this->is_terminal(j->current_state(), n);
}
if (b)
{
delete seen_;
seen_ = NULL;
if (acc_ == this->all_acceptance_conditions())
ret = false;
}
return ret;
}
bool bool
tgba_reduc::is_terminal(const spot::state* s, int n) tgba_reduc::is_terminal(const spot::state* s, int n)
@ -650,12 +604,18 @@ namespace spot
// So we can remove it safely without change the // So we can remove it safely without change the
// automaton language. // automaton language.
std::cout << "is_terminal : ["
<< this->format_state(s)
<< "]"
<< std::endl;
bool b = false; bool b = false;
// First call of is_terminal //
seen_map::const_iterator i; seen_map::const_iterator i;
if (n == -1) if (n == -1)
{ {
acc_ == bddfalse; acc_ = bddfalse;
b = true; b = true;
assert(seen_ == NULL); assert(seen_ == NULL);
seen_ = new seen_map(); seen_ = new seen_map();
@ -663,11 +623,13 @@ namespace spot
assert(i->first != NULL); assert(i->first != NULL);
n = i->second; n = i->second;
} }
///////////////////////////////
seen_map::const_iterator sm = seen_->find(s); seen_map::const_iterator sm = seen_->find(s);
if (sm == seen_->end()) if (sm == seen_->end())
{ {
// this state is visited for the first time. // this state is visited for the first time.
std::cout << "first time" << std::endl;
seen_->insert(std::pair<const spot::state*, int>(s, 1)); seen_->insert(std::pair<const spot::state*, int>(s, 1));
i = si_.find(s); i = si_.find(s);
assert(i->first != 0); assert(i->first != 0);
@ -675,19 +637,27 @@ namespace spot
return false; return false;
} }
else else
{
// This state is already visited. // This state is already visited.
{
std::cout << "second time" << std::endl;
return true; return true;
} }
bool ret = true; bool ret = true;
spot::state* s2;
tgba_succ_iterator* j = this->succ_iter(s); tgba_succ_iterator* j = this->succ_iter(s);
int nb_succ = 0;
for (j->first(); !j->done(); j->next()) for (j->first(); !j->done(); j->next())
{ {
std::cout << "successor " << nb_succ++ << std::endl;
s2 = j->current_state();
acc_ |= j->current_acceptance_conditions(); acc_ |= j->current_acceptance_conditions();
ret &= this->is_terminal(j->current_state(), n); ret &= this->is_terminal(s2, n);
delete s2;
} }
delete j;
// First call of is_terminal //
if (b) if (b)
{ {
delete seen_; delete seen_;
@ -695,6 +665,7 @@ namespace spot
if (acc_ == this->all_acceptance_conditions()) if (acc_ == this->all_acceptance_conditions())
ret = false; ret = false;
} }
///////////////////////////////
return ret; return ret;
} }
@ -704,6 +675,8 @@ namespace spot
{ {
// To remove a scc, we remove all his state. // To remove a scc, we remove all his state.
std::cout << "remove_scc" << std::endl;
seen_map::iterator sm = si_.find(s); seen_map::iterator sm = si_.find(s);
sm = si_.find(s); sm = si_.find(s);
int n = sm->second; int n = sm->second;
@ -748,6 +721,62 @@ namespace spot
} }
} }
bool
tgba_reduc::is_alpha_ball(const spot::state* s, bdd label, int n)
{
/// FIXME
// a SCC is alpha ball if she's terminal but with some acceptance
// condition, and all transition have the same label.
// So we replace this SCC by a single state.
bool b = false;
seen_map::const_iterator i;
if ((n == -1) &&
(label == bddfalse))
{
acc_ == bddfalse;
b = true;
assert(seen_ == NULL);
seen_ = new seen_map();
i = si_.find(s);
assert(i->first != NULL);
n = i->second;
}
seen_map::const_iterator sm = seen_->find(s);
if (sm == seen_->end())
{
seen_->insert(std::pair<const spot::state*, int>(s, 1));
i = si_.find(s);
assert(i->first != 0);
if (n != i->second)
return false;
}
else
{
return true;
}
bool ret = true;
tgba_succ_iterator* j = this->succ_iter(s);
for (j->first(); !j->done(); j->next())
{
acc_ |= j->current_acceptance_conditions();
ret &= this->is_terminal(j->current_state(), n);
}
if (b)
{
delete seen_;
seen_ = NULL;
if (acc_ == this->all_acceptance_conditions())
ret = false;
}
return ret;
}
//////// JUST FOR DEBUG ////////// //////// JUST FOR DEBUG //////////
void void

1
src/tgba/tgbareduc.hh
View file

@ -139,6 +139,7 @@ namespace spot
/// } /// }
/// \endverbatim /// \endverbatim
bool is_alpha_ball(const spot::state* s, bool is_alpha_ball(const spot::state* s,
bdd label = bddfalse,
int n = -1); int n = -1);
// Return true if we can't reach a state with // Return true if we can't reach a state with

24
src/tgbaalgos/reductgba_sim.cc
View file

@ -33,7 +33,6 @@ namespace spot
{ {
num_ = num; num_ = num;
sc_ = new state_couple(d_node, s_node); sc_ = new state_couple(d_node, s_node);
//lnode_succ = new Sgi::vector<spoiler_node*>;
lnode_succ = new sn_v; lnode_succ = new sn_v;
lnode_pred = new sn_v; lnode_pred = new sn_v;
this->not_win = false; this->not_win = false;
@ -48,33 +47,48 @@ namespace spot
delete sc_; delete sc_;
} }
void bool
spoiler_node::add_succ(spoiler_node* n) spoiler_node::add_succ(spoiler_node* n)
{ {
/*
bool exist = false;
for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end();)
if (*i == n)
exist = true;
if (exist)
return false;
*/
lnode_succ->push_back(n); lnode_succ->push_back(n);
return true;
} }
void void
spoiler_node::del_succ(spoiler_node* n) spoiler_node::del_succ(spoiler_node* n)
{ {
//std::cout << "del_succ : begin" << std::endl;
for (sn_v::iterator i = lnode_succ->begin(); for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end();) i != lnode_succ->end();)
{ {
if (*i == n) if (*i == n)
{ {
//std::cout << "erase" << std::endl;
i = lnode_succ->erase(i); i = lnode_succ->erase(i);
} }
else else
++i; ++i;
} }
//std::cout << "del_succ : end" << std::endl;
} }
void void
spoiler_node::add_pred(spoiler_node* n) spoiler_node::add_pred(spoiler_node* n)
{ {
/*
bool exist = false;
for (sn_v::iterator i = lnode_pred->begin();
i != lnode_pred->end();)
if (*i == n)
exist = true;
if (!exist)
*/
lnode_pred->push_back(n); lnode_pred->push_back(n);
} }

8
src/tgbaalgos/reductgba_sim.hh
View file

@ -132,7 +132,10 @@ namespace spot
int num); int num);
virtual ~spoiler_node(); virtual ~spoiler_node();
void add_succ(spoiler_node* n); /// \brief Add a successor.
/// Return true if \a n wasn't yet in the list of successor,
/// false eitherwise.
bool add_succ(spoiler_node* n);
void del_succ(spoiler_node* n); void del_succ(spoiler_node* n);
virtual void add_pred(spoiler_node* n); virtual void add_pred(spoiler_node* n);
virtual void del_pred(); virtual void del_pred();
@ -300,7 +303,8 @@ namespace spot
virtual void build_couple(); virtual void build_couple();
virtual void build_link(); virtual void build_link();
void build_recurse_successor_spoiler(spoiler_node* sn); void build_recurse_successor_spoiler(spoiler_node* sn);
void build_recurse_successor_duplicator(duplicator_node* dn); void build_recurse_successor_duplicator(duplicator_node* dn,
spoiler_node* sn);
/// \brief The Jurdzinski's lifting algorithm. /// \brief The Jurdzinski's lifting algorithm.
void lift(); void lift();

65
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -311,7 +311,7 @@ namespace spot
*/ */
} }
/*
void void
parity_game_graph_delayed::build_couple() parity_game_graph_delayed::build_couple()
{ {
@ -512,8 +512,8 @@ namespace spot
} }
} }
} }
*/
/*
// We build only node which are reachable // We build only node which are reachable
void void
parity_game_graph_delayed::build_couple() parity_game_graph_delayed::build_couple()
@ -546,13 +546,15 @@ namespace spot
// We create when it's possible a duplicator node // We create when it's possible a duplicator node
// and recursively his successor. // and recursively his successor.
spot::state* s1 = NULL; //spot::state* s1 = NULL;
bool exist_pred = false; //bool exist_pred = false;
sn_v::iterator i1; sn_v::iterator i1;
for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1) for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1)
{ {
/*
exist_pred = false; exist_pred = false;
// We check if there is a predecessor only if the duplicator // We check if there is a predecessor only if the duplicator
// is the initial state. // is the initial state.
s1 = automata_->get_init_state(); s1 = automata_->get_init_state();
@ -577,6 +579,7 @@ namespace spot
if (!exist_pred) if (!exist_pred)
continue; continue;
*/
// We add a link between a spoiler and a (new) duplicator. // We add a link between a spoiler and a (new) duplicator.
// The acc of the duplicator must contains the // The acc of the duplicator must contains the
@ -590,10 +593,15 @@ namespace spot
void void
parity_game_graph_delayed::build_recurse_successor_spoiler(spoiler_node* sn) parity_game_graph_delayed::build_recurse_successor_spoiler(spoiler_node* sn)
{ {
std::cout << "build_recurse_successor_spoiler" << std::endl;
tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());
int i = 0;
for (si->first(); !si->done(); si->next()) for (si->first(); !si->done(); si->next())
{ {
std::cout << "transition " << i++ << std::endl;
bdd btmp = si->current_acceptance_conditions() | bdd btmp = si->current_acceptance_conditions() |
dynamic_cast<spoiler_node_delayed*>(sn)-> dynamic_cast<spoiler_node_delayed*>(sn)->
get_acceptance_condition_visited(); get_acceptance_condition_visited();
@ -614,10 +622,18 @@ namespace spot
nb_node_parity_game++); nb_node_parity_game++);
duplicator_vertice_.push_back(dn); duplicator_vertice_.push_back(dn);
sn->add_succ(dn); // dn is already a successor of sn.
if (!(sn->add_succ(dn)))
continue;
(dn)->add_pred(sn); (dn)->add_pred(sn);
build_recurse_successor_duplicator(dn); /* TEST
bdd btmp2 =
dynamic_cast<spoiler_node_delayed*>(sn)->
get_acceptance_condition_visited();
*/
build_recurse_successor_duplicator(dn, sn);
} }
delete s; delete s;
} }
@ -629,12 +645,18 @@ namespace spot
void void
parity_game_graph_delayed:: parity_game_graph_delayed::
build_recurse_successor_duplicator(duplicator_node* dn) build_recurse_successor_duplicator(duplicator_node* dn,
spoiler_node* sn)
{ {
tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); std::cout << "build_recurse_successor_duplicator" << std::endl;
tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node());
int i = 0;
for (si->first(); !si->done(); si->next()) for (si->first(); !si->done(); si->next())
{ {
std::cout << "transition " << i++ << std::endl;
bdd btmp = bdd btmp =
dynamic_cast<spoiler_node_delayed*>(sn)-> dynamic_cast<spoiler_node_delayed*>(sn)->
get_acceptance_condition_visited(); get_acceptance_condition_visited();
@ -648,17 +670,19 @@ namespace spot
s = si->current_state(); s = si->current_state();
if (s->compare(*i1) == 0) if (s->compare(*i1) == 0)
{ {
spoiler_node_delayed* sn spoiler_node_delayed* sn_n
= new spoiler_node_delayed(sn->get_spoiler_node(), = new spoiler_node_delayed(sn->get_spoiler_node(),
*i1, *i1,
bddtmp2, btmp2,
nb_node_parity_game++); nb_node_parity_game++);
spoiler_vertice_.push_back(n1); spoiler_vertice_.push_back(sn_n);
sn->add_succ(dn); // dn is already a successor of sn.
(dn)->add_pred(sn); if (!(dn->add_succ(sn_n)))
continue;
(sn_n)->add_pred(dn);
build_recurse_successor_spoiler(sn); build_recurse_successor_spoiler(sn_n);
} }
delete s; delete s;
@ -668,7 +692,7 @@ namespace spot
delete si; delete si;
} }
*/
void void
parity_game_graph_delayed::add_dup_node(state*, parity_game_graph_delayed::add_dup_node(state*,
@ -686,6 +710,7 @@ namespace spot
while (change) while (change)
{ {
std::cout << "prune::change = true" << std::endl;
change = false; change = false;
for (Sgi::vector<duplicator_node*>::iterator i for (Sgi::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
@ -716,7 +741,7 @@ namespace spot
++i; ++i;
} }
} }
std::cout << "prune::change = false" << std::endl;
} }
void void
@ -728,6 +753,7 @@ namespace spot
while (change) while (change)
{ {
std::cout << "lift::change = true" << std::endl;
change = false; change = false;
for (Sgi::vector<duplicator_node*>::iterator i for (Sgi::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
@ -742,7 +768,7 @@ namespace spot
change |= (*i)->set_win(); change |= (*i)->set_win();
} }
} }
std::cout << "lift::change = false" << std::endl;
} }
simulation_relation* simulation_relation*
@ -792,10 +818,15 @@ namespace spot
return; return;
this->build_sub_set_acc_cond(); this->build_sub_set_acc_cond();
*/ */
std::cout << "build couple" << std::endl;
this->build_couple(); this->build_couple();
std::cout << "build link" << std::endl;
this->build_link(); this->build_link();
std::cout << "prune" << std::endl;
this->prune(); this->prune();
std::cout << "lift" << std::endl;
this->lift(); this->lift();
std::cout << "END" << std::endl;
//this->print(std::cout); //this->print(std::cout);
} }

4
src/tgbatest/Makefile.am
View file

@ -39,6 +39,7 @@ check_PROGRAMS = \
powerset \ powerset \
readsave \ readsave \
reductgba \ reductgba \
reduccmp \
tgbaread \ tgbaread \
tripprod tripprod
@ -55,12 +56,15 @@ mixprod_SOURCES = mixprod.cc
powerset_SOURCES = powerset.cc powerset_SOURCES = powerset.cc
readsave_SOURCES = readsave.cc readsave_SOURCES = readsave.cc
reductgba_SOURCES = reductgba.cc reductgba_SOURCES = reductgba.cc
reduccmp_SOURCES = reductgba.cc
reduccmp_CXXFLAGS = -DREDUCCMP
tgbaread_SOURCES = tgbaread.cc tgbaread_SOURCES = tgbaread.cc
tripprod_SOURCES = tripprod.cc tripprod_SOURCES = tripprod.cc
# Keep this sorted by STRENGTH. Test basic things first, # Keep this sorted by STRENGTH. Test basic things first,
# because such failures will be easier to diagnose and fix. # because such failures will be easier to diagnose and fix.
TESTS = \ TESTS = \
reduccmp.test \
reductgba.test \ reductgba.test \
explicit.test \ explicit.test \
tgbaread.test \ tgbaread.test \

28
src/tgbatest/ltl2tgba.cc
View file

@ -88,6 +88,16 @@ syntax(char* prog)
<< " -r4 reduce formula using all rules" << std::endl << " -r4 reduce formula using all rules" << std::endl
<< " -rd display the reduce formula" << std::endl << " -rd display the reduce formula" << std::endl
<< " -R same as -r, but as a set" << std::endl << " -R same as -r, but as a set" << std::endl
<< " -R1 use direct simulation to reduce the automata "
<< "(implies -L)"
<< std::endl
<< " -R2 use delayed simulation to reduce the automata, incorrect"
<< "(implies -L)"
<< std::endl
<< " -R3 use SCC to reduce the automata"
<< std::endl
<< " -Rd to display simulation relation"
<< std::endl
<< " -s convert to explicit automata, and number states " << " -s convert to explicit automata, and number states "
<< "in DFS order" << std::endl << "in DFS order" << std::endl
<< " -S convert to explicit automata, and number states " << " -S convert to explicit automata, and number states "
@ -102,17 +112,7 @@ syntax(char* prog)
<< " -X do not compute an automaton, read it from a file" << " -X do not compute an automaton, read it from a file"
<< std::endl << std::endl
<< " -y do not merge states with same symbolic representation " << " -y do not merge states with same symbolic representation "
<< "(implies -f)" << std::endl << "(implies -f)" << std::endl;
<< " -R1 use direct simulation to reduce the automata "
<< "(implies -L)"
<< std::endl
<< " -R2 use delayed simulation to reduce the automata, incorrect"
<< "(implies -L)"
<< std::endl
<< " -R3 use SCC to reduce the automata"
<< std::endl
<< " -Rd to display simulation relation"
<< std::endl;
exit(2); exit(2);
} }
@ -393,12 +393,6 @@ main(int argc, char** argv)
to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
} }
/*
spot::tgba* aut_red = 0;
if (reduc_aut != spot::Reduce_None)
a = aut_red = spot::reduc_tgba_sim(a, reduc_aut);
*/
spot::tgba_reduc* aut_red = 0; spot::tgba_reduc* aut_red = 0;
if (reduc_aut != spot::Reduce_None) if (reduc_aut != spot::Reduce_None)
{ {

98
src/tgbatest/reductgba.cc
View file

@ -45,81 +45,107 @@
void void
syntax(char* prog) syntax(char* prog)
{ {
std::cerr << prog << " option formula1" << std::endl; #ifdef REDUCCMP
std::cerr << prog << " option file" << std::endl;
#else
std::cerr << prog << " option formula" << std::endl;
#endif
exit(2); exit(2);
} }
int int
main(int argc, char** argv) main(int argc, char** argv)
{ {
if (argc < 2) if (argc < 3)
syntax(argv[0]); syntax(argv[0]);
int o = spot::ltl::Reduce_None;
switch (atoi(argv[1]))
{
case 0:
o = spot::Reduce_Scc;
break;
case 1:
o = spot::Reduce_Dir_Sim;
break;
case 2:
o = spot::Reduce_Del_Sim;
break;
case 3:
o = spot::Reduce_Dir_Sim | spot::Reduce_Scc;
break;
case 4:
o = spot::Reduce_Del_Sim | spot::Reduce_Scc;
break;
case 5:
// No Reduction
break;
default:
return 2;
}
int exit_code = 0; int exit_code = 0;
spot::simulation_relation* rel = NULL; spot::simulation_relation* rel = NULL;
spot::tgba* automata = NULL; spot::tgba* automata = NULL;
spot::tgba* aut_red = NULL;
spot::tgba_reduc* automatareduc = NULL; spot::tgba_reduc* automatareduc = NULL;
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::bdd_dict* dict = new spot::bdd_dict(); spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::parse_error_list p1;
spot::ltl::formula* f = spot::ltl::parse(argv[1], p1, env);
//std::cout << "Compute the automata" << std::endl; #ifdef REDUCCMP
spot::tgba_parse_error_list pel;
automata = spot::tgba_parse(argv[2], pel, dict, env, false);
if (spot::format_tgba_parse_errors(std::cerr, pel))
return 2;
#else
spot::ltl::parse_error_list p1;
spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
return 2;
automata = spot::ltl_to_tgba_fm(f, dict, automata = spot::ltl_to_tgba_fm(f, dict,
false, true, false, true,
false, true); false, true);
#endif
//std::cout << "Display the automata" << std::endl;
spot::dotty_reachable(std::cout, automata); spot::dotty_reachable(std::cout, automata);
//std::cout << "Initialize the reduction automata" << std::endl;
automatareduc = new spot::tgba_reduc(automata); automatareduc = new spot::tgba_reduc(automata);
//aut_red = spot::reduc_tgba_sim(automata); if (o & spot::Reduce_Dir_Sim)
{
//std::cout << "Compute the simulation relation" << std::endl; rel = spot::get_direct_relation_simulation(automatareduc);
//rel = spot::get_direct_relation_simulation(automatareduc);
rel = spot::get_delayed_relation_simulation(automatareduc);
//rel = NULL;
//std::cout << "Display of the parity game" << std::endl;
//std::cout << "Display of the simulation relation" << std::endl;
if (rel != NULL)
automatareduc->display_rel_sim(rel, std::cout);
//std::cout << "Prune automata using simulation relation" << std::endl;
if (rel != NULL)
automatareduc->prune_automata(rel); automatareduc->prune_automata(rel);
}
//automatareduc->compute_scc(); else if (o & spot::Reduce_Del_Sim)
//std::cout << "Prune automata using scc" << std::endl; {
//automatareduc->prune_scc(); rel = spot::get_delayed_relation_simulation(automatareduc);
automatareduc->quotient_state(rel);
//std::cout << "Display of scc" << std::endl; }
//automatareduc->display_scc(std::cout);
if (rel != NULL) if (rel != NULL)
{
automatareduc->display_rel_sim(rel, std::cout);
spot::free_relation_simulation(rel); spot::free_relation_simulation(rel);
}
if (o & spot::Reduce_Scc)
{
automatareduc->prune_scc();
//automatareduc->display_scc(std::cout);
}
if (automatareduc != NULL) if (automatareduc != NULL)
{ {
std::cout << "Display of the minimize automata" << std::endl;
std::cout << std::endl;
spot::dotty_reachable(std::cout, automatareduc); spot::dotty_reachable(std::cout, automatareduc);
} }
if (aut_red != NULL)
delete aut_red;
if (automata != NULL) if (automata != NULL)
delete automata; delete automata;
if (automatareduc != NULL) if (automatareduc != NULL)
delete automatareduc; delete automatareduc;
#ifndef REDUCCMP
if (f != NULL) if (f != NULL)
spot::ltl::destroy(f); spot::ltl::destroy(f);
#endif
assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0);

73
src/tgbatest/reductgba.test
View file

@ -25,24 +25,67 @@
set -e set -e
check () check()
{ {
run 0 ./reductgba "$1" run 0 ./reductgba "$1" "$2"
} }
# We don't check the output, but just running these might be enough to # We don't check the output, but just running these might be enough to
# trigger assertions. # trigger assertions.
check 'a' # No reduction
check 'a U b' check 0 'Fa & Xb & GFc & Gd'
check 'a U Fb' check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 'X a'
check 'a & b & c' check 1 a
check 'a | b | (c U (d & (g U (h ^ i))))' check 1 'a U b'
check 'Xa & (b U !a) & (b U !a)' check 1 'X a'
check 'Fa & Xb & GFc & Gd' check 1 'a & b & c'
check 'Fa & Xa & GFc & Gc' check 1 'a | b | (c U (d & (g U (h ^ i))))'
check 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 1 'Xa & (b U !a) & (b U !a)'
check 'a R (b R c)' check 1 'Fa & Xb & GFc & Gd'
check '(a U b) U (c U d)' check 1 'Fa & Xa & GFc & Gc'
check '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 1 'a R (b R c)'
check 1 '(a U b) U (c U d)'
check 1 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
#reduction
check 1 'a U Fb'
#check 0 a
#check 0 'a U b'
#check 0 'a U Fb'
#check 3 a
#check 3 'a U b'
#check 3 'a U Fb'
#check 0 a
#check 0 'a U b'
#check 0 'a U Fb'
#check 0 'X a'
#check 0 'a & b & c'
#check 0 'a | b | (c U (d & (g U (h ^ i))))'
#check 0 'Xa & (b U !a) & (b U !a)'
#check 0 'Fa & Xb & GFc & Gd'
#check 0 'Fa & Xa & GFc & Gc'
#check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
#check 0 'a R (b R c)'
#check 0 '(a U b) U (c U d)'
#check 0 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
#check 3 a
#check 3 'a U b'
#check 3 'a U Fb'
#check 3 'X a'
#check 3 'a & b & c'
#check 3 'a | b | (c U (d & (g U (h ^ i))))'
#check 3 'Xa & (b U !a) & (b U !a)'
#check 3 'Fa & Xb & GFc & Gd'
#check 3 'Fa & Xa & GFc & Gc'
#check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
#check 3 'a R (b R c)'
#check 3 '(a U b) U (c U d)'
#check 3 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'

4
src/tgbatest/spotlbtt.test
View file

@ -94,14 +94,14 @@ Algorithm
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM), post reduction" Name = "Spot (Couvreur -- FM), post reduction"
Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R1 -R2 -F -f -t'" Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R1 -F -f -t'"
Enabled = yes Enabled = yes
} }
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM), pre + post reduction" Name = "Spot (Couvreur -- FM), pre + post reduction"
Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -R1 -R2 -F -f -t'" Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -R1 -F -f -t'"
Enabled = yes Enabled = yes
} }