spot  2.8.3
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
22 #pragma once
23 
30 
33 
36 
39 
42 
45 
46 #include <spot/misc/common.hh>
47 #include <memory>
48 #include <cstdint>
49 #include <initializer_list>
50 #include <cassert>
51 #include <vector>
52 #include <string>
53 #include <iterator>
54 #include <iosfwd>
55 #include <sstream>
56 #include <list>
57 #include <cstddef>
58 #include <limits>
59 
60 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  first_match,
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  static const fnode* nested_unop_range(op uo, op bo, unsigned min,
160  unsigned max, const fnode* f);
161 
163  op kind() const
164  {
165  return op_;
166  }
167 
169  std::string kindstr() const;
170 
172  bool is(op o) const
173  {
174  return op_ == o;
175  }
176 
178  bool is(op o1, op o2) const
179  {
180  return op_ == o1 || op_ == o2;
181  }
182 
184  bool is(std::initializer_list<op> l) const
185  {
186  const fnode* n = this;
187  for (auto o: l)
188  {
189  if (!n->is(o))
190  return false;
191  n = n->nth(0);
192  }
193  return true;
194  }
195 
197  const fnode* get_child_of(op o) const
198  {
199  if (op_ != o)
200  return nullptr;
201  if (SPOT_UNLIKELY(size_ != 1))
202  report_get_child_of_expecting_single_child_node();
203  return nth(0);
204  }
205 
207  const fnode* get_child_of(std::initializer_list<op> l) const
208  {
209  auto c = this;
210  for (auto o: l)
211  {
212  c = c->get_child_of(o);
213  if (c == nullptr)
214  return c;
215  }
216  return c;
217  }
218 
220  unsigned min() const
221  {
222  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
223  report_min_invalid_arg();
224  return min_;
225  }
226 
228  unsigned max() const
229  {
230  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
231  report_max_invalid_arg();
232  return max_;
233  }
234 
236  unsigned size() const
237  {
238  return size_;
239  }
240 
242  bool is_leaf() const
243  {
244  return size_ == 0;
245  }
246 
248  size_t id() const
249  {
250  return id_;
251  }
252 
254  const fnode*const* begin() const
255  {
256  return children;
257  }
258 
260  const fnode*const* end() const
261  {
262  return children + size();
263  }
264 
266  const fnode* nth(unsigned i) const
267  {
268  if (SPOT_UNLIKELY(i >= size()))
269  report_non_existing_child();
270  return children[i];
271  }
272 
274  static const fnode* ff()
275  {
276  return ff_;
277  }
278 
280  bool is_ff() const
281  {
282  return op_ == op::ff;
283  }
284 
286  static const fnode* tt()
287  {
288  return tt_;
289  }
290 
292  bool is_tt() const
293  {
294  return op_ == op::tt;
295  }
296 
298  static const fnode* eword()
299  {
300  return ew_;
301  }
302 
304  bool is_eword() const
305  {
306  return op_ == op::eword;
307  }
308 
310  bool is_constant() const
311  {
312  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
313  }
314 
316  bool is_Kleene_star() const
317  {
318  if (op_ != op::Star)
319  return false;
320  return min_ == 0 && max_ == unbounded();
321  }
322 
324  static const fnode* one_star()
325  {
326  if (!one_star_)
327  one_star_ = bunop(op::Star, tt(), 0);
328  return one_star_;
329  }
330 
332  const std::string& ap_name() const;
333 
335  std::ostream& dump(std::ostream& os) const;
336 
338  const fnode* all_but(unsigned i) const;
339 
341  unsigned boolean_count() const
342  {
343  unsigned pos = 0;
344  unsigned s = size();
345  while (pos < s && children[pos]->is_boolean())
346  ++pos;
347  return pos;
348  }
349 
351  const fnode* boolean_operands(unsigned* width = nullptr) const;
352 
363  static bool instances_check();
364 
366  // Properties //
368 
370  bool is_boolean() const
371  {
372  return is_.boolean;
373  }
374 
377  {
378  return is_.sugar_free_boolean;
379  }
380 
382  bool is_in_nenoform() const
383  {
384  return is_.in_nenoform;
385  }
386 
389  {
390  return is_.syntactic_si;
391  }
392 
394  bool is_sugar_free_ltl() const
395  {
396  return is_.sugar_free_ltl;
397  }
398 
400  bool is_ltl_formula() const
401  {
402  return is_.ltl_formula;
403  }
404 
406  bool is_psl_formula() const
407  {
408  return is_.psl_formula;
409  }
410 
412  bool is_sere_formula() const
413  {
414  return is_.sere_formula;
415  }
416 
418  bool is_finite() const
419  {
420  return is_.finite;
421  }
422 
424  bool is_eventual() const
425  {
426  return is_.eventual;
427  }
428 
430  bool is_universal() const
431  {
432  return is_.universal;
433  }
434 
436  bool is_syntactic_safety() const
437  {
438  return is_.syntactic_safety;
439  }
440 
443  {
444  return is_.syntactic_guarantee;
445  }
446 
449  {
450  return is_.syntactic_obligation;
451  }
452 
455  {
456  return is_.syntactic_recurrence;
457  }
458 
461  {
462  return is_.syntactic_persistence;
463  }
464 
466  bool is_marked() const
467  {
468  return !is_.not_marked;
469  }
470 
472  bool accepts_eword() const
473  {
474  return is_.accepting_eword;
475  }
476 
478  bool has_lbt_atomic_props() const
479  {
480  return is_.lbt_atomic_props;
481  }
482 
485  {
486  return is_.spin_atomic_props;
487  }
488 
489  private:
490  void setup_props(op o);
491  void destroy_aux() const;
492 
493  [[noreturn]] static void report_non_existing_child();
494  [[noreturn]] static void report_too_many_children();
495  [[noreturn]] static void
496  report_get_child_of_expecting_single_child_node();
497  [[noreturn]] static void report_min_invalid_arg();
498  [[noreturn]] static void report_max_invalid_arg();
499 
500  static const fnode* unique(fnode*);
501 
502  // Destruction may only happen via destroy().
503  ~fnode() = default;
504  // Disallow copies.
505  fnode(const fnode&) = delete;
506  fnode& operator=(const fnode&) = delete;
507 
508 
509 
510  template<class iter>
511  fnode(op o, iter begin, iter end)
512  // Clang has some optimization where is it able to combine the
513  // 4 movb initializing op_,min_,max_,saturated_ into a single
514  // movl. Also it can optimize the three byte-comparisons of
515  // is_Kleene_star() into a single masked 32-bit comparison.
516  // The latter optimization triggers warnings from valgrind if
517  // min_ and max_ are not initialized. So to benefit from the
518  // initialization optimization and the is_Kleene_star()
519  // optimization in Clang, we always initialize min_ and max_
520  // with this compiler. Do not do it the rest of the time,
521  // since the optimization is not done.
522  : op_(o),
523 #if __llvm__
524  min_(0), max_(0),
525 #endif
526  saturated_(0)
527  {
528  size_t s = std::distance(begin, end);
529  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
530  report_too_many_children();
531  size_ = s;
532  auto pos = children;
533  for (auto i = begin; i != end; ++i)
534  *pos++ = *i;
535  setup_props(o);
536  }
537 
538  fnode(op o, std::initializer_list<const fnode*> l)
539  : fnode(o, l.begin(), l.end())
540  {
541  }
542 
543  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
544  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
545  {
546  children[0] = f;
547  setup_props(o);
548  }
549 
550  static const fnode* ff_;
551  static const fnode* tt_;
552  static const fnode* ew_;
553  static const fnode* one_star_;
554 
555  op op_; // operator
556  uint8_t min_; // range minimum (for star-like operators)
557  uint8_t max_; // range maximum;
558  mutable uint8_t saturated_;
559  uint16_t size_; // number of children
560  mutable uint16_t refs_ = 0; // reference count - 1;
561  size_t id_; // Also used as hash.
562  static size_t next_id_;
563 
564  struct ltl_prop
565  {
566  // All properties here should be expressed in such a a way
567  // that property(f && g) is just property(f)&property(g).
568  // This allows us to compute all properties of a compound
569  // formula in one operation.
570  //
571  // For instance we do not use a property that says "has
572  // temporal operator", because it would require an OR between
573  // the two arguments. Instead we have a property that
574  // says "no temporal operator", and that one is computed
575  // with an AND between the arguments.
576  //
577  // Also choose a name that makes sense when prefixed with
578  // "the formula is".
579  bool boolean:1; // No temporal operators.
580  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
581  bool in_nenoform:1; // Negative Normal Form.
582  bool syntactic_si:1; // LTL-X or siPSL
583  bool sugar_free_ltl:1; // No F and G operators.
584  bool ltl_formula:1; // Only LTL operators.
585  bool psl_formula:1; // Only PSL operators.
586  bool sere_formula:1; // Only SERE operators.
587  bool finite:1; // Finite SERE formulae, or Bool+X forms.
588  bool eventual:1; // Purely eventual formula.
589  bool universal:1; // Purely universal formula.
590  bool syntactic_safety:1; // Syntactic Safety Property.
591  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
592  bool syntactic_obligation:1; // Syntactic Obligation Property.
593  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
594  bool syntactic_persistence:1; // Syntactic Persistence Property.
595  bool not_marked:1; // No occurrence of EConcatMarked.
596  bool accepting_eword:1; // Accepts the empty word.
597  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
598  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
599  };
600  union
601  {
602  // Use an unsigned for fast computation of all properties.
603  unsigned props;
604  ltl_prop is_;
605  };
606 
607  const fnode* children[1];
608  };
609 
611  SPOT_API
612  int atomic_prop_cmp(const fnode* f, const fnode* g);
613 
615  {
616  bool
617  operator()(const fnode* left, const fnode* right) const
618  {
619  SPOT_ASSERT(left);
620  SPOT_ASSERT(right);
621  if (left == right)
622  return false;
623 
624  // We want Boolean formulae first.
625  bool lib = left->is_boolean();
626  if (lib != right->is_boolean())
627  return lib;
628 
629  // We have two Boolean formulae
630  if (lib)
631  {
632  bool lconst = left->is_constant();
633  if (lconst != right->is_constant())
634  return lconst;
635  if (!lconst)
636  {
637  auto get_literal = [](const fnode* f) -> const fnode*
638  {
639  if (f->is(op::Not))
640  f = f->nth(0);
641  if (f->is(op::ap))
642  return f;
643  return nullptr;
644  };
645  // Literals should come first
646  const fnode* litl = get_literal(left);
647  const fnode* litr = get_literal(right);
648  if (!litl != !litr)
649  return litl;
650  if (litl)
651  {
652  // And they should be sorted alphabetically
653  int cmp = atomic_prop_cmp(litl, litr);
654  if (cmp)
655  return cmp < 0;
656  }
657  }
658  }
659 
660  size_t l = left->id();
661  size_t r = right->id();
662  if (l != r)
663  return l < r;
664  // Because the hash code assigned to each formula is the
665  // number of formulae constructed so far, it is very unlikely
666  // that we will ever reach a case were two different formulae
667  // have the same hash. This will happen only ever with have
668  // produced 256**sizeof(size_t) formulae (i.e. max_count has
669  // looped back to 0 and started over). In that case we can
670  // order two formulas by looking at their text representation.
671  // We could be more efficient and look at their AST, but it's
672  // not worth the burden. (Also ordering pointers is ruled out
673  // because it breaks the determinism of the implementation.)
674  std::ostringstream old;
675  left->dump(old);
676  std::ostringstream ord;
677  right->dump(ord);
678  return old.str() < ord.str();
679  }
680  };
681 
682 #endif // SWIG
683 
686  class SPOT_API formula final
687  {
688  const fnode* ptr_;
689  public:
694  explicit formula(const fnode* f) noexcept
695  : ptr_(f)
696  {
697  }
698 
704  formula(std::nullptr_t) noexcept
705  : ptr_(nullptr)
706  {
707  }
708 
710  formula() noexcept
711  : ptr_(nullptr)
712  {
713  }
714 
716  formula(const formula& f) noexcept
717  : ptr_(f.ptr_)
718  {
719  if (ptr_)
720  ptr_->clone();
721  }
722 
724  formula(formula&& f) noexcept
725  : ptr_(f.ptr_)
726  {
727  f.ptr_ = nullptr;
728  }
729 
732  {
733  if (ptr_)
734  ptr_->destroy();
735  }
736 
744  const formula& operator=(std::nullptr_t)
745  {
746  this->~formula();
747  ptr_ = nullptr;
748  return *this;
749  }
750 
751  const formula& operator=(const formula& f)
752  {
753  this->~formula();
754  if ((ptr_ = f.ptr_))
755  ptr_->clone();
756  return *this;
757  }
758 
759  const formula& operator=(formula&& f) noexcept
760  {
761  std::swap(f.ptr_, ptr_);
762  return *this;
763  }
764 
765  bool operator<(const formula& other) const noexcept
766  {
767  if (SPOT_UNLIKELY(!other.ptr_))
768  return false;
769  if (SPOT_UNLIKELY(!ptr_))
770  return true;
771  if (id() < other.id())
772  return true;
773  if (id() > other.id())
774  return false;
775  // The case where id()==other.id() but ptr_ != other.ptr_ is
776  // very unlikely (we would need to build more that UINT_MAX
777  // formulas), so let's just compare pointer, and ignore the fact
778  // that it may give some nondeterminism.
779  return ptr_ < other.ptr_;
780  }
781 
782  bool operator<=(const formula& other) const noexcept
783  {
784  return *this == other || *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 !(*this < other);
795  }
796 
797  bool operator==(const formula& other) const noexcept
798  {
799  return other.ptr_ == ptr_;
800  }
801 
802  bool operator==(std::nullptr_t) const noexcept
803  {
804  return ptr_ == nullptr;
805  }
806 
807  bool operator!=(const formula& other) const noexcept
808  {
809  return other.ptr_ != ptr_;
810  }
811 
812  bool operator!=(std::nullptr_t) const noexcept
813  {
814  return ptr_ != nullptr;
815  }
816 
817  operator bool() const
818  {
819  return ptr_ != nullptr;
820  }
821 
823  // Forwarded functions //
825 
827  static constexpr uint8_t unbounded()
828  {
829  return fnode::unbounded();
830  }
831 
833  static formula ap(const std::string& name)
834  {
835  return formula(fnode::ap(name));
836  }
837 
843  static formula ap(const formula& a)
844  {
845  if (SPOT_UNLIKELY(a.kind() != op::ap))
846  report_ap_invalid_arg();
847  return a;
848  }
849 
854  static formula unop(op o, const formula& f)
855  {
856  return formula(fnode::unop(o, f.ptr_->clone()));
857  }
858 
859 #ifndef SWIG
860  static formula unop(op o, formula&& f)
861  {
862  return formula(fnode::unop(o, f.to_node_()));
863  }
864 #endif // !SWIG
865 
867 #ifdef SWIG
868 #define SPOT_DEF_UNOP(Name) \
869  static formula Name(const formula& f) \
870  { \
871  return unop(op::Name, f); \
872  }
873 #else // !SWIG
874 #define SPOT_DEF_UNOP(Name) \
875  static formula Name(const formula& f) \
876  { \
877  return unop(op::Name, f); \
878  } \
879  static formula Name(formula&& f) \
880  { \
881  return unop(op::Name, std::move(f)); \
882  }
883 #endif // !SWIG
884  SPOT_DEF_UNOP(Not);
888 
891  SPOT_DEF_UNOP(X);
893 
897  static formula X(unsigned level, const formula& f)
898  {
899  return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
900  }
901 
904  SPOT_DEF_UNOP(F);
906 
913  static formula F(unsigned min_level, unsigned max_level, const formula& f)
914  {
915  return nested_unop_range(op::X, op::Or, min_level, max_level, f);
916  }
917 
924  static formula G(unsigned min_level, unsigned max_level, const formula& f)
925  {
926  return nested_unop_range(op::X, op::And, min_level, max_level, f);
927  }
928 
931  SPOT_DEF_UNOP(G);
933 
936  SPOT_DEF_UNOP(Closure);
938 
941  SPOT_DEF_UNOP(NegClosure);
943 
946  SPOT_DEF_UNOP(NegClosureMarked);
948 
951  SPOT_DEF_UNOP(first_match);
953 #undef SPOT_DEF_UNOP
954 
960  static formula binop(op o, const formula& f, const formula& g)
961  {
962  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
963  }
964 
965 #ifndef SWIG
966  static formula binop(op o, const formula& f, formula&& g)
967  {
968  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
969  }
970 
971  static formula binop(op o, formula&& f, const formula& g)
972  {
973  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
974  }
975 
976  static formula binop(op o, formula&& f, formula&& g)
977  {
978  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
979  }
981 
982 #endif //SWIG
983 
984 #ifdef SWIG
985 #define SPOT_DEF_BINOP(Name) \
986  static formula Name(const formula& f, const formula& g) \
987  { \
988  return binop(op::Name, f, g); \
989  }
990 #else // !SWIG
991 #define SPOT_DEF_BINOP(Name) \
992  static formula Name(const formula& f, const formula& g) \
993  { \
994  return binop(op::Name, f, g); \
995  } \
996  static formula Name(const formula& f, formula&& g) \
997  { \
998  return binop(op::Name, f, std::move(g)); \
999  } \
1000  static formula Name(formula&& f, const formula& g) \
1001  { \
1002  return binop(op::Name, std::move(f), g); \
1003  } \
1004  static formula Name(formula&& f, formula&& g) \
1005  { \
1006  return binop(op::Name, std::move(f), std::move(g)); \
1007  }
1008 #endif // !SWIG
1009  SPOT_DEF_BINOP(Xor);
1013 
1016  SPOT_DEF_BINOP(Implies);
1018 
1021  SPOT_DEF_BINOP(Equiv);
1023 
1026  SPOT_DEF_BINOP(U);
1028 
1031  SPOT_DEF_BINOP(R);
1033 
1036  SPOT_DEF_BINOP(W);
1038 
1041  SPOT_DEF_BINOP(M);
1043 
1046  SPOT_DEF_BINOP(EConcat);
1048 
1051  SPOT_DEF_BINOP(EConcatMarked);
1053 
1056  SPOT_DEF_BINOP(UConcat);
1058 #undef SPOT_DEF_BINOP
1059 
1065  static formula multop(op o, const std::vector<formula>& l)
1066  {
1067  std::vector<const fnode*> tmp;
1068  tmp.reserve(l.size());
1069  for (auto f: l)
1070  if (f.ptr_)
1071  tmp.emplace_back(f.ptr_->clone());
1072  return formula(fnode::multop(o, std::move(tmp)));
1073  }
1074 
1075 #ifndef SWIG
1076  static formula multop(op o, std::vector<formula>&& l)
1077  {
1078  std::vector<const fnode*> tmp;
1079  tmp.reserve(l.size());
1080  for (auto f: l)
1081  if (f.ptr_)
1082  tmp.emplace_back(f.to_node_());
1083  return formula(fnode::multop(o, std::move(tmp)));
1084  }
1085 #endif // !SWIG
1086 
1088 #ifdef SWIG
1089 #define SPOT_DEF_MULTOP(Name) \
1090  static formula Name(const std::vector<formula>& l) \
1091  { \
1092  return multop(op::Name, l); \
1093  }
1094 #else // !SWIG
1095 #define SPOT_DEF_MULTOP(Name) \
1096  static formula Name(const std::vector<formula>& l) \
1097  { \
1098  return multop(op::Name, l); \
1099  } \
1100  \
1101  static formula Name(std::vector<formula>&& l) \
1102  { \
1103  return multop(op::Name, std::move(l)); \
1104  }
1105 #endif // !SWIG
1106  SPOT_DEF_MULTOP(Or);
1110 
1113  SPOT_DEF_MULTOP(OrRat);
1115 
1118  SPOT_DEF_MULTOP(And);
1120 
1123  SPOT_DEF_MULTOP(AndRat);
1125 
1128  SPOT_DEF_MULTOP(AndNLM);
1130 
1133  SPOT_DEF_MULTOP(Concat);
1135 
1138  SPOT_DEF_MULTOP(Fusion);
1140 #undef SPOT_DEF_MULTOP
1141 
1146  static formula bunop(op o, const formula& f,
1147  uint8_t min = 0U,
1148  uint8_t max = unbounded())
1149  {
1150  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1151  }
1152 
1153 #ifndef SWIG
1154  static formula bunop(op o, formula&& f,
1155  uint8_t min = 0U,
1156  uint8_t max = unbounded())
1157  {
1158  return formula(fnode::bunop(o, f.to_node_(), min, max));
1159  }
1160 #endif // !SWIG
1161 
1163 #if SWIG
1164 #define SPOT_DEF_BUNOP(Name) \
1165  static formula Name(const formula& f, \
1166  uint8_t min = 0U, \
1167  uint8_t max = unbounded()) \
1168  { \
1169  return bunop(op::Name, f, min, max); \
1170  }
1171 #else // !SWIG
1172 #define SPOT_DEF_BUNOP(Name) \
1173  static formula Name(const formula& f, \
1174  uint8_t min = 0U, \
1175  uint8_t max = unbounded()) \
1176  { \
1177  return bunop(op::Name, f, min, max); \
1178  } \
1179  static formula Name(formula&& f, \
1180  uint8_t min = 0U, \
1181  uint8_t max = unbounded()) \
1182  { \
1183  return bunop(op::Name, std::move(f), min, max); \
1184  }
1185 #endif
1186  SPOT_DEF_BUNOP(Star);
1190 
1196  SPOT_DEF_BUNOP(FStar);
1198 #undef SPOT_DEF_BUNOP
1199 
1211  static const formula nested_unop_range(op uo, op bo, unsigned min,
1212  unsigned max, formula f)
1213  {
1214  return formula(fnode::nested_unop_range(uo, bo, min, max,
1215  f.ptr_->clone()));
1216  }
1217 
1223  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1224 
1230  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1231 
1253  static formula sugar_delay(const formula& a, const formula& b,
1254  unsigned min, unsigned max);
1255  static formula sugar_delay(const formula& b,
1256  unsigned min, unsigned max);
1258 
1259 #ifndef SWIG
1260  const fnode* to_node_()
1270  {
1271  auto tmp = ptr_;
1272  ptr_ = nullptr;
1273  return tmp;
1274  }
1275 #endif
1276 
1278  op kind() const
1279  {
1280  return ptr_->kind();
1281  }
1282 
1284  std::string kindstr() const
1285  {
1286  return ptr_->kindstr();
1287  }
1288 
1290  bool is(op o) const
1291  {
1292  return ptr_->is(o);
1293  }
1294 
1295 #ifndef SWIG
1296  bool is(op o1, op o2) const
1298  {
1299  return ptr_->is(o1, o2);
1300  }
1301 
1303  bool is(std::initializer_list<op> l) const
1304  {
1305  return ptr_->is(l);
1306  }
1307 #endif
1308 
1313  {
1314  auto f = ptr_->get_child_of(o);
1315  if (f)
1316  f->clone();
1317  return formula(f);
1318  }
1319 
1320 #ifndef SWIG
1321  formula get_child_of(std::initializer_list<op> l) const
1328  {
1329  auto f = ptr_->get_child_of(l);
1330  if (f)
1331  f->clone();
1332  return formula(f);
1333  }
1334 #endif
1335 
1339  unsigned min() const
1340  {
1341  return ptr_->min();
1342  }
1343 
1347  unsigned max() const
1348  {
1349  return ptr_->max();
1350  }
1351 
1353  unsigned size() const
1354  {
1355  return ptr_->size();
1356  }
1357 
1362  bool is_leaf() const
1363  {
1364  return ptr_->is_leaf();
1365  }
1366 
1375  size_t id() const
1376  {
1377  return ptr_->id();
1378  }
1379 
1380 #ifndef SWIG
1381  class SPOT_API formula_child_iterator final
1383  {
1384  const fnode*const* ptr_;
1385  public:
1386  formula_child_iterator()
1387  : ptr_(nullptr)
1388  {
1389  }
1390 
1391  formula_child_iterator(const fnode*const* f)
1392  : ptr_(f)
1393  {
1394  }
1395 
1396  bool operator==(formula_child_iterator o)
1397  {
1398  return ptr_ == o.ptr_;
1399  }
1400 
1401  bool operator!=(formula_child_iterator o)
1402  {
1403  return ptr_ != o.ptr_;
1404  }
1405 
1406  formula operator*()
1407  {
1408  return formula((*ptr_)->clone());
1409  }
1410 
1411  formula_child_iterator operator++()
1412  {
1413  ++ptr_;
1414  return *this;
1415  }
1416 
1417  formula_child_iterator operator++(int)
1418  {
1419  auto tmp = *this;
1420  ++ptr_;
1421  return tmp;
1422  }
1423  };
1424 
1426  formula_child_iterator begin() const
1427  {
1428  return ptr_->begin();
1429  }
1430 
1432  formula_child_iterator end() const
1433  {
1434  return ptr_->end();
1435  }
1436 
1438  formula operator[](unsigned i) const
1439  {
1440  return formula(ptr_->nth(i)->clone());
1441  }
1442 #endif
1443 
1445  static formula ff()
1446  {
1447  return formula(fnode::ff());
1448  }
1449 
1451  bool is_ff() const
1452  {
1453  return ptr_->is_ff();
1454  }
1455 
1457  static formula tt()
1458  {
1459  return formula(fnode::tt());
1460  }
1461 
1463  bool is_tt() const
1464  {
1465  return ptr_->is_tt();
1466  }
1467 
1469  static formula eword()
1470  {
1471  return formula(fnode::eword());
1472  }
1473 
1475  bool is_eword() const
1476  {
1477  return ptr_->is_eword();
1478  }
1479 
1481  bool is_constant() const
1482  {
1483  return ptr_->is_constant();
1484  }
1485 
1490  bool is_Kleene_star() const
1491  {
1492  return ptr_->is_Kleene_star();
1493  }
1494 
1497  {
1498  return formula(fnode::one_star()->clone());
1499  }
1500 
1503  bool is_literal()
1504  {
1505  return (is(op::ap) ||
1506  // If f is in nenoform, Not can only occur in front of
1507  // an atomic proposition. So this way we do not have
1508  // to check the type of the child.
1509  (is(op::Not) && is_boolean() && is_in_nenoform()));
1510  }
1511 
1515  const std::string& ap_name() const
1516  {
1517  return ptr_->ap_name();
1518  }
1519 
1524  std::ostream& dump(std::ostream& os) const
1525  {
1526  return ptr_->dump(os);
1527  }
1528 
1534  formula all_but(unsigned i) const
1535  {
1536  return formula(ptr_->all_but(i));
1537  }
1538 
1548  unsigned boolean_count() const
1549  {
1550  return ptr_->boolean_count();
1551  }
1552 
1566  formula boolean_operands(unsigned* width = nullptr) const
1567  {
1568  return formula(ptr_->boolean_operands(width));
1569  }
1570 
1571 #define SPOT_DEF_PROP(Name) \
1572  bool Name() const \
1573  { \
1574  return ptr_->Name(); \
1575  }
1576  // Properties //
1579 
1581  SPOT_DEF_PROP(is_boolean);
1583  SPOT_DEF_PROP(is_sugar_free_boolean);
1588  SPOT_DEF_PROP(is_in_nenoform);
1590  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1592  SPOT_DEF_PROP(is_sugar_free_ltl);
1594  SPOT_DEF_PROP(is_ltl_formula);
1596  SPOT_DEF_PROP(is_psl_formula);
1598  SPOT_DEF_PROP(is_sere_formula);
1601  SPOT_DEF_PROP(is_finite);
1609  SPOT_DEF_PROP(is_eventual);
1617  SPOT_DEF_PROP(is_universal);
1619  SPOT_DEF_PROP(is_syntactic_safety);
1621  SPOT_DEF_PROP(is_syntactic_guarantee);
1623  SPOT_DEF_PROP(is_syntactic_obligation);
1625  SPOT_DEF_PROP(is_syntactic_recurrence);
1627  SPOT_DEF_PROP(is_syntactic_persistence);
1630  SPOT_DEF_PROP(is_marked);
1632  SPOT_DEF_PROP(accepts_eword);
1638  SPOT_DEF_PROP(has_lbt_atomic_props);
1647  SPOT_DEF_PROP(has_spin_atomic_props);
1648 #undef SPOT_DEF_PROP
1649 
1653  template<typename Trans, typename... Args>
1654  formula map(Trans trans, Args&&... args)
1655  {
1656  switch (op o = kind())
1657  {
1658  case op::ff:
1659  case op::tt:
1660  case op::eword:
1661  case op::ap:
1662  return *this;
1663  case op::Not:
1664  case op::X:
1665  case op::F:
1666  case op::G:
1667  case op::Closure:
1668  case op::NegClosure:
1669  case op::NegClosureMarked:
1670  case op::first_match:
1671  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1672  case op::Xor:
1673  case op::Implies:
1674  case op::Equiv:
1675  case op::U:
1676  case op::R:
1677  case op::W:
1678  case op::M:
1679  case op::EConcat:
1680  case op::EConcatMarked:
1681  case op::UConcat:
1682  {
1683  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1684  return binop(o, tmp,
1685  trans((*this)[1], std::forward<Args>(args)...));
1686  }
1687  case op::Or:
1688  case op::OrRat:
1689  case op::And:
1690  case op::AndRat:
1691  case op::AndNLM:
1692  case op::Concat:
1693  case op::Fusion:
1694  {
1695  std::vector<formula> tmp;
1696  tmp.reserve(size());
1697  for (auto f: *this)
1698  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1699  return multop(o, std::move(tmp));
1700  }
1701  case op::Star:
1702  case op::FStar:
1703  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1704  min(), max());
1705  }
1706  SPOT_UNREACHABLE();
1707  }
1708 
1717  template<typename Func, typename... Args>
1718  void traverse(Func func, Args&&... args)
1719  {
1720  if (func(*this, std::forward<Args>(args)...))
1721  return;
1722  for (auto f: *this)
1723  f.traverse(func, std::forward<Args>(args)...);
1724  }
1725 
1726  private:
1727 #ifndef SWIG
1728  [[noreturn]] static void report_ap_invalid_arg();
1729 #endif
1730  };
1731 
1733  SPOT_API
1734  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1735  bool abbreviated = false);
1736 
1738  SPOT_API
1739  std::list<std::string> list_formula_props(const formula& f);
1740 
1742  SPOT_API
1743  std::ostream& operator<<(std::ostream& os, const formula& f);
1744 }
1745 
1746 #ifndef SWIG
1747 namespace std
1748 {
1749  template <>
1750  struct hash<spot::formula>
1751  {
1752  size_t operator()(const spot::formula& x) const noexcept
1753  {
1754  return x.id();
1755  }
1756  };
1757 }
1758 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1065
const fnode *const * begin() const
Definition: formula.hh:254
Definition: automata.hh:26
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1496
~formula()
Destroy a formula.
Definition: formula.hh:731
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:976
bool is_boolean() const
Definition: formula.hh:370
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1426
static const fnode * eword()
Definition: formula.hh:298
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:1481
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1524
unsigned max() const
Definition: formula.hh:228
size_t id() const
Definition: formula.hh:248
PSL Closure.
bool is(op o) const
Definition: formula.hh:172
bool is_psl_formula() const
Definition: formula.hh:406
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1347
bool is_leaf() const
Definition: formula.hh:242
bool is_finite() const
Definition: formula.hh:418
bool is_eword() const
Definition: formula.hh:304
unsigned boolean_count() const
Definition: formula.hh:341
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:833
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition: formula.hh:913
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:716
static formula tt()
Return the true constant.
Definition: formula.hh:1457
const fnode * get_child_of(op o) const
Definition: formula.hh:197
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition: formula.hh:924
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1339
Definition: bitset.hh:405
Empty word.
bool is_syntactic_guarantee() const
Definition: formula.hh:442
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1451
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1515
static const fnode * tt()
Definition: formula.hh:286
bool is_syntactic_persistence() const
Definition: formula.hh:460
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:971
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:966
const fnode * nth(unsigned i) const
Definition: formula.hh:266
bool is_marked() const
Definition: formula.hh:466
Concatenation.
bool is_syntactic_recurrence() const
Definition: formula.hh:454
bool is(std::initializer_list< op > l) const
Definition: formula.hh:184
Main class for temporal logic formula.
Definition: formula.hh:686
bool is_syntactic_obligation() const
Definition: formula.hh:448
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:178
bool has_spin_atomic_props() const
Definition: formula.hh:484
release (dual of until)
bool is_constant() const
Definition: formula.hh:310
unsigned size() const
Return the number of children.
Definition: formula.hh:1353
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1503
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:860
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:388
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:1303
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1490
size_t id() const
Return the id of a formula.
Definition: formula.hh:1375
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1290
void destroy() const
Dereference an fnode.
Definition: formula.hh:131
static formula ff()
Return the false constant.
Definition: formula.hh:1445
std::list< std::string > list_formula_props(const formula &f)
List the properties of formula f.
static const formula nested_unop_range(op uo, op bo, unsigned min, unsigned max, formula f)
Nested operator construction (syntactic sugar).
Definition: formula.hh:1211
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1076
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:274
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:1475
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:1154
static const fnode * one_star()
Definition: formula.hh:324
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:704
bool is_syntactic_safety() const
Definition: formula.hh:436
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1284
Exclusive Or.
marked version of the Negated PSL Closure
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition: formula.hh:897
bool is_sugar_free_boolean() const
Definition: formula.hh:376
static formula eword()
Return the empty word constant.
Definition: formula.hh:1469
bool is_ltl_formula() const
Definition: formula.hh:400
Definition: formula.hh:614
bool is_in_nenoform() const
Definition: formula.hh:382
first_match(sere)
bool is_ff() const
Definition: formula.hh:280
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1463
(omega-Rational) Or
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:694
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:827
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:207
static constexpr uint8_t unbounded()
Definition: formula.hh:141
unsigned size() const
Definition: formula.hh:236
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:744
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:117
bool has_lbt_atomic_props() const
Definition: formula.hh:478
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1438
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1269
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:843
bool is_sugar_free_ltl() const
Definition: formula.hh:394
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:412
op
Operator types.
Definition: formula.hh:64
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:854
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1362
bool is_tt() const
Definition: formula.hh:292
const fnode *const * end() const
Definition: formula.hh:260
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:1146
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1312
Implication.
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1548
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1718
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:163
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1432
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
bool is_eventual() const
Definition: formula.hh:424
unsigned min() const
Definition: formula.hh:220
bool is_universal() const
Definition: formula.hh:430
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1566
Negated PSL Closure.
Rational And.
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1534
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:960
op kind() const
Return top-most operator.
Definition: formula.hh:1278
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:472
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:316
Atomic proposition.
Eventually.
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:724
(omega-Rational) And
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1654
Rational Or.
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:710

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