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;
52 [[noreturn]]
static void report_too_many_sets();
72 template<
class iterator>
73 mark_t(
const iterator& begin,
const iterator& end)
76 for (iterator i = begin; i != end; ++i)
80 mark_t(std::initializer_list<unsigned> vals)
81 :
mark_t(vals.begin(), vals.end())
85 SPOT_DEPRECATED(
"use brace initialization instead")
106 return SPOT_MAX_ACCSETS;
111 return mark_t(_value_t::mone());
114 size_t hash()
const noexcept
116 std::hash<decltype(id)> h;
120 SPOT_DEPRECATED(
"compare mark_t to mark_t, not to unsigned")
121 bool operator==(
unsigned o)
const 123 SPOT_ASSERT(o == 0
U);
128 SPOT_DEPRECATED(
"compare mark_t to mark_t, not to unsigned")
129 bool operator!=(
unsigned o)
const 131 SPOT_ASSERT(o == 0
U);
136 bool operator==(
mark_t o)
const 141 bool operator!=(
mark_t o)
const 146 bool operator<(
mark_t o)
const 151 bool operator<=(
mark_t o)
const 156 bool operator>(
mark_t o)
const 161 bool operator>=(
mark_t o)
const 166 explicit operator bool()
const 171 bool has(
unsigned u)
const 173 return !!this->operator&(
mark_t({0}) << u);
181 void clear(
unsigned u)
235 #if SPOT_DEBUG || defined(SWIGPYTHON) 236 # define SPOT_WRAP_OP(ins) \ 241 catch (const std::runtime_error& e) \ 243 report_too_many_sets(); \ 246 # define SPOT_WRAP_OP(ins) ins; 248 mark_t operator<<(
unsigned i)
const 250 SPOT_WRAP_OP(
return id << i);
253 mark_t& operator<<=(
unsigned i)
255 SPOT_WRAP_OP(
id <<= i;
return *
this);
258 mark_t operator>>(
unsigned i)
const 260 SPOT_WRAP_OP(
return id >> i);
263 mark_t& operator>>=(
unsigned i)
265 SPOT_WRAP_OP(
id >>= i;
return *
this);
283 auto rm = (~yv) & (yv - 1);
285 auto lm = ~(yv ^ (yv - 1));
286 xv = ((xv & lm) >> 1) | (xv & rm);
292 bool subset(
mark_t m)
const 294 return !((*this) - m);
297 bool proper_subset(
mark_t m)
const 299 return *
this != m && this->subset(m);
303 unsigned count()
const 311 unsigned max_set()
const 314 return id.highest()+1;
322 unsigned min_set()
const 325 return id.lowest()+1;
337 mark_t& remove_some(
unsigned n)
344 template<
class iterator>
345 void fill(iterator here)
const 362 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
366 enum class acc_op : unsigned short
367 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
378 struct SPOT_API
acc_code:
public std::vector<acc_word>
380 bool operator==(
const acc_code& other)
const 382 unsigned pos = size();
383 if (other.size() != pos)
387 auto op = (*this)[pos - 1].sub.op;
388 auto sz = (*this)[pos - 1].sub.size;
389 if (other[pos - 1].sub.op !=
op ||
390 other[pos - 1].sub.size != sz)
394 case acc_cond::acc_op::And:
395 case acc_cond::acc_op::Or:
398 case acc_cond::acc_op::Inf:
399 case acc_cond::acc_op::InfNeg:
400 case acc_cond::acc_op::Fin:
401 case acc_cond::acc_op::FinNeg:
403 if (other[pos].mark != (*
this)[pos].mark)
411 bool operator<(
const acc_code& other)
const 413 unsigned pos = size();
414 auto osize = other.size();
421 auto op = (*this)[pos - 1].sub.op;
422 auto oop = other[pos - 1].sub.op;
427 auto sz = (*this)[pos - 1].sub.size;
428 auto osz = other[pos - 1].sub.size;
435 case acc_cond::acc_op::And:
436 case acc_cond::acc_op::Or:
439 case acc_cond::acc_op::Inf:
440 case acc_cond::acc_op::InfNeg:
441 case acc_cond::acc_op::Fin:
442 case acc_cond::acc_op::FinNeg:
445 auto m = (*this)[pos].mark;
446 auto om = other[pos].mark;
458 bool operator>(
const acc_code& other)
const 460 return other < *
this;
463 bool operator<=(
const acc_code& other)
const 465 return !(other < *
this);
468 bool operator>=(
const acc_code& other)
const 470 return !(*
this < other);
473 bool operator!=(
const acc_code& other)
const 475 return !(*
this == other);
481 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
482 && !((*this)[s - 2].mark));
489 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
497 res[1].sub.op = acc_op::Fin;
512 res[1].sub.op = acc_op::Fin;
517 static acc_code fin(std::initializer_list<unsigned> vals)
527 res[1].sub.op = acc_op::FinNeg;
532 static acc_code fin_neg(std::initializer_list<unsigned> vals)
534 return fin_neg(
mark_t(vals));
542 res[1].sub.op = acc_op::Inf;
547 static acc_code inf(std::initializer_list<unsigned> vals)
557 res[1].sub.op = acc_op::InfNeg;
562 static acc_code inf_neg(std::initializer_list<unsigned> vals)
564 return inf_neg(
mark_t(vals));
577 static acc_code generalized_buchi(
unsigned n)
582 m >>= mark_t::max_accsets() - n;
586 static acc_code generalized_co_buchi(
unsigned n)
591 m >>= mark_t::max_accsets() - n;
601 res |= inf({2*n - 1}) & fin({2*n - 2});
613 res &= inf({2*n - 1}) | fin({2*n - 2});
619 template<
class Iterator>
620 static acc_code generalized_rabin(Iterator begin, Iterator end)
624 for (Iterator i = begin; i != end; ++i)
628 for (
unsigned ni = *i; ni > 0; --ni)
630 auto pair = inf(m) & fin({f});
631 std::swap(pair, res);
632 res |= std::move(pair);
637 static acc_code parity(
bool max,
bool odd,
unsigned sets);
642 static acc_code random(
unsigned n,
double reuse = 0.0);
646 if (is_t() || r.is_f())
651 if (is_f() || r.is_t())
653 unsigned s = size() - 1;
654 unsigned rs = r.size() - 1;
657 if (((*
this)[s].sub.op == acc_op::Inf
658 && r[rs].sub.op == acc_op::Inf)
659 || ((*
this)[s].sub.op == acc_op::InfNeg
660 && r[rs].sub.op == acc_op::InfNeg))
662 (*this)[s - 1].mark |= r[rs - 1].mark;
674 auto start = &(*this)[s] - (*this)[s].sub.size;
675 auto pos = &(*this)[s] - 1;
679 if (pos->sub.op == acc_op::Inf)
684 pos -= pos->sub.size + 1;
687 else if ((*
this)[s].sub.op == acc_op::Inf)
689 left_inf = &(*this)[s - 1];
692 const acc_word* right_inf =
nullptr;
693 auto right_end = &r.back();
697 auto pos = --right_end;
700 if (pos->sub.op == acc_op::Inf)
705 pos -= pos->sub.size + 1;
708 else if (right_end->sub.op == acc_op::Inf)
710 right_inf = right_end - 1;
714 if (left_inf && right_inf)
716 carry = left_inf->mark;
717 auto pos = left_inf - &(*this)[0];
718 erase(begin() + pos, begin() + pos + 2);
721 insert(end(), &r[0], right_end + 1);
723 (*this)[sz + (right_inf - &r[0])].mark |= carry;
748 if (is_t() || r.is_f())
750 if (is_f() || r.is_t())
755 unsigned s = size() - 1;
756 unsigned rs = r.size() - 1;
758 if (((*
this)[s].sub.op == acc_op::Fin
759 && r[rs].sub.op == acc_op::Fin)
760 || ((*
this)[s].sub.op == acc_op::FinNeg
761 && r[rs].sub.op == acc_op::FinNeg))
763 (*this)[s - 1].mark |= r[rs - 1].mark;
775 auto start = &(*this)[s] - (*this)[s].sub.size;
776 auto pos = &(*this)[s] - 1;
780 if (pos->sub.op == acc_op::Fin)
785 pos -= pos->sub.size + 1;
788 else if ((*
this)[s].sub.op == acc_op::Fin)
790 left_fin = &(*this)[s - 1];
793 const acc_word* right_fin =
nullptr;
794 auto right_end = &r.back();
798 auto pos = --right_end;
801 if (pos->sub.op == acc_op::Fin)
806 pos -= pos->sub.size + 1;
809 else if (right_end->sub.op == acc_op::Fin)
811 right_fin = right_end - 1;
815 if (left_fin && right_fin)
817 carry = left_fin->mark;
818 auto pos = (left_fin - &(*this)[0]);
819 this->erase(begin() + pos, begin() + pos + 2);
822 insert(end(), &r[0], right_end + 1);
824 (*this)[sz + (right_fin - &r[0])].mark |= carry;
846 acc_code& operator<<=(
unsigned sets)
848 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
849 report_too_many_sets();
852 unsigned pos = size();
855 switch ((*
this)[pos - 1].sub.op)
857 case acc_cond::acc_op::And:
858 case acc_cond::acc_op::Or:
861 case acc_cond::acc_op::Inf:
862 case acc_cond::acc_op::InfNeg:
863 case acc_cond::acc_op::Fin:
864 case acc_cond::acc_op::FinNeg:
866 (*this)[pos].mark <<= sets;
874 acc_code operator<<(
unsigned sets)
const 894 std::vector<std::vector<int>>
895 missing(
mark_t inf,
bool accepting)
const;
897 bool accepting(
mark_t inf)
const;
899 bool inf_satisfiable(
mark_t inf)
const;
902 mark_t always_present)
const;
926 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets()
const;
931 to_html(std::ostream& os,
932 std::function<
void(std::ostream&,
int)>
933 set_printer =
nullptr)
const;
938 to_text(std::ostream& os,
939 std::function<
void(std::ostream&,
int)>
940 set_printer =
nullptr)
const;
945 to_latex(std::ostream& os,
946 std::function<
void(std::ostream&,
int)>
947 set_printer =
nullptr)
const;
982 friend std::ostream& operator<<(std::ostream& os,
const acc_code& code);
986 : num_(0
U), all_({}), code_(code)
989 uses_fin_acceptance_ = check_fin_acceptance();
993 : num_(0
U), all_({}), code_(code)
995 add_sets(code.used_sets().max_set());
996 uses_fin_acceptance_ = check_fin_acceptance();
1000 : num_(o.num_), all_(o.all_), code_(o.code_),
1001 uses_fin_acceptance_(o.uses_fin_acceptance_)
1010 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1018 void set_acceptance(
const acc_code& code)
1021 uses_fin_acceptance_ = check_fin_acceptance();
1024 const acc_code& get_acceptance()
const 1034 bool operator==(
const acc_cond& other)
const 1036 return other.num_sets() == num_ && other.get_acceptance() == code_;
1039 bool operator!=(
const acc_cond& other)
const 1041 return !(*
this == other);
1044 bool uses_fin_acceptance()
const 1046 return uses_fin_acceptance_;
1051 return code_.is_t();
1056 return num_ == 0 && is_t();
1061 return code_.is_f();
1064 bool is_none()
const 1066 return num_ == 0 && is_f();
1069 bool is_buchi()
const 1071 unsigned s = code_.size();
1073 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1076 bool is_co_buchi()
const 1078 return num_ == 1 && is_generalized_co_buchi();
1081 void set_generalized_buchi()
1083 set_acceptance(inf(all_sets()));
1086 void set_generalized_co_buchi()
1088 set_acceptance(fin(all_sets()));
1091 bool is_generalized_buchi()
const 1093 unsigned s = code_.size();
1094 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1095 && code_[0].mark == all_sets());
1098 bool is_generalized_co_buchi()
const 1100 unsigned s = code_.size();
1102 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1106 int is_rabin()
const;
1108 int is_streett()
const;
1131 bool operator==(
rs_pair o)
const 1133 return fin == o.fin && inf == o.inf;
1135 bool operator!=(
rs_pair o)
const 1137 return fin != o.fin || inf != o.inf;
1139 bool operator<(
rs_pair o)
const 1141 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1143 bool operator<=(
rs_pair o)
const 1145 return !(o < *
this);
1147 bool operator>(
rs_pair o)
const 1151 bool operator>=(
rs_pair o)
const 1153 return !(*
this < o);
1166 bool is_streett_like(std::vector<rs_pair>& pairs)
const;
1178 bool is_rabin_like(std::vector<rs_pair>& pairs)
const;
1181 bool is_generalized_rabin(std::vector<unsigned>& pairs)
const;
1184 bool is_generalized_streett(std::vector<unsigned>& pairs)
const;
1191 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1192 bool is_parity()
const 1196 return is_parity(max, odd);
1202 std::pair<bool, acc_cond::mark_t> unsat_mark()
const 1204 return sat_unsat_mark(
false);
1209 std::pair<bool, acc_cond::mark_t> sat_mark()
const 1211 return sat_unsat_mark(
true);
1215 bool check_fin_acceptance()
const;
1216 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(
bool)
const;
1221 return acc_code::inf(mark);
1224 static acc_code inf(std::initializer_list<unsigned> vals)
1226 return inf(
mark_t(vals.begin(), vals.end()));
1231 return acc_code::inf_neg(mark);
1234 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1236 return inf_neg(
mark_t(vals.begin(), vals.end()));
1241 return acc_code::fin(mark);
1244 static acc_code fin(std::initializer_list<unsigned> vals)
1246 return fin(
mark_t(vals.begin(), vals.end()));
1251 return acc_code::fin_neg(mark);
1254 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1256 return fin_neg(
mark_t(vals.begin(), vals.end()));
1259 unsigned add_sets(
unsigned num)
1265 if (num > mark_t::max_accsets())
1266 report_too_many_sets();
1278 mark_t mark(
unsigned u)
const 1280 SPOT_ASSERT(u < num_sets());
1294 bool accepting(
mark_t inf)
const 1296 return code_.accepting(inf);
1299 bool inf_satisfiable(
mark_t inf)
const 1301 return code_.inf_satisfiable(inf);
1306 return code_.maybe_accepting(infinitely_often, always_present);
1311 std::ostream& format(std::ostream& os,
mark_t m)
const 1319 std::string format(
mark_t m)
const 1321 std::ostringstream os;
1326 unsigned num_sets()
const 1331 template<
class iterator>
1332 mark_t useless(iterator begin, iterator end)
const 1336 for (
unsigned x = 0; x < num_; ++x)
1341 auto all = all_ ^ (u | (one << x));
1342 for (iterator y = begin; y != end; ++y)
1345 if (!!(v & (one << x)))
1372 return {num_sets(), code_.remove(rem, missing)};
1379 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1386 return {num_sets(), code_.remove(all_sets() - rem,
true)};
1400 std::string name(
const char* fmt =
"alo")
const;
1411 bool uses_fin_acceptance_ =
false;
1416 typedef std::vector<acc_cond::rs_pair> rs_pairs;
1420 : pairs_(p), view_marks_(m) {}
1446 return !visible(p.inf) && visible(p.fin) ? p.fin
1455 return !visible(p.fin) && visible(p.inf) ? p.inf
1463 for (
const auto& p: pairs_)
1464 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
1469 const rs_pairs& pairs()
const 1475 template<
typename filter>
1479 for (
const auto& p: pairs_)
1486 return !!(view_marks_ & v);
1489 const rs_pairs& pairs_;
1495 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
1502 typedef unsigned value_type;
1503 typedef const value_type& reference;
1504 typedef const value_type* pointer;
1505 typedef std::ptrdiff_t difference_type;
1506 typedef std::forward_iterator_tag iterator_category;
1528 value_type operator*()
const 1531 return m_.min_set() - 1;
1536 m_.clear(this->
operator*());
1580 struct hash<
spot::acc_cond::mark_t>
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:104
Definition: automata.hh:26
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1119
Definition: bitset.hh:405
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:976
op
Operator types.
Definition: formula.hh:65