spot 2.11.5.dev
formula.hh
Go to the documentation of this file.
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015-2022 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
22#pragma once
23
30
33
36
39
42
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
72namespace spot
73{
74
75
78 enum class op: uint8_t
79 {
80 ff,
81 tt,
82 eword,
83 ap,
84 // unary operators
85 Not,
86 X,
87 F,
88 G,
89 Closure,
92 // binary operators
93 Xor,
94 Implies,
95 Equiv,
96 U,
97 R,
98 W,
99 M,
100 EConcat,
102 UConcat,
103 // n-ary operators
104 Or,
105 OrRat,
106 And,
107 AndRat,
108 AndNLM,
109 Concat,
110 Fusion,
111 // star-like operators
112 Star,
113 FStar,
115#ifdef SPOT_WANT_STRONG_X
116 strong_X,
117#endif
118 };
119
120#ifndef SWIG
127 class SPOT_API fnode final
128 {
129 public:
134 const fnode* clone() const
135 {
136 // Saturate.
137 ++refs_;
138 if (SPOT_UNLIKELY(!refs_))
139 saturated_ = 1;
140 return this;
141 }
142
148 void destroy() const
149 {
150 if (SPOT_LIKELY(refs_))
151 --refs_;
152 else if (SPOT_LIKELY(!saturated_))
153 // last reference to a node that is not a constant
154 destroy_aux();
155 }
156
158 static constexpr uint8_t unbounded()
159 {
160 return UINT8_MAX;
161 }
162
164 static const fnode* ap(const std::string& name);
166 static const fnode* unop(op o, const fnode* f);
168 static const fnode* binop(op o, const fnode* f, const fnode* g);
170 static const fnode* multop(op o, std::vector<const fnode*> l);
172 static const fnode* bunop(op o, const fnode* f,
173 unsigned min, unsigned max = unbounded());
174
176 static const fnode* nested_unop_range(op uo, op bo, unsigned min,
177 unsigned max, const fnode* f);
178
180 op kind() const
181 {
182 return op_;
183 }
184
186 std::string kindstr() const;
187
190 bool is(op o) const
191 {
192 return op_ == o;
193 }
194
195 bool is(op o1, op o2) const
196 {
197 return op_ == o1 || op_ == o2;
198 }
199
200 bool is(op o1, op o2, op o3) const
201 {
202 return op_ == o1 || op_ == o2 || op_ == o3;
203 }
204
205 bool is(op o1, op o2, op o3, op o4) const
206 {
207 return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
208 }
209
210 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 }
222
224 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
234 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
247 unsigned min() const
248 {
249 if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
250 report_min_invalid_arg();
251 return min_;
252 }
253
255 unsigned max() const
256 {
257 if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
258 report_max_invalid_arg();
259 return max_;
260 }
261
263 unsigned size() const
264 {
265 return size_;
266 }
267
269 bool is_leaf() const
270 {
271 return size_ == 0;
272 }
273
275 size_t id() const
276 {
277 return id_;
278 }
279
281 const fnode*const* begin() const
282 {
283 return children;
284 }
285
287 const fnode*const* end() const
288 {
289 return children + size();
290 }
291
293 const fnode* nth(unsigned i) const
294 {
295 if (SPOT_UNLIKELY(i >= size()))
296 report_non_existing_child();
297 const fnode* c = children[i];
298 SPOT_ASSUME(c != nullptr);
299 return c;
300 }
301
303 static const fnode* ff()
304 {
305 return ff_;
306 }
307
309 bool is_ff() const
310 {
311 return op_ == op::ff;
312 }
313
315 static const fnode* tt()
316 {
317 return tt_;
318 }
319
321 bool is_tt() const
322 {
323 return op_ == op::tt;
324 }
325
327 static const fnode* eword()
328 {
329 return ew_;
330 }
331
333 bool is_eword() const
334 {
335 return op_ == op::eword;
336 }
337
339 bool is_constant() const
340 {
341 return op_ == op::ff || op_ == op::tt || op_ == op::eword;
342 }
343
345 bool is_Kleene_star() const
346 {
347 if (op_ != op::Star)
348 return false;
349 return min_ == 0 && max_ == unbounded();
350 }
351
353 static const fnode* one_star()
354 {
355 if (!one_star_)
356 one_star_ = new fnode(op::Star, tt_, 0, unbounded(), true);
357 return one_star_;
358 }
359
361 static const fnode* one_plus()
362 {
363 if (!one_plus_)
364 one_plus_ = new fnode(op::Star, tt_, 1, unbounded(), true);
365 return one_plus_;
366 }
367
369 const std::string& ap_name() const;
370
372 std::ostream& dump(std::ostream& os) const;
373
375 const fnode* all_but(unsigned i) const;
376
378 unsigned boolean_count() const
379 {
380 unsigned pos = 0;
381 unsigned s = size();
382 while (pos < s && children[pos]->is_boolean())
383 ++pos;
384 return pos;
385 }
386
388 const fnode* boolean_operands(unsigned* width = nullptr) const;
389
400 static bool instances_check();
401
403 // Properties //
405
407 bool is_boolean() const
408 {
409 return is_.boolean;
410 }
411
414 {
415 return is_.sugar_free_boolean;
416 }
417
419 bool is_in_nenoform() const
420 {
421 return is_.in_nenoform;
422 }
423
426 {
427 return is_.syntactic_si;
428 }
429
431 bool is_sugar_free_ltl() const
432 {
433 return is_.sugar_free_ltl;
434 }
435
437 bool is_ltl_formula() const
438 {
439 return is_.ltl_formula;
440 }
441
443 bool is_psl_formula() const
444 {
445 return is_.psl_formula;
446 }
447
449 bool is_sere_formula() const
450 {
451 return is_.sere_formula;
452 }
453
455 bool is_finite() const
456 {
457 return is_.finite;
458 }
459
461 bool is_eventual() const
462 {
463 return is_.eventual;
464 }
465
467 bool is_universal() const
468 {
469 return is_.universal;
470 }
471
474 {
475 return is_.syntactic_safety;
476 }
477
480 {
481 return is_.syntactic_guarantee;
482 }
483
486 {
487 return is_.syntactic_obligation;
488 }
489
492 {
493 return is_.syntactic_recurrence;
494 }
495
498 {
499 return is_.syntactic_persistence;
500 }
501
503 bool is_marked() const
504 {
505 return !is_.not_marked;
506 }
507
509 bool accepts_eword() const
510 {
511 return is_.accepting_eword;
512 }
513
516 {
517 return is_.lbt_atomic_props;
518 }
519
522 {
523 return is_.spin_atomic_props;
524 }
525
526 private:
527 static size_t bump_next_id();
528 void setup_props(op o);
529 void destroy_aux() const;
530
531 [[noreturn]] static void report_non_existing_child();
532 [[noreturn]] static void report_too_many_children();
533 [[noreturn]] static void
534 report_get_child_of_expecting_single_child_node();
535 [[noreturn]] static void report_min_invalid_arg();
536 [[noreturn]] static void report_max_invalid_arg();
537
538 static const fnode* unique(fnode*);
539
540 // Destruction may only happen via destroy().
541 ~fnode() = default;
542 // Disallow copies.
543 fnode(const fnode&) = delete;
544 fnode& operator=(const fnode&) = delete;
545
546
547
548 template<class iter>
549 fnode(op o, iter begin, iter end, bool saturated = false)
550 // Clang has some optimization where is it able to combine the
551 // 4 movb initializing op_,min_,max_,saturated_ into a single
552 // movl. Also it can optimize the three byte-comparisons of
553 // is_Kleene_star() into a single masked 32-bit comparison.
554 // The latter optimization triggers warnings from valgrind if
555 // min_ and max_ are not initialized. So to benefit from the
556 // initialization optimization and the is_Kleene_star()
557 // optimization in Clang, we always initialize min_ and max_
558 // with this compiler. Do not do it the rest of the time,
559 // since the optimization is not done.
560 : op_(o),
561#if __llvm__
562 min_(0), max_(0),
563#endif
564 saturated_(saturated)
565 {
566 size_t s = std::distance(begin, end);
567 if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
568 report_too_many_children();
569 size_ = s;
570 auto pos = children;
571 for (auto i = begin; i != end; ++i)
572 *pos++ = *i;
573 setup_props(o);
574 }
575
576 fnode(op o, std::initializer_list<const fnode*> l,
577 bool saturated = false)
578 : fnode(o, l.begin(), l.end(), saturated)
579 {
580 }
581
582 fnode(op o, const fnode* f, uint8_t min, uint8_t max,
583 bool saturated = false)
584 : op_(o), min_(min), max_(max), saturated_(saturated), size_(1)
585 {
586 children[0] = f;
587 setup_props(o);
588 }
589
590 static const fnode* ff_;
591 static const fnode* tt_;
592 static const fnode* ew_;
593 static const fnode* one_star_;
594 static const fnode* one_plus_;
595
596 op op_; // operator
597 uint8_t min_; // range minimum (for star-like operators)
598 uint8_t max_; // range maximum;
599 mutable uint8_t saturated_;
600 uint16_t size_; // number of children
601 mutable uint16_t refs_ = 0; // reference count - 1;
602 size_t id_; // Also used as hash.
603 static size_t next_id_;
604
605 struct ltl_prop
606 {
607 // All properties here should be expressed in such a a way
608 // that property(f && g) is just property(f)&property(g).
609 // This allows us to compute all properties of a compound
610 // formula in one operation.
611 //
612 // For instance we do not use a property that says "has
613 // temporal operator", because it would require an OR between
614 // the two arguments. Instead we have a property that
615 // says "no temporal operator", and that one is computed
616 // with an AND between the arguments.
617 //
618 // Also choose a name that makes sense when prefixed with
619 // "the formula is".
620 bool boolean:1; // No temporal operators.
621 bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
622 bool in_nenoform:1; // Negative Normal Form.
623 bool syntactic_si:1; // LTL-X or siPSL
624 bool sugar_free_ltl:1; // No F and G operators.
625 bool ltl_formula:1; // Only LTL operators.
626 bool psl_formula:1; // Only PSL operators.
627 bool sere_formula:1; // Only SERE operators.
628 bool finite:1; // Finite SERE formulae, or Bool+X forms.
629 bool eventual:1; // Purely eventual formula.
630 bool universal:1; // Purely universal formula.
631 bool syntactic_safety:1; // Syntactic Safety Property.
632 bool syntactic_guarantee:1; // Syntactic Guarantee Property.
633 bool syntactic_obligation:1; // Syntactic Obligation Property.
634 bool syntactic_recurrence:1; // Syntactic Recurrence Property.
635 bool syntactic_persistence:1; // Syntactic Persistence Property.
636 bool not_marked:1; // No occurrence of EConcatMarked.
637 bool accepting_eword:1; // Accepts the empty word.
638 bool lbt_atomic_props:1; // Use only atomic propositions like p42.
639 bool spin_atomic_props:1; // Use only spin-compatible atomic props.
640 };
641 union
642 {
643 // Use an unsigned for fast computation of all properties.
644 unsigned props;
645 ltl_prop is_;
646 };
647
648 const fnode* children[1];
649 };
650
652 SPOT_API
653 int atomic_prop_cmp(const fnode* f, const fnode* g);
654
656 {
657 bool
658 operator()(const fnode* left, const fnode* right) const
659 {
660 SPOT_ASSERT(left);
661 SPOT_ASSERT(right);
662 if (left == right)
663 return false;
664
665 // We want Boolean formulae first.
666 bool lib = left->is_boolean();
667 if (lib != right->is_boolean())
668 return lib;
669
670 // We have two Boolean formulae
671 if (lib)
672 {
673 bool lconst = left->is_constant();
674 if (lconst != right->is_constant())
675 return lconst;
676 if (!lconst)
677 {
678 auto get_literal = [](const fnode* f) -> const fnode*
679 {
680 if (f->is(op::Not))
681 f = f->nth(0);
682 if (f->is(op::ap))
683 return f;
684 return nullptr;
685 };
686 // Literals should come first
687 const fnode* litl = get_literal(left);
688 const fnode* litr = get_literal(right);
689 if (!litl != !litr)
690 return litl;
691 if (litl)
692 {
693 // And they should be sorted alphabetically
694 int cmp = atomic_prop_cmp(litl, litr);
695 if (cmp)
696 return cmp < 0;
697 }
698 }
699 }
700
701 size_t l = left->id();
702 size_t r = right->id();
703 if (l != r)
704 return l < r;
705 // Because the hash code assigned to each formula is the
706 // number of formulae constructed so far, it is very unlikely
707 // that we will ever reach a case were two different formulae
708 // have the same hash. This will happen only ever with have
709 // produced 256**sizeof(size_t) formulae (i.e. max_count has
710 // looped back to 0 and started over). In that case we can
711 // order two formulas by looking at their text representation.
712 // We could be more efficient and look at their AST, but it's
713 // not worth the burden. (Also ordering pointers is ruled out
714 // because it breaks the determinism of the implementation.)
715 std::ostringstream old;
716 left->dump(old);
717 std::ostringstream ord;
718 right->dump(ord);
719 return old.str() < ord.str();
720 }
721 };
722
723#endif // SWIG
724
727 class SPOT_API formula final
728 {
729 const fnode* ptr_;
730 public:
735 explicit formula(const fnode* f) noexcept
736 : ptr_(f)
737 {
738 }
739
745 formula(std::nullptr_t) noexcept
746 : ptr_(nullptr)
747 {
748 }
749
751 formula() noexcept
752 : ptr_(nullptr)
753 {
754 }
755
757 formula(const formula& f) noexcept
758 : ptr_(f.ptr_)
759 {
760 if (ptr_)
761 ptr_->clone();
762 }
763
765 formula(formula&& f) noexcept
766 : ptr_(f.ptr_)
767 {
768 f.ptr_ = nullptr;
769 }
770
773 {
774 if (ptr_)
775 ptr_->destroy();
776 }
777
785 const formula& operator=(std::nullptr_t)
786 {
787 this->~formula();
788 ptr_ = nullptr;
789 return *this;
790 }
791
792 const formula& operator=(const formula& f)
793 {
794 this->~formula();
795 if ((ptr_ = f.ptr_))
796 ptr_->clone();
797 return *this;
798 }
799
800 const formula& operator=(formula&& f) noexcept
801 {
802 std::swap(f.ptr_, ptr_);
803 return *this;
804 }
805
806 bool operator<(const formula& other) const noexcept
807 {
808 if (SPOT_UNLIKELY(!other.ptr_))
809 return false;
810 if (SPOT_UNLIKELY(!ptr_))
811 return true;
812 if (id() < other.id())
813 return true;
814 if (id() > other.id())
815 return false;
816 // The case where id()==other.id() but ptr_ != other.ptr_ is
817 // very unlikely (we would need to build more than UINT_MAX
818 // formulas), so let's just compare pointers, and ignore the
819 // fact that it may introduce some nondeterminism.
820 return ptr_ < other.ptr_;
821 }
822
823 bool operator<=(const formula& other) const noexcept
824 {
825 return *this == other || *this < other;
826 }
827
828 bool operator>(const formula& other) const noexcept
829 {
830 return !(*this <= other);
831 }
832
833 bool operator>=(const formula& other) const noexcept
834 {
835 return !(*this < other);
836 }
837
838 bool operator==(const formula& other) const noexcept
839 {
840 return other.ptr_ == ptr_;
841 }
842
843 bool operator==(std::nullptr_t) const noexcept
844 {
845 return ptr_ == nullptr;
846 }
847
848 bool operator!=(const formula& other) const noexcept
849 {
850 return other.ptr_ != ptr_;
851 }
852
853 bool operator!=(std::nullptr_t) const noexcept
854 {
855 return ptr_ != nullptr;
856 }
857
858 explicit operator bool() const noexcept
859 {
860 return ptr_ != nullptr;
861 }
862
864 // Forwarded functions //
866
868 static constexpr uint8_t unbounded()
869 {
870 return fnode::unbounded();
871 }
872
874 static formula ap(const std::string& name)
875 {
876 return formula(fnode::ap(name));
877 }
878
884 static formula ap(const formula& a)
885 {
886 if (SPOT_UNLIKELY(a.kind() != op::ap))
887 report_ap_invalid_arg();
888 return a;
889 }
890
895 static formula unop(op o, const formula& f)
896 {
897 return formula(fnode::unop(o, f.ptr_->clone()));
898 }
899
900#ifndef SWIG
901 static formula unop(op o, formula&& f)
902 {
903 return formula(fnode::unop(o, f.to_node_()));
904 }
905#endif // !SWIG
907
908#ifdef SWIG
909#define SPOT_DEF_UNOP(Name) \
910 static formula Name(const formula& f) \
911 { \
912 return unop(op::Name, f); \
913 }
914#else // !SWIG
915#define SPOT_DEF_UNOP(Name) \
916 static formula Name(const formula& f) \
917 { \
918 return unop(op::Name, f); \
919 } \
920 static formula Name(formula&& f) \
921 { \
922 return unop(op::Name, std::move(f)); \
923 }
924#endif // !SWIG
927 SPOT_DEF_UNOP(Not);
929
932 SPOT_DEF_UNOP(X);
934
938 static formula X(unsigned level, const formula& f)
939 {
940 return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
941 }
942
943#if SPOT_WANT_STRONG_X
946 SPOT_DEF_UNOP(strong_X);
948
952 static formula strong_X(unsigned level, const formula& f)
953 {
954 return nested_unop_range(op::strong_X, op::Or /* unused */,
955 level, level, f);
956 }
957#endif
958
961 SPOT_DEF_UNOP(F);
963
970 static formula F(unsigned min_level, unsigned max_level, const formula& f)
971 {
972 return nested_unop_range(op::X, op::Or, min_level, max_level, f);
973 }
974
981 static formula G(unsigned min_level, unsigned max_level, const formula& f)
982 {
983 return nested_unop_range(op::X, op::And, min_level, max_level, f);
984 }
985
988 SPOT_DEF_UNOP(G);
990
993 SPOT_DEF_UNOP(Closure);
995
998 SPOT_DEF_UNOP(NegClosure);
1000
1003 SPOT_DEF_UNOP(NegClosureMarked);
1005
1008 SPOT_DEF_UNOP(first_match);
1010#undef SPOT_DEF_UNOP
1011
1017 static formula binop(op o, const formula& f, const formula& g)
1018 {
1019 return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
1020 }
1021
1022#ifndef SWIG
1023 static formula binop(op o, const formula& f, formula&& g)
1024 {
1025 return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
1026 }
1027
1028 static formula binop(op o, formula&& f, const formula& g)
1029 {
1030 return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
1031 }
1032
1033 static formula binop(op o, formula&& f, formula&& g)
1034 {
1035 return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
1036 }
1038
1039#endif //SWIG
1040
1041#ifdef SWIG
1042#define SPOT_DEF_BINOP(Name) \
1043 static formula Name(const formula& f, const formula& g) \
1044 { \
1045 return binop(op::Name, f, g); \
1046 }
1047#else // !SWIG
1048#define SPOT_DEF_BINOP(Name) \
1049 static formula Name(const formula& f, const formula& g) \
1050 { \
1051 return binop(op::Name, f, g); \
1052 } \
1053 static formula Name(const formula& f, formula&& g) \
1054 { \
1055 return binop(op::Name, f, std::move(g)); \
1056 } \
1057 static formula Name(formula&& f, const formula& g) \
1058 { \
1059 return binop(op::Name, std::move(f), g); \
1060 } \
1061 static formula Name(formula&& f, formula&& g) \
1062 { \
1063 return binop(op::Name, std::move(f), std::move(g)); \
1064 }
1065#endif // !SWIG
1068 SPOT_DEF_BINOP(Xor);
1070
1073 SPOT_DEF_BINOP(Implies);
1075
1078 SPOT_DEF_BINOP(Equiv);
1080
1083 SPOT_DEF_BINOP(U);
1085
1088 SPOT_DEF_BINOP(R);
1090
1093 SPOT_DEF_BINOP(W);
1095
1098 SPOT_DEF_BINOP(M);
1100
1103 SPOT_DEF_BINOP(EConcat);
1105
1108 SPOT_DEF_BINOP(EConcatMarked);
1110
1113 SPOT_DEF_BINOP(UConcat);
1115#undef SPOT_DEF_BINOP
1116
1122 static formula multop(op o, const std::vector<formula>& l)
1123 {
1124 std::vector<const fnode*> tmp;
1125 tmp.reserve(l.size());
1126 for (auto f: l)
1127 if (f.ptr_)
1128 tmp.emplace_back(f.ptr_->clone());
1129 return formula(fnode::multop(o, std::move(tmp)));
1130 }
1131
1132#ifndef SWIG
1133 static formula multop(op o, std::vector<formula>&& l)
1134 {
1135 std::vector<const fnode*> tmp;
1136 tmp.reserve(l.size());
1137 for (auto f: l)
1138 if (f.ptr_)
1139 tmp.emplace_back(f.to_node_());
1140 return formula(fnode::multop(o, std::move(tmp)));
1141 }
1142#endif // !SWIG
1144
1145#ifdef SWIG
1146#define SPOT_DEF_MULTOP(Name) \
1147 static formula Name(const std::vector<formula>& l) \
1148 { \
1149 return multop(op::Name, l); \
1150 }
1151#else // !SWIG
1152#define SPOT_DEF_MULTOP(Name) \
1153 static formula Name(const std::vector<formula>& l) \
1154 { \
1155 return multop(op::Name, l); \
1156 } \
1157 \
1158 static formula Name(std::vector<formula>&& l) \
1159 { \
1160 return multop(op::Name, std::move(l)); \
1161 }
1162#endif // !SWIG
1165 SPOT_DEF_MULTOP(Or);
1167
1170 SPOT_DEF_MULTOP(OrRat);
1172
1175 SPOT_DEF_MULTOP(And);
1177
1180 SPOT_DEF_MULTOP(AndRat);
1182
1185 SPOT_DEF_MULTOP(AndNLM);
1187
1190 SPOT_DEF_MULTOP(Concat);
1192
1195 SPOT_DEF_MULTOP(Fusion);
1197#undef SPOT_DEF_MULTOP
1198
1203 static formula bunop(op o, const formula& f,
1204 unsigned min = 0U,
1205 unsigned max = unbounded())
1206 {
1207 return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1208 }
1209
1210#ifndef SWIG
1211 static formula bunop(op o, formula&& f,
1212 unsigned min = 0U,
1213 unsigned max = unbounded())
1214 {
1215 return formula(fnode::bunop(o, f.to_node_(), min, max));
1216 }
1217#endif // !SWIG
1219
1220#if SWIG
1221#define SPOT_DEF_BUNOP(Name) \
1222 static formula Name(const formula& f, \
1223 unsigned min = 0U, \
1224 unsigned max = unbounded()) \
1225 { \
1226 return bunop(op::Name, f, min, max); \
1227 }
1228#else // !SWIG
1229#define SPOT_DEF_BUNOP(Name) \
1230 static formula Name(const formula& f, \
1231 unsigned min = 0U, \
1232 unsigned max = unbounded()) \
1233 { \
1234 return bunop(op::Name, f, min, max); \
1235 } \
1236 static formula Name(formula&& f, \
1237 unsigned min = 0U, \
1238 unsigned max = unbounded()) \
1239 { \
1240 return bunop(op::Name, std::move(f), min, max); \
1241 }
1242#endif
1245 SPOT_DEF_BUNOP(Star);
1247
1253 SPOT_DEF_BUNOP(FStar);
1255#undef SPOT_DEF_BUNOP
1256
1268 static const formula nested_unop_range(op uo, op bo, unsigned min,
1269 unsigned max, formula f)
1270 {
1271 return formula(fnode::nested_unop_range(uo, bo, min, max,
1272 f.ptr_->clone()));
1273 }
1274
1280 static formula sugar_goto(const formula& b, unsigned min, unsigned max);
1281
1287 static formula sugar_equal(const formula& b, unsigned min, unsigned max);
1288
1310 static formula sugar_delay(const formula& a, const formula& b,
1311 unsigned min, unsigned max);
1312 static formula sugar_delay(const formula& b,
1313 unsigned min, unsigned max);
1315
1316#ifndef SWIG
1327 {
1328 auto tmp = ptr_;
1329 ptr_ = nullptr;
1330 return tmp;
1331 }
1332#endif
1333
1335 op kind() const
1336 {
1337 return ptr_->kind();
1338 }
1339
1341 std::string kindstr() const
1342 {
1343 return ptr_->kindstr();
1344 }
1345
1347 bool is(op o) const
1348 {
1349 return ptr_->is(o);
1350 }
1351
1352#ifndef SWIG
1354 bool is(op o1, op o2) const
1355 {
1356 return ptr_->is(o1, o2);
1357 }
1358
1360 bool is(op o1, op o2, op o3) const
1361 {
1362 return ptr_->is(o1, o2, o3);
1363 }
1364
1367 bool is(op o1, op o2, op o3, op o4) const
1368 {
1369 return ptr_->is(o1, o2, o3, o4);
1370 }
1371
1373 bool is(std::initializer_list<op> l) const
1374 {
1375 return ptr_->is(l);
1376 }
1377#endif
1378
1383 {
1384 auto f = ptr_->get_child_of(o);
1385 if (f)
1386 f->clone();
1387 return formula(f);
1388 }
1389
1390#ifndef SWIG
1397 formula get_child_of(std::initializer_list<op> l) const
1398 {
1399 auto f = ptr_->get_child_of(l);
1400 if (f)
1401 f->clone();
1402 return formula(f);
1403 }
1404#endif
1405
1409 unsigned min() const
1410 {
1411 return ptr_->min();
1412 }
1413
1417 unsigned max() const
1418 {
1419 return ptr_->max();
1420 }
1421
1423 unsigned size() const
1424 {
1425 return ptr_->size();
1426 }
1427
1432 bool is_leaf() const
1433 {
1434 return ptr_->is_leaf();
1435 }
1436
1445 size_t id() const
1446 {
1447 return ptr_->id();
1448 }
1449
1450#ifndef SWIG
1452 class SPOT_API formula_child_iterator final
1453 {
1454 const fnode*const* ptr_;
1455 public:
1457 : ptr_(nullptr)
1458 {
1459 }
1460
1461 formula_child_iterator(const fnode*const* f)
1462 : ptr_(f)
1463 {
1464 }
1465
1466 bool operator==(formula_child_iterator o)
1467 {
1468 return ptr_ == o.ptr_;
1469 }
1470
1471 bool operator!=(formula_child_iterator o)
1472 {
1473 return ptr_ != o.ptr_;
1474 }
1475
1476 formula operator*()
1477 {
1478 return formula((*ptr_)->clone());
1479 }
1480
1481 formula_child_iterator operator++()
1482 {
1483 ++ptr_;
1484 return *this;
1485 }
1486
1487 formula_child_iterator operator++(int)
1488 {
1489 auto tmp = *this;
1490 ++ptr_;
1491 return tmp;
1492 }
1493 };
1494
1497 {
1498 return ptr_->begin();
1499 }
1500
1503 {
1504 return ptr_->end();
1505 }
1506
1508 formula operator[](unsigned i) const
1509 {
1510 return formula(ptr_->nth(i)->clone());
1511 }
1512#endif
1513
1515 static formula ff()
1516 {
1517 return formula(fnode::ff());
1518 }
1519
1521 bool is_ff() const
1522 {
1523 return ptr_->is_ff();
1524 }
1525
1527 static formula tt()
1528 {
1529 return formula(fnode::tt());
1530 }
1531
1533 bool is_tt() const
1534 {
1535 return ptr_->is_tt();
1536 }
1537
1540 {
1541 return formula(fnode::eword());
1542 }
1543
1545 bool is_eword() const
1546 {
1547 return ptr_->is_eword();
1548 }
1549
1551 bool is_constant() const
1552 {
1553 return ptr_->is_constant();
1554 }
1555
1560 bool is_Kleene_star() const
1561 {
1562 return ptr_->is_Kleene_star();
1563 }
1564
1567 {
1568 // no need to clone, 1[*] is not reference counted
1569 return formula(fnode::one_star());
1570 }
1571
1574 {
1575 // no need to clone, 1[+] is not reference counted
1576 return formula(fnode::one_plus());
1577 }
1578
1581 bool is_literal() const
1582 {
1583 return (is(op::ap) ||
1584 // If f is in nenoform, Not can only occur in front of
1585 // an atomic proposition. So this way we do not have
1586 // to check the type of the child.
1587 (is(op::Not) && is_boolean() && is_in_nenoform()));
1588 }
1589
1593 const std::string& ap_name() const
1594 {
1595 return ptr_->ap_name();
1596 }
1597
1602 std::ostream& dump(std::ostream& os) const
1603 {
1604 return ptr_->dump(os);
1605 }
1606
1612 formula all_but(unsigned i) const
1613 {
1614 return formula(ptr_->all_but(i));
1615 }
1616
1626 unsigned boolean_count() const
1627 {
1628 return ptr_->boolean_count();
1629 }
1630
1644 formula boolean_operands(unsigned* width = nullptr) const
1645 {
1646 return formula(ptr_->boolean_operands(width));
1647 }
1648
1649#define SPOT_DEF_PROP(Name) \
1650 bool Name() const \
1651 { \
1652 return ptr_->Name(); \
1653 }
1655 // Properties //
1657
1659 SPOT_DEF_PROP(is_boolean);
1661 SPOT_DEF_PROP(is_sugar_free_boolean);
1666 SPOT_DEF_PROP(is_in_nenoform);
1668 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1670 SPOT_DEF_PROP(is_sugar_free_ltl);
1672 SPOT_DEF_PROP(is_ltl_formula);
1674 SPOT_DEF_PROP(is_psl_formula);
1676 SPOT_DEF_PROP(is_sere_formula);
1679 SPOT_DEF_PROP(is_finite);
1687 SPOT_DEF_PROP(is_eventual);
1695 SPOT_DEF_PROP(is_universal);
1697 SPOT_DEF_PROP(is_syntactic_safety);
1699 SPOT_DEF_PROP(is_syntactic_guarantee);
1701 SPOT_DEF_PROP(is_syntactic_obligation);
1703 SPOT_DEF_PROP(is_syntactic_recurrence);
1705 SPOT_DEF_PROP(is_syntactic_persistence);
1708 SPOT_DEF_PROP(is_marked);
1710 SPOT_DEF_PROP(accepts_eword);
1716 SPOT_DEF_PROP(has_lbt_atomic_props);
1725 SPOT_DEF_PROP(has_spin_atomic_props);
1726#undef SPOT_DEF_PROP
1727
1731 template<typename Trans, typename... Args>
1732 formula map(Trans trans, Args&&... args)
1733 {
1734 switch (op o = kind())
1735 {
1736 case op::ff:
1737 case op::tt:
1738 case op::eword:
1739 case op::ap:
1740 return *this;
1741 case op::Not:
1742 case op::X:
1743#if SPOT_HAS_STRONG_X
1744 case op::strong_X:
1745#endif
1746 case op::F:
1747 case op::G:
1748 case op::Closure:
1749 case op::NegClosure:
1751 case op::first_match:
1752 return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1753 case op::Xor:
1754 case op::Implies:
1755 case op::Equiv:
1756 case op::U:
1757 case op::R:
1758 case op::W:
1759 case op::M:
1760 case op::EConcat:
1761 case op::EConcatMarked:
1762 case op::UConcat:
1763 {
1764 formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1765 return binop(o, tmp,
1766 trans((*this)[1], std::forward<Args>(args)...));
1767 }
1768 case op::Or:
1769 case op::OrRat:
1770 case op::And:
1771 case op::AndRat:
1772 case op::AndNLM:
1773 case op::Concat:
1774 case op::Fusion:
1775 {
1776 std::vector<formula> tmp;
1777 tmp.reserve(size());
1778 for (auto f: *this)
1779 tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1780 return multop(o, std::move(tmp));
1781 }
1782 case op::Star:
1783 case op::FStar:
1784 return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1785 min(), max());
1786 }
1787 SPOT_UNREACHABLE();
1788 }
1789
1798 template<typename Func, typename... Args>
1799 void traverse(Func func, Args&&... args)
1800 {
1801 if (func(*this, std::forward<Args>(args)...))
1802 return;
1803 for (auto f: *this)
1804 f.traverse(func, std::forward<Args>(args)...);
1805 }
1806
1807 private:
1808#ifndef SWIG
1809 [[noreturn]] static void report_ap_invalid_arg();
1810#endif
1811 };
1812
1814 SPOT_API
1815 std::ostream& print_formula_props(std::ostream& out, const formula& f,
1816 bool abbreviated = false);
1817
1819 SPOT_API
1820 std::list<std::string> list_formula_props(const formula& f);
1821
1823 SPOT_API
1824 std::ostream& operator<<(std::ostream& os, const formula& f);
1825}
1826
1827#ifndef SWIG
1828namespace std
1829{
1830 template <>
1831 struct hash<spot::formula>
1832 {
1833 size_t operator()(const spot::formula& x) const noexcept
1834 {
1835 return x.id();
1836 }
1837 };
1838}
1839#endif
Actual storage for formula nodes.
Definition: formula.hh:128
std::string kindstr() const
const fnode * boolean_operands(unsigned *width=nullptr) const
bool is_boolean() const
Definition: formula.hh:407
size_t id() const
Definition: formula.hh:275
bool is_ff() const
Definition: formula.hh:309
bool is_sugar_free_boolean() const
Definition: formula.hh:413
bool is_Kleene_star() const
Definition: formula.hh:345
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
const fnode *const * end() const
Definition: formula.hh:287
unsigned min() const
Definition: formula.hh:247
bool is_syntactic_safety() const
Definition: formula.hh:473
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:425
static const fnode * binop(op o, const fnode *f, const fnode *g)
unsigned size() const
Definition: formula.hh:263
static constexpr uint8_t unbounded()
Definition: formula.hh:158
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:234
unsigned max() const
Definition: formula.hh:255
const fnode * get_child_of(op o) const
Definition: formula.hh:224
const fnode * all_but(unsigned i) const
bool accepts_eword() const
Definition: formula.hh:509
bool is_eventual() const
Definition: formula.hh:461
bool is(op o1, op o2, op o3, op o4) const
Definition: formula.hh:205
static bool instances_check()
safety check for the reference counters
bool is_leaf() const
Definition: formula.hh:269
bool has_spin_atomic_props() const
Definition: formula.hh:521
bool is_eword() const
Definition: formula.hh:333
bool is(op o1, op o2, op o3) const
Definition: formula.hh:200
op kind() const
Definition: formula.hh:180
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:134
bool has_lbt_atomic_props() const
Definition: formula.hh:515
bool is_sugar_free_ltl() const
Definition: formula.hh:431
const std::string & ap_name() const
bool is_syntactic_persistence() const
Definition: formula.hh:497
unsigned boolean_count() const
Definition: formula.hh:378
static const fnode * tt()
Definition: formula.hh:315
bool is_universal() const
Definition: formula.hh:467
bool is_tt() const
Definition: formula.hh:321
bool is_constant() const
Definition: formula.hh:339
bool is_syntactic_recurrence() const
Definition: formula.hh:491
bool is(std::initializer_list< op > l) const
Definition: formula.hh:210
bool is_syntactic_obligation() const
Definition: formula.hh:485
static const fnode * unop(op o, const fnode *f)
const fnode * nth(unsigned i) const
Definition: formula.hh:293
bool is_ltl_formula() const
Definition: formula.hh:437
static const fnode * ff()
Definition: formula.hh:303
bool is_finite() const
Definition: formula.hh:455
bool is_psl_formula() const
Definition: formula.hh:443
static const fnode * eword()
Definition: formula.hh:327
bool is_marked() const
Definition: formula.hh:503
std::ostream & dump(std::ostream &os) const
void destroy() const
Dereference an fnode.
Definition: formula.hh:148
static const fnode * one_plus()
Definition: formula.hh:361
static const fnode * ap(const std::string &name)
bool is(op o1, op o2) const
Definition: formula.hh:195
bool is_in_nenoform() const
Definition: formula.hh:419
static const fnode * bunop(op o, const fnode *f, unsigned min, unsigned max=unbounded())
bool is_syntactic_guarantee() const
Definition: formula.hh:479
static const fnode * multop(op o, std::vector< const fnode * > l)
bool is_sere_formula() const
Definition: formula.hh:449
static const fnode * one_star()
Definition: formula.hh:353
const fnode *const * begin() const
Definition: formula.hh:281
bool is(op o) const
Definition: formula.hh:190
Allow iterating over children.
Definition: formula.hh:1453
Main class for temporal logic formula.
Definition: formula.hh:728
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1602
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1626
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1432
size_t id() const
Return the id of a formula.
Definition: formula.hh:1445
static formula bunop(op o, formula &&f, unsigned min=0U, unsigned max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1211
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1732
static formula bunop(op o, const formula &f, unsigned min=0U, unsigned max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1203
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition: formula.hh:981
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1017
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1347
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1133
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:765
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:735
bool is(op o1, op o2) const
Return true if the formula is of kind o1 or o2.
Definition: formula.hh:1354
static formula one_plus()
Return a copy of the formula 1[+].
Definition: formula.hh:1573
static formula sugar_delay(const formula &b, unsigned min, unsigned max)
Create the SERE a ##[n:m] b
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1566
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1409
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:868
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:901
static formula eword()
Return the empty word constant.
Definition: formula.hh:1539
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1612
static formula ff()
Return the false constant.
Definition: formula.hh:1515
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1023
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:785
op kind() const
Return top-most operator.
Definition: formula.hh:1335
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1593
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1122
unsigned size() const
Return the number of children.
Definition: formula.hh:1423
static formula sugar_goto(const formula &b, unsigned min, unsigned max)
Create a SERE equivalent to b[->min..max]
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1533
bool is(op o1, op o2, op o3, op o4) const
Definition: formula.hh:1367
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1341
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:757
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1502
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1326
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1033
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:884
formula get_child_of(std::initializer_list< op > l) const
Remove all operators in l and return the child.
Definition: formula.hh:1397
bool is_eword() const
Whether the formula is the empty word constant.
Definition: formula.hh:1545
static formula sugar_delay(const formula &a, const formula &b, unsigned min, unsigned max)
Create the SERE a ##[n:m] b
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1799
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition: formula.hh:970
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:745
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:874
bool is(op o1, op o2, op o3) const
Return true if the formula is of kind o1 or o2 or o3.
Definition: formula.hh:1360
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1417
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition: formula.hh:938
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1521
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1496
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition: formula.hh:1551
~formula()
Destroy a formula.
Definition: formula.hh:772
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1382
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition: formula.hh:1373
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1508
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1560
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1028
bool is_literal() const
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1581
static formula tt()
Return the true constant.
Definition: formula.hh:1527
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:751
static formula sugar_equal(const formula &b, unsigned min, unsigned max)
Create the SERE b[=min..max]
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:895
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1644
static const formula nested_unop_range(op uo, op bo, unsigned min, unsigned max, formula f)
Nested operator construction (syntactic sugar).
Definition: formula.hh:1268
op
Operator types.
Definition: formula.hh:79
@ X
Next.
@ first_match
first_match(sere)
@ EConcatMarked
Seq, Marked.
@ Star
Star.
@ UConcat
Triggers.
@ Or
(omega-Rational) Or
@ Equiv
Equivalence.
@ NegClosure
Negated PSL Closure.
@ U
until
@ EConcat
Seq.
@ FStar
Fustion Star.
@ W
weak until
@ ap
Atomic proposition.
@ ff
False.
@ M
strong release (dual of weak until)
@ NegClosureMarked
marked version of the Negated PSL Closure
@ Xor
Exclusive Or.
@ F
Eventually.
@ OrRat
Rational Or.
@ Not
Negation.
@ tt
True.
@ Fusion
Fusion.
@ Closure
PSL Closure.
@ And
(omega-Rational) And
@ AndNLM
Non-Length-Matching Rational-And.
@ eword
Empty word.
@ AndRat
Rational And.
@ G
Globally.
@ R
release (dual of until)
@ Concat
Concatenation.
@ Implies
Implication.
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
Definition: automata.hh:27
int atomic_prop_cmp(const fnode *f, const fnode *g)
Order two atomic propositions.
std::list< std::string > list_formula_props(const formula &f)
List the properties of formula f.
std::ostream & print_formula_props(std::ostream &out, const formula &f, bool abbreviated=false)
Print the properties of formula f on stream out.
Definition: formula.hh:656

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4