spot 2.11.6.dev
Loading...
Searching...
No Matches
formula.hh
Go to the documentation of this file.
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015-2023 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 may #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
655 class SPOT_API formula;
656
658 {
659 bool
660 operator()(const fnode* left, const fnode* right) const
661 {
662 SPOT_ASSERT(left);
663 SPOT_ASSERT(right);
664 if (left == right)
665 return false;
666
667 // We want Boolean formulae first.
668 bool lib = left->is_boolean();
669 if (lib != right->is_boolean())
670 return lib;
671
672 // We have two Boolean formulae
673 if (lib)
674 {
675 bool lconst = left->is_constant();
676 if (lconst != right->is_constant())
677 return lconst;
678 if (!lconst)
679 {
680 auto get_literal = [](const fnode* f) -> const fnode*
681 {
682 if (f->is(op::Not))
683 f = f->nth(0);
684 if (f->is(op::ap))
685 return f;
686 return nullptr;
687 };
688 // Literals should come first
689 const fnode* litl = get_literal(left);
690 const fnode* litr = get_literal(right);
691 if (!litl != !litr)
692 return litl;
693 if (litl)
694 {
695 // And they should be sorted alphabetically
696 int cmp = atomic_prop_cmp(litl, litr);
697 if (cmp)
698 return cmp < 0;
699 }
700 }
701 }
702
703 size_t l = left->id();
704 size_t r = right->id();
705 if (l != r)
706 return l < r;
707 // Because the hash code assigned to each formula is the
708 // number of formulae constructed so far, it is very unlikely
709 // that we will ever reach a case were two different formulae
710 // have the same hash. This will happen only ever with have
711 // produced 256**sizeof(size_t) formulae (i.e. max_count has
712 // looped back to 0 and started over). In that case we can
713 // order two formulas by looking at their text representation.
714 // We could be more efficient and look at their AST, but it's
715 // not worth the burden. (Also ordering pointers is ruled out
716 // because it breaks the determinism of the implementation.)
717 std::ostringstream old;
718 left->dump(old);
719 std::ostringstream ord;
720 right->dump(ord);
721 return old.str() < ord.str();
722 }
723
724 SPOT_API bool
725 operator()(const formula& left, const formula& right) const;
726};
727
728#endif // SWIG
729
732 class SPOT_API formula final
733 {
735 const fnode* ptr_;
736 public:
741 explicit formula(const fnode* f) noexcept
742 : ptr_(f)
743 {
744 }
745
751 formula(std::nullptr_t) noexcept
752 : ptr_(nullptr)
753 {
754 }
755
757 formula() noexcept
758 : ptr_(nullptr)
759 {
760 }
761
763 formula(const formula& f) noexcept
764 : ptr_(f.ptr_)
765 {
766 if (ptr_)
767 ptr_->clone();
768 }
769
771 formula(formula&& f) noexcept
772 : ptr_(f.ptr_)
773 {
774 f.ptr_ = nullptr;
775 }
776
779 {
780 if (ptr_)
781 ptr_->destroy();
782 }
783
791 const formula& operator=(std::nullptr_t)
792 {
793 this->~formula();
794 ptr_ = nullptr;
795 return *this;
796 }
797
798 const formula& operator=(const formula& f)
799 {
800 this->~formula();
801 if ((ptr_ = f.ptr_))
802 ptr_->clone();
803 return *this;
804 }
805
806 const formula& operator=(formula&& f) noexcept
807 {
808 std::swap(f.ptr_, ptr_);
809 return *this;
810 }
811
812 bool operator<(const formula& other) const noexcept
813 {
814 if (SPOT_UNLIKELY(!other.ptr_))
815 return false;
816 if (SPOT_UNLIKELY(!ptr_))
817 return true;
818 if (id() < other.id())
819 return true;
820 if (id() > other.id())
821 return false;
822 // The case where id()==other.id() but ptr_ != other.ptr_ is
823 // very unlikely (we would need to build more than UINT_MAX
824 // formulas), so let's just compare pointers, and ignore the
825 // fact that it may introduce some nondeterminism.
826 return ptr_ < other.ptr_;
827 }
828
829 bool operator<=(const formula& other) const noexcept
830 {
831 return *this == other || *this < other;
832 }
833
834 bool operator>(const formula& other) const noexcept
835 {
836 return !(*this <= other);
837 }
838
839 bool operator>=(const formula& other) const noexcept
840 {
841 return !(*this < other);
842 }
843
844 bool operator==(const formula& other) const noexcept
845 {
846 return other.ptr_ == ptr_;
847 }
848
849 bool operator==(std::nullptr_t) const noexcept
850 {
851 return ptr_ == nullptr;
852 }
853
854 bool operator!=(const formula& other) const noexcept
855 {
856 return other.ptr_ != ptr_;
857 }
858
859 bool operator!=(std::nullptr_t) const noexcept
860 {
861 return ptr_ != nullptr;
862 }
863
864 explicit operator bool() const noexcept
865 {
866 return ptr_ != nullptr;
867 }
868
870 // Forwarded functions //
872
874 static constexpr uint8_t unbounded()
875 {
876 return fnode::unbounded();
877 }
878
880 static formula ap(const std::string& name)
881 {
882 return formula(fnode::ap(name));
883 }
884
890 static formula ap(const formula& a)
891 {
892 if (SPOT_UNLIKELY(a.kind() != op::ap))
893 report_ap_invalid_arg();
894 return a;
895 }
896
901 static formula unop(op o, const formula& f)
902 {
903 return formula(fnode::unop(o, f.ptr_->clone()));
904 }
905
906#ifndef SWIG
907 static formula unop(op o, formula&& f)
908 {
909 return formula(fnode::unop(o, f.to_node_()));
910 }
911#endif // !SWIG
913
914#ifdef SWIG
915#define SPOT_DEF_UNOP(Name) \
916 static formula Name(const formula& f) \
917 { \
918 return unop(op::Name, f); \
919 }
920#else // !SWIG
921#define SPOT_DEF_UNOP(Name) \
922 static formula Name(const formula& f) \
923 { \
924 return unop(op::Name, f); \
925 } \
926 static formula Name(formula&& f) \
927 { \
928 return unop(op::Name, std::move(f)); \
929 }
930#endif // !SWIG
933 SPOT_DEF_UNOP(Not);
935
938 SPOT_DEF_UNOP(X);
940
944 static formula X(unsigned level, const formula& f)
945 {
946 return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
947 }
948
949#if SPOT_WANT_STRONG_X
952 SPOT_DEF_UNOP(strong_X);
954
958 static formula strong_X(unsigned level, const formula& f)
959 {
960 return nested_unop_range(op::strong_X, op::Or /* unused */,
961 level, level, f);
962 }
963#endif
964
967 SPOT_DEF_UNOP(F);
969
976 static formula F(unsigned min_level, unsigned max_level, const formula& f)
977 {
978 return nested_unop_range(op::X, op::Or, min_level, max_level, f);
979 }
980
987 static formula G(unsigned min_level, unsigned max_level, const formula& f)
988 {
989 return nested_unop_range(op::X, op::And, min_level, max_level, f);
990 }
991
994 SPOT_DEF_UNOP(G);
996
999 SPOT_DEF_UNOP(Closure);
1001
1004 SPOT_DEF_UNOP(NegClosure);
1006
1009 SPOT_DEF_UNOP(NegClosureMarked);
1011
1014 SPOT_DEF_UNOP(first_match);
1016#undef SPOT_DEF_UNOP
1017
1023 static formula binop(op o, const formula& f, const formula& g)
1024 {
1025 return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
1026 }
1027
1028#ifndef SWIG
1029 static formula binop(op o, const formula& f, formula&& g)
1030 {
1031 return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
1032 }
1033
1034 static formula binop(op o, formula&& f, const formula& g)
1035 {
1036 return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
1037 }
1038
1039 static formula binop(op o, formula&& f, formula&& g)
1040 {
1041 return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
1042 }
1044
1045#endif //SWIG
1046
1047#ifdef 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#else // !SWIG
1054#define SPOT_DEF_BINOP(Name) \
1055 static formula Name(const formula& f, const formula& g) \
1056 { \
1057 return binop(op::Name, f, g); \
1058 } \
1059 static formula Name(const formula& f, formula&& g) \
1060 { \
1061 return binop(op::Name, f, std::move(g)); \
1062 } \
1063 static formula Name(formula&& f, const formula& g) \
1064 { \
1065 return binop(op::Name, std::move(f), g); \
1066 } \
1067 static formula Name(formula&& f, formula&& g) \
1068 { \
1069 return binop(op::Name, std::move(f), std::move(g)); \
1070 }
1071#endif // !SWIG
1074 SPOT_DEF_BINOP(Xor);
1076
1079 SPOT_DEF_BINOP(Implies);
1081
1084 SPOT_DEF_BINOP(Equiv);
1086
1089 SPOT_DEF_BINOP(U);
1091
1094 SPOT_DEF_BINOP(R);
1096
1099 SPOT_DEF_BINOP(W);
1101
1104 SPOT_DEF_BINOP(M);
1106
1109 SPOT_DEF_BINOP(EConcat);
1111
1114 SPOT_DEF_BINOP(EConcatMarked);
1116
1119 SPOT_DEF_BINOP(UConcat);
1121#undef SPOT_DEF_BINOP
1122
1128 static formula multop(op o, const std::vector<formula>& l)
1129 {
1130 std::vector<const fnode*> tmp;
1131 tmp.reserve(l.size());
1132 for (auto f: l)
1133 if (f.ptr_)
1134 tmp.emplace_back(f.ptr_->clone());
1135 return formula(fnode::multop(o, std::move(tmp)));
1136 }
1137
1138#ifndef SWIG
1139 static formula multop(op o, std::vector<formula>&& l)
1140 {
1141 std::vector<const fnode*> tmp;
1142 tmp.reserve(l.size());
1143 for (auto f: l)
1144 if (f.ptr_)
1145 tmp.emplace_back(f.to_node_());
1146 return formula(fnode::multop(o, std::move(tmp)));
1147 }
1148#endif // !SWIG
1150
1151#ifdef 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#else // !SWIG
1158#define SPOT_DEF_MULTOP(Name) \
1159 static formula Name(const std::vector<formula>& l) \
1160 { \
1161 return multop(op::Name, l); \
1162 } \
1163 \
1164 static formula Name(std::vector<formula>&& l) \
1165 { \
1166 return multop(op::Name, std::move(l)); \
1167 }
1168#endif // !SWIG
1171 SPOT_DEF_MULTOP(Or);
1173
1176 SPOT_DEF_MULTOP(OrRat);
1178
1181 SPOT_DEF_MULTOP(And);
1183
1186 SPOT_DEF_MULTOP(AndRat);
1188
1191 SPOT_DEF_MULTOP(AndNLM);
1193
1196 SPOT_DEF_MULTOP(Concat);
1198
1201 SPOT_DEF_MULTOP(Fusion);
1203#undef SPOT_DEF_MULTOP
1204
1209 static formula bunop(op o, const formula& f,
1210 unsigned min = 0U,
1211 unsigned max = unbounded())
1212 {
1213 return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1214 }
1215
1216#ifndef SWIG
1217 static formula bunop(op o, formula&& f,
1218 unsigned min = 0U,
1219 unsigned max = unbounded())
1220 {
1221 return formula(fnode::bunop(o, f.to_node_(), min, max));
1222 }
1223#endif // !SWIG
1225
1226#if SWIG
1227#define SPOT_DEF_BUNOP(Name) \
1228 static formula Name(const formula& f, \
1229 unsigned min = 0U, \
1230 unsigned max = unbounded()) \
1231 { \
1232 return bunop(op::Name, f, min, max); \
1233 }
1234#else // !SWIG
1235#define SPOT_DEF_BUNOP(Name) \
1236 static formula Name(const formula& f, \
1237 unsigned min = 0U, \
1238 unsigned max = unbounded()) \
1239 { \
1240 return bunop(op::Name, f, min, max); \
1241 } \
1242 static formula Name(formula&& f, \
1243 unsigned min = 0U, \
1244 unsigned max = unbounded()) \
1245 { \
1246 return bunop(op::Name, std::move(f), min, max); \
1247 }
1248#endif
1251 SPOT_DEF_BUNOP(Star);
1253
1259 SPOT_DEF_BUNOP(FStar);
1261#undef SPOT_DEF_BUNOP
1262
1274 static const formula nested_unop_range(op uo, op bo, unsigned min,
1275 unsigned max, formula f)
1276 {
1277 return formula(fnode::nested_unop_range(uo, bo, min, max,
1278 f.ptr_->clone()));
1279 }
1280
1286 static formula sugar_goto(const formula& b, unsigned min, unsigned max);
1287
1293 static formula sugar_equal(const formula& b, unsigned min, unsigned max);
1294
1316 static formula sugar_delay(const formula& a, const formula& b,
1317 unsigned min, unsigned max);
1318 static formula sugar_delay(const formula& b,
1319 unsigned min, unsigned max);
1321
1322#ifndef SWIG
1333 {
1334 auto tmp = ptr_;
1335 ptr_ = nullptr;
1336 return tmp;
1337 }
1338#endif
1339
1341 op kind() const
1342 {
1343 return ptr_->kind();
1344 }
1345
1347 std::string kindstr() const
1348 {
1349 return ptr_->kindstr();
1350 }
1351
1353 bool is(op o) const
1354 {
1355 return ptr_->is(o);
1356 }
1357
1358#ifndef SWIG
1360 bool is(op o1, op o2) const
1361 {
1362 return ptr_->is(o1, o2);
1363 }
1364
1366 bool is(op o1, op o2, op o3) const
1367 {
1368 return ptr_->is(o1, o2, o3);
1369 }
1370
1373 bool is(op o1, op o2, op o3, op o4) const
1374 {
1375 return ptr_->is(o1, o2, o3, o4);
1376 }
1377
1379 bool is(std::initializer_list<op> l) const
1380 {
1381 return ptr_->is(l);
1382 }
1383#endif
1384
1389 {
1390 auto f = ptr_->get_child_of(o);
1391 if (f)
1392 f->clone();
1393 return formula(f);
1394 }
1395
1396#ifndef SWIG
1403 formula get_child_of(std::initializer_list<op> l) const
1404 {
1405 auto f = ptr_->get_child_of(l);
1406 if (f)
1407 f->clone();
1408 return formula(f);
1409 }
1410#endif
1411
1415 unsigned min() const
1416 {
1417 return ptr_->min();
1418 }
1419
1423 unsigned max() const
1424 {
1425 return ptr_->max();
1426 }
1427
1429 unsigned size() const
1430 {
1431 return ptr_->size();
1432 }
1433
1438 bool is_leaf() const
1439 {
1440 return ptr_->is_leaf();
1441 }
1442
1451 size_t id() const
1452 {
1453 return ptr_->id();
1454 }
1455
1456#ifndef SWIG
1458 class SPOT_API formula_child_iterator final
1459 {
1460 const fnode*const* ptr_;
1461 public:
1463 : ptr_(nullptr)
1464 {
1465 }
1466
1467 formula_child_iterator(const fnode*const* f)
1468 : ptr_(f)
1469 {
1470 }
1471
1472 bool operator==(formula_child_iterator o)
1473 {
1474 return ptr_ == o.ptr_;
1475 }
1476
1477 bool operator!=(formula_child_iterator o)
1478 {
1479 return ptr_ != o.ptr_;
1480 }
1481
1482 formula operator*()
1483 {
1484 return formula((*ptr_)->clone());
1485 }
1486
1487 formula_child_iterator operator++()
1488 {
1489 ++ptr_;
1490 return *this;
1491 }
1492
1493 formula_child_iterator operator++(int)
1494 {
1495 auto tmp = *this;
1496 ++ptr_;
1497 return tmp;
1498 }
1499 };
1500
1503 {
1504 return ptr_->begin();
1505 }
1506
1509 {
1510 return ptr_->end();
1511 }
1512
1514 formula operator[](unsigned i) const
1515 {
1516 return formula(ptr_->nth(i)->clone());
1517 }
1518#endif
1519
1521 static formula ff()
1522 {
1523 return formula(fnode::ff());
1524 }
1525
1527 bool is_ff() const
1528 {
1529 return ptr_->is_ff();
1530 }
1531
1533 static formula tt()
1534 {
1535 return formula(fnode::tt());
1536 }
1537
1539 bool is_tt() const
1540 {
1541 return ptr_->is_tt();
1542 }
1543
1546 {
1547 return formula(fnode::eword());
1548 }
1549
1551 bool is_eword() const
1552 {
1553 return ptr_->is_eword();
1554 }
1555
1557 bool is_constant() const
1558 {
1559 return ptr_->is_constant();
1560 }
1561
1566 bool is_Kleene_star() const
1567 {
1568 return ptr_->is_Kleene_star();
1569 }
1570
1573 {
1574 // no need to clone, 1[*] is not reference counted
1575 return formula(fnode::one_star());
1576 }
1577
1580 {
1581 // no need to clone, 1[+] is not reference counted
1582 return formula(fnode::one_plus());
1583 }
1584
1587 bool is_literal() const
1588 {
1589 return (is(op::ap) ||
1590 // If f is in nenoform, Not can only occur in front of
1591 // an atomic proposition. So this way we do not have
1592 // to check the type of the child.
1593 (is(op::Not) && is_boolean() && is_in_nenoform()));
1594 }
1595
1599 const std::string& ap_name() const
1600 {
1601 return ptr_->ap_name();
1602 }
1603
1608 std::ostream& dump(std::ostream& os) const
1609 {
1610 return ptr_->dump(os);
1611 }
1612
1618 formula all_but(unsigned i) const
1619 {
1620 return formula(ptr_->all_but(i));
1621 }
1622
1632 unsigned boolean_count() const
1633 {
1634 return ptr_->boolean_count();
1635 }
1636
1650 formula boolean_operands(unsigned* width = nullptr) const
1651 {
1652 return formula(ptr_->boolean_operands(width));
1653 }
1654
1655#define SPOT_DEF_PROP(Name) \
1656 bool Name() const \
1657 { \
1658 return ptr_->Name(); \
1659 }
1661 // Properties //
1663
1665 SPOT_DEF_PROP(is_boolean);
1667 SPOT_DEF_PROP(is_sugar_free_boolean);
1672 SPOT_DEF_PROP(is_in_nenoform);
1674 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1676 SPOT_DEF_PROP(is_sugar_free_ltl);
1678 SPOT_DEF_PROP(is_ltl_formula);
1680 SPOT_DEF_PROP(is_psl_formula);
1682 SPOT_DEF_PROP(is_sere_formula);
1685 SPOT_DEF_PROP(is_finite);
1693 SPOT_DEF_PROP(is_eventual);
1701 SPOT_DEF_PROP(is_universal);
1703 SPOT_DEF_PROP(is_syntactic_safety);
1705 SPOT_DEF_PROP(is_syntactic_guarantee);
1707 SPOT_DEF_PROP(is_syntactic_obligation);
1709 SPOT_DEF_PROP(is_syntactic_recurrence);
1711 SPOT_DEF_PROP(is_syntactic_persistence);
1714 SPOT_DEF_PROP(is_marked);
1716 SPOT_DEF_PROP(accepts_eword);
1722 SPOT_DEF_PROP(has_lbt_atomic_props);
1731 SPOT_DEF_PROP(has_spin_atomic_props);
1732#undef SPOT_DEF_PROP
1733
1737 template<typename Trans, typename... Args>
1738 formula map(Trans trans, Args&&... args)
1739 {
1740 switch (op o = kind())
1741 {
1742 case op::ff:
1743 case op::tt:
1744 case op::eword:
1745 case op::ap:
1746 return *this;
1747 case op::Not:
1748 case op::X:
1749#if SPOT_HAS_STRONG_X
1750 case op::strong_X:
1751#endif
1752 case op::F:
1753 case op::G:
1754 case op::Closure:
1755 case op::NegClosure:
1756 case op::NegClosureMarked:
1757 case op::first_match:
1758 return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1759 case op::Xor:
1760 case op::Implies:
1761 case op::Equiv:
1762 case op::U:
1763 case op::R:
1764 case op::W:
1765 case op::M:
1766 case op::EConcat:
1767 case op::EConcatMarked:
1768 case op::UConcat:
1769 {
1770 formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1771 return binop(o, tmp,
1772 trans((*this)[1], std::forward<Args>(args)...));
1773 }
1774 case op::Or:
1775 case op::OrRat:
1776 case op::And:
1777 case op::AndRat:
1778 case op::AndNLM:
1779 case op::Concat:
1780 case op::Fusion:
1781 {
1782 std::vector<formula> tmp;
1783 tmp.reserve(size());
1784 for (auto f: *this)
1785 tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1786 return multop(o, std::move(tmp));
1787 }
1788 case op::Star:
1789 case op::FStar:
1790 return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1791 min(), max());
1792 }
1793 SPOT_UNREACHABLE();
1794 }
1795
1804 template<typename Func, typename... Args>
1805 void traverse(Func func, Args&&... args)
1806 {
1807 if (func(*this, std::forward<Args>(args)...))
1808 return;
1809 for (auto f: *this)
1810 f.traverse(func, std::forward<Args>(args)...);
1811 }
1812
1813 private:
1814#ifndef SWIG
1815 [[noreturn]] static void report_ap_invalid_arg();
1816#endif
1817 };
1818
1820 SPOT_API
1821 std::ostream& print_formula_props(std::ostream& out, const formula& f,
1822 bool abbreviated = false);
1823
1825 SPOT_API
1826 std::list<std::string> list_formula_props(const formula& f);
1827
1829 SPOT_API
1830 std::ostream& operator<<(std::ostream& os, const formula& f);
1831}
1832
1833#ifndef SWIG
1834namespace std
1835{
1836 template <>
1837 struct hash<spot::formula>
1838 {
1839 size_t operator()(const spot::formula& x) const noexcept
1840 {
1841 return x.id();
1842 }
1843 };
1844}
1845#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:1459
Main class for temporal logic formula.
Definition formula.hh:733
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition formula.hh:1608
unsigned boolean_count() const
number of Boolean children
Definition formula.hh:1632
bool is_leaf() const
Whether the formula is a leaf.
Definition formula.hh:1438
size_t id() const
Return the id of a formula.
Definition formula.hh:1451
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:1217
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition formula.hh:1738
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:1209
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition formula.hh:987
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition formula.hh:1023
bool is(op o) const
Return true if the formula is of kind o.
Definition formula.hh:1353
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition formula.hh:1139
formula(formula &&f) noexcept
Move-construct a formula.
Definition formula.hh:771
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition formula.hh:741
bool is(op o1, op o2) const
Return true if the formula is of kind o1 or o2.
Definition formula.hh:1360
static formula one_plus()
Return a copy of the formula 1[+].
Definition formula.hh:1579
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:1572
unsigned min() const
Return start of the range for star-like operators.
Definition formula.hh:1415
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition formula.hh:874
static formula unop(op o, formula &&f)
Build a unary operator.
Definition formula.hh:907
static formula eword()
Return the empty word constant.
Definition formula.hh:1545
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition formula.hh:1618
static formula ff()
Return the false constant.
Definition formula.hh:1521
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition formula.hh:1029
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition formula.hh:791
op kind() const
Return top-most operator.
Definition formula.hh:1341
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition formula.hh:1599
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition formula.hh:1128
unsigned size() const
Return the number of children.
Definition formula.hh:1429
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:1539
bool is(op o1, op o2, op o3, op o4) const
Definition formula.hh:1373
std::string kindstr() const
Return the name of the top-most operator.
Definition formula.hh:1347
formula(const formula &f) noexcept
Clone a formula.
Definition formula.hh:763
formula_child_iterator end() const
Allow iterating over children.
Definition formula.hh:1508
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition formula.hh:1332
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition formula.hh:1039
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition formula.hh:890
formula get_child_of(std::initializer_list< op > l) const
Remove all operators in l and return the child.
Definition formula.hh:1403
bool is_eword() const
Whether the formula is the empty word constant.
Definition formula.hh:1551
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:1805
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition formula.hh:976
formula(std::nullptr_t) noexcept
Create a null formula.
Definition formula.hh:751
static formula ap(const std::string &name)
Build an atomic proposition.
Definition formula.hh:880
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:1366
unsigned max() const
Return end of the range for star-like operators.
Definition formula.hh:1423
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition formula.hh:944
bool is_ff() const
Whether the formula is the false constant.
Definition formula.hh:1527
formula_child_iterator begin() const
Allow iterating over children.
Definition formula.hh:1502
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition formula.hh:1557
~formula()
Destroy a formula.
Definition formula.hh:778
formula get_child_of(op o) const
Remove operator o and return the child.
Definition formula.hh:1388
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition formula.hh:1379
formula operator[](unsigned i) const
Return children number i.
Definition formula.hh:1514
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition formula.hh:1566
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition formula.hh:1034
bool is_literal() const
Whether the formula is an atomic proposition or its negation.
Definition formula.hh:1587
static formula tt()
Return the true constant.
Definition formula.hh:1533
formula() noexcept
Default initialize a formula to nullptr.
Definition formula.hh:757
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:901
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition formula.hh:1650
static const formula nested_unop_range(op uo, op bo, unsigned min, unsigned max, formula f)
Nested operator construction (syntactic sugar).
Definition formula.hh:1274
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.
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.

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.8