Commit abbd0eee authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgbaalgos/gtec/status.hh

(couvreur99_check_status::cycle_seed): New attribute.
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
couvreur99_check_shy::check): Fill cycle_seed.
* src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc:
(couvreur99_check_result::accepting_run,
couvreur99_check_result::accepting_cycle): Revamp to compute a
cycle from the cycle_start, and then the shortest prefix to this
cycle.
parent 27966c28
2004-12-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/status.hh
(couvreur99_check_status::cycle_seed): New attribute.
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
couvreur99_check_shy::check): Fill cycle_seed.
* src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc:
(couvreur99_check_result::accepting_run,
couvreur99_check_result::accepting_cycle): Revamp to compute a
cycle from the cycle_start, and then the shortest prefix to this
cycle.
* iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, iface/gspn/ssp.cc: Disable
the functions that were using the interface I have just broken.
* src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap::find): Clarify
comment.
......
......@@ -263,7 +263,11 @@ main(int argc, char **argv)
ce = new spot::couvreur99_check_result(ecs);
break;
default:
ce = spot::counter_example_ssp(ecs);
// ce = spot::counter_example_ssp(ecs);
std::cerr
<< "counter_example_ssp() is no longer supported"
<< std::endl;
exit(1);
}
#endif
spot::tgba_run* run = ce->accepting_run();
......
......@@ -1003,6 +1003,10 @@ namespace spot
return new couvreur99_check_shy_ssp(ssp_automata);
}
#if 0
// I rewrote couvreur99_check_result today, and it no longer use
// connected_component_ssp_factory. So this cannot work anymore.
// -- adl 2004-12-10.
couvreur99_check_result*
counter_example_ssp(const couvreur99_check_status* status)
{
......@@ -1010,4 +1014,5 @@ namespace spot
couvreur99_check_result(status,
connected_component_ssp_factory::instance());
}
#endif
}
......@@ -55,9 +55,13 @@ namespace spot
couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata);
couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata);
couvreur99_check_result*
counter_example_ssp(const couvreur99_check_status* status);
/// @}
// I rewrote couvreur99_check_result today, and it no longer use
// connected_component_ssp_factory. So this cannot work anymore.
// -- adl 2004-12-10.
// couvreur99_check_result*
// counter_example_ssp(const couvreur99_check_status* status);
}
#endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH
......@@ -24,167 +24,153 @@
namespace spot
{
couvreur99_check_result::couvreur99_check_result
(const couvreur99_check_status* ecs,
const explicit_connected_component_factory* eccf)
: emptiness_check_result(ecs->aut), ecs_(ecs), eccf_(eccf)
{
}
tgba_run*
couvreur99_check_result::accepting_run()
namespace
{
run_ = new tgba_run;
assert(!ecs_->root.empty());
scc_stack::stack_type root = ecs_->root.s;
int comp_size = root.size();
// Transform the stack of connected component into an array.
explicit_connected_component** scc =
new explicit_connected_component*[comp_size];
for (int j = comp_size - 1; 0 <= j; --j)
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> state_set;
class shortest_path: public bfs_steps
{
public:
shortest_path(const state_set* t, const couvreur99_check_status* ecs)
: bfs_steps(ecs->aut), target(t), ecs(ecs)
{
scc[j] = eccf_->build();
scc[j]->index = root.top().index;
scc[j]->condition = root.top().condition;
root.pop();
}
assert(root.empty());
// Build the set of states for all SCCs.
numbered_state_heap_const_iterator* i = ecs_->h->iterator();
for (i->first(); !i->done(); i->next())
const state*
search(const state* start, tgba_run::steps& l)
{
int index = i->get_index();
// Skip states from dead SCCs.
if (index < 0)
continue;
assert(index != 0);
// Find the SCC this state belongs to.
int j;
for (j = 1; j < comp_size; ++j)
if (index < scc[j]->index)
break;
scc[j - 1]->insert(i->get_state());
return this->bfs_steps::search(filter(start), l);
}
delete i;
numbered_state_heap::state_index_p spi =
ecs_->h->index(ecs_->aut->get_init_state());
assert(spi.first);
// We build a path trough each SCC in the stack. For the
// first SCC, the starting state is the initial state of the
// automaton. The destination state is the closest state
// from the next SCC. This destination state becomes the
// starting state when building a path through the next SCC.
const state* start = spi.first;
for (int k = 0; k < comp_size - 1; ++k)
{
struct scc_bfs: bfs_steps
{
explicit_connected_component** scc;
int k;
bool in_next;
scc_bfs(const tgba* a, explicit_connected_component** scc, int k)
: bfs_steps(a), scc(scc), k(k)
{
}
virtual const state*
filter(const state* s)
{
const state* h_s = scc[k]->has_state(s);
if (!h_s)
{
h_s = scc[k+1]->has_state(s);
in_next = true;
if (!h_s)
delete s;
}
else
{
in_next = false;
}
return h_s;
}
virtual bool
match(tgba_run::step&, const state*)
const state*
filter(const state* s)
{
numbered_state_heap::state_index_p sip = ecs->h->find(s);
// Ignore unknown states ...
if (!sip.first)
{
return in_next;
delete s;
return 0;
}
} b(ecs_->aut, scc, k);
start = b.search(start, run_->prefix);
// ... as well as dead states.
if (*sip.second == -1)
return 0;
return sip.first;
}
accepting_cycle(scc[comp_size - 1], start,
scc[comp_size - 1]->condition);
bool
match(tgba_run::step&, const state* dest)
{
return target->find(dest) != target->end();
}
for (int j = comp_size - 1; 0 <= j; --j)
delete scc[j];
delete[] scc;
private:
state_set seen;
const state_set* target;
const couvreur99_check_status* ecs;
};
}
return run_;
couvreur99_check_result::couvreur99_check_result
(const couvreur99_check_status* ecs)
: emptiness_check_result(ecs->aut), ecs_(ecs)
{
}
namespace
tgba_run*
couvreur99_check_result::accepting_run()
{
struct triplet
{
const state* s; // Current state.
tgba_succ_iterator* iter; // Iterator to successor of the current state.
bdd acc; // All acceptance conditions traversed by
// the path so far.
run_ = new tgba_run;
triplet (const state* s, tgba_succ_iterator* iter, bdd acc)
: s(s), iter(iter), acc(acc)
assert(!ecs_->root.empty());
// Compute an accepting cycle.
accepting_cycle();
// Compute the prefix: it's the shortest path from the initial
// state of the automata to any state of the cycle.
// Register all states from the cycle as target of the BFS.
state_set ss;
for (tgba_run::steps::const_iterator i = run_->cycle.begin();
i != run_->cycle.end(); ++i)
ss.insert(i->s);
shortest_path shpath(&ss, ecs_);
const state* prefix_start = ecs_->aut->get_init_state();
// There are two cases: either the initial state is already on
// the cycle, or it is not. If it is, we will have to rotate
// the cycle so it begins on this position. Otherwise we will shift
// the cycle so it begins on the state that follows the prefix.
// cycle_entry_point is that state.
const state* cycle_entry_point;
state_set::const_iterator ps = ss.find(prefix_start);
if (ps != ss.end())
{
// The initial state is on the cycle.
delete prefix_start;
cycle_entry_point = *ps;
}
};
else
{
// This initial state is outside the cycle. Compute the prefix.
cycle_entry_point = shpath.search(prefix_start, run_->prefix);
}
// Locate cycle_entry_point on the cycle.
tgba_run::steps::iterator cycle_ep_it;
for (cycle_ep_it = run_->cycle.begin();
cycle_ep_it != run_->cycle.end()
&& cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
continue;
assert(cycle_ep_it != run_->cycle.end());
// Now shift the cycle so it starts on cycle_entry_point.
run_->cycle.splice(run_->cycle.end(), run_->cycle,
run_->cycle.begin(), cycle_ep_it);
run_->cycle.erase(run_->cycle.begin(), cycle_ep_it);
return run_;
}
void
couvreur99_check_result::accepting_cycle(const explicit_connected_component*
scc,
const state* start, bdd
acc_to_traverse)
couvreur99_check_result::accepting_cycle()
{
bdd acc_to_traverse = ecs_->aut->all_acceptance_conditions();
// Compute an accepting cycle using successive BFS that are
// restarted from the point reached after we have discovered a
// transition with a new acceptance conditions.
//
// This idea is taken from Product<T>::findWitness in LBTT 1.1.2.
const state* substart = start;
const state* substart = ecs_->cycle_seed;
do
{
struct scc_bfs: bfs_steps
{
const explicit_connected_component* scc;
bool in_next;
const couvreur99_check_status* ecs;
bdd& acc_to_traverse;
const state* start;
scc_bfs(const tgba* a, const explicit_connected_component* scc,
bdd& acc_to_traverse, const state* start)
: bfs_steps(a), scc(scc), acc_to_traverse(acc_to_traverse),
start(start)
int scc_root;
scc_bfs(const couvreur99_check_status* ecs,
bdd& acc_to_traverse)
: bfs_steps(ecs->aut), ecs(ecs), acc_to_traverse(acc_to_traverse),
scc_root(ecs->root.s.top().index)
{
}
virtual const state*
filter(const state* s)
{
const state* h_s = scc->has_state(s);
if (!h_s)
delete s;
return h_s;
numbered_state_heap::state_index_p sip = ecs->h->find(s);
// Ignore unknown states.
if (!sip.first)
{
delete s;
return 0;
}
// Stay in the final SCC.
if (*sip.second < scc_root)
return 0;
return sip.first;
}
virtual bool
......@@ -193,7 +179,7 @@ namespace spot
bdd less_acc = acc_to_traverse - st.acc;
if (less_acc != acc_to_traverse
|| (acc_to_traverse == bddfalse
&& s == start))
&& s == ecs->cycle_seed))
{
acc_to_traverse = less_acc;
return true;
......@@ -201,11 +187,11 @@ namespace spot
return false;
}
} b(ecs_->aut, scc, acc_to_traverse, start);
} b(ecs_, acc_to_traverse);
substart = b.search(substart, run_->cycle);
}
while (acc_to_traverse != bddfalse || substart != start);
while (acc_to_traverse != bddfalse || substart != ecs_->cycle_seed);
}
void
......
......@@ -23,7 +23,6 @@
# define SPOT_TGBAALGOS_GTEC_CE_HH
#include "status.hh"
#include "explscc.hh"
#include "tgbaalgos/emptiness.hh"
namespace spot
......@@ -32,11 +31,7 @@ namespace spot
class couvreur99_check_result: public emptiness_check_result
{
public:
couvreur99_check_result(const couvreur99_check_status* ecs,
const explicit_connected_component_factory*
eccf =
connected_component_hash_set_factory::instance());
couvreur99_check_result(const couvreur99_check_status* ecs);
virtual tgba_run* accepting_run();
......@@ -45,12 +40,10 @@ namespace spot
protected:
/// Called by accepting_run() to find a cycle which traverses all
/// acceptance conditions in the accepted SCC.
void accepting_cycle(const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse);
void accepting_cycle();
private:
const couvreur99_check_status* ecs_;
const explicit_connected_component_factory* eccf_;
tgba_run* run_;
};
}
......
......@@ -229,6 +229,9 @@ namespace spot
todo.pop();
dec_depth();
}
// Use this state to start the computation of an accepting
// cycle.
ecs_->cycle_seed = spi.first;
set_states(ecs_->states());
return new couvreur99_check_result(ecs_);
}
......@@ -288,7 +291,8 @@ namespace spot
succ_queue::iterator q = queue.begin();
while (q != queue.end())
{
int* i = find_state(q->s);
numbered_state_heap::state_index_p sip = ecs_->h->find(q->s);
int* i = sip.second;
if (!i)
{
// Skip unknown states.
......@@ -333,10 +337,15 @@ namespace spot
// merged SCC.
ecs_->root.top().condition |= acc;
// Have we found all acceptance conditions?
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
{
/// q->s has already been freed by find_state().
// Use this state to start the computation of an accepting
// cycle.
ecs_->cycle_seed = sip.first;
/// q->s has already been freed by ecs_->h->find.
queue.erase(q);
// We have found an accepting SCC. Clean up TODO.
// We must delete all states of apparing in TODO
......
......@@ -44,6 +44,7 @@ namespace spot
const tgba* aut;
scc_stack root;
numbered_state_heap* h; ///< Heap of visited states.
const state* cycle_seed;
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment