diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 674da38a0..b09e5831b 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -711,7 +711,7 @@ namespace spot if (st->successors.empty()) return false; return (st->successors.front().acceptance_conditions - == this->all_acceptance_conditions_); + == this->all_acceptance_conditions()); } private: diff --git a/src/tgbatest/explicit2.cc b/src/tgbatest/explicit2.cc index 3d7b526ed..5a5f75022 100644 --- a/src/tgbatest/explicit2.cc +++ b/src/tgbatest/explicit2.cc @@ -107,17 +107,19 @@ void create_sba_explicit_string(bdd_dict* d) sba_explicit* sba = new sba_explicit(d); + ltl::formula* acc = ltl::constant::true_instance(); + sba->declare_acceptance_condition(acc); + state_explicit_string* s1 = sba->add_state("STATE1"); state_explicit_string* s2 = sba->add_state("STATE2"); state_explicit_string* s3 = sba->add_state("STATE3"); - int v = d->register_acceptance_variable(ltl::constant::true_instance(), sba); - state_explicit_string::transition* t = sba->create_transition(s1, s2); + sba->add_acceptance_condition(t, acc); t = sba->create_transition(s1, s3); - sba->add_acceptance_conditions(t, bdd_ithvar(v)); + sba->add_acceptance_condition(t, acc); std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; @@ -131,15 +133,14 @@ void create_sba_explicit_number(bdd_dict* d) sba_explicit* sba = new sba_explicit(d); + ltl::formula* acc = ltl::constant::true_instance(); + sba->declare_acceptance_condition(acc); + state_explicit_number* s1 = sba->add_state(1); state_explicit_number* s2 = sba->add_state(2); - //state 1 is accepting - int v = d->register_acceptance_variable(ltl::constant::true_instance(), sba); - - state_explicit_number::transition* t = - sba->create_transition(s1, s2); - sba->add_acceptance_conditions(t, bdd_ithvar(v)); + state_explicit_number::transition* t = sba->create_transition(s1, s2); + sba->add_acceptance_condition(t, acc); std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; @@ -153,19 +154,18 @@ create_sba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) sba_explicit* sba = new sba_explicit(d); + ltl::formula* acc = ltl::constant::true_instance(); + sba->declare_acceptance_condition(acc); + state_explicit_formula* s1 = sba->add_state(e.require("a")); state_explicit_formula* s2 = sba->add_state(e.require("b")); state_explicit_formula* s3 = sba->add_state(e.require("c")); - int v = d->register_acceptance_variable(ltl::constant::true_instance(), sba); - - state_explicit_formula::transition* t = - sba->create_transition(s1, s2); - - sba->add_acceptance_conditions(t, bdd_ithvar(v)); + state_explicit_formula::transition* t = sba->create_transition(s1, s2); + sba->add_acceptance_condition(t, acc); t = sba->create_transition(s1, s3); - sba->add_acceptance_conditions(t, bdd_ithvar(v)); + sba->add_acceptance_condition(t, acc); std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; @@ -193,7 +193,7 @@ main(int argc, char** argv) create_tgba_explicit_formula(d, e); //check sba creation - std::cout << "* SBA explicit string, no accepting state" << std::endl; + std::cout << "* SBA explicit string, 1 accepting state" << std::endl; create_sba_explicit_string(d); std::cout << "* SBA explicit number, 1 accepting state" << std::endl; create_sba_explicit_number(d); diff --git a/src/tgbatest/explicit2.test b/src/tgbatest/explicit2.test index 6fcd7ad06..6025a84f9 100755 --- a/src/tgbatest/explicit2.test +++ b/src/tgbatest/explicit2.test @@ -30,8 +30,8 @@ tata 69 * TGBA explicit formula b -* SBA explicit string, no accepting state -S1 ACCEPTING? 0 +* SBA explicit string, 1 accepting state +S1 ACCEPTING? 1 S2 ACCEPTING? 0 S3 ACCEPTING? 0 * SBA explicit number, 1 accepting state