spot  2.4
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
3 // 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 
43 #include <spot/misc/common.hh>
44 #include <memory>
45 #include <cstdint>
46 #include <initializer_list>
47 #include <cassert>
48 #include <vector>
49 #include <string>
50 #include <iterator>
51 #include <iosfwd>
52 #include <sstream>
53 #include <list>
54 #include <cstddef>
55 #include <initializer_list>
56 #include <limits>
57 
58 namespace spot
59 {
62  enum class op: uint8_t
63  {
64  ff,
65  tt,
66  eword,
67  ap,
68  // unary operators
69  Not,
70  X,
71  F,
72  G,
73  Closure,
74  NegClosure,
76  // binary operators
77  Xor,
78  Implies,
79  Equiv,
80  U,
81  R,
82  W,
83  M,
84  EConcat,
86  UConcat,
87  // n-ary operators
88  Or,
89  OrRat,
90  And,
91  AndRat,
92  AndNLM,
93  Concat,
94  Fusion,
95  // star-like operators
96  Star,
97  FStar,
98  };
99 
100 #ifndef SWIG
101  class SPOT_API fnode final
108  {
109  public:
114  const fnode* clone() const
115  {
116  // Saturate.
117  ++refs_;
118  if (SPOT_UNLIKELY(!refs_))
119  saturated_ = 1;
120  return this;
121  }
122 
128  void destroy() const
129  {
130  if (SPOT_LIKELY(refs_))
131  --refs_;
132  else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
133  // last reference to a node that is not a constant
134  destroy_aux();
135  }
136 
138  static constexpr uint8_t unbounded()
139  {
140  return UINT8_MAX;
141  }
142 
144  static const fnode* ap(const std::string& name);
146  static const fnode* unop(op o, const fnode* f);
148  static const fnode* binop(op o, const fnode* f, const fnode* g);
150  static const fnode* multop(op o, std::vector<const fnode*> l);
152  static const fnode* bunop(op o, const fnode* f,
153  uint8_t min, uint8_t max = unbounded());
154 
156  op kind() const
157  {
158  return op_;
159  }
160 
162  std::string kindstr() const;
163 
165  bool is(op o) const
166  {
167  return op_ == o;
168  }
169 
171  bool is(op o1, op o2) const
172  {
173  return op_ == o1 || op_ == o2;
174  }
175 
177  bool is(std::initializer_list<op> l) const
178  {
179  const fnode* n = this;
180  for (auto o: l)
181  {
182  if (!n->is(o))
183  return false;
184  n = n->nth(0);
185  }
186  return true;
187  }
188 
190  const fnode* get_child_of(op o) const
191  {
192  if (op_ != o)
193  return nullptr;
194  if (SPOT_UNLIKELY(size_ != 1))
195  report_get_child_of_expecting_single_child_node();
196  return nth(0);
197  }
198 
200  const fnode* get_child_of(std::initializer_list<op> l) const
201  {
202  auto c = this;
203  for (auto o: l)
204  {
205  c = c->get_child_of(o);
206  if (c == nullptr)
207  return c;
208  }
209  return c;
210  }
211 
213  unsigned min() const
214  {
215  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
216  report_min_invalid_arg();
217  return min_;
218  }
219 
221  unsigned max() const
222  {
223  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
224  report_max_invalid_arg();
225  return max_;
226  }
227 
229  unsigned size() const
230  {
231  return size_;
232  }
233 
235  size_t id() const
236  {
237  return id_;
238  }
239 
241  const fnode*const* begin() const
242  {
243  return children;
244  }
245 
247  const fnode*const* end() const
248  {
249  return children + size();
250  }
251 
253  const fnode* nth(unsigned i) const
254  {
255  if (SPOT_UNLIKELY(i >= size()))
256  report_non_existing_child();
257  return children[i];
258  }
259 
261  static const fnode* ff()
262  {
263  return ff_;
264  }
265 
267  bool is_ff() const
268  {
269  return op_ == op::ff;
270  }
271 
273  static const fnode* tt()
274  {
275  return tt_;
276  }
277 
279  bool is_tt() const
280  {
281  return op_ == op::tt;
282  }
283 
285  static const fnode* eword()
286  {
287  return ew_;
288  }
289 
291  bool is_eword() const
292  {
293  return op_ == op::eword;
294  }
295 
297  bool is_constant() const
298  {
299  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
300  }
301 
303  bool is_Kleene_star() const
304  {
305  if (op_ != op::Star)
306  return false;
307  return min_ == 0 && max_ == unbounded();
308  }
309 
311  static const fnode* one_star()
312  {
313  if (!one_star_)
314  one_star_ = bunop(op::Star, tt(), 0);
315  return one_star_;
316  }
317 
319  const std::string& ap_name() const;
320 
322  std::ostream& dump(std::ostream& os) const;
323 
325  const fnode* all_but(unsigned i) const;
326 
328  unsigned boolean_count() const
329  {
330  unsigned pos = 0;
331  unsigned s = size();
332  while (pos < s && children[pos]->is_boolean())
333  ++pos;
334  return pos;
335  }
336 
338  const fnode* boolean_operands(unsigned* width = nullptr) const;
339 
350  static bool instances_check();
351 
353  // Properties //
355 
357  bool is_boolean() const
358  {
359  return is_.boolean;
360  }
361 
364  {
365  return is_.sugar_free_boolean;
366  }
367 
369  bool is_in_nenoform() const
370  {
371  return is_.in_nenoform;
372  }
373 
376  {
377  return is_.syntactic_si;
378  }
379 
381  bool is_sugar_free_ltl() const
382  {
383  return is_.sugar_free_ltl;
384  }
385 
387  bool is_ltl_formula() const
388  {
389  return is_.ltl_formula;
390  }
391 
393  bool is_psl_formula() const
394  {
395  return is_.psl_formula;
396  }
397 
399  bool is_sere_formula() const
400  {
401  return is_.sere_formula;
402  }
403 
405  bool is_finite() const
406  {
407  return is_.finite;
408  }
409 
411  bool is_eventual() const
412  {
413  return is_.eventual;
414  }
415 
417  bool is_universal() const
418  {
419  return is_.universal;
420  }
421 
423  bool is_syntactic_safety() const
424  {
425  return is_.syntactic_safety;
426  }
427 
430  {
431  return is_.syntactic_guarantee;
432  }
433 
436  {
437  return is_.syntactic_obligation;
438  }
439 
442  {
443  return is_.syntactic_recurrence;
444  }
445 
448  {
449  return is_.syntactic_persistence;
450  }
451 
453  bool is_marked() const
454  {
455  return !is_.not_marked;
456  }
457 
459  bool accepts_eword() const
460  {
461  return is_.accepting_eword;
462  }
463 
465  bool has_lbt_atomic_props() const
466  {
467  return is_.lbt_atomic_props;
468  }
469 
472  {
473  return is_.spin_atomic_props;
474  }
475 
476  private:
477  void setup_props(op o);
478  void destroy_aux() const;
479 
480  [[noreturn]] static void report_non_existing_child();
481  [[noreturn]] static void report_too_many_children();
482  [[noreturn]] static void
483  report_get_child_of_expecting_single_child_node();
484  [[noreturn]] static void report_min_invalid_arg();
485  [[noreturn]] static void report_max_invalid_arg();
486 
487  static const fnode* unique(const fnode*);
488 
489  // Destruction may only happen via destroy().
490  ~fnode() = default;
491  // Disallow copies.
492  fnode(const fnode&) = delete;
493  fnode& operator=(const fnode&) = delete;
494 
495 
496 
497  template<class iter>
498  fnode(op o, iter begin, iter end)
499  // Clang has some optimization where is it able to combine the
500  // 4 movb initializing op_,min_,max_,saturated_ into a single
501  // movl. Also it can optimize the three byte-comparisons of
502  // is_Kleene_star() into a single masked 32-bit comparison.
503  // The latter optimization triggers warnings from valgrind if
504  // min_ and max_ are not initialized. So to benefit from the
505  // initialization optimization and the is_Kleene_star()
506  // optimization in Clang, we always initialize min_ and max_
507  // with this compiler. Do not do it the rest of the time,
508  // since the optimization is not done.
509  : op_(o),
510 #if __llvm__
511  min_(0), max_(0),
512 #endif
513  saturated_(0)
514  {
515  size_t s = std::distance(begin, end);
516  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
517  report_too_many_children();
518  size_ = s;
519  auto pos = children;
520  for (auto i = begin; i != end; ++i)
521  *pos++ = *i;
522  setup_props(o);
523  }
524 
525  fnode(op o, std::initializer_list<const fnode*> l)
526  : fnode(o, l.begin(), l.end())
527  {
528  }
529 
530  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
531  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
532  {
533  children[0] = f;
534  setup_props(o);
535  }
536 
537  static const fnode* ff_;
538  static const fnode* tt_;
539  static const fnode* ew_;
540  static const fnode* one_star_;
541 
542  op op_; // operator
543  uint8_t min_; // range minimum (for star-like operators)
544  uint8_t max_; // range maximum;
545  mutable uint8_t saturated_;
546  uint16_t size_; // number of children
547  mutable uint16_t refs_ = 0; // reference count - 1;
548  size_t id_; // Also used as hash.
549  static size_t next_id_;
550 
551  struct ltl_prop
552  {
553  // All properties here should be expressed in such a a way
554  // that property(f && g) is just property(f)&property(g).
555  // This allows us to compute all properties of a compound
556  // formula in one operation.
557  //
558  // For instance we do not use a property that says "has
559  // temporal operator", because it would require an OR between
560  // the two arguments. Instead we have a property that
561  // says "no temporal operator", and that one is computed
562  // with an AND between the arguments.
563  //
564  // Also choose a name that makes sense when prefixed with
565  // "the formula is".
566  bool boolean:1; // No temporal operators.
567  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
568  bool in_nenoform:1; // Negative Normal Form.
569  bool syntactic_si:1; // LTL-X or siPSL
570  bool sugar_free_ltl:1; // No F and G operators.
571  bool ltl_formula:1; // Only LTL operators.
572  bool psl_formula:1; // Only PSL operators.
573  bool sere_formula:1; // Only SERE operators.
574  bool finite:1; // Finite SERE formulae, or Bool+X forms.
575  bool eventual:1; // Purely eventual formula.
576  bool universal:1; // Purely universal formula.
577  bool syntactic_safety:1; // Syntactic Safety Property.
578  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
579  bool syntactic_obligation:1; // Syntactic Obligation Property.
580  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
581  bool syntactic_persistence:1; // Syntactic Persistence Property.
582  bool not_marked:1; // No occurrence of EConcatMarked.
583  bool accepting_eword:1; // Accepts the empty word.
584  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
585  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
586  };
587  union
588  {
589  // Use an unsigned for fast computation of all properties.
590  unsigned props;
591  ltl_prop is_;
592  };
593 
594  const fnode* children[1];
595  };
596 
598  SPOT_API
599  int atomic_prop_cmp(const fnode* f, const fnode* g);
600 
602  {
603  bool
604  operator()(const fnode* left, const fnode* right) const
605  {
606  SPOT_ASSERT(left);
607  SPOT_ASSERT(right);
608  if (left == right)
609  return false;
610 
611  // We want Boolean formulae first.
612  bool lib = left->is_boolean();
613  if (lib != right->is_boolean())
614  return lib;
615 
616  // We have two Boolean formulae
617  if (lib)
618  {
619  bool lconst = left->is_constant();
620  if (lconst != right->is_constant())
621  return lconst;
622  if (!lconst)
623  {
624  auto get_literal = [](const fnode* f) -> const fnode*
625  {
626  if (f->is(op::Not))
627  f = f->nth(0);
628  if (f->is(op::ap))
629  return f;
630  return nullptr;
631  };
632  // Literals should come first
633  const fnode* litl = get_literal(left);
634  const fnode* litr = get_literal(right);
635  if (!litl != !litr)
636  return litl;
637  if (litl)
638  {
639  // And they should be sorted alphabetically
640  int cmp = atomic_prop_cmp(litl, litr);
641  if (cmp)
642  return cmp < 0;
643  }
644  }
645  }
646 
647  size_t l = left->id();
648  size_t r = right->id();
649  if (l != r)
650  return l < r;
651  // Because the hash code assigned to each formula is the
652  // number of formulae constructed so far, it is very unlikely
653  // that we will ever reach a case were two different formulae
654  // have the same hash. This will happen only ever with have
655  // produced 256**sizeof(size_t) formulae (i.e. max_count has
656  // looped back to 0 and started over). In that case we can
657  // order two formulas by looking at their text representation.
658  // We could be more efficient and look at their AST, but it's
659  // not worth the burden. (Also ordering pointers is ruled out
660  // because it breaks the determinism of the implementation.)
661  std::ostringstream old;
662  left->dump(old);
663  std::ostringstream ord;
664  right->dump(ord);
665  return old.str() < ord.str();
666  }
667  };
668 
669 #endif // SWIG
670 
673  class SPOT_API formula final
674  {
675  const fnode* ptr_;
676  public:
681  explicit formula(const fnode* f) noexcept
682  : ptr_(f)
683  {
684  }
685 
691  formula(std::nullptr_t) noexcept
692  : ptr_(nullptr)
693  {
694  }
695 
697  formula() noexcept
698  : ptr_(nullptr)
699  {
700  }
701 
703  formula(const formula& f) noexcept
704  : ptr_(f.ptr_)
705  {
706  if (ptr_)
707  ptr_->clone();
708  }
709 
711  formula(formula&& f) noexcept
712  : ptr_(f.ptr_)
713  {
714  f.ptr_ = nullptr;
715  }
716 
719  {
720  if (ptr_)
721  ptr_->destroy();
722  }
723 
731  const formula& operator=(std::nullptr_t)
732  {
733  this->~formula();
734  ptr_ = nullptr;
735  return *this;
736  }
737 
738  const formula& operator=(const formula& f)
739  {
740  this->~formula();
741  if ((ptr_ = f.ptr_))
742  ptr_->clone();
743  return *this;
744  }
745 
746  const formula& operator=(formula&& f) noexcept
747  {
748  std::swap(f.ptr_, ptr_);
749  return *this;
750  }
751 
752  bool operator<(const formula& other) const noexcept
753  {
754  if (SPOT_UNLIKELY(!other.ptr_))
755  return false;
756  if (SPOT_UNLIKELY(!ptr_))
757  return true;
758  if (id() < other.id())
759  return true;
760  if (id() > other.id())
761  return false;
762  // The case where id()==other.id() but ptr_ != other.ptr_ is
763  // very unlikely (we would need to build more that UINT_MAX
764  // formulas), so let's just compare pointer, and ignore the fact
765  // that it may give some nondeterminism.
766  return ptr_ < other.ptr_;
767  }
768 
769  bool operator<=(const formula& other) const noexcept
770  {
771  return *this == other || *this < other;
772  }
773 
774  bool operator>(const formula& other) const noexcept
775  {
776  return !(*this <= other);
777  }
778 
779  bool operator>=(const formula& other) const noexcept
780  {
781  return !(*this < other);
782  }
783 
784  bool operator==(const formula& other) const noexcept
785  {
786  return other.ptr_ == ptr_;
787  }
788 
789  bool operator==(std::nullptr_t) const noexcept
790  {
791  return ptr_ == nullptr;
792  }
793 
794  bool operator!=(const formula& other) const noexcept
795  {
796  return other.ptr_ != ptr_;
797  }
798 
799  bool operator!=(std::nullptr_t) const noexcept
800  {
801  return ptr_ != nullptr;
802  }
803 
804  operator bool() const
805  {
806  return ptr_ != nullptr;
807  }
808 
810  // Forwarded functions //
812 
814  static constexpr uint8_t unbounded()
815  {
816  return fnode::unbounded();
817  }
818 
820  static formula ap(const std::string& name)
821  {
822  return formula(fnode::ap(name));
823  }
824 
830  static formula ap(const formula& a)
831  {
832  if (SPOT_UNLIKELY(a.kind() != op::ap))
833  report_ap_invalid_arg();
834  return a;
835  }
836 
841  static formula unop(op o, const formula& f)
842  {
843  return formula(fnode::unop(o, f.ptr_->clone()));
844  }
845 
846 #ifndef SWIG
847  static formula unop(op o, formula&& f)
848  {
849  return formula(fnode::unop(o, f.to_node_()));
850  }
851 #endif // !SWIG
852 
854 #ifdef SWIG
855 #define SPOT_DEF_UNOP(Name) \
856  static formula Name(const formula& f) \
857  { \
858  return unop(op::Name, f); \
859  }
860 #else // !SWIG
861 #define SPOT_DEF_UNOP(Name) \
862  static formula Name(const formula& f) \
863  { \
864  return unop(op::Name, f); \
865  } \
866  static formula Name(formula&& f) \
867  { \
868  return unop(op::Name, std::move(f)); \
869  }
870 #endif // !SWIG
871  SPOT_DEF_UNOP(Not);
875 
878  SPOT_DEF_UNOP(X);
880 
883  SPOT_DEF_UNOP(F);
885 
888  SPOT_DEF_UNOP(G);
890 
893  SPOT_DEF_UNOP(Closure);
895 
898  SPOT_DEF_UNOP(NegClosure);
900 
903  SPOT_DEF_UNOP(NegClosureMarked);
905 #undef SPOT_DEF_UNOP
906 
912  static formula binop(op o, const formula& f, const formula& g)
913  {
914  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
915  }
916 
917 #ifndef SWIG
918  static formula binop(op o, const formula& f, formula&& g)
919  {
920  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
921  }
922 
923  static formula binop(op o, formula&& f, const formula& g)
924  {
925  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
926  }
927 
928  static formula binop(op o, formula&& f, formula&& g)
929  {
930  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
931  }
933 
934 #endif //SWIG
935 
936 #ifdef SWIG
937 #define SPOT_DEF_BINOP(Name) \
938  static formula Name(const formula& f, const formula& g) \
939  { \
940  return binop(op::Name, f, g); \
941  }
942 #else // !SWIG
943 #define SPOT_DEF_BINOP(Name) \
944  static formula Name(const formula& f, const formula& g) \
945  { \
946  return binop(op::Name, f, g); \
947  } \
948  static formula Name(const formula& f, formula&& g) \
949  { \
950  return binop(op::Name, f, std::move(g)); \
951  } \
952  static formula Name(formula&& f, const formula& g) \
953  { \
954  return binop(op::Name, std::move(f), g); \
955  } \
956  static formula Name(formula&& f, formula&& g) \
957  { \
958  return binop(op::Name, std::move(f), std::move(g)); \
959  }
960 #endif // !SWIG
961  SPOT_DEF_BINOP(Xor);
965 
968  SPOT_DEF_BINOP(Implies);
970 
973  SPOT_DEF_BINOP(Equiv);
975 
978  SPOT_DEF_BINOP(U);
980 
983  SPOT_DEF_BINOP(R);
985 
988  SPOT_DEF_BINOP(W);
990 
993  SPOT_DEF_BINOP(M);
995 
998  SPOT_DEF_BINOP(EConcat);
1000 
1003  SPOT_DEF_BINOP(EConcatMarked);
1005 
1008  SPOT_DEF_BINOP(UConcat);
1010 #undef SPOT_DEF_BINOP
1011 
1017  static formula multop(op o, const std::vector<formula>& l)
1018  {
1019  std::vector<const fnode*> tmp;
1020  tmp.reserve(l.size());
1021  for (auto f: l)
1022  if (f.ptr_)
1023  tmp.emplace_back(f.ptr_->clone());
1024  return formula(fnode::multop(o, std::move(tmp)));
1025  }
1026 
1027 #ifndef SWIG
1028  static formula multop(op o, std::vector<formula>&& l)
1029  {
1030  std::vector<const fnode*> tmp;
1031  tmp.reserve(l.size());
1032  for (auto f: l)
1033  if (f.ptr_)
1034  tmp.emplace_back(f.to_node_());
1035  return formula(fnode::multop(o, std::move(tmp)));
1036  }
1037 #endif // !SWIG
1038 
1040 #ifdef SWIG
1041 #define SPOT_DEF_MULTOP(Name) \
1042  static formula Name(const std::vector<formula>& l) \
1043  { \
1044  return multop(op::Name, l); \
1045  }
1046 #else // !SWIG
1047 #define SPOT_DEF_MULTOP(Name) \
1048  static formula Name(const std::vector<formula>& l) \
1049  { \
1050  return multop(op::Name, l); \
1051  } \
1052  \
1053  static formula Name(std::vector<formula>&& l) \
1054  { \
1055  return multop(op::Name, std::move(l)); \
1056  }
1057 #endif // !SWIG
1058  SPOT_DEF_MULTOP(Or);
1062 
1065  SPOT_DEF_MULTOP(OrRat);
1067 
1070  SPOT_DEF_MULTOP(And);
1072 
1075  SPOT_DEF_MULTOP(AndRat);
1077 
1080  SPOT_DEF_MULTOP(AndNLM);
1082 
1085  SPOT_DEF_MULTOP(Concat);
1087 
1090  SPOT_DEF_MULTOP(Fusion);
1092 #undef SPOT_DEF_MULTOP
1093 
1098  static formula bunop(op o, const formula& f,
1099  uint8_t min = 0U,
1100  uint8_t max = unbounded())
1101  {
1102  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1103  }
1104 
1105 #ifndef SWIG
1106  static formula bunop(op o, formula&& f,
1107  uint8_t min = 0U,
1108  uint8_t max = unbounded())
1109  {
1110  return formula(fnode::bunop(o, f.to_node_(), min, max));
1111  }
1112 #endif // !SWIG
1113 
1115 #if SWIG
1116 #define SPOT_DEF_BUNOP(Name) \
1117  static formula Name(const formula& f, \
1118  uint8_t min = 0U, \
1119  uint8_t max = unbounded()) \
1120  { \
1121  return bunop(op::Name, f, min, max); \
1122  }
1123 #else // !SWIG
1124 #define SPOT_DEF_BUNOP(Name) \
1125  static formula Name(const formula& f, \
1126  uint8_t min = 0U, \
1127  uint8_t max = unbounded()) \
1128  { \
1129  return bunop(op::Name, f, min, max); \
1130  } \
1131  static formula Name(formula&& f, \
1132  uint8_t min = 0U, \
1133  uint8_t max = unbounded()) \
1134  { \
1135  return bunop(op::Name, std::move(f), min, max); \
1136  }
1137 #endif
1138  SPOT_DEF_BUNOP(Star);
1142 
1147 
1162  SPOT_DEF_BUNOP(FStar);
1165 #undef SPOT_DEF_BUNOP
1166 
1172  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1173 
1179  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1180 
1181 #ifndef SWIG
1182  const fnode* to_node_()
1192  {
1193  auto tmp = ptr_;
1194  ptr_ = nullptr;
1195  return tmp;
1196  }
1197 #endif
1198 
1200  op kind() const
1201  {
1202  return ptr_->kind();
1203  }
1204 
1206  std::string kindstr() const
1207  {
1208  return ptr_->kindstr();
1209  }
1210 
1212  bool is(op o) const
1213  {
1214  return ptr_->is(o);
1215  }
1216 
1217 #ifndef SWIG
1218  bool is(op o1, op o2) const
1220  {
1221  return ptr_->is(o1, o2);
1222  }
1223 
1225  bool is(std::initializer_list<op> l) const
1226  {
1227  return ptr_->is(l);
1228  }
1229 #endif
1230 
1235  {
1236  auto f = ptr_->get_child_of(o);
1237  if (f)
1238  f->clone();
1239  return formula(f);
1240  }
1241 
1242 #ifndef SWIG
1243  formula get_child_of(std::initializer_list<op> l) const
1250  {
1251  auto f = ptr_->get_child_of(l);
1252  if (f)
1253  f->clone();
1254  return formula(f);
1255  }
1256 #endif
1257 
1261  unsigned min() const
1262  {
1263  return ptr_->min();
1264  }
1265 
1269  unsigned max() const
1270  {
1271  return ptr_->max();
1272  }
1273 
1275  unsigned size() const
1276  {
1277  return ptr_->size();
1278  }
1279 
1288  size_t id() const
1289  {
1290  return ptr_->id();
1291  }
1292 
1293 #ifndef SWIG
1294  class SPOT_API formula_child_iterator final
1296  {
1297  const fnode*const* ptr_;
1298  public:
1299  formula_child_iterator()
1300  : ptr_(nullptr)
1301  {
1302  }
1303 
1304  formula_child_iterator(const fnode*const* f)
1305  : ptr_(f)
1306  {
1307  }
1308 
1309  bool operator==(formula_child_iterator o)
1310  {
1311  return ptr_ == o.ptr_;
1312  }
1313 
1314  bool operator!=(formula_child_iterator o)
1315  {
1316  return ptr_ != o.ptr_;
1317  }
1318 
1319  formula operator*()
1320  {
1321  return formula((*ptr_)->clone());
1322  }
1323 
1324  formula_child_iterator operator++()
1325  {
1326  ++ptr_;
1327  return *this;
1328  }
1329 
1330  formula_child_iterator operator++(int)
1331  {
1332  auto tmp = *this;
1333  ++ptr_;
1334  return tmp;
1335  }
1336  };
1337 
1339  formula_child_iterator begin() const
1340  {
1341  return ptr_->begin();
1342  }
1343 
1345  formula_child_iterator end() const
1346  {
1347  return ptr_->end();
1348  }
1349 
1351  formula operator[](unsigned i) const
1352  {
1353  return formula(ptr_->nth(i)->clone());
1354  }
1355 #endif
1356 
1358  static formula ff()
1359  {
1360  return formula(fnode::ff());
1361  }
1362 
1364  bool is_ff() const
1365  {
1366  return ptr_->is_ff();
1367  }
1368 
1370  static formula tt()
1371  {
1372  return formula(fnode::tt());
1373  }
1374 
1376  bool is_tt() const
1377  {
1378  return ptr_->is_tt();
1379  }
1380 
1382  static formula eword()
1383  {
1384  return formula(fnode::eword());
1385  }
1386 
1388  bool is_eword() const
1389  {
1390  return ptr_->is_eword();
1391  }
1392 
1394  bool is_constant() const
1395  {
1396  return ptr_->is_constant();
1397  }
1398 
1403  bool is_Kleene_star() const
1404  {
1405  return ptr_->is_Kleene_star();
1406  }
1407 
1410  {
1411  return formula(fnode::one_star()->clone());
1412  }
1413 
1416  bool is_literal()
1417  {
1418  return (is(op::ap) ||
1419  // If f is in nenoform, Not can only occur in front of
1420  // an atomic proposition. So this way we do not have
1421  // to check the type of the child.
1422  (is(op::Not) && is_boolean() && is_in_nenoform()));
1423  }
1424 
1428  const std::string& ap_name() const
1429  {
1430  return ptr_->ap_name();
1431  }
1432 
1437  std::ostream& dump(std::ostream& os) const
1438  {
1439  return ptr_->dump(os);
1440  }
1441 
1447  formula all_but(unsigned i) const
1448  {
1449  return formula(ptr_->all_but(i));
1450  }
1451 
1461  unsigned boolean_count() const
1462  {
1463  return ptr_->boolean_count();
1464  }
1465 
1479  formula boolean_operands(unsigned* width = nullptr) const
1480  {
1481  return formula(ptr_->boolean_operands(width));
1482  }
1483 
1484 #define SPOT_DEF_PROP(Name) \
1485  bool Name() const \
1486  { \
1487  return ptr_->Name(); \
1488  }
1489  // Properties //
1492 
1494  SPOT_DEF_PROP(is_boolean);
1496  SPOT_DEF_PROP(is_sugar_free_boolean);
1501  SPOT_DEF_PROP(is_in_nenoform);
1503  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1505  SPOT_DEF_PROP(is_sugar_free_ltl);
1507  SPOT_DEF_PROP(is_ltl_formula);
1509  SPOT_DEF_PROP(is_psl_formula);
1511  SPOT_DEF_PROP(is_sere_formula);
1514  SPOT_DEF_PROP(is_finite);
1518 
1532  SPOT_DEF_PROP(is_eventual);
1539 
1553  SPOT_DEF_PROP(is_universal);
1558  SPOT_DEF_PROP(is_syntactic_safety);
1560  SPOT_DEF_PROP(is_syntactic_guarantee);
1562  SPOT_DEF_PROP(is_syntactic_obligation);
1564  SPOT_DEF_PROP(is_syntactic_recurrence);
1566  SPOT_DEF_PROP(is_syntactic_persistence);
1569  SPOT_DEF_PROP(is_marked);
1571  SPOT_DEF_PROP(accepts_eword);
1577  SPOT_DEF_PROP(has_lbt_atomic_props);
1586  SPOT_DEF_PROP(has_spin_atomic_props);
1587 #undef SPOT_DEF_PROP
1588 
1590  template<typename Trans>
1591  formula map(Trans trans)
1592  {
1593  switch (op o = kind())
1594  {
1595  case op::ff:
1596  case op::tt:
1597  case op::eword:
1598  case op::ap:
1599  return *this;
1600  case op::Not:
1601  case op::X:
1602  case op::F:
1603  case op::G:
1604  case op::Closure:
1605  case op::NegClosure:
1606  case op::NegClosureMarked:
1607  return unop(o, trans((*this)[0]));
1608  case op::Xor:
1609  case op::Implies:
1610  case op::Equiv:
1611  case op::U:
1612  case op::R:
1613  case op::W:
1614  case op::M:
1615  case op::EConcat:
1616  case op::EConcatMarked:
1617  case op::UConcat:
1618  {
1619  formula tmp = trans((*this)[0]);
1620  return binop(o, tmp, trans((*this)[1]));
1621  }
1622  case op::Or:
1623  case op::OrRat:
1624  case op::And:
1625  case op::AndRat:
1626  case op::AndNLM:
1627  case op::Concat:
1628  case op::Fusion:
1629  {
1630  std::vector<formula> tmp;
1631  tmp.reserve(size());
1632  for (auto f: *this)
1633  tmp.emplace_back(trans(f));
1634  return multop(o, std::move(tmp));
1635  }
1636  case op::Star:
1637  case op::FStar:
1638  return bunop(o, trans((*this)[0]), min(), max());
1639  }
1640  SPOT_UNREACHABLE();
1641  }
1642 
1648  template<typename Func>
1649  void traverse(Func func)
1650  {
1651  if (func(*this))
1652  return;
1653  for (auto f: *this)
1654  f.traverse(func);
1655  }
1656 
1657  private:
1658 #ifndef SWIG
1659  [[noreturn]] static void report_ap_invalid_arg();
1660 #endif
1661  };
1662 
1664  SPOT_API
1665  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1666  bool abbreviated = false);
1667 
1669  SPOT_API
1670  std::list<std::string> list_formula_props(const formula& f);
1671 
1673  SPOT_API
1674  std::ostream& operator<<(std::ostream& os, const formula& f);
1675 }
1676 
1677 #ifndef SWIG
1678 namespace std
1679 {
1680  template <>
1681  struct hash<spot::formula>
1682  {
1683  size_t operator()(const spot::formula& x) const noexcept
1684  {
1685  return x.id();
1686  }
1687  };
1688 }
1689 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1017
const fnode *const * begin() const
Definition: formula.hh:241
Definition: automata.hh:26
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1409
~formula()
Destroy a formula.
Definition: formula.hh:718
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:928
bool is_boolean() const
Definition: formula.hh:357
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1339
static const fnode * eword()
Definition: formula.hh:285
static const fnode * ap(const std::string &name)
std::ostream & dump(std::ostream &os) const
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition: formula.hh:1394
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1437
unsigned max() const
Definition: formula.hh:221
size_t id() const
Definition: formula.hh:235
PSL Closure.
bool is(op o) const
Definition: formula.hh:165
bool is_psl_formula() const
Definition: formula.hh:393
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1269
bool is_finite() const
Definition: formula.hh:405
bool is_eword() const
Definition: formula.hh:291
unsigned boolean_count() const
Definition: formula.hh:328
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:820
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:703
static formula tt()
Return the true constant.
Definition: formula.hh:1370
const fnode * get_child_of(op o) const
Definition: formula.hh:190
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1261
Definition: formula.hh:1678
Empty word.
bool is_syntactic_guarantee() const
Definition: formula.hh:429
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1364
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1428
static const fnode * tt()
Definition: formula.hh:273
bool is_syntactic_persistence() const
Definition: formula.hh:447
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:923
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:918
const fnode * nth(unsigned i) const
Definition: formula.hh:253
bool is_marked() const
Definition: formula.hh:453
Concatenation.
bool is_syntactic_recurrence() const
Definition: formula.hh:441
bool is(std::initializer_list< op > l) const
Definition: formula.hh:177
Main class for temporal logic formula.
Definition: formula.hh:673
bool is_syntactic_obligation() const
Definition: formula.hh:435
int atomic_prop_cmp(const fnode *f, const fnode *g)
Order two atomic propositions.
Globally.
bool is(op o1, op o2) const
Definition: formula.hh:171
bool has_spin_atomic_props() const
Definition: formula.hh:471
release (dual of until)
bool is_constant() const
Definition: formula.hh:297
unsigned size() const
Return the number of children.
Definition: formula.hh:1275
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1416
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:847
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:375
Fustion Star.
weak until
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition: formula.hh:1225
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1403
size_t id() const
Return the id of a formula.
Definition: formula.hh:1288
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1212
void destroy() const
Dereference an fnode.
Definition: formula.hh:128
static formula ff()
Return the false constant.
Definition: formula.hh:1358
std::list< std::string > list_formula_props(const formula &f)
List the properties of formula f.
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1028
static const fnode * bunop(op o, const fnode *f, uint8_t min, uint8_t max=unbounded())
Equivalence.
Non-Length-Matching Rational-And.
static const fnode * ff()
Definition: formula.hh:261
std::ostream & print_formula_props(std::ostream &out, const formula &f, bool abbreviated=false)
Print the properties of formula f on stream out.
bool is_eword() const
Whether the formula is the empty word constant.
Definition: formula.hh:1388
static formula bunop(op o, formula &&f, uint8_t min=0U, uint8_t max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1106
static const fnode * one_star()
Definition: formula.hh:311
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:691
bool is_syntactic_safety() const
Definition: formula.hh:423
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1206
Exclusive Or.
marked version of the Negated PSL Clusure
bool is_sugar_free_boolean() const
Definition: formula.hh:363
static formula eword()
Return the empty word constant.
Definition: formula.hh:1382
bool is_ltl_formula() const
Definition: formula.hh:387
Definition: formula.hh:601
bool is_in_nenoform() const
Definition: formula.hh:369
formula map(Trans trans)
Clone this node after applying trans to its children.
Definition: formula.hh:1591
bool is_ff() const
Definition: formula.hh:267
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1376
(omega-Rational) Or
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:681
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:814
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:200
static constexpr uint8_t unbounded()
Definition: formula.hh:138
unsigned size() const
Definition: formula.hh:229
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:731
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:114
bool has_lbt_atomic_props() const
Definition: formula.hh:465
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1351
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1191
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:830
bool is_sugar_free_ltl() const
Definition: formula.hh:381
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:399
op
Operator types.
Definition: formula.hh:62
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:841
bool is_tt() const
Definition: formula.hh:279
const fnode *const * end() const
Definition: formula.hh:247
static formula bunop(op o, const formula &f, uint8_t min=0U, uint8_t max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1098
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1234
Implication.
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1461
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:156
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1345
bool is_eventual() const
Definition: formula.hh:411
unsigned min() const
Definition: formula.hh:213
bool is_universal() const
Definition: formula.hh:417
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1479
Negated PSL Closure.
Rational And.
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1447
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:912
op kind() const
Return top-most operator.
Definition: formula.hh:1200
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:459
static const fnode * multop(op o, std::vector< const fnode *> l)
void traverse(Func func)
Apply func to each subformula.
Definition: formula.hh:1649
bool is_Kleene_star() const
Definition: formula.hh:303
Atomic proposition.
Eventually.
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:711
(omega-Rational) And
Rational Or.
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:697

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Wed Sep 6 2017 05:14:05 for spot by doxygen 1.8.13