spot  2.0.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
3 // l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
22 #pragma once
23 
30 
33 
36 
39 
42 
43 #include <spot/misc/common.hh>
44 #include <memory>
45 #include <cstdint>
46 #include <initializer_list>
47 #include <cassert>
48 #include <vector>
49 #include <string>
50 #include <iterator>
51 #include <iosfwd>
52 #include <sstream>
53 #include <list>
54 #include <cstddef>
55 #include <initializer_list>
56 #include <limits>
57 
58 namespace spot
59 {
62  enum class op: uint8_t
63  {
64  ff,
65  tt,
66  eword,
67  ap,
68  // unary operators
69  Not,
70  X,
71  F,
72  G,
73  Closure,
74  NegClosure,
76  // binary operators
77  Xor,
78  Implies,
79  Equiv,
80  U,
81  R,
82  W,
83  M,
84  EConcat,
86  UConcat,
87  // n-ary operators
88  Or,
89  OrRat,
90  And,
91  AndRat,
92  AndNLM,
93  Concat,
94  Fusion,
95  // star-like operators
96  Star,
97  FStar,
98  };
99 
100 #ifndef SWIG
101  class SPOT_API fnode final
108  {
109  public:
114  const fnode* clone() const
115  {
116  // Saturate.
117  ++refs_;
118  if (SPOT_UNLIKELY(!refs_))
119  saturated_ = 1;
120  return this;
121  }
122 
128  void destroy() const
129  {
130  if (SPOT_LIKELY(refs_))
131  --refs_;
132  else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
133  // last reference to a node that is not a constant
134  destroy_aux();
135  }
136 
138  static constexpr uint8_t unbounded()
139  {
140  return UINT8_MAX;
141  }
142 
144  static const fnode* ap(const std::string& name);
146  static const fnode* unop(op o, const fnode* f);
148  static const fnode* binop(op o, const fnode* f, const fnode* g);
150  static const fnode* multop(op o, std::vector<const fnode*> l);
152  static const fnode* bunop(op o, const fnode* f,
153  uint8_t min, uint8_t max = unbounded());
154 
156  op kind() const
157  {
158  return op_;
159  }
160 
162  std::string kindstr() const;
163 
165  bool is(op o) const
166  {
167  return op_ == o;
168  }
169 
171  bool is(op o1, op o2) const
172  {
173  return op_ == o1 || op_ == o2;
174  }
175 
177  bool is(std::initializer_list<op> l) const
178  {
179  const fnode* n = this;
180  for (auto o: l)
181  {
182  if (!n->is(o))
183  return false;
184  n = n->nth(0);
185  }
186  return true;
187  }
188 
190  const fnode* get_child_of(op o) const
191  {
192  if (op_ != o)
193  return nullptr;
194  assert(size_ == 1);
195  return nth(0);
196  }
197 
199  const fnode* get_child_of(std::initializer_list<op> l) const
200  {
201  auto c = this;
202  for (auto o: l)
203  {
204  c = c->get_child_of(o);
205  if (c == nullptr)
206  return c;
207  }
208  return c;
209  }
210 
212  unsigned min() const
213  {
214  assert(op_ == op::FStar || op_ == op::Star);
215  return min_;
216  }
217 
219  unsigned max() const
220  {
221  assert(op_ == op::FStar || op_ == op::Star);
222  return max_;
223  }
224 
226  unsigned size() const
227  {
228  return size_;
229  }
230 
232  size_t id() const
233  {
234  return id_;
235  }
236 
238  const fnode*const* begin() const
239  {
240  return children;
241  }
242 
244  const fnode*const* end() const
245  {
246  return children + size();
247  }
248 
250  const fnode* nth(unsigned i) const
251  {
252  if (i >= size())
253  throw std::runtime_error("access to non-existing child");
254  return children[i];
255  }
256 
258  static const fnode* ff()
259  {
260  return ff_;
261  }
262 
264  bool is_ff() const
265  {
266  return op_ == op::ff;
267  }
268 
270  static const fnode* tt()
271  {
272  return tt_;
273  }
274 
276  bool is_tt() const
277  {
278  return op_ == op::tt;
279  }
280 
282  static const fnode* eword()
283  {
284  return ew_;
285  }
286 
288  bool is_eword() const
289  {
290  return op_ == op::eword;
291  }
292 
294  bool is_constant() const
295  {
296  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
297  }
298 
300  bool is_Kleene_star() const
301  {
302  if (op_ != op::Star)
303  return false;
304  return min_ == 0 && max_ == unbounded();
305  }
306 
308  static const fnode* one_star()
309  {
310  if (!one_star_)
311  one_star_ = bunop(op::Star, tt(), 0);
312  return one_star_;
313  }
314 
316  const std::string& ap_name() const;
317 
319  std::ostream& dump(std::ostream& os) const;
320 
322  const fnode* all_but(unsigned i) const;
323 
325  unsigned boolean_count() const
326  {
327  unsigned pos = 0;
328  unsigned s = size();
329  while (pos < s && children[pos]->is_boolean())
330  ++pos;
331  return pos;
332  }
333 
335  const fnode* boolean_operands(unsigned* width = nullptr) const;
336 
347  static bool instances_check();
348 
350  // Properties //
352 
354  bool is_boolean() const
355  {
356  return is_.boolean;
357  }
358 
361  {
362  return is_.sugar_free_boolean;
363  }
364 
366  bool is_in_nenoform() const
367  {
368  return is_.in_nenoform;
369  }
370 
373  {
374  return is_.syntactic_si;
375  }
376 
378  bool is_sugar_free_ltl() const
379  {
380  return is_.sugar_free_ltl;
381  }
382 
384  bool is_ltl_formula() const
385  {
386  return is_.ltl_formula;
387  }
388 
390  bool is_psl_formula() const
391  {
392  return is_.psl_formula;
393  }
394 
396  bool is_sere_formula() const
397  {
398  return is_.sere_formula;
399  }
400 
402  bool is_finite() const
403  {
404  return is_.finite;
405  }
406 
408  bool is_eventual() const
409  {
410  return is_.eventual;
411  }
412 
414  bool is_universal() const
415  {
416  return is_.universal;
417  }
418 
420  bool is_syntactic_safety() const
421  {
422  return is_.syntactic_safety;
423  }
424 
427  {
428  return is_.syntactic_guarantee;
429  }
430 
433  {
434  return is_.syntactic_obligation;
435  }
436 
439  {
440  return is_.syntactic_recurrence;
441  }
442 
445  {
446  return is_.syntactic_persistence;
447  }
448 
450  bool is_marked() const
451  {
452  return !is_.not_marked;
453  }
454 
456  bool accepts_eword() const
457  {
458  return is_.accepting_eword;
459  }
460 
462  bool has_lbt_atomic_props() const
463  {
464  return is_.lbt_atomic_props;
465  }
466 
469  {
470  return is_.spin_atomic_props;
471  }
472 
473  private:
474  void setup_props(op o);
475  void destroy_aux() const;
476 
477  static const fnode* unique(const fnode*);
478 
479  // Destruction may only happen via destroy().
480  ~fnode() = default;
481  // Disallow copies.
482  fnode(const fnode&) = delete;
483  fnode& operator=(const fnode&) = delete;
484 
485 
486 
487  template<class iter>
488  fnode(op o, iter begin, iter end)
489  {
490  size_t s = std::distance(begin, end);
491  if (s > (size_t) UINT16_MAX)
492  throw std::runtime_error("too many children for formula");
493  size_ = s;
494  auto pos = children;
495  for (auto i = begin; i != end; ++i)
496  *pos++ = *i;
497  setup_props(o);
498  }
499 
500  fnode(op o, std::initializer_list<const fnode*> l)
501  : fnode(o, l.begin(), l.end())
502  {
503  }
504 
505  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
506  {
507  size_ = 1;
508  children[0] = f;
509  min_ = min;
510  max_ = max;
511  setup_props(o);
512  }
513 
514  static const fnode* ff_;
515  static const fnode* tt_;
516  static const fnode* ew_;
517  static const fnode* one_star_;
518 
519  op op_; // operator
520  uint8_t min_; // range minimum (for star-like operators)
521  uint8_t max_; // range maximum;
522  mutable uint8_t saturated_ = 0;
523  uint16_t size_; // number of children
524  mutable uint16_t refs_ = 0; // reference count - 1;
525  size_t id_; // Also used as hash.
526  static size_t next_id_;
527 
528  struct ltl_prop
529  {
530  // All properties here should be expressed in such a a way
531  // that property(f && g) is just property(f)&property(g).
532  // This allows us to compute all properties of a compound
533  // formula in one operation.
534  //
535  // For instance we do not use a property that says "has
536  // temporal operator", because it would require an OR between
537  // the two arguments. Instead we have a property that
538  // says "no temporal operator", and that one is computed
539  // with an AND between the arguments.
540  //
541  // Also choose a name that makes sense when prefixed with
542  // "the formula is".
543  bool boolean:1; // No temporal operators.
544  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
545  bool in_nenoform:1; // Negative Normal Form.
546  bool syntactic_si:1; // LTL-X or siPSL
547  bool sugar_free_ltl:1; // No F and G operators.
548  bool ltl_formula:1; // Only LTL operators.
549  bool psl_formula:1; // Only PSL operators.
550  bool sere_formula:1; // Only SERE operators.
551  bool finite:1; // Finite SERE formulae, or Bool+X forms.
552  bool eventual:1; // Purely eventual formula.
553  bool universal:1; // Purely universal formula.
554  bool syntactic_safety:1; // Syntactic Safety Property.
555  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
556  bool syntactic_obligation:1; // Syntactic Obligation Property.
557  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
558  bool syntactic_persistence:1; // Syntactic Persistence Property.
559  bool not_marked:1; // No occurrence of EConcatMarked.
560  bool accepting_eword:1; // Accepts the empty word.
561  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
562  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
563  };
564  union
565  {
566  // Use an unsigned for fast computation of all properties.
567  unsigned props;
568  ltl_prop is_;
569  };
570 
571  const fnode* children[1];
572  };
573 
575  SPOT_API
576  int atomic_prop_cmp(const fnode* f, const fnode* g);
577 
579  {
580  bool
581  operator()(const fnode* left, const fnode* right) const
582  {
583  assert(left);
584  assert(right);
585  if (left == right)
586  return false;
587 
588  // We want Boolean formulae first.
589  bool lib = left->is_boolean();
590  if (lib != right->is_boolean())
591  return lib;
592 
593  // We have two Boolean formulae
594  if (lib)
595  {
596  bool lconst = left->is_constant();
597  if (lconst != right->is_constant())
598  return lconst;
599  if (!lconst)
600  {
601  auto get_literal = [](const fnode* f) -> const fnode*
602  {
603  if (f->is(op::Not))
604  f = f->nth(0);
605  if (f->is(op::ap))
606  return f;
607  return nullptr;
608  };
609  // Literals should come first
610  const fnode* litl = get_literal(left);
611  const fnode* litr = get_literal(right);
612  if (!litl != !litr)
613  return litl;
614  if (litl)
615  {
616  // And they should be sorted alphabetically
617  int cmp = atomic_prop_cmp(litl, litr);
618  if (cmp)
619  return cmp < 0;
620  }
621  }
622  }
623 
624  size_t l = left->id();
625  size_t r = right->id();
626  if (l != r)
627  return l < r;
628  // Because the hash code assigned to each formula is the
629  // number of formulae constructed so far, it is very unlikely
630  // that we will ever reach a case were two different formulae
631  // have the same hash. This will happen only ever with have
632  // produced 256**sizeof(size_t) formulae (i.e. max_count has
633  // looped back to 0 and started over). In that case we can
634  // order two formulas by looking at their text representation.
635  // We could be more efficient and look at their AST, but it's
636  // not worth the burden. (Also ordering pointers is ruled out
637  // because it breaks the determinism of the implementation.)
638  std::ostringstream old;
639  left->dump(old);
640  std::ostringstream ord;
641  right->dump(ord);
642  return old.str() < ord.str();
643  }
644  };
645 
646 #endif // SWIG
647 
650  class SPOT_API formula final
651  {
652  const fnode* ptr_;
653  public:
658  explicit formula(const fnode* f) noexcept
659  : ptr_(f)
660  {
661  }
662 
668  formula(std::nullptr_t) noexcept
669  : ptr_(nullptr)
670  {
671  }
672 
674  formula() noexcept
675  : ptr_(nullptr)
676  {
677  }
678 
680  formula(const formula& f) noexcept
681  : ptr_(f.ptr_)
682  {
683  if (ptr_)
684  ptr_->clone();
685  }
686 
688  formula(formula&& f) noexcept
689  : ptr_(f.ptr_)
690  {
691  f.ptr_ = nullptr;
692  }
693 
696  {
697  if (ptr_)
698  ptr_->destroy();
699  }
700 
708  const formula& operator=(std::nullptr_t)
709  {
710  this->~formula();
711  ptr_ = nullptr;
712  return *this;
713  }
714 
715  const formula& operator=(const formula& f)
716  {
717  this->~formula();
718  if ((ptr_ = f.ptr_))
719  ptr_->clone();
720  return *this;
721  }
722 
723  const formula& operator=(formula&& f) noexcept
724  {
725  std::swap(f.ptr_, ptr_);
726  return *this;
727  }
728 
729  bool operator<(const formula& other) const noexcept
730  {
731  if (SPOT_UNLIKELY(!other.ptr_))
732  return false;
733  if (SPOT_UNLIKELY(!ptr_))
734  return true;
735  if (id() < other.id())
736  return true;
737  if (id() > other.id())
738  return false;
739  // The case where id()==other.id() but ptr_ != other.ptr_ is
740  // very unlikely (we would need to build more that UINT_MAX
741  // formulas), so let's just compare pointer, and ignore the fact
742  // that it may give some nondeterminism.
743  return ptr_ < other.ptr_;
744  }
745 
746  bool operator<=(const formula& other) const noexcept
747  {
748  return *this == other || *this < other;
749  }
750 
751  bool operator>(const formula& other) const noexcept
752  {
753  return !(*this <= other);
754  }
755 
756  bool operator>=(const formula& other) const noexcept
757  {
758  return !(*this < other);
759  }
760 
761  bool operator==(const formula& other) const noexcept
762  {
763  return other.ptr_ == ptr_;
764  }
765 
766  bool operator==(std::nullptr_t) const noexcept
767  {
768  return ptr_ == nullptr;
769  }
770 
771  bool operator!=(const formula& other) const noexcept
772  {
773  return other.ptr_ != ptr_;
774  }
775 
776  bool operator!=(std::nullptr_t) const noexcept
777  {
778  return ptr_ != nullptr;
779  }
780 
781  operator bool() const
782  {
783  return ptr_ != nullptr;
784  }
785 
787  // Forwarded functions //
789 
791  static constexpr uint8_t unbounded()
792  {
793  return fnode::unbounded();
794  }
795 
797  static formula ap(const std::string& name)
798  {
799  return formula(fnode::ap(name));
800  }
801 
807  static formula ap(const formula& a)
808  {
809  if (a.kind() == op::ap)
810  return a;
811  else
812  throw std::invalid_argument("atomic propositions cannot be "
813  "constructed from arbitrary formulas");
814  }
815 
820  static formula unop(op o, const formula& f)
821  {
822  return formula(fnode::unop(o, f.ptr_->clone()));
823  }
824 
825 #ifndef SWIG
826  static formula unop(op o, formula&& f)
827  {
828  return formula(fnode::unop(o, f.to_node_()));
829  }
830 #endif // !SWIG
831 
833 #ifdef SWIG
834 #define SPOT_DEF_UNOP(Name) \
835  static formula Name(const formula& f) \
836  { \
837  return unop(op::Name, f); \
838  }
839 #else // !SWIG
840 #define SPOT_DEF_UNOP(Name) \
841  static formula Name(const formula& f) \
842  { \
843  return unop(op::Name, f); \
844  } \
845  static formula Name(formula&& f) \
846  { \
847  return unop(op::Name, std::move(f)); \
848  }
849 #endif // !SWIG
850  SPOT_DEF_UNOP(Not);
854 
857  SPOT_DEF_UNOP(X);
859 
862  SPOT_DEF_UNOP(F);
864 
867  SPOT_DEF_UNOP(G);
869 
872  SPOT_DEF_UNOP(Closure);
874 
877  SPOT_DEF_UNOP(NegClosure);
879 
882  SPOT_DEF_UNOP(NegClosureMarked);
884 #undef SPOT_DEF_UNOP
885 
891  static formula binop(op o, const formula& f, const formula& g)
892  {
893  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
894  }
895 
896 #ifndef SWIG
897  static formula binop(op o, const formula& f, formula&& g)
898  {
899  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
900  }
901 
902  static formula binop(op o, formula&& f, const formula& g)
903  {
904  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
905  }
906 
907  static formula binop(op o, formula&& f, formula&& g)
908  {
909  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
910  }
912 
913 #endif //SWIG
914 
915 #ifdef SWIG
916 #define SPOT_DEF_BINOP(Name) \
917  static formula Name(const formula& f, const formula& g) \
918  { \
919  return binop(op::Name, f, g); \
920  }
921 #else // !SWIG
922 #define SPOT_DEF_BINOP(Name) \
923  static formula Name(const formula& f, const formula& g) \
924  { \
925  return binop(op::Name, f, g); \
926  } \
927  static formula Name(const formula& f, formula&& g) \
928  { \
929  return binop(op::Name, f, std::move(g)); \
930  } \
931  static formula Name(formula&& f, const formula& g) \
932  { \
933  return binop(op::Name, std::move(f), g); \
934  } \
935  static formula Name(formula&& f, formula&& g) \
936  { \
937  return binop(op::Name, std::move(f), std::move(g)); \
938  }
939 #endif // !SWIG
940  SPOT_DEF_BINOP(Xor);
944 
947  SPOT_DEF_BINOP(Implies);
949 
952  SPOT_DEF_BINOP(Equiv);
954 
957  SPOT_DEF_BINOP(U);
959 
962  SPOT_DEF_BINOP(R);
964 
967  SPOT_DEF_BINOP(W);
969 
972  SPOT_DEF_BINOP(M);
974 
977  SPOT_DEF_BINOP(EConcat);
979 
982  SPOT_DEF_BINOP(EConcatMarked);
984 
987  SPOT_DEF_BINOP(UConcat);
989 #undef SPOT_DEF_BINOP
990 
996  static formula multop(op o, const std::vector<formula>& l)
997  {
998  std::vector<const fnode*> tmp;
999  tmp.reserve(l.size());
1000  for (auto f: l)
1001  if (f.ptr_)
1002  tmp.push_back(f.ptr_->clone());
1003  return formula(fnode::multop(o, std::move(tmp)));
1004  }
1005 
1006 #ifndef SWIG
1007  static formula multop(op o, std::vector<formula>&& l)
1008  {
1009  std::vector<const fnode*> tmp;
1010  tmp.reserve(l.size());
1011  for (auto f: l)
1012  if (f.ptr_)
1013  tmp.push_back(f.to_node_());
1014  return formula(fnode::multop(o, std::move(tmp)));
1015  }
1016 #endif // !SWIG
1017 
1019 #ifdef SWIG
1020 #define SPOT_DEF_MULTOP(Name) \
1021  static formula Name(const std::vector<formula>& l) \
1022  { \
1023  return multop(op::Name, l); \
1024  }
1025 #else // !SWIG
1026 #define SPOT_DEF_MULTOP(Name) \
1027  static formula Name(const std::vector<formula>& l) \
1028  { \
1029  return multop(op::Name, l); \
1030  } \
1031  \
1032  static formula Name(std::vector<formula>&& l) \
1033  { \
1034  return multop(op::Name, std::move(l)); \
1035  }
1036 #endif // !SWIG
1037  SPOT_DEF_MULTOP(Or);
1041 
1044  SPOT_DEF_MULTOP(OrRat);
1046 
1049  SPOT_DEF_MULTOP(And);
1051 
1054  SPOT_DEF_MULTOP(AndRat);
1056 
1059  SPOT_DEF_MULTOP(AndNLM);
1061 
1064  SPOT_DEF_MULTOP(Concat);
1066 
1069  SPOT_DEF_MULTOP(Fusion);
1071 #undef SPOT_DEF_MULTOP
1072 
1077  static formula bunop(op o, const formula& f,
1078  uint8_t min = 0U,
1079  uint8_t max = unbounded())
1080  {
1081  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1082  }
1083 
1084 #ifndef SWIG
1085  static formula bunop(op o, formula&& f,
1086  uint8_t min = 0U,
1087  uint8_t max = unbounded())
1088  {
1089  return formula(fnode::bunop(o, f.to_node_(), min, max));
1090  }
1091 #endif // !SWIG
1092 
1094 #if SWIG
1095 #define SPOT_DEF_BUNOP(Name) \
1096  static formula Name(const formula& f, \
1097  uint8_t min = 0U, \
1098  uint8_t max = unbounded()) \
1099  { \
1100  return bunop(op::Name, f, min, max); \
1101  }
1102 #else // !SWIG
1103 #define SPOT_DEF_BUNOP(Name) \
1104  static formula Name(const formula& f, \
1105  uint8_t min = 0U, \
1106  uint8_t max = unbounded()) \
1107  { \
1108  return bunop(op::Name, f, min, max); \
1109  } \
1110  static formula Name(formula&& f, \
1111  uint8_t min = 0U, \
1112  uint8_t max = unbounded()) \
1113  { \
1114  return bunop(op::Name, std::move(f), min, max); \
1115  }
1116 #endif
1117  SPOT_DEF_BUNOP(Star);
1121 
1126 
1141  SPOT_DEF_BUNOP(FStar);
1144 #undef SPOT_DEF_BUNOP
1145 
1151  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1152 
1158  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1159 
1160 #ifndef SWIG
1161  const fnode* to_node_()
1171  {
1172  auto tmp = ptr_;
1173  ptr_ = nullptr;
1174  return tmp;
1175  }
1176 #endif
1177 
1179  op kind() const
1180  {
1181  return ptr_->kind();
1182  }
1183 
1185  std::string kindstr() const
1186  {
1187  return ptr_->kindstr();
1188  }
1189 
1191  bool is(op o) const
1192  {
1193  return ptr_->is(o);
1194  }
1195 
1196 #ifndef SWIG
1197  bool is(op o1, op o2) const
1199  {
1200  return ptr_->is(o1, o2);
1201  }
1202 
1204  bool is(std::initializer_list<op> l) const
1205  {
1206  return ptr_->is(l);
1207  }
1208 #endif
1209 
1214  {
1215  auto f = ptr_->get_child_of(o);
1216  if (f)
1217  f->clone();
1218  return formula(f);
1219  }
1220 
1221 #ifndef SWIG
1222  formula get_child_of(std::initializer_list<op> l) const
1229  {
1230  auto f = ptr_->get_child_of(l);
1231  if (f)
1232  f->clone();
1233  return formula(f);
1234  }
1235 #endif
1236 
1240  unsigned min() const
1241  {
1242  return ptr_->min();
1243  }
1244 
1248  unsigned max() const
1249  {
1250  return ptr_->max();
1251  }
1252 
1254  unsigned size() const
1255  {
1256  return ptr_->size();
1257  }
1258 
1267  size_t id() const
1268  {
1269  return ptr_->id();
1270  }
1271 
1272 #ifndef SWIG
1273  class SPOT_API formula_child_iterator final
1275  {
1276  const fnode*const* ptr_;
1277  public:
1278  formula_child_iterator()
1279  : ptr_(nullptr)
1280  {
1281  }
1282 
1283  formula_child_iterator(const fnode*const* f)
1284  : ptr_(f)
1285  {
1286  }
1287 
1288  bool operator==(formula_child_iterator o)
1289  {
1290  return ptr_ == o.ptr_;
1291  }
1292 
1293  bool operator!=(formula_child_iterator o)
1294  {
1295  return ptr_ != o.ptr_;
1296  }
1297 
1298  formula operator*()
1299  {
1300  return formula((*ptr_)->clone());
1301  }
1302 
1303  formula_child_iterator operator++()
1304  {
1305  ++ptr_;
1306  return *this;
1307  }
1308 
1309  formula_child_iterator operator++(int)
1310  {
1311  auto tmp = *this;
1312  ++ptr_;
1313  return tmp;
1314  }
1315  };
1316 
1319  {
1320  return ptr_->begin();
1321  }
1322 
1325  {
1326  return ptr_->end();
1327  }
1328 
1330  formula operator[](unsigned i) const
1331  {
1332  return formula(ptr_->nth(i)->clone());
1333  }
1334 #endif
1335 
1337  static formula ff()
1338  {
1339  return formula(fnode::ff());
1340  }
1341 
1343  bool is_ff() const
1344  {
1345  return ptr_->is_ff();
1346  }
1347 
1349  static formula tt()
1350  {
1351  return formula(fnode::tt());
1352  }
1353 
1355  bool is_tt() const
1356  {
1357  return ptr_->is_tt();
1358  }
1359 
1361  static formula eword()
1362  {
1363  return formula(fnode::eword());
1364  }
1365 
1367  bool is_eword() const
1368  {
1369  return ptr_->is_eword();
1370  }
1371 
1373  bool is_constant() const
1374  {
1375  return ptr_->is_constant();
1376  }
1377 
1382  bool is_Kleene_star() const
1383  {
1384  return ptr_->is_Kleene_star();
1385  }
1386 
1389  {
1390  return formula(fnode::one_star()->clone());
1391  }
1392 
1395  bool is_literal()
1396  {
1397  return (is(op::ap) ||
1398  // If f is in nenoform, Not can only occur in front of
1399  // an atomic proposition. So this way we do not have
1400  // to check the type of the child.
1401  (is(op::Not) && is_boolean() && is_in_nenoform()));
1402  }
1403 
1407  const std::string& ap_name() const
1408  {
1409  return ptr_->ap_name();
1410  }
1411 
1416  std::ostream& dump(std::ostream& os) const
1417  {
1418  return ptr_->dump(os);
1419  }
1420 
1426  formula all_but(unsigned i) const
1427  {
1428  return formula(ptr_->all_but(i));
1429  }
1430 
1440  unsigned boolean_count() const
1441  {
1442  return ptr_->boolean_count();
1443  }
1444 
1458  formula boolean_operands(unsigned* width = nullptr) const
1459  {
1460  return formula(ptr_->boolean_operands(width));
1461  }
1462 
1463 #define SPOT_DEF_PROP(Name) \
1464  bool Name() const \
1465  { \
1466  return ptr_->Name(); \
1467  }
1468  // Properties //
1471 
1473  SPOT_DEF_PROP(is_boolean);
1475  SPOT_DEF_PROP(is_sugar_free_boolean);
1480  SPOT_DEF_PROP(is_in_nenoform);
1482  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1484  SPOT_DEF_PROP(is_sugar_free_ltl);
1486  SPOT_DEF_PROP(is_ltl_formula);
1488  SPOT_DEF_PROP(is_psl_formula);
1490  SPOT_DEF_PROP(is_sere_formula);
1493  SPOT_DEF_PROP(is_finite);
1497 
1511  SPOT_DEF_PROP(is_eventual);
1518 
1532  SPOT_DEF_PROP(is_universal);
1537  SPOT_DEF_PROP(is_syntactic_safety);
1539  SPOT_DEF_PROP(is_syntactic_guarantee);
1541  SPOT_DEF_PROP(is_syntactic_obligation);
1543  SPOT_DEF_PROP(is_syntactic_recurrence);
1545  SPOT_DEF_PROP(is_syntactic_persistence);
1548  SPOT_DEF_PROP(is_marked);
1550  SPOT_DEF_PROP(accepts_eword);
1556  SPOT_DEF_PROP(has_lbt_atomic_props);
1565  SPOT_DEF_PROP(has_spin_atomic_props);
1566 #undef SPOT_DEF_PROP
1567 
1569  template<typename Trans>
1570  formula map(Trans trans)
1571  {
1572  switch (op o = kind())
1573  {
1574  case op::ff:
1575  case op::tt:
1576  case op::eword:
1577  case op::ap:
1578  return *this;
1579  case op::Not:
1580  case op::X:
1581  case op::F:
1582  case op::G:
1583  case op::Closure:
1584  case op::NegClosure:
1585  case op::NegClosureMarked:
1586  return unop(o, trans((*this)[0]));
1587  case op::Xor:
1588  case op::Implies:
1589  case op::Equiv:
1590  case op::U:
1591  case op::R:
1592  case op::W:
1593  case op::M:
1594  case op::EConcat:
1595  case op::EConcatMarked:
1596  case op::UConcat:
1597  {
1598  formula tmp = trans((*this)[0]);
1599  return binop(o, tmp, trans((*this)[1]));
1600  }
1601  case op::Or:
1602  case op::OrRat:
1603  case op::And:
1604  case op::AndRat:
1605  case op::AndNLM:
1606  case op::Concat:
1607  case op::Fusion:
1608  {
1609  std::vector<formula> tmp;
1610  tmp.reserve(size());
1611  for (auto f: *this)
1612  tmp.push_back(trans(f));
1613  return multop(o, std::move(tmp));
1614  }
1615  case op::Star:
1616  case op::FStar:
1617  return bunop(o, trans((*this)[0]), min(), max());
1618  }
1619  SPOT_UNREACHABLE();
1620  }
1621 
1627  template<typename Func>
1628  void traverse(Func func)
1629  {
1630  if (func(*this))
1631  return;
1632  for (auto f: *this)
1633  f.traverse(func);
1634  }
1635  };
1636 
1638  SPOT_API
1639  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1640  bool abbreviated = false);
1641 
1643  SPOT_API
1644  std::list<std::string> list_formula_props(const formula& f);
1645 
1647  SPOT_API
1648  std::ostream& operator<<(std::ostream& os, const formula& f);
1649 }
1650 
1651 #ifndef SWIG
1652 namespace std
1653 {
1654  template <>
1655  struct hash<spot::formula>
1656  {
1657  size_t operator()(const spot::formula& x) const noexcept
1658  {
1659  return x.id();
1660  }
1661  };
1662 }
1663 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:996
bool is_tt() const
Definition: formula.hh:276
Definition: graph.hh:32
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1388
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition: formula.hh:1373
~formula()
Destroy a formula.
Definition: formula.hh:695
bool is(op o) const
Definition: formula.hh:165
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1416
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:907
const fnode *const * begin() const
Definition: formula.hh:238
static const fnode * eword()
Definition: formula.hh:282
static const fnode * ap(const std::string &name)
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1213
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1426
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:372
PSL Closure.
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1248
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1407
bool is_syntactic_safety() const
Definition: formula.hh:420
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1355
bool is_eventual() const
Definition: formula.hh:408
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:797
unsigned size() const
Return the number of children.
Definition: formula.hh:1254
bool is_ltl_formula() const
Definition: formula.hh:384
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:680
static formula tt()
Return the true constant.
Definition: formula.hh:1349
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1440
Definition: formula.hh:1652
bool is_psl_formula() const
Definition: formula.hh:390
bool is_sere_formula() const
Definition: formula.hh:396
Empty word.
static const fnode * tt()
Definition: formula.hh:270
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:902
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:897
bool is_marked() const
Definition: formula.hh:450
Concatenation.
bool is(op o1, op o2) const
Definition: formula.hh:171
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1240
bool is_syntactic_recurrence() const
Definition: formula.hh:438
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:114
Main class for temporal logic formula.
Definition: formula.hh:650
Globally.
release (dual of until)
unsigned size() const
Definition: formula.hh:226
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1395
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1458
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:826
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1343
bool is_Kleene_star() const
Definition: formula.hh:300
Fustion Star.
bool is_in_nenoform() const
Definition: formula.hh:366
unsigned boolean_count() const
Definition: formula.hh:325
weak until
bool is_sugar_free_boolean() const
Definition: formula.hh:360
unsigned max() const
Definition: formula.hh:219
unsigned min() const
Definition: formula.hh:212
static formula ff()
Return the false constant.
Definition: formula.hh:1337
static const fnode * multop(op o, std::vector< const fnode * > l)
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1007
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1330
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:258
Allow iterating over children.
Definition: formula.hh:1274
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:1085
static const fnode * one_star()
Definition: formula.hh:308
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:668
Exclusive Or.
marked version of the Negated PSL Clusure
bool is_constant() const
Definition: formula.hh:294
static formula eword()
Return the empty word constant.
Definition: formula.hh:1361
const fnode * get_child_of(op o) const
Definition: formula.hh:190
const fnode *const * end() const
Definition: formula.hh:244
op kind() const
Return top-most operator.
Definition: formula.hh:1179
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1191
Definition: formula.hh:578
formula map(Trans trans)
Clone this node after applying trans to its children.
Definition: formula.hh:1570
bool has_spin_atomic_props() const
Definition: formula.hh:468
bool accepts_eword() const
Definition: formula.hh:456
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1382
const fnode * nth(unsigned i) const
Definition: formula.hh:250
(omega-Rational) Or
void destroy() const
Dereference an fnode.
Definition: formula.hh:128
op kind() const
Definition: formula.hh:156
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:658
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:791
static constexpr uint8_t unbounded()
Definition: formula.hh:138
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:708
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1170
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:807
bool is_syntactic_guarantee() const
Definition: formula.hh:426
std::ostream & dump(std::ostream &os) const
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1318
static const fnode * binop(op o, const fnode *f, const fnode *g)
op
Operator types.
Definition: formula.hh:62
bool is_syntactic_persistence() const
Definition: formula.hh:444
bool is_ff() const
Definition: formula.hh:264
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:820
bool is_universal() const
Definition: formula.hh:414
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:1077
Implication.
bool is_boolean() const
Definition: formula.hh:354
bool is_syntactic_obligation() const
Definition: formula.hh:432
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1324
bool is_sugar_free_ltl() const
Definition: formula.hh:378
Actual storage for formula nodes.
Definition: formula.hh:107
size_t id() const
Return the id of a formula.
Definition: formula.hh:1267
Negated PSL Closure.
bool is(std::initializer_list< op > l) const
Definition: formula.hh:177
Rational And.
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:891
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition: formula.hh:1204
bool is_finite() const
Definition: formula.hh:402
strong release (dual of weak until)
void traverse(Func func)
Apply func to each subformula.
Definition: formula.hh:1628
bool has_lbt_atomic_props() const
Definition: formula.hh:462
Atomic proposition.
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:199
Eventually.
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1185
formula(formula &&f) noexcept
Clone a formula.
Definition: formula.hh:688
(omega-Rational) And
size_t id() const
Definition: formula.hh:232
bool is_eword() const
Whether the formula is the empty word constant.
Definition: formula.hh:1367
Rational Or.
bool is_eword() const
Definition: formula.hh:288
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:674

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Jul 11 2016 09:54:34 for spot by doxygen 1.8.8