totgba: fix conversion of false acceptance
* src/tgbaalgos/totgba.cc: false must become true... * src/tgbatest/remfin.test: adjust.
This commit is contained in:
parent
e589e208bd
commit
57b0586400
2 changed files with 19 additions and 2 deletions
|
|
@ -68,13 +68,28 @@ namespace spot
|
||||||
auto cnf = res->get_acceptance().to_cnf();
|
auto cnf = res->get_acceptance().to_cnf();
|
||||||
// If we are very lucky, building a CNF actually gave us a GBA...
|
// If we are very lucky, building a CNF actually gave us a GBA...
|
||||||
if (cnf.empty() ||
|
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);
|
res->set_acceptance(res->acc().num_sets(), cnf);
|
||||||
cleanup_acceptance_here(res);
|
cleanup_acceptance_here(res);
|
||||||
return 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);
|
auto terms = cnf_terms(cnf);
|
||||||
unsigned nterms = terms.size();
|
unsigned nterms = terms.size();
|
||||||
assert(nterms > 0);
|
assert(nterms > 0);
|
||||||
|
|
|
||||||
|
|
@ -385,8 +385,10 @@ HOA: v1
|
||||||
States: 1
|
States: 1
|
||||||
Start: 0
|
Start: 0
|
||||||
AP: 0
|
AP: 0
|
||||||
Acceptance: 0 f
|
acc-name: all
|
||||||
|
Acceptance: 0 t
|
||||||
properties: trans-labels explicit-labels state-acc deterministic
|
properties: trans-labels explicit-labels state-acc deterministic
|
||||||
|
properties: stutter-invariant inherently-weak
|
||||||
--BODY--
|
--BODY--
|
||||||
State: 0
|
State: 0
|
||||||
--END--
|
--END--
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue