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

Kill some FIXMEs.

Browse source 
* src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove
useless FIXMEs.
* src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute
syntactic implications only when needed.
* src/tgbaalgos/reductgba_sim_del.cc
(build_recurse_successor_spoiler): Remplace the FIXME by an assert.
* src/tgba/tgbareduc.cc: Reword some comments, discard old
commented code.
This commit is contained in:
Alexandre Duret-Lutz 2008-04-14 11:35:57 +02:00
parent 6b9acabe76
commit 21c98c0a01
6 changed files with 47 additions and 156 deletions
Download patch file Download diff file Expand all files Collapse all files

13
ChangeLog
View file

@ -1,3 +1,16 @@
2008-04-14 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Kill some FIXMEs.
* src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove
useless FIXMEs.
* src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute
syntactic implications only when needed.
* src/tgbaalgos/reductgba_sim_del.cc
(build_recurse_successor_spoiler): Remplace the FIXME by an assert.
* src/tgba/tgbareduc.cc: Reword some comments, discard old
commented code.
2008-03-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/evtgbaparse/Makefile.am (AM_CXXFLAGS): Remove -Werror

9
src/ltlenv/environment.hh
View file

@ -1,6 +1,6 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -60,9 +60,6 @@ namespace spot
~environment()
{
}
// FIXME: More functions will be needed later, but
// it's enough for now.
};
}

5
src/ltlvisit/basicreduce.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2007, 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -309,7 +309,8 @@ namespace spot
for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
{
// FIXME: why would *i be 0 ?
// An iteration of the loop may zero some later elements
// of the vector to mark them as redundant. Skip them.
if (!*i)
continue;
unop* uo = dynamic_cast<unop*>(*i);

19
src/ltlvisit/reduce.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Copyright (C) 2004, 2006, 2007, 2008 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
@ -121,12 +121,6 @@ namespace spot
if (opt_ & Reduce_Syntactic_Implications)
{
// FIXME: These should be done only when needed.
bool inf = syntactic_implication(f1, f2);
bool infinv = syntactic_implication(f2, f1);
bool infnegleft = syntactic_implication_neg(f2, f1, false);
bool infnegright = syntactic_implication_neg(f2, f1, true);
switch (bo->op())
{
case binop::Xor:
@ -136,14 +130,14 @@ namespace spot
case binop::U:
/* a < b => a U b = b */
if (inf)
if (syntactic_implication(f1, f2))
{
result_ = f2;
destroy(f1);
return;
}
/* !b < a => a U b = Fb */
if (infnegleft)
if (syntactic_implication_neg(f2, f1, false))
{
result_ = unop::instance(unop::F, f2);
destroy(f1);
@ -164,14 +158,14 @@ namespace spot
case binop::R:
/* b < a => a R b = b */
if (infinv)
if (syntactic_implication(f2, f1))
{
result_ = f2;
destroy(f1);
return;
}
/* b < !a => a R b = Gb */
if (infnegright)
if (syntactic_implication_neg(f2, f1, true))
{
result_ = unop::instance(unop::G, f2);
destroy(f1);
@ -247,7 +241,6 @@ namespace spot
}
}
// FIXME
/* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */
for (f1 = res->begin(); f1 != res->end(); f1++)

151
src/tgba/tgbareduc.cc
View file

@ -1,6 +1,6 @@
// 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.
// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -318,10 +318,9 @@ namespace spot
void
tgba_reduc::remove_state(const spot::state* s)
{
// We suppose than the state is not reachable when call by
// merge_state => NO PREDECESSOR !!
// But it can be have some predecessor in state_predecessor_map_ !!
// So, we remove from it.
// We suppose that the state is not reachable when called by
// merge_state => NO PREDECESSOR. But it can be have some
// predecessor in state_predecessor_map_.
ns_map::iterator k =
name_state_map_.find(tgba_explicit::format_state(s));
@ -341,7 +340,7 @@ namespace spot
if (i == state_predecessor_map_.end()) // 0 predecessor
return;
// for all predecessor of s. Zero if call by merge_state.
// for all predecessor of s (none when called by merge_state)
for (std::list<state*>::iterator p = (i->second)->begin();
p != (i->second)->end(); ++p)
{
@ -362,7 +361,7 @@ namespace spot
}
// DESTROY THE STATE !? USELESS
// it will be destroy when the automaton will be delete
// it will be destroyed when the automaton is deleted
// name_state_map_::iterator = name_state_map_[st];
// const tgba_explicit::state* st = name_state_map_[this->format_state(s)];
}
@ -391,14 +390,14 @@ namespace spot
sp_map::iterator i = state_predecessor_map_.find(s1);
if (i == state_predecessor_map_.end()) // 0 predecessor
{
// We can remove s1 safely, without change the language
// We can remove s1 safely, without changing the language
// of the automaton.
this->remove_state(sim1);
return;
}
// for all predecessor of s1, not the initial state,
// we redirect transition whose lead to s1 to s2.
// we redirect to s2 the transitions that lead to s1.
for (std::list<state*>::iterator p = (i->second)->begin();
p != (i->second)->end(); ++p)
{
@ -406,24 +405,24 @@ namespace spot
for (tgba_explicit::state::iterator j = (*p)->begin();
j != (*p)->end(); ++j)
{
// if the successor if s1.
// if the successor was s1...
if ((*j)->dest == s1)
{
// We can redirect transition to s2.
// ... make it s2.
(*j)->dest = const_cast<tgba_explicit::state*>(s2);
}
}
}
// FIXME:
// Be careful, we have to stock on s2 the acceptance condition on the arc
// leaving s1 (possible when the simulation is delayed). Since s2 simulate
// s1, s2 has some label whose implies these of s1, so we can put the
// acceptance conditions on this arcs.
// FIXME: The following justification sounds really dubious.
//
// We have to stock on s2 the acceptance condition of the arc
// leaving s1 (possible when the simulation is delayed). Since s2
// simulates s1, s2 has some labels that imply these of s1, so we
// can put the acceptance conditions on its arcs.
for (tgba_explicit::state::const_iterator j = s1->begin();
j != s1->end(); ++j)
{
// FIXME
transition* t = new transition();
t->dest = (*j)->dest;
t->condition = (*j)->condition;
@ -434,11 +433,9 @@ namespace spot
// We remove all the predecessor of s1.
(i->second)->clear();
// then we can remove s1 safely, without change the language
// then we can remove s1 safely, without changing the language
// of the automaton.
// useless because the state is not reachable.
this->remove_state(sim1);
}
void
@ -621,25 +618,6 @@ namespace spot
i != s1->end(); ++i)
(*i)->acceptance_conditions = bddfalse;
}
/*
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;
}
*/
}
}
@ -825,7 +803,7 @@ namespace spot
void
tgba_reduc::remove_scc(spot::state* s)
{
// To remove a scc, we remove all his state.
// To remove a scc, we remove all its states.
seen_map::iterator sm = si_.find(s);
sm = si_.find(s);
@ -842,95 +820,6 @@ namespace spot
}
/*
void
tgba_reduc::remove_scc_depth_first(spot::state* s, int n)
{
if (n == -1)
{
assert(seen_ == 0);
seen_ = new seen_map();
}
seen_map::const_iterator sm = seen_->find(s);
if (sm == seen_->end())
seen_->insert(std::pair<const spot::state*, int>(s, 1));
else
return;
tgba_succ_iterator* j = this->succ_iter(s);
for (j->first(); !j->done(); j->next())
{
this->remove_scc_depth_first(j->current_state(), 1);
}
this->remove_state(s);
if (n == -1)
{
delete seen_;
seen_ = 0;
}
}
*/
/*
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_ == 0);
seen_ = new seen_map();
i = si_.find(s);
assert(i->first != 0);
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_ = 0;
if (acc_ == this->all_acceptance_conditions())
ret = false;
}
return ret;
}
*/
int
tgba_reduc::nb_set_acc_cond() const
{

6
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -389,9 +389,7 @@ namespace spot
build_recurse_successor_spoiler(spoiler_node* sn,
std::ostringstream& os)
{
// FIXME
if (sn == 0)
return;
assert(sn);
tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());