* src/tgbaalgos/emptinesscheck.cc
(emptiness_check::tgba_emptiness_check): Do not print anything. (emptiness_check::counter_example): Assume that tgba_emptiness_check has already been called.
This commit is contained in:
Alexandre Duret-Lutz
parent
93c0732f0e
commit
a11a29a1f7
2 changed files with 117 additions and 127 deletions
|
|
@ -170,11 +170,8 @@ namespace spot
|
|||
comp.condition |= new_condition;
|
||||
if (aut_check->all_accepting_conditions() == comp.condition)
|
||||
{
|
||||
// A failure SCC is find, the automata is not empty.
|
||||
// spot::bdd_print_dot(std::cout, aut_check->get_dict(),
|
||||
// comp.condition);
|
||||
// A failure SCC was found, the automata is not empty.
|
||||
root_component.push(comp);
|
||||
std::cout << "CONSISTENT AUTOMATA" << std::endl;
|
||||
return false;
|
||||
}
|
||||
root_component.push(comp);
|
||||
|
|
@ -183,7 +180,6 @@ namespace spot
|
|||
}
|
||||
}
|
||||
// The automata is empty.
|
||||
std::cout << "EMPTY LANGUAGE" << std::endl;
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -197,7 +193,7 @@ namespace spot
|
|||
os << "======================" << std::endl;
|
||||
const bdd_dict* d = aut->get_dict();
|
||||
for (state_sequence::const_iterator i_se = suffix.begin();
|
||||
i_se != suffix.end(); i_se++)
|
||||
i_se != suffix.end(); ++i_se)
|
||||
{
|
||||
if (restrict)
|
||||
{
|
||||
|
|
@ -213,7 +209,7 @@ namespace spot
|
|||
os << "Cycle:" <<std::endl;
|
||||
os << "======================" << std::endl;
|
||||
for (cycle_path::const_iterator it = period.begin();
|
||||
it != period.end(); it++)
|
||||
it != period.end(); ++it)
|
||||
{
|
||||
if (restrict)
|
||||
{
|
||||
|
|
@ -240,144 +236,134 @@ namespace spot
|
|||
spot::state_ptr_less_than> path_state;
|
||||
path_state path_map;
|
||||
|
||||
if (!root_component.empty())
|
||||
assert(!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--)
|
||||
{
|
||||
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;
|
||||
vec_component[j] = root_component.top();
|
||||
root_component.pop();
|
||||
}
|
||||
|
||||
for (int j = comp_size -1; j >= 0; j--)
|
||||
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)
|
||||
{
|
||||
vec_component[j] = root_component.top();
|
||||
root_component.pop();
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
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++)
|
||||
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)
|
||||
{
|
||||
q_index = (*iter_map).second;
|
||||
tmp_int = 0;
|
||||
if (q_index > 0)
|
||||
// We build a path trought all SCC in the stack: a
|
||||
// possible prefix for a counter example.
|
||||
while (!todo_trace.empty())
|
||||
{
|
||||
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);
|
||||
}
|
||||
}
|
||||
pair_state_iter started_from = todo_trace.front();
|
||||
todo_trace.pop_front();
|
||||
started_from.second->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 prefix for a counter example.
|
||||
while (!todo_trace.empty())
|
||||
for (started_from.second->first();
|
||||
!started_from.second->done();
|
||||
started_from.second->next())
|
||||
{
|
||||
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_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))
|
||||
{
|
||||
const state* curr_father = started_from.first;
|
||||
seq.push_front(*iter_set);
|
||||
seq.push_front(curr_father);
|
||||
seen::iterator i_2 =
|
||||
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_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;
|
||||
assert(i_3 != seen_state_num.end());
|
||||
}
|
||||
else
|
||||
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())
|
||||
{
|
||||
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);
|
||||
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;
|
||||
}
|
||||
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())));
|
||||
}
|
||||
todo_trace.
|
||||
push_back(pair_state_iter(vec_sequence[k].back(),
|
||||
aut_counter->succ_iter(vec_sequence[k].back())));
|
||||
}
|
||||
else
|
||||
{
|
||||
suffix.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++)
|
||||
{
|
||||
suffix.push_back(*it);
|
||||
}
|
||||
}
|
||||
suffix.unique();
|
||||
emptiness_check::accepting_path(aut_counter,
|
||||
vec_component[comp_size-1],
|
||||
suffix.back(),
|
||||
vec_component[comp_size-1].condition);
|
||||
}
|
||||
else
|
||||
{
|
||||
std::cout << "EMPTY LANGUAGE NO COUNTER EXEMPLE" << std::endl;
|
||||
suffix.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)
|
||||
suffix.push_back(*it);
|
||||
suffix.unique();
|
||||
emptiness_check::accepting_path(aut_counter,
|
||||
vec_component[comp_size - 1],
|
||||
suffix.back(),
|
||||
vec_component[comp_size - 1].condition);
|
||||
}
|
||||
|
||||
/// \brief complete the path build by accepting_path to get the period.
|
||||
|
|
@ -450,7 +436,7 @@ namespace spot
|
|||
std::stack<triplet> todo_path;
|
||||
tgba_succ_iterator* t_s_i = aut_counter->succ_iter(start_path);
|
||||
t_s_i->first();
|
||||
todo_path.push(triplet(pair_state_iter(start_path,t_s_i), bddfalse));
|
||||
todo_path.push(triplet(pair_state_iter(start_path, t_s_i), bddfalse));
|
||||
bdd tmp_acc = bddfalse;
|
||||
bdd best_acc = bddfalse;
|
||||
cycle_path tmp_lst;
|
||||
|
|
@ -460,11 +446,11 @@ namespace spot
|
|||
while (!todo_path.empty())
|
||||
{
|
||||
triplet step_ = todo_path.top();
|
||||
tgba_succ_iterator* iter_ = (step_.first).second;
|
||||
tgba_succ_iterator* iter_ = step_.first.second;
|
||||
if (iter_->done())
|
||||
{
|
||||
todo_path.pop();
|
||||
seen_priority.erase((step_.first).first);
|
||||
seen_priority.erase(step_.first.first);
|
||||
tmp_lst.pop_back();
|
||||
}
|
||||
else
|
||||
|
|
@ -504,9 +490,6 @@ namespace spot
|
|||
{
|
||||
cycle_path tmp(tmp_lst);
|
||||
best_lst = tmp;
|
||||
spot::bdd_print_dot(std::cout,
|
||||
aut_counter->get_dict(),
|
||||
step_.second);
|
||||
}
|
||||
}
|
||||
else
|
||||
|
|
@ -537,7 +520,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
for (cycle_path::iterator it = best_lst.begin();
|
||||
it != best_lst.end(); it++)
|
||||
it != best_lst.end(); ++it)
|
||||
emptiness_check::period.push_back(*it);
|
||||
|
||||
if (best_acc != to_accept)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue