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

Post-rebase fixup.

Browse source 
* src/taalgos/tgba2ta.cc: Adjust to use the sba base class.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-24 13:05:29 +02:00
parent 67bbe6a6c7
commit 2462a3d570
1 changed files with 16 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/taalgos/tgba2ta.cc
View file

@ -31,7 +31,7 @@
#include "ltlast/atomic_prop.hh" #include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "tgba/tgbatba.hh" #include "tgba/sba.hh"
#include "misc/bddop.hh" #include "misc/bddop.hh"
#include <cassert> #include <cassert>
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
@ -451,6 +451,8 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
std::stack<state_ta_explicit*> todo; std::stack<state_ta_explicit*> todo;
const tgba* tgba_ = ta->get_tgba(); const tgba* tgba_ = ta->get_tgba();
const sba* sba_ = down_cast<const sba*>(tgba_);
assert(!degeneralized || sba_);
// build Initial states set: // build Initial states set:
state* tgba_init_state = tgba_->get_init_state(); state* tgba_init_state = tgba_->get_init_state();
@ -465,10 +467,10 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit* init_state; state_ta_explicit* init_state;
if (degeneralized) if (degeneralized)
{ {
init_state = new state_ta_explicit(tgba_init_state->clone(), init_state =
satone_tgba_condition, true, new state_ta_explicit(tgba_init_state->clone(),
((const tgba_sba_proxy*) tgba_)->state_is_accepting( satone_tgba_condition, true,
tgba_init_state)); sba_->state_is_accepting(tgba_init_state));
} }
else else
{ {
@ -513,22 +515,18 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
all_props -= dest_condition; all_props -= dest_condition;
state_ta_explicit* new_dest; state_ta_explicit* new_dest;
if (degeneralized) if (degeneralized)
{ {
new_dest = new state_ta_explicit
(tgba_state->clone(),
dest_condition,
false,
sba_->state_is_accepting(tgba_state));
new_dest }
= new state_ta_explicit(
tgba_state->clone(),
dest_condition,
false,
((const tgba_sba_proxy*) tgba_)->state_is_accepting(
tgba_state));
}
else else
{ {
new_dest = new state_ta_explicit(tgba_state->clone(), new_dest = new state_ta_explicit
dest_condition, false, false); (tgba_state->clone(), dest_condition, false, false);
} }
state_ta_explicit* dest = ta->add_state(new_dest); state_ta_explicit* dest = ta->add_state(new_dest);