1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2014-2021 Laboratoire de Recherche et Développement 3 // de l'Epita. 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <functional> 23 #include <sstream> 24 #include <vector> 25 #include <iostream> 26 #include <algorithm> 27 #include <numeric> 28 #include <bddx.h> 29 #include <spot/misc/_config.h> 30 #include <spot/misc/bitset.hh> 31 #include <spot/misc/trival.hh> 32 33 namespace spot 34 { 35 namespace internal 36 { 37 class mark_container; 38 39 template<bool> 40 struct _32acc {}; 41 template<> 42 struct _32acc<true> 43 { 44 SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t") 45 typedef unsigned value_t; 46 }; 47 } 48 49 /// \ingroup twa_essentials 50 /// @{ 51 52 /// \brief An acceptance condition 53 /// 54 /// This represent an acceptance condition in the HOA sense, that 55 /// is, an acceptance formula plus a number of acceptance sets. The 56 /// acceptance formula is expected to use a subset of the acceptance 57 /// sets. (It usually uses *all* sets, otherwise that means that 58 /// some of the sets have no influence on the automaton language and 59 /// could be removed.) 60 class SPOT_API acc_cond 61 { 62 63 public: 64 bool 65 has_parity_prefix(acc_cond& new_acc, std::vector<unsigned>& colors) const; 66 67 #ifndef SWIG 68 private: 69 [[noreturn]] static void report_too_many_sets(); 70 #endif 71 public: 72 73 /// \brief An acceptance mark 74 /// 75 /// This type is used to represent a set of acceptance sets. It 76 /// works (and is implemented) like a bit vector where bit at 77 /// index i represents the membership to the i-th acceptance set. 78 /// 79 /// Typically, each transition of an automaton is labeled by a 80 /// mark_t that represents the membership of the transition to 81 /// each of the acceptance sets. 82 /// 83 /// For efficiency reason, the maximum number of acceptance sets 84 /// (i.e., the size of the bit vector) supported is a compile-time 85 /// constant. It can be changed by passing an option to the 86 /// configure script of Spot. 87 struct mark_t : 88 public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)> 89 { 90 private: 91 // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0 92 typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t; 93 _value_t id; 94 mark_tspot::acc_cond::mark_t95 mark_t(_value_t id) noexcept 96 : id(id) 97 { 98 } 99 100 public: 101 /// Initialize an empty mark_t. 102 mark_t() = default; 103 104 mark_t 105 apply_permutation(std::vector<unsigned> permut); 106 107 108 #ifndef SWIG 109 /// Create a mark_t from a range of set numbers. 110 template<class iterator> mark_tspot::acc_cond::mark_t111 mark_t(const iterator& begin, const iterator& end) 112 : mark_t(_value_t::zero()) 113 { 114 for (iterator i = begin; i != end; ++i) 115 if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS)) 116 set(*i); 117 else 118 report_too_many_sets(); 119 } 120 121 /// Create a mark_t from a list of set numbers. mark_tspot::acc_cond::mark_t122 mark_t(std::initializer_list<unsigned> vals) 123 : mark_t(vals.begin(), vals.end()) 124 { 125 } 126 127 SPOT_DEPRECATED("use brace initialization instead") mark_tspot::acc_cond::mark_t128 mark_t(unsigned i) 129 { 130 unsigned j = 0; 131 while (i) 132 { 133 if (i & 1U) 134 this->set(j); 135 ++j; 136 i >>= 1; 137 } 138 } 139 #endif 140 141 /// \brief The maximum number of acceptance sets supported by 142 /// this implementation. 143 /// 144 /// The value can be changed at compile-time using configure's 145 /// --enable-max-accsets=N option. max_accsetsspot::acc_cond::mark_t146 constexpr static unsigned max_accsets() 147 { 148 return SPOT_MAX_ACCSETS; 149 } 150 151 /// \brief A mark_t with all bits set to one. 152 /// 153 /// Beware that *all* bits are sets, not just the bits used in 154 /// the acceptance condition. This class is unaware of the 155 /// acceptance condition. allspot::acc_cond::mark_t156 static mark_t all() 157 { 158 return mark_t(_value_t::mone()); 159 } 160 hashspot::acc_cond::mark_t161 size_t hash() const noexcept 162 { 163 std::hash<decltype(id)> h; 164 return h(id); 165 } 166 167 SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned") operator ==spot::acc_cond::mark_t168 bool operator==(unsigned o) const 169 { 170 SPOT_ASSERT(o == 0U); 171 (void)o; 172 return !id; 173 } 174 175 SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned") operator !=spot::acc_cond::mark_t176 bool operator!=(unsigned o) const 177 { 178 SPOT_ASSERT(o == 0U); 179 (void)o; 180 return !!id; 181 } 182 operator ==spot::acc_cond::mark_t183 bool operator==(mark_t o) const 184 { 185 return id == o.id; 186 } 187 operator !=spot::acc_cond::mark_t188 bool operator!=(mark_t o) const 189 { 190 return id != o.id; 191 } 192 operator <spot::acc_cond::mark_t193 bool operator<(mark_t o) const 194 { 195 return id < o.id; 196 } 197 operator <=spot::acc_cond::mark_t198 bool operator<=(mark_t o) const 199 { 200 return id <= o.id; 201 } 202 operator >spot::acc_cond::mark_t203 bool operator>(mark_t o) const 204 { 205 return id > o.id; 206 } 207 operator >=spot::acc_cond::mark_t208 bool operator>=(mark_t o) const 209 { 210 return id >= o.id; 211 } 212 operator boolspot::acc_cond::mark_t213 explicit operator bool() const 214 { 215 return !!id; 216 } 217 hasspot::acc_cond::mark_t218 bool has(unsigned u) const 219 { 220 return !!this->operator&(mark_t({0}) << u); 221 } 222 setspot::acc_cond::mark_t223 void set(unsigned u) 224 { 225 id.set(u); 226 } 227 clearspot::acc_cond::mark_t228 void clear(unsigned u) 229 { 230 id.clear(u); 231 } 232 operator &=spot::acc_cond::mark_t233 mark_t& operator&=(mark_t r) 234 { 235 id &= r.id; 236 return *this; 237 } 238 operator |=spot::acc_cond::mark_t239 mark_t& operator|=(mark_t r) 240 { 241 id |= r.id; 242 return *this; 243 } 244 operator -=spot::acc_cond::mark_t245 mark_t& operator-=(mark_t r) 246 { 247 id &= ~r.id; 248 return *this; 249 } 250 operator ^=spot::acc_cond::mark_t251 mark_t& operator^=(mark_t r) 252 { 253 id ^= r.id; 254 return *this; 255 } 256 operator &spot::acc_cond::mark_t257 mark_t operator&(mark_t r) const 258 { 259 return id & r.id; 260 } 261 operator |spot::acc_cond::mark_t262 mark_t operator|(mark_t r) const 263 { 264 return id | r.id; 265 } 266 operator -spot::acc_cond::mark_t267 mark_t operator-(mark_t r) const 268 { 269 return id & ~r.id; 270 } 271 operator ~spot::acc_cond::mark_t272 mark_t operator~() const 273 { 274 return ~id; 275 } 276 operator ^spot::acc_cond::mark_t277 mark_t operator^(mark_t r) const 278 { 279 return id ^ r.id; 280 } 281 282 #if SPOT_DEBUG || defined(SWIGPYTHON) 283 # define SPOT_WRAP_OP(ins) \ 284 try \ 285 { \ 286 ins; \ 287 } \ 288 catch (const std::runtime_error& e) \ 289 { \ 290 report_too_many_sets(); \ 291 } 292 #else 293 # define SPOT_WRAP_OP(ins) ins; 294 #endif operator <<spot::acc_cond::mark_t295 mark_t operator<<(unsigned i) const 296 { 297 SPOT_WRAP_OP(return id << i); 298 } 299 operator <<=spot::acc_cond::mark_t300 mark_t& operator<<=(unsigned i) 301 { 302 SPOT_WRAP_OP(id <<= i; return *this); 303 } 304 operator >>spot::acc_cond::mark_t305 mark_t operator>>(unsigned i) const 306 { 307 SPOT_WRAP_OP(return id >> i); 308 } 309 operator >>=spot::acc_cond::mark_t310 mark_t& operator>>=(unsigned i) 311 { 312 SPOT_WRAP_OP(id >>= i; return *this); 313 } 314 #undef SPOT_WRAP_OP 315 stripspot::acc_cond::mark_t316 mark_t strip(mark_t y) const 317 { 318 // strip every bit of id that is marked in y 319 // 100101110100.strip( 320 // 001011001000) 321 // == 10 1 11 100 322 // == 10111100 323 324 auto xv = id; // 100101110100 325 auto yv = y.id; // 001011001000 326 327 while (yv && xv) 328 { 329 // Mask for everything after the last 1 in y 330 auto rm = (~yv) & (yv - 1); // 000000000111 331 // Mask for everything before the last 1 in y 332 auto lm = ~(yv ^ (yv - 1)); // 111111110000 333 xv = ((xv & lm) >> 1) | (xv & rm); 334 yv = (yv & lm) >> 1; 335 } 336 return xv; 337 } 338 339 /// \brief Whether the set of bits represented by *this is a 340 /// subset of those represented by \a m. subsetspot::acc_cond::mark_t341 bool subset(mark_t m) const 342 { 343 return !((*this) - m); 344 } 345 346 /// \brief Whether the set of bits represented by *this is a 347 /// proper subset of those represented by \a m. proper_subsetspot::acc_cond::mark_t348 bool proper_subset(mark_t m) const 349 { 350 return *this != m && this->subset(m); 351 } 352 353 /// \brief Number of bits sets. countspot::acc_cond::mark_t354 unsigned count() const 355 { 356 return id.count(); 357 } 358 359 /// \brief The number of the highest set used plus one. 360 /// 361 /// If no set is used, this returns 0, 362 /// If the sets {1,3,8} are used, this returns 9. max_setspot::acc_cond::mark_t363 unsigned max_set() const 364 { 365 if (id) 366 return id.highest()+1; 367 else 368 return 0; 369 } 370 371 /// \brief The number of the lowest set used plus one. 372 /// 373 /// If no set is used, this returns 0. 374 /// If the sets {1,3,8} are used, this returns 2. min_setspot::acc_cond::mark_t375 unsigned min_set() const 376 { 377 if (id) 378 return id.lowest()+1; 379 else 380 return 0; 381 } 382 383 /// \brief A mark_t where all bits have been removed except the 384 /// lowest one. 385 /// 386 /// For instance if this contains {1,3,8}, the output is {1}. lowestspot::acc_cond::mark_t387 mark_t lowest() const 388 { 389 return id & -id; 390 } 391 392 /// \brief Whether the mark contains only one bit set. is_singletonspot::acc_cond::mark_t393 bool is_singleton() const 394 { 395 #if __GNUC__ 396 /* With GCC and Clang, count() is implemented using popcount. */ 397 return count() == 1; 398 #else 399 return id && !(id & (id - 1)); 400 #endif 401 } 402 403 /// \brief Whether the mark contains at least two bits set. has_manyspot::acc_cond::mark_t404 bool has_many() const 405 { 406 #if __GNUC__ 407 /* With GCC and Clang, count() is implemented using popcount. */ 408 return count() > 1; 409 #else 410 return !!(id & (id - 1)); 411 #endif 412 } 413 414 /// \brief Remove n bits that where set. 415 /// 416 /// If there are less than n bits set, the output is empty. remove_somespot::acc_cond::mark_t417 mark_t& remove_some(unsigned n) 418 { 419 while (n--) 420 id &= id - 1; 421 return *this; 422 } 423 424 /// \brief Fill a container with the indices of the bits that are set. 425 template<class iterator> fillspot::acc_cond::mark_t426 void fill(iterator here) const 427 { 428 auto a = *this; 429 unsigned level = 0; 430 while (a) 431 { 432 if (a.has(0)) 433 *here++ = level; 434 ++level; 435 a >>= 1; 436 } 437 } 438 439 /// Returns some iterable object that contains the used sets. 440 spot::internal::mark_container sets() const; 441 442 SPOT_API 443 friend std::ostream& operator<<(std::ostream& os, mark_t m); 444 as_stringspot::acc_cond::mark_t445 std::string as_string() const 446 { 447 std::ostringstream os; 448 os << *this; 449 return os.str(); 450 } 451 }; 452 453 /// \brief Operators for acceptance formulas. 454 enum class acc_op : unsigned short 455 { Inf, Fin, InfNeg, FinNeg, And, Or }; 456 457 /// \brief A "node" in an acceptance formulas. 458 /// 459 /// Acceptance formulas are stored as a vector of acc_word in a 460 /// kind of reverse polish notation. Each acc_word is either an 461 /// operator, or a set of acceptance sets. Operators come with a 462 /// size that represent the number of words in the subtree, 463 /// current operator excluded. 464 union acc_word 465 { 466 mark_t mark; 467 struct { 468 acc_op op; // Operator 469 unsigned short size; // Size of the subtree (number of acc_word), 470 // not counting this node. 471 } sub; 472 }; 473 474 /// \brief An acceptance formula. 475 /// 476 /// Acceptance formulas are stored as a vector of acc_word in a 477 /// kind of reverse polish notation. The motivation for this 478 /// design was that we could evaluate the acceptance condition 479 /// using a very simple stack-based interpreter; however it turned 480 /// out that such a stack-based interpretation would prevent us 481 /// from doing short-circuit evaluation, so we are not evaluating 482 /// acceptance conditions this way, and maybe the implementation 483 /// of acc_code could change in the future. It's best not to rely 484 /// on the fact that formulas are stored as vectors. Use the 485 /// provided methods instead. 486 struct SPOT_API acc_code: public std::vector<acc_word> 487 { 488 acc_code 489 unit_propagation(); 490 491 bool 492 has_parity_prefix(acc_cond& new_cond, 493 std::vector<unsigned>& colors) const; 494 495 bool 496 is_parity_max_equiv(std::vector<int>& permut, 497 unsigned new_color, 498 bool even) const; 499 operator ==spot::acc_cond::acc_code500 bool operator==(const acc_code& other) const 501 { 502 unsigned pos = size(); 503 if (other.size() != pos) 504 return false; 505 while (pos > 0) 506 { 507 auto op = (*this)[pos - 1].sub.op; 508 auto sz = (*this)[pos - 1].sub.size; 509 if (other[pos - 1].sub.op != op || 510 other[pos - 1].sub.size != sz) 511 return false; 512 switch (op) 513 { 514 case acc_cond::acc_op::And: 515 case acc_cond::acc_op::Or: 516 --pos; 517 break; 518 case acc_cond::acc_op::Inf: 519 case acc_cond::acc_op::InfNeg: 520 case acc_cond::acc_op::Fin: 521 case acc_cond::acc_op::FinNeg: 522 pos -= 2; 523 if (other[pos].mark != (*this)[pos].mark) 524 return false; 525 break; 526 } 527 } 528 return true; 529 }; 530 operator <spot::acc_cond::acc_code531 bool operator<(const acc_code& other) const 532 { 533 unsigned pos = size(); 534 auto osize = other.size(); 535 if (pos < osize) 536 return true; 537 if (pos > osize) 538 return false; 539 while (pos > 0) 540 { 541 auto op = (*this)[pos - 1].sub.op; 542 auto oop = other[pos - 1].sub.op; 543 if (op < oop) 544 return true; 545 if (op > oop) 546 return false; 547 auto sz = (*this)[pos - 1].sub.size; 548 auto osz = other[pos - 1].sub.size; 549 if (sz < osz) 550 return true; 551 if (sz > osz) 552 return false; 553 switch (op) 554 { 555 case acc_cond::acc_op::And: 556 case acc_cond::acc_op::Or: 557 --pos; 558 break; 559 case acc_cond::acc_op::Inf: 560 case acc_cond::acc_op::InfNeg: 561 case acc_cond::acc_op::Fin: 562 case acc_cond::acc_op::FinNeg: 563 { 564 pos -= 2; 565 auto m = (*this)[pos].mark; 566 auto om = other[pos].mark; 567 if (m < om) 568 return true; 569 if (m > om) 570 return false; 571 break; 572 } 573 } 574 } 575 return false; 576 } 577 operator >spot::acc_cond::acc_code578 bool operator>(const acc_code& other) const 579 { 580 return other < *this; 581 } 582 operator <=spot::acc_cond::acc_code583 bool operator<=(const acc_code& other) const 584 { 585 return !(other < *this); 586 } 587 operator >=spot::acc_cond::acc_code588 bool operator>=(const acc_code& other) const 589 { 590 return !(*this < other); 591 } 592 operator !=spot::acc_cond::acc_code593 bool operator!=(const acc_code& other) const 594 { 595 return !(*this == other); 596 } 597 598 /// \brief Is this the "true" acceptance condition? 599 /// 600 /// This corresponds to "t" in the HOA format. Under this 601 /// acceptance condition, all runs are accepting. is_tspot::acc_cond::acc_code602 bool is_t() const 603 { 604 // We store "t" as an empty condition, or as Inf({}). 605 unsigned s = size(); 606 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf 607 && !((*this)[s - 2].mark)); 608 } 609 610 /// \brief Is this the "false" acceptance condition? 611 /// 612 /// This corresponds to "f" in the HOA format. Under this 613 /// acceptance condition, no runs is accepting. Obviously, this 614 /// has very few practical application, except as neutral 615 /// element in some construction. is_fspot::acc_cond::acc_code616 bool is_f() const 617 { 618 // We store "f" as Fin({}). 619 unsigned s = size(); 620 return s > 1 621 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark); 622 } 623 624 /// \brief Construct the "false" acceptance condition. 625 /// 626 /// This corresponds to "f" in the HOA format. Under this 627 /// acceptance condition, no runs is accepting. Obviously, this 628 /// has very few practical application, except as neutral 629 /// element in some construction. fspot::acc_cond::acc_code630 static acc_code f() 631 { 632 acc_code res; 633 res.resize(2); 634 res[0].mark = {}; 635 res[1].sub.op = acc_op::Fin; 636 res[1].sub.size = 1; 637 return res; 638 } 639 640 /// \brief Construct the "true" acceptance condition. 641 /// 642 /// This corresponds to "t" in the HOA format. Under this 643 /// acceptance condition, all runs are accepting. tspot::acc_cond::acc_code644 static acc_code t() 645 { 646 return {}; 647 } 648 649 /// \brief Construct a generalized co-Büchi acceptance 650 /// 651 /// For the input m={1,8,9}, this constructs Fin(1)|Fin(8)|Fin(9). 652 /// 653 /// Internally, such a formula is stored using a single word 654 /// Fin({1,8,9}). 655 /// @{ finspot::acc_cond::acc_code656 static acc_code fin(mark_t m) 657 { 658 acc_code res; 659 res.resize(2); 660 res[0].mark = m; 661 res[1].sub.op = acc_op::Fin; 662 res[1].sub.size = 1; 663 return res; 664 } 665 finspot::acc_cond::acc_code666 static acc_code fin(std::initializer_list<unsigned> vals) 667 { 668 return fin(mark_t(vals)); 669 } 670 /// @} 671 672 /// \brief Construct a generalized co-Büchi acceptance for 673 /// complemented sets. 674 /// 675 /// For the input `m={1,8,9}`, this constructs 676 /// `Fin(!1)|Fin(!8)|Fin(!9)`. 677 /// 678 /// Internally, such a formula is stored using a single word 679 /// `FinNeg({1,8,9})`. 680 /// 681 /// Note that `FinNeg` formulas are not supported by most methods 682 /// of this class, and not supported by algorithms in Spot. 683 /// This is mostly used in the parser for HOA files: if the 684 /// input file uses `Fin(!0)` as acceptance condition, the 685 /// condition will eventually be rewritten as `Fin(0)` by toggling 686 /// the membership to set 0 of each transition. 687 /// @{ fin_negspot::acc_cond::acc_code688 static acc_code fin_neg(mark_t m) 689 { 690 acc_code res; 691 res.resize(2); 692 res[0].mark = m; 693 res[1].sub.op = acc_op::FinNeg; 694 res[1].sub.size = 1; 695 return res; 696 } 697 fin_negspot::acc_cond::acc_code698 static acc_code fin_neg(std::initializer_list<unsigned> vals) 699 { 700 return fin_neg(mark_t(vals)); 701 } 702 /// @} 703 704 /// \brief Construct a generalized Büchi acceptance 705 /// 706 /// For the input `m={1,8,9}`, this constructs 707 /// `Inf(1)&Inf(8)&Inf(9)`. 708 /// 709 /// Internally, such a formula is stored using a single word 710 /// `Inf({1,8,9})`. 711 /// @{ infspot::acc_cond::acc_code712 static acc_code inf(mark_t m) 713 { 714 acc_code res; 715 res.resize(2); 716 res[0].mark = m; 717 res[1].sub.op = acc_op::Inf; 718 res[1].sub.size = 1; 719 return res; 720 } 721 infspot::acc_cond::acc_code722 static acc_code inf(std::initializer_list<unsigned> vals) 723 { 724 return inf(mark_t(vals)); 725 } 726 /// @} 727 728 /// \brief Construct a generalized Büchi acceptance for 729 /// complemented sets. 730 /// 731 /// For the input `m={1,8,9}`, this constructs 732 /// `Inf(!1)&Inf(!8)&Inf(!9)`. 733 /// 734 /// Internally, such a formula is stored using a single word 735 /// `InfNeg({1,8,9})`. 736 /// 737 /// Note that `InfNeg` formulas are not supported by most methods 738 /// of this class, and not supported by algorithms in Spot. 739 /// This is mostly used in the parser for HOA files: if the 740 /// input file uses `Inf(!0)` as acceptance condition, the 741 /// condition will eventually be rewritten as `Inf(0)` by toggling 742 /// the membership to set 0 of each transition. 743 /// @{ inf_negspot::acc_cond::acc_code744 static acc_code inf_neg(mark_t m) 745 { 746 acc_code res; 747 res.resize(2); 748 res[0].mark = m; 749 res[1].sub.op = acc_op::InfNeg; 750 res[1].sub.size = 1; 751 return res; 752 } 753 inf_negspot::acc_cond::acc_code754 static acc_code inf_neg(std::initializer_list<unsigned> vals) 755 { 756 return inf_neg(mark_t(vals)); 757 } 758 /// @} 759 760 /// \brief Build a Büchi acceptance condition. 761 /// 762 /// This builds the formula `Inf(0)`. buchispot::acc_cond::acc_code763 static acc_code buchi() 764 { 765 return inf({0}); 766 } 767 768 /// \brief Build a co-Büchi acceptance condition. 769 /// 770 /// This builds the formula `Fin(0)`. cobuchispot::acc_cond::acc_code771 static acc_code cobuchi() 772 { 773 return fin({0}); 774 } 775 776 /// \brief Build a generalized-Büchi acceptance condition with n sets 777 /// 778 /// This builds the formula `Inf(0)&Inf(1)&...&Inf(n-1)`. 779 /// 780 /// When n is zero, the acceptance condition reduces to true. generalized_buchispot::acc_cond::acc_code781 static acc_code generalized_buchi(unsigned n) 782 { 783 if (n == 0) 784 return inf({}); 785 acc_cond::mark_t m = mark_t::all(); 786 m >>= mark_t::max_accsets() - n; 787 return inf(m); 788 } 789 790 /// \brief Build a generalized-co-Büchi acceptance condition with n sets 791 /// 792 /// This builds the formula `Fin(0)|Fin(1)|...|Fin(n-1)`. 793 /// 794 /// When n is zero, the acceptance condition reduces to false. generalized_co_buchispot::acc_cond::acc_code795 static acc_code generalized_co_buchi(unsigned n) 796 { 797 if (n == 0) 798 return fin({}); 799 acc_cond::mark_t m = mark_t::all(); 800 m >>= mark_t::max_accsets() - n; 801 return fin(m); 802 } 803 804 /// \brief Build a Rabin condition with n pairs. 805 /// 806 /// This builds the formula 807 /// `(Fin(0)&Inf(1))|(Fin(2)&Inf(3))|...|(Fin(2n-2)&Inf(2n-1))` rabinspot::acc_cond::acc_code808 static acc_code rabin(unsigned n) 809 { 810 acc_cond::acc_code res = f(); 811 while (n > 0) 812 { 813 res |= inf({2*n - 1}) & fin({2*n - 2}); 814 --n; 815 } 816 return res; 817 } 818 819 /// \brief Build a Streett condition with n pairs. 820 /// 821 /// This builds the formula 822 /// `(Fin(0)|Inf(1))&(Fin(2)|Inf(3))&...&(Fin(2n-2)|Inf(2n-1))` streettspot::acc_cond::acc_code823 static acc_code streett(unsigned n) 824 { 825 acc_cond::acc_code res = t(); 826 while (n > 0) 827 { 828 res &= inf({2*n - 1}) | fin({2*n - 2}); 829 --n; 830 } 831 return res; 832 } 833 834 /// \brief Build a generalized Rabin condition. 835 /// 836 /// The two iterators should point to a range of integers, each 837 /// integer being the number of Inf term in a generalized Rabin pair. 838 /// 839 /// For instance if the input is `[2,3,0]`, the output 840 /// will have three clauses (=generalized pairs), with 2 Inf terms in 841 /// the first clause, 3 in the second, and 0 in the last: 842 /// `(Fin(0)&Inf(1)&Inf(2))|Fin(3)&Inf(4)&Inf(5)&Inf(6)|Fin(7)`. 843 /// 844 /// Since set numbers are not reused, the number of sets used is 845 /// the sum of all input integers plus their count. 846 template<class Iterator> generalized_rabinspot::acc_cond::acc_code847 static acc_code generalized_rabin(Iterator begin, Iterator end) 848 { 849 acc_cond::acc_code res = f(); 850 unsigned n = 0; 851 for (Iterator i = begin; i != end; ++i) 852 { 853 unsigned f = n++; 854 acc_cond::mark_t m = {}; 855 for (unsigned ni = *i; ni > 0; --ni) 856 m.set(n++); 857 auto pair = inf(m) & fin({f}); 858 std::swap(pair, res); 859 res |= std::move(pair); 860 } 861 return res; 862 } 863 864 /// \brief Build a parity acceptance condition 865 /// 866 /// In parity acceptance a run is accepting if the maximum (or 867 /// minimum) set number that is seen infinitely often is odd (or 868 /// even). These functions will build a formula for that, as 869 /// specified in the HOA format. 870 /// @{ 871 static acc_code parity(bool is_max, bool is_odd, unsigned sets); parity_maxspot::acc_cond::acc_code872 static acc_code parity_max(bool is_odd, unsigned sets) 873 { 874 return parity(true, is_odd, sets); 875 } parity_max_oddspot::acc_cond::acc_code876 static acc_code parity_max_odd(unsigned sets) 877 { 878 return parity_max(true, sets); 879 } parity_max_evenspot::acc_cond::acc_code880 static acc_code parity_max_even(unsigned sets) 881 { 882 return parity_max(false, sets); 883 } parity_minspot::acc_cond::acc_code884 static acc_code parity_min(bool is_odd, unsigned sets) 885 { 886 return parity(false, is_odd, sets); 887 } parity_min_oddspot::acc_cond::acc_code888 static acc_code parity_min_odd(unsigned sets) 889 { 890 return parity_min(true, sets); 891 } parity_min_evenspot::acc_cond::acc_code892 static acc_code parity_min_even(unsigned sets) 893 { 894 return parity_min(false, sets); 895 } 896 /// @} 897 898 /// \brief Build a random acceptance condition 899 /// 900 /// If \a n is 0, this will always generate the true acceptance, 901 /// because working with false acceptance is somehow pointless. 902 /// 903 /// For \a n>0, we randomly create a term Fin(i) or Inf(i) for 904 /// each set 0≤i<n. If \a reuse>0.0, it gives the probability 905 /// that a set i can generate more than one Fin(i)/Inf(i) term. 906 /// Set i will be reused as long as our [0,1) random number 907 /// generator gives a value ≤reuse. (Do not set reuse≥1.0 as 908 /// that will give an infinite loop.) 909 /// 910 /// All these Fin/Inf terms are the leaves of the tree we are 911 /// building. That tree is then build by picking two random 912 /// subtrees, and joining them with & and | randomly, until we 913 /// are left with a single tree. 914 static acc_code random(unsigned n, double reuse = 0.0); 915 916 /// \brief Conjunct the current condition in place with \a r. operator &=spot::acc_cond::acc_code917 acc_code& operator&=(const acc_code& r) 918 { 919 if (is_t() || r.is_f()) 920 { 921 *this = r; 922 return *this; 923 } 924 if (is_f() || r.is_t()) 925 return *this; 926 unsigned s = size() - 1; 927 unsigned rs = r.size() - 1; 928 // We want to group all Inf(x) operators: 929 // Inf(a) & Inf(b) = Inf(a & b) 930 if (((*this)[s].sub.op == acc_op::Inf 931 && r[rs].sub.op == acc_op::Inf) 932 || ((*this)[s].sub.op == acc_op::InfNeg 933 && r[rs].sub.op == acc_op::InfNeg)) 934 { 935 (*this)[s - 1].mark |= r[rs - 1].mark; 936 return *this; 937 } 938 939 // In the more complex scenarios, left and right may both 940 // be conjunctions, and Inf(x) might be a member of each 941 // side. Find it if it exists. 942 // left_inf points to the left Inf mark if any. 943 // right_inf points to the right Inf mark if any. 944 acc_word* left_inf = nullptr; 945 if ((*this)[s].sub.op == acc_op::And) 946 { 947 auto start = &(*this)[s] - (*this)[s].sub.size; 948 auto pos = &(*this)[s] - 1; 949 pop_back(); 950 while (pos > start) 951 { 952 if (pos->sub.op == acc_op::Inf) 953 { 954 left_inf = pos - 1; 955 break; 956 } 957 pos -= pos->sub.size + 1; 958 } 959 } 960 else if ((*this)[s].sub.op == acc_op::Inf) 961 { 962 left_inf = &(*this)[s - 1]; 963 } 964 965 const acc_word* right_inf = nullptr; 966 auto right_end = &r.back(); 967 if (right_end->sub.op == acc_op::And) 968 { 969 auto start = &r[0]; 970 auto pos = --right_end; 971 while (pos > start) 972 { 973 if (pos->sub.op == acc_op::Inf) 974 { 975 right_inf = pos - 1; 976 break; 977 } 978 pos -= pos->sub.size + 1; 979 } 980 } 981 else if (right_end->sub.op == acc_op::Inf) 982 { 983 right_inf = right_end - 1; 984 } 985 986 acc_cond::mark_t carry = {}; 987 if (left_inf && right_inf) 988 { 989 carry = left_inf->mark; 990 auto pos = left_inf - &(*this)[0]; 991 erase(begin() + pos, begin() + pos + 2); 992 } 993 auto sz = size(); 994 insert(end(), &r[0], right_end + 1); 995 if (carry) 996 (*this)[sz + (right_inf - &r[0])].mark |= carry; 997 998 acc_word w; 999 w.sub.op = acc_op::And; 1000 w.sub.size = size(); 1001 emplace_back(w); 1002 return *this; 1003 } 1004 1005 /// \brief Conjunct the current condition with \a r. operator &spot::acc_cond::acc_code1006 acc_code operator&(const acc_code& r) const 1007 { 1008 acc_code res = *this; 1009 res &= r; 1010 return res; 1011 } 1012 1013 /// \brief Conjunct the current condition with \a r. operator &spot::acc_cond::acc_code1014 acc_code operator&(acc_code&& r) const 1015 { 1016 acc_code res = *this; 1017 res &= r; 1018 return res; 1019 } 1020 1021 /// \brief Disjunct the current condition in place with \a r. operator |=spot::acc_cond::acc_code1022 acc_code& operator|=(const acc_code& r) 1023 { 1024 if (is_t() || r.is_f()) 1025 return *this; 1026 if (is_f() || r.is_t()) 1027 { 1028 *this = r; 1029 return *this; 1030 } 1031 unsigned s = size() - 1; 1032 unsigned rs = r.size() - 1; 1033 // Fin(a) | Fin(b) = Fin(a | b) 1034 if (((*this)[s].sub.op == acc_op::Fin 1035 && r[rs].sub.op == acc_op::Fin) 1036 || ((*this)[s].sub.op == acc_op::FinNeg 1037 && r[rs].sub.op == acc_op::FinNeg)) 1038 { 1039 (*this)[s - 1].mark |= r[rs - 1].mark; 1040 return *this; 1041 } 1042 1043 // In the more complex scenarios, left and right may both 1044 // be disjunctions, and Fin(x) might be a member of each 1045 // side. Find it if it exists. 1046 // left_inf points to the left Inf mark if any. 1047 // right_inf points to the right Inf mark if any. 1048 acc_word* left_fin = nullptr; 1049 if ((*this)[s].sub.op == acc_op::Or) 1050 { 1051 auto start = &(*this)[s] - (*this)[s].sub.size; 1052 auto pos = &(*this)[s] - 1; 1053 pop_back(); 1054 while (pos > start) 1055 { 1056 if (pos->sub.op == acc_op::Fin) 1057 { 1058 left_fin = pos - 1; 1059 break; 1060 } 1061 pos -= pos->sub.size + 1; 1062 } 1063 } 1064 else if ((*this)[s].sub.op == acc_op::Fin) 1065 { 1066 left_fin = &(*this)[s - 1]; 1067 } 1068 1069 const acc_word* right_fin = nullptr; 1070 auto right_end = &r.back(); 1071 if (right_end->sub.op == acc_op::Or) 1072 { 1073 auto start = &r[0]; 1074 auto pos = --right_end; 1075 while (pos > start) 1076 { 1077 if (pos->sub.op == acc_op::Fin) 1078 { 1079 right_fin = pos - 1; 1080 break; 1081 } 1082 pos -= pos->sub.size + 1; 1083 } 1084 } 1085 else if (right_end->sub.op == acc_op::Fin) 1086 { 1087 right_fin = right_end - 1; 1088 } 1089 1090 acc_cond::mark_t carry = {}; 1091 if (left_fin && right_fin) 1092 { 1093 carry = left_fin->mark; 1094 auto pos = (left_fin - &(*this)[0]); 1095 this->erase(begin() + pos, begin() + pos + 2); 1096 } 1097 auto sz = size(); 1098 insert(end(), &r[0], right_end + 1); 1099 if (carry) 1100 (*this)[sz + (right_fin - &r[0])].mark |= carry; 1101 acc_word w; 1102 w.sub.op = acc_op::Or; 1103 w.sub.size = size(); 1104 emplace_back(w); 1105 return *this; 1106 } 1107 1108 /// \brief Disjunct the current condition with \a r. operator |spot::acc_cond::acc_code1109 acc_code operator|(acc_code&& r) const 1110 { 1111 acc_code res = *this; 1112 res |= r; 1113 return res; 1114 } 1115 1116 /// \brief Disjunct the current condition with \a r. operator |spot::acc_cond::acc_code1117 acc_code operator|(const acc_code& r) const 1118 { 1119 acc_code res = *this; 1120 res |= r; 1121 return res; 1122 } 1123 1124 /// \brief Apply a left shift to all mark_t that appear in the condition. 1125 /// 1126 /// Shifting `Fin(0)&Inf(3)` by 2 will give `Fin(2)&Inf(5)`. 1127 /// 1128 /// The result is modified in place. operator <<=spot::acc_cond::acc_code1129 acc_code& operator<<=(unsigned sets) 1130 { 1131 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets())) 1132 report_too_many_sets(); 1133 if (empty()) 1134 return *this; 1135 unsigned pos = size(); 1136 do 1137 { 1138 switch ((*this)[pos - 1].sub.op) 1139 { 1140 case acc_cond::acc_op::And: 1141 case acc_cond::acc_op::Or: 1142 --pos; 1143 break; 1144 case acc_cond::acc_op::Inf: 1145 case acc_cond::acc_op::InfNeg: 1146 case acc_cond::acc_op::Fin: 1147 case acc_cond::acc_op::FinNeg: 1148 pos -= 2; 1149 (*this)[pos].mark <<= sets; 1150 break; 1151 } 1152 } 1153 while (pos > 0); 1154 return *this; 1155 } 1156 1157 /// \brief Apply a left shift to all mark_t that appear in the condition. 1158 /// 1159 /// Shifting `Fin(0)&Inf(3)` by 2 will give `Fin(2)&Inf(5)`. operator <<spot::acc_cond::acc_code1160 acc_code operator<<(unsigned sets) const 1161 { 1162 acc_code res = *this; 1163 res <<= sets; 1164 return res; 1165 } 1166 1167 /// \brief Whether the acceptance formula is in disjunctive normal form. 1168 /// 1169 /// The formula is in DNF if it is either: 1170 /// - one of `t`, `f`, `Fin(i)`, `Inf(i)` 1171 /// - a conjunction of any of the above 1172 /// - a disjunction of any of the above (including the conjunctions). 1173 bool is_dnf() const; 1174 1175 /// \brief Whether the acceptance formula is in conjunctive normal form. 1176 /// 1177 /// The formula is in DNF if it is either: 1178 /// - one of `t`, `f`, `Fin(i)`, `Inf(i)` 1179 /// - a disjunction of any of the above 1180 /// - a conjunction of any of the above (including the disjunctions). 1181 bool is_cnf() const; 1182 1183 /// \brief Convert the acceptance formula into disjunctive normal form 1184 /// 1185 /// This works by distributing `&` over `|`, resulting in a formula that 1186 /// can be exponentially larger than the input. 1187 /// 1188 /// The implementation works by converting the formula into a 1189 /// BDD where `Inf(i)` is encoded by vᵢ and `Fin(i)` is encoded 1190 /// by !vᵢ, and then finding prime implicants to build an 1191 /// irredundant sum-of-products. In practice, the results are 1192 /// usually better than what we would expect by hand. 1193 acc_code to_dnf() const; 1194 1195 /// \brief Convert the acceptance formula into disjunctive normal form 1196 /// 1197 /// This works by distributing `|` over `&`, resulting in a formula that 1198 /// can be exponentially larger than the input. 1199 /// 1200 /// This implementation is the dual of `to_dnf()`. 1201 acc_code to_cnf() const; 1202 1203 /// \brief Convert the acceptance formula into a BDD 1204 /// 1205 /// \a map should be a vector indiced by colors, that 1206 /// maps each color to the desired BDD representation. 1207 bdd to_bdd(const bdd* map) const; 1208 1209 /// \brief Return the top-level disjuncts. 1210 /// 1211 /// For instance, if the formula is 1212 /// Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns 1213 /// [Fin(0), Fin(1), Fin(2)&(Inf(3)|Fin(4))]. 1214 /// 1215 /// If the formula is not a disjunction, this returns 1216 /// a vector with the formula as only element. 1217 std::vector<acc_code> top_disjuncts() const; 1218 1219 /// \brief Return the top-level conjuncts. 1220 /// 1221 /// For instance, if the formula is 1222 /// Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns 1223 /// [Fin(0), Fin(1), Fin(2)&(Inf(3)|Fin(4))]. 1224 /// 1225 /// If the formula is not a conjunction, this returns 1226 /// a vector with the formula as only element. 1227 std::vector<acc_code> top_conjuncts() const; 1228 1229 /// \brief Complement an acceptance formula. 1230 /// 1231 /// Also known as "dualizing the acceptance condition" since 1232 /// this replaces `Fin` ↔ `Inf`, and `&` ↔ `|`. 1233 /// 1234 /// Not that dualizing the acceptance condition on a 1235 /// deterministic automaton is enough to complement that 1236 /// automaton. On a non-deterministic automaton, you should 1237 /// also replace existential choices by universal choices, 1238 /// as done by the dualize() function. 1239 acc_code complement() const; 1240 1241 /// \brief Find a `Fin(i)` that is a unit clause. 1242 /// 1243 /// This return a mark_t `{i}` such that `Fin(i)` appears as a 1244 /// unit clause in the acceptance condition. I.e., either the 1245 /// condition is exactly `Fin(i)`, or the condition has the form 1246 /// `...&Fin(i)&...`. If there is no such `Fin(i)`, an empty 1247 /// mark_t is returned. 1248 /// 1249 /// If multiple unit-Fin appear as unit-clauses, the set of 1250 /// those will be returned. For instance applied to 1251 /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. 1252 mark_t fin_unit() const; 1253 1254 /// \brief Find a `Inf(i)` that is a unit clause. 1255 /// 1256 /// This return a mark_t `{i}` such that `Inf(i)` appears as a 1257 /// unit clause in the acceptance condition. I.e., either the 1258 /// condition is exactly `Inf(i)`, or the condition has the form 1259 /// `...&Inf(i)&...`. If there is no such `Inf(i)`, an empty 1260 /// mark_t is returned. 1261 /// 1262 /// If multiple unit-Inf appear as unit-clauses, the set of 1263 /// those will be returned. For instance applied to 1264 /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. 1265 mark_t inf_unit() const; 1266 1267 /// \brief Return one acceptance set i that appears as `Fin(i)` 1268 /// in the condition. 1269 /// 1270 /// Return -1 if no such set exist. 1271 int fin_one() const; 1272 1273 /// \brief Return one acceptance set i that appears as `Fin(i)` 1274 /// in the condition, and all disjuncts containing it. 1275 /// 1276 /// If the condition is a disjunction and one of the disjunct 1277 /// has the shape `...&Fin(i)&...`, then `i` will be prefered 1278 /// over any arbitrary Fin. 1279 /// 1280 /// The second element of the pair, is the same acceptance 1281 /// condition in which all top-level disjunct not featuring 1282 /// `Fin(i)` have been removed. 1283 /// 1284 /// For example on 1285 /// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` 1286 /// the output would be the pair 1287 /// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. 1288 /// On that example `Fin(1)` is prefered to `Fin(7)` because 1289 /// it appears at the top-level. 1290 std::pair<int, acc_code> fin_one_extract() const; 1291 1292 /// \brief Help closing accepting or rejecting cycle. 1293 /// 1294 /// Assuming you have a partial cycle visiting all acceptance 1295 /// sets in \a inf, this returns the combination of set you 1296 /// should see or avoid when closing the cycle to make it 1297 /// accepting or rejecting (as specified with \a accepting). 1298 /// 1299 /// The result is a vector of vectors of integers. 1300 /// A positive integer x denote a set that should be seen, 1301 /// a negative value x means the set -x-1 must be absent. 1302 /// The different inter vectors correspond to different 1303 /// solutions satisfying the \a accepting criterion. 1304 std::vector<std::vector<int>> 1305 missing(mark_t inf, bool accepting) const; 1306 1307 /// \brief Check whether visiting *exactly* all sets \a inf 1308 /// infinitely often satisfies the acceptance condition. 1309 bool accepting(mark_t inf) const; 1310 1311 /// \brief Assuming that we will visit at least all sets in \a 1312 /// inf, is there any chance that we will satisfy the condition? 1313 /// 1314 /// This return false only when it is sure that visiting more 1315 /// set will never make the condition satisfiable. 1316 bool inf_satisfiable(mark_t inf) const; 1317 1318 /// \brief Check potential acceptance of an SCC. 1319 /// 1320 /// Assuming that an SCC intersects all sets in \a 1321 /// infinitely_often (i.e., for each set in \a infinetely_often, 1322 /// there exist one marked transition in the SCC), and is 1323 /// included in all sets in \a always_present (i.e., all 1324 /// transitions are marked with \a always_present), this returns 1325 /// one tree possible results: 1326 /// - trival::yes() the SCC is necessarily accepting, 1327 /// - trival::no() the SCC is necessarily rejecting, 1328 /// - trival::maybe() the SCC could contain an accepting cycle. 1329 trival maybe_accepting(mark_t infinitely_often, 1330 mark_t always_present) const; 1331 1332 /// \brief compute the symmetry class of the acceptance sets. 1333 /// 1334 /// Two sets x and y are symmetric if swapping them in the 1335 /// acceptance condition produces an equivalent formula. 1336 /// For instance 0 and 2 are symmetric in Inf(0)&Fin(1)&Inf(2). 1337 /// 1338 /// The returned vector is indexed by set numbers, and each 1339 /// entry points to the "root" (or representative element) of 1340 /// its symmetry class. In the above example the result would 1341 /// be [0,1,0], showing that 0 and 2 are in the same class. 1342 std::vector<unsigned> symmetries() const; 1343 1344 /// \brief Remove all the acceptance sets in \a rem. 1345 /// 1346 /// If \a missing is set, the acceptance sets are assumed to be 1347 /// missing from the automaton, and the acceptance is updated to 1348 /// reflect this. For instance `(Inf(1)&Inf(2))|Fin(3)` will 1349 /// become `Fin(3)` if we remove `2` because it is missing from this 1350 /// automaton. Indeed there is no way to fulfill `Inf(1)&Inf(2)` 1351 /// in this case. So essentially `missing=true` causes Inf(rem) to 1352 /// become `f`, and `Fin(rem)` to become `t`. 1353 /// 1354 /// If \a missing is unset, `Inf(rem)` become `t` while 1355 /// `Fin(rem)` become `f`. Removing `2` from 1356 /// `(Inf(1)&Inf(2))|Fin(3)` would then give `Inf(1)|Fin(3)`. 1357 acc_code remove(acc_cond::mark_t rem, bool missing) const; 1358 1359 /// \brief Remove acceptance sets, and shift set numbers 1360 /// 1361 /// Same as remove, but also shift set numbers in the result so 1362 /// that all used set numbers are continuous. 1363 acc_code strip(acc_cond::mark_t rem, bool missing) const; 1364 /// \brief For all `x` in \a m, replaces `Fin(x)` by `false`. 1365 acc_code force_inf(mark_t m) const; 1366 1367 /// \brief Return the set of sets appearing in the condition. 1368 acc_cond::mark_t used_sets() const; 1369 1370 /// \brief Find patterns of useless colors. 1371 /// 1372 /// If any subformula of the acceptance condition looks like 1373 /// (Inf(y₁)&Inf(y₂)&...&Inf(yₙ)) | f(x₁,...,xₙ) 1374 /// or (Fin(y₁)|Fin(y₂)|...|Fin(yₙ)) & f(x₁,...,xₙ) 1375 /// then for each transition with all colors {y₁,y₂,...,yₙ} we 1376 /// can add or remove all the xᵢ that are used only once in 1377 /// the formula. 1378 /// 1379 /// This method returns a vector of pairs: 1380 /// [({y₁,y₂,...,yₙ},{x₁,x₂,...,xₙ}),...] 1381 std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>> 1382 useless_colors_patterns() const; 1383 1384 /// \brief Return the sets that appears only once in the 1385 /// acceptance. 1386 /// 1387 /// For instance if the condition is 1388 /// `Fin(0)&(Inf(1)|(Fin(1)&Inf(2)))`, this returns `{0,2}`, 1389 /// because set `1` is used more than once. 1390 mark_t used_once_sets() const; 1391 1392 /// \brief Return the sets used as Inf or Fin in the acceptance condition 1393 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const; 1394 1395 /// \brief Print the acceptance formula as HTML. 1396 /// 1397 /// The set_printer function can be used to customize the output 1398 /// of set numbers. 1399 std::ostream& 1400 to_html(std::ostream& os, 1401 std::function<void(std::ostream&, int)> 1402 set_printer = nullptr) const; 1403 1404 /// \brief Print the acceptance formula as text. 1405 /// 1406 /// The set_printer function can be used to customize the output 1407 /// of set numbers. 1408 std::ostream& 1409 to_text(std::ostream& os, 1410 std::function<void(std::ostream&, int)> 1411 set_printer = nullptr) const; 1412 1413 /// \brief Print the acceptance formula as LaTeX. 1414 /// 1415 /// The set_printer function can be used to customize the output 1416 /// of set numbers. 1417 std::ostream& 1418 to_latex(std::ostream& os, 1419 std::function<void(std::ostream&, int)> 1420 set_printer = nullptr) const; 1421 1422 /// \brief Construct an acc_code from a string. 1423 /// 1424 /// The string should either follow the following grammar: 1425 /// 1426 /// <pre> 1427 /// acc ::= "t" 1428 /// | "f" 1429 /// | "Inf" "(" num ")" 1430 /// | "Fin" "(" num ")" 1431 /// | "(" acc ")" 1432 /// | acc "&" acc 1433 /// | acc "|" acc 1434 /// </pre> 1435 /// 1436 /// Where num is an integer and "&" has priority over "|". Note that 1437 /// "Fin(!x)" and "Inf(!x)" are not supported by this parser. 1438 /// 1439 /// Or the string could be the name of an acceptance condition, as 1440 /// speficied in the HOA format. (E.g. "Rabin 2", "parity max odd 3", 1441 /// "generalized-Rabin 4 2 1", etc.). 1442 /// 1443 /// A spot::parse_error is thrown on syntax error. 1444 acc_code(const char* input); 1445 1446 /// \brief Build an empty acceptance formula. 1447 /// 1448 /// This is the same as t(). acc_codespot::acc_cond::acc_code1449 acc_code() 1450 { 1451 } 1452 1453 /// \brief Copy a part of another acceptance formula acc_codespot::acc_cond::acc_code1454 acc_code(const acc_word* other) 1455 : std::vector<acc_word>(other - other->sub.size, other + 1) 1456 { 1457 } 1458 1459 /// \brief prints the acceptance formula as text 1460 SPOT_API 1461 friend std::ostream& operator<<(std::ostream& os, const acc_code& code); 1462 }; 1463 1464 /// \brief Build an acceptance condition 1465 /// 1466 /// This takes a number of sets \a n_sets, and an acceptance 1467 /// formula (\a code) over those sets. 1468 /// 1469 /// The number of sets should be at least cover all the sets used 1470 /// in \a code. acc_cond(unsigned n_sets=0,const acc_code & code={})1471 acc_cond(unsigned n_sets = 0, const acc_code& code = {}) 1472 : num_(0U), all_({}), code_(code) 1473 { 1474 add_sets(n_sets); 1475 uses_fin_acceptance_ = check_fin_acceptance(); 1476 } 1477 1478 /// \brief Build an acceptance condition 1479 /// 1480 /// In this version, the number of sets is set the the smallest 1481 /// number necessary for \a code. acc_cond(const acc_code & code)1482 acc_cond(const acc_code& code) 1483 : num_(0U), all_({}), code_(code) 1484 { 1485 add_sets(code.used_sets().max_set()); 1486 uses_fin_acceptance_ = check_fin_acceptance(); 1487 } 1488 1489 /// \brief Copy an acceptance condition acc_cond(const acc_cond & o)1490 acc_cond(const acc_cond& o) 1491 : num_(o.num_), all_(o.all_), code_(o.code_), 1492 uses_fin_acceptance_(o.uses_fin_acceptance_) 1493 { 1494 } 1495 1496 /// \brief Copy an acceptance condition operator =(const acc_cond & o)1497 acc_cond& operator=(const acc_cond& o) 1498 { 1499 num_ = o.num_; 1500 all_ = o.all_; 1501 code_ = o.code_; 1502 uses_fin_acceptance_ = o.uses_fin_acceptance_; 1503 return *this; 1504 } 1505 ~acc_cond()1506 ~acc_cond() 1507 { 1508 } 1509 1510 /// \brief Change the acceptance formula. 1511 /// 1512 /// Beware, this does not change the number of declared sets. set_acceptance(const acc_code & code)1513 void set_acceptance(const acc_code& code) 1514 { 1515 code_ = code; 1516 uses_fin_acceptance_ = check_fin_acceptance(); 1517 } 1518 1519 /// \brief Retrieve the acceptance formula get_acceptance() const1520 const acc_code& get_acceptance() const 1521 { 1522 return code_; 1523 } 1524 1525 /// \brief Retrieve the acceptance formula get_acceptance()1526 acc_code& get_acceptance() 1527 { 1528 return code_; 1529 } 1530 operator ==(const acc_cond & other) const1531 bool operator==(const acc_cond& other) const 1532 { 1533 return other.num_sets() == num_ && other.get_acceptance() == code_; 1534 } 1535 operator !=(const acc_cond & other) const1536 bool operator!=(const acc_cond& other) const 1537 { 1538 return !(*this == other); 1539 } 1540 1541 /// \brief Whether the acceptance condition uses Fin terms uses_fin_acceptance() const1542 bool uses_fin_acceptance() const 1543 { 1544 return uses_fin_acceptance_; 1545 } 1546 1547 /// \brief Whether the acceptance formula is "t" (true) is_t() const1548 bool is_t() const 1549 { 1550 return code_.is_t(); 1551 } 1552 1553 /// \brief Whether the acceptance condition is "all" 1554 /// 1555 /// In the HOA format, the acceptance condition "all" correspond 1556 /// to the formula "t" with 0 declared acceptance sets. is_all() const1557 bool is_all() const 1558 { 1559 return num_ == 0 && is_t(); 1560 } 1561 1562 /// \brief Whether the acceptance formula is "f" (false) is_f() const1563 bool is_f() const 1564 { 1565 return code_.is_f(); 1566 } 1567 1568 /// \brief Whether the acceptance condition is "none" 1569 /// 1570 /// In the HOA format, the acceptance condition "all" correspond 1571 /// to the formula "f" with 0 declared acceptance sets. is_none() const1572 bool is_none() const 1573 { 1574 return num_ == 0 && is_f(); 1575 } 1576 1577 /// \brief Whether the acceptance condition is "Büchi" 1578 /// 1579 /// The acceptance condition is Büchi if its formula is Inf(0) and 1580 /// only 1 set is used. is_buchi() const1581 bool is_buchi() const 1582 { 1583 unsigned s = code_.size(); 1584 return num_ == 1 && 1585 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets(); 1586 } 1587 1588 /// \brief Whether the acceptance condition is "co-Büchi" 1589 /// 1590 /// The acceptance condition is co-Büchi if its formula is Fin(0) and 1591 /// only 1 set is used. is_co_buchi() const1592 bool is_co_buchi() const 1593 { 1594 return num_ == 1 && is_generalized_co_buchi(); 1595 } 1596 1597 /// \brief Change the acceptance condition to generalized-Büchi, 1598 /// over all declared sets. set_generalized_buchi()1599 void set_generalized_buchi() 1600 { 1601 set_acceptance(inf(all_sets())); 1602 } 1603 1604 /// \brief Change the acceptance condition to 1605 /// generalized-co-Büchi, over all declared sets. set_generalized_co_buchi()1606 void set_generalized_co_buchi() 1607 { 1608 set_acceptance(fin(all_sets())); 1609 } 1610 1611 /// \brief Whether the acceptance condition is "generalized-Büchi" 1612 /// 1613 /// The acceptance condition with n sets is generalized-Büchi if its 1614 /// formula is Inf(0)&Inf(1)&...&Inf(n-1). is_generalized_buchi() const1615 bool is_generalized_buchi() const 1616 { 1617 unsigned s = code_.size(); 1618 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf 1619 && code_[0].mark == all_sets()); 1620 } 1621 1622 /// \brief Whether the acceptance condition is "generalized-co-Büchi" 1623 /// 1624 /// The acceptance condition with n sets is generalized-co-Büchi if its 1625 /// formula is Fin(0)|Fin(1)|...|Fin(n-1). is_generalized_co_buchi() const1626 bool is_generalized_co_buchi() const 1627 { 1628 unsigned s = code_.size(); 1629 return (s == 2 && 1630 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets()); 1631 } 1632 1633 /// \brief Check if the acceptance condition matches the Rabin 1634 /// acceptance of the HOA format 1635 /// 1636 /// Rabin acceptance over 2n sets look like 1637 /// `(Fin(0)&Inf(1))|...|(Fin(2n-2)&Inf(2n-1))`; i.e., a 1638 /// disjunction of n pairs of the form `Fin(2i)&Inf(2i+1)`. 1639 /// 1640 /// `f` is a special kind of Rabin acceptance with 0 pairs. 1641 /// 1642 /// This function returns a number of pairs (>=0) or -1 if the 1643 /// acceptance condition is not Rabin. 1644 int is_rabin() const; 1645 1646 /// \brief Check if the acceptance condition matches the Streett 1647 /// acceptance of the HOA format 1648 /// 1649 /// Streett acceptance over 2n sets look like 1650 /// `(Fin(0)|Inf(1))&...&(Fin(2n-2)|Inf(2n-1))`; i.e., a 1651 /// conjunction of n pairs of the form `Fin(2i)|Inf(2i+1)`. 1652 /// 1653 /// `t` is a special kind of Streett acceptance with 0 pairs. 1654 /// 1655 /// This function returns a number of pairs (>=0) or -1 if the 1656 /// acceptance condition is not Streett. 1657 int is_streett() const; 1658 1659 /// \brief Rabin/streett pairs used by is_rabin_like and is_streett_like. 1660 /// 1661 /// These pairs hold two marks which can each contain one or no set number. 1662 /// 1663 /// For instance is_streett_like() rewrites Inf(0)&(Inf(2)|Fin(1))&Fin(3) 1664 /// as three pairs: [(fin={},inf={0}),(fin={1},inf={2}),(fin={3},inf={})]. 1665 /// 1666 /// Empty marks should be interpreted in a way that makes them 1667 /// false in Streett, and true in Rabin. 1668 struct SPOT_API rs_pair 1669 { 1670 #ifndef SWIG 1671 rs_pair() = default; 1672 rs_pair(const rs_pair&) = default; 1673 rs_pair& operator=(const rs_pair&) = default; 1674 #endif 1675 rs_pairspot::acc_cond::rs_pair1676 rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept: 1677 fin(fin), 1678 inf(inf) 1679 {} 1680 acc_cond::mark_t fin; 1681 acc_cond::mark_t inf; 1682 operator ==spot::acc_cond::rs_pair1683 bool operator==(rs_pair o) const 1684 { 1685 return fin == o.fin && inf == o.inf; 1686 } operator !=spot::acc_cond::rs_pair1687 bool operator!=(rs_pair o) const 1688 { 1689 return fin != o.fin || inf != o.inf; 1690 } operator <spot::acc_cond::rs_pair1691 bool operator<(rs_pair o) const 1692 { 1693 return fin < o.fin || (!(o.fin < fin) && inf < o.inf); 1694 } operator <=spot::acc_cond::rs_pair1695 bool operator<=(rs_pair o) const 1696 { 1697 return !(o < *this); 1698 } operator >spot::acc_cond::rs_pair1699 bool operator>(rs_pair o) const 1700 { 1701 return o < *this; 1702 } operator >=spot::acc_cond::rs_pair1703 bool operator>=(rs_pair o) const 1704 { 1705 return !(*this < o); 1706 } 1707 }; 1708 /// \brief Test whether an acceptance condition is Streett-like 1709 /// and returns each Streett pair in an std::vector<rs_pair>. 1710 /// 1711 /// An acceptance condition is Streett-like if it can be transformed into 1712 /// a Streett acceptance with little modification to its automaton. 1713 /// A Streett-like acceptance condition follows one of those rules: 1714 /// -It is a conjunction of disjunctive clauses containing at most one 1715 /// Inf and at most one Fin. 1716 /// -It is true (with 0 pair) 1717 /// -It is false (1 pair [0U, 0U]) 1718 bool is_streett_like(std::vector<rs_pair>& pairs) const; 1719 1720 /// \brief Test whether an acceptance condition is Rabin-like 1721 /// and returns each Rabin pair in an std::vector<rs_pair>. 1722 /// 1723 /// An acceptance condition is Rabin-like if it can be transformed into 1724 /// a Rabin acceptance with little modification to its automaton. 1725 /// A Rabin-like acceptance condition follows one of those rules: 1726 /// -It is a disjunction of conjunctive clauses containing at most one 1727 /// Inf and at most one Fin. 1728 /// -It is true (1 pair [0U, 0U]) 1729 /// -It is false (0 pairs) 1730 bool is_rabin_like(std::vector<rs_pair>& pairs) const; 1731 1732 /// \brief Is the acceptance condition generalized-Rabin? 1733 /// 1734 /// Check if the condition follows the generalized-Rabin 1735 /// definition of the HOA format. So one Fin should be in front 1736 /// of each generalized pair, and set numbers should all be used 1737 /// once. 1738 /// 1739 /// When true is returned, the \a pairs vector contains the number 1740 /// of `Inf` term in each pair. Otherwise, \a pairs is emptied. 1741 bool is_generalized_rabin(std::vector<unsigned>& pairs) const; 1742 1743 /// \brief Is the acceptance condition generalized-Streett? 1744 /// 1745 /// There is no definition of generalized Streett in HOA v1, 1746 /// so this uses the definition from the development version 1747 /// of the HOA format, that should eventually become HOA v1.1 or 1748 /// HOA v2. 1749 /// 1750 /// One Inf should be in front of each generalized pair, and 1751 /// set numbers should all be used once. 1752 /// 1753 /// When true is returned, the \a pairs vector contains the number 1754 /// of `Fin` term in each pair. Otherwise, \a pairs is emptied. 1755 bool is_generalized_streett(std::vector<unsigned>& pairs) const; 1756 1757 /// \brief check is the acceptance condition matches one of the 1758 /// four type of parity acceptance defined in the HOA format. 1759 /// 1760 /// On success, this return true and sets \a max, and \a odd to 1761 /// the type of parity acceptance detected. By default \a equiv = 1762 /// false, and the parity acceptance should match exactly the 1763 /// order of operators given in the HOA format. If \a equiv is 1764 /// set, any formula that this logically equivalent to one of the 1765 /// HOA format will be accepted. 1766 bool is_parity(bool& max, bool& odd, bool equiv = false) const; 1767 1768 1769 bool is_parity_max_equiv(std::vector<int>& permut, bool even) const; 1770 1771 /// \brief check is the acceptance condition matches one of the 1772 /// four type of parity acceptance defined in the HOA format. is_parity() const1773 bool is_parity() const 1774 { 1775 bool max; 1776 bool odd; 1777 return is_parity(max, odd); 1778 } 1779 1780 /// \brief Remove superfluous Fin and Inf by unit propagation. 1781 /// 1782 /// For example in `Fin(0)|(Inf(0) & Fin(1))`, `Inf(0)` is true 1783 /// iff `Fin(0)` is false so we can rewrite it as `Fin(0)|Fin(1)`. 1784 /// 1785 /// The number of acceptance sets is not modified even if some do 1786 /// not appear in the acceptance condition anymore. unit_propagation()1787 acc_cond unit_propagation() 1788 { 1789 return acc_cond(num_, code_.unit_propagation()); 1790 } 1791 1792 // Return (true, m) if there exist some acceptance mark m that 1793 // does not satisfy the acceptance condition. Return (false, 0U) 1794 // otherwise. unsat_mark() const1795 std::pair<bool, acc_cond::mark_t> unsat_mark() const 1796 { 1797 return sat_unsat_mark(false); 1798 } 1799 // Return (true, m) if there exist some acceptance mark m that 1800 // does satisfy the acceptance condition. Return (false, 0U) 1801 // otherwise. sat_mark() const1802 std::pair<bool, acc_cond::mark_t> sat_mark() const 1803 { 1804 return sat_unsat_mark(true); 1805 } 1806 1807 protected: 1808 bool check_fin_acceptance() const; 1809 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const; 1810 1811 public: 1812 /// \brief Construct a generalized Büchi acceptance 1813 /// 1814 /// For the input `m={1,8,9}`, this constructs 1815 /// `Inf(1)&Inf(8)&Inf(9)`. 1816 /// 1817 /// Internally, such a formula is stored using a single word 1818 /// `Inf({1,8,9})`. 1819 /// @{ inf(mark_t mark)1820 static acc_code inf(mark_t mark) 1821 { 1822 return acc_code::inf(mark); 1823 } 1824 inf(std::initializer_list<unsigned> vals)1825 static acc_code inf(std::initializer_list<unsigned> vals) 1826 { 1827 return inf(mark_t(vals.begin(), vals.end())); 1828 } 1829 /// @} 1830 1831 /// \brief Construct a generalized Büchi acceptance for 1832 /// complemented sets. 1833 /// 1834 /// For the input `m={1,8,9}`, this constructs 1835 /// `Inf(!1)&Inf(!8)&Inf(!9)`. 1836 /// 1837 /// Internally, such a formula is stored using a single word 1838 /// `InfNeg({1,8,9})`. 1839 /// 1840 /// Note that `InfNeg` formulas are not supported by most methods 1841 /// of this class, and not supported by algorithms in Spot. 1842 /// This is mostly used in the parser for HOA files: if the 1843 /// input file uses `Inf(!0)` as acceptance condition, the 1844 /// condition will eventually be rewritten as `Inf(0)` by toggling 1845 /// the membership to set 0 of each transition. 1846 /// @{ inf_neg(mark_t mark)1847 static acc_code inf_neg(mark_t mark) 1848 { 1849 return acc_code::inf_neg(mark); 1850 } 1851 inf_neg(std::initializer_list<unsigned> vals)1852 static acc_code inf_neg(std::initializer_list<unsigned> vals) 1853 { 1854 return inf_neg(mark_t(vals.begin(), vals.end())); 1855 } 1856 /// @} 1857 1858 /// \brief Construct a generalized co-Büchi acceptance 1859 /// 1860 /// For the input m={1,8,9}, this constructs Fin(1)|Fin(8)|Fin(9). 1861 /// 1862 /// Internally, such a formula is stored using a single word 1863 /// Fin({1,8,9}). 1864 /// @{ fin(mark_t mark)1865 static acc_code fin(mark_t mark) 1866 { 1867 return acc_code::fin(mark); 1868 } 1869 fin(std::initializer_list<unsigned> vals)1870 static acc_code fin(std::initializer_list<unsigned> vals) 1871 { 1872 return fin(mark_t(vals.begin(), vals.end())); 1873 } 1874 /// @} 1875 1876 /// \brief Construct a generalized co-Büchi acceptance for 1877 /// complemented sets. 1878 /// 1879 /// For the input `m={1,8,9}`, this constructs 1880 /// `Fin(!1)|Fin(!8)|Fin(!9)`. 1881 /// 1882 /// Internally, such a formula is stored using a single word 1883 /// `FinNeg({1,8,9})`. 1884 /// 1885 /// Note that `FinNeg` formulas are not supported by most methods 1886 /// of this class, and not supported by algorithms in Spot. 1887 /// This is mostly used in the parser for HOA files: if the 1888 /// input file uses `Fin(!0)` as acceptance condition, the 1889 /// condition will eventually be rewritten as `Fin(0)` by toggling 1890 /// the membership to set 0 of each transition. 1891 /// @{ fin_neg(mark_t mark)1892 static acc_code fin_neg(mark_t mark) 1893 { 1894 return acc_code::fin_neg(mark); 1895 } 1896 fin_neg(std::initializer_list<unsigned> vals)1897 static acc_code fin_neg(std::initializer_list<unsigned> vals) 1898 { 1899 return fin_neg(mark_t(vals.begin(), vals.end())); 1900 } 1901 /// @} 1902 1903 /// \brief Add more sets to the acceptance condition. 1904 /// 1905 /// This simply augment the number of sets, without changing the 1906 /// acceptance formula. add_sets(unsigned num)1907 unsigned add_sets(unsigned num) 1908 { 1909 if (num == 0) 1910 return -1U; 1911 unsigned j = num_; 1912 num += j; 1913 if (num > mark_t::max_accsets()) 1914 report_too_many_sets(); 1915 // Make sure we do not update if we raised an exception. 1916 num_ = num; 1917 all_ = all_sets_(); 1918 return j; 1919 } 1920 1921 /// \brief Add a single set to the acceptance condition. 1922 /// 1923 /// This simply augment the number of sets, without changing the 1924 /// acceptance formula. add_set()1925 unsigned add_set() 1926 { 1927 return add_sets(1); 1928 } 1929 1930 /// \brief Build a mark_t with a single set mark(unsigned u) const1931 mark_t mark(unsigned u) const 1932 { 1933 SPOT_ASSERT(u < num_sets()); 1934 return mark_t({u}); 1935 } 1936 1937 /// \brief Complement a mark_t 1938 /// 1939 /// Complementation is done with respect to the number of sets 1940 /// declared. comp(const mark_t & l) const1941 mark_t comp(const mark_t& l) const 1942 { 1943 return all_ ^ l; 1944 } 1945 1946 /// \brief Construct a mark_t with all declared sets. all_sets() const1947 mark_t all_sets() const 1948 { 1949 return all_; 1950 } 1951 1952 acc_cond apply_permutation(std::vector<unsigned> permut)1953 apply_permutation(std::vector<unsigned>permut) 1954 { 1955 return acc_cond(apply_permutation_aux(permut)); 1956 } 1957 1958 acc_code apply_permutation_aux(std::vector<unsigned> permut)1959 apply_permutation_aux(std::vector<unsigned>permut) 1960 { 1961 auto conj = top_conjuncts(); 1962 auto disj = top_disjuncts(); 1963 1964 if (conj.size() > 1) 1965 { 1966 auto transformed = std::vector<acc_code>(); 1967 for (auto elem : conj) 1968 transformed.push_back(elem.apply_permutation_aux(permut)); 1969 std::sort(transformed.begin(), transformed.end()); 1970 auto uniq = std::unique(transformed.begin(), transformed.end()); 1971 auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(), 1972 [](acc_code c1, acc_code c2) 1973 { 1974 return c1 & c2; 1975 }); 1976 return result; 1977 } 1978 else if (disj.size() > 1) 1979 { 1980 auto transformed = std::vector<acc_code>(); 1981 for (auto elem : disj) 1982 transformed.push_back(elem.apply_permutation_aux(permut)); 1983 std::sort(transformed.begin(), transformed.end()); 1984 auto uniq = std::unique(transformed.begin(), transformed.end()); 1985 auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(), 1986 [](acc_code c1, acc_code c2) 1987 { 1988 return c1 | c2; 1989 }); 1990 return result; 1991 } 1992 else 1993 { 1994 if (code_.back().sub.op == acc_cond::acc_op::Fin) 1995 return fin(code_[0].mark.apply_permutation(permut)); 1996 if (code_.back().sub.op == acc_cond::acc_op::Inf) 1997 return inf(code_[0].mark.apply_permutation(permut)); 1998 } 1999 SPOT_ASSERT(false); 2000 return {}; 2001 } 2002 2003 /// \brief Check whether visiting *exactly* all sets \a inf 2004 /// infinitely often satisfies the acceptance condition. accepting(mark_t inf) const2005 bool accepting(mark_t inf) const 2006 { 2007 return code_.accepting(inf); 2008 } 2009 2010 /// \brief Assuming that we will visit at least all sets in \a 2011 /// inf, is there any chance that we will satisfy the condition? 2012 /// 2013 /// This return false only when it is sure that visiting more 2014 /// set will never make the condition satisfiable. inf_satisfiable(mark_t inf) const2015 bool inf_satisfiable(mark_t inf) const 2016 { 2017 return code_.inf_satisfiable(inf); 2018 } 2019 2020 /// \brief Check potential acceptance of an SCC. 2021 /// 2022 /// Assuming that an SCC intersects all sets in \a 2023 /// infinitely_often (i.e., for each set in \a infinitely_often, 2024 /// there exist one marked transition in the SCC), and is 2025 /// included in all sets in \a always_present (i.e., all 2026 /// transitions are marked with \a always_present), this returns 2027 /// one tree possible results: 2028 /// - trival::yes() the SCC is necessarily accepting, 2029 /// - trival::no() the SCC is necessarily rejecting, 2030 /// - trival::maybe() the SCC could contain an accepting cycle. maybe_accepting(mark_t infinitely_often,mark_t always_present) const2031 trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const 2032 { 2033 return code_.maybe_accepting(infinitely_often, always_present); 2034 } 2035 2036 /// \brief Return an accepting subset of \a inf 2037 /// 2038 /// This function works only on Fin-less acceptance, and returns a 2039 /// subset of \a inf that is enough to satisfy the acceptance 2040 /// condition. This is typically used when an accepting SCC that 2041 /// visits all sets in \a inf has been found, and we want to find 2042 /// an accepting cycle: maybe it is not necessary for the accepting 2043 /// cycle to intersect all sets in \a inf. 2044 /// 2045 /// This returns `mark_t({})` if \a inf does not satisfies the 2046 /// acceptance condition, or if the acceptance condition is `t`. 2047 /// So usually you should only use this method in cases you know 2048 /// that the condition is satisfied. 2049 mark_t accepting_sets(mark_t inf) const; 2050 2051 // Deprecated since Spot 2.8 2052 SPOT_DEPRECATED("Use operator<< instead.") format(std::ostream & os,mark_t m) const2053 std::ostream& format(std::ostream& os, mark_t m) const 2054 { 2055 if (!m) 2056 return os; 2057 return os << m; 2058 } 2059 2060 // Deprecated since Spot 2.8 2061 SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.") format(mark_t m) const2062 std::string format(mark_t m) const 2063 { 2064 std::ostringstream os; 2065 if (m) 2066 os << m; 2067 return os.str(); 2068 } 2069 2070 /// \brief The number of sets used in the acceptance condition. num_sets() const2071 unsigned num_sets() const 2072 { 2073 return num_; 2074 } 2075 2076 /// \brief Compute useless acceptance sets given a list of mark_t 2077 /// that occur in an SCC. 2078 /// 2079 /// Assuming that the condition is generalized Büchi using all 2080 /// declared sets, this scans all the mark_t between \a begin and 2081 /// \a end, and return the set of acceptance sets that are useless 2082 /// because they are always implied by other sets. 2083 template<class iterator> useless(iterator begin,iterator end) const2084 mark_t useless(iterator begin, iterator end) const 2085 { 2086 mark_t u = {}; // The set of useless sets 2087 for (unsigned x = 0; x < num_; ++x) 2088 { 2089 // Skip sets that are already known to be useless. 2090 if (u.has(x)) 2091 continue; 2092 auto all = comp(u | mark_t({x})); 2093 // Iterate over all mark_t, and keep track of 2094 // set numbers that always appear with x. 2095 for (iterator y = begin; y != end; ++y) 2096 { 2097 const mark_t& v = *y; 2098 if (v.has(x)) 2099 { 2100 all &= v; 2101 if (!all) 2102 break; 2103 } 2104 } 2105 u |= all; 2106 } 2107 return u; 2108 } 2109 2110 /// \brief Remove all the acceptance sets in \a rem. 2111 /// 2112 /// If \a missing is set, the acceptance sets are assumed to be 2113 /// missing from the automaton, and the acceptance is updated to 2114 /// reflect this. For instance `(Inf(1)&Inf(2))|Fin(3)` will 2115 /// become `Fin(3)` if we remove `2` because it is missing from this 2116 /// automaton. Indeed there is no way to fulfill `Inf(1)&Inf(2)` 2117 /// in this case. So essentially `missing=true` causes Inf(rem) to 2118 /// become `f`, and `Fin(rem)` to become `t`. 2119 /// 2120 /// If \a missing is unset, `Inf(rem)` become `t` while 2121 /// `Fin(rem)` become `f`. Removing `2` from 2122 /// `(Inf(1)&Inf(2))|Fin(3)` would then give `Inf(1)|Fin(3)`. remove(mark_t rem,bool missing) const2123 acc_cond remove(mark_t rem, bool missing) const 2124 { 2125 return {num_sets(), code_.remove(rem, missing)}; 2126 } 2127 2128 /// \brief Remove acceptance sets, and shift set numbers 2129 /// 2130 /// Same as remove, but also shift set numbers in the result so 2131 /// that all used set numbers are continuous. strip(mark_t rem,bool missing) const2132 acc_cond strip(mark_t rem, bool missing) const 2133 { 2134 return 2135 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) }; 2136 } 2137 2138 /// \brief For all `x` in \a m, replaces `Fin(x)` by `false`. force_inf(mark_t m) const2139 acc_cond force_inf(mark_t m) const 2140 { 2141 return {num_sets(), code_.force_inf(m)}; 2142 } 2143 2144 /// \brief Restrict an acceptance condition to a subset of set 2145 /// numbers that are occurring at some point. restrict_to(mark_t rem) const2146 acc_cond restrict_to(mark_t rem) const 2147 { 2148 return {num_sets(), code_.remove(all_sets() - rem, true)}; 2149 } 2150 2151 /// \brief Return the name of this acceptance condition, in the 2152 /// specified format. 2153 /// 2154 /// The empty string is returned if no name is known. 2155 /// 2156 /// \a fmt should be a combination of the following letters. (0) 2157 /// no parameters, (a) accentuated, (b) abbreviated, (d) style 2158 /// used in dot output, (g) no generalized parameter, (l) 2159 /// recognize Street-like and Rabin-like, (m) no main parameter, 2160 /// (p) no parity parameter, (o) name unknown acceptance as 2161 /// 'other', (s) shorthand for 'lo0'. 2162 std::string name(const char* fmt = "alo") const; 2163 2164 /// \brief Find a `Fin(i)` that is a unit clause. 2165 /// 2166 /// This return a mark_t `{i}` such that `Fin(i)` appears as a 2167 /// unit clause in the acceptance condition. I.e., either the 2168 /// condition is exactly `Fin(i)`, or the condition has the form 2169 /// `...&Fin(i)&...`. If there is no such `Fin(i)`, an empty 2170 /// mark_t is returned. 2171 /// 2172 /// If multiple unit-Fin appear as unit-clauses, the set of 2173 /// those will be returned. For instance applied to 2174 /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))``, this will return `{0,1}`. fin_unit() const2175 mark_t fin_unit() const 2176 { 2177 return code_.fin_unit(); 2178 } 2179 2180 /// \brief Find a `Inf(i)` that is a unit clause. 2181 /// 2182 /// This return a mark_t `{i}` such that `Inf(i)` appears as a 2183 /// unit clause in the acceptance condition. I.e., either the 2184 /// condition is exactly `Inf(i)`, or the condition has the form 2185 /// `...&Inf(i)&...`. If there is no such `Inf(i)`, an empty 2186 /// mark_t is returned. 2187 /// 2188 /// If multiple unit-Inf appear as unit-clauses, the set of 2189 /// those will be returned. For instance applied to 2190 /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. inf_unit() const2191 mark_t inf_unit() const 2192 { 2193 return code_.inf_unit(); 2194 } 2195 2196 /// \brief Return one acceptance set i that appear as `Fin(i)` 2197 /// in the condition. 2198 /// 2199 /// Return -1 if no such set exist. fin_one() const2200 int fin_one() const 2201 { 2202 return code_.fin_one(); 2203 } 2204 2205 /// \brief Return one acceptance set i that appears as `Fin(i)` 2206 /// in the condition, and all disjuncts containing it. 2207 /// 2208 /// If the condition is a disjunction and one of the disjunct 2209 /// has the shape `...&Fin(i)&...`, then `i` will be prefered 2210 /// over any arbitrary Fin. 2211 /// 2212 /// The second element of the pair, is the same acceptance 2213 /// condition in which all top-level disjunct not featuring 2214 /// `Fin(i)` have been removed. 2215 /// 2216 /// For example on 2217 /// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` 2218 /// the output would be the pair 2219 /// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. 2220 /// On that example `Fin(1)` is prefered to `Fin(7)` because 2221 /// it appears at the top-level. fin_one_extract() const2222 std::pair<int, acc_cond> fin_one_extract() const 2223 { 2224 auto [f, c] = code_.fin_one_extract(); 2225 return {f, {num_sets(), std::move(c)}}; 2226 } 2227 2228 /// \brief Return the top-level disjuncts. 2229 /// 2230 /// For instance, if the formula is 2231 /// (5, Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4)))), this returns 2232 /// [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)|Fin(4)))]. 2233 /// 2234 /// If the formula is not a disjunction, this returns 2235 /// a vector with the formula as only element. 2236 std::vector<acc_cond> top_disjuncts() const; 2237 2238 /// \brief Return the top-level conjuncts. 2239 /// 2240 /// For instance, if the formula is 2241 /// (5, Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4)))), this returns 2242 /// [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)|Fin(4)))]. 2243 /// 2244 /// If the formula is not a conjunction, this returns 2245 /// a vector with the formula as only element. 2246 std::vector<acc_cond> top_conjuncts() const; 2247 2248 protected: all_sets_() const2249 mark_t all_sets_() const 2250 { 2251 return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_); 2252 } 2253 2254 unsigned num_; 2255 mark_t all_; 2256 acc_code code_; 2257 bool uses_fin_acceptance_ = false; 2258 2259 }; 2260 2261 struct rs_pairs_view { 2262 typedef std::vector<acc_cond::rs_pair> rs_pairs; 2263 2264 // Creates view of pairs 'p' with restriction only to marks in 'm' rs_pairs_viewspot::rs_pairs_view2265 explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m) 2266 : pairs_(p), view_marks_(m) {} 2267 2268 // Creates view of pairs without restriction to marks rs_pairs_viewspot::rs_pairs_view2269 explicit rs_pairs_view(const rs_pairs& p) 2270 : rs_pairs_view(p, acc_cond::mark_t::all()) {} 2271 infsspot::rs_pairs_view2272 acc_cond::mark_t infs() const 2273 { 2274 return do_view([&](const acc_cond::rs_pair& p) 2275 { 2276 return visible(p.inf) ? p.inf : acc_cond::mark_t({}); 2277 }); 2278 } 2279 finsspot::rs_pairs_view2280 acc_cond::mark_t fins() const 2281 { 2282 return do_view([&](const acc_cond::rs_pair& p) 2283 { 2284 return visible(p.fin) ? p.fin : acc_cond::mark_t({}); 2285 }); 2286 } 2287 fins_alonespot::rs_pairs_view2288 acc_cond::mark_t fins_alone() const 2289 { 2290 return do_view([&](const acc_cond::rs_pair& p) 2291 { 2292 return !visible(p.inf) && visible(p.fin) ? p.fin 2293 : acc_cond::mark_t({}); 2294 }); 2295 } 2296 infs_alonespot::rs_pairs_view2297 acc_cond::mark_t infs_alone() const 2298 { 2299 return do_view([&](const acc_cond::rs_pair& p) 2300 { 2301 return !visible(p.fin) && visible(p.inf) ? p.inf 2302 : acc_cond::mark_t({}); 2303 }); 2304 } 2305 paired_with_finspot::rs_pairs_view2306 acc_cond::mark_t paired_with_fin(unsigned mark) const 2307 { 2308 acc_cond::mark_t res = {}; 2309 for (const auto& p: pairs_) 2310 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf)) 2311 res |= p.inf; 2312 return res; 2313 } 2314 pairsspot::rs_pairs_view2315 const rs_pairs& pairs() const 2316 { 2317 return pairs_; 2318 } 2319 2320 private: 2321 template<typename filter> do_viewspot::rs_pairs_view2322 acc_cond::mark_t do_view(const filter& filt) const 2323 { 2324 acc_cond::mark_t res = {}; 2325 for (const auto& p: pairs_) 2326 res |= filt(p); 2327 return res; 2328 } 2329 visiblespot::rs_pairs_view2330 bool visible(const acc_cond::mark_t& v) const 2331 { 2332 return !!(view_marks_ & v); 2333 } 2334 2335 const rs_pairs& pairs_; 2336 acc_cond::mark_t view_marks_; 2337 }; 2338 2339 2340 SPOT_API 2341 std::ostream& operator<<(std::ostream& os, const acc_cond& acc); 2342 2343 /// @} 2344 2345 namespace internal 2346 { 2347 class SPOT_API mark_iterator 2348 { 2349 public: 2350 typedef unsigned value_type; 2351 typedef const value_type& reference; 2352 typedef const value_type* pointer; 2353 typedef std::ptrdiff_t difference_type; 2354 typedef std::forward_iterator_tag iterator_category; 2355 mark_iterator()2356 mark_iterator() noexcept 2357 : m_({}) 2358 { 2359 } 2360 mark_iterator(acc_cond::mark_t m)2361 mark_iterator(acc_cond::mark_t m) noexcept 2362 : m_(m) 2363 { 2364 } 2365 operator ==(mark_iterator m) const2366 bool operator==(mark_iterator m) const 2367 { 2368 return m_ == m.m_; 2369 } 2370 operator !=(mark_iterator m) const2371 bool operator!=(mark_iterator m) const 2372 { 2373 return m_ != m.m_; 2374 } 2375 operator *() const2376 value_type operator*() const 2377 { 2378 SPOT_ASSERT(m_); 2379 return m_.min_set() - 1; 2380 } 2381 operator ++()2382 mark_iterator& operator++() 2383 { 2384 m_.clear(this->operator*()); 2385 return *this; 2386 } 2387 operator ++(int)2388 mark_iterator operator++(int) 2389 { 2390 mark_iterator it = *this; 2391 ++(*this); 2392 return it; 2393 } 2394 private: 2395 acc_cond::mark_t m_; 2396 }; 2397 2398 class SPOT_API mark_container 2399 { 2400 public: mark_container(spot::acc_cond::mark_t m)2401 mark_container(spot::acc_cond::mark_t m) noexcept 2402 : m_(m) 2403 { 2404 } 2405 begin() const2406 mark_iterator begin() const 2407 { 2408 return {m_}; 2409 } end() const2410 mark_iterator end() const 2411 { 2412 return {}; 2413 } 2414 private: 2415 spot::acc_cond::mark_t m_; 2416 }; 2417 } 2418 sets() const2419 inline spot::internal::mark_container acc_cond::mark_t::sets() const 2420 { 2421 return {*this}; 2422 } 2423 2424 inline acc_cond::mark_t apply_permutation(std::vector<unsigned> permut)2425 acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut) 2426 { 2427 mark_t result { }; 2428 for (auto color : sets()) 2429 if (color < permut.size()) 2430 result.set(permut[color]); 2431 return result; 2432 } 2433 } 2434 2435 namespace std 2436 { 2437 template<> 2438 struct hash<spot::acc_cond::mark_t> 2439 { operator ()std::hash2440 size_t operator()(spot::acc_cond::mark_t m) const noexcept 2441 { 2442 return m.hash(); 2443 } 2444 }; 2445 } 2446