spot  2.7
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015-2018 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  };
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  static const fnode* nested_unop_range(op uo, op bo, unsigned min,
159  unsigned max, const fnode* f);
160 
162  op kind() const
163  {
164  return op_;
165  }
166 
168  std::string kindstr() const;
169 
171  bool is(op o) const
172  {
173  return op_ == o;
174  }
175 
177  bool is(op o1, op o2) const
178  {
179  return op_ == o1 || op_ == o2;
180  }
181 
183  bool is(std::initializer_list<op> l) const
184  {
185  const fnode* n = this;
186  for (auto o: l)
187  {
188  if (!n->is(o))
189  return false;
190  n = n->nth(0);
191  }
192  return true;
193  }
194 
196  const fnode* get_child_of(op o) const
197  {
198  if (op_ != o)
199  return nullptr;
200  if (SPOT_UNLIKELY(size_ != 1))
201  report_get_child_of_expecting_single_child_node();
202  return nth(0);
203  }
204 
206  const fnode* get_child_of(std::initializer_list<op> l) const
207  {
208  auto c = this;
209  for (auto o: l)
210  {
211  c = c->get_child_of(o);
212  if (c == nullptr)
213  return c;
214  }
215  return c;
216  }
217 
219  unsigned min() const
220  {
221  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
222  report_min_invalid_arg();
223  return min_;
224  }
225 
227  unsigned max() const
228  {
229  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
230  report_max_invalid_arg();
231  return max_;
232  }
233 
235  unsigned size() const
236  {
237  return size_;
238  }
239 
241  bool is_leaf() const
242  {
243  return size_ == 0;
244  }
245 
247  size_t id() const
248  {
249  return id_;
250  }
251 
253  const fnode*const* begin() const
254  {
255  return children;
256  }
257 
259  const fnode*const* end() const
260  {
261  return children + size();
262  }
263 
265  const fnode* nth(unsigned i) const
266  {
267  if (SPOT_UNLIKELY(i >= size()))
268  report_non_existing_child();
269  return children[i];
270  }
271 
273  static const fnode* ff()
274  {
275  return ff_;
276  }
277 
279  bool is_ff() const
280  {
281  return op_ == op::ff;
282  }
283 
285  static const fnode* tt()
286  {
287  return tt_;
288  }
289 
291  bool is_tt() const
292  {
293  return op_ == op::tt;
294  }
295 
297  static const fnode* eword()
298  {
299  return ew_;
300  }
301 
303  bool is_eword() const
304  {
305  return op_ == op::eword;
306  }
307 
309  bool is_constant() const
310  {
311  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
312  }
313 
315  bool is_Kleene_star() const
316  {
317  if (op_ != op::Star)
318  return false;
319  return min_ == 0 && max_ == unbounded();
320  }
321 
323  static const fnode* one_star()
324  {
325  if (!one_star_)
326  one_star_ = bunop(op::Star, tt(), 0);
327  return one_star_;
328  }
329 
331  const std::string& ap_name() const;
332 
334  std::ostream& dump(std::ostream& os) const;
335 
337  const fnode* all_but(unsigned i) const;
338 
340  unsigned boolean_count() const
341  {
342  unsigned pos = 0;
343  unsigned s = size();
344  while (pos < s && children[pos]->is_boolean())
345  ++pos;
346  return pos;
347  }
348 
350  const fnode* boolean_operands(unsigned* width = nullptr) const;
351 
362  static bool instances_check();
363 
365  // Properties //
367 
369  bool is_boolean() const
370  {
371  return is_.boolean;
372  }
373 
376  {
377  return is_.sugar_free_boolean;
378  }
379 
381  bool is_in_nenoform() const
382  {
383  return is_.in_nenoform;
384  }
385 
388  {
389  return is_.syntactic_si;
390  }
391 
393  bool is_sugar_free_ltl() const
394  {
395  return is_.sugar_free_ltl;
396  }
397 
399  bool is_ltl_formula() const
400  {
401  return is_.ltl_formula;
402  }
403 
405  bool is_psl_formula() const
406  {
407  return is_.psl_formula;
408  }
409 
411  bool is_sere_formula() const
412  {
413  return is_.sere_formula;
414  }
415 
417  bool is_finite() const
418  {
419  return is_.finite;
420  }
421 
423  bool is_eventual() const
424  {
425  return is_.eventual;
426  }
427 
429  bool is_universal() const
430  {
431  return is_.universal;
432  }
433 
435  bool is_syntactic_safety() const
436  {
437  return is_.syntactic_safety;
438  }
439 
442  {
443  return is_.syntactic_guarantee;
444  }
445 
448  {
449  return is_.syntactic_obligation;
450  }
451 
454  {
455  return is_.syntactic_recurrence;
456  }
457 
460  {
461  return is_.syntactic_persistence;
462  }
463 
465  bool is_marked() const
466  {
467  return !is_.not_marked;
468  }
469 
471  bool accepts_eword() const
472  {
473  return is_.accepting_eword;
474  }
475 
477  bool has_lbt_atomic_props() const
478  {
479  return is_.lbt_atomic_props;
480  }
481 
484  {
485  return is_.spin_atomic_props;
486  }
487 
488  private:
489  void setup_props(op o);
490  void destroy_aux() const;
491 
492  [[noreturn]] static void report_non_existing_child();
493  [[noreturn]] static void report_too_many_children();
494  [[noreturn]] static void
495  report_get_child_of_expecting_single_child_node();
496  [[noreturn]] static void report_min_invalid_arg();
497  [[noreturn]] static void report_max_invalid_arg();
498 
499  static const fnode* unique(fnode*);
500 
501  // Destruction may only happen via destroy().
502  ~fnode() = default;
503  // Disallow copies.
504  fnode(const fnode&) = delete;
505  fnode& operator=(const fnode&) = delete;
506 
507 
508 
509  template<class iter>
510  fnode(op o, iter begin, iter end)
511  // Clang has some optimization where is it able to combine the
512  // 4 movb initializing op_,min_,max_,saturated_ into a single
513  // movl. Also it can optimize the three byte-comparisons of
514  // is_Kleene_star() into a single masked 32-bit comparison.
515  // The latter optimization triggers warnings from valgrind if
516  // min_ and max_ are not initialized. So to benefit from the
517  // initialization optimization and the is_Kleene_star()
518  // optimization in Clang, we always initialize min_ and max_
519  // with this compiler. Do not do it the rest of the time,
520  // since the optimization is not done.
521  : op_(o),
522 #if __llvm__
523  min_(0), max_(0),
524 #endif
525  saturated_(0)
526  {
527  size_t s = std::distance(begin, end);
528  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
529  report_too_many_children();
530  size_ = s;
531  auto pos = children;
532  for (auto i = begin; i != end; ++i)
533  *pos++ = *i;
534  setup_props(o);
535  }
536 
537  fnode(op o, std::initializer_list<const fnode*> l)
538  : fnode(o, l.begin(), l.end())
539  {
540  }
541 
542  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
543  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
544  {
545  children[0] = f;
546  setup_props(o);
547  }
548 
549  static const fnode* ff_;
550  static const fnode* tt_;
551  static const fnode* ew_;
552  static const fnode* one_star_;
553 
554  op op_; // operator
555  uint8_t min_; // range minimum (for star-like operators)
556  uint8_t max_; // range maximum;
557  mutable uint8_t saturated_;
558  uint16_t size_; // number of children
559  mutable uint16_t refs_ = 0; // reference count - 1;
560  size_t id_; // Also used as hash.
561  static size_t next_id_;
562 
563  struct ltl_prop
564  {
565  // All properties here should be expressed in such a a way
566  // that property(f && g) is just property(f)&property(g).
567  // This allows us to compute all properties of a compound
568  // formula in one operation.
569  //
570  // For instance we do not use a property that says "has
571  // temporal operator", because it would require an OR between
572  // the two arguments. Instead we have a property that
573  // says "no temporal operator", and that one is computed
574  // with an AND between the arguments.
575  //
576  // Also choose a name that makes sense when prefixed with
577  // "the formula is".
578  bool boolean:1; // No temporal operators.
579  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
580  bool in_nenoform:1; // Negative Normal Form.
581  bool syntactic_si:1; // LTL-X or siPSL
582  bool sugar_free_ltl:1; // No F and G operators.
583  bool ltl_formula:1; // Only LTL operators.
584  bool psl_formula:1; // Only PSL operators.
585  bool sere_formula:1; // Only SERE operators.
586  bool finite:1; // Finite SERE formulae, or Bool+X forms.
587  bool eventual:1; // Purely eventual formula.
588  bool universal:1; // Purely universal formula.
589  bool syntactic_safety:1; // Syntactic Safety Property.
590  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
591  bool syntactic_obligation:1; // Syntactic Obligation Property.
592  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
593  bool syntactic_persistence:1; // Syntactic Persistence Property.
594  bool not_marked:1; // No occurrence of EConcatMarked.
595  bool accepting_eword:1; // Accepts the empty word.
596  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
597  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
598  };
599  union
600  {
601  // Use an unsigned for fast computation of all properties.
602  unsigned props;
603  ltl_prop is_;
604  };
605 
606  const fnode* children[1];
607  };
608 
610  SPOT_API
611  int atomic_prop_cmp(const fnode* f, const fnode* g);
612 
614  {
615  bool
616  operator()(const fnode* left, const fnode* right) const
617  {
618  SPOT_ASSERT(left);
619  SPOT_ASSERT(right);
620  if (left == right)
621  return false;
622 
623  // We want Boolean formulae first.
624  bool lib = left->is_boolean();
625  if (lib != right->is_boolean())
626  return lib;
627 
628  // We have two Boolean formulae
629  if (lib)
630  {
631  bool lconst = left->is_constant();
632  if (lconst != right->is_constant())
633  return lconst;
634  if (!lconst)
635  {
636  auto get_literal = [](const fnode* f) -> const fnode*
637  {
638  if (f->is(op::Not))
639  f = f->nth(0);
640  if (f->is(op::ap))
641  return f;
642  return nullptr;
643  };
644  // Literals should come first
645  const fnode* litl = get_literal(left);
646  const fnode* litr = get_literal(right);
647  if (!litl != !litr)
648  return litl;
649  if (litl)
650  {
651  // And they should be sorted alphabetically
652  int cmp = atomic_prop_cmp(litl, litr);
653  if (cmp)
654  return cmp < 0;
655  }
656  }
657  }
658 
659  size_t l = left->id();
660  size_t r = right->id();
661  if (l != r)
662  return l < r;
663  // Because the hash code assigned to each formula is the
664  // number of formulae constructed so far, it is very unlikely
665  // that we will ever reach a case were two different formulae
666  // have the same hash. This will happen only ever with have
667  // produced 256**sizeof(size_t) formulae (i.e. max_count has
668  // looped back to 0 and started over). In that case we can
669  // order two formulas by looking at their text representation.
670  // We could be more efficient and look at their AST, but it's
671  // not worth the burden. (Also ordering pointers is ruled out
672  // because it breaks the determinism of the implementation.)
673  std::ostringstream old;
674  left->dump(old);
675  std::ostringstream ord;
676  right->dump(ord);
677  return old.str() < ord.str();
678  }
679  };
680 
681 #endif // SWIG
682 
685  class SPOT_API formula final
686  {
687  const fnode* ptr_;
688  public:
693  explicit formula(const fnode* f) noexcept
694  : ptr_(f)
695  {
696  }
697 
703  formula(std::nullptr_t) noexcept
704  : ptr_(nullptr)
705  {
706  }
707 
709  formula() noexcept
710  : ptr_(nullptr)
711  {
712  }
713 
715  formula(const formula& f) noexcept
716  : ptr_(f.ptr_)
717  {
718  if (ptr_)
719  ptr_->clone();
720  }
721 
723  formula(formula&& f) noexcept
724  : ptr_(f.ptr_)
725  {
726  f.ptr_ = nullptr;
727  }
728 
731  {
732  if (ptr_)
733  ptr_->destroy();
734  }
735 
743  const formula& operator=(std::nullptr_t)
744  {
745  this->~formula();
746  ptr_ = nullptr;
747  return *this;
748  }
749 
750  const formula& operator=(const formula& f)
751  {
752  this->~formula();
753  if ((ptr_ = f.ptr_))
754  ptr_->clone();
755  return *this;
756  }
757 
758  const formula& operator=(formula&& f) noexcept
759  {
760  std::swap(f.ptr_, ptr_);
761  return *this;
762  }
763 
764  bool operator<(const formula& other) const noexcept
765  {
766  if (SPOT_UNLIKELY(!other.ptr_))
767  return false;
768  if (SPOT_UNLIKELY(!ptr_))
769  return true;
770  if (id() < other.id())
771  return true;
772  if (id() > other.id())
773  return false;
774  // The case where id()==other.id() but ptr_ != other.ptr_ is
775  // very unlikely (we would need to build more that UINT_MAX
776  // formulas), so let's just compare pointer, and ignore the fact
777  // that it may give some nondeterminism.
778  return ptr_ < other.ptr_;
779  }
780 
781  bool operator<=(const formula& other) const noexcept
782  {
783  return *this == other || *this < other;
784  }
785 
786  bool operator>(const formula& other) const noexcept
787  {
788  return !(*this <= other);
789  }
790 
791  bool operator>=(const formula& other) const noexcept
792  {
793  return !(*this < other);
794  }
795 
796  bool operator==(const formula& other) const noexcept
797  {
798  return other.ptr_ == ptr_;
799  }
800 
801  bool operator==(std::nullptr_t) const noexcept
802  {
803  return ptr_ == nullptr;
804  }
805 
806  bool operator!=(const formula& other) const noexcept
807  {
808  return other.ptr_ != ptr_;
809  }
810 
811  bool operator!=(std::nullptr_t) const noexcept
812  {
813  return ptr_ != nullptr;
814  }
815 
816  operator bool() const
817  {
818  return ptr_ != nullptr;
819  }
820 
822  // Forwarded functions //
824 
826  static constexpr uint8_t unbounded()
827  {
828  return fnode::unbounded();
829  }
830 
832  static formula ap(const std::string& name)
833  {
834  return formula(fnode::ap(name));
835  }
836 
842  static formula ap(const formula& a)
843  {
844  if (SPOT_UNLIKELY(a.kind() != op::ap))
845  report_ap_invalid_arg();
846  return a;
847  }
848 
853  static formula unop(op o, const formula& f)
854  {
855  return formula(fnode::unop(o, f.ptr_->clone()));
856  }
857 
858 #ifndef SWIG
859  static formula unop(op o, formula&& f)
860  {
861  return formula(fnode::unop(o, f.to_node_()));
862  }
863 #endif // !SWIG
864 
866 #ifdef SWIG
867 #define SPOT_DEF_UNOP(Name) \
868  static formula Name(const formula& f) \
869  { \
870  return unop(op::Name, f); \
871  }
872 #else // !SWIG
873 #define SPOT_DEF_UNOP(Name) \
874  static formula Name(const formula& f) \
875  { \
876  return unop(op::Name, f); \
877  } \
878  static formula Name(formula&& f) \
879  { \
880  return unop(op::Name, std::move(f)); \
881  }
882 #endif // !SWIG
883  SPOT_DEF_UNOP(Not);
887 
890  SPOT_DEF_UNOP(X);
892 
896  static formula X(unsigned level, const formula& f)
897  {
898  return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
899  }
900 
903  SPOT_DEF_UNOP(F);
905 
911  static formula F(unsigned min_level, unsigned max_level, const formula& f)
912  {
913  return nested_unop_range(op::X, op::Or, min_level, max_level, f);
914  }
915 
921  static formula G(unsigned min_level, unsigned max_level, const formula& f)
922  {
923  return nested_unop_range(op::X, op::And, min_level, max_level, f);
924  }
925 
928  SPOT_DEF_UNOP(G);
930 
933  SPOT_DEF_UNOP(Closure);
935 
938  SPOT_DEF_UNOP(NegClosure);
940 
943  SPOT_DEF_UNOP(NegClosureMarked);
945 #undef SPOT_DEF_UNOP
946 
952  static formula binop(op o, const formula& f, const formula& g)
953  {
954  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
955  }
956 
957 #ifndef SWIG
958  static formula binop(op o, const formula& f, formula&& g)
959  {
960  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
961  }
962 
963  static formula binop(op o, formula&& f, const formula& g)
964  {
965  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
966  }
967 
968  static formula binop(op o, formula&& f, formula&& g)
969  {
970  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
971  }
973 
974 #endif //SWIG
975 
976 #ifdef SWIG
977 #define SPOT_DEF_BINOP(Name) \
978  static formula Name(const formula& f, const formula& g) \
979  { \
980  return binop(op::Name, f, g); \
981  }
982 #else // !SWIG
983 #define SPOT_DEF_BINOP(Name) \
984  static formula Name(const formula& f, const formula& g) \
985  { \
986  return binop(op::Name, f, g); \
987  } \
988  static formula Name(const formula& f, formula&& g) \
989  { \
990  return binop(op::Name, f, std::move(g)); \
991  } \
992  static formula Name(formula&& f, const formula& g) \
993  { \
994  return binop(op::Name, std::move(f), g); \
995  } \
996  static formula Name(formula&& f, formula&& g) \
997  { \
998  return binop(op::Name, std::move(f), std::move(g)); \
999  }
1000 #endif // !SWIG
1001  SPOT_DEF_BINOP(Xor);
1005 
1008  SPOT_DEF_BINOP(Implies);
1010 
1013  SPOT_DEF_BINOP(Equiv);
1015 
1018  SPOT_DEF_BINOP(U);
1020 
1023  SPOT_DEF_BINOP(R);
1025 
1028  SPOT_DEF_BINOP(W);
1030 
1033  SPOT_DEF_BINOP(M);
1035 
1038  SPOT_DEF_BINOP(EConcat);
1040 
1043  SPOT_DEF_BINOP(EConcatMarked);
1045 
1048  SPOT_DEF_BINOP(UConcat);
1050 #undef SPOT_DEF_BINOP
1051 
1057  static formula multop(op o, const std::vector<formula>& l)
1058  {
1059  std::vector<const fnode*> tmp;
1060  tmp.reserve(l.size());
1061  for (auto f: l)
1062  if (f.ptr_)
1063  tmp.emplace_back(f.ptr_->clone());
1064  return formula(fnode::multop(o, std::move(tmp)));
1065  }
1066 
1067 #ifndef SWIG
1068  static formula multop(op o, std::vector<formula>&& l)
1069  {
1070  std::vector<const fnode*> tmp;
1071  tmp.reserve(l.size());
1072  for (auto f: l)
1073  if (f.ptr_)
1074  tmp.emplace_back(f.to_node_());
1075  return formula(fnode::multop(o, std::move(tmp)));
1076  }
1077 #endif // !SWIG
1078 
1080 #ifdef SWIG
1081 #define SPOT_DEF_MULTOP(Name) \
1082  static formula Name(const std::vector<formula>& l) \
1083  { \
1084  return multop(op::Name, l); \
1085  }
1086 #else // !SWIG
1087 #define SPOT_DEF_MULTOP(Name) \
1088  static formula Name(const std::vector<formula>& l) \
1089  { \
1090  return multop(op::Name, l); \
1091  } \
1092  \
1093  static formula Name(std::vector<formula>&& l) \
1094  { \
1095  return multop(op::Name, std::move(l)); \
1096  }
1097 #endif // !SWIG
1098  SPOT_DEF_MULTOP(Or);
1102 
1105  SPOT_DEF_MULTOP(OrRat);
1107 
1110  SPOT_DEF_MULTOP(And);
1112 
1115  SPOT_DEF_MULTOP(AndRat);
1117 
1120  SPOT_DEF_MULTOP(AndNLM);
1122 
1125  SPOT_DEF_MULTOP(Concat);
1127 
1130  SPOT_DEF_MULTOP(Fusion);
1132 #undef SPOT_DEF_MULTOP
1133 
1138  static formula bunop(op o, const formula& f,
1139  uint8_t min = 0U,
1140  uint8_t max = unbounded())
1141  {
1142  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1143  }
1144 
1145 #ifndef SWIG
1146  static formula bunop(op o, formula&& f,
1147  uint8_t min = 0U,
1148  uint8_t max = unbounded())
1149  {
1150  return formula(fnode::bunop(o, f.to_node_(), min, max));
1151  }
1152 #endif // !SWIG
1153 
1155 #if SWIG
1156 #define SPOT_DEF_BUNOP(Name) \
1157  static formula Name(const formula& f, \
1158  uint8_t min = 0U, \
1159  uint8_t max = unbounded()) \
1160  { \
1161  return bunop(op::Name, f, min, max); \
1162  }
1163 #else // !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  static formula Name(formula&& f, \
1172  uint8_t min = 0U, \
1173  uint8_t max = unbounded()) \
1174  { \
1175  return bunop(op::Name, std::move(f), min, max); \
1176  }
1177 #endif
1178  SPOT_DEF_BUNOP(Star);
1182 
1187 
1202  SPOT_DEF_BUNOP(FStar);
1205 #undef SPOT_DEF_BUNOP
1206 
1214  static const formula nested_unop_range(op uo, op bo, unsigned min,
1215  unsigned max, formula f)
1216  {
1217  return formula(fnode::nested_unop_range(uo, bo, min, max,
1218  f.ptr_->clone()));
1219  }
1220 
1226  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1227 
1233  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1234 
1235 #ifndef SWIG
1236  const fnode* to_node_()
1246  {
1247  auto tmp = ptr_;
1248  ptr_ = nullptr;
1249  return tmp;
1250  }
1251 #endif
1252 
1254  op kind() const
1255  {
1256  return ptr_->kind();
1257  }
1258 
1260  std::string kindstr() const
1261  {
1262  return ptr_->kindstr();
1263  }
1264 
1266  bool is(op o) const
1267  {
1268  return ptr_->is(o);
1269  }
1270 
1271 #ifndef SWIG
1272  bool is(op o1, op o2) const
1274  {
1275  return ptr_->is(o1, o2);
1276  }
1277 
1279  bool is(std::initializer_list<op> l) const
1280  {
1281  return ptr_->is(l);
1282  }
1283 #endif
1284 
1289  {
1290  auto f = ptr_->get_child_of(o);
1291  if (f)
1292  f->clone();
1293  return formula(f);
1294  }
1295 
1296 #ifndef SWIG
1297  formula get_child_of(std::initializer_list<op> l) const
1304  {
1305  auto f = ptr_->get_child_of(l);
1306  if (f)
1307  f->clone();
1308  return formula(f);
1309  }
1310 #endif
1311 
1315  unsigned min() const
1316  {
1317  return ptr_->min();
1318  }
1319 
1323  unsigned max() const
1324  {
1325  return ptr_->max();
1326  }
1327 
1329  unsigned size() const
1330  {
1331  return ptr_->size();
1332  }
1333 
1338  bool is_leaf() const
1339  {
1340  return ptr_->is_leaf();
1341  }
1342 
1351  size_t id() const
1352  {
1353  return ptr_->id();
1354  }
1355 
1356 #ifndef SWIG
1357  class SPOT_API formula_child_iterator final
1359  {
1360  const fnode*const* ptr_;
1361  public:
1362  formula_child_iterator()
1363  : ptr_(nullptr)
1364  {
1365  }
1366 
1367  formula_child_iterator(const fnode*const* f)
1368  : ptr_(f)
1369  {
1370  }
1371 
1372  bool operator==(formula_child_iterator o)
1373  {
1374  return ptr_ == o.ptr_;
1375  }
1376 
1377  bool operator!=(formula_child_iterator o)
1378  {
1379  return ptr_ != o.ptr_;
1380  }
1381 
1382  formula operator*()
1383  {
1384  return formula((*ptr_)->clone());
1385  }
1386 
1387  formula_child_iterator operator++()
1388  {
1389  ++ptr_;
1390  return *this;
1391  }
1392 
1393  formula_child_iterator operator++(int)
1394  {
1395  auto tmp = *this;
1396  ++ptr_;
1397  return tmp;
1398  }
1399  };
1400 
1402  formula_child_iterator begin() const
1403  {
1404  return ptr_->begin();
1405  }
1406 
1408  formula_child_iterator end() const
1409  {
1410  return ptr_->end();
1411  }
1412 
1414  formula operator[](unsigned i) const
1415  {
1416  return formula(ptr_->nth(i)->clone());
1417  }
1418 #endif
1419 
1421  static formula ff()
1422  {
1423  return formula(fnode::ff());
1424  }
1425 
1427  bool is_ff() const
1428  {
1429  return ptr_->is_ff();
1430  }
1431 
1433  static formula tt()
1434  {
1435  return formula(fnode::tt());
1436  }
1437 
1439  bool is_tt() const
1440  {
1441  return ptr_->is_tt();
1442  }
1443 
1445  static formula eword()
1446  {
1447  return formula(fnode::eword());
1448  }
1449 
1451  bool is_eword() const
1452  {
1453  return ptr_->is_eword();
1454  }
1455 
1457  bool is_constant() const
1458  {
1459  return ptr_->is_constant();
1460  }
1461 
1466  bool is_Kleene_star() const
1467  {
1468  return ptr_->is_Kleene_star();
1469  }
1470 
1473  {
1474  return formula(fnode::one_star()->clone());
1475  }
1476 
1479  bool is_literal()
1480  {
1481  return (is(op::ap) ||
1482  // If f is in nenoform, Not can only occur in front of
1483  // an atomic proposition. So this way we do not have
1484  // to check the type of the child.
1485  (is(op::Not) && is_boolean() && is_in_nenoform()));
1486  }
1487 
1491  const std::string& ap_name() const
1492  {
1493  return ptr_->ap_name();
1494  }
1495 
1500  std::ostream& dump(std::ostream& os) const
1501  {
1502  return ptr_->dump(os);
1503  }
1504 
1510  formula all_but(unsigned i) const
1511  {
1512  return formula(ptr_->all_but(i));
1513  }
1514 
1524  unsigned boolean_count() const
1525  {
1526  return ptr_->boolean_count();
1527  }
1528 
1542  formula boolean_operands(unsigned* width = nullptr) const
1543  {
1544  return formula(ptr_->boolean_operands(width));
1545  }
1546 
1547 #define SPOT_DEF_PROP(Name) \
1548  bool Name() const \
1549  { \
1550  return ptr_->Name(); \
1551  }
1552  // Properties //
1555 
1557  SPOT_DEF_PROP(is_boolean);
1559  SPOT_DEF_PROP(is_sugar_free_boolean);
1564  SPOT_DEF_PROP(is_in_nenoform);
1566  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1568  SPOT_DEF_PROP(is_sugar_free_ltl);
1570  SPOT_DEF_PROP(is_ltl_formula);
1572  SPOT_DEF_PROP(is_psl_formula);
1574  SPOT_DEF_PROP(is_sere_formula);
1577  SPOT_DEF_PROP(is_finite);
1581 
1595  SPOT_DEF_PROP(is_eventual);
1602 
1616  SPOT_DEF_PROP(is_universal);
1621  SPOT_DEF_PROP(is_syntactic_safety);
1623  SPOT_DEF_PROP(is_syntactic_guarantee);
1625  SPOT_DEF_PROP(is_syntactic_obligation);
1627  SPOT_DEF_PROP(is_syntactic_recurrence);
1629  SPOT_DEF_PROP(is_syntactic_persistence);
1632  SPOT_DEF_PROP(is_marked);
1634  SPOT_DEF_PROP(accepts_eword);
1640  SPOT_DEF_PROP(has_lbt_atomic_props);
1649  SPOT_DEF_PROP(has_spin_atomic_props);
1650 #undef SPOT_DEF_PROP
1651 
1655  template<typename Trans, typename... Args>
1656  formula map(Trans trans, Args&&... args)
1657  {
1658  switch (op o = kind())
1659  {
1660  case op::ff:
1661  case op::tt:
1662  case op::eword:
1663  case op::ap:
1664  return *this;
1665  case op::Not:
1666  case op::X:
1667  case op::F:
1668  case op::G:
1669  case op::Closure:
1670  case op::NegClosure:
1671  case op::NegClosureMarked:
1672  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1673  case op::Xor:
1674  case op::Implies:
1675  case op::Equiv:
1676  case op::U:
1677  case op::R:
1678  case op::W:
1679  case op::M:
1680  case op::EConcat:
1681  case op::EConcatMarked:
1682  case op::UConcat:
1683  {
1684  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1685  return binop(o, tmp,
1686  trans((*this)[1], std::forward<Args>(args)...));
1687  }
1688  case op::Or:
1689  case op::OrRat:
1690  case op::And:
1691  case op::AndRat:
1692  case op::AndNLM:
1693  case op::Concat:
1694  case op::Fusion:
1695  {
1696  std::vector<formula> tmp;
1697  tmp.reserve(size());
1698  for (auto f: *this)
1699  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1700  return multop(o, std::move(tmp));
1701  }
1702  case op::Star:
1703  case op::FStar:
1704  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1705  min(), max());
1706  }
1707  SPOT_UNREACHABLE();
1708  }
1709 
1718  template<typename Func, typename... Args>
1719  void traverse(Func func, Args&&... args)
1720  {
1721  if (func(*this, std::forward<Args>(args)...))
1722  return;
1723  for (auto f: *this)
1724  f.traverse(func, std::forward<Args>(args)...);
1725  }
1726 
1727  private:
1728 #ifndef SWIG
1729  [[noreturn]] static void report_ap_invalid_arg();
1730 #endif
1731  };
1732 
1734  SPOT_API
1735  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1736  bool abbreviated = false);
1737 
1739  SPOT_API
1740  std::list<std::string> list_formula_props(const formula& f);
1741 
1743  SPOT_API
1744  std::ostream& operator<<(std::ostream& os, const formula& f);
1745 }
1746 
1747 #ifndef SWIG
1748 namespace std
1749 {
1750  template <>
1751  struct hash<spot::formula>
1752  {
1753  size_t operator()(const spot::formula& x) const noexcept
1754  {
1755  return x.id();
1756  }
1757  };
1758 }
1759 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1057
const fnode *const * begin() const
Definition: formula.hh:253
Definition: automata.hh:26
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1472
~formula()
Destroy a formula.
Definition: formula.hh:730
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:968
bool is_boolean() const
Definition: formula.hh:369
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1402
static const fnode * eword()
Definition: formula.hh:297
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:1457
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1500
unsigned max() const
Definition: formula.hh:227
size_t id() const
Definition: formula.hh:247
PSL Closure.
bool is(op o) const
Definition: formula.hh:171
bool is_psl_formula() const
Definition: formula.hh:405
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1323
bool is_leaf() const
Definition: formula.hh:241
bool is_finite() const
Definition: formula.hh:417
bool is_eword() const
Definition: formula.hh:303
unsigned boolean_count() const
Definition: formula.hh:340
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:832
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition: formula.hh:911
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:715
static formula tt()
Return the true constant.
Definition: formula.hh:1433
const fnode * get_child_of(op o) const
Definition: formula.hh:196
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition: formula.hh:921
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1315
Definition: bitset.hh:405
Empty word.
bool is_syntactic_guarantee() const
Definition: formula.hh:441
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1427
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1491
static const fnode * tt()
Definition: formula.hh:285
bool is_syntactic_persistence() const
Definition: formula.hh:459
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:963
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:958
const fnode * nth(unsigned i) const
Definition: formula.hh:265
bool is_marked() const
Definition: formula.hh:465
Concatenation.
bool is_syntactic_recurrence() const
Definition: formula.hh:453
bool is(std::initializer_list< op > l) const
Definition: formula.hh:183
Main class for temporal logic formula.
Definition: formula.hh:685
bool is_syntactic_obligation() const
Definition: formula.hh:447
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:177
bool has_spin_atomic_props() const
Definition: formula.hh:483
release (dual of until)
bool is_constant() const
Definition: formula.hh:309
unsigned size() const
Return the number of children.
Definition: formula.hh:1329
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1479
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:859
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:387
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:1279
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1466
size_t id() const
Return the id of a formula.
Definition: formula.hh:1351
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1266
void destroy() const
Dereference an fnode.
Definition: formula.hh:130
static formula ff()
Return the false constant.
Definition: formula.hh:1421
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:1214
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1068
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:273
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:1451
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:1146
static const fnode * one_star()
Definition: formula.hh:323
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:703
bool is_syntactic_safety() const
Definition: formula.hh:435
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1260
Exclusive Or.
marked version of the Negated PSL Closure
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition: formula.hh:896
bool is_sugar_free_boolean() const
Definition: formula.hh:375
static formula eword()
Return the empty word constant.
Definition: formula.hh:1445
bool is_ltl_formula() const
Definition: formula.hh:399
Definition: formula.hh:613
bool is_in_nenoform() const
Definition: formula.hh:381
bool is_ff() const
Definition: formula.hh:279
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1439
(omega-Rational) Or
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:693
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:826
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:206
static constexpr uint8_t unbounded()
Definition: formula.hh:140
unsigned size() const
Definition: formula.hh:235
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:743
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:116
bool has_lbt_atomic_props() const
Definition: formula.hh:477
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1414
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1245
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:842
bool is_sugar_free_ltl() const
Definition: formula.hh:393
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:411
op
Operator types.
Definition: formula.hh:64
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:853
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1338
bool is_tt() const
Definition: formula.hh:291
const fnode *const * end() const
Definition: formula.hh:259
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:1138
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1288
Implication.
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1524
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1719
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:162
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1408
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
bool is_eventual() const
Definition: formula.hh:423
unsigned min() const
Definition: formula.hh:219
bool is_universal() const
Definition: formula.hh:429
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1542
Negated PSL Closure.
Rational And.
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1510
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:952
op kind() const
Return top-most operator.
Definition: formula.hh:1254
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:471
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:315
Atomic proposition.
Eventually.
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:723
(omega-Rational) And
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1656
Rational Or.
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:709

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