23 #include <unordered_map> 26 #include <spot/tl/defaultenv.hh> 27 #include <spot/misc/trival.hh> 42 typedef unsigned value_t;
47 mark_t(value_t
id) noexcept
52 template<
class iterator>
53 mark_t(
const iterator& begin,
const iterator& end) noexcept
56 for (iterator i = begin; i != end; ++i)
60 mark_t(std::initializer_list<unsigned> vals) noexcept
61 :
mark_t(vals.begin(), vals.end())
65 bool operator==(
unsigned o)
const 71 bool operator!=(
unsigned o)
const 77 bool operator==(
mark_t o)
const 82 bool operator!=(
mark_t o)
const 87 bool operator<(
mark_t o)
const 92 bool operator<=(
mark_t o)
const 97 bool operator>(
mark_t o)
const 102 bool operator>=(
mark_t o)
const 107 explicit operator bool()
const 112 bool has(
unsigned u)
const 114 return id & (1
U << u);
122 void clear(
unsigned u)
176 mark_t operator<<(
unsigned i)
const 181 mark_t& operator<<=(
unsigned i)
187 mark_t operator>>(
unsigned i)
const 192 mark_t& operator>>=(
unsigned i)
212 auto rm = (~yv) & (yv - 1);
214 auto lm = ~(yv ^ (yv - 1));
215 xv = ((xv & lm) >> 1) | (xv & rm);
221 bool subset(
mark_t m)
const 223 return (*
this) - m == 0
U;
226 bool proper_subset(
mark_t m)
const 228 return *
this != m && this->subset(m);
232 unsigned count()
const 235 return __builtin_popcount(
id);
251 unsigned max_set()
const 254 return (
id == 0) ? 0 : (
sizeof(unsigned) * 8 - __builtin_clz(
id));
270 unsigned min_set()
const 275 return __builtin_ctz(
id) + 1;
295 mark_t& remove_some(
unsigned n)
302 template<
class iterator>
303 void fill(iterator here)
const 320 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
324 enum class acc_op : unsigned short
325 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
336 struct SPOT_API
acc_code:
public std::vector<acc_word>
338 bool operator==(
const acc_code& other)
const 340 unsigned pos = size();
341 if (other.size() != pos)
345 auto op = (*this)[pos - 1].sub.op;
346 auto sz = (*this)[pos - 1].sub.size;
347 if (other[pos - 1].sub.op !=
op ||
348 other[pos - 1].sub.size != sz)
352 case acc_cond::acc_op::And:
353 case acc_cond::acc_op::Or:
356 case acc_cond::acc_op::Inf:
357 case acc_cond::acc_op::InfNeg:
358 case acc_cond::acc_op::Fin:
359 case acc_cond::acc_op::FinNeg:
361 if (other[pos].mark != (*
this)[pos].mark)
369 bool operator<(
const acc_code& other)
const 371 unsigned pos = size();
372 auto osize = other.size();
379 auto op = (*this)[pos - 1].sub.op;
380 auto oop = other[pos - 1].sub.op;
385 auto sz = (*this)[pos - 1].sub.size;
386 auto osz = other[pos - 1].sub.size;
393 case acc_cond::acc_op::And:
394 case acc_cond::acc_op::Or:
397 case acc_cond::acc_op::Inf:
398 case acc_cond::acc_op::InfNeg:
399 case acc_cond::acc_op::Fin:
400 case acc_cond::acc_op::FinNeg:
403 auto m = (*this)[pos].mark;
404 auto om = other[pos].mark;
416 bool operator>(
const acc_code& other)
const 418 return other < *
this;
421 bool operator<=(
const acc_code& other)
const 423 return !(other < *
this);
426 bool operator>=(
const acc_code& other)
const 428 return !(*
this < other);
431 bool operator!=(
const acc_code& other)
const 433 return !(*
this == other);
439 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
440 && (*this)[s - 2].mark == 0
U);
447 && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0
U;
455 res[1].sub.op = acc_op::Fin;
470 res[1].sub.op = acc_op::Fin;
475 static acc_code fin(std::initializer_list<unsigned> vals)
485 res[1].sub.op = acc_op::FinNeg;
490 static acc_code fin_neg(std::initializer_list<unsigned> vals)
492 return fin_neg(
mark_t(vals));
500 res[1].sub.op = acc_op::Inf;
505 static acc_code inf(std::initializer_list<unsigned> vals)
515 res[1].sub.op = acc_op::InfNeg;
520 static acc_code inf_neg(std::initializer_list<unsigned> vals)
522 return inf_neg(
mark_t(vals));
535 static acc_code generalized_buchi(
unsigned n)
538 if (n == 8 *
sizeof(mark_t::value_t))
543 static acc_code generalized_co_buchi(
unsigned n)
546 if (n == 8 *
sizeof(mark_t::value_t))
557 res |= inf({2*n - 1}) & fin({2*n - 2});
569 res &= inf({2*n - 1}) | fin({2*n - 2});
575 template<
class Iterator>
576 static acc_code generalized_rabin(Iterator begin, Iterator end)
580 for (Iterator i = begin; i != end; ++i)
584 for (
unsigned ni = *i; ni > 0; --ni)
586 auto pair = inf(m) & fin({f});
587 std::swap(pair, res);
588 res |= std::move(pair);
593 static acc_code parity(
bool max,
bool odd,
unsigned sets);
598 static acc_code random(
unsigned n,
double reuse = 0.0);
602 if (is_t() || r.is_f())
607 if (is_f() || r.is_t())
609 unsigned s = size() - 1;
610 unsigned rs = r.size() - 1;
613 if (((*
this)[s].sub.op == acc_op::Inf
614 && r[rs].sub.op == acc_op::Inf)
615 || ((*
this)[s].sub.op == acc_op::InfNeg
616 && r[rs].sub.op == acc_op::InfNeg))
618 (*this)[s - 1].mark |= r[rs - 1].mark;
630 auto start = &(*this)[s] - (*this)[s].sub.size;
631 auto pos = &(*this)[s] - 1;
635 if (pos->sub.op == acc_op::Inf)
640 pos -= pos->sub.size + 1;
643 else if ((*
this)[s].sub.op == acc_op::Inf)
645 left_inf = &(*this)[s - 1];
648 const acc_word* right_inf =
nullptr;
649 auto right_end = &r.back();
653 auto pos = --right_end;
656 if (pos->sub.op == acc_op::Inf)
661 pos -= pos->sub.size + 1;
664 else if (right_end->sub.op == acc_op::Inf)
666 right_inf = right_end - 1;
670 if (left_inf && right_inf)
672 carry = left_inf->mark;
673 auto pos = left_inf - &(*this)[0];
674 erase(begin() + pos, begin() + pos + 2);
677 insert(end(), &r[0], right_end + 1);
679 (*this)[sz + (right_inf - &r[0])].mark |= carry;
704 if (is_t() || r.is_f())
706 if (is_f() || r.is_t())
711 unsigned s = size() - 1;
712 unsigned rs = r.size() - 1;
714 if (((*
this)[s].sub.op == acc_op::Fin
715 && r[rs].sub.op == acc_op::Fin)
716 || ((*
this)[s].sub.op == acc_op::FinNeg
717 && r[rs].sub.op == acc_op::FinNeg))
719 (*this)[s - 1].mark |= r[rs - 1].mark;
731 auto start = &(*this)[s] - (*this)[s].sub.size;
732 auto pos = &(*this)[s] - 1;
736 if (pos->sub.op == acc_op::Fin)
741 pos -= pos->sub.size + 1;
744 else if ((*
this)[s].sub.op == acc_op::Fin)
746 left_fin = &(*this)[s - 1];
749 const acc_word* right_fin =
nullptr;
750 auto right_end = &r.back();
754 auto pos = --right_end;
757 if (pos->sub.op == acc_op::Fin)
762 pos -= pos->sub.size + 1;
765 else if (right_end->sub.op == acc_op::Fin)
767 right_fin = right_end - 1;
771 if (left_fin && right_fin)
773 carry = left_fin->mark;
774 auto pos = (left_fin - &(*this)[0]);
775 this->erase(begin() + pos, begin() + pos + 2);
778 insert(end(), &r[0], right_end + 1);
780 (*this)[sz + (right_fin - &r[0])].mark |= carry;
802 acc_code& operator<<=(
unsigned sets)
806 unsigned pos = size();
809 switch ((*
this)[pos - 1].sub.op)
811 case acc_cond::acc_op::And:
812 case acc_cond::acc_op::Or:
815 case acc_cond::acc_op::Inf:
816 case acc_cond::acc_op::InfNeg:
817 case acc_cond::acc_op::Fin:
818 case acc_cond::acc_op::FinNeg:
820 (*this)[pos].mark.id <<= sets;
828 acc_code operator<<(
unsigned sets)
const 848 std::vector<std::vector<int>>
849 missing(
mark_t inf,
bool accepting)
const;
851 bool accepting(
mark_t inf)
const;
853 bool inf_satisfiable(
mark_t inf)
const;
856 mark_t always_present)
const;
880 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets()
const;
885 to_html(std::ostream& os,
886 std::function<
void(std::ostream&,
int)>
887 set_printer =
nullptr)
const;
892 to_text(std::ostream& os,
893 std::function<
void(std::ostream&,
int)>
894 set_printer =
nullptr)
const;
899 to_latex(std::ostream& os,
900 std::function<
void(std::ostream&,
int)>
901 set_printer =
nullptr)
const;
936 friend std::ostream& operator<<(std::ostream& os,
const acc_code& code);
940 : num_(0
U), all_(0
U), code_(code)
943 uses_fin_acceptance_ = check_fin_acceptance();
947 : num_(0
U), all_(0
U), code_(code)
949 add_sets(code.used_sets().max_set());
950 uses_fin_acceptance_ = check_fin_acceptance();
954 : num_(o.num_), all_(o.all_), code_(o.code_),
955 uses_fin_acceptance_(o.uses_fin_acceptance_)
964 uses_fin_acceptance_ = o.uses_fin_acceptance_;
972 void set_acceptance(
const acc_code& code)
975 uses_fin_acceptance_ = check_fin_acceptance();
978 const acc_code& get_acceptance()
const 988 bool operator==(
const acc_cond& other)
const 990 return other.num_sets() == num_ && other.get_acceptance() == code_;
993 bool operator!=(
const acc_cond& other)
const 995 return !(*
this == other);
998 bool uses_fin_acceptance()
const 1000 return uses_fin_acceptance_;
1005 return code_.is_t();
1010 return num_ == 0 && is_t();
1015 return code_.is_f();
1018 bool is_none()
const 1020 return num_ == 0 && is_f();
1023 bool is_buchi()
const 1025 unsigned s = code_.size();
1027 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1030 bool is_co_buchi()
const 1032 return num_ == 1 && is_generalized_co_buchi();
1035 void set_generalized_buchi()
1037 set_acceptance(inf(all_sets()));
1040 void set_generalized_co_buchi()
1042 set_acceptance(fin(all_sets()));
1045 bool is_generalized_buchi()
const 1047 unsigned s = code_.size();
1048 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1049 && code_[0].mark == all_sets());
1052 bool is_generalized_co_buchi()
const 1054 unsigned s = code_.size();
1056 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1060 int is_rabin()
const;
1062 int is_streett()
const;
1085 bool operator==(
rs_pair o)
const 1087 return fin == o.fin && inf == o.inf;
1089 bool operator!=(
rs_pair o)
const 1091 return fin != o.fin || inf != o.inf;
1093 bool operator<(
rs_pair o)
const 1095 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1097 bool operator<=(
rs_pair o)
const 1099 return !(o < *
this);
1101 bool operator>(
rs_pair o)
const 1105 bool operator>=(
rs_pair o)
const 1107 return !(*
this < o);
1120 bool is_streett_like(std::vector<rs_pair>& pairs)
const;
1132 bool is_rabin_like(std::vector<rs_pair>& pairs)
const;
1135 bool is_generalized_rabin(std::vector<unsigned>& pairs)
const;
1138 bool is_generalized_streett(std::vector<unsigned>& pairs)
const;
1145 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1146 bool is_parity()
const 1150 return is_parity(max, odd);
1156 std::pair<bool, acc_cond::mark_t> unsat_mark()
const;
1159 bool check_fin_acceptance()
const;
1164 return acc_code::inf(mark);
1167 static acc_code inf(std::initializer_list<unsigned> vals)
1169 return inf(
mark_t(vals.begin(), vals.end()));
1174 return acc_code::inf_neg(mark);
1177 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1179 return inf_neg(
mark_t(vals.begin(), vals.end()));
1184 return acc_code::fin(mark);
1187 static acc_code fin(std::initializer_list<unsigned> vals)
1189 return fin(
mark_t(vals.begin(), vals.end()));
1194 return acc_code::fin_neg(mark);
1197 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1199 return fin_neg(
mark_t(vals.begin(), vals.end()));
1202 unsigned add_sets(
unsigned num)
1208 if (num_ > 8 *
sizeof(mark_t::id))
1209 throw std::runtime_error(
"Too many acceptance sets used.");
1219 mark_t mark(
unsigned u)
const 1221 SPOT_ASSERT(u < num_sets());
1235 bool accepting(
mark_t inf)
const 1237 return code_.accepting(inf);
1240 bool inf_satisfiable(
mark_t inf)
const 1242 return code_.inf_satisfiable(inf);
1247 return code_.maybe_accepting(infinitely_often, always_present);
1252 std::ostream& format(std::ostream& os,
mark_t m)
const 1260 std::string format(
mark_t m)
const 1262 std::ostringstream os;
1267 unsigned num_sets()
const 1272 template<
class iterator>
1273 mark_t useless(iterator begin, iterator end)
const 1275 mark_t::value_t u = 0
U;
1276 for (
unsigned x = 0; x < num_; ++x)
1281 unsigned all = all_ ^ (u | (1 << x));
1282 for (iterator y = begin; y != end; ++y)
1312 return {num_sets(), code_.remove(rem, missing)};
1319 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1326 return {num_sets(), code_.remove(all_sets() - rem,
true)};
1340 std::string name(
const char* fmt =
"alo")
const;
1343 mark_t::value_t all_sets_()
const 1347 return -1
U >> (8 *
sizeof(mark_t::value_t) - num_);
1351 mark_t::value_t all_;
1353 bool uses_fin_acceptance_ =
false;
1358 typedef std::vector<acc_cond::rs_pair> rs_pairs;
1362 : pairs_(p), view_marks_(m) {}
1372 return visible(p.inf) ? p.inf : 0
U;
1380 return visible(p.fin) ? p.fin : 0
U;
1388 return !visible(p.inf) && visible(p.fin) ? p.fin : 0
U;
1396 return !visible(p.fin) && visible(p.inf) ? p.inf : 0
U;
1403 for (
const auto& p: pairs_)
1405 if (visible(p.fin) && visible(p.inf))
1407 if (p.fin.has(mark))
1409 if (p.inf.has(mark))
1416 const rs_pairs& pairs()
const 1422 template<
typename filter>
1426 for (
const auto& p: pairs_)
1433 return (view_marks_ & v) != 0;
1436 const rs_pairs& pairs_;
1442 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
1449 typedef unsigned value_type;
1450 typedef const value_type& reference;
1451 typedef const value_type* pointer;
1452 typedef std::ptrdiff_t difference_type;
1453 typedef std::forward_iterator_tag iterator_category;
1475 value_type operator*()
const 1478 return m_.min_set() - 1;
1527 struct hash<
spot::acc_cond::mark_t>
1531 std::hash<decltype(m.id)> h;
Definition: automata.hh:26
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1073
Definition: formula.hh:1703
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:930
op
Operator types.
Definition: formula.hh:65