spot  2.6.2
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016, 2017 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 
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 namespace spot
61 {
64  enum class op: uint8_t
65  {
66  ff,
67  tt,
68  eword,
69  ap,
70  // unary operators
71  Not,
72  X,
73  F,
74  G,
75  Closure,
76  NegClosure,
78  // binary operators
79  Xor,
80  Implies,
81  Equiv,
82  U,
83  R,
84  W,
85  M,
86  EConcat,
88  UConcat,
89  // n-ary operators
90  Or,
91  OrRat,
92  And,
93  AndRat,
94  AndNLM,
95  Concat,
96  Fusion,
97  // star-like operators
98  Star,
99  FStar,
100  };
101 
102 #ifndef SWIG
103  class SPOT_API fnode final
110  {
111  public:
116  const fnode* clone() const
117  {
118  // Saturate.
119  ++refs_;
120  if (SPOT_UNLIKELY(!refs_))
121  saturated_ = 1;
122  return this;
123  }
124 
130  void destroy() const
131  {
132  if (SPOT_LIKELY(refs_))
133  --refs_;
134  else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
135  // last reference to a node that is not a constant
136  destroy_aux();
137  }
138 
140  static constexpr uint8_t unbounded()
141  {
142  return UINT8_MAX;
143  }
144 
146  static const fnode* ap(const std::string& name);
148  static const fnode* unop(op o, const fnode* f);
150  static const fnode* binop(op o, const fnode* f, const fnode* g);
152  static const fnode* multop(op o, std::vector<const fnode*> l);
154  static const fnode* bunop(op o, const fnode* f,
155  uint8_t min, uint8_t max = unbounded());
156 
158  op kind() const
159  {
160  return op_;
161  }
162 
164  std::string kindstr() const;
165 
167  bool is(op o) const
168  {
169  return op_ == o;
170  }
171 
173  bool is(op o1, op o2) const
174  {
175  return op_ == o1 || op_ == o2;
176  }
177 
179  bool is(std::initializer_list<op> l) const
180  {
181  const fnode* n = this;
182  for (auto o: l)
183  {
184  if (!n->is(o))
185  return false;
186  n = n->nth(0);
187  }
188  return true;
189  }
190 
192  const fnode* get_child_of(op o) const
193  {
194  if (op_ != o)
195  return nullptr;
196  if (SPOT_UNLIKELY(size_ != 1))
197  report_get_child_of_expecting_single_child_node();
198  return nth(0);
199  }
200 
202  const fnode* get_child_of(std::initializer_list<op> l) const
203  {
204  auto c = this;
205  for (auto o: l)
206  {
207  c = c->get_child_of(o);
208  if (c == nullptr)
209  return c;
210  }
211  return c;
212  }
213 
215  unsigned min() const
216  {
217  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
218  report_min_invalid_arg();
219  return min_;
220  }
221 
223  unsigned max() const
224  {
225  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
226  report_max_invalid_arg();
227  return max_;
228  }
229 
231  unsigned size() const
232  {
233  return size_;
234  }
235 
237  bool is_leaf() const
238  {
239  return size_ == 0;
240  }
241 
243  size_t id() const
244  {
245  return id_;
246  }
247 
249  const fnode*const* begin() const
250  {
251  return children;
252  }
253 
255  const fnode*const* end() const
256  {
257  return children + size();
258  }
259 
261  const fnode* nth(unsigned i) const
262  {
263  if (SPOT_UNLIKELY(i >= size()))
264  report_non_existing_child();
265  return children[i];
266  }
267 
269  static const fnode* ff()
270  {
271  return ff_;
272  }
273 
275  bool is_ff() const
276  {
277  return op_ == op::ff;
278  }
279 
281  static const fnode* tt()
282  {
283  return tt_;
284  }
285 
287  bool is_tt() const
288  {
289  return op_ == op::tt;
290  }
291 
293  static const fnode* eword()
294  {
295  return ew_;
296  }
297 
299  bool is_eword() const
300  {
301  return op_ == op::eword;
302  }
303 
305  bool is_constant() const
306  {
307  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
308  }
309 
311  bool is_Kleene_star() const
312  {
313  if (op_ != op::Star)
314  return false;
315  return min_ == 0 && max_ == unbounded();
316  }
317 
319  static const fnode* one_star()
320  {
321  if (!one_star_)
322  one_star_ = bunop(op::Star, tt(), 0);
323  return one_star_;
324  }
325 
327  const std::string& ap_name() const;
328 
330  std::ostream& dump(std::ostream& os) const;
331 
333  const fnode* all_but(unsigned i) const;
334 
336  unsigned boolean_count() const
337  {
338  unsigned pos = 0;
339  unsigned s = size();
340  while (pos < s && children[pos]->is_boolean())
341  ++pos;
342  return pos;
343  }
344 
346  const fnode* boolean_operands(unsigned* width = nullptr) const;
347 
358  static bool instances_check();
359 
361  // Properties //
363 
365  bool is_boolean() const
366  {
367  return is_.boolean;
368  }
369 
372  {
373  return is_.sugar_free_boolean;
374  }
375 
377  bool is_in_nenoform() const
378  {
379  return is_.in_nenoform;
380  }
381 
384  {
385  return is_.syntactic_si;
386  }
387 
389  bool is_sugar_free_ltl() const
390  {
391  return is_.sugar_free_ltl;
392  }
393 
395  bool is_ltl_formula() const
396  {
397  return is_.ltl_formula;
398  }
399 
401  bool is_psl_formula() const
402  {
403  return is_.psl_formula;
404  }
405 
407  bool is_sere_formula() const
408  {
409  return is_.sere_formula;
410  }
411 
413  bool is_finite() const
414  {
415  return is_.finite;
416  }
417 
419  bool is_eventual() const
420  {
421  return is_.eventual;
422  }
423 
425  bool is_universal() const
426  {
427  return is_.universal;
428  }
429 
431  bool is_syntactic_safety() const
432  {
433  return is_.syntactic_safety;
434  }
435 
438  {
439  return is_.syntactic_guarantee;
440  }
441 
444  {
445  return is_.syntactic_obligation;
446  }
447 
450  {
451  return is_.syntactic_recurrence;
452  }
453 
456  {
457  return is_.syntactic_persistence;
458  }
459 
461  bool is_marked() const
462  {
463  return !is_.not_marked;
464  }
465 
467  bool accepts_eword() const
468  {
469  return is_.accepting_eword;
470  }
471 
473  bool has_lbt_atomic_props() const
474  {
475  return is_.lbt_atomic_props;
476  }
477 
480  {
481  return is_.spin_atomic_props;
482  }
483 
484  private:
485  void setup_props(op o);
486  void destroy_aux() const;
487 
488  [[noreturn]] static void report_non_existing_child();
489  [[noreturn]] static void report_too_many_children();
490  [[noreturn]] static void
491  report_get_child_of_expecting_single_child_node();
492  [[noreturn]] static void report_min_invalid_arg();
493  [[noreturn]] static void report_max_invalid_arg();
494 
495  static const fnode* unique(fnode*);
496 
497  // Destruction may only happen via destroy().
498  ~fnode() = default;
499  // Disallow copies.
500  fnode(const fnode&) = delete;
501  fnode& operator=(const fnode&) = delete;
502 
503 
504 
505  template<class iter>
506  fnode(op o, iter begin, iter end)
507  // Clang has some optimization where is it able to combine the
508  // 4 movb initializing op_,min_,max_,saturated_ into a single
509  // movl. Also it can optimize the three byte-comparisons of
510  // is_Kleene_star() into a single masked 32-bit comparison.
511  // The latter optimization triggers warnings from valgrind if
512  // min_ and max_ are not initialized. So to benefit from the
513  // initialization optimization and the is_Kleene_star()
514  // optimization in Clang, we always initialize min_ and max_
515  // with this compiler. Do not do it the rest of the time,
516  // since the optimization is not done.
517  : op_(o),
518 #if __llvm__
519  min_(0), max_(0),
520 #endif
521  saturated_(0)
522  {
523  size_t s = std::distance(begin, end);
524  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
525  report_too_many_children();
526  size_ = s;
527  auto pos = children;
528  for (auto i = begin; i != end; ++i)
529  *pos++ = *i;
530  setup_props(o);
531  }
532 
533  fnode(op o, std::initializer_list<const fnode*> l)
534  : fnode(o, l.begin(), l.end())
535  {
536  }
537 
538  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
539  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
540  {
541  children[0] = f;
542  setup_props(o);
543  }
544 
545  static const fnode* ff_;
546  static const fnode* tt_;
547  static const fnode* ew_;
548  static const fnode* one_star_;
549 
550  op op_; // operator
551  uint8_t min_; // range minimum (for star-like operators)
552  uint8_t max_; // range maximum;
553  mutable uint8_t saturated_;
554  uint16_t size_; // number of children
555  mutable uint16_t refs_ = 0; // reference count - 1;
556  size_t id_; // Also used as hash.
557  static size_t next_id_;
558 
559  struct ltl_prop
560  {
561  // All properties here should be expressed in such a a way
562  // that property(f && g) is just property(f)&property(g).
563  // This allows us to compute all properties of a compound
564  // formula in one operation.
565  //
566  // For instance we do not use a property that says "has
567  // temporal operator", because it would require an OR between
568  // the two arguments. Instead we have a property that
569  // says "no temporal operator", and that one is computed
570  // with an AND between the arguments.
571  //
572  // Also choose a name that makes sense when prefixed with
573  // "the formula is".
574  bool boolean:1; // No temporal operators.
575  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
576  bool in_nenoform:1; // Negative Normal Form.
577  bool syntactic_si:1; // LTL-X or siPSL
578  bool sugar_free_ltl:1; // No F and G operators.
579  bool ltl_formula:1; // Only LTL operators.
580  bool psl_formula:1; // Only PSL operators.
581  bool sere_formula:1; // Only SERE operators.
582  bool finite:1; // Finite SERE formulae, or Bool+X forms.
583  bool eventual:1; // Purely eventual formula.
584  bool universal:1; // Purely universal formula.
585  bool syntactic_safety:1; // Syntactic Safety Property.
586  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
587  bool syntactic_obligation:1; // Syntactic Obligation Property.
588  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
589  bool syntactic_persistence:1; // Syntactic Persistence Property.
590  bool not_marked:1; // No occurrence of EConcatMarked.
591  bool accepting_eword:1; // Accepts the empty word.
592  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
593  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
594  };
595  union
596  {
597  // Use an unsigned for fast computation of all properties.
598  unsigned props;
599  ltl_prop is_;
600  };
601 
602  const fnode* children[1];
603  };
604 
606  SPOT_API
607  int atomic_prop_cmp(const fnode* f, const fnode* g);
608 
610  {
611  bool
612  operator()(const fnode* left, const fnode* right) const
613  {
614  SPOT_ASSERT(left);
615  SPOT_ASSERT(right);
616  if (left == right)
617  return false;
618 
619  // We want Boolean formulae first.
620  bool lib = left->is_boolean();
621  if (lib != right->is_boolean())
622  return lib;
623 
624  // We have two Boolean formulae
625  if (lib)
626  {
627  bool lconst = left->is_constant();
628  if (lconst != right->is_constant())
629  return lconst;
630  if (!lconst)
631  {
632  auto get_literal = [](const fnode* f) -> const fnode*
633  {
634  if (f->is(op::Not))
635  f = f->nth(0);
636  if (f->is(op::ap))
637  return f;
638  return nullptr;
639  };
640  // Literals should come first
641  const fnode* litl = get_literal(left);
642  const fnode* litr = get_literal(right);
643  if (!litl != !litr)
644  return litl;
645  if (litl)
646  {
647  // And they should be sorted alphabetically
648  int cmp = atomic_prop_cmp(litl, litr);
649  if (cmp)
650  return cmp < 0;
651  }
652  }
653  }
654 
655  size_t l = left->id();
656  size_t r = right->id();
657  if (l != r)
658  return l < r;
659  // Because the hash code assigned to each formula is the
660  // number of formulae constructed so far, it is very unlikely
661  // that we will ever reach a case were two different formulae
662  // have the same hash. This will happen only ever with have
663  // produced 256**sizeof(size_t) formulae (i.e. max_count has
664  // looped back to 0 and started over). In that case we can
665  // order two formulas by looking at their text representation.
666  // We could be more efficient and look at their AST, but it's
667  // not worth the burden. (Also ordering pointers is ruled out
668  // because it breaks the determinism of the implementation.)
669  std::ostringstream old;
670  left->dump(old);
671  std::ostringstream ord;
672  right->dump(ord);
673  return old.str() < ord.str();
674  }
675  };
676 
677 #endif // SWIG
678 
681  class SPOT_API formula final
682  {
683  const fnode* ptr_;
684  public:
689  explicit formula(const fnode* f) noexcept
690  : ptr_(f)
691  {
692  }
693 
699  formula(std::nullptr_t) noexcept
700  : ptr_(nullptr)
701  {
702  }
703 
705  formula() noexcept
706  : ptr_(nullptr)
707  {
708  }
709 
711  formula(const formula& f) noexcept
712  : ptr_(f.ptr_)
713  {
714  if (ptr_)
715  ptr_->clone();
716  }
717 
719  formula(formula&& f) noexcept
720  : ptr_(f.ptr_)
721  {
722  f.ptr_ = nullptr;
723  }
724 
727  {
728  if (ptr_)
729  ptr_->destroy();
730  }
731 
739  const formula& operator=(std::nullptr_t)
740  {
741  this->~formula();
742  ptr_ = nullptr;
743  return *this;
744  }
745 
746  const formula& operator=(const formula& f)
747  {
748  this->~formula();
749  if ((ptr_ = f.ptr_))
750  ptr_->clone();
751  return *this;
752  }
753 
754  const formula& operator=(formula&& f) noexcept
755  {
756  std::swap(f.ptr_, ptr_);
757  return *this;
758  }
759 
760  bool operator<(const formula& other) const noexcept
761  {
762  if (SPOT_UNLIKELY(!other.ptr_))
763  return false;
764  if (SPOT_UNLIKELY(!ptr_))
765  return true;
766  if (id() < other.id())
767  return true;
768  if (id() > other.id())
769  return false;
770  // The case where id()==other.id() but ptr_ != other.ptr_ is
771  // very unlikely (we would need to build more that UINT_MAX
772  // formulas), so let's just compare pointer, and ignore the fact
773  // that it may give some nondeterminism.
774  return ptr_ < other.ptr_;
775  }
776 
777  bool operator<=(const formula& other) const noexcept
778  {
779  return *this == other || *this < other;
780  }
781 
782  bool operator>(const formula& other) const noexcept
783  {
784  return !(*this <= other);
785  }
786 
787  bool operator>=(const formula& other) const noexcept
788  {
789  return !(*this < other);
790  }
791 
792  bool operator==(const formula& other) const noexcept
793  {
794  return other.ptr_ == ptr_;
795  }
796 
797  bool operator==(std::nullptr_t) const noexcept
798  {
799  return ptr_ == nullptr;
800  }
801 
802  bool operator!=(const formula& other) const noexcept
803  {
804  return other.ptr_ != ptr_;
805  }
806 
807  bool operator!=(std::nullptr_t) const noexcept
808  {
809  return ptr_ != nullptr;
810  }
811 
812  operator bool() const
813  {
814  return ptr_ != nullptr;
815  }
816 
818  // Forwarded functions //
820 
822  static constexpr uint8_t unbounded()
823  {
824  return fnode::unbounded();
825  }
826 
828  static formula ap(const std::string& name)
829  {
830  return formula(fnode::ap(name));
831  }
832 
838  static formula ap(const formula& a)
839  {
840  if (SPOT_UNLIKELY(a.kind() != op::ap))
841  report_ap_invalid_arg();
842  return a;
843  }
844 
849  static formula unop(op o, const formula& f)
850  {
851  return formula(fnode::unop(o, f.ptr_->clone()));
852  }
853 
854 #ifndef SWIG
855  static formula unop(op o, formula&& f)
856  {
857  return formula(fnode::unop(o, f.to_node_()));
858  }
859 #endif // !SWIG
860 
862 #ifdef SWIG
863 #define SPOT_DEF_UNOP(Name) \
864  static formula Name(const formula& f) \
865  { \
866  return unop(op::Name, f); \
867  }
868 #else // !SWIG
869 #define SPOT_DEF_UNOP(Name) \
870  static formula Name(const formula& f) \
871  { \
872  return unop(op::Name, f); \
873  } \
874  static formula Name(formula&& f) \
875  { \
876  return unop(op::Name, std::move(f)); \
877  }
878 #endif // !SWIG
879  SPOT_DEF_UNOP(Not);
883 
886  SPOT_DEF_UNOP(X);
888 
891  SPOT_DEF_UNOP(F);
893 
896  SPOT_DEF_UNOP(G);
898 
901  SPOT_DEF_UNOP(Closure);
903 
906  SPOT_DEF_UNOP(NegClosure);
908 
911  SPOT_DEF_UNOP(NegClosureMarked);
913 #undef SPOT_DEF_UNOP
914 
920  static formula binop(op o, const formula& f, const formula& g)
921  {
922  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
923  }
924 
925 #ifndef SWIG
926  static formula binop(op o, const formula& f, formula&& g)
927  {
928  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
929  }
930 
931  static formula binop(op o, formula&& f, const formula& g)
932  {
933  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
934  }
935 
936  static formula binop(op o, formula&& f, formula&& g)
937  {
938  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
939  }
941 
942 #endif //SWIG
943 
944 #ifdef SWIG
945 #define SPOT_DEF_BINOP(Name) \
946  static formula Name(const formula& f, const formula& g) \
947  { \
948  return binop(op::Name, f, g); \
949  }
950 #else // !SWIG
951 #define SPOT_DEF_BINOP(Name) \
952  static formula Name(const formula& f, const formula& g) \
953  { \
954  return binop(op::Name, f, g); \
955  } \
956  static formula Name(const formula& f, formula&& g) \
957  { \
958  return binop(op::Name, f, std::move(g)); \
959  } \
960  static formula Name(formula&& f, const formula& g) \
961  { \
962  return binop(op::Name, std::move(f), g); \
963  } \
964  static formula Name(formula&& f, formula&& g) \
965  { \
966  return binop(op::Name, std::move(f), std::move(g)); \
967  }
968 #endif // !SWIG
969  SPOT_DEF_BINOP(Xor);
973 
976  SPOT_DEF_BINOP(Implies);
978 
981  SPOT_DEF_BINOP(Equiv);
983 
986  SPOT_DEF_BINOP(U);
988 
991  SPOT_DEF_BINOP(R);
993 
996  SPOT_DEF_BINOP(W);
998 
1001  SPOT_DEF_BINOP(M);
1003 
1006  SPOT_DEF_BINOP(EConcat);
1008 
1011  SPOT_DEF_BINOP(EConcatMarked);
1013 
1016  SPOT_DEF_BINOP(UConcat);
1018 #undef SPOT_DEF_BINOP
1019 
1025  static formula multop(op o, const std::vector<formula>& l)
1026  {
1027  std::vector<const fnode*> tmp;
1028  tmp.reserve(l.size());
1029  for (auto f: l)
1030  if (f.ptr_)
1031  tmp.emplace_back(f.ptr_->clone());
1032  return formula(fnode::multop(o, std::move(tmp)));
1033  }
1034 
1035 #ifndef SWIG
1036  static formula multop(op o, std::vector<formula>&& l)
1037  {
1038  std::vector<const fnode*> tmp;
1039  tmp.reserve(l.size());
1040  for (auto f: l)
1041  if (f.ptr_)
1042  tmp.emplace_back(f.to_node_());
1043  return formula(fnode::multop(o, std::move(tmp)));
1044  }
1045 #endif // !SWIG
1046 
1048 #ifdef SWIG
1049 #define SPOT_DEF_MULTOP(Name) \
1050  static formula Name(const std::vector<formula>& l) \
1051  { \
1052  return multop(op::Name, l); \
1053  }
1054 #else // !SWIG
1055 #define SPOT_DEF_MULTOP(Name) \
1056  static formula Name(const std::vector<formula>& l) \
1057  { \
1058  return multop(op::Name, l); \
1059  } \
1060  \
1061  static formula Name(std::vector<formula>&& l) \
1062  { \
1063  return multop(op::Name, std::move(l)); \
1064  }
1065 #endif // !SWIG
1066  SPOT_DEF_MULTOP(Or);
1070 
1073  SPOT_DEF_MULTOP(OrRat);
1075 
1078  SPOT_DEF_MULTOP(And);
1080 
1083  SPOT_DEF_MULTOP(AndRat);
1085 
1088  SPOT_DEF_MULTOP(AndNLM);
1090 
1093  SPOT_DEF_MULTOP(Concat);
1095 
1098  SPOT_DEF_MULTOP(Fusion);
1100 #undef SPOT_DEF_MULTOP
1101 
1106  static formula bunop(op o, const formula& f,
1107  uint8_t min = 0U,
1108  uint8_t max = unbounded())
1109  {
1110  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1111  }
1112 
1113 #ifndef SWIG
1114  static formula bunop(op o, formula&& f,
1115  uint8_t min = 0U,
1116  uint8_t max = unbounded())
1117  {
1118  return formula(fnode::bunop(o, f.to_node_(), min, max));
1119  }
1120 #endif // !SWIG
1121 
1123 #if 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 #else // !SWIG
1132 #define SPOT_DEF_BUNOP(Name) \
1133  static formula Name(const formula& f, \
1134  uint8_t min = 0U, \
1135  uint8_t max = unbounded()) \
1136  { \
1137  return bunop(op::Name, f, min, max); \
1138  } \
1139  static formula Name(formula&& f, \
1140  uint8_t min = 0U, \
1141  uint8_t max = unbounded()) \
1142  { \
1143  return bunop(op::Name, std::move(f), min, max); \
1144  }
1145 #endif
1146  SPOT_DEF_BUNOP(Star);
1150 
1155 
1170  SPOT_DEF_BUNOP(FStar);
1173 #undef SPOT_DEF_BUNOP
1174 
1180  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1181 
1187  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1188 
1189 #ifndef SWIG
1190  const fnode* to_node_()
1200  {
1201  auto tmp = ptr_;
1202  ptr_ = nullptr;
1203  return tmp;
1204  }
1205 #endif
1206 
1208  op kind() const
1209  {
1210  return ptr_->kind();
1211  }
1212 
1214  std::string kindstr() const
1215  {
1216  return ptr_->kindstr();
1217  }
1218 
1220  bool is(op o) const
1221  {
1222  return ptr_->is(o);
1223  }
1224 
1225 #ifndef SWIG
1226  bool is(op o1, op o2) const
1228  {
1229  return ptr_->is(o1, o2);
1230  }
1231 
1233  bool is(std::initializer_list<op> l) const
1234  {
1235  return ptr_->is(l);
1236  }
1237 #endif
1238 
1243  {
1244  auto f = ptr_->get_child_of(o);
1245  if (f)
1246  f->clone();
1247  return formula(f);
1248  }
1249 
1250 #ifndef SWIG
1251  formula get_child_of(std::initializer_list<op> l) const
1258  {
1259  auto f = ptr_->get_child_of(l);
1260  if (f)
1261  f->clone();
1262  return formula(f);
1263  }
1264 #endif
1265 
1269  unsigned min() const
1270  {
1271  return ptr_->min();
1272  }
1273 
1277  unsigned max() const
1278  {
1279  return ptr_->max();
1280  }
1281 
1283  unsigned size() const
1284  {
1285  return ptr_->size();
1286  }
1287 
1292  bool is_leaf() const
1293  {
1294  return ptr_->is_leaf();
1295  }
1296 
1305  size_t id() const
1306  {
1307  return ptr_->id();
1308  }
1309 
1310 #ifndef SWIG
1311  class SPOT_API formula_child_iterator final
1313  {
1314  const fnode*const* ptr_;
1315  public:
1316  formula_child_iterator()
1317  : ptr_(nullptr)
1318  {
1319  }
1320 
1321  formula_child_iterator(const fnode*const* f)
1322  : ptr_(f)
1323  {
1324  }
1325 
1326  bool operator==(formula_child_iterator o)
1327  {
1328  return ptr_ == o.ptr_;
1329  }
1330 
1331  bool operator!=(formula_child_iterator o)
1332  {
1333  return ptr_ != o.ptr_;
1334  }
1335 
1336  formula operator*()
1337  {
1338  return formula((*ptr_)->clone());
1339  }
1340 
1341  formula_child_iterator operator++()
1342  {
1343  ++ptr_;
1344  return *this;
1345  }
1346 
1347  formula_child_iterator operator++(int)
1348  {
1349  auto tmp = *this;
1350  ++ptr_;
1351  return tmp;
1352  }
1353  };
1354 
1356  formula_child_iterator begin() const
1357  {
1358  return ptr_->begin();
1359  }
1360 
1362  formula_child_iterator end() const
1363  {
1364  return ptr_->end();
1365  }
1366 
1368  formula operator[](unsigned i) const
1369  {
1370  return formula(ptr_->nth(i)->clone());
1371  }
1372 #endif
1373 
1375  static formula ff()
1376  {
1377  return formula(fnode::ff());
1378  }
1379 
1381  bool is_ff() const
1382  {
1383  return ptr_->is_ff();
1384  }
1385 
1387  static formula tt()
1388  {
1389  return formula(fnode::tt());
1390  }
1391 
1393  bool is_tt() const
1394  {
1395  return ptr_->is_tt();
1396  }
1397 
1399  static formula eword()
1400  {
1401  return formula(fnode::eword());
1402  }
1403 
1405  bool is_eword() const
1406  {
1407  return ptr_->is_eword();
1408  }
1409 
1411  bool is_constant() const
1412  {
1413  return ptr_->is_constant();
1414  }
1415 
1420  bool is_Kleene_star() const
1421  {
1422  return ptr_->is_Kleene_star();
1423  }
1424 
1427  {
1428  return formula(fnode::one_star()->clone());
1429  }
1430 
1433  bool is_literal()
1434  {
1435  return (is(op::ap) ||
1436  // If f is in nenoform, Not can only occur in front of
1437  // an atomic proposition. So this way we do not have
1438  // to check the type of the child.
1439  (is(op::Not) && is_boolean() && is_in_nenoform()));
1440  }
1441 
1445  const std::string& ap_name() const
1446  {
1447  return ptr_->ap_name();
1448  }
1449 
1454  std::ostream& dump(std::ostream& os) const
1455  {
1456  return ptr_->dump(os);
1457  }
1458 
1464  formula all_but(unsigned i) const
1465  {
1466  return formula(ptr_->all_but(i));
1467  }
1468 
1478  unsigned boolean_count() const
1479  {
1480  return ptr_->boolean_count();
1481  }
1482 
1496  formula boolean_operands(unsigned* width = nullptr) const
1497  {
1498  return formula(ptr_->boolean_operands(width));
1499  }
1500 
1501 #define SPOT_DEF_PROP(Name) \
1502  bool Name() const \
1503  { \
1504  return ptr_->Name(); \
1505  }
1506  // Properties //
1509 
1511  SPOT_DEF_PROP(is_boolean);
1513  SPOT_DEF_PROP(is_sugar_free_boolean);
1518  SPOT_DEF_PROP(is_in_nenoform);
1520  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1522  SPOT_DEF_PROP(is_sugar_free_ltl);
1524  SPOT_DEF_PROP(is_ltl_formula);
1526  SPOT_DEF_PROP(is_psl_formula);
1528  SPOT_DEF_PROP(is_sere_formula);
1531  SPOT_DEF_PROP(is_finite);
1535 
1549  SPOT_DEF_PROP(is_eventual);
1556 
1570  SPOT_DEF_PROP(is_universal);
1575  SPOT_DEF_PROP(is_syntactic_safety);
1577  SPOT_DEF_PROP(is_syntactic_guarantee);
1579  SPOT_DEF_PROP(is_syntactic_obligation);
1581  SPOT_DEF_PROP(is_syntactic_recurrence);
1583  SPOT_DEF_PROP(is_syntactic_persistence);
1586  SPOT_DEF_PROP(is_marked);
1588  SPOT_DEF_PROP(accepts_eword);
1594  SPOT_DEF_PROP(has_lbt_atomic_props);
1603  SPOT_DEF_PROP(has_spin_atomic_props);
1604 #undef SPOT_DEF_PROP
1605 
1609  template<typename Trans, typename... Args>
1610  formula map(Trans trans, Args&&... args)
1611  {
1612  switch (op o = kind())
1613  {
1614  case op::ff:
1615  case op::tt:
1616  case op::eword:
1617  case op::ap:
1618  return *this;
1619  case op::Not:
1620  case op::X:
1621  case op::F:
1622  case op::G:
1623  case op::Closure:
1624  case op::NegClosure:
1625  case op::NegClosureMarked:
1626  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1627  case op::Xor:
1628  case op::Implies:
1629  case op::Equiv:
1630  case op::U:
1631  case op::R:
1632  case op::W:
1633  case op::M:
1634  case op::EConcat:
1635  case op::EConcatMarked:
1636  case op::UConcat:
1637  {
1638  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1639  return binop(o, tmp,
1640  trans((*this)[1], std::forward<Args>(args)...));
1641  }
1642  case op::Or:
1643  case op::OrRat:
1644  case op::And:
1645  case op::AndRat:
1646  case op::AndNLM:
1647  case op::Concat:
1648  case op::Fusion:
1649  {
1650  std::vector<formula> tmp;
1651  tmp.reserve(size());
1652  for (auto f: *this)
1653  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1654  return multop(o, std::move(tmp));
1655  }
1656  case op::Star:
1657  case op::FStar:
1658  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1659  min(), max());
1660  }
1661  SPOT_UNREACHABLE();
1662  }
1663 
1672  template<typename Func, typename... Args>
1673  void traverse(Func func, Args&&... args)
1674  {
1675  if (func(*this, std::forward<Args>(args)...))
1676  return;
1677  for (auto f: *this)
1678  f.traverse(func, std::forward<Args>(args)...);
1679  }
1680 
1681  private:
1682 #ifndef SWIG
1683  [[noreturn]] static void report_ap_invalid_arg();
1684 #endif
1685  };
1686 
1688  SPOT_API
1689  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1690  bool abbreviated = false);
1691 
1693  SPOT_API
1694  std::list<std::string> list_formula_props(const formula& f);
1695 
1697  SPOT_API
1698  std::ostream& operator<<(std::ostream& os, const formula& f);
1699 }
1700 
1701 #ifndef SWIG
1702 namespace std
1703 {
1704  template <>
1705  struct hash<spot::formula>
1706  {
1707  size_t operator()(const spot::formula& x) const noexcept
1708  {
1709  return x.id();
1710  }
1711  };
1712 }
1713 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1025
const fnode *const * begin() const
Definition: formula.hh:249
Definition: automata.hh:26
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1426
~formula()
Destroy a formula.
Definition: formula.hh:726
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:936
bool is_boolean() const
Definition: formula.hh:365
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1356
static const fnode * eword()
Definition: formula.hh:293
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:1411
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1454
unsigned max() const
Definition: formula.hh:223
size_t id() const
Definition: formula.hh:243
PSL Closure.
bool is(op o) const
Definition: formula.hh:167
bool is_psl_formula() const
Definition: formula.hh:401
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1277
bool is_leaf() const
Definition: formula.hh:237
bool is_finite() const
Definition: formula.hh:413
bool is_eword() const
Definition: formula.hh:299
unsigned boolean_count() const
Definition: formula.hh:336
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:828
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:711
static formula tt()
Return the true constant.
Definition: formula.hh:1387
const fnode * get_child_of(op o) const
Definition: formula.hh:192
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1269
Definition: bitset.hh:405
Empty word.
bool is_syntactic_guarantee() const
Definition: formula.hh:437
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1381
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1445
static const fnode * tt()
Definition: formula.hh:281
bool is_syntactic_persistence() const
Definition: formula.hh:455
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:931
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:926
const fnode * nth(unsigned i) const
Definition: formula.hh:261
bool is_marked() const
Definition: formula.hh:461
Concatenation.
bool is_syntactic_recurrence() const
Definition: formula.hh:449
bool is(std::initializer_list< op > l) const
Definition: formula.hh:179
Main class for temporal logic formula.
Definition: formula.hh:681
bool is_syntactic_obligation() const
Definition: formula.hh:443
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:173
bool has_spin_atomic_props() const
Definition: formula.hh:479
release (dual of until)
bool is_constant() const
Definition: formula.hh:305
unsigned size() const
Return the number of children.
Definition: formula.hh:1283
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1433
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:855
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:383
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:1233
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1420
size_t id() const
Return the id of a formula.
Definition: formula.hh:1305
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1220
void destroy() const
Dereference an fnode.
Definition: formula.hh:130
static formula ff()
Return the false constant.
Definition: formula.hh:1375
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:1036
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:269
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:1405
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:1114
static const fnode * one_star()
Definition: formula.hh:319
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:699
bool is_syntactic_safety() const
Definition: formula.hh:431
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1214
Exclusive Or.
marked version of the Negated PSL Closure
bool is_sugar_free_boolean() const
Definition: formula.hh:371
static formula eword()
Return the empty word constant.
Definition: formula.hh:1399
bool is_ltl_formula() const
Definition: formula.hh:395
Definition: formula.hh:609
bool is_in_nenoform() const
Definition: formula.hh:377
bool is_ff() const
Definition: formula.hh:275
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1393
(omega-Rational) Or
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:689
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:822
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:202
static constexpr uint8_t unbounded()
Definition: formula.hh:140
unsigned size() const
Definition: formula.hh:231
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:739
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:116
bool has_lbt_atomic_props() const
Definition: formula.hh:473
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1368
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1199
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:838
bool is_sugar_free_ltl() const
Definition: formula.hh:389
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:407
op
Operator types.
Definition: formula.hh:64
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:849
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1292
bool is_tt() const
Definition: formula.hh:287
const fnode *const * end() const
Definition: formula.hh:255
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:1106
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1242
Implication.
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1478
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1673
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:158
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1362
bool is_eventual() const
Definition: formula.hh:419
unsigned min() const
Definition: formula.hh:215
bool is_universal() const
Definition: formula.hh:425
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1496
Negated PSL Closure.
Rational And.
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1464
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:920
op kind() const
Return top-most operator.
Definition: formula.hh:1208
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:467
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:311
Atomic proposition.
Eventually.
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:719
(omega-Rational) And
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1610
Rational Or.
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:705

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