The computation of the counter example fails the valgrind tests
and is wrong into two ways: the search stack is generally not a path, and does not run until the end of the STL container. Remove it. * src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh (tarjan_on_fly): Do not inherit from the emptiness_search class, because the check method will no longer return a counter example. (tarjan_on_fly::check): Return only a boolean. (tarjan_on_fly::build_counter): Delete. * src/tgbatest/ltl2tgba.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
ca27267c69
commit
e8e2bec243
4 changed files with 30 additions and 88 deletions
17
ChangeLog
17
ChangeLog
|
|
@ -1,5 +1,16 @@
|
|||
2004-10-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
The computation of the counter example fails the valgrind tests
|
||||
and is wrong into two ways: the search stack is generally not a
|
||||
path, and does not run until the end of the STL container.
|
||||
Remove it.
|
||||
* src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh
|
||||
(tarjan_on_fly): Do not inherit from the emptiness_search class,
|
||||
because the check method will no longer return a counter example.
|
||||
(tarjan_on_fly::check): Return only a boolean.
|
||||
(tarjan_on_fly::build_counter): Delete.
|
||||
* src/tgbatest/ltl2tgba.cc: Adjust.
|
||||
|
||||
* src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state,
|
||||
tgba_explicit_succ_iterator::current_condition,
|
||||
tgba_explicit_succ_iterator::current_accepting_conditions): Assert
|
||||
|
|
@ -109,7 +120,7 @@
|
|||
src/tgbaalgos/minimalce.hh,
|
||||
src/tgbaalgos/minimalce.cc,
|
||||
src/tgbaalgos/colordfs.hh,
|
||||
src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check.
|
||||
src/tgbaalgos/colordfs.cc: four new algorithms for emptiness check.
|
||||
|
||||
* src/tgbaalgos/gtec/ce.hh,
|
||||
src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
|
||||
|
|
@ -117,7 +128,7 @@
|
|||
|
||||
* src/tgbatest/ltl2tgba.cc,
|
||||
src/tgbatest/emptchk.test,
|
||||
src/tgbaalgos/Makefile.am: Add files for emptyness-check.
|
||||
src/tgbaalgos/Makefile.am: Add files for emptiness-check.
|
||||
|
||||
2004-08-23 Thomas Martinez <martinez@src.lip6.fr>
|
||||
|
||||
|
|
@ -3174,7 +3185,7 @@
|
|||
|
||||
Switch from "promises" to "accepting sets". Fix the definitions
|
||||
of these accepting sets so that they are really useful. Provide
|
||||
an all_accepting_conditions() method for use in the emptyness
|
||||
an all_accepting_conditions() method for use in the emptiness
|
||||
check, and a neg_accepting_conditions() for products. Predeclare
|
||||
TGBA accepting conditions in the i/o.
|
||||
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
ce::counter_example*
|
||||
bool
|
||||
tarjan_on_fly::check()
|
||||
{
|
||||
tgba_succ_iterator* iter = 0;
|
||||
|
|
@ -96,12 +96,7 @@ namespace spot
|
|||
pop();
|
||||
}
|
||||
|
||||
if (violation)
|
||||
return build_counter();
|
||||
|
||||
//std::cout << "NO COUNTER EXAMPLE FOUND" << std::endl;
|
||||
|
||||
return 0;
|
||||
return violation;
|
||||
}
|
||||
|
||||
void
|
||||
|
|
@ -148,12 +143,6 @@ namespace spot
|
|||
void
|
||||
tarjan_on_fly::pop()
|
||||
{
|
||||
/*
|
||||
const state *s = stack[dftop].s;
|
||||
hash_type::iterator hi = h.find(s);
|
||||
hi->second = -1;
|
||||
*/
|
||||
|
||||
int p = stack[dftop].pre;
|
||||
|
||||
if (p >= 0)
|
||||
|
|
@ -183,14 +172,6 @@ namespace spot
|
|||
{
|
||||
int n = 0;
|
||||
|
||||
/*
|
||||
hash_type::const_iterator hi = h.find(s);
|
||||
if (hi != h.end())
|
||||
n = hi->second;
|
||||
else
|
||||
n = -1;
|
||||
*/
|
||||
|
||||
stack_type::const_iterator i;
|
||||
for (i = stack.begin(); i != stack.end(); ++i, ++n)
|
||||
if (s->compare(i->s) == 0)
|
||||
|
|
@ -202,38 +183,10 @@ namespace spot
|
|||
return n;
|
||||
}
|
||||
|
||||
ce::counter_example*
|
||||
tarjan_on_fly::build_counter()
|
||||
{
|
||||
ce = new ce::counter_example(a);
|
||||
|
||||
stack_type::iterator i;
|
||||
for (i = stack.begin(); i != stack.end(); ++i)
|
||||
{
|
||||
if (x && x->compare(i->s) == 0)
|
||||
break;
|
||||
|
||||
ce->prefix.push_back(ce::state_ce(i->s->clone(),
|
||||
i->lasttr->current_condition()));
|
||||
}
|
||||
|
||||
for (; i != stack.end(); ++i)
|
||||
{
|
||||
ce->cycle.push_back(ce::state_ce(i->s->clone(),
|
||||
i->lasttr->current_condition()));
|
||||
}
|
||||
|
||||
return ce;
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
tarjan_on_fly::print_stat(std::ostream& os) const
|
||||
{
|
||||
int ce_size = 0;
|
||||
if (ce)
|
||||
ce_size = ce->size();
|
||||
os << "Size of Counter Example : " << ce_size << std::endl
|
||||
<< "States explored : " << h.size() << std::endl;
|
||||
os << "States explored : " << h.size() << std::endl;
|
||||
return os;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -27,13 +27,11 @@
|
|||
#include <utility>
|
||||
#include <ostream>
|
||||
#include "tgba/tgbatba.hh"
|
||||
//#include "tgba/bddprint.hh"
|
||||
#include "tgbaalgos/minimalce.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
class tarjan_on_fly: public emptiness_search
|
||||
class tarjan_on_fly
|
||||
{
|
||||
|
||||
public:
|
||||
|
|
@ -41,8 +39,8 @@ namespace spot
|
|||
tarjan_on_fly(const tgba_tba_proxy *a);
|
||||
virtual ~tarjan_on_fly();
|
||||
|
||||
/// \brief Find a counter example.
|
||||
virtual ce::counter_example* check();
|
||||
/// \brief Return true if there exits an accepting path.
|
||||
bool check();
|
||||
|
||||
/// \brief Print Stat.
|
||||
std::ostream& print_stat(std::ostream& os) const;
|
||||
|
|
@ -56,8 +54,6 @@ namespace spot
|
|||
int lowlink;
|
||||
int pre;
|
||||
int acc;
|
||||
|
||||
//int pos;
|
||||
};
|
||||
|
||||
//typedef std::pair<int, tgba_succ_iterator*> state_iter_pair;
|
||||
|
|
@ -65,8 +61,6 @@ namespace spot
|
|||
state_ptr_hash, state_ptr_equal> hash_type;
|
||||
hash_type h; ///< Map of visited states.
|
||||
|
||||
|
||||
//typedef std::pair<const state*, struct_state> pair_type;
|
||||
typedef std::vector<struct_state> stack_type;
|
||||
stack_type stack; ///< Stack of visited states on the path.
|
||||
|
||||
|
|
@ -77,16 +71,11 @@ namespace spot
|
|||
bool violation;
|
||||
|
||||
const state* x;
|
||||
ce::counter_example* ce;
|
||||
|
||||
void push(const state* s);
|
||||
void pop();
|
||||
void lowlinkupdate(int f, int t);
|
||||
int in_stack(const state* s) const;
|
||||
|
||||
ce::counter_example* build_counter();
|
||||
//clock_t tps_;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -721,14 +721,6 @@ main(int argc, char** argv)
|
|||
spot::counter_example ce(ec->result());
|
||||
ce.print_result(std::cout);
|
||||
ce.print_stats(std::cout);
|
||||
|
||||
//spot::ce::counter_example* res2 = ce.get_counter_example();
|
||||
//spot::tgba* aut = res2->ce2tgba();
|
||||
//spot::dotty_reachable(std::cout, aut);
|
||||
//res2->print(std::cout);
|
||||
//delete res2;
|
||||
//delete aut;
|
||||
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -744,15 +736,7 @@ main(int argc, char** argv)
|
|||
spot::nesteddfsgen_search* ec = new spot::nesteddfsgen_search(a);
|
||||
bool res = ec->check();
|
||||
ec->print_stats(std::cout);
|
||||
if (expect_counter_example)
|
||||
{
|
||||
if (!res)
|
||||
exit_code = 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
exit_code = res;
|
||||
}
|
||||
exit_code = expect_counter_example ? !res : res;
|
||||
delete ec;
|
||||
}
|
||||
break;
|
||||
|
|
@ -786,9 +770,14 @@ main(int argc, char** argv)
|
|||
break;
|
||||
|
||||
case TarjanOnFly:
|
||||
std::cout << "Tarjan On Fly" << std::endl;
|
||||
es = new spot::tarjan_on_fly(degeneralized);
|
||||
break;
|
||||
{
|
||||
std::cout << "Tarjan On Fly" << std::endl;
|
||||
spot::tarjan_on_fly* tof = new spot::tarjan_on_fly(degeneralized);
|
||||
bool res = tof->check();
|
||||
exit_code = expect_counter_example ? !res : res;
|
||||
delete tof;
|
||||
break;
|
||||
}
|
||||
|
||||
case MinimalSearch:
|
||||
{
|
||||
|
|
@ -804,7 +793,7 @@ main(int argc, char** argv)
|
|||
break;
|
||||
|
||||
case MinimalSearchIterative:
|
||||
std::cout << "Iterative Minimal Search" << std::endl;
|
||||
std::cout << "Iterative Minimal Search" << std::endl;
|
||||
es = new spot::minimalce_search(degeneralized, true);
|
||||
break;
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue