diff --git a/src/tgbaalgos/totgba.cc b/src/tgbaalgos/totgba.cc index 3b54195f3..210c08b45 100644 --- a/src/tgbaalgos/totgba.cc +++ b/src/tgbaalgos/totgba.cc @@ -68,13 +68,28 @@ namespace spot auto cnf = res->get_acceptance().to_cnf(); // If we are very lucky, building a CNF actually gave us a GBA... if (cnf.empty() || - (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin)) + (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Inf)) { res->set_acceptance(res->acc().num_sets(), cnf); cleanup_acceptance_here(res); return res; } + // Handle false specifically. We want the output + // an automaton with Acceptance: t, that has a single + // state without successor. + if (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin) + { + assert(cnf.front().mark == 0U); + res = make_tgba_digraph(aut->get_dict()); + res->set_init_state(res->new_state()); + res->prop_state_based_acc(); + res->prop_inherently_weak(); + res->prop_deterministic(); + res->prop_stutter_invariant(); + return res; + } + auto terms = cnf_terms(cnf); unsigned nterms = terms.size(); assert(nterms > 0); diff --git a/src/tgbatest/remfin.test b/src/tgbatest/remfin.test index da241d870..3748f0405 100755 --- a/src/tgbatest/remfin.test +++ b/src/tgbatest/remfin.test @@ -385,8 +385,10 @@ HOA: v1 States: 1 Start: 0 AP: 0 -Acceptance: 0 f +acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant inherently-weak --BODY-- State: 0 --END--