spot  2.5.3
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 <initializer_list>
59 #include <limits>
60 
61 namespace spot
62 {
65  enum class op: uint8_t
66  {
67  ff,
68  tt,
69  eword,
70  ap,
71  // unary operators
72  Not,
73  X,
74  F,
75  G,
76  Closure,
77  NegClosure,
79  // binary operators
80  Xor,
81  Implies,
82  Equiv,
83  U,
84  R,
85  W,
86  M,
87  EConcat,
89  UConcat,
90  // n-ary operators
91  Or,
92  OrRat,
93  And,
94  AndRat,
95  AndNLM,
96  Concat,
97  Fusion,
98  // star-like operators
99  Star,
100  FStar,
101  };
102 
103 #ifndef SWIG
104  class SPOT_API fnode final
111  {
112  public:
117  const fnode* clone() const
118  {
119  // Saturate.
120  ++refs_;
121  if (SPOT_UNLIKELY(!refs_))
122  saturated_ = 1;
123  return this;
124  }
125 
131  void destroy() const
132  {
133  if (SPOT_LIKELY(refs_))
134  --refs_;
135  else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
136  // last reference to a node that is not a constant
137  destroy_aux();
138  }
139 
141  static constexpr uint8_t unbounded()
142  {
143  return UINT8_MAX;
144  }
145 
147  static const fnode* ap(const std::string& name);
149  static const fnode* unop(op o, const fnode* f);
151  static const fnode* binop(op o, const fnode* f, const fnode* g);
153  static const fnode* multop(op o, std::vector<const fnode*> l);
155  static const fnode* bunop(op o, const fnode* f,
156  uint8_t min, uint8_t max = unbounded());
157 
159  op kind() const
160  {
161  return op_;
162  }
163 
165  std::string kindstr() const;
166 
168  bool is(op o) const
169  {
170  return op_ == o;
171  }
172 
174  bool is(op o1, op o2) const
175  {
176  return op_ == o1 || op_ == o2;
177  }
178 
180  bool is(std::initializer_list<op> l) const
181  {
182  const fnode* n = this;
183  for (auto o: l)
184  {
185  if (!n->is(o))
186  return false;
187  n = n->nth(0);
188  }
189  return true;
190  }
191 
193  const fnode* get_child_of(op o) const
194  {
195  if (op_ != o)
196  return nullptr;
197  if (SPOT_UNLIKELY(size_ != 1))
198  report_get_child_of_expecting_single_child_node();
199  return nth(0);
200  }
201 
203  const fnode* get_child_of(std::initializer_list<op> l) const
204  {
205  auto c = this;
206  for (auto o: l)
207  {
208  c = c->get_child_of(o);
209  if (c == nullptr)
210  return c;
211  }
212  return c;
213  }
214 
216  unsigned min() const
217  {
218  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
219  report_min_invalid_arg();
220  return min_;
221  }
222 
224  unsigned max() const
225  {
226  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
227  report_max_invalid_arg();
228  return max_;
229  }
230 
232  unsigned size() const
233  {
234  return size_;
235  }
236 
238  bool is_leaf() const
239  {
240  return size_ == 0;
241  }
242 
244  size_t id() const
245  {
246  return id_;
247  }
248 
250  const fnode*const* begin() const
251  {
252  return children;
253  }
254 
256  const fnode*const* end() const
257  {
258  return children + size();
259  }
260 
262  const fnode* nth(unsigned i) const
263  {
264  if (SPOT_UNLIKELY(i >= size()))
265  report_non_existing_child();
266  return children[i];
267  }
268 
270  static const fnode* ff()
271  {
272  return ff_;
273  }
274 
276  bool is_ff() const
277  {
278  return op_ == op::ff;
279  }
280 
282  static const fnode* tt()
283  {
284  return tt_;
285  }
286 
288  bool is_tt() const
289  {
290  return op_ == op::tt;
291  }
292 
294  static const fnode* eword()
295  {
296  return ew_;
297  }
298 
300  bool is_eword() const
301  {
302  return op_ == op::eword;
303  }
304 
306  bool is_constant() const
307  {
308  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
309  }
310 
312  bool is_Kleene_star() const
313  {
314  if (op_ != op::Star)
315  return false;
316  return min_ == 0 && max_ == unbounded();
317  }
318 
320  static const fnode* one_star()
321  {
322  if (!one_star_)
323  one_star_ = bunop(op::Star, tt(), 0);
324  return one_star_;
325  }
326 
328  const std::string& ap_name() const;
329 
331  std::ostream& dump(std::ostream& os) const;
332 
334  const fnode* all_but(unsigned i) const;
335 
337  unsigned boolean_count() const
338  {
339  unsigned pos = 0;
340  unsigned s = size();
341  while (pos < s && children[pos]->is_boolean())
342  ++pos;
343  return pos;
344  }
345 
347  const fnode* boolean_operands(unsigned* width = nullptr) const;
348 
359  static bool instances_check();
360 
362  // Properties //
364 
366  bool is_boolean() const
367  {
368  return is_.boolean;
369  }
370 
373  {
374  return is_.sugar_free_boolean;
375  }
376 
378  bool is_in_nenoform() const
379  {
380  return is_.in_nenoform;
381  }
382 
385  {
386  return is_.syntactic_si;
387  }
388 
390  bool is_sugar_free_ltl() const
391  {
392  return is_.sugar_free_ltl;
393  }
394 
396  bool is_ltl_formula() const
397  {
398  return is_.ltl_formula;
399  }
400 
402  bool is_psl_formula() const
403  {
404  return is_.psl_formula;
405  }
406 
408  bool is_sere_formula() const
409  {
410  return is_.sere_formula;
411  }
412 
414  bool is_finite() const
415  {
416  return is_.finite;
417  }
418 
420  bool is_eventual() const
421  {
422  return is_.eventual;
423  }
424 
426  bool is_universal() const
427  {
428  return is_.universal;
429  }
430 
432  bool is_syntactic_safety() const
433  {
434  return is_.syntactic_safety;
435  }
436 
439  {
440  return is_.syntactic_guarantee;
441  }
442 
445  {
446  return is_.syntactic_obligation;
447  }
448 
451  {
452  return is_.syntactic_recurrence;
453  }
454 
457  {
458  return is_.syntactic_persistence;
459  }
460 
462  bool is_marked() const
463  {
464  return !is_.not_marked;
465  }
466 
468  bool accepts_eword() const
469  {
470  return is_.accepting_eword;
471  }
472 
474  bool has_lbt_atomic_props() const
475  {
476  return is_.lbt_atomic_props;
477  }
478 
481  {
482  return is_.spin_atomic_props;
483  }
484 
485  private:
486  void setup_props(op o);
487  void destroy_aux() const;
488 
489  [[noreturn]] static void report_non_existing_child();
490  [[noreturn]] static void report_too_many_children();
491  [[noreturn]] static void
492  report_get_child_of_expecting_single_child_node();
493  [[noreturn]] static void report_min_invalid_arg();
494  [[noreturn]] static void report_max_invalid_arg();
495 
496  static const fnode* unique(fnode*);
497 
498  // Destruction may only happen via destroy().
499  ~fnode() = default;
500  // Disallow copies.
501  fnode(const fnode&) = delete;
502  fnode& operator=(const fnode&) = delete;
503 
504 
505 
506  template<class iter>
507  fnode(op o, iter begin, iter end)
508  // Clang has some optimization where is it able to combine the
509  // 4 movb initializing op_,min_,max_,saturated_ into a single
510  // movl. Also it can optimize the three byte-comparisons of
511  // is_Kleene_star() into a single masked 32-bit comparison.
512  // The latter optimization triggers warnings from valgrind if
513  // min_ and max_ are not initialized. So to benefit from the
514  // initialization optimization and the is_Kleene_star()
515  // optimization in Clang, we always initialize min_ and max_
516  // with this compiler. Do not do it the rest of the time,
517  // since the optimization is not done.
518  : op_(o),
519 #if __llvm__
520  min_(0), max_(0),
521 #endif
522  saturated_(0)
523  {
524  size_t s = std::distance(begin, end);
525  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
526  report_too_many_children();
527  size_ = s;
528  auto pos = children;
529  for (auto i = begin; i != end; ++i)
530  *pos++ = *i;
531  setup_props(o);
532  }
533 
534  fnode(op o, std::initializer_list<const fnode*> l)
535  : fnode(o, l.begin(), l.end())
536  {
537  }
538 
539  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
540  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
541  {
542  children[0] = f;
543  setup_props(o);
544  }
545 
546  static const fnode* ff_;
547  static const fnode* tt_;
548  static const fnode* ew_;
549  static const fnode* one_star_;
550 
551  op op_; // operator
552  uint8_t min_; // range minimum (for star-like operators)
553  uint8_t max_; // range maximum;
554  mutable uint8_t saturated_;
555  uint16_t size_; // number of children
556  mutable uint16_t refs_ = 0; // reference count - 1;
557  size_t id_; // Also used as hash.
558  static size_t next_id_;
559 
560  struct ltl_prop
561  {
562  // All properties here should be expressed in such a a way
563  // that property(f && g) is just property(f)&property(g).
564  // This allows us to compute all properties of a compound
565  // formula in one operation.
566  //
567  // For instance we do not use a property that says "has
568  // temporal operator", because it would require an OR between
569  // the two arguments. Instead we have a property that
570  // says "no temporal operator", and that one is computed
571  // with an AND between the arguments.
572  //
573  // Also choose a name that makes sense when prefixed with
574  // "the formula is".
575  bool boolean:1; // No temporal operators.
576  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
577  bool in_nenoform:1; // Negative Normal Form.
578  bool syntactic_si:1; // LTL-X or siPSL
579  bool sugar_free_ltl:1; // No F and G operators.
580  bool ltl_formula:1; // Only LTL operators.
581  bool psl_formula:1; // Only PSL operators.
582  bool sere_formula:1; // Only SERE operators.
583  bool finite:1; // Finite SERE formulae, or Bool+X forms.
584  bool eventual:1; // Purely eventual formula.
585  bool universal:1; // Purely universal formula.
586  bool syntactic_safety:1; // Syntactic Safety Property.
587  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
588  bool syntactic_obligation:1; // Syntactic Obligation Property.
589  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
590  bool syntactic_persistence:1; // Syntactic Persistence Property.
591  bool not_marked:1; // No occurrence of EConcatMarked.
592  bool accepting_eword:1; // Accepts the empty word.
593  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
594  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
595  };
596  union
597  {
598  // Use an unsigned for fast computation of all properties.
599  unsigned props;
600  ltl_prop is_;
601  };
602 
603  const fnode* children[1];
604  };
605 
607  SPOT_API
608  int atomic_prop_cmp(const fnode* f, const fnode* g);
609 
611  {
612  bool
613  operator()(const fnode* left, const fnode* right) const
614  {
615  SPOT_ASSERT(left);
616  SPOT_ASSERT(right);
617  if (left == right)
618  return false;
619 
620  // We want Boolean formulae first.
621  bool lib = left->is_boolean();
622  if (lib != right->is_boolean())
623  return lib;
624 
625  // We have two Boolean formulae
626  if (lib)
627  {
628  bool lconst = left->is_constant();
629  if (lconst != right->is_constant())
630  return lconst;
631  if (!lconst)
632  {
633  auto get_literal = [](const fnode* f) -> const fnode*
634  {
635  if (f->is(op::Not))
636  f = f->nth(0);
637  if (f->is(op::ap))
638  return f;
639  return nullptr;
640  };
641  // Literals should come first
642  const fnode* litl = get_literal(left);
643  const fnode* litr = get_literal(right);
644  if (!litl != !litr)
645  return litl;
646  if (litl)
647  {
648  // And they should be sorted alphabetically
649  int cmp = atomic_prop_cmp(litl, litr);
650  if (cmp)
651  return cmp < 0;
652  }
653  }
654  }
655 
656  size_t l = left->id();
657  size_t r = right->id();
658  if (l != r)
659  return l < r;
660  // Because the hash code assigned to each formula is the
661  // number of formulae constructed so far, it is very unlikely
662  // that we will ever reach a case were two different formulae
663  // have the same hash. This will happen only ever with have
664  // produced 256**sizeof(size_t) formulae (i.e. max_count has
665  // looped back to 0 and started over). In that case we can
666  // order two formulas by looking at their text representation.
667  // We could be more efficient and look at their AST, but it's
668  // not worth the burden. (Also ordering pointers is ruled out
669  // because it breaks the determinism of the implementation.)
670  std::ostringstream old;
671  left->dump(old);
672  std::ostringstream ord;
673  right->dump(ord);
674  return old.str() < ord.str();
675  }
676  };
677 
678 #endif // SWIG
679 
682  class SPOT_API formula final
683  {
684  const fnode* ptr_;
685  public:
690  explicit formula(const fnode* f) noexcept
691  : ptr_(f)
692  {
693  }
694 
700  formula(std::nullptr_t) noexcept
701  : ptr_(nullptr)
702  {
703  }
704 
706  formula() noexcept
707  : ptr_(nullptr)
708  {
709  }
710 
712  formula(const formula& f) noexcept
713  : ptr_(f.ptr_)
714  {
715  if (ptr_)
716  ptr_->clone();
717  }
718 
720  formula(formula&& f) noexcept
721  : ptr_(f.ptr_)
722  {
723  f.ptr_ = nullptr;
724  }
725 
728  {
729  if (ptr_)
730  ptr_->destroy();
731  }
732 
740  const formula& operator=(std::nullptr_t)
741  {
742  this->~formula();
743  ptr_ = nullptr;
744  return *this;
745  }
746 
747  const formula& operator=(const formula& f)
748  {
749  this->~formula();
750  if ((ptr_ = f.ptr_))
751  ptr_->clone();
752  return *this;
753  }
754 
755  const formula& operator=(formula&& f) noexcept
756  {
757  std::swap(f.ptr_, ptr_);
758  return *this;
759  }
760 
761  bool operator<(const formula& other) const noexcept
762  {
763  if (SPOT_UNLIKELY(!other.ptr_))
764  return false;
765  if (SPOT_UNLIKELY(!ptr_))
766  return true;
767  if (id() < other.id())
768  return true;
769  if (id() > other.id())
770  return false;
771  // The case where id()==other.id() but ptr_ != other.ptr_ is
772  // very unlikely (we would need to build more that UINT_MAX
773  // formulas), so let's just compare pointer, and ignore the fact
774  // that it may give some nondeterminism.
775  return ptr_ < other.ptr_;
776  }
777 
778  bool operator<=(const formula& other) const noexcept
779  {
780  return *this == other || *this < other;
781  }
782 
783  bool operator>(const formula& other) const noexcept
784  {
785  return !(*this <= other);
786  }
787 
788  bool operator>=(const formula& other) const noexcept
789  {
790  return !(*this < other);
791  }
792 
793  bool operator==(const formula& other) const noexcept
794  {
795  return other.ptr_ == ptr_;
796  }
797 
798  bool operator==(std::nullptr_t) const noexcept
799  {
800  return ptr_ == nullptr;
801  }
802 
803  bool operator!=(const formula& other) const noexcept
804  {
805  return other.ptr_ != ptr_;
806  }
807 
808  bool operator!=(std::nullptr_t) const noexcept
809  {
810  return ptr_ != nullptr;
811  }
812 
813  operator bool() const
814  {
815  return ptr_ != nullptr;
816  }
817 
819  // Forwarded functions //
821 
823  static constexpr uint8_t unbounded()
824  {
825  return fnode::unbounded();
826  }
827 
829  static formula ap(const std::string& name)
830  {
831  return formula(fnode::ap(name));
832  }
833 
839  static formula ap(const formula& a)
840  {
841  if (SPOT_UNLIKELY(a.kind() != op::ap))
842  report_ap_invalid_arg();
843  return a;
844  }
845 
850  static formula unop(op o, const formula& f)
851  {
852  return formula(fnode::unop(o, f.ptr_->clone()));
853  }
854 
855 #ifndef SWIG
856  static formula unop(op o, formula&& f)
857  {
858  return formula(fnode::unop(o, f.to_node_()));
859  }
860 #endif // !SWIG
861 
863 #ifdef SWIG
864 #define SPOT_DEF_UNOP(Name) \
865  static formula Name(const formula& f) \
866  { \
867  return unop(op::Name, f); \
868  }
869 #else // !SWIG
870 #define SPOT_DEF_UNOP(Name) \
871  static formula Name(const formula& f) \
872  { \
873  return unop(op::Name, f); \
874  } \
875  static formula Name(formula&& f) \
876  { \
877  return unop(op::Name, std::move(f)); \
878  }
879 #endif // !SWIG
880  SPOT_DEF_UNOP(Not);
884 
887  SPOT_DEF_UNOP(X);
889 
892  SPOT_DEF_UNOP(F);
894 
897  SPOT_DEF_UNOP(G);
899 
902  SPOT_DEF_UNOP(Closure);
904 
907  SPOT_DEF_UNOP(NegClosure);
909 
912  SPOT_DEF_UNOP(NegClosureMarked);
914 #undef SPOT_DEF_UNOP
915 
921  static formula binop(op o, const formula& f, const formula& g)
922  {
923  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
924  }
925 
926 #ifndef SWIG
927  static formula binop(op o, const formula& f, formula&& g)
928  {
929  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
930  }
931 
932  static formula binop(op o, formula&& f, const formula& g)
933  {
934  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
935  }
936 
937  static formula binop(op o, formula&& f, formula&& g)
938  {
939  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
940  }
942 
943 #endif //SWIG
944 
945 #ifdef SWIG
946 #define SPOT_DEF_BINOP(Name) \
947  static formula Name(const formula& f, const formula& g) \
948  { \
949  return binop(op::Name, f, g); \
950  }
951 #else // !SWIG
952 #define SPOT_DEF_BINOP(Name) \
953  static formula Name(const formula& f, const formula& g) \
954  { \
955  return binop(op::Name, f, g); \
956  } \
957  static formula Name(const formula& f, formula&& g) \
958  { \
959  return binop(op::Name, f, std::move(g)); \
960  } \
961  static formula Name(formula&& f, const formula& g) \
962  { \
963  return binop(op::Name, std::move(f), g); \
964  } \
965  static formula Name(formula&& f, formula&& g) \
966  { \
967  return binop(op::Name, std::move(f), std::move(g)); \
968  }
969 #endif // !SWIG
970  SPOT_DEF_BINOP(Xor);
974 
977  SPOT_DEF_BINOP(Implies);
979 
982  SPOT_DEF_BINOP(Equiv);
984 
987  SPOT_DEF_BINOP(U);
989 
992  SPOT_DEF_BINOP(R);
994 
997  SPOT_DEF_BINOP(W);
999 
1002  SPOT_DEF_BINOP(M);
1004 
1007  SPOT_DEF_BINOP(EConcat);
1009 
1012  SPOT_DEF_BINOP(EConcatMarked);
1014 
1017  SPOT_DEF_BINOP(UConcat);
1019 #undef SPOT_DEF_BINOP
1020 
1026  static formula multop(op o, const std::vector<formula>& l)
1027  {
1028  std::vector<const fnode*> tmp;
1029  tmp.reserve(l.size());
1030  for (auto f: l)
1031  if (f.ptr_)
1032  tmp.emplace_back(f.ptr_->clone());
1033  return formula(fnode::multop(o, std::move(tmp)));
1034  }
1035 
1036 #ifndef SWIG
1037  static formula multop(op o, std::vector<formula>&& l)
1038  {
1039  std::vector<const fnode*> tmp;
1040  tmp.reserve(l.size());
1041  for (auto f: l)
1042  if (f.ptr_)
1043  tmp.emplace_back(f.to_node_());
1044  return formula(fnode::multop(o, std::move(tmp)));
1045  }
1046 #endif // !SWIG
1047 
1049 #ifdef SWIG
1050 #define SPOT_DEF_MULTOP(Name) \
1051  static formula Name(const std::vector<formula>& l) \
1052  { \
1053  return multop(op::Name, l); \
1054  }
1055 #else // !SWIG
1056 #define SPOT_DEF_MULTOP(Name) \
1057  static formula Name(const std::vector<formula>& l) \
1058  { \
1059  return multop(op::Name, l); \
1060  } \
1061  \
1062  static formula Name(std::vector<formula>&& l) \
1063  { \
1064  return multop(op::Name, std::move(l)); \
1065  }
1066 #endif // !SWIG
1067  SPOT_DEF_MULTOP(Or);
1071 
1074  SPOT_DEF_MULTOP(OrRat);
1076 
1079  SPOT_DEF_MULTOP(And);
1081 
1084  SPOT_DEF_MULTOP(AndRat);
1086 
1089  SPOT_DEF_MULTOP(AndNLM);
1091 
1094  SPOT_DEF_MULTOP(Concat);
1096 
1099  SPOT_DEF_MULTOP(Fusion);
1101 #undef SPOT_DEF_MULTOP
1102 
1107  static formula bunop(op o, const formula& f,
1108  uint8_t min = 0U,
1109  uint8_t max = unbounded())
1110  {
1111  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1112  }
1113 
1114 #ifndef SWIG
1115  static formula bunop(op o, formula&& f,
1116  uint8_t min = 0U,
1117  uint8_t max = unbounded())
1118  {
1119  return formula(fnode::bunop(o, f.to_node_(), min, max));
1120  }
1121 #endif // !SWIG
1122 
1124 #if SWIG
1125 #define SPOT_DEF_BUNOP(Name) \
1126  static formula Name(const formula& f, \
1127  uint8_t min = 0U, \
1128  uint8_t max = unbounded()) \
1129  { \
1130  return bunop(op::Name, f, min, max); \
1131  }
1132 #else // !SWIG
1133 #define SPOT_DEF_BUNOP(Name) \
1134  static formula Name(const formula& f, \
1135  uint8_t min = 0U, \
1136  uint8_t max = unbounded()) \
1137  { \
1138  return bunop(op::Name, f, min, max); \
1139  } \
1140  static formula Name(formula&& f, \
1141  uint8_t min = 0U, \
1142  uint8_t max = unbounded()) \
1143  { \
1144  return bunop(op::Name, std::move(f), min, max); \
1145  }
1146 #endif
1147  SPOT_DEF_BUNOP(Star);
1151 
1156 
1171  SPOT_DEF_BUNOP(FStar);
1174 #undef SPOT_DEF_BUNOP
1175 
1181  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1182 
1188  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1189 
1190 #ifndef SWIG
1191  const fnode* to_node_()
1201  {
1202  auto tmp = ptr_;
1203  ptr_ = nullptr;
1204  return tmp;
1205  }
1206 #endif
1207 
1209  op kind() const
1210  {
1211  return ptr_->kind();
1212  }
1213 
1215  std::string kindstr() const
1216  {
1217  return ptr_->kindstr();
1218  }
1219 
1221  bool is(op o) const
1222  {
1223  return ptr_->is(o);
1224  }
1225 
1226 #ifndef SWIG
1227  bool is(op o1, op o2) const
1229  {
1230  return ptr_->is(o1, o2);
1231  }
1232 
1234  bool is(std::initializer_list<op> l) const
1235  {
1236  return ptr_->is(l);
1237  }
1238 #endif
1239 
1244  {
1245  auto f = ptr_->get_child_of(o);
1246  if (f)
1247  f->clone();
1248  return formula(f);
1249  }
1250 
1251 #ifndef SWIG
1252  formula get_child_of(std::initializer_list<op> l) const
1259  {
1260  auto f = ptr_->get_child_of(l);
1261  if (f)
1262  f->clone();
1263  return formula(f);
1264  }
1265 #endif
1266 
1270  unsigned min() const
1271  {
1272  return ptr_->min();
1273  }
1274 
1278  unsigned max() const
1279  {
1280  return ptr_->max();
1281  }
1282 
1284  unsigned size() const
1285  {
1286  return ptr_->size();
1287  }
1288 
1293  bool is_leaf() const
1294  {
1295  return ptr_->is_leaf();
1296  }
1297 
1306  size_t id() const
1307  {
1308  return ptr_->id();
1309  }
1310 
1311 #ifndef SWIG
1312  class SPOT_API formula_child_iterator final
1314  {
1315  const fnode*const* ptr_;
1316  public:
1317  formula_child_iterator()
1318  : ptr_(nullptr)
1319  {
1320  }
1321 
1322  formula_child_iterator(const fnode*const* f)
1323  : ptr_(f)
1324  {
1325  }
1326 
1327  bool operator==(formula_child_iterator o)
1328  {
1329  return ptr_ == o.ptr_;
1330  }
1331 
1332  bool operator!=(formula_child_iterator o)
1333  {
1334  return ptr_ != o.ptr_;
1335  }
1336 
1337  formula operator*()
1338  {
1339  return formula((*ptr_)->clone());
1340  }
1341 
1342  formula_child_iterator operator++()
1343  {
1344  ++ptr_;
1345  return *this;
1346  }
1347 
1348  formula_child_iterator operator++(int)
1349  {
1350  auto tmp = *this;
1351  ++ptr_;
1352  return tmp;
1353  }
1354  };
1355 
1357  formula_child_iterator begin() const
1358  {
1359  return ptr_->begin();
1360  }
1361 
1363  formula_child_iterator end() const
1364  {
1365  return ptr_->end();
1366  }
1367 
1369  formula operator[](unsigned i) const
1370  {
1371  return formula(ptr_->nth(i)->clone());
1372  }
1373 #endif
1374 
1376  static formula ff()
1377  {
1378  return formula(fnode::ff());
1379  }
1380 
1382  bool is_ff() const
1383  {
1384  return ptr_->is_ff();
1385  }
1386 
1388  static formula tt()
1389  {
1390  return formula(fnode::tt());
1391  }
1392 
1394  bool is_tt() const
1395  {
1396  return ptr_->is_tt();
1397  }
1398 
1400  static formula eword()
1401  {
1402  return formula(fnode::eword());
1403  }
1404 
1406  bool is_eword() const
1407  {
1408  return ptr_->is_eword();
1409  }
1410 
1412  bool is_constant() const
1413  {
1414  return ptr_->is_constant();
1415  }
1416 
1421  bool is_Kleene_star() const
1422  {
1423  return ptr_->is_Kleene_star();
1424  }
1425 
1428  {
1429  return formula(fnode::one_star()->clone());
1430  }
1431 
1434  bool is_literal()
1435  {
1436  return (is(op::ap) ||
1437  // If f is in nenoform, Not can only occur in front of
1438  // an atomic proposition. So this way we do not have
1439  // to check the type of the child.
1440  (is(op::Not) && is_boolean() && is_in_nenoform()));
1441  }
1442 
1446  const std::string& ap_name() const
1447  {
1448  return ptr_->ap_name();
1449  }
1450 
1455  std::ostream& dump(std::ostream& os) const
1456  {
1457  return ptr_->dump(os);
1458  }
1459 
1465  formula all_but(unsigned i) const
1466  {
1467  return formula(ptr_->all_but(i));
1468  }
1469 
1479  unsigned boolean_count() const
1480  {
1481  return ptr_->boolean_count();
1482  }
1483 
1497  formula boolean_operands(unsigned* width = nullptr) const
1498  {
1499  return formula(ptr_->boolean_operands(width));
1500  }
1501 
1502 #define SPOT_DEF_PROP(Name) \
1503  bool Name() const \
1504  { \
1505  return ptr_->Name(); \
1506  }
1507  // Properties //
1510 
1512  SPOT_DEF_PROP(is_boolean);
1514  SPOT_DEF_PROP(is_sugar_free_boolean);
1519  SPOT_DEF_PROP(is_in_nenoform);
1521  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1523  SPOT_DEF_PROP(is_sugar_free_ltl);
1525  SPOT_DEF_PROP(is_ltl_formula);
1527  SPOT_DEF_PROP(is_psl_formula);
1529  SPOT_DEF_PROP(is_sere_formula);
1532  SPOT_DEF_PROP(is_finite);
1536 
1550  SPOT_DEF_PROP(is_eventual);
1557 
1571  SPOT_DEF_PROP(is_universal);
1576  SPOT_DEF_PROP(is_syntactic_safety);
1578  SPOT_DEF_PROP(is_syntactic_guarantee);
1580  SPOT_DEF_PROP(is_syntactic_obligation);
1582  SPOT_DEF_PROP(is_syntactic_recurrence);
1584  SPOT_DEF_PROP(is_syntactic_persistence);
1587  SPOT_DEF_PROP(is_marked);
1589  SPOT_DEF_PROP(accepts_eword);
1595  SPOT_DEF_PROP(has_lbt_atomic_props);
1604  SPOT_DEF_PROP(has_spin_atomic_props);
1605 #undef SPOT_DEF_PROP
1606 
1610  template<typename Trans, typename... Args>
1611  formula map(Trans trans, Args&&... args)
1612  {
1613  switch (op o = kind())
1614  {
1615  case op::ff:
1616  case op::tt:
1617  case op::eword:
1618  case op::ap:
1619  return *this;
1620  case op::Not:
1621  case op::X:
1622  case op::F:
1623  case op::G:
1624  case op::Closure:
1625  case op::NegClosure:
1626  case op::NegClosureMarked:
1627  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1628  case op::Xor:
1629  case op::Implies:
1630  case op::Equiv:
1631  case op::U:
1632  case op::R:
1633  case op::W:
1634  case op::M:
1635  case op::EConcat:
1636  case op::EConcatMarked:
1637  case op::UConcat:
1638  {
1639  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1640  return binop(o, tmp,
1641  trans((*this)[1], std::forward<Args>(args)...));
1642  }
1643  case op::Or:
1644  case op::OrRat:
1645  case op::And:
1646  case op::AndRat:
1647  case op::AndNLM:
1648  case op::Concat:
1649  case op::Fusion:
1650  {
1651  std::vector<formula> tmp;
1652  tmp.reserve(size());
1653  for (auto f: *this)
1654  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1655  return multop(o, std::move(tmp));
1656  }
1657  case op::Star:
1658  case op::FStar:
1659  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1660  min(), max());
1661  }
1662  SPOT_UNREACHABLE();
1663  }
1664 
1673  template<typename Func, typename... Args>
1674  void traverse(Func func, Args&&... args)
1675  {
1676  if (func(*this, std::forward<Args>(args)...))
1677  return;
1678  for (auto f: *this)
1679  f.traverse(func, std::forward<Args>(args)...);
1680  }
1681 
1682  private:
1683 #ifndef SWIG
1684  [[noreturn]] static void report_ap_invalid_arg();
1685 #endif
1686  };
1687 
1689  SPOT_API
1690  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1691  bool abbreviated = false);
1692 
1694  SPOT_API
1695  std::list<std::string> list_formula_props(const formula& f);
1696 
1698  SPOT_API
1699  std::ostream& operator<<(std::ostream& os, const formula& f);
1700 }
1701 
1702 #ifndef SWIG
1703 namespace std
1704 {
1705  template <>
1706  struct hash<spot::formula>
1707  {
1708  size_t operator()(const spot::formula& x) const noexcept
1709  {
1710  return x.id();
1711  }
1712  };
1713 }
1714 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1026
const fnode *const * begin() const
Definition: formula.hh:250
Definition: automata.hh:26
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1427
~formula()
Destroy a formula.
Definition: formula.hh:727
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:937
bool is_boolean() const
Definition: formula.hh:366
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1357
static const fnode * eword()
Definition: formula.hh:294
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:1412
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1455
unsigned max() const
Definition: formula.hh:224
size_t id() const
Definition: formula.hh:244
PSL Closure.
bool is(op o) const
Definition: formula.hh:168
bool is_psl_formula() const
Definition: formula.hh:402
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1278
bool is_leaf() const
Definition: formula.hh:238
bool is_finite() const
Definition: formula.hh:414
bool is_eword() const
Definition: formula.hh:300
unsigned boolean_count() const
Definition: formula.hh:337
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:829
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:712
static formula tt()
Return the true constant.
Definition: formula.hh:1388
const fnode * get_child_of(op o) const
Definition: formula.hh:193
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1270
Definition: formula.hh:1703
Empty word.
bool is_syntactic_guarantee() const
Definition: formula.hh:438
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1382
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1446
static const fnode * tt()
Definition: formula.hh:282
bool is_syntactic_persistence() const
Definition: formula.hh:456
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:932
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:927
const fnode * nth(unsigned i) const
Definition: formula.hh:262
bool is_marked() const
Definition: formula.hh:462
Concatenation.
bool is_syntactic_recurrence() const
Definition: formula.hh:450
bool is(std::initializer_list< op > l) const
Definition: formula.hh:180
Main class for temporal logic formula.
Definition: formula.hh:682
bool is_syntactic_obligation() const
Definition: formula.hh:444
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:174
bool has_spin_atomic_props() const
Definition: formula.hh:480
release (dual of until)
bool is_constant() const
Definition: formula.hh:306
unsigned size() const
Return the number of children.
Definition: formula.hh:1284
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1434
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:856
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:384
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:1234
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1421
size_t id() const
Return the id of a formula.
Definition: formula.hh:1306
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1221
void destroy() const
Dereference an fnode.
Definition: formula.hh:131
static formula ff()
Return the false constant.
Definition: formula.hh:1376
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:1037
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:270
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:1406
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:1115
static const fnode * one_star()
Definition: formula.hh:320
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:700
bool is_syntactic_safety() const
Definition: formula.hh:432
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1215
Exclusive Or.
marked version of the Negated PSL Closure
bool is_sugar_free_boolean() const
Definition: formula.hh:372
static formula eword()
Return the empty word constant.
Definition: formula.hh:1400
bool is_ltl_formula() const
Definition: formula.hh:396
Definition: formula.hh:610
bool is_in_nenoform() const
Definition: formula.hh:378
bool is_ff() const
Definition: formula.hh:276
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1394
(omega-Rational) Or
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:690
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:823
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:203
static constexpr uint8_t unbounded()
Definition: formula.hh:141
unsigned size() const
Definition: formula.hh:232
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:740
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:117
bool has_lbt_atomic_props() const
Definition: formula.hh:474
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1369
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1200
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:839
bool is_sugar_free_ltl() const
Definition: formula.hh:390
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:408
op
Operator types.
Definition: formula.hh:65
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:850
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1293
bool is_tt() const
Definition: formula.hh:288
const fnode *const * end() const
Definition: formula.hh:256
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:1107
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1243
Implication.
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1479
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1674
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:159
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1363
bool is_eventual() const
Definition: formula.hh:420
unsigned min() const
Definition: formula.hh:216
bool is_universal() const
Definition: formula.hh:426
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1497
Negated PSL Closure.
Rational And.
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1465
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:921
op kind() const
Return top-most operator.
Definition: formula.hh:1209
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:468
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:312
Atomic proposition.
Eventually.
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:720
(omega-Rational) And
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1611
Rational Or.
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:706

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