27 #include <spot/misc/_config.h> 28 #include <spot/misc/bitset.hh> 29 #include <spot/misc/trival.hh> 42 SPOT_DEPRECATED(
"mark_t no longer relies on unsigned, stop using value_t")
43 typedef unsigned value_t;
63 [[noreturn]]
static void report_too_many_sets();
99 template<
class iterator>
101 mark_t(
const iterator& begin,
const iterator& end)
104 for (iterator i = begin; i != end; ++i)
109 mark_t(std::initializer_list<unsigned> vals)
110 :
mark_t(vals.begin(), vals.end())
114 SPOT_DEPRECATED(
"use brace initialization instead")
135 return SPOT_MAX_ACCSETS;
145 return mark_t(_value_t::mone());
148 size_t hash()
const noexcept
150 std::hash<decltype(id)> h;
154 SPOT_DEPRECATED(
"compare mark_t to mark_t, not to unsigned")
155 bool operator==(
unsigned o)
const 157 SPOT_ASSERT(o == 0
U);
162 SPOT_DEPRECATED(
"compare mark_t to mark_t, not to unsigned")
163 bool operator!=(
unsigned o)
const 165 SPOT_ASSERT(o == 0
U);
170 bool operator==(
mark_t o)
const 175 bool operator!=(
mark_t o)
const 180 bool operator<(
mark_t o)
const 185 bool operator<=(
mark_t o)
const 190 bool operator>(
mark_t o)
const 195 bool operator>=(
mark_t o)
const 200 explicit operator bool()
const 205 bool has(
unsigned u)
const 207 return !!this->operator&(
mark_t({0}) << u);
215 void clear(
unsigned u)
269 #if SPOT_DEBUG || defined(SWIGPYTHON) 270 # define SPOT_WRAP_OP(ins) \ 275 catch (const std::runtime_error& e) \ 277 report_too_many_sets(); \ 280 # define SPOT_WRAP_OP(ins) ins; 282 mark_t operator<<(
unsigned i)
const 284 SPOT_WRAP_OP(
return id << i);
287 mark_t& operator<<=(
unsigned i)
289 SPOT_WRAP_OP(
id <<= i;
return *
this);
292 mark_t operator>>(
unsigned i)
const 294 SPOT_WRAP_OP(
return id >> i);
297 mark_t& operator>>=(
unsigned i)
299 SPOT_WRAP_OP(
id >>= i;
return *
this);
317 auto rm = (~yv) & (yv - 1);
319 auto lm = ~(yv ^ (yv - 1));
320 xv = ((xv & lm) >> 1) | (xv & rm);
330 return !((*this) - m);
337 return *
this != m && this->subset(m);
353 return id.highest()+1;
365 return id.lowest()+1;
390 template<
class iterator>
408 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
413 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
444 struct SPOT_API
acc_code:
public std::vector<acc_word>
446 bool operator==(
const acc_code& other)
const 448 unsigned pos = size();
449 if (other.size() != pos)
453 auto op = (*this)[pos - 1].sub.op;
454 auto sz = (*this)[pos - 1].sub.size;
455 if (other[pos - 1].sub.op !=
op ||
456 other[pos - 1].sub.size != sz)
460 case acc_cond::acc_op::And:
461 case acc_cond::acc_op::Or:
464 case acc_cond::acc_op::Inf:
465 case acc_cond::acc_op::InfNeg:
466 case acc_cond::acc_op::Fin:
467 case acc_cond::acc_op::FinNeg:
469 if (other[pos].mark != (*
this)[pos].mark)
477 bool operator<(
const acc_code& other)
const 479 unsigned pos = size();
480 auto osize = other.size();
487 auto op = (*this)[pos - 1].sub.op;
488 auto oop = other[pos - 1].sub.op;
493 auto sz = (*this)[pos - 1].sub.size;
494 auto osz = other[pos - 1].sub.size;
501 case acc_cond::acc_op::And:
502 case acc_cond::acc_op::Or:
505 case acc_cond::acc_op::Inf:
506 case acc_cond::acc_op::InfNeg:
507 case acc_cond::acc_op::Fin:
508 case acc_cond::acc_op::FinNeg:
511 auto m = (*this)[pos].mark;
512 auto om = other[pos].mark;
524 bool operator>(
const acc_code& other)
const 526 return other < *
this;
529 bool operator<=(
const acc_code& other)
const 531 return !(other < *
this);
534 bool operator>=(
const acc_code& other)
const 536 return !(*
this < other);
539 bool operator!=(
const acc_code& other)
const 541 return !(*
this == other);
552 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
553 && !((*this)[s - 2].mark));
567 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
581 res[1].sub.op = acc_op::Fin;
607 res[1].sub.op = acc_op::Fin;
639 res[1].sub.op = acc_op::FinNeg;
646 return fin_neg(
mark_t(vals));
663 res[1].sub.op = acc_op::Inf;
695 res[1].sub.op = acc_op::InfNeg;
702 return inf_neg(
mark_t(vals));
732 m >>= mark_t::max_accsets() - n;
746 m >>= mark_t::max_accsets() - n;
759 res |= inf({2*n - 1}) & fin({2*n - 2});
774 res &= inf({2*n - 1}) | fin({2*n - 2});
792 template<
class Iterator>
797 for (Iterator i = begin; i != end; ++i)
801 for (
unsigned ni = *i; ni > 0; --ni)
803 auto pair = inf(m) & fin({f});
804 std::swap(pair, res);
805 res |= std::move(pair);
816 static acc_code parity(
bool max,
bool odd,
unsigned sets);
834 static acc_code random(
unsigned n,
double reuse = 0.0);
839 if (is_t() || r.
is_f())
844 if (is_f() || r.
is_t())
846 unsigned s = size() - 1;
847 unsigned rs = r.size() - 1;
850 if (((*
this)[s].sub.op == acc_op::Inf
851 && r[rs].sub.op == acc_op::Inf)
852 || ((*
this)[s].sub.op == acc_op::InfNeg
853 && r[rs].sub.op == acc_op::InfNeg))
855 (*this)[s - 1].mark |= r[rs - 1].mark;
867 auto start = &(*this)[s] - (*this)[s].sub.size;
868 auto pos = &(*this)[s] - 1;
872 if (pos->sub.op == acc_op::Inf)
877 pos -= pos->sub.size + 1;
880 else if ((*
this)[s].sub.op == acc_op::Inf)
882 left_inf = &(*this)[s - 1];
885 const acc_word* right_inf =
nullptr;
886 auto right_end = &r.back();
890 auto pos = --right_end;
893 if (pos->sub.op == acc_op::Inf)
898 pos -= pos->sub.size + 1;
901 else if (right_end->sub.op == acc_op::Inf)
903 right_inf = right_end - 1;
907 if (left_inf && right_inf)
909 carry = left_inf->mark;
910 auto pos = left_inf - &(*this)[0];
911 erase(begin() + pos, begin() + pos + 2);
914 insert(end(), &r[0], right_end + 1);
916 (*this)[sz + (right_inf - &r[0])].mark |= carry;
944 if (is_t() || r.
is_f())
946 if (is_f() || r.
is_t())
951 unsigned s = size() - 1;
952 unsigned rs = r.size() - 1;
954 if (((*
this)[s].sub.op == acc_op::Fin
955 && r[rs].sub.op == acc_op::Fin)
956 || ((*
this)[s].sub.op == acc_op::FinNeg
957 && r[rs].sub.op == acc_op::FinNeg))
959 (*this)[s - 1].mark |= r[rs - 1].mark;
971 auto start = &(*this)[s] - (*this)[s].sub.size;
972 auto pos = &(*this)[s] - 1;
976 if (pos->sub.op == acc_op::Fin)
981 pos -= pos->sub.size + 1;
984 else if ((*
this)[s].sub.op == acc_op::Fin)
986 left_fin = &(*this)[s - 1];
989 const acc_word* right_fin =
nullptr;
990 auto right_end = &r.back();
994 auto pos = --right_end;
997 if (pos->sub.op == acc_op::Fin)
1002 pos -= pos->sub.size + 1;
1005 else if (right_end->sub.op == acc_op::Fin)
1007 right_fin = right_end - 1;
1011 if (left_fin && right_fin)
1013 carry = left_fin->mark;
1014 auto pos = (left_fin - &(*this)[0]);
1015 this->erase(begin() + pos, begin() + pos + 2);
1018 insert(end(), &r[0], right_end + 1);
1020 (*this)[sz + (right_fin - &r[0])].mark |= carry;
1023 w.sub.size = size();
1051 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1052 report_too_many_sets();
1055 unsigned pos = size();
1058 switch ((*
this)[pos - 1].sub.op)
1060 case acc_cond::acc_op::And:
1061 case acc_cond::acc_op::Or:
1064 case acc_cond::acc_op::Inf:
1065 case acc_cond::acc_op::InfNeg:
1066 case acc_cond::acc_op::Fin:
1067 case acc_cond::acc_op::FinNeg:
1069 (*this)[pos].mark <<= sets;
1093 bool is_dnf()
const;
1101 bool is_cnf()
const;
1152 int fin_one()
const;
1166 std::vector<std::vector<int>>
1167 missing(
mark_t inf,
bool accepting)
const;
1171 bool accepting(
mark_t inf)
const;
1178 bool inf_satisfiable(
mark_t inf)
const;
1192 mark_t always_present)
const;
1204 std::vector<unsigned> symmetries()
const;
1233 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets()
const;
1240 to_html(std::ostream& os,
1241 std::function<
void(std::ostream&,
int)>
1242 set_printer =
nullptr)
const;
1249 to_text(std::ostream& os,
1250 std::function<
void(std::ostream&,
int)>
1251 set_printer =
nullptr)
const;
1258 to_latex(std::ostream& os,
1259 std::function<
void(std::ostream&,
int)>
1260 set_printer =
nullptr)
const;
1295 :
std::vector<
acc_word>(other - other->sub.size, other + 1)
1301 friend std::ostream& operator<<(std::ostream& os,
const acc_code& code);
1312 : num_(0
U), all_({}), code_(code)
1315 uses_fin_acceptance_ = check_fin_acceptance();
1323 : num_(0
U), all_({}), code_(code)
1325 add_sets(code.used_sets().max_set());
1326 uses_fin_acceptance_ = check_fin_acceptance();
1331 : num_(o.num_), all_(o.all_), code_(o.code_),
1332 uses_fin_acceptance_(o.uses_fin_acceptance_)
1342 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1356 uses_fin_acceptance_ = check_fin_acceptance();
1371 bool operator==(
const acc_cond& other)
const 1376 bool operator!=(
const acc_cond& other)
const 1378 return !(*
this == other);
1384 return uses_fin_acceptance_;
1390 return code_.is_t();
1399 return num_ == 0 && is_t();
1405 return code_.is_f();
1414 return num_ == 0 && is_f();
1423 unsigned s = code_.size();
1425 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1434 return num_ == 1 && is_generalized_co_buchi();
1441 set_acceptance(inf(all_sets()));
1448 set_acceptance(fin(all_sets()));
1457 unsigned s = code_.size();
1458 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1459 && code_[0].mark == all_sets());
1468 unsigned s = code_.size();
1470 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1484 int is_rabin()
const;
1497 int is_streett()
const;
1522 bool operator==(
rs_pair o)
const 1524 return fin == o.fin && inf == o.inf;
1526 bool operator!=(
rs_pair o)
const 1528 return fin != o.fin || inf != o.inf;
1530 bool operator<(
rs_pair o)
const 1532 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1534 bool operator<=(
rs_pair o)
const 1536 return !(o < *
this);
1538 bool operator>(
rs_pair o)
const 1542 bool operator>=(
rs_pair o)
const 1544 return !(*
this < o);
1557 bool is_streett_like(std::vector<rs_pair>& pairs)
const;
1569 bool is_rabin_like(std::vector<rs_pair>& pairs)
const;
1580 bool is_generalized_rabin(std::vector<unsigned>& pairs)
const;
1594 bool is_generalized_streett(std::vector<unsigned>& pairs)
const;
1605 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1613 return is_parity(max, odd);
1619 std::pair<bool, acc_cond::mark_t> unsat_mark()
const 1621 return sat_unsat_mark(
false);
1626 std::pair<bool, acc_cond::mark_t> sat_mark()
const 1628 return sat_unsat_mark(
true);
1632 bool check_fin_acceptance()
const;
1633 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(
bool)
const;
1646 return acc_code::inf(mark);
1651 return inf(
mark_t(vals.begin(), vals.end()));
1673 return acc_code::inf_neg(mark);
1678 return inf_neg(
mark_t(vals.begin(), vals.end()));
1691 return acc_code::fin(mark);
1696 return fin(
mark_t(vals.begin(), vals.end()));
1718 return acc_code::fin_neg(mark);
1723 return fin_neg(
mark_t(vals.begin(), vals.end()));
1737 if (num > mark_t::max_accsets())
1738 report_too_many_sets();
1757 SPOT_ASSERT(u < num_sets());
1780 return code_.accepting(inf);
1790 return code_.inf_satisfiable(inf);
1806 return code_.maybe_accepting(infinitely_often, always_present);
1825 std::ostream& format(std::ostream& os,
mark_t m)
const 1834 std::string format(
mark_t m)
const 1836 std::ostringstream os;
1854 template<
class iterator>
1858 for (
unsigned x = 0; x < num_; ++x)
1863 auto all = comp(u |
mark_t({x}));
1866 for (iterator y = begin; y != end; ++y)
1896 return {num_sets(), code_.
remove(rem, missing)};
1906 { num_sets() - (all_sets() & rem).count(), code_.
strip(rem, missing) };
1912 return {num_sets(), code_.
force_inf(m)};
1919 return {num_sets(), code_.
remove(all_sets() - rem,
true)};
1933 std::string name(
const char* fmt =
"alo")
const;
1948 return code_.fin_unit();
1957 return code_.fin_one();
1969 bool uses_fin_acceptance_ =
false;
1974 typedef std::vector<acc_cond::rs_pair> rs_pairs;
1978 : pairs_(p), view_marks_(m) {}
2004 return !visible(p.inf) && visible(p.fin) ? p.fin
2013 return !visible(p.fin) && visible(p.inf) ? p.inf
2021 for (
const auto& p: pairs_)
2022 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2027 const rs_pairs& pairs()
const 2033 template<
typename filter>
2037 for (
const auto& p: pairs_)
2044 return !!(view_marks_ & v);
2047 const rs_pairs& pairs_;
2053 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
2062 typedef unsigned value_type;
2063 typedef const value_type& reference;
2064 typedef const value_type* pointer;
2065 typedef std::ptrdiff_t difference_type;
2066 typedef std::forward_iterator_tag iterator_category;
2088 value_type operator*()
const 2091 return m_.min_set() - 1;
2096 m_.clear(this->
operator*());
2140 struct hash<
spot::acc_cond::mark_t>
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:658
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:133
Definition: automata.hh:26
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:362
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:374
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1397
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1771
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2131
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1689
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:1910
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1403
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:562
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
Definition: acc.hh:1788
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1421
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1731
acc_op
Operators for acceptance formulas.
Definition: acc.hh:412
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1721
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1755
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:350
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1382
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1508
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:391
const acc_code & get_acceptance() const
Retrieve teh acceptance formula.
Definition: acc.hh:1360
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:576
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1644
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:101
Definition: bitset.hh:405
acc_cond restrict_to(mark_t rem) const
Restrict an acceptance condition to a subset of set numbers that are occurring at some point...
Definition: acc.hh:1917
bool subset(mark_t m) const
Whether the set of bits represented by *this is a subset of those represented by m.
Definition: acc.hh:328
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1694
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:143
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1080
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:769
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1455
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1353
bool proper_subset(mark_t m) const
Whether the set of bits represented by *this is a proper subset of those represented by m...
Definition: acc.hh:335
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1716
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1029
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1294
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1671
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:1894
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:382
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1412
An acceptance condition.
Definition: acc.hh:58
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:1903
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1337
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1311
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:109
A "node" in an acceptance formulas.
Definition: acc.hh:422
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:942
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:668
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1446
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:612
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:1955
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:709
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1676
acc_code & get_acceptance()
Retrieve teh acceptance formula.
Definition: acc.hh:1366
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1432
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1765
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:590
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:717
unsigned count() const
Number of bits sets.
Definition: acc.hh:341
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:690
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1289
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1466
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:1946
op
Operator types.
Definition: formula.hh:64
bool is_parity() const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
Definition: acc.hh:1609
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1049
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:1842
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1649
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:727
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1330
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1037
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:754
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1749
An acceptance formulas.
Definition: acc.hh:444
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:602
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:793
mark_t useless(iterator begin, iterator end) const
Compute useless acceptance sets given a list of mark_t that occur in an SCC.
Definition: acc.hh:1855
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1322
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition...
Definition: acc.hh:1778
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1388
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:1804
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1439
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:634
An acceptance mark.
Definition: acc.hh:81
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:700
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:644
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:741
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:548