1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2015-2021 Laboratoire de Recherche et Développement 3 // de l'Epita (LRDE). 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 /// \file tl/formula.hh 21 /// \brief LTL/PSL formula interface 22 #pragma once 23 24 /// \defgroup tl Temporal Logic 25 /// 26 /// Spot supports the future-time fragment of LTL, and the linear-time 27 /// fragment of and PSL formulas. The former is included in the 28 /// latter. Both types of formulas are represented by instances of 29 /// the spot::formula class. 30 31 /// \addtogroup tl_essentials Essential Temporal Logic Types 32 /// \ingroup tl 33 34 /// \addtogroup tl_io Input and Output of Formulas 35 /// \ingroup tl 36 37 /// \addtogroup tl_rewriting Rewriting Algorithms for Formulas 38 /// \ingroup tl 39 40 /// \addtogroup tl_hier Algorithms related to the temporal hierarchy 41 /// \ingroup tl 42 43 /// \addtogroup tl_misc Miscellaneous Algorithms for Formulas 44 /// \ingroup tl 45 46 #include <spot/misc/common.hh> 47 #include <memory> 48 #include <cstdint> 49 #include <initializer_list> 50 #include <cassert> 51 #include <vector> 52 #include <string> 53 #include <iterator> 54 #include <iosfwd> 55 #include <sstream> 56 #include <list> 57 #include <cstddef> 58 #include <limits> 59 60 // The strong_X operator was introduced in Spot 2.8.2 to fix an issue 61 // with from_ltlf(). As adding a new operator is a backward 62 // incompatibility, causing new warnings from the compiler. 63 #if defined(SPOT_BUILD) or defined(SPOT_USES_STRONG_X) 64 // Use #if SPOT_HAS_STRONG_X in code that need to be backward 65 // compatible with older Spot versions. 66 # define SPOT_HAS_STRONG_X 1 67 // You me #define SPOT_WANT_STRONG_X yourself before including 68 // this file to force the use of STRONG_X 69 # define SPOT_WANT_STRONG_X 1 70 #endif 71 72 namespace spot 73 { 74 75 76 /// \ingroup tl_essentials 77 /// \brief Operator types 78 enum class op: uint8_t 79 { 80 ff, ///< False 81 tt, ///< True 82 eword, ///< Empty word 83 ap, ///< Atomic proposition 84 // unary operators 85 Not, ///< Negation 86 X, ///< Next 87 F, ///< Eventually 88 G, ///< Globally 89 Closure, ///< PSL Closure 90 NegClosure, ///< Negated PSL Closure 91 NegClosureMarked, ///< marked version of the Negated PSL Closure 92 // binary operators 93 Xor, ///< Exclusive Or 94 Implies, ///< Implication 95 Equiv, ///< Equivalence 96 U, ///< until 97 R, ///< release (dual of until) 98 W, ///< weak until 99 M, ///< strong release (dual of weak until) 100 EConcat, ///< Seq 101 EConcatMarked, ///< Seq, Marked 102 UConcat, ///< Triggers 103 // n-ary operators 104 Or, ///< (omega-Rational) Or 105 OrRat, ///< Rational Or 106 And, ///< (omega-Rational) And 107 AndRat, ///< Rational And 108 AndNLM, ///< Non-Length-Matching Rational-And 109 Concat, ///< Concatenation 110 Fusion, ///< Fusion 111 // star-like operators 112 Star, ///< Star 113 FStar, ///< Fustion Star 114 first_match, ///< first_match(sere) 115 #ifdef SPOT_WANT_STRONG_X 116 strong_X, ///< strong Next 117 #endif 118 }; 119 120 #ifndef SWIG 121 /// \brief Actual storage for formula nodes. 122 /// 123 /// spot::formula objects contain references to instances of this 124 /// class, and delegate most of their methods. Because 125 /// spot::formula is meant to be the public interface, most of the 126 /// methods are documented there, rather than here. 127 class SPOT_API fnode final 128 { 129 public: 130 /// \brief Clone an fnode. 131 /// 132 /// This simply increment the reference counter. If the counter 133 /// saturates, the fnode will stay permanently allocated. clone() const134 const fnode* clone() const 135 { 136 // Saturate. 137 ++refs_; 138 if (SPOT_UNLIKELY(!refs_)) 139 saturated_ = 1; 140 return this; 141 } 142 143 /// \brief Dereference an fnode. 144 /// 145 /// This decrement the reference counter (unless the counter is 146 /// saturated), and actually deallocate the fnode when the 147 /// counder reaches 0 (unless the fnode denotes a constant). destroy() const148 void destroy() const 149 { 150 if (SPOT_LIKELY(refs_)) 151 --refs_; 152 else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_)) 153 // last reference to a node that is not a constant 154 destroy_aux(); 155 } 156 157 /// \see formula::unbounded unbounded()158 static constexpr uint8_t unbounded() 159 { 160 return UINT8_MAX; 161 } 162 163 /// \see formula::ap 164 static const fnode* ap(const std::string& name); 165 /// \see formula::unop 166 static const fnode* unop(op o, const fnode* f); 167 /// \see formula::binop 168 static const fnode* binop(op o, const fnode* f, const fnode* g); 169 /// \see formula::multop 170 static const fnode* multop(op o, std::vector<const fnode*> l); 171 /// \see formula::bunop 172 static const fnode* bunop(op o, const fnode* f, 173 unsigned min, unsigned max = unbounded()); 174 175 /// \see formula::nested_unop_range 176 static const fnode* nested_unop_range(op uo, op bo, unsigned min, 177 unsigned max, const fnode* f); 178 179 /// \see formula::kind kind() const180 op kind() const 181 { 182 return op_; 183 } 184 185 /// \see formula::kindstr 186 std::string kindstr() const; 187 188 /// \see formula::is 189 /// @{ is(op o) const190 bool is(op o) const 191 { 192 return op_ == o; 193 } 194 is(op o1,op o2) const195 bool is(op o1, op o2) const 196 { 197 return op_ == o1 || op_ == o2; 198 } 199 is(op o1,op o2,op o3) const200 bool is(op o1, op o2, op o3) const 201 { 202 return op_ == o1 || op_ == o2 || op_ == o3; 203 } 204 is(op o1,op o2,op o3,op o4) const205 bool is(op o1, op o2, op o3, op o4) const 206 { 207 return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4; 208 } 209 is(std::initializer_list<op> l) const210 bool is(std::initializer_list<op> l) const 211 { 212 const fnode* n = this; 213 for (auto o: l) 214 { 215 if (!n->is(o)) 216 return false; 217 n = n->nth(0); 218 } 219 return true; 220 } 221 /// @} 222 223 /// \see formula::get_child_of get_child_of(op o) const224 const fnode* get_child_of(op o) const 225 { 226 if (op_ != o) 227 return nullptr; 228 if (SPOT_UNLIKELY(size_ != 1)) 229 report_get_child_of_expecting_single_child_node(); 230 return nth(0); 231 } 232 233 /// \see formula::get_child_of get_child_of(std::initializer_list<op> l) const234 const fnode* get_child_of(std::initializer_list<op> l) const 235 { 236 auto c = this; 237 for (auto o: l) 238 { 239 c = c->get_child_of(o); 240 if (c == nullptr) 241 return c; 242 } 243 return c; 244 } 245 246 /// \see formula::min min() const247 unsigned min() const 248 { 249 if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star)) 250 report_min_invalid_arg(); 251 return min_; 252 } 253 254 /// \see formula::max max() const255 unsigned max() const 256 { 257 if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star)) 258 report_max_invalid_arg(); 259 return max_; 260 } 261 262 /// \see formula::size size() const263 unsigned size() const 264 { 265 return size_; 266 } 267 268 /// \see formula::is_leaf is_leaf() const269 bool is_leaf() const 270 { 271 return size_ == 0; 272 } 273 274 /// \see formula::id id() const275 size_t id() const 276 { 277 return id_; 278 } 279 280 /// \see formula::begin begin() const281 const fnode*const* begin() const 282 { 283 return children; 284 } 285 286 /// \see formula::end end() const287 const fnode*const* end() const 288 { 289 return children + size(); 290 } 291 292 /// \see formula::nth nth(unsigned i) const293 const fnode* nth(unsigned i) const 294 { 295 if (SPOT_UNLIKELY(i >= size())) 296 report_non_existing_child(); 297 return children[i]; 298 } 299 300 /// \see formula::ff ff()301 static const fnode* ff() 302 { 303 return ff_; 304 } 305 306 /// \see formula::is_ff is_ff() const307 bool is_ff() const 308 { 309 return op_ == op::ff; 310 } 311 312 /// \see formula::tt tt()313 static const fnode* tt() 314 { 315 return tt_; 316 } 317 318 /// \see formula::is_tt is_tt() const319 bool is_tt() const 320 { 321 return op_ == op::tt; 322 } 323 324 /// \see formula::eword eword()325 static const fnode* eword() 326 { 327 return ew_; 328 } 329 330 /// \see formula::is_eword is_eword() const331 bool is_eword() const 332 { 333 return op_ == op::eword; 334 } 335 336 /// \see formula::is_constant is_constant() const337 bool is_constant() const 338 { 339 return op_ == op::ff || op_ == op::tt || op_ == op::eword; 340 } 341 342 /// \see formula::is_Kleene_star is_Kleene_star() const343 bool is_Kleene_star() const 344 { 345 if (op_ != op::Star) 346 return false; 347 return min_ == 0 && max_ == unbounded(); 348 } 349 350 /// \see formula::one_star one_star()351 static const fnode* one_star() 352 { 353 if (!one_star_) 354 one_star_ = bunop(op::Star, tt(), 0); 355 return one_star_; 356 } 357 358 /// \see formula::ap_name 359 const std::string& ap_name() const; 360 361 /// \see formula::dump 362 std::ostream& dump(std::ostream& os) const; 363 364 /// \see formula::all_but 365 const fnode* all_but(unsigned i) const; 366 367 /// \see formula::boolean_count boolean_count() const368 unsigned boolean_count() const 369 { 370 unsigned pos = 0; 371 unsigned s = size(); 372 while (pos < s && children[pos]->is_boolean()) 373 ++pos; 374 return pos; 375 } 376 377 /// \see formula::boolean_operands 378 const fnode* boolean_operands(unsigned* width = nullptr) const; 379 380 /// \brief safety check for the reference counters 381 /// 382 /// \return true iff the unicity map contains only the globally 383 /// pre-allocated formulas. 384 /// 385 /// This is meant to be used as 386 /// \code 387 /// assert(spot::fnode::instances_check()); 388 /// \endcode 389 /// at the end of a program. 390 static bool instances_check(); 391 392 //////////////// 393 // Properties // 394 //////////////// 395 396 /// \see formula::is_boolean is_boolean() const397 bool is_boolean() const 398 { 399 return is_.boolean; 400 } 401 402 /// \see formula::is_sugar_free_boolean is_sugar_free_boolean() const403 bool is_sugar_free_boolean() const 404 { 405 return is_.sugar_free_boolean; 406 } 407 408 /// \see formula::is_in_nenoform is_in_nenoform() const409 bool is_in_nenoform() const 410 { 411 return is_.in_nenoform; 412 } 413 414 /// \see formula::is_syntactic_stutter_invariant is_syntactic_stutter_invariant() const415 bool is_syntactic_stutter_invariant() const 416 { 417 return is_.syntactic_si; 418 } 419 420 /// \see formula::is_sugar_free_ltl is_sugar_free_ltl() const421 bool is_sugar_free_ltl() const 422 { 423 return is_.sugar_free_ltl; 424 } 425 426 /// \see formula::is_ltl_formula is_ltl_formula() const427 bool is_ltl_formula() const 428 { 429 return is_.ltl_formula; 430 } 431 432 /// \see formula::is_psl_formula is_psl_formula() const433 bool is_psl_formula() const 434 { 435 return is_.psl_formula; 436 } 437 438 /// \see formula::is_sere_formula is_sere_formula() const439 bool is_sere_formula() const 440 { 441 return is_.sere_formula; 442 } 443 444 /// \see formula::is_finite is_finite() const445 bool is_finite() const 446 { 447 return is_.finite; 448 } 449 450 /// \see formula::is_eventual is_eventual() const451 bool is_eventual() const 452 { 453 return is_.eventual; 454 } 455 456 /// \see formula::is_universal is_universal() const457 bool is_universal() const 458 { 459 return is_.universal; 460 } 461 462 /// \see formula::is_syntactic_safety is_syntactic_safety() const463 bool is_syntactic_safety() const 464 { 465 return is_.syntactic_safety; 466 } 467 468 /// \see formula::is_syntactic_guarantee is_syntactic_guarantee() const469 bool is_syntactic_guarantee() const 470 { 471 return is_.syntactic_guarantee; 472 } 473 474 /// \see formula::is_syntactic_obligation is_syntactic_obligation() const475 bool is_syntactic_obligation() const 476 { 477 return is_.syntactic_obligation; 478 } 479 480 /// \see formula::is_syntactic_recurrence is_syntactic_recurrence() const481 bool is_syntactic_recurrence() const 482 { 483 return is_.syntactic_recurrence; 484 } 485 486 /// \see formula::is_syntactic_persistence is_syntactic_persistence() const487 bool is_syntactic_persistence() const 488 { 489 return is_.syntactic_persistence; 490 } 491 492 /// \see formula::is_marked is_marked() const493 bool is_marked() const 494 { 495 return !is_.not_marked; 496 } 497 498 /// \see formula::accepts_eword accepts_eword() const499 bool accepts_eword() const 500 { 501 return is_.accepting_eword; 502 } 503 504 /// \see formula::has_lbt_atomic_props has_lbt_atomic_props() const505 bool has_lbt_atomic_props() const 506 { 507 return is_.lbt_atomic_props; 508 } 509 510 /// \see formula::has_spin_atomic_props has_spin_atomic_props() const511 bool has_spin_atomic_props() const 512 { 513 return is_.spin_atomic_props; 514 } 515 516 private: 517 static size_t bump_next_id(); 518 void setup_props(op o); 519 void destroy_aux() const; 520 521 [[noreturn]] static void report_non_existing_child(); 522 [[noreturn]] static void report_too_many_children(); 523 [[noreturn]] static void 524 report_get_child_of_expecting_single_child_node(); 525 [[noreturn]] static void report_min_invalid_arg(); 526 [[noreturn]] static void report_max_invalid_arg(); 527 528 static const fnode* unique(fnode*); 529 530 // Destruction may only happen via destroy(). 531 ~fnode() = default; 532 // Disallow copies. 533 fnode(const fnode&) = delete; 534 fnode& operator=(const fnode&) = delete; 535 536 537 538 template<class iter> fnode(op o,iter begin,iter end)539 fnode(op o, iter begin, iter end) 540 // Clang has some optimization where is it able to combine the 541 // 4 movb initializing op_,min_,max_,saturated_ into a single 542 // movl. Also it can optimize the three byte-comparisons of 543 // is_Kleene_star() into a single masked 32-bit comparison. 544 // The latter optimization triggers warnings from valgrind if 545 // min_ and max_ are not initialized. So to benefit from the 546 // initialization optimization and the is_Kleene_star() 547 // optimization in Clang, we always initialize min_ and max_ 548 // with this compiler. Do not do it the rest of the time, 549 // since the optimization is not done. 550 : op_(o), 551 #if __llvm__ 552 min_(0), max_(0), 553 #endif 554 saturated_(0) 555 { 556 size_t s = std::distance(begin, end); 557 if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX)) 558 report_too_many_children(); 559 size_ = s; 560 auto pos = children; 561 for (auto i = begin; i != end; ++i) 562 *pos++ = *i; 563 setup_props(o); 564 } 565 fnode(op o,std::initializer_list<const fnode * > l)566 fnode(op o, std::initializer_list<const fnode*> l) 567 : fnode(o, l.begin(), l.end()) 568 { 569 } 570 fnode(op o,const fnode * f,uint8_t min,uint8_t max)571 fnode(op o, const fnode* f, uint8_t min, uint8_t max) 572 : op_(o), min_(min), max_(max), saturated_(0), size_(1) 573 { 574 children[0] = f; 575 setup_props(o); 576 } 577 578 static const fnode* ff_; 579 static const fnode* tt_; 580 static const fnode* ew_; 581 static const fnode* one_star_; 582 583 op op_; // operator 584 uint8_t min_; // range minimum (for star-like operators) 585 uint8_t max_; // range maximum; 586 mutable uint8_t saturated_; 587 uint16_t size_; // number of children 588 mutable uint16_t refs_ = 0; // reference count - 1; 589 size_t id_; // Also used as hash. 590 static size_t next_id_; 591 592 struct ltl_prop 593 { 594 // All properties here should be expressed in such a a way 595 // that property(f && g) is just property(f)&property(g). 596 // This allows us to compute all properties of a compound 597 // formula in one operation. 598 // 599 // For instance we do not use a property that says "has 600 // temporal operator", because it would require an OR between 601 // the two arguments. Instead we have a property that 602 // says "no temporal operator", and that one is computed 603 // with an AND between the arguments. 604 // 605 // Also choose a name that makes sense when prefixed with 606 // "the formula is". 607 bool boolean:1; // No temporal operators. 608 bool sugar_free_boolean:1; // Only AND, OR, and NOT operators. 609 bool in_nenoform:1; // Negative Normal Form. 610 bool syntactic_si:1; // LTL-X or siPSL 611 bool sugar_free_ltl:1; // No F and G operators. 612 bool ltl_formula:1; // Only LTL operators. 613 bool psl_formula:1; // Only PSL operators. 614 bool sere_formula:1; // Only SERE operators. 615 bool finite:1; // Finite SERE formulae, or Bool+X forms. 616 bool eventual:1; // Purely eventual formula. 617 bool universal:1; // Purely universal formula. 618 bool syntactic_safety:1; // Syntactic Safety Property. 619 bool syntactic_guarantee:1; // Syntactic Guarantee Property. 620 bool syntactic_obligation:1; // Syntactic Obligation Property. 621 bool syntactic_recurrence:1; // Syntactic Recurrence Property. 622 bool syntactic_persistence:1; // Syntactic Persistence Property. 623 bool not_marked:1; // No occurrence of EConcatMarked. 624 bool accepting_eword:1; // Accepts the empty word. 625 bool lbt_atomic_props:1; // Use only atomic propositions like p42. 626 bool spin_atomic_props:1; // Use only spin-compatible atomic props. 627 }; 628 union 629 { 630 // Use an unsigned for fast computation of all properties. 631 unsigned props; 632 ltl_prop is_; 633 }; 634 635 const fnode* children[1]; 636 }; 637 638 /// Order two atomic propositions. 639 SPOT_API 640 int atomic_prop_cmp(const fnode* f, const fnode* g); 641 642 struct formula_ptr_less_than_bool_first 643 { 644 bool operator ()spot::formula_ptr_less_than_bool_first645 operator()(const fnode* left, const fnode* right) const 646 { 647 SPOT_ASSERT(left); 648 SPOT_ASSERT(right); 649 if (left == right) 650 return false; 651 652 // We want Boolean formulae first. 653 bool lib = left->is_boolean(); 654 if (lib != right->is_boolean()) 655 return lib; 656 657 // We have two Boolean formulae 658 if (lib) 659 { 660 bool lconst = left->is_constant(); 661 if (lconst != right->is_constant()) 662 return lconst; 663 if (!lconst) 664 { 665 auto get_literal = [](const fnode* f) -> const fnode* 666 { 667 if (f->is(op::Not)) 668 f = f->nth(0); 669 if (f->is(op::ap)) 670 return f; 671 return nullptr; 672 }; 673 // Literals should come first 674 const fnode* litl = get_literal(left); 675 const fnode* litr = get_literal(right); 676 if (!litl != !litr) 677 return litl; 678 if (litl) 679 { 680 // And they should be sorted alphabetically 681 int cmp = atomic_prop_cmp(litl, litr); 682 if (cmp) 683 return cmp < 0; 684 } 685 } 686 } 687 688 size_t l = left->id(); 689 size_t r = right->id(); 690 if (l != r) 691 return l < r; 692 // Because the hash code assigned to each formula is the 693 // number of formulae constructed so far, it is very unlikely 694 // that we will ever reach a case were two different formulae 695 // have the same hash. This will happen only ever with have 696 // produced 256**sizeof(size_t) formulae (i.e. max_count has 697 // looped back to 0 and started over). In that case we can 698 // order two formulas by looking at their text representation. 699 // We could be more efficient and look at their AST, but it's 700 // not worth the burden. (Also ordering pointers is ruled out 701 // because it breaks the determinism of the implementation.) 702 std::ostringstream old; 703 left->dump(old); 704 std::ostringstream ord; 705 right->dump(ord); 706 return old.str() < ord.str(); 707 } 708 }; 709 710 #endif // SWIG 711 712 /// \ingroup tl_essentials 713 /// \brief Main class for temporal logic formula 714 class SPOT_API formula final 715 { 716 const fnode* ptr_; 717 public: 718 /// \brief Create a formula from an fnode. 719 /// 720 /// This constructor is mainly for internal use, as spot::fnode 721 /// object should usually not be manipulated from user code. formula(const fnode * f)722 explicit formula(const fnode* f) noexcept 723 : ptr_(f) 724 { 725 } 726 727 /// \brief Create a null formula. 728 /// 729 /// This could be used to default-initialize a formula, however 730 /// null formula should be short lived: most algorithms and member 731 /// functions assume that formulas should not be null. formula(std::nullptr_t)732 formula(std::nullptr_t) noexcept 733 : ptr_(nullptr) 734 { 735 } 736 737 /// \brief Default initialize a formula to nullptr. formula()738 formula() noexcept 739 : ptr_(nullptr) 740 { 741 } 742 743 /// Clone a formula. formula(const formula & f)744 formula(const formula& f) noexcept 745 : ptr_(f.ptr_) 746 { 747 if (ptr_) 748 ptr_->clone(); 749 } 750 751 /// Move-construct a formula. formula(formula && f)752 formula(formula&& f) noexcept 753 : ptr_(f.ptr_) 754 { 755 f.ptr_ = nullptr; 756 } 757 758 /// Destroy a formula. ~formula()759 ~formula() 760 { 761 if (ptr_) 762 ptr_->destroy(); 763 } 764 765 /// \brief Reset a formula to null 766 /// 767 /// Note that null formula should be short lived: most algorithms 768 /// and member function assume that formulas should not be null. 769 /// Assigning nullptr to a formula can be useful when cleaning an 770 /// array of formula using multiple passes and marking some 771 /// formula as nullptr before actually erasing them. operator =(std::nullptr_t)772 const formula& operator=(std::nullptr_t) 773 { 774 this->~formula(); 775 ptr_ = nullptr; 776 return *this; 777 } 778 operator =(const formula & f)779 const formula& operator=(const formula& f) 780 { 781 this->~formula(); 782 if ((ptr_ = f.ptr_)) 783 ptr_->clone(); 784 return *this; 785 } 786 operator =(formula && f)787 const formula& operator=(formula&& f) noexcept 788 { 789 std::swap(f.ptr_, ptr_); 790 return *this; 791 } 792 operator <(const formula & other) const793 bool operator<(const formula& other) const noexcept 794 { 795 if (SPOT_UNLIKELY(!other.ptr_)) 796 return false; 797 if (SPOT_UNLIKELY(!ptr_)) 798 return true; 799 if (id() < other.id()) 800 return true; 801 if (id() > other.id()) 802 return false; 803 // The case where id()==other.id() but ptr_ != other.ptr_ is 804 // very unlikely (we would need to build more than UINT_MAX 805 // formulas), so let's just compare pointers, and ignore the 806 // fact that it may introduce some nondeterminism. 807 return ptr_ < other.ptr_; 808 } 809 operator <=(const formula & other) const810 bool operator<=(const formula& other) const noexcept 811 { 812 return *this == other || *this < other; 813 } 814 operator >(const formula & other) const815 bool operator>(const formula& other) const noexcept 816 { 817 return !(*this <= other); 818 } 819 operator >=(const formula & other) const820 bool operator>=(const formula& other) const noexcept 821 { 822 return !(*this < other); 823 } 824 operator ==(const formula & other) const825 bool operator==(const formula& other) const noexcept 826 { 827 return other.ptr_ == ptr_; 828 } 829 operator ==(std::nullptr_t) const830 bool operator==(std::nullptr_t) const noexcept 831 { 832 return ptr_ == nullptr; 833 } 834 operator !=(const formula & other) const835 bool operator!=(const formula& other) const noexcept 836 { 837 return other.ptr_ != ptr_; 838 } 839 operator !=(std::nullptr_t) const840 bool operator!=(std::nullptr_t) const noexcept 841 { 842 return ptr_ != nullptr; 843 } 844 operator bool() const845 explicit operator bool() const noexcept 846 { 847 return ptr_ != nullptr; 848 } 849 850 ///////////////////////// 851 // Forwarded functions // 852 ///////////////////////// 853 854 /// Unbounded constant to use as end of range for bounded operators. unbounded()855 static constexpr uint8_t unbounded() 856 { 857 return fnode::unbounded(); 858 } 859 860 /// Build an atomic proposition. ap(const std::string & name)861 static formula ap(const std::string& name) 862 { 863 return formula(fnode::ap(name)); 864 } 865 866 /// \brief Build an atomic proposition from... an atomic proposition. 867 /// 868 /// The only practical interest of this methods is for the Python 869 /// bindings, where ap() can therefore work both from string or 870 /// atomic propositions. ap(const formula & a)871 static formula ap(const formula& a) 872 { 873 if (SPOT_UNLIKELY(a.kind() != op::ap)) 874 report_ap_invalid_arg(); 875 return a; 876 } 877 878 /// \brief Build a unary operator. 879 /// \pre \a o should be one of op::Not, op::X, op::F, op::G, 880 /// op::Closure, op::NegClosure, op::NegClosureMarked. 881 /// @{ unop(op o,const formula & f)882 static formula unop(op o, const formula& f) 883 { 884 return formula(fnode::unop(o, f.ptr_->clone())); 885 } 886 887 #ifndef SWIG unop(op o,formula && f)888 static formula unop(op o, formula&& f) 889 { 890 return formula(fnode::unop(o, f.to_node_())); 891 } 892 #endif // !SWIG 893 /// @} 894 895 #ifdef SWIG 896 #define SPOT_DEF_UNOP(Name) \ 897 static formula Name(const formula& f) \ 898 { \ 899 return unop(op::Name, f); \ 900 } 901 #else // !SWIG 902 #define SPOT_DEF_UNOP(Name) \ 903 static formula Name(const formula& f) \ 904 { \ 905 return unop(op::Name, f); \ 906 } \ 907 static formula Name(formula&& f) \ 908 { \ 909 return unop(op::Name, std::move(f)); \ 910 } 911 #endif // !SWIG 912 /// \brief Construct a negation 913 /// @{ 914 SPOT_DEF_UNOP(Not); 915 /// @} 916 917 /// \brief Construct an X 918 /// @{ 919 SPOT_DEF_UNOP(X); 920 /// @} 921 922 /// \brief Construct an X[n] 923 /// 924 /// X[3]f = XXXf X(unsigned level,const formula & f)925 static formula X(unsigned level, const formula& f) 926 { 927 return nested_unop_range(op::X, op::Or /* unused */, level, level, f); 928 } 929 930 #if SPOT_WANT_STRONG_X 931 /// \brief Construct a strong_X 932 /// @{ 933 SPOT_DEF_UNOP(strong_X); 934 /// @} 935 936 /// \brief Construct a strong_X[n] 937 /// 938 /// strong_X[3]f = strong_X strong_X strong_X f strong_X(unsigned level,const formula & f)939 static formula strong_X(unsigned level, const formula& f) 940 { 941 return nested_unop_range(op::strong_X, op::Or /* unused */, 942 level, level, f); 943 } 944 #endif 945 946 /// \brief Construct an F 947 /// @{ 948 SPOT_DEF_UNOP(F); 949 /// @} 950 951 /// \brief Construct F[n:m] 952 /// 953 /// F[2:3]a = XX(a | Xa) 954 /// F[2:$]a = XXFa 955 /// 956 /// This syntax is from TSLF; the operator is called next_e![n..m] in PSL. F(unsigned min_level,unsigned max_level,const formula & f)957 static formula F(unsigned min_level, unsigned max_level, const formula& f) 958 { 959 return nested_unop_range(op::X, op::Or, min_level, max_level, f); 960 } 961 962 /// \brief Construct G[n:m] 963 /// 964 /// G[2:3]a = XX(a & Xa) 965 /// G[2:$]a = XXGa 966 /// 967 /// This syntax is from TSLF; the operator is called next_a![n..m] in PSL. G(unsigned min_level,unsigned max_level,const formula & f)968 static formula G(unsigned min_level, unsigned max_level, const formula& f) 969 { 970 return nested_unop_range(op::X, op::And, min_level, max_level, f); 971 } 972 973 /// \brief Construct a G 974 /// @{ 975 SPOT_DEF_UNOP(G); 976 /// @} 977 978 /// \brief Construct a PSL Closure 979 /// @{ 980 SPOT_DEF_UNOP(Closure); 981 /// @} 982 983 /// \brief Construct a negated PSL Closure 984 /// @{ 985 SPOT_DEF_UNOP(NegClosure); 986 /// @} 987 988 /// \brief Construct a marked negated PSL Closure 989 /// @{ 990 SPOT_DEF_UNOP(NegClosureMarked); 991 /// @} 992 993 /// \brief Construct first_match(sere) 994 /// @{ 995 SPOT_DEF_UNOP(first_match); 996 /// @} 997 #undef SPOT_DEF_UNOP 998 999 /// @{ 1000 /// \brief Construct a binary operator 1001 /// \pre \a o should be one of op::Xor, op::Implies, op::Equiv, 1002 /// op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked, 1003 /// or op::UConcat. binop(op o,const formula & f,const formula & g)1004 static formula binop(op o, const formula& f, const formula& g) 1005 { 1006 return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone())); 1007 } 1008 1009 #ifndef SWIG binop(op o,const formula & f,formula && g)1010 static formula binop(op o, const formula& f, formula&& g) 1011 { 1012 return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_())); 1013 } 1014 binop(op o,formula && f,const formula & g)1015 static formula binop(op o, formula&& f, const formula& g) 1016 { 1017 return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone())); 1018 } 1019 binop(op o,formula && f,formula && g)1020 static formula binop(op o, formula&& f, formula&& g) 1021 { 1022 return formula(fnode::binop(o, f.to_node_(), g.to_node_())); 1023 } 1024 ///@} 1025 1026 #endif //SWIG 1027 1028 #ifdef SWIG 1029 #define SPOT_DEF_BINOP(Name) \ 1030 static formula Name(const formula& f, const formula& g) \ 1031 { \ 1032 return binop(op::Name, f, g); \ 1033 } 1034 #else // !SWIG 1035 #define SPOT_DEF_BINOP(Name) \ 1036 static formula Name(const formula& f, const formula& g) \ 1037 { \ 1038 return binop(op::Name, f, g); \ 1039 } \ 1040 static formula Name(const formula& f, formula&& g) \ 1041 { \ 1042 return binop(op::Name, f, std::move(g)); \ 1043 } \ 1044 static formula Name(formula&& f, const formula& g) \ 1045 { \ 1046 return binop(op::Name, std::move(f), g); \ 1047 } \ 1048 static formula Name(formula&& f, formula&& g) \ 1049 { \ 1050 return binop(op::Name, std::move(f), std::move(g)); \ 1051 } 1052 #endif // !SWIG 1053 /// \brief Construct an `Xor` formula 1054 /// @{ 1055 SPOT_DEF_BINOP(Xor); 1056 /// @} 1057 1058 /// \brief Construct an `->` formula 1059 /// @{ 1060 SPOT_DEF_BINOP(Implies); 1061 /// @} 1062 1063 /// \brief Construct an `<->` formula 1064 /// @{ 1065 SPOT_DEF_BINOP(Equiv); 1066 /// @} 1067 1068 /// \brief Construct a `U` formula 1069 /// @{ 1070 SPOT_DEF_BINOP(U); 1071 /// @} 1072 1073 /// \brief Construct an `R` formula 1074 /// @{ 1075 SPOT_DEF_BINOP(R); 1076 /// @} 1077 1078 /// \brief Construct a `W` formula 1079 /// @{ 1080 SPOT_DEF_BINOP(W); 1081 /// @} 1082 1083 /// \brief Construct an `M` formula 1084 /// @{ 1085 SPOT_DEF_BINOP(M); 1086 /// @} 1087 1088 /// \brief Construct a `<>->` PSL formula 1089 /// @{ 1090 SPOT_DEF_BINOP(EConcat); 1091 /// @} 1092 1093 /// \brief Construct a marked `<>->` PSL formula 1094 /// @{ 1095 SPOT_DEF_BINOP(EConcatMarked); 1096 /// @} 1097 1098 /// \brief Construct a `[]->` PSL formula 1099 /// @{ 1100 SPOT_DEF_BINOP(UConcat); 1101 /// @} 1102 #undef SPOT_DEF_BINOP 1103 1104 /// \brief Construct an n-ary operator 1105 /// 1106 /// \pre \a o should be one of op::Or, op::OrRat, op::And, 1107 /// op::AndRat, op::AndNLM, op::Concat, op::Fusion. 1108 /// @{ multop(op o,const std::vector<formula> & l)1109 static formula multop(op o, const std::vector<formula>& l) 1110 { 1111 std::vector<const fnode*> tmp; 1112 tmp.reserve(l.size()); 1113 for (auto f: l) 1114 if (f.ptr_) 1115 tmp.emplace_back(f.ptr_->clone()); 1116 return formula(fnode::multop(o, std::move(tmp))); 1117 } 1118 1119 #ifndef SWIG multop(op o,std::vector<formula> && l)1120 static formula multop(op o, std::vector<formula>&& l) 1121 { 1122 std::vector<const fnode*> tmp; 1123 tmp.reserve(l.size()); 1124 for (auto f: l) 1125 if (f.ptr_) 1126 tmp.emplace_back(f.to_node_()); 1127 return formula(fnode::multop(o, std::move(tmp))); 1128 } 1129 #endif // !SWIG 1130 /// @} 1131 1132 #ifdef SWIG 1133 #define SPOT_DEF_MULTOP(Name) \ 1134 static formula Name(const std::vector<formula>& l) \ 1135 { \ 1136 return multop(op::Name, l); \ 1137 } 1138 #else // !SWIG 1139 #define SPOT_DEF_MULTOP(Name) \ 1140 static formula Name(const std::vector<formula>& l) \ 1141 { \ 1142 return multop(op::Name, l); \ 1143 } \ 1144 \ 1145 static formula Name(std::vector<formula>&& l) \ 1146 { \ 1147 return multop(op::Name, std::move(l)); \ 1148 } 1149 #endif // !SWIG 1150 /// \brief Construct an Or formula. 1151 /// @{ 1152 SPOT_DEF_MULTOP(Or); 1153 /// @} 1154 1155 /// \brief Construct an Or SERE. 1156 /// @{ 1157 SPOT_DEF_MULTOP(OrRat); 1158 /// @} 1159 1160 /// \brief Construct an And formula. 1161 /// @{ 1162 SPOT_DEF_MULTOP(And); 1163 /// @} 1164 1165 /// \brief Construct an And SERE. 1166 /// @{ 1167 SPOT_DEF_MULTOP(AndRat); 1168 /// @} 1169 1170 /// \brief Construct a non-length-matching And SERE. 1171 /// @{ 1172 SPOT_DEF_MULTOP(AndNLM); 1173 /// @} 1174 1175 /// \brief Construct a Concatenation SERE. 1176 /// @{ 1177 SPOT_DEF_MULTOP(Concat); 1178 /// @} 1179 1180 /// \brief Construct a Fusion SERE. 1181 /// @{ 1182 SPOT_DEF_MULTOP(Fusion); 1183 /// @} 1184 #undef SPOT_DEF_MULTOP 1185 1186 /// \brief Define a bounded unary-operator (i.e. star-like) 1187 /// 1188 /// \pre \a o should be op::Star or op::FStar. 1189 /// @{ bunop(op o,const formula & f,unsigned min=0U,unsigned max=unbounded ())1190 static formula bunop(op o, const formula& f, 1191 unsigned min = 0U, 1192 unsigned max = unbounded()) 1193 { 1194 return formula(fnode::bunop(o, f.ptr_->clone(), min, max)); 1195 } 1196 1197 #ifndef SWIG bunop(op o,formula && f,unsigned min=0U,unsigned max=unbounded ())1198 static formula bunop(op o, formula&& f, 1199 unsigned min = 0U, 1200 unsigned max = unbounded()) 1201 { 1202 return formula(fnode::bunop(o, f.to_node_(), min, max)); 1203 } 1204 #endif // !SWIG 1205 ///@} 1206 1207 #if SWIG 1208 #define SPOT_DEF_BUNOP(Name) \ 1209 static formula Name(const formula& f, \ 1210 unsigned min = 0U, \ 1211 unsigned max = unbounded()) \ 1212 { \ 1213 return bunop(op::Name, f, min, max); \ 1214 } 1215 #else // !SWIG 1216 #define SPOT_DEF_BUNOP(Name) \ 1217 static formula Name(const formula& f, \ 1218 unsigned min = 0U, \ 1219 unsigned max = unbounded()) \ 1220 { \ 1221 return bunop(op::Name, f, min, max); \ 1222 } \ 1223 static formula Name(formula&& f, \ 1224 unsigned min = 0U, \ 1225 unsigned max = unbounded()) \ 1226 { \ 1227 return bunop(op::Name, std::move(f), min, max); \ 1228 } 1229 #endif 1230 /// \brief Create SERE for f[*min..max] 1231 /// @{ 1232 SPOT_DEF_BUNOP(Star); 1233 /// @} 1234 1235 /// \brief Create SERE for f[:*min..max] 1236 /// 1237 /// This operator is a generalization of the (+) operator 1238 /// defined by Dax et al. \cite dax.09.atva 1239 /// @{ 1240 SPOT_DEF_BUNOP(FStar); 1241 /// @} 1242 #undef SPOT_DEF_BUNOP 1243 1244 /// \brief Nested operator construction (syntactic sugar). 1245 /// 1246 /// Build between min and max nested uo, and chose between the 1247 /// different numbers with bo. 1248 /// 1249 /// For instance nested_unup_range(op::X, op::Or, 2, 4, a) returns 1250 /// XX(a | X(a | Xa)). 1251 /// 1252 /// For `max==unbounded()`, \a uo is repeated \a min times, and 1253 /// its child is set to `F(a)` if \a bo is `op::Or` or to `G(a)` 1254 /// otherwise. nested_unop_range(op uo,op bo,unsigned min,unsigned max,formula f)1255 static const formula nested_unop_range(op uo, op bo, unsigned min, 1256 unsigned max, formula f) 1257 { 1258 return formula(fnode::nested_unop_range(uo, bo, min, max, 1259 f.ptr_->clone())); 1260 } 1261 1262 /// \brief Create a SERE equivalent to b[->min..max] 1263 /// 1264 /// The operator does not exist: it is handled as syntactic sugar 1265 /// by the parser and the printer. This function is used by the 1266 /// parser to create the equivalent SERE. 1267 static formula sugar_goto(const formula& b, unsigned min, unsigned max); 1268 1269 /// Create the SERE b[=min..max] 1270 /// 1271 /// The operator does not exist: it is handled as syntactic sugar 1272 /// by the parser and the printer. This function is used by the 1273 /// parser to create the equivalent SERE. 1274 static formula sugar_equal(const formula& b, unsigned min, unsigned max); 1275 1276 /// Create the SERE a ##[n:m] b 1277 /// 1278 /// This ##[n:m] operator comes from SVA. When n=m, it is simply 1279 /// written ##n. 1280 /// 1281 /// The operator does not exist in Spot it is handled as syntactic 1282 /// sugar by the parser. This function is used by the parser to 1283 /// create the equivalent SERE using PSL operators. 1284 /// 1285 /// The rewriting rules depends on the values of a, n, and b. 1286 /// If n≥1 `a ##[n:m] b` is encoded as `a;1[*n-1,m-1];b`. 1287 /// Otherwise: 1288 /// * `a ##[0:0] b` is encoded as `a:b`, 1289 /// * For m>0, `a ##[0:m] b` is encoded as 1290 /// - `a:(1[*0:m];b)` is `a` rejects `[*0]`, 1291 /// - `(a;1[*0:m]):b` is `b` rejects `[*0]`, 1292 /// - `(a:b) | (a;1[*0:m-1];b)` is `a` and `b` accept `[*0]`. 1293 /// 1294 /// The left operand can also be missing, in which case 1295 /// `##[n:m] b` is rewritten as `1[*n:m];b`. 1296 /// @{ 1297 static formula sugar_delay(const formula& a, const formula& b, 1298 unsigned min, unsigned max); 1299 static formula sugar_delay(const formula& b, 1300 unsigned min, unsigned max); 1301 /// @} 1302 1303 #ifndef SWIG 1304 /// \brief Return the underlying pointer to the formula. 1305 /// 1306 /// It is not recommended to call this function, which is 1307 /// mostly meant for internal use. 1308 /// 1309 /// By calling this function you take ownership of the fnode 1310 /// instance pointed by this formula instance, and should take 1311 /// care of calling its destroy() methods once you are done with 1312 /// it. Otherwise the fnode will be leaked. to_node_()1313 const fnode* to_node_() 1314 { 1315 auto tmp = ptr_; 1316 ptr_ = nullptr; 1317 return tmp; 1318 } 1319 #endif 1320 1321 /// Return top-most operator. kind() const1322 op kind() const 1323 { 1324 return ptr_->kind(); 1325 } 1326 1327 /// Return the name of the top-most operator. kindstr() const1328 std::string kindstr() const 1329 { 1330 return ptr_->kindstr(); 1331 } 1332 1333 /// Return true if the formula is of kind \a o. is(op o) const1334 bool is(op o) const 1335 { 1336 return ptr_->is(o); 1337 } 1338 1339 #ifndef SWIG 1340 /// Return true if the formula is of kind \a o1 or \a o2. is(op o1,op o2) const1341 bool is(op o1, op o2) const 1342 { 1343 return ptr_->is(o1, o2); 1344 } 1345 1346 /// Return true if the formula is of kind \a o1 or \a o2 or \a o3 is(op o1,op o2,op o3) const1347 bool is(op o1, op o2, op o3) const 1348 { 1349 return ptr_->is(o1, o2, o3); 1350 } 1351 1352 /// Return true if the formula is of kind \a o1 or \a o2 or \a o3 1353 /// or \a a4. is(op o1,op o2,op o3,op o4) const1354 bool is(op o1, op o2, op o3, op o4) const 1355 { 1356 return ptr_->is(o1, o2, o3, o4); 1357 } 1358 1359 /// Return true if the formulas nests all the operators in \a l. is(std::initializer_list<op> l) const1360 bool is(std::initializer_list<op> l) const 1361 { 1362 return ptr_->is(l); 1363 } 1364 #endif 1365 1366 /// \brief Remove operator \a o and return the child. 1367 /// 1368 /// This works only for unary operators. get_child_of(op o) const1369 formula get_child_of(op o) const 1370 { 1371 auto f = ptr_->get_child_of(o); 1372 if (f) 1373 f->clone(); 1374 return formula(f); 1375 } 1376 1377 #ifndef SWIG 1378 /// \brief Remove all operators in \a l and return the child. 1379 /// 1380 /// This works only for a list of unary operators. 1381 /// For instance if \c f is a formula for XG(a U b), 1382 /// then <code>f.get_child_of({op::X, op::G})</code> 1383 /// will return the subformula a U b. get_child_of(std::initializer_list<op> l) const1384 formula get_child_of(std::initializer_list<op> l) const 1385 { 1386 auto f = ptr_->get_child_of(l); 1387 if (f) 1388 f->clone(); 1389 return formula(f); 1390 } 1391 #endif 1392 1393 /// \brief Return start of the range for star-like operators. 1394 /// 1395 /// \pre The formula should have kind op::Star or op::FStar. min() const1396 unsigned min() const 1397 { 1398 return ptr_->min(); 1399 } 1400 1401 /// \brief Return end of the range for star-like operators. 1402 /// 1403 /// \pre The formula should have kind op::Star or op::FStar. max() const1404 unsigned max() const 1405 { 1406 return ptr_->max(); 1407 } 1408 1409 /// Return the number of children. size() const1410 unsigned size() const 1411 { 1412 return ptr_->size(); 1413 } 1414 1415 /// \brief Whether the formula is a leaf. 1416 /// 1417 /// Leaves are formulas without children. They are either 1418 /// constants (true, false, empty word) or atomic propositions. is_leaf() const1419 bool is_leaf() const 1420 { 1421 return ptr_->is_leaf(); 1422 } 1423 1424 /// \brief Return the id of a formula. 1425 /// 1426 /// Can be used as a hash number. 1427 /// 1428 /// The id is almost unique as it is an unsigned number 1429 /// incremented for each formula construction, and the number may 1430 /// wrap around zero. If this is used for ordering, make sure to 1431 /// deal with equality id() const1432 size_t id() const 1433 { 1434 return ptr_->id(); 1435 } 1436 1437 #ifndef SWIG 1438 /// Allow iterating over children 1439 class SPOT_API formula_child_iterator final 1440 { 1441 const fnode*const* ptr_; 1442 public: formula_child_iterator()1443 formula_child_iterator() 1444 : ptr_(nullptr) 1445 { 1446 } 1447 formula_child_iterator(const fnode * const * f)1448 formula_child_iterator(const fnode*const* f) 1449 : ptr_(f) 1450 { 1451 } 1452 operator ==(formula_child_iterator o)1453 bool operator==(formula_child_iterator o) 1454 { 1455 return ptr_ == o.ptr_; 1456 } 1457 operator !=(formula_child_iterator o)1458 bool operator!=(formula_child_iterator o) 1459 { 1460 return ptr_ != o.ptr_; 1461 } 1462 operator *()1463 formula operator*() 1464 { 1465 return formula((*ptr_)->clone()); 1466 } 1467 operator ++()1468 formula_child_iterator operator++() 1469 { 1470 ++ptr_; 1471 return *this; 1472 } 1473 operator ++(int)1474 formula_child_iterator operator++(int) 1475 { 1476 auto tmp = *this; 1477 ++ptr_; 1478 return tmp; 1479 } 1480 }; 1481 1482 /// Allow iterating over children begin() const1483 formula_child_iterator begin() const 1484 { 1485 return ptr_->begin(); 1486 } 1487 1488 /// Allow iterating over children end() const1489 formula_child_iterator end() const 1490 { 1491 return ptr_->end(); 1492 } 1493 1494 /// Return children number \a i operator [](unsigned i) const1495 formula operator[](unsigned i) const 1496 { 1497 return formula(ptr_->nth(i)->clone()); 1498 } 1499 #endif 1500 1501 /// Return the false constant. ff()1502 static formula ff() 1503 { 1504 return formula(fnode::ff()); 1505 } 1506 1507 /// Whether the formula is the false constant. is_ff() const1508 bool is_ff() const 1509 { 1510 return ptr_->is_ff(); 1511 } 1512 1513 /// Return the true constant. tt()1514 static formula tt() 1515 { 1516 return formula(fnode::tt()); 1517 } 1518 1519 /// Whether the formula is the true constant. is_tt() const1520 bool is_tt() const 1521 { 1522 return ptr_->is_tt(); 1523 } 1524 1525 /// Return the empty word constant. eword()1526 static formula eword() 1527 { 1528 return formula(fnode::eword()); 1529 } 1530 1531 /// Whether the formula is the empty word constant. is_eword() const1532 bool is_eword() const 1533 { 1534 return ptr_->is_eword(); 1535 } 1536 1537 /// Whether the formula is op::ff, op::tt, or op::eword. is_constant() const1538 bool is_constant() const 1539 { 1540 return ptr_->is_constant(); 1541 } 1542 1543 /// \brief Test whether the formula represent a Kleene star 1544 /// 1545 /// That is, it should be of kind op::Star, with min=0 and 1546 /// max=unbounded(). is_Kleene_star() const1547 bool is_Kleene_star() const 1548 { 1549 return ptr_->is_Kleene_star(); 1550 } 1551 1552 /// \brief Return a copy of the formula 1[*]. one_star()1553 static formula one_star() 1554 { 1555 return formula(fnode::one_star()->clone()); 1556 } 1557 1558 /// \brief Whether the formula is an atomic proposition or its 1559 /// negation. is_literal() const1560 bool is_literal() const 1561 { 1562 return (is(op::ap) || 1563 // If f is in nenoform, Not can only occur in front of 1564 // an atomic proposition. So this way we do not have 1565 // to check the type of the child. 1566 (is(op::Not) && is_boolean() && is_in_nenoform())); 1567 } 1568 1569 /// \brief Print the name of an atomic proposition. 1570 /// 1571 /// \pre the formula should be of kind op::ap. ap_name() const1572 const std::string& ap_name() const 1573 { 1574 return ptr_->ap_name(); 1575 } 1576 1577 /// \brief Print the formula for debugging 1578 /// 1579 /// In addition to the operator and children, this also display 1580 /// the formula's unique id, and its reference count. dump(std::ostream & os) const1581 std::ostream& dump(std::ostream& os) const 1582 { 1583 return ptr_->dump(os); 1584 } 1585 1586 /// \brief clone this formula, omitting child \a i 1587 /// 1588 /// \pre The current node should be an n-ary operator such as 1589 /// op::And, op::AndRat, op::AndNLM, op::Or, op::OrRat, 1590 /// op::Concat, or op::Fusion. all_but(unsigned i) const1591 formula all_but(unsigned i) const 1592 { 1593 return formula(ptr_->all_but(i)); 1594 } 1595 1596 /// \brief number of Boolean children 1597 /// 1598 /// \pre The current node should be an n-ary operator such as 1599 /// op::And, op::AndRat, op::AndNLM, op::Or, or op::OrRat. 1600 /// 1601 /// Note that the children of an n-ary operator are always sorted 1602 /// when the node is constructed, and such that Boolean children 1603 /// appear at the beginning. This function therefore return the 1604 /// number of the first non-Boolean child if it exists. boolean_count() const1605 unsigned boolean_count() const 1606 { 1607 return ptr_->boolean_count(); 1608 } 1609 1610 /// \brief return a clone of the current node, restricted to its 1611 /// Boolean children 1612 /// 1613 /// \pre The current node should be an n-ary operator such as 1614 /// op::And, op::AndRat, op::AndNLM, op::Or, or op::OrRat. 1615 /// 1616 /// On a formula such as And({a,b,c,d,F(e),G(f)}), this returns 1617 /// And({a,b,c,d}). If \a width is not nullptr, it is set the the 1618 /// number of Boolean children gathered. Note that the children 1619 /// of an n-ary operator are always sorted when the node is 1620 /// constructed, and such that Boolean children appear at the 1621 /// beginning. \a width would therefore give the number of the 1622 /// first non-Boolean child if it exists. boolean_operands(unsigned * width=nullptr) const1623 formula boolean_operands(unsigned* width = nullptr) const 1624 { 1625 return formula(ptr_->boolean_operands(width)); 1626 } 1627 1628 #define SPOT_DEF_PROP(Name) \ 1629 bool Name() const \ 1630 { \ 1631 return ptr_->Name(); \ 1632 } 1633 //////////////// 1634 // Properties // 1635 //////////////// 1636 1637 /// Whether the formula use only boolean operators. 1638 SPOT_DEF_PROP(is_boolean); 1639 /// Whether the formula use only AND, OR, and NOT operators. 1640 SPOT_DEF_PROP(is_sugar_free_boolean); 1641 /// \brief Whether the formula is in negative normal form. 1642 /// 1643 /// A formula is in negative normal form if the not operators 1644 /// occur only in front of atomic propositions. 1645 SPOT_DEF_PROP(is_in_nenoform); 1646 /// Whether the formula is syntactically stutter_invariant 1647 SPOT_DEF_PROP(is_syntactic_stutter_invariant); 1648 /// Whether the formula avoids the F and G operators. 1649 SPOT_DEF_PROP(is_sugar_free_ltl); 1650 /// Whether the formula uses only LTL operators. 1651 SPOT_DEF_PROP(is_ltl_formula); 1652 /// Whether the formula uses only PSL operators. 1653 SPOT_DEF_PROP(is_psl_formula); 1654 /// Whether the formula uses only SERE operators. 1655 SPOT_DEF_PROP(is_sere_formula); 1656 /// \brief Whether a SERE describes a finite language, or an LTL 1657 /// formula uses no temporal operator but X. 1658 SPOT_DEF_PROP(is_finite); 1659 /// \brief Whether the formula is purely eventual. 1660 /// 1661 /// Pure eventuality formulae are defined in 1662 /// 1663 /// A word that satisfies a pure eventuality can be prefixed by 1664 /// anything and still satisfies the formula. 1665 /// \cite etessami.00.concur 1666 SPOT_DEF_PROP(is_eventual); 1667 /// \brief Whether a formula is purely universal. 1668 /// 1669 /// Purely universal formulae are defined in 1670 /// 1671 /// Any (non-empty) suffix of a word that satisfies a purely 1672 /// universal formula also satisfies the formula. 1673 /// \cite etessami.00.concur 1674 SPOT_DEF_PROP(is_universal); 1675 /// Whether a PSL/LTL formula is syntactic safety property. 1676 SPOT_DEF_PROP(is_syntactic_safety); 1677 /// Whether a PSL/LTL formula is syntactic guarantee property. 1678 SPOT_DEF_PROP(is_syntactic_guarantee); 1679 /// Whether a PSL/LTL formula is syntactic obligation property. 1680 SPOT_DEF_PROP(is_syntactic_obligation); 1681 /// Whether a PSL/LTL formula is syntactic recurrence property. 1682 SPOT_DEF_PROP(is_syntactic_recurrence); 1683 /// Whether a PSL/LTL formula is syntactic persistence property. 1684 SPOT_DEF_PROP(is_syntactic_persistence); 1685 /// \brief Whether the formula has an occurrence of EConcatMarked 1686 /// or NegClosureMarked 1687 SPOT_DEF_PROP(is_marked); 1688 /// Whether the formula accepts [*0]. 1689 SPOT_DEF_PROP(accepts_eword); 1690 /// \brief Whether the formula has only LBT-compatible atomic 1691 /// propositions. 1692 /// 1693 /// LBT only supports atomic propositions of the form p1, p12, 1694 /// etc. 1695 SPOT_DEF_PROP(has_lbt_atomic_props); 1696 /// \brief Whether the formula has spin-compatible atomic 1697 /// propositions. 1698 /// 1699 /// In Spin 5 (and hence ltl2ba, ltl3ba, ltl3dra), atomic 1700 /// propositions should start with a lowercase letter, and can 1701 /// then consist solely of alphanumeric characters and underscores. 1702 /// 1703 /// \see spot::is_spin_ap() 1704 SPOT_DEF_PROP(has_spin_atomic_props); 1705 #undef SPOT_DEF_PROP 1706 1707 /// \brief Clone this node after applying \a trans to its children. 1708 /// 1709 /// Any additional argument is passed to trans. 1710 template<typename Trans, typename... Args> map(Trans trans,Args &&...args)1711 formula map(Trans trans, Args&&... args) 1712 { 1713 switch (op o = kind()) 1714 { 1715 case op::ff: 1716 case op::tt: 1717 case op::eword: 1718 case op::ap: 1719 return *this; 1720 case op::Not: 1721 case op::X: 1722 #if SPOT_HAS_STRONG_X 1723 case op::strong_X: 1724 #endif 1725 case op::F: 1726 case op::G: 1727 case op::Closure: 1728 case op::NegClosure: 1729 case op::NegClosureMarked: 1730 case op::first_match: 1731 return unop(o, trans((*this)[0], std::forward<Args>(args)...)); 1732 case op::Xor: 1733 case op::Implies: 1734 case op::Equiv: 1735 case op::U: 1736 case op::R: 1737 case op::W: 1738 case op::M: 1739 case op::EConcat: 1740 case op::EConcatMarked: 1741 case op::UConcat: 1742 { 1743 formula tmp = trans((*this)[0], std::forward<Args>(args)...); 1744 return binop(o, tmp, 1745 trans((*this)[1], std::forward<Args>(args)...)); 1746 } 1747 case op::Or: 1748 case op::OrRat: 1749 case op::And: 1750 case op::AndRat: 1751 case op::AndNLM: 1752 case op::Concat: 1753 case op::Fusion: 1754 { 1755 std::vector<formula> tmp; 1756 tmp.reserve(size()); 1757 for (auto f: *this) 1758 tmp.emplace_back(trans(f, std::forward<Args>(args)...)); 1759 return multop(o, std::move(tmp)); 1760 } 1761 case op::Star: 1762 case op::FStar: 1763 return bunop(o, trans((*this)[0], std::forward<Args>(args)...), 1764 min(), max()); 1765 } 1766 SPOT_UNREACHABLE(); 1767 } 1768 1769 /// \brief Apply \a func to each subformula. 1770 /// 1771 /// This does a simple DFS without checking for duplicate 1772 /// subformulas. If \a func returns true, the children of the 1773 /// current node are skipped. 1774 /// 1775 /// Any additional argument is passed to \a func when it is 1776 /// invoked. 1777 template<typename Func, typename... Args> traverse(Func func,Args &&...args)1778 void traverse(Func func, Args&&... args) 1779 { 1780 if (func(*this, std::forward<Args>(args)...)) 1781 return; 1782 for (auto f: *this) 1783 f.traverse(func, std::forward<Args>(args)...); 1784 } 1785 1786 private: 1787 #ifndef SWIG 1788 [[noreturn]] static void report_ap_invalid_arg(); 1789 #endif 1790 }; 1791 1792 /// Print the properties of formula \a f on stream \a out. 1793 SPOT_API 1794 std::ostream& print_formula_props(std::ostream& out, const formula& f, 1795 bool abbreviated = false); 1796 1797 /// List the properties of formula \a f. 1798 SPOT_API 1799 std::list<std::string> list_formula_props(const formula& f); 1800 1801 /// Print a formula. 1802 SPOT_API 1803 std::ostream& operator<<(std::ostream& os, const formula& f); 1804 } 1805 1806 #ifndef SWIG 1807 namespace std 1808 { 1809 template <> 1810 struct hash<spot::formula> 1811 { operator ()std::hash1812 size_t operator()(const spot::formula& x) const noexcept 1813 { 1814 return x.id(); 1815 } 1816 }; 1817 } 1818 #endif 1819