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

* src/tgbaalgo/semptinesscheck.hh (counter_example): New class,

Browse source 
extracted from ...
(emptiness_check): ... here.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-13 09:39:30 +00:00
parent 80b7cbcf45
commit 8a84cc6fb3
5 changed files with 124 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,5 +1,11 @@
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgo/semptinesscheck.hh (counter_example): New class,
extracted from ...
(emptiness_check): ... here.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.
* wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx)
($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c.

9
iface/gspn/ltlgspn.cc
View file

@ -175,24 +175,27 @@ main(int argc, char **argv)
res = ec.check();
else
res = ec.check2();
const spot::emptiness_check_status* ecs = ec.result();
if (!res)
{
if (compute_counter_example)
{
ec.counter_example();
ec.print_result(std::cout, proj ? model : 0);
spot::counter_example ce(ecs);
ce.print_result(std::cout, proj ? model : 0);
ce.print_stats(std::cout);
}
else
{
std::cout << "non empty" << std::endl;
ecs->print_stats(std::cout);
}
}
else
{
std::cout << "empty" << std::endl;
ecs->print_stats(std::cout);
}
std::cout << std::endl;
ec.print_stats(std::cout);
if (!res)
exit(1);
}

138
src/tgbaalgos/emptinesscheck.cc
View file

@ -96,6 +96,14 @@ namespace spot
return i->first;
}
void
emptiness_check_status::print_stats(std::ostream& os) const
{
os << h.size() << " unique states visited" << std::endl;
os << root.size()
<< " strongly connected components in search stack"
<< std::endl;
}
//////////////////////////////////////////////////////////////////////
@ -105,13 +113,6 @@ namespace spot
bool
emptiness_check::connected_component_set::has_state(const state* s) const
{
return states.find(s) != states.end();
}
emptiness_check::emptiness_check(const tgba* a)
{
ecs_ = new emptiness_check_status(a);
@ -473,68 +474,42 @@ namespace spot
}
}
std::ostream&
emptiness_check::print_result(std::ostream& os, const tgba* restrict) const
const emptiness_check_status*
emptiness_check::result() const
{
os << "Prefix:" << std::endl;
const bdd_dict* d = ecs_->aut->get_dict();
for (state_sequence::const_iterator i_se = suffix.begin();
i_se != suffix.end(); ++i_se)
{
os << " ";
if (restrict)
{
const state* s = ecs_->aut->project_state(*i_se, restrict);
assert(s);
os << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << ecs_->aut->format_state(*i_se) << std::endl;
}
}
os << "Cycle:" <<std::endl;
for (cycle_path::const_iterator it = period.begin();
it != period.end(); ++it)
{
os << " | " << bdd_format_set(d, it->second) << std::endl;
os << " ";
if (restrict)
{
const state* s = ecs_->aut->project_state(it->first, restrict);
assert(s);
os << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << ecs_->aut->format_state(it->first) << std::endl;
}
}
return os;
return ecs_;
}
void
emptiness_check::counter_example()
//////////////////////////////////////////////////////////////////////
bool
counter_example::connected_component_set::has_state(const state* s) const
{
return states.find(s) != states.end();
}
//////////////////////////////////////////////////////////////////////
counter_example::counter_example(const emptiness_check_status* ecs)
: ecs_(ecs)
{
assert(!ecs_->root.empty());
assert(suffix.empty());
int comp_size = ecs_->root.size();
scc_stack::stack_type root = ecs_->root.s;
int comp_size = root.size();
// Transform the stack of connected component into an array.
connected_component_set* scc = new connected_component_set[comp_size];
for (int j = comp_size - 1; 0 <= j; --j)
{
scc[j].index = ecs_->root.top().index;
scc[j].condition = ecs_->root.top().condition;
ecs_->root.pop();
scc[j].index = root.top().index;
scc[j].condition = root.top().condition;
root.pop();
}
assert(ecs_->root.empty());
assert(root.empty());
// Build the set of states for all SCCs.
for (emptiness_check_status::hash_type::iterator i = ecs_->h.begin();
for (emptiness_check_status::hash_type::const_iterator i = ecs_->h.begin();
i != ecs_->h.end(); ++i)
{
int index = i->second;
@ -635,7 +610,7 @@ namespace spot
}
void
emptiness_check::complete_cycle(const connected_component_set& scc,
counter_example::complete_cycle(const connected_component_set& scc,
const state* from,
const state* to)
{
@ -727,7 +702,7 @@ namespace spot
}
void
emptiness_check::accepting_path(const connected_component_set& scc,
counter_example::accepting_path(const connected_component_set& scc,
const state* start, bdd acc_to_traverse)
{
// State seen during the DFS.
@ -861,16 +836,55 @@ namespace spot
complete_cycle(scc, start, suffix.back());
}
std::ostream&
counter_example::print_result(std::ostream& os, const tgba* restrict) const
{
os << "Prefix:" << std::endl;
const bdd_dict* d = ecs_->aut->get_dict();
for (state_sequence::const_iterator i_se = suffix.begin();
i_se != suffix.end(); ++i_se)
{
os << " ";
if (restrict)
{
const state* s = ecs_->aut->project_state(*i_se, restrict);
assert(s);
os << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << ecs_->aut->format_state(*i_se) << std::endl;
}
}
os << "Cycle:" <<std::endl;
for (cycle_path::const_iterator it = period.begin();
it != period.end(); ++it)
{
os << " | " << bdd_format_set(d, it->second) << std::endl;
os << " ";
if (restrict)
{
const state* s = ecs_->aut->project_state(it->first, restrict);
assert(s);
os << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << ecs_->aut->format_state(it->first) << std::endl;
}
}
return os;
}
void
emptiness_check::print_stats(std::ostream& os) const
counter_example::print_stats(std::ostream& os) const
{
os << ecs_->h.size() << " unique states visited" << std::endl;
ecs_->print_stats(os);
os << suffix.size() << " states in suffix" << std::endl;
os << period.size() << " states in period" << std::endl;
os << ecs_->root.size()
<< " strongly connected components in search stack"
<< std::endl;
}
}

53
src/tgbaalgos/emptinesscheck.hh
View file

@ -53,7 +53,8 @@ namespace spot
size_t size() const;
bool empty() const;
std::stack<connected_component> s;
typedef std::stack<connected_component> stack_type;
stack_type s;
};
class emptiness_check_status
@ -74,6 +75,9 @@ namespace spot
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
};
/// \brief Check whether the language of an automate is empty.
@ -98,9 +102,6 @@ namespace spot
/// \endverbatim
class emptiness_check
{
typedef std::list<const state*> state_sequence;
typedef std::pair<const state*, bdd> state_proposition;
typedef std::list<state_proposition> cycle_path;
public:
emptiness_check(const tgba* a);
~emptiness_check();
@ -130,8 +131,31 @@ namespace spot
bool check2();
//@}
/// Compute a counter example if tgba_emptiness_check() returned false.
void counter_example();
const emptiness_check_status* result() const;
private:
emptiness_check_status* ecs_;
/// \brief Remove a strongly component from the hash.
///
/// This function remove all accessible state from a given
/// state. In other words, it removes the strongly connected
/// component that contains this state.
void remove_component(const state* start_delete);
};
class counter_example
{
public:
counter_example(const emptiness_check_status* ecs);
typedef std::pair<const state*, bdd> state_proposition;
typedef std::list<const state*> state_sequence;
typedef std::list<state_proposition> cycle_path;
state_sequence suffix;
cycle_path period;
/// \brief Display the example computed by counter_example().
///
@ -142,8 +166,7 @@ namespace spot
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
private:
protected:
struct connected_component_set: public scc_stack::connected_component
{
typedef Sgi::hash_set<const state*,
@ -156,17 +179,6 @@ namespace spot
bool has_state(const state* s) const;
};
emptiness_check_status* ecs_;
state_sequence suffix;
cycle_path period;
/// \brief Remove a strongly component from the hash.
///
/// This function remove all accessible state from a given
/// state. In other words, it removes the strongly connected
/// component that contains this state.
void remove_component(const state* start_delete);
/// Called by counter_example to find a path which traverses all
/// acceptance conditions in the accepted SCC.
void accepting_path (const connected_component_set& scc,
@ -176,6 +188,9 @@ namespace spot
/// example. Append a sequence to the path given by accepting_path.
void complete_cycle(const connected_component_set& scc,
const state* from, const state* to);
private:
const emptiness_check_status* ecs_;
};
}
#endif // SPOT_EMPTINESS_CHECK_HH

4
src/tgbatest/ltl2tgba.cc
View file

@ -379,8 +379,8 @@ main(int argc, char** argv)
exit_code = 1;
break;
}
ec.counter_example();
ec.print_result(std::cout);
spot::counter_example ce(ec.result());
ce.print_result(std::cout);
}
else
{