spot  2.12.2
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
21 #pragma once
22 
29 
32 
35 
38 
41 
44 
45 #include <spot/misc/common.hh>
46 #include <memory>
47 #include <cstdint>
48 #include <initializer_list>
49 #include <cassert>
50 #include <vector>
51 #include <string>
52 #include <iterator>
53 #include <iosfwd>
54 #include <sstream>
55 #include <list>
56 #include <cstddef>
57 #include <limits>
58 
59 // The strong_X operator was introduced in Spot 2.8.2 to fix an issue
60 // with from_ltlf(). As adding a new operator is a backward
61 // incompatibility, causing new warnings from the compiler.
62 #if defined(SPOT_BUILD) || defined(SPOT_USES_STRONG_X)
63 // Use #if SPOT_HAS_STRONG_X in code that need to be backward
64 // compatible with older Spot versions.
65 # define SPOT_HAS_STRONG_X 1
66 // You may #define SPOT_WANT_STRONG_X yourself before including
67 // this file to force the use of STRONG_X
68 # define SPOT_WANT_STRONG_X 1
69 #endif
70 
71 namespace spot
72 {
73 
74 
77  enum class op: uint8_t
78  {
79  ff,
80  tt,
81  eword,
82  ap,
83  // unary operators
84  Not,
85  X,
86  F,
87  G,
88  Closure,
89  NegClosure,
91  // binary operators
92  Xor,
93  Implies,
94  Equiv,
95  U,
96  R,
97  W,
98  M,
99  EConcat,
100  EConcatMarked,
101  UConcat,
102  // n-ary operators
103  Or,
104  OrRat,
105  And,
106  AndRat,
107  AndNLM,
108  Concat,
109  Fusion,
110  // star-like operators
111  Star,
112  FStar,
113  first_match,
114 #ifdef SPOT_WANT_STRONG_X
115  strong_X,
116 #endif
117  };
118 
119 #ifndef SWIG
126  class SPOT_API fnode final
127  {
128  public:
133  const fnode* clone() const
134  {
135  // Saturate.
136  ++refs_;
137  if (SPOT_UNLIKELY(!refs_))
138  saturated_ = 1;
139  return this;
140  }
141 
147  void destroy() const
148  {
149  if (SPOT_LIKELY(refs_))
150  --refs_;
151  else if (SPOT_LIKELY(!saturated_))
152  // last reference to a node that is not a constant
153  destroy_aux();
154  }
155 
157  static constexpr uint8_t unbounded()
158  {
159  return UINT8_MAX;
160  }
161 
163  static const fnode* ap(const std::string& name);
165  static const fnode* unop(op o, const fnode* f);
167  static const fnode* binop(op o, const fnode* f, const fnode* g);
169  static const fnode* multop(op o, std::vector<const fnode*> l);
171  static const fnode* bunop(op o, const fnode* f,
172  unsigned min, unsigned max = unbounded());
173 
175  static const fnode* nested_unop_range(op uo, op bo, unsigned min,
176  unsigned max, const fnode* f);
177 
179  op kind() const
180  {
181  return op_;
182  }
183 
185  std::string kindstr() const;
186 
189  bool is(op o) const
190  {
191  return op_ == o;
192  }
193 
194  bool is(op o1, op o2) const
195  {
196  return op_ == o1 || op_ == o2;
197  }
198 
199  bool is(op o1, op o2, op o3) const
200  {
201  return op_ == o1 || op_ == o2 || op_ == o3;
202  }
203 
204  bool is(op o1, op o2, op o3, op o4) const
205  {
206  return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
207  }
208 
209  bool is(std::initializer_list<op> l) const
210  {
211  const fnode* n = this;
212  for (auto o: l)
213  {
214  if (!n->is(o))
215  return false;
216  n = n->nth(0);
217  }
218  return true;
219  }
221 
223  const fnode* get_child_of(op o) const
224  {
225  if (op_ != o)
226  return nullptr;
227  if (SPOT_UNLIKELY(size_ != 1))
228  report_get_child_of_expecting_single_child_node();
229  return nth(0);
230  }
231 
233  const fnode* get_child_of(std::initializer_list<op> l) const
234  {
235  auto c = this;
236  for (auto o: l)
237  {
238  c = c->get_child_of(o);
239  if (c == nullptr)
240  return c;
241  }
242  return c;
243  }
244 
246  unsigned min() const
247  {
248  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
249  report_min_invalid_arg();
250  return min_;
251  }
252 
254  unsigned max() const
255  {
256  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
257  report_max_invalid_arg();
258  return max_;
259  }
260 
262  unsigned size() const
263  {
264  return size_;
265  }
266 
268  bool is_leaf() const
269  {
270  return size_ == 0;
271  }
272 
274  size_t id() const
275  {
276  return id_;
277  }
278 
280  const fnode*const* begin() const
281  {
282  return children;
283  }
284 
286  const fnode*const* end() const
287  {
288  return children + size();
289  }
290 
292  const fnode* nth(unsigned i) const
293  {
294  if (SPOT_UNLIKELY(i >= size()))
295  report_non_existing_child();
296  const fnode* c = children[i];
297  SPOT_ASSUME(c != nullptr);
298  return c;
299  }
300 
302  static const fnode* ff()
303  {
304  return ff_;
305  }
306 
308  bool is_ff() const
309  {
310  return op_ == op::ff;
311  }
312 
314  static const fnode* tt()
315  {
316  return tt_;
317  }
318 
320  bool is_tt() const
321  {
322  return op_ == op::tt;
323  }
324 
326  static const fnode* eword()
327  {
328  return ew_;
329  }
330 
332  bool is_eword() const
333  {
334  return op_ == op::eword;
335  }
336 
338  bool is_constant() const
339  {
340  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
341  }
342 
344  bool is_Kleene_star() const
345  {
346  if (op_ != op::Star)
347  return false;
348  return min_ == 0 && max_ == unbounded();
349  }
350 
352  static const fnode* one_star()
353  {
354  if (!one_star_)
355  one_star_ = new fnode(op::Star, tt_, 0, unbounded(), true);
356  return one_star_;
357  }
358 
360  static const fnode* one_plus()
361  {
362  if (!one_plus_)
363  one_plus_ = new fnode(op::Star, tt_, 1, unbounded(), true);
364  return one_plus_;
365  }
366 
368  const std::string& ap_name() const;
369 
371  std::ostream& dump(std::ostream& os) const;
372 
374  const fnode* all_but(unsigned i) const;
375 
377  unsigned boolean_count() const
378  {
379  unsigned pos = 0;
380  unsigned s = size();
381  while (pos < s && children[pos]->is_boolean())
382  ++pos;
383  return pos;
384  }
385 
387  const fnode* boolean_operands(unsigned* width = nullptr) const;
388 
399  static bool instances_check();
400 
402  // Properties //
404 
406  bool is_boolean() const
407  {
408  return is_.boolean;
409  }
410 
413  {
414  return is_.sugar_free_boolean;
415  }
416 
418  bool is_in_nenoform() const
419  {
420  return is_.in_nenoform;
421  }
422 
425  {
426  return is_.syntactic_si;
427  }
428 
430  bool is_sugar_free_ltl() const
431  {
432  return is_.sugar_free_ltl;
433  }
434 
436  bool is_ltl_formula() const
437  {
438  return is_.ltl_formula;
439  }
440 
442  bool is_psl_formula() const
443  {
444  return is_.psl_formula;
445  }
446 
448  bool is_sere_formula() const
449  {
450  return is_.sere_formula;
451  }
452 
454  bool is_finite() const
455  {
456  return is_.finite;
457  }
458 
460  bool is_eventual() const
461  {
462  return is_.eventual;
463  }
464 
466  bool is_universal() const
467  {
468  return is_.universal;
469  }
470 
472  bool is_syntactic_safety() const
473  {
474  return is_.syntactic_safety;
475  }
476 
479  {
480  return is_.syntactic_guarantee;
481  }
482 
485  {
486  return is_.syntactic_obligation;
487  }
488 
491  {
492  return is_.syntactic_recurrence;
493  }
494 
497  {
498  return is_.syntactic_persistence;
499  }
500 
502  bool is_marked() const
503  {
504  return !is_.not_marked;
505  }
506 
508  bool accepts_eword() const
509  {
510  return is_.accepting_eword;
511  }
512 
514  bool has_lbt_atomic_props() const
515  {
516  return is_.lbt_atomic_props;
517  }
518 
521  {
522  return is_.spin_atomic_props;
523  }
524 
525  private:
526  static size_t bump_next_id();
527  void setup_props(op o);
528  void destroy_aux() const;
529 
530  [[noreturn]] static void report_non_existing_child();
531  [[noreturn]] static void report_too_many_children();
532  [[noreturn]] static void
533  report_get_child_of_expecting_single_child_node();
534  [[noreturn]] static void report_min_invalid_arg();
535  [[noreturn]] static void report_max_invalid_arg();
536 
537  static const fnode* unique(fnode*);
538 
539  // Destruction may only happen via destroy().
540  ~fnode() = default;
541  // Disallow copies.
542  fnode(const fnode&) = delete;
543  fnode& operator=(const fnode&) = delete;
544 
545 
546 
547  template<class iter>
548  fnode(op o, iter begin, iter end, bool saturated = false)
549  // Clang has some optimization where is it able to combine the
550  // 4 movb initializing op_,min_,max_,saturated_ into a single
551  // movl. Also it can optimize the three byte-comparisons of
552  // is_Kleene_star() into a single masked 32-bit comparison.
553  // The latter optimization triggers warnings from valgrind if
554  // min_ and max_ are not initialized. So to benefit from the
555  // initialization optimization and the is_Kleene_star()
556  // optimization in Clang, we always initialize min_ and max_
557  // with this compiler. Do not do it the rest of the time,
558  // since the optimization is not done.
559  : op_(o),
560 #if __llvm__
561  min_(0), max_(0),
562 #endif
563  saturated_(saturated)
564  {
565  size_t s = std::distance(begin, end);
566  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
567  report_too_many_children();
568  size_ = s;
569  auto pos = children;
570  for (auto i = begin; i != end; ++i)
571  *pos++ = *i;
572  setup_props(o);
573  }
574 
575  fnode(op o, std::initializer_list<const fnode*> l,
576  bool saturated = false)
577  : fnode(o, l.begin(), l.end(), saturated)
578  {
579  }
580 
581  fnode(op o, const fnode* f, uint8_t min, uint8_t max,
582  bool saturated = false)
583  : op_(o), min_(min), max_(max), saturated_(saturated), size_(1)
584  {
585  children[0] = f;
586  setup_props(o);
587  }
588 
589  static const fnode* ff_;
590  static const fnode* tt_;
591  static const fnode* ew_;
592  static const fnode* one_star_;
593  static const fnode* one_plus_;
594 
595  op op_; // operator
596  uint8_t min_; // range minimum (for star-like operators)
597  uint8_t max_; // range maximum;
598  mutable uint8_t saturated_;
599  uint16_t size_; // number of children
600  mutable uint16_t refs_ = 0; // reference count - 1;
601  size_t id_; // Also used as hash.
602  static size_t next_id_;
603 
604  struct ltl_prop
605  {
606  // All properties here should be expressed in such a a way
607  // that property(f && g) is just property(f)&property(g).
608  // This allows us to compute all properties of a compound
609  // formula in one operation.
610  //
611  // For instance we do not use a property that says "has
612  // temporal operator", because it would require an OR between
613  // the two arguments. Instead we have a property that
614  // says "no temporal operator", and that one is computed
615  // with an AND between the arguments.
616  //
617  // Also choose a name that makes sense when prefixed with
618  // "the formula is".
619  bool boolean:1; // No temporal operators.
620  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
621  bool in_nenoform:1; // Negative Normal Form.
622  bool syntactic_si:1; // LTL-X or siPSL
623  bool sugar_free_ltl:1; // No F and G operators.
624  bool ltl_formula:1; // Only LTL operators.
625  bool psl_formula:1; // Only PSL operators.
626  bool sere_formula:1; // Only SERE operators.
627  bool finite:1; // Finite SERE formulae, or Bool+X forms.
628  bool eventual:1; // Purely eventual formula.
629  bool universal:1; // Purely universal formula.
630  bool syntactic_safety:1; // Syntactic Safety Property.
631  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
632  bool syntactic_obligation:1; // Syntactic Obligation Property.
633  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
634  bool syntactic_persistence:1; // Syntactic Persistence Property.
635  bool not_marked:1; // No occurrence of EConcatMarked.
636  bool accepting_eword:1; // Accepts the empty word.
637  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
638  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
639  };
640  union
641  {
642  // Use an unsigned for fast computation of all properties.
643  unsigned props;
644  ltl_prop is_;
645  };
646 
647  const fnode* children[1];
648  };
649 
651  SPOT_API
652  int atomic_prop_cmp(const fnode* f, const fnode* g);
653 
654  class SPOT_API formula;
655 
657  {
658  bool
659  operator()(const fnode* left, const fnode* right) const
660  {
661  SPOT_ASSERT(left);
662  SPOT_ASSERT(right);
663  if (left == right)
664  return false;
665 
666  // We want Boolean formulae first.
667  bool lib = left->is_boolean();
668  if (lib != right->is_boolean())
669  return lib;
670 
671  // We have two Boolean formulae
672  if (lib)
673  {
674  bool lconst = left->is_constant();
675  if (lconst != right->is_constant())
676  return lconst;
677  if (!lconst)
678  {
679  auto get_literal = [](const fnode* f) -> const fnode*
680  {
681  if (f->is(op::Not))
682  f = f->nth(0);
683  if (f->is(op::ap))
684  return f;
685  return nullptr;
686  };
687  // Literals should come first
688  const fnode* litl = get_literal(left);
689  const fnode* litr = get_literal(right);
690  if (!litl != !litr)
691  return litl;
692  if (litl)
693  {
694  // And they should be sorted alphabetically
695  int cmp = atomic_prop_cmp(litl, litr);
696  if (cmp)
697  return cmp < 0;
698  }
699  }
700  }
701 
702  size_t l = left->id();
703  size_t r = right->id();
704  if (l != r)
705  return l < r;
706  // Because the hash code assigned to each formula is the
707  // number of formulae constructed so far, it is very unlikely
708  // that we will ever reach a case were two different formulae
709  // have the same hash. This will happen only ever with have
710  // produced 256**sizeof(size_t) formulae (i.e. max_count has
711  // looped back to 0 and started over). In that case we can
712  // order two formulas by looking at their text representation.
713  // We could be more efficient and look at their AST, but it's
714  // not worth the burden. (Also ordering pointers is ruled out
715  // because it breaks the determinism of the implementation.)
716  std::ostringstream old;
717  left->dump(old);
718  std::ostringstream ord;
719  right->dump(ord);
720  return old.str() < ord.str();
721  }
722 
723  SPOT_API bool
724  operator()(const formula& left, const formula& right) const;
725 };
726 
727 #endif // SWIG
728 
731  class SPOT_API formula final
732  {
733  friend struct formula_ptr_less_than_bool_first;
734  const fnode* ptr_;
735  public:
740  explicit formula(const fnode* f) noexcept
741  : ptr_(f)
742  {
743  }
744 
750  formula(std::nullptr_t) noexcept
751  : ptr_(nullptr)
752  {
753  }
754 
756  formula() noexcept
757  : ptr_(nullptr)
758  {
759  }
760 
762  formula(const formula& f) noexcept
763  : ptr_(f.ptr_)
764  {
765  if (ptr_)
766  ptr_->clone();
767  }
768 
770  formula(formula&& f) noexcept
771  : ptr_(f.ptr_)
772  {
773  f.ptr_ = nullptr;
774  }
775 
778  {
779  if (ptr_)
780  ptr_->destroy();
781  }
782 
790  const formula& operator=(std::nullptr_t)
791  {
792  this->~formula();
793  ptr_ = nullptr;
794  return *this;
795  }
796 
797  const formula& operator=(const formula& f)
798  {
799  this->~formula();
800  if ((ptr_ = f.ptr_))
801  ptr_->clone();
802  return *this;
803  }
804 
805  const formula& operator=(formula&& f) noexcept
806  {
807  std::swap(f.ptr_, ptr_);
808  return *this;
809  }
810 
811  bool operator<(const formula& other) const noexcept
812  {
813  if (SPOT_UNLIKELY(!other.ptr_))
814  return false;
815  if (SPOT_UNLIKELY(!ptr_))
816  return true;
817  if (id() < other.id())
818  return true;
819  if (id() > other.id())
820  return false;
821  // The case where id()==other.id() but ptr_ != other.ptr_ is
822  // very unlikely (we would need to build more than UINT_MAX
823  // formulas), so let's just compare pointers, and ignore the
824  // fact that it may introduce some nondeterminism.
825  return ptr_ < other.ptr_;
826  }
827 
828  bool operator<=(const formula& other) const noexcept
829  {
830  return *this == other || *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 !(*this < other);
841  }
842 
843  bool operator==(const formula& other) const noexcept
844  {
845  return other.ptr_ == ptr_;
846  }
847 
848  bool operator==(std::nullptr_t) const noexcept
849  {
850  return ptr_ == nullptr;
851  }
852 
853  bool operator!=(const formula& other) const noexcept
854  {
855  return other.ptr_ != ptr_;
856  }
857 
858  bool operator!=(std::nullptr_t) const noexcept
859  {
860  return ptr_ != nullptr;
861  }
862 
863  explicit operator bool() const noexcept
864  {
865  return ptr_ != nullptr;
866  }
867 
869  // Forwarded functions //
871 
873  static constexpr uint8_t unbounded()
874  {
875  return fnode::unbounded();
876  }
877 
879  static formula ap(const std::string& name)
880  {
881  return formula(fnode::ap(name));
882  }
883 
889  static formula ap(const formula& a)
890  {
891  if (SPOT_UNLIKELY(a.kind() != op::ap))
892  report_ap_invalid_arg();
893  return a;
894  }
895 
900  static formula unop(op o, const formula& f)
901  {
902  return formula(fnode::unop(o, f.ptr_->clone()));
903  }
904 
905 #ifndef SWIG
906  static formula unop(op o, formula&& f)
907  {
908  return formula(fnode::unop(o, f.to_node_()));
909  }
910 #endif // !SWIG
912 
913 #ifdef SWIG
914 #define SPOT_DEF_UNOP(Name) \
915  static formula Name(const formula& f) \
916  { \
917  return unop(op::Name, f); \
918  }
919 #else // !SWIG
920 #define SPOT_DEF_UNOP(Name) \
921  static formula Name(const formula& f) \
922  { \
923  return unop(op::Name, f); \
924  } \
925  static formula Name(formula&& f) \
926  { \
927  return unop(op::Name, std::move(f)); \
928  }
929 #endif // !SWIG
932  SPOT_DEF_UNOP(Not);
934 
937  SPOT_DEF_UNOP(X);
939 
943  static formula X(unsigned level, const formula& f)
944  {
945  return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
946  }
947 
948 #if SPOT_WANT_STRONG_X
951  SPOT_DEF_UNOP(strong_X);
953 
957  static formula strong_X(unsigned level, const formula& f)
958  {
959  return nested_unop_range(op::strong_X, op::Or /* unused */,
960  level, level, f);
961  }
962 #endif
963 
966  SPOT_DEF_UNOP(F);
968 
975  static formula F(unsigned min_level, unsigned max_level, const formula& f)
976  {
977  return nested_unop_range(op::X, op::Or, min_level, max_level, f);
978  }
979 
986  static formula G(unsigned min_level, unsigned max_level, const formula& f)
987  {
988  return nested_unop_range(op::X, op::And, min_level, max_level, f);
989  }
990 
993  SPOT_DEF_UNOP(G);
995 
998  SPOT_DEF_UNOP(Closure);
1000 
1003  SPOT_DEF_UNOP(NegClosure);
1005 
1008  SPOT_DEF_UNOP(NegClosureMarked);
1010 
1013  SPOT_DEF_UNOP(first_match);
1015 #undef SPOT_DEF_UNOP
1016 
1022  static formula binop(op o, const formula& f, const formula& g)
1023  {
1024  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
1025  }
1026 
1027 #ifndef SWIG
1028  static formula binop(op o, const formula& f, formula&& g)
1029  {
1030  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
1031  }
1032 
1033  static formula binop(op o, formula&& f, const formula& g)
1034  {
1035  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
1036  }
1037 
1038  static formula binop(op o, formula&& f, formula&& g)
1039  {
1040  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
1041  }
1043 
1044 #endif //SWIG
1045 
1046 #ifdef SWIG
1047 #define SPOT_DEF_BINOP(Name) \
1048  static formula Name(const formula& f, const formula& g) \
1049  { \
1050  return binop(op::Name, f, g); \
1051  }
1052 #else // !SWIG
1053 #define SPOT_DEF_BINOP(Name) \
1054  static formula Name(const formula& f, const formula& g) \
1055  { \
1056  return binop(op::Name, f, g); \
1057  } \
1058  static formula Name(const formula& f, formula&& g) \
1059  { \
1060  return binop(op::Name, f, std::move(g)); \
1061  } \
1062  static formula Name(formula&& f, const formula& g) \
1063  { \
1064  return binop(op::Name, std::move(f), g); \
1065  } \
1066  static formula Name(formula&& f, formula&& g) \
1067  { \
1068  return binop(op::Name, std::move(f), std::move(g)); \
1069  }
1070 #endif // !SWIG
1073  SPOT_DEF_BINOP(Xor);
1075 
1078  SPOT_DEF_BINOP(Implies);
1080 
1083  SPOT_DEF_BINOP(Equiv);
1085 
1088  SPOT_DEF_BINOP(U);
1090 
1093  SPOT_DEF_BINOP(R);
1095 
1098  SPOT_DEF_BINOP(W);
1100 
1103  SPOT_DEF_BINOP(M);
1105 
1108  SPOT_DEF_BINOP(EConcat);
1110 
1113  SPOT_DEF_BINOP(EConcatMarked);
1115 
1118  SPOT_DEF_BINOP(UConcat);
1120 #undef SPOT_DEF_BINOP
1121 
1127  static formula multop(op o, const std::vector<formula>& l)
1128  {
1129  std::vector<const fnode*> tmp;
1130  tmp.reserve(l.size());
1131  for (auto f: l)
1132  if (f.ptr_)
1133  tmp.emplace_back(f.ptr_->clone());
1134  return formula(fnode::multop(o, std::move(tmp)));
1135  }
1136 
1137 #ifndef SWIG
1138  static formula multop(op o, std::vector<formula>&& l)
1139  {
1140  std::vector<const fnode*> tmp;
1141  tmp.reserve(l.size());
1142  for (auto f: l)
1143  if (f.ptr_)
1144  tmp.emplace_back(f.to_node_());
1145  return formula(fnode::multop(o, std::move(tmp)));
1146  }
1147 #endif // !SWIG
1149 
1150 #ifdef SWIG
1151 #define SPOT_DEF_MULTOP(Name) \
1152  static formula Name(const std::vector<formula>& l) \
1153  { \
1154  return multop(op::Name, l); \
1155  }
1156 #else // !SWIG
1157 #define SPOT_DEF_MULTOP(Name) \
1158  static formula Name(const std::vector<formula>& l) \
1159  { \
1160  return multop(op::Name, l); \
1161  } \
1162  \
1163  static formula Name(std::vector<formula>&& l) \
1164  { \
1165  return multop(op::Name, std::move(l)); \
1166  }
1167 #endif // !SWIG
1170  SPOT_DEF_MULTOP(Or);
1172 
1175  SPOT_DEF_MULTOP(OrRat);
1177 
1180  SPOT_DEF_MULTOP(And);
1182 
1185  SPOT_DEF_MULTOP(AndRat);
1187 
1190  SPOT_DEF_MULTOP(AndNLM);
1192 
1195  SPOT_DEF_MULTOP(Concat);
1197 
1200  SPOT_DEF_MULTOP(Fusion);
1202 #undef SPOT_DEF_MULTOP
1203 
1208  static formula bunop(op o, const formula& f,
1209  unsigned min = 0U,
1210  unsigned max = unbounded())
1211  {
1212  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1213  }
1214 
1215 #ifndef SWIG
1216  static formula bunop(op o, formula&& f,
1217  unsigned min = 0U,
1218  unsigned max = unbounded())
1219  {
1220  return formula(fnode::bunop(o, f.to_node_(), min, max));
1221  }
1222 #endif // !SWIG
1224 
1225 #if SWIG
1226 #define SPOT_DEF_BUNOP(Name) \
1227  static formula Name(const formula& f, \
1228  unsigned min = 0U, \
1229  unsigned max = unbounded()) \
1230  { \
1231  return bunop(op::Name, f, min, max); \
1232  }
1233 #else // !SWIG
1234 #define SPOT_DEF_BUNOP(Name) \
1235  static formula Name(const formula& f, \
1236  unsigned min = 0U, \
1237  unsigned max = unbounded()) \
1238  { \
1239  return bunop(op::Name, f, min, max); \
1240  } \
1241  static formula Name(formula&& f, \
1242  unsigned min = 0U, \
1243  unsigned max = unbounded()) \
1244  { \
1245  return bunop(op::Name, std::move(f), min, max); \
1246  }
1247 #endif
1250  SPOT_DEF_BUNOP(Star);
1252 
1258  SPOT_DEF_BUNOP(FStar);
1260 #undef SPOT_DEF_BUNOP
1261 
1273  static const formula nested_unop_range(op uo, op bo, unsigned min,
1274  unsigned max, formula f)
1275  {
1276  return formula(fnode::nested_unop_range(uo, bo, min, max,
1277  f.ptr_->clone()));
1278  }
1279 
1285  static formula sugar_goto(const formula& b, unsigned min, unsigned max);
1286 
1292  static formula sugar_equal(const formula& b, unsigned min, unsigned max);
1293 
1315  static formula sugar_delay(const formula& a, const formula& b,
1316  unsigned min, unsigned max);
1317  static formula sugar_delay(const formula& b,
1318  unsigned min, unsigned max);
1320 
1321 #ifndef SWIG
1331  const fnode* to_node_()
1332  {
1333  auto tmp = ptr_;
1334  ptr_ = nullptr;
1335  return tmp;
1336  }
1337 #endif
1338 
1340  op kind() const
1341  {
1342  return ptr_->kind();
1343  }
1344 
1346  std::string kindstr() const
1347  {
1348  return ptr_->kindstr();
1349  }
1350 
1352  bool is(op o) const
1353  {
1354  return ptr_->is(o);
1355  }
1356 
1357 #ifndef SWIG
1359  bool is(op o1, op o2) const
1360  {
1361  return ptr_->is(o1, o2);
1362  }
1363 
1365  bool is(op o1, op o2, op o3) const
1366  {
1367  return ptr_->is(o1, o2, o3);
1368  }
1369 
1372  bool is(op o1, op o2, op o3, op o4) const
1373  {
1374  return ptr_->is(o1, o2, o3, o4);
1375  }
1376 
1378  bool is(std::initializer_list<op> l) const
1379  {
1380  return ptr_->is(l);
1381  }
1382 #endif
1383 
1388  {
1389  auto f = ptr_->get_child_of(o);
1390  if (f)
1391  f->clone();
1392  return formula(f);
1393  }
1394 
1395 #ifndef SWIG
1402  formula get_child_of(std::initializer_list<op> l) const
1403  {
1404  auto f = ptr_->get_child_of(l);
1405  if (f)
1406  f->clone();
1407  return formula(f);
1408  }
1409 #endif
1410 
1414  unsigned min() const
1415  {
1416  return ptr_->min();
1417  }
1418 
1422  unsigned max() const
1423  {
1424  return ptr_->max();
1425  }
1426 
1428  unsigned size() const
1429  {
1430  return ptr_->size();
1431  }
1432 
1437  bool is_leaf() const
1438  {
1439  return ptr_->is_leaf();
1440  }
1441 
1450  size_t id() const
1451  {
1452  return ptr_->id();
1453  }
1454 
1455 #ifndef SWIG
1457  class SPOT_API formula_child_iterator final
1458  {
1459  const fnode*const* ptr_;
1460  public:
1462  : ptr_(nullptr)
1463  {
1464  }
1465 
1466  formula_child_iterator(const fnode*const* f)
1467  : ptr_(f)
1468  {
1469  }
1470 
1471  bool operator==(formula_child_iterator o)
1472  {
1473  return ptr_ == o.ptr_;
1474  }
1475 
1476  bool operator!=(formula_child_iterator o)
1477  {
1478  return ptr_ != o.ptr_;
1479  }
1480 
1481  formula operator*()
1482  {
1483  return formula((*ptr_)->clone());
1484  }
1485 
1486  formula_child_iterator operator++()
1487  {
1488  ++ptr_;
1489  return *this;
1490  }
1491 
1492  formula_child_iterator operator++(int)
1493  {
1494  auto tmp = *this;
1495  ++ptr_;
1496  return tmp;
1497  }
1498  };
1499 
1502  {
1503  return ptr_->begin();
1504  }
1505 
1508  {
1509  return ptr_->end();
1510  }
1511 
1513  formula operator[](unsigned i) const
1514  {
1515  return formula(ptr_->nth(i)->clone());
1516  }
1517 #endif
1518 
1520  static formula ff()
1521  {
1522  return formula(fnode::ff());
1523  }
1524 
1526  bool is_ff() const
1527  {
1528  return ptr_->is_ff();
1529  }
1530 
1532  static formula tt()
1533  {
1534  return formula(fnode::tt());
1535  }
1536 
1538  bool is_tt() const
1539  {
1540  return ptr_->is_tt();
1541  }
1542 
1544  static formula eword()
1545  {
1546  return formula(fnode::eword());
1547  }
1548 
1550  bool is_eword() const
1551  {
1552  return ptr_->is_eword();
1553  }
1554 
1556  bool is_constant() const
1557  {
1558  return ptr_->is_constant();
1559  }
1560 
1565  bool is_Kleene_star() const
1566  {
1567  return ptr_->is_Kleene_star();
1568  }
1569 
1572  {
1573  // no need to clone, 1[*] is not reference counted
1574  return formula(fnode::one_star());
1575  }
1576 
1579  {
1580  // no need to clone, 1[+] is not reference counted
1581  return formula(fnode::one_plus());
1582  }
1583 
1586  bool is_literal() const
1587  {
1588  return (is(op::ap) ||
1589  // If f is in nenoform, Not can only occur in front of
1590  // an atomic proposition. So this way we do not have
1591  // to check the type of the child.
1592  (is(op::Not) && is_boolean() && is_in_nenoform()));
1593  }
1594 
1598  const std::string& ap_name() const
1599  {
1600  return ptr_->ap_name();
1601  }
1602 
1607  std::ostream& dump(std::ostream& os) const
1608  {
1609  return ptr_->dump(os);
1610  }
1611 
1617  formula all_but(unsigned i) const
1618  {
1619  return formula(ptr_->all_but(i));
1620  }
1621 
1631  unsigned boolean_count() const
1632  {
1633  return ptr_->boolean_count();
1634  }
1635 
1649  formula boolean_operands(unsigned* width = nullptr) const
1650  {
1651  return formula(ptr_->boolean_operands(width));
1652  }
1653 
1654 #define SPOT_DEF_PROP(Name) \
1655  bool Name() const \
1656  { \
1657  return ptr_->Name(); \
1658  }
1660  // Properties //
1662 
1664  SPOT_DEF_PROP(is_boolean);
1666  SPOT_DEF_PROP(is_sugar_free_boolean);
1671  SPOT_DEF_PROP(is_in_nenoform);
1673  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1675  SPOT_DEF_PROP(is_sugar_free_ltl);
1677  SPOT_DEF_PROP(is_ltl_formula);
1679  SPOT_DEF_PROP(is_psl_formula);
1681  SPOT_DEF_PROP(is_sere_formula);
1684  SPOT_DEF_PROP(is_finite);
1692  SPOT_DEF_PROP(is_eventual);
1700  SPOT_DEF_PROP(is_universal);
1702  SPOT_DEF_PROP(is_syntactic_safety);
1704  SPOT_DEF_PROP(is_syntactic_guarantee);
1706  SPOT_DEF_PROP(is_syntactic_obligation);
1708  SPOT_DEF_PROP(is_syntactic_recurrence);
1710  SPOT_DEF_PROP(is_syntactic_persistence);
1713  SPOT_DEF_PROP(is_marked);
1715  SPOT_DEF_PROP(accepts_eword);
1721  SPOT_DEF_PROP(has_lbt_atomic_props);
1730  SPOT_DEF_PROP(has_spin_atomic_props);
1731 #undef SPOT_DEF_PROP
1732 
1736  template<typename Trans, typename... Args>
1737  formula map(Trans trans, Args&&... args)
1738  {
1739  switch (op o = kind())
1740  {
1741  case op::ff:
1742  case op::tt:
1743  case op::eword:
1744  case op::ap:
1745  return *this;
1746  case op::Not:
1747  case op::X:
1748 #if SPOT_HAS_STRONG_X
1749  case op::strong_X:
1750 #endif
1751  case op::F:
1752  case op::G:
1753  case op::Closure:
1754  case op::NegClosure:
1755  case op::NegClosureMarked:
1756  case op::first_match:
1757  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1758  case op::Xor:
1759  case op::Implies:
1760  case op::Equiv:
1761  case op::U:
1762  case op::R:
1763  case op::W:
1764  case op::M:
1765  case op::EConcat:
1766  case op::EConcatMarked:
1767  case op::UConcat:
1768  {
1769  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1770  return binop(o, tmp,
1771  trans((*this)[1], std::forward<Args>(args)...));
1772  }
1773  case op::Or:
1774  case op::OrRat:
1775  case op::And:
1776  case op::AndRat:
1777  case op::AndNLM:
1778  case op::Concat:
1779  case op::Fusion:
1780  {
1781  std::vector<formula> tmp;
1782  tmp.reserve(size());
1783  for (auto f: *this)
1784  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1785  return multop(o, std::move(tmp));
1786  }
1787  case op::Star:
1788  case op::FStar:
1789  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1790  min(), max());
1791  }
1792  SPOT_UNREACHABLE();
1793  }
1794 
1803  template<typename Func, typename... Args>
1804  void traverse(Func func, Args&&... args)
1805  {
1806  if (func(*this, std::forward<Args>(args)...))
1807  return;
1808  for (auto f: *this)
1809  f.traverse(func, std::forward<Args>(args)...);
1810  }
1811 
1812  private:
1813 #ifndef SWIG
1814  [[noreturn]] static void report_ap_invalid_arg();
1815 #endif
1816  };
1817 
1819  SPOT_API
1820  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1821  bool abbreviated = false);
1822 
1824  SPOT_API
1825  std::list<std::string> list_formula_props(const formula& f);
1826 
1828  SPOT_API
1829  std::ostream& operator<<(std::ostream& os, const formula& f);
1830 }
1831 
1832 #ifndef SWIG
1833 namespace std
1834 {
1835  template <>
1836  struct hash<spot::formula>
1837  {
1838  size_t operator()(const spot::formula& x) const noexcept
1839  {
1840  return x.id();
1841  }
1842  };
1843 }
1844 #endif
Actual storage for formula nodes.
Definition: formula.hh:127
const fnode *const * begin() const
Definition: formula.hh:280
const fnode *const * end() const
Definition: formula.hh:286
std::string kindstr() const
std::ostream & dump(std::ostream &os) const
bool is_boolean() const
Definition: formula.hh:406
size_t id() const
Definition: formula.hh:274
bool is_ff() const
Definition: formula.hh:308
bool is_sugar_free_boolean() const
Definition: formula.hh:412
bool is_Kleene_star() const
Definition: formula.hh:344
unsigned min() const
Definition: formula.hh:246
bool is_syntactic_safety() const
Definition: formula.hh:472
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:424
unsigned size() const
Definition: formula.hh:262
static constexpr uint8_t unbounded()
Definition: formula.hh:157
static const fnode * eword()
Definition: formula.hh:326
const fnode * get_child_of(op o) const
Definition: formula.hh:223
unsigned max() const
Definition: formula.hh:254
static const fnode * ff()
Definition: formula.hh:302
const fnode * boolean_operands(unsigned *width=nullptr) const
bool accepts_eword() const
Definition: formula.hh:508
bool is_eventual() const
Definition: formula.hh:460
const std::string & ap_name() const
bool is(op o1, op o2, op o3, op o4) const
Definition: formula.hh:204
static bool instances_check()
safety check for the reference counters
bool is_leaf() const
Definition: formula.hh:268
bool has_spin_atomic_props() const
Definition: formula.hh:520
bool is_eword() const
Definition: formula.hh:332
static const fnode * tt()
Definition: formula.hh:314
bool is(op o1, op o2, op o3) const
Definition: formula.hh:199
op kind() const
Definition: formula.hh:179
bool has_lbt_atomic_props() const
Definition: formula.hh:514
bool is_sugar_free_ltl() const
Definition: formula.hh:430
bool is_syntactic_persistence() const
Definition: formula.hh:496
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
unsigned boolean_count() const
Definition: formula.hh:377
bool is_universal() const
Definition: formula.hh:466
bool is_tt() const
Definition: formula.hh:320
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:233
static const fnode * one_plus()
Definition: formula.hh:360
const fnode * nth(unsigned i) const
Definition: formula.hh:292
bool is_constant() const
Definition: formula.hh:338
static const fnode * binop(op o, const fnode *f, const fnode *g)
static const fnode * one_star()
Definition: formula.hh:352
const fnode * all_but(unsigned i) const
bool is_syntactic_recurrence() const
Definition: formula.hh:490
bool is(std::initializer_list< op > l) const
Definition: formula.hh:209
bool is_syntactic_obligation() const
Definition: formula.hh:484
static const fnode * unop(op o, const fnode *f)
bool is_ltl_formula() const
Definition: formula.hh:436
bool is_finite() const
Definition: formula.hh:454
bool is_psl_formula() const
Definition: formula.hh:442
static const fnode * multop(op o, std::vector< const fnode * > l)
bool is_marked() const
Definition: formula.hh:502
void destroy() const
Dereference an fnode.
Definition: formula.hh:147
static const fnode * bunop(op o, const fnode *f, unsigned min, unsigned max=unbounded())
bool is(op o1, op o2) const
Definition: formula.hh:194
bool is_in_nenoform() const
Definition: formula.hh:418
static const fnode * ap(const std::string &name)
bool is_syntactic_guarantee() const
Definition: formula.hh:478
bool is_sere_formula() const
Definition: formula.hh:448
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:133
bool is(op o) const
Definition: formula.hh:189
Allow iterating over children.
Definition: formula.hh:1458
Main class for temporal logic formula.
Definition: formula.hh:732
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1631
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1437
size_t id() const
Return the id of a formula.
Definition: formula.hh:1450
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:1216
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1737
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:1208
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition: formula.hh:986
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1022
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1352
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1138
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:770
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:740
bool is(op o1, op o2) const
Return true if the formula is of kind o1 or o2.
Definition: formula.hh:1359
static formula one_plus()
Return a copy of the formula 1[+].
Definition: formula.hh:1578
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:1571
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1414
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:873
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:906
static formula eword()
Return the empty word constant.
Definition: formula.hh:1544
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1617
static formula ff()
Return the false constant.
Definition: formula.hh:1520
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1028
op kind() const
Return top-most operator.
Definition: formula.hh:1340
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1127
unsigned size() const
Return the number of children.
Definition: formula.hh:1428
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:1538
bool is(op o1, op o2, op o3, op o4) const
Definition: formula.hh:1372
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1346
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:762
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1507
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1038
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:889
formula get_child_of(std::initializer_list< op > l) const
Remove all operators in l and return the child.
Definition: formula.hh:1402
bool is_eword() const
Whether the formula is the empty word constant.
Definition: formula.hh:1550
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:1804
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition: formula.hh:975
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:750
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:879
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1598
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:1365
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:790
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1422
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition: formula.hh:943
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1526
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1501
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition: formula.hh:1556
~formula()
Destroy a formula.
Definition: formula.hh:777
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1607
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1387
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1331
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition: formula.hh:1378
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1513
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1565
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1033
bool is_literal() const
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1586
static formula tt()
Return the true constant.
Definition: formula.hh:1532
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:756
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:900
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1649
static const formula nested_unop_range(op uo, op bo, unsigned min, unsigned max, formula f)
Nested operator construction (syntactic sugar).
Definition: formula.hh:1273
op
Operator types.
Definition: formula.hh:78
@ 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:26
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:657

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