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

* src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh:

Browse source 
Reindent.
(emptiness_check::~emptiness_check, emptiness_check::emptiness_check):
Remove, unused.
This commit is contained in:
Alexandre Duret-Lutz 2003-10-22 14:33:12 +00:00
parent 22a53800d9
commit 558642fe9c
3 changed files with 382 additions and 368 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2003-10-22 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh:
Reindent.
(emptiness_check::~emptiness_check, emptiness_check::emptiness_check):
Remove, unused.
2003-10-15 Alexandre Duret-Lutz <adl@src.lip6.fr> 2003-10-15 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/ltlgspn.cc (main): Allow invocations with * iface/gspn/ltlgspn.cc (main): Allow invocations with

610
src/tgbaalgos/emptinesscheck.cc
View file

@ -22,55 +22,48 @@ namespace spot
{ {
connected_component::connected_component() connected_component::connected_component()
{ {
index = 0; index = 0;
condition = bddfalse; condition = bddfalse;
transition_acc = -1; transition_acc = -1;
nb_transition = 0; nb_transition = 0;
nb_state = 1; nb_state = 1;
not_null = false; not_null = false;
} }
connected_component::connected_component(int i, bdd a) connected_component::connected_component(int i, bdd a)
{ {
index = i; index = i;
condition = a; condition = a;
transition_acc = -1; transition_acc = -1;
nb_transition = 0; nb_transition = 0;
nb_state = 1; nb_state = 1;
not_null = false; not_null = false;
} }
connected_component::~connected_component() connected_component::~connected_component()
{ {
} }
std::string
connected_component::to_string_component()
{
return "+ index + condition + nbTransition + transitionCondition + notNull +";
}
bool bool
connected_component::isAccepted(tgba* aut) connected_component::isAccepted(tgba* aut)
{ {
return aut->all_accepting_conditions() == condition; return aut->all_accepting_conditions() == condition;
} }
/// \brief Remove all the nodes accessible from the given node start_delete. /// \brief Remove all the nodes accessible from the given node start_delete.
/// ///
/// The removed graphe is the subgraphe containing nodes store /// The removed graph is the subgraph containing nodes stored
///intable state_map with order -1. /// in table state_map with order -1.
void void
emptiness_check::remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete) emptiness_check::remove_component(const tgba& aut, seen& state_map,
{ const spot::state* start_delete)
{
std::stack<spot::tgba_succ_iterator*> to_remove; std::stack<spot::tgba_succ_iterator*> to_remove;
state_map[start_delete] = -1; state_map[start_delete] = -1;
tgba_succ_iterator* iter_delete = aut.succ_iter(start_delete); tgba_succ_iterator* iter_delete = aut.succ_iter(start_delete);
iter_delete->first(); iter_delete->first();
to_remove.push(iter_delete); to_remove.push(iter_delete);
while (!to_remove.empty()) while (!to_remove.empty())
{ {
tgba_succ_iterator* succ_delete = to_remove.top(); tgba_succ_iterator* succ_delete = to_remove.top();
to_remove.pop(); to_remove.pop();
@ -88,20 +81,12 @@ namespace spot
} }
} }
} }
} }
emptiness_check::~emptiness_check() /// \brief On-the-fly emptiness check.
{ ///
} /// The algorithm used here is adapted from Jean-Michel Couvreur's
/// Probataf tool.
emptiness_check::emptiness_check()
{
}
/// \brief On-the-fly emptiness check.
///
/// The algorithm used here is adapted from Jean-Michel Couvreur's
/// Probataf tool.
bool bool
emptiness_check::tgba_emptiness_check(const spot::tgba* aut_check) emptiness_check::tgba_emptiness_check(const spot::tgba* aut_check)
{ {
@ -110,11 +95,11 @@ emptiness_check::emptiness_check()
state* init = aut_check->get_init_state(); state* init = aut_check->get_init_state();
seen_state_num[init] = 1; seen_state_num[init] = 1;
root_component.push(spot::connected_component(1,bddfalse)); root_component.push(spot::connected_component(1,bddfalse));
arc_accepting.push(bddfalse); arc_accepting.push(bddfalse);
tgba_succ_iterator* iter_ = aut_check->succ_iter(init); tgba_succ_iterator* iter_ = aut_check->succ_iter(init);
iter_->first(); iter_->first();
todo.push(pair_state_iter(init, iter_ )); todo.push(pair_state_iter(init, iter_ ));
while (!todo.empty()) while (!todo.empty())
{ {
pair_state_iter step = todo.top(); pair_state_iter step = todo.top();
if ((step.second)->done()) if ((step.second)->done())
@ -123,12 +108,14 @@ emptiness_check::emptiness_check()
assert(!root_component.empty()); assert(!root_component.empty());
connected_component comp_tmp = root_component.top(); connected_component comp_tmp = root_component.top();
root_component.pop(); root_component.pop();
seen::iterator i_0 = seen_state_num.find(step.first); seen::iterator i_0 = seen_state_num.find(step.first);
assert(i_0 != seen_state_num.end()); assert(i_0 != seen_state_num.end());
if (comp_tmp.index == seen_state_num[step.first]) if (comp_tmp.index == seen_state_num[step.first])
{ {
/// The current node is a root of a Strong Connected Component. /// The current node is a root of a Strong Connected Component.
spot::emptiness_check::remove_component(*aut_check, seen_state_num, step.first); spot::emptiness_check::remove_component(*aut_check,
seen_state_num,
step.first);
assert(!arc_accepting.empty()); assert(!arc_accepting.empty());
arc_accepting.pop(); arc_accepting.pop();
assert(root_component.size() == arc_accepting.size()); assert(root_component.size() == arc_accepting.size());
@ -148,9 +135,9 @@ emptiness_check::emptiness_check()
iter_->next(); iter_->next();
if (i == seen_state_num.end()) if (i == seen_state_num.end())
{ {
/// New node. // New node.
nbstate = nbstate + 1; nbstate = nbstate + 1;
assert(nbstate != 0); assert(nbstate != 0);
seen_state_num[current_state] = nbstate; seen_state_num[current_state] = nbstate;
root_component.push(connected_component(nbstate, bddfalse)); root_component.push(connected_component(nbstate, bddfalse));
arc_accepting.push(current_accepting); arc_accepting.push(current_accepting);
@ -160,33 +147,39 @@ emptiness_check::emptiness_check()
} }
else if (seen_state_num[current_state] != -1) else if (seen_state_num[current_state] != -1)
{ {
/// A node with order != -1 (a seen node not removed). // A node with order != -1 (a seen node not removed).
assert(!root_component.empty()); assert(!root_component.empty());
connected_component comp = root_component.top(); connected_component comp = root_component.top();
root_component.pop(); root_component.pop();
bdd new_condition = bddfalse; bdd new_condition = bddfalse;
new_condition = bdd_apply(new_condition, current_accepting, bddop_or); new_condition = bdd_apply(new_condition, current_accepting,
new_condition = bdd_apply(new_condition, comp.condition, bddop_or); bddop_or);
new_condition = bdd_apply(new_condition, comp.condition,
bddop_or);
int current_index = seen_state_num[current_state]; int current_index = seen_state_num[current_state];
while (comp.index > current_index) while (comp.index > current_index)
{ {
/// root_component and arc_accepting are popped // root_component and arc_accepting are popped
/// until the head of root_component is less or // until the head of root_component is less or
/// equal to the order of the current state. // equal to the order of the current state.
assert(!root_component.empty()); assert(!root_component.empty());
comp = root_component.top(); comp = root_component.top();
root_component.pop(); root_component.pop();
new_condition = bdd_apply(new_condition,comp.condition, bddop_or); new_condition = bdd_apply(new_condition,comp.condition,
bddop_or);
assert(!arc_accepting.empty()); assert(!arc_accepting.empty());
bdd arc_acc = arc_accepting.top(); bdd arc_acc = arc_accepting.top();
arc_accepting.pop(); arc_accepting.pop();
new_condition = bdd_apply(new_condition, arc_acc, bddop_or); new_condition = bdd_apply(new_condition, arc_acc,
bddop_or);
} }
comp.condition = bdd_apply(comp.condition, new_condition, bddop_or); comp.condition = bdd_apply(comp.condition, new_condition,
bddop_or);
if (aut_check->all_accepting_conditions() == comp.condition) if (aut_check->all_accepting_conditions() == comp.condition)
{ {
/// A failure SCC is find, the automata is not empty. // A failure SCC is find, the automata is not empty.
//spot::bdd_print_dot(std::cout, aut_check->get_dict(),comp.condition); // spot::bdd_print_dot(std::cout, aut_check->get_dict(),
// comp.condition);
root_component.push(comp); root_component.push(comp);
std::cout << "CONSISTENT AUTOMATA" << std::endl; std::cout << "CONSISTENT AUTOMATA" << std::endl;
return false; return false;
@ -196,232 +189,264 @@ emptiness_check::emptiness_check()
} }
} }
} }
/// The automata is empty. // The automata is empty.
std::cout << "EMPTY LANGUAGE" << std::endl; std::cout << "EMPTY LANGUAGE" << std::endl;
return true; return true;
} }
std::ostream& std::ostream&
emptiness_check::print_result(std::ostream& os, const spot::tgba* aut, const tgba* restrict ) const emptiness_check::print_result(std::ostream& os, const spot::tgba* aut,
const tgba* restrict) const
{ {
os << "======================" << std::endl; os << "======================" << std::endl;
os << "Prefix:" << std::endl; os << "Prefix:" << std::endl;
os << "======================" << std::endl; os << "======================" << std::endl;
const bdd_dict* d = aut->get_dict(); const bdd_dict* d = aut->get_dict();
for (state_sequence::const_iterator i_se = seq_counter.begin(); i_se != seq_counter.end(); i_se++) for (state_sequence::const_iterator i_se = seq_counter.begin();
{ i_se != seq_counter.end(); i_se++)
if (restrict) {
{ if (restrict)
os << "*****Projected STATE :" << restrict->format_state(aut->project_state((*i_se), restrict)) << "*****" << std::endl;
}
else
{
os << "*****print STATE :" << aut->format_state((*i_se)) << "*****" << std::endl;
}
}
os << "======================" << std::endl;
os << "Cycle:" <<std::endl;
os << "======================" << std::endl;
for (cycle_path::const_iterator it = periode.begin(); it != periode.end(); it++)
{
if (restrict)
{
os << " | " << bdd_format_set(d, (*it).second) <<std::endl ;
os << "*****Projected STATE :" << restrict->format_state(aut->project_state((*it).first, restrict)) << "*****" << std::endl;
}
else
{
os << " | " << bdd_format_set(d, (*it).second) <<std::endl ;
os << "*****print STATE :" << aut->format_state((*it).first) << "*****" << std::endl;
}
}
return os;
}
/// \brief Build a possible prefixe and period for a counter example.
void
emptiness_check::counter_example(const spot::tgba* aut_counter)
{
std::deque <pair_state_iter> todo_trace;
typedef std::map <const spot::state*, const spot::state*, spot::state_ptr_less_than> path_state;
path_state path_map;
if (!root_component.empty()){
int comp_size = root_component.size();
typedef std::vector<connected_component> vec_compo;
vec_compo vec_component;
vec_component.resize(comp_size);
vec_sequence.resize(comp_size);
state_sequence seq;
state_sequence tmp_lst;
state_sequence best_lst;
bdd tmp_acc = bddfalse;
std::stack <pair_state_iter> todo_accept;
for (int j = comp_size -1; j >= 0; j--)
{ {
vec_component[j] = root_component.top(); os << restrict->format_state(aut->project_state((*i_se), restrict))
root_component.pop(); << std::endl;
}
int q_index;
int tmp_int = 0;
/// Fill the SCC in the stack root_component.
for (seen::iterator iter_map = seen_state_num.begin(); iter_map != seen_state_num.end(); iter_map++)
{
q_index = (*iter_map).second;
tmp_int = 0;
if (q_index > 0)
{
while ((tmp_int < comp_size) && (vec_component[tmp_int].index <= q_index))
{
tmp_int = tmp_int+1;
}
if (tmp_int < comp_size)
{
vec_component[tmp_int-1].state_set.insert((*iter_map).first);
}
else
{
vec_component[comp_size-1].state_set.insert((*iter_map).first);
}
}
}
state* start_state = aut_counter->get_init_state();
if (comp_size != 1)
{
todo_trace.push_back(pair_state_iter(start_state, aut_counter->succ_iter(start_state)));
for (int k = 0; k < comp_size-1; k++)
{
/// We build a path trought all SCC in the stack : a
///possible prefixe for a counter example.
while (!todo_trace.empty())
{
pair_state_iter started_from = todo_trace.front();
todo_trace.pop_front();
(started_from.second)->first();
for ((started_from.second)->first(); !started_from.second->done(); started_from.second->next())
{
const state* curr_state =(started_from.second)->current_state();
connected_component::set_of_state::iterator iter_set = vec_component[k+1].state_set.find(curr_state);
if (iter_set != vec_component[k+1].state_set.end())
{
const state* curr_father = started_from.first;
seq.push_front(*iter_set);
seq.push_front(curr_father);
seen::iterator i_2 = seen_state_num.find(curr_father);
assert(i_2 != seen_state_num.end());
while ((vec_component[k].index < seen_state_num[curr_father]) && (seen_state_num[curr_father] != 1))
{
seq.push_front(path_map[curr_father]);
curr_father = path_map[curr_father];
seen::iterator i_3 = seen_state_num.find(curr_father);
assert(i_3 != seen_state_num.end());
}
vec_sequence[k] = seq;
seq.clear();
todo_trace.clear();
break;
}
else
{
connected_component::set_of_state::iterator i_s = vec_component[k].state_set.find(curr_state);
if (i_s != vec_component[k].state_set.end())
{
path_state::iterator i_path = path_map.find(curr_state);
seen::iterator i_seen = seen_state_num.find(curr_state);
if (i_seen != seen_state_num.end() && seen_state_num[curr_state] > 0 && i_path == path_map.end())
{
todo_trace.push_back(pair_state_iter(curr_state, aut_counter->succ_iter(curr_state)));
path_map[curr_state] = started_from.first;
}
}
}
}
}
todo_trace.push_back(pair_state_iter(vec_sequence[k].back(), aut_counter->succ_iter(vec_sequence[k].back())));
}
} }
else else
{ {
seq_counter.push_front(start_state); os << aut->format_state((*i_se)) << std::endl;
} }
for (int n_ = 0; n_ < comp_size-1; n_++) }
{ os << "======================" << std::endl;
for (state_sequence::iterator it = vec_sequence[n_].begin(); it != vec_sequence[n_].end(); it++) os << "Cycle:" <<std::endl;
os << "======================" << std::endl;
for (cycle_path::const_iterator it = periode.begin();
it != periode.end(); it++)
{
if (restrict)
{
os << " | " << bdd_format_set(d, (*it).second) <<std::endl ;
os << restrict->format_state(aut->project_state((*it).first,
restrict))
<< std::endl;
}
else
{
os << " | " << bdd_format_set(d, (*it).second) <<std::endl ;
os << aut->format_state((*it).first) << std::endl;
}
}
return os;
}
/// \brief Build a possible prefixe and period for a counter example.
void
emptiness_check::counter_example(const spot::tgba* aut_counter)
{
std::deque <pair_state_iter> todo_trace;
typedef std::map<const spot::state*, const spot::state*,
spot::state_ptr_less_than> path_state;
path_state path_map;
if (!root_component.empty()){
int comp_size = root_component.size();
typedef std::vector<connected_component> vec_compo;
vec_compo vec_component;
vec_component.resize(comp_size);
vec_sequence.resize(comp_size);
state_sequence seq;
state_sequence tmp_lst;
state_sequence best_lst;
bdd tmp_acc = bddfalse;
std::stack<pair_state_iter> todo_accept;
for (int j = comp_size -1; j >= 0; j--)
{
vec_component[j] = root_component.top();
root_component.pop();
}
int q_index;
int tmp_int = 0;
// Fill the SCC in the stack root_component.
for (seen::iterator iter_map = seen_state_num.begin();
iter_map != seen_state_num.end(); iter_map++)
{
q_index = (*iter_map).second;
tmp_int = 0;
if (q_index > 0)
{
while ((tmp_int < comp_size)
&& (vec_component[tmp_int].index <= q_index))
tmp_int = tmp_int+1;
if (tmp_int < comp_size)
vec_component[tmp_int-1].state_set.insert((*iter_map).first);
else
vec_component[comp_size-1].state_set.insert((*iter_map).first);
}
}
state* start_state = aut_counter->get_init_state();
if (comp_size != 1)
{
tgba_succ_iterator* i = aut_counter->succ_iter(start_state);
todo_trace.push_back(pair_state_iter(start_state, i));
for (int k = 0; k < comp_size-1; k++)
{
// We build a path trought all SCC in the stack : a
// possible prefixe for a counter example.
while (!todo_trace.empty())
{
pair_state_iter started_from = todo_trace.front();
todo_trace.pop_front();
started_from.second->first();
for (started_from.second->first();
!started_from.second->done();
started_from.second->next())
{
const state* curr_state =
started_from.second->current_state();
connected_component::set_of_state::iterator iter_set =
vec_component[k+1].state_set.find(curr_state);
if (iter_set != vec_component[k+1].state_set.end())
{
const state* curr_father = started_from.first;
seq.push_front(*iter_set);
seq.push_front(curr_father);
seen::iterator i_2 =
seen_state_num.find(curr_father);
assert(i_2 != seen_state_num.end());
while ((vec_component[k].index
< seen_state_num[curr_father])
&& (seen_state_num[curr_father] != 1))
{
seq.push_front(path_map[curr_father]);
curr_father = path_map[curr_father];
seen::iterator i_3 =
seen_state_num.find(curr_father);
assert(i_3 != seen_state_num.end());
}
vec_sequence[k] = seq;
seq.clear();
todo_trace.clear();
break;
}
else
{
connected_component::set_of_state::iterator i_s =
vec_component[k].state_set.find(curr_state);
if (i_s != vec_component[k].state_set.end())
{
path_state::iterator i_path =
path_map.find(curr_state);
seen::iterator i_seen =
seen_state_num.find(curr_state);
if (i_seen != seen_state_num.end()
&& seen_state_num[curr_state] > 0
&& i_path == path_map.end())
{
todo_trace.
push_back(pair_state_iter(curr_state,
aut_counter->succ_iter(curr_state)));
path_map[curr_state] = started_from.first;
}
}
}
}
}
todo_trace.
push_back(pair_state_iter(vec_sequence[k].back(),
aut_counter->succ_iter(vec_sequence[k].back())));
}
}
else
{
seq_counter.push_front(start_state);
}
for (int n_ = 0; n_ < comp_size-1; n_++)
{
for (state_sequence::iterator it = vec_sequence[n_].begin();
it != vec_sequence[n_].end(); it++)
{ {
seq_counter.push_back(*it); seq_counter.push_back(*it);
} }
}
seq_counter.unique();
emptiness_check::accepting_path(aut_counter, vec_component[comp_size-1], seq_counter.back(),vec_component[comp_size-1].condition);
}
else
{
std::cout << "EMPTY LANGUAGE NO COUNTER EXEMPLE" << std::endl;
} }
seq_counter.unique();
emptiness_check::accepting_path(aut_counter, vec_component[comp_size-1], seq_counter.back(),vec_component[comp_size-1].condition);
} }
else
{
std::cout << "EMPTY LANGUAGE NO COUNTER EXEMPLE" << std::endl;
}
}
/// \brief complete the path build by accepting_path to get the /// \brief complete the path build by accepting_path to get the period.
///period (cycle). void
void emptiness_check::complete_cycle(const spot::tgba* aut_counter,
emptiness_check::complete_cycle(const spot::tgba* aut_counter, const connected_component& comp_path, const state* from_state,const state* to_state) const connected_component& comp_path,
{ const state* from_state,
if (seen_state_num[from_state] != seen_state_num[to_state]) const state* to_state)
{ {
std::map <const spot::state*, state_proposition, spot::state_ptr_less_than> complete_map; if (seen_state_num[from_state] != seen_state_num[to_state])
std::deque <pair_state_iter> todo_complete; {
spot::tgba_succ_iterator* ite = aut_counter->succ_iter(from_state); std::map<const spot::state*, state_proposition,
todo_complete.push_back(pair_state_iter(from_state, ite)); spot::state_ptr_less_than> complete_map;
cycle_path tmp_comp; std::deque<pair_state_iter> todo_complete;
while(!todo_complete.empty()) spot::tgba_succ_iterator* ite = aut_counter->succ_iter(from_state);
{ todo_complete.push_back(pair_state_iter(from_state, ite));
pair_state_iter started_ = todo_complete.front(); cycle_path tmp_comp;
todo_complete.pop_front(); while(!todo_complete.empty())
tgba_succ_iterator* iter_s = started_.second; {
iter_s->first(); pair_state_iter started_ = todo_complete.front();
for (iter_s->first(); !iter_s->done(); iter_s->next()) todo_complete.pop_front();
{ tgba_succ_iterator* iter_s = started_.second;
const state* curr_state = (started_.second)->current_state(); iter_s->first();
connected_component::set_of_state::iterator i_set = comp_path.state_set.find(curr_state); for (iter_s->first(); !iter_s->done(); iter_s->next())
if (i_set != comp_path.state_set.end()) {
{ const state* curr_state = (started_.second)->current_state();
if (curr_state->compare(to_state) == 0) connected_component::set_of_state::iterator i_set =
{ comp_path.state_set.find(curr_state);
const state* curr_father = started_.first; if (i_set != comp_path.state_set.end())
bdd curr_condition = iter_s->current_condition(); {
tmp_comp.push_front(state_proposition(curr_state, curr_condition)); if (curr_state->compare(to_state) == 0)
while (curr_father->compare(from_state) != 0) {
{ const state* curr_father = started_.first;
tmp_comp.push_front(state_proposition(curr_father, complete_map[curr_father].second)); bdd curr_condition = iter_s->current_condition();
curr_father = complete_map[curr_father].first; tmp_comp.push_front(state_proposition(curr_state, curr_condition));
} while (curr_father->compare(from_state) != 0)
emptiness_check::periode.splice(periode.end(), tmp_comp); {
todo_complete.clear(); tmp_comp.push_front(state_proposition(curr_father,
break; complete_map[curr_father].second));
} curr_father = complete_map[curr_father].first;
else }
{ emptiness_check::periode.splice(periode.end(),
todo_complete.push_back(pair_state_iter(curr_state, aut_counter->succ_iter(curr_state))); tmp_comp);
complete_map[curr_state] = state_proposition(started_.first, iter_s->current_condition()); todo_complete.clear();
} break;
} }
} else
} {
} todo_complete.push_back(pair_state_iter(curr_state,
} aut_counter->succ_iter(curr_state)));
complete_map[curr_state] =
state_proposition(started_.first,
iter_s->current_condition());
}
}
}
}
}
}
/// \Brief build recursively a path in the accepting SCC to get /// \Brief build recursively a path in the accepting SCC to get
///all accepting conditions. This path is the first part of the /// all accepting conditions. This path is the first part of the
///period. /// period.
void void
emptiness_check::accepting_path(const spot::tgba* aut_counter, const connected_component& comp_path, const spot::state* start_path, bdd to_accept) emptiness_check::accepting_path(const spot::tgba* aut_counter,
const connected_component& comp_path,
const spot::state* start_path, bdd to_accept)
{ {
seen seen_priority; seen seen_priority;
std::stack<triplet> todo_path; std::stack<triplet> todo_path;
@ -447,18 +472,24 @@ void
else else
{ {
state* curr_state = iter_->current_state(); state* curr_state = iter_->current_state();
connected_component::set_of_state::iterator it_set = comp_path.state_set.find(curr_state); connected_component::set_of_state::iterator it_set =
comp_path.state_set.find(curr_state);
if (it_set != comp_path.state_set.end()) if (it_set != comp_path.state_set.end())
{ {
seen::iterator i = seen_priority.find(curr_state); seen::iterator i = seen_priority.find(curr_state);
if (i == seen_priority.end()) if (i == seen_priority.end())
{ {
tgba_succ_iterator* c_iter = aut_counter->succ_iter(curr_state); tgba_succ_iterator* c_iter =
bdd curr_bdd = bdd_apply(iter_->current_accepting_conditions(), step_.second, bddop_or); aut_counter->succ_iter(curr_state);
c_iter->first(); bdd curr_bdd =
todo_path.push(triplet(pair_state_iter(curr_state, c_iter), curr_bdd)); bdd_apply(iter_->current_accepting_conditions(),
tmp_lst.push_back(state_proposition(curr_state, iter_->current_condition())); step_.second, bddop_or);
seen_priority[curr_state] = seen_state_num[curr_state]; c_iter->first();
todo_path.push(triplet(pair_state_iter(curr_state, c_iter),
curr_bdd));
tmp_lst.push_back(state_proposition(curr_state,
iter_->current_condition()));
seen_priority[curr_state] = seen_state_num[curr_state];
} }
else else
{ {
@ -476,16 +507,19 @@ void
{ {
cycle_path tmp(tmp_lst); cycle_path tmp(tmp_lst);
best_lst = tmp; best_lst = tmp;
spot::bdd_print_dot(std::cout, aut_counter->get_dict(),step_.second); spot::bdd_print_dot(std::cout,
aut_counter->get_dict(),
step_.second);
} }
} }
else else
{ {
if (bddtrue == bdd_apply(best_in, curr_in, bddop_imp)) if (bddtrue == bdd_apply(best_in, curr_in,
bddop_imp))
{ {
cycle_path tmp(tmp_lst); cycle_path tmp(tmp_lst);
best_lst = tmp; best_lst = tmp;
best_acc = tmp_acc; best_acc = tmp_acc;
} }
} }
} }
@ -494,7 +528,8 @@ void
bdd last_ = iter_->current_accepting_conditions(); bdd last_ = iter_->current_accepting_conditions();
bdd prop_ = iter_->current_condition(); bdd prop_ = iter_->current_condition();
tmp_acc = bdd_apply(last_, step_.second, bddop_or); tmp_acc = bdd_apply(last_, step_.second, bddop_or);
tmp_lst.push_back(state_proposition(curr_state, prop_)); tmp_lst.push_back(state_proposition(curr_state,
prop_));
cycle_path tmp(tmp_lst); cycle_path tmp(tmp_lst);
best_lst = tmp; best_lst = tmp;
best_acc = tmp_acc; best_acc = tmp_acc;
@ -503,17 +538,17 @@ void
} }
} }
iter_->next(); iter_->next();
} }
} }
for (cycle_path::iterator it = best_lst.begin(); it != best_lst.end(); it++) for (cycle_path::iterator it = best_lst.begin();
{ it != best_lst.end(); it++)
emptiness_check::periode.push_back(*it); emptiness_check::periode.push_back(*it);
}
if (best_acc != to_accept) if (best_acc != to_accept)
{ {
bdd rec_to_acc = bdd_apply(to_accept, !best_acc, bddop_and); bdd rec_to_acc = bdd_apply(to_accept, !best_acc, bddop_and);
emptiness_check::accepting_path(aut_counter, comp_path, periode.back().first, rec_to_acc); emptiness_check::accepting_path(aut_counter, comp_path,
periode.back().first, rec_to_acc);
} }
else else
{ {
@ -522,7 +557,8 @@ void
{ {
/// The path contains all accepting conditions. Then we /// The path contains all accepting conditions. Then we
///complete the cycle in this SCC by calling complete_cycle. ///complete the cycle in this SCC by calling complete_cycle.
complete_cycle(aut_counter, comp_path, periode.back().first, seq_counter.back()); complete_cycle(aut_counter, comp_path, periode.back().first,
seq_counter.back());
} }
} }
} }

133
src/tgbaalgos/emptinesscheck.hh
View file

@ -1,6 +1,5 @@
#ifndef SPOT_EMPTINESS_CHECK_HH #ifndef SPOT_EMPTINESS_CHECK_HH
# define SPOT_EMPTINESS_CHECK_HH # define SPOT_EMPTINESS_CHECK_HH
//#include "tgba/bddfactory.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "tgba/statebdd.hh" #include "tgba/statebdd.hh"
#include "tgba/tgbabddfactory.hh" #include "tgba/tgbabddfactory.hh"
@ -14,31 +13,28 @@
#include <utility> #include <utility>
#include <ostream> #include <ostream>
/// \brief Emptiness check on spot::tgba
namespace spot namespace spot
{ {
class connected_component class connected_component
{ {
/// During the Depth path we keep the connected component that we met. // During the Depth path we keep the connected component that we met.
public: public:
connected_component(); connected_component();
connected_component(int i, bdd a); connected_component(int i, bdd a);
virtual virtual ~connected_component();
~connected_component(); bool isAccepted(tgba* aut);
std::string
to_string_component();
bool
isAccepted(tgba* aut);
public: public:
int index; int index;
/// The bdd condition is the union of all accepting condition of /// The bdd condition is the union of all accepting condition of
/// transitions which connect the states of the connected component. /// transitions which connect the states of the connected component.
bdd condition; bdd condition;
typedef std::set<const spot::state*, spot::state_ptr_less_than> set_of_state; typedef std::set<const spot::state*,
spot::state_ptr_less_than> set_of_state;
/// for the counter example we need to know all the states of the /// for the counter example we need to know all the states of the
///component /// component
set_of_state state_set; set_of_state state_set;
int transition_acc; int transition_acc;
int nb_transition; int nb_transition;
@ -48,99 +44,74 @@ namespace spot
class emptiness_check class emptiness_check
{ {
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter; typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
typedef std::pair<pair_state_iter, bdd> triplet; typedef std::pair<pair_state_iter, bdd> triplet;
typedef std::map <const spot::state*, int, spot::state_ptr_less_than> seen; typedef std::map<const spot::state*, int, spot::state_ptr_less_than> seen;
typedef std::list<const state*> state_sequence; typedef std::list<const state*> state_sequence;
typedef std::pair<const spot::state*, bdd> state_proposition; typedef std::pair<const spot::state*, bdd> state_proposition;
typedef std::list<state_proposition> cycle_path; typedef std::list<state_proposition> cycle_path;
public: public:
virtual
~emptiness_check();
emptiness_check();
/// this function remove all accessible state from a given /// this function remove all accessible state from a given
/// state. In other words, it removes the strongly connected /// state. In other words, it removes the strongly connected
/// component that contents this state. /// component that contents this state.
/// \brief Emptiness check on spot::tgba
/// \brief Emptiness check on spot::tgba
void void
remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete); remove_component(const tgba& aut, seen& state_map,
const spot::state* start_delete);
/// This is based on the following papers. /// This function returns true if the automata's language is empty,
/// \verbatim /// and builds a stack of SCC.
/// @InProceedings{ couvreur.00.lacim, ///
/// author = {Jean-Michel Couvreur}, /// This is based on the following paper.
/// title = {Un point de vue symbolique sur la logique temporelle /// \verbatim
/// lin{\'e}aire}, /// @InProceedings{couvreur.99.fm,
/// booktitle = {Actes du Colloque LaCIM 2000}, /// author = {Jean-Michel Couvreur},
/// month = {August}, /// title = {On-the-fly Verification of Temporal Logic},
/// year = {2000}, /// pages = {253--271},
/// pages = {131--140}, /// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
/// volume = {27}, /// booktitle = {Proceedings of the World Congress on Formal Methods in
/// series = {Publications du LaCIM}, /// the Development of Computing Systems (FM'99)},
/// publisher = {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al}, /// publisher = {Springer-Verlag},
/// editor = {Pierre Leroux} /// series = {Lecture Notes in Computer Science},
/// } /// volume = {1708},
/// \endverbatim /// year = {1999},
/// and /// address = {Toulouse, France},
/// \verbatim /// month = {September},
/// @InProceedings{couvreur.99.fm, /// isbn = {3-540-66587-0}
/// author = {Jean-Michel Couvreur}, /// }
/// title = {On-the-fly Verification of Temporal Logic}, /// \endverbatim
/// pages = {253--271}, bool tgba_emptiness_check(const spot::tgba* aut_check);
/// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
/// booktitle = {Proceedings of the World Congress on Formal Methods in the
/// Development of Computing Systems (FM'99)},
/// publisher = {Springer-Verlag},
/// series = {Lecture Notes in Computer Science},
/// volume = {1708},
/// year = {1999},
/// address = {Toulouse, France},
/// month = {September},
/// isbn = {3-540-66587-0}
/// }
/// \endverbatim
/// This function return true if the automata is empty and build a stack of SCC.
bool
tgba_emptiness_check(const spot::tgba* aut_check);
/// counter_example check if the automata is empty. If it is not, /// Compute a counter example if tgba_emptiness_check() returned false.
///then this function return an accepted word (a trace) and an accepted sequence. void counter_example(const spot::tgba* aut_counter);
void std::ostream& print_result(std::ostream& os, const spot::tgba* aut,
counter_example(const spot::tgba* aut_counter); const tgba* restrict = 0) const;
std::ostream& std::stack<bdd> arc_accepting;
print_result(std::ostream& os, const spot::tgba* aut, const tgba* restrict = 0) const; std::stack<connected_component> root_component;
std::stack <bdd> arc_accepting;
std::stack <connected_component> root_component;
seen seen_state_num; seen seen_state_num;
state_sequence seq_counter; state_sequence seq_counter;
cycle_path periode; cycle_path periode;
private: private:
std::stack <pair_state_iter> todo; std::stack<pair_state_iter> todo;
std::vector<state_sequence> vec_sequence; std::vector<state_sequence> vec_sequence;
/// This function is called by counter_example to find a path
/// which contents all accepting conditions in the accepted SCC (get all the
/// accepting conditions).
/// Called by counter_example to find a path which traverses all
/// accepting conditions in the accepted SCC.
void void
accepting_path (const spot::tgba* aut_counter, const connected_component& comp_path, const spot::state* start_path, bdd to_accept); accepting_path (const spot::tgba* aut_counter,
const connected_component& comp_path,
const spot::state* start_path, bdd to_accept);
/// This function is called by counter_example (after
//accepting_path) to complete the cycle that caraterise the periode
//of the counter example. Append a sequence to the path given by accepting_path.
void
complete_cycle(const spot::tgba* aut_counter, const connected_component& comp_path, const state* from_state,const state* to_state);
/// Complete a cycle that caraterise the period of the counter
/// example. Append a sequence to the path given by accepting_path.
void complete_cycle(const spot::tgba* aut_counter,
const connected_component& comp_path,
const state* from_state,const state* to_state);
}; };
} }
#endif // SPOT_EMPTINESS_CHECK_HH #endif // SPOT_EMPTINESS_CHECK_HH