diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index fd7311412..b1ec3335c 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -2825,6 +2825,37 @@ namespace spot return res; } + acc_cond::mark_t acc_cond::acc_code::inf_unit() const + { + mark_t res = {}; + if (empty() || is_f()) + return res; + const acc_cond::acc_word* pos = &back(); + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + --pos; + break; + case acc_cond::acc_op::Or: + pos -= pos->sub.size + 1; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + pos -= 2; + break; + case acc_cond::acc_op::Inf: + res |= pos[-1].mark; + pos -= 2; + break; + } + } + while (pos >= &front()); + return res; + } + acc_cond::mark_t acc_cond::acc_code::used_once_sets() const { mark_t seen = {}; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index abd85a2b4..684b4b576 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1257,6 +1257,19 @@ namespace spot /// Return -1 if no such set exist. int fin_one() const; + /// \brief Find a `Inf(i)` that is a unit clause. + /// + /// This return a mark_t `{i}` such that `Inf(i)` appears as a + /// unit clause in the acceptance condition. I.e., either the + /// condition is exactly `Inf(i)`, or the condition has the form + /// `...&Inf(i)&...`. If there is no such `Inf(i)`, an empty + /// mark_t is returned. + /// + /// If multiple unit-Inf appear as unit-clauses, the set of + /// those will be returned. For instance applied to + /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. + mark_t inf_unit() const; + /// \brief Help closing accepting or rejecting cycle. /// /// Assuming you have a partial cycle visiting all acceptance @@ -2153,6 +2166,22 @@ namespace spot return code_.fin_one(); } + /// \brief Find a `Inf(i)` that is a unit clause. + /// + /// This return a mark_t `{i}` such that `Inf(i)` appears as a + /// unit clause in the acceptance condition. I.e., either the + /// condition is exactly `Inf(i)`, or the condition has the form + /// `...&Inf(i)&...`. If there is no such `Inf(i)`, an empty + /// mark_t is returned. + /// + /// If multiple unit-Inf appear as unit-clauses, the set of + /// those will be returned. For instance applied to + /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. + mark_t inf_unit() const + { + return code_.inf_unit(); + } + /// \brief Return the top-level disjuncts. /// /// For instance, if the formula is diff --git a/tests/python/setacc.py b/tests/python/setacc.py index 3ccf935cf..8d20b6a49 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -106,3 +106,20 @@ assert acc == spot.acc_cond('Inf(0)') acc = spot.translate('b').get_acceptance() collect() assert acc == spot.acc_code('Inf(0)') + + +c = spot.acc_cond('Fin(0)&Fin(1)&(Inf(2)|Fin(3))') +m1 = c.fin_unit() +m2 = c.inf_unit() +assert m1 == [0,1] +assert m2 == [] +c = spot.acc_cond('Inf(0)&Inf(1)&(Inf(2)|Fin(3))') +m1 = c.fin_unit() +m2 = c.inf_unit() +assert m1 == [] +assert m2 == [0,1] +c = spot.acc_cond('Inf(0)&Inf(1)|(Inf(2)|Fin(3))') +m1 = c.fin_unit() +m2 = c.inf_unit() +assert m1 == [] +assert m2 == []