Set is_accepting_state to false in GTA
* src/taalgos/tgba2ta.cc: Set is_accepting_state to false in GTA. * src/tgbatest/ltl2tgba.cc: Call tgta_explicit.get_ta() to avoid segfault.
This commit is contained in:
parent
941cb0b57b
commit
e30b92327a
2 changed files with 34 additions and 1 deletions
|
|
@ -604,6 +604,39 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
||||||
// build ta automata:
|
// build ta automata:
|
||||||
build_ta(ta, atomic_propositions_set_, degeneralized,
|
build_ta(ta, atomic_propositions_set_, degeneralized,
|
||||||
single_pass_emptiness_check, artificial_livelock_state_mode);
|
single_pass_emptiness_check, artificial_livelock_state_mode);
|
||||||
|
|
||||||
|
// (degeneralized=true) => TA
|
||||||
|
if (degeneralized)
|
||||||
|
return ta;
|
||||||
|
|
||||||
|
// (degeneralized=false) => GTA
|
||||||
|
// adapt a GTA to remove acceptance conditions from states
|
||||||
|
ta::states_set_t states_set = ta->get_states_set();
|
||||||
|
ta::states_set_t::iterator it;
|
||||||
|
for (it = states_set.begin(); it != states_set.end(); it++)
|
||||||
|
{
|
||||||
|
state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);
|
||||||
|
|
||||||
|
if (state->is_accepting_state())
|
||||||
|
{
|
||||||
|
|
||||||
|
state_ta_explicit::transitions* trans = state->get_transitions();
|
||||||
|
state_ta_explicit::transitions::iterator it_trans;
|
||||||
|
|
||||||
|
for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++)
|
||||||
|
{
|
||||||
|
(*it_trans)->acceptance_conditions
|
||||||
|
= ta->all_acceptance_conditions();
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
state->set_accepting_state(false);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
return ta;
|
return ta;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1174,7 +1174,7 @@ main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
case 0:
|
case 0:
|
||||||
spot::dotty_reachable(std::cout,
|
spot::dotty_reachable(std::cout,
|
||||||
dynamic_cast<spot::ta*>(a));
|
dynamic_cast<spot::tgta_explicit*>(a)->get_ta());
|
||||||
break;
|
break;
|
||||||
case 12:
|
case 12:
|
||||||
stats_reachable(a).dump(std::cout);
|
stats_reachable(a).dump(std::cout);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue