spot  2.9
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 // The strong_X operator was introduced in Spot 2.8.2 to fix an issue
61 // with from_ltlf(). As adding a new operator is a backward
62 // incompatibility, causing new warnings from the compiler.
63 #if defined(SPOT_BUILD) or defined(SPOT_USES_STRONG_X)
64 // Use #if SPOT_HAS_STRONG_X in code that need to be backward
65 // compatible with older Spot versions.
66 # define SPOT_HAS_STRONG_X 1
67 // You me #define SPOT_WANT_STRONG_X yourself before including
68 // this file to force the use of STRONG_X
69 # define SPOT_WANT_STRONG_X 1
70 #endif
71 
72 namespace spot
73 {
74 
75 
78  enum class op: uint8_t
79  {
80  ff,
81  tt,
82  eword,
83  ap,
84  // unary operators
85  Not,
86  X,
87  F,
88  G,
89  Closure,
90  NegClosure,
92  // binary operators
93  Xor,
94  Implies,
95  Equiv,
96  U,
97  R,
98  W,
99  M,
100  EConcat,
101  EConcatMarked,
102  UConcat,
103  // n-ary operators
104  Or,
105  OrRat,
106  And,
107  AndRat,
108  AndNLM,
109  Concat,
110  Fusion,
111  // star-like operators
112  Star,
113  FStar,
114  first_match,
115 #ifdef SPOT_WANT_STRONG_X
116  strong_X,
117 #endif
118  };
119 
120 #ifndef SWIG
121  class SPOT_API fnode final
128  {
129  public:
134  const fnode* clone() const
135  {
136  // Saturate.
137  ++refs_;
138  if (SPOT_UNLIKELY(!refs_))
139  saturated_ = 1;
140  return this;
141  }
142 
148  void destroy() const
149  {
150  if (SPOT_LIKELY(refs_))
151  --refs_;
152  else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
153  // last reference to a node that is not a constant
154  destroy_aux();
155  }
156 
158  static constexpr uint8_t unbounded()
159  {
160  return UINT8_MAX;
161  }
162 
164  static const fnode* ap(const std::string& name);
166  static const fnode* unop(op o, const fnode* f);
168  static const fnode* binop(op o, const fnode* f, const fnode* g);
170  static const fnode* multop(op o, std::vector<const fnode*> l);
172  static const fnode* bunop(op o, const fnode* f,
173  uint8_t min, uint8_t max = unbounded());
174 
176  static const fnode* nested_unop_range(op uo, op bo, unsigned min,
177  unsigned max, const fnode* f);
178 
180  op kind() const
181  {
182  return op_;
183  }
184 
186  std::string kindstr() const;
187 
189  bool is(op o) const
190  {
191  return op_ == o;
192  }
193 
195  bool is(op o1, op o2) const
196  {
197  return op_ == o1 || op_ == o2;
198  }
199 
201  bool is(std::initializer_list<op> l) const
202  {
203  const fnode* n = this;
204  for (auto o: l)
205  {
206  if (!n->is(o))
207  return false;
208  n = n->nth(0);
209  }
210  return true;
211  }
212 
214  const fnode* get_child_of(op o) const
215  {
216  if (op_ != o)
217  return nullptr;
218  if (SPOT_UNLIKELY(size_ != 1))
219  report_get_child_of_expecting_single_child_node();
220  return nth(0);
221  }
222 
224  const fnode* get_child_of(std::initializer_list<op> l) const
225  {
226  auto c = this;
227  for (auto o: l)
228  {
229  c = c->get_child_of(o);
230  if (c == nullptr)
231  return c;
232  }
233  return c;
234  }
235 
237  unsigned min() const
238  {
239  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
240  report_min_invalid_arg();
241  return min_;
242  }
243 
245  unsigned max() const
246  {
247  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
248  report_max_invalid_arg();
249  return max_;
250  }
251 
253  unsigned size() const
254  {
255  return size_;
256  }
257 
259  bool is_leaf() const
260  {
261  return size_ == 0;
262  }
263 
265  size_t id() const
266  {
267  return id_;
268  }
269 
271  const fnode*const* begin() const
272  {
273  return children;
274  }
275 
277  const fnode*const* end() const
278  {
279  return children + size();
280  }
281 
283  const fnode* nth(unsigned i) const
284  {
285  if (SPOT_UNLIKELY(i >= size()))
286  report_non_existing_child();
287  return children[i];
288  }
289 
291  static const fnode* ff()
292  {
293  return ff_;
294  }
295 
297  bool is_ff() const
298  {
299  return op_ == op::ff;
300  }
301 
303  static const fnode* tt()
304  {
305  return tt_;
306  }
307 
309  bool is_tt() const
310  {
311  return op_ == op::tt;
312  }
313 
315  static const fnode* eword()
316  {
317  return ew_;
318  }
319 
321  bool is_eword() const
322  {
323  return op_ == op::eword;
324  }
325 
327  bool is_constant() const
328  {
329  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
330  }
331 
333  bool is_Kleene_star() const
334  {
335  if (op_ != op::Star)
336  return false;
337  return min_ == 0 && max_ == unbounded();
338  }
339 
341  static const fnode* one_star()
342  {
343  if (!one_star_)
344  one_star_ = bunop(op::Star, tt(), 0);
345  return one_star_;
346  }
347 
349  const std::string& ap_name() const;
350 
352  std::ostream& dump(std::ostream& os) const;
353 
355  const fnode* all_but(unsigned i) const;
356 
358  unsigned boolean_count() const
359  {
360  unsigned pos = 0;
361  unsigned s = size();
362  while (pos < s && children[pos]->is_boolean())
363  ++pos;
364  return pos;
365  }
366 
368  const fnode* boolean_operands(unsigned* width = nullptr) const;
369 
380  static bool instances_check();
381 
383  // Properties //
385 
387  bool is_boolean() const
388  {
389  return is_.boolean;
390  }
391 
394  {
395  return is_.sugar_free_boolean;
396  }
397 
399  bool is_in_nenoform() const
400  {
401  return is_.in_nenoform;
402  }
403 
406  {
407  return is_.syntactic_si;
408  }
409 
411  bool is_sugar_free_ltl() const
412  {
413  return is_.sugar_free_ltl;
414  }
415 
417  bool is_ltl_formula() const
418  {
419  return is_.ltl_formula;
420  }
421 
423  bool is_psl_formula() const
424  {
425  return is_.psl_formula;
426  }
427 
429  bool is_sere_formula() const
430  {
431  return is_.sere_formula;
432  }
433 
435  bool is_finite() const
436  {
437  return is_.finite;
438  }
439 
441  bool is_eventual() const
442  {
443  return is_.eventual;
444  }
445 
447  bool is_universal() const
448  {
449  return is_.universal;
450  }
451 
453  bool is_syntactic_safety() const
454  {
455  return is_.syntactic_safety;
456  }
457 
460  {
461  return is_.syntactic_guarantee;
462  }
463 
466  {
467  return is_.syntactic_obligation;
468  }
469 
472  {
473  return is_.syntactic_recurrence;
474  }
475 
478  {
479  return is_.syntactic_persistence;
480  }
481 
483  bool is_marked() const
484  {
485  return !is_.not_marked;
486  }
487 
489  bool accepts_eword() const
490  {
491  return is_.accepting_eword;
492  }
493 
495  bool has_lbt_atomic_props() const
496  {
497  return is_.lbt_atomic_props;
498  }
499 
502  {
503  return is_.spin_atomic_props;
504  }
505 
506  private:
507  static size_t bump_next_id();
508  void setup_props(op o);
509  void destroy_aux() const;
510 
511  [[noreturn]] static void report_non_existing_child();
512  [[noreturn]] static void report_too_many_children();
513  [[noreturn]] static void
514  report_get_child_of_expecting_single_child_node();
515  [[noreturn]] static void report_min_invalid_arg();
516  [[noreturn]] static void report_max_invalid_arg();
517 
518  static const fnode* unique(fnode*);
519 
520  // Destruction may only happen via destroy().
521  ~fnode() = default;
522  // Disallow copies.
523  fnode(const fnode&) = delete;
524  fnode& operator=(const fnode&) = delete;
525 
526 
527 
528  template<class iter>
529  fnode(op o, iter begin, iter end)
530  // Clang has some optimization where is it able to combine the
531  // 4 movb initializing op_,min_,max_,saturated_ into a single
532  // movl. Also it can optimize the three byte-comparisons of
533  // is_Kleene_star() into a single masked 32-bit comparison.
534  // The latter optimization triggers warnings from valgrind if
535  // min_ and max_ are not initialized. So to benefit from the
536  // initialization optimization and the is_Kleene_star()
537  // optimization in Clang, we always initialize min_ and max_
538  // with this compiler. Do not do it the rest of the time,
539  // since the optimization is not done.
540  : op_(o),
541 #if __llvm__
542  min_(0), max_(0),
543 #endif
544  saturated_(0)
545  {
546  size_t s = std::distance(begin, end);
547  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
548  report_too_many_children();
549  size_ = s;
550  auto pos = children;
551  for (auto i = begin; i != end; ++i)
552  *pos++ = *i;
553  setup_props(o);
554  }
555 
556  fnode(op o, std::initializer_list<const fnode*> l)
557  : fnode(o, l.begin(), l.end())
558  {
559  }
560 
561  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
562  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
563  {
564  children[0] = f;
565  setup_props(o);
566  }
567 
568  static const fnode* ff_;
569  static const fnode* tt_;
570  static const fnode* ew_;
571  static const fnode* one_star_;
572 
573  op op_; // operator
574  uint8_t min_; // range minimum (for star-like operators)
575  uint8_t max_; // range maximum;
576  mutable uint8_t saturated_;
577  uint16_t size_; // number of children
578  mutable uint16_t refs_ = 0; // reference count - 1;
579  size_t id_; // Also used as hash.
580  static size_t next_id_;
581 
582  struct ltl_prop
583  {
584  // All properties here should be expressed in such a a way
585  // that property(f && g) is just property(f)&property(g).
586  // This allows us to compute all properties of a compound
587  // formula in one operation.
588  //
589  // For instance we do not use a property that says "has
590  // temporal operator", because it would require an OR between
591  // the two arguments. Instead we have a property that
592  // says "no temporal operator", and that one is computed
593  // with an AND between the arguments.
594  //
595  // Also choose a name that makes sense when prefixed with
596  // "the formula is".
597  bool boolean:1; // No temporal operators.
598  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
599  bool in_nenoform:1; // Negative Normal Form.
600  bool syntactic_si:1; // LTL-X or siPSL
601  bool sugar_free_ltl:1; // No F and G operators.
602  bool ltl_formula:1; // Only LTL operators.
603  bool psl_formula:1; // Only PSL operators.
604  bool sere_formula:1; // Only SERE operators.
605  bool finite:1; // Finite SERE formulae, or Bool+X forms.
606  bool eventual:1; // Purely eventual formula.
607  bool universal:1; // Purely universal formula.
608  bool syntactic_safety:1; // Syntactic Safety Property.
609  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
610  bool syntactic_obligation:1; // Syntactic Obligation Property.
611  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
612  bool syntactic_persistence:1; // Syntactic Persistence Property.
613  bool not_marked:1; // No occurrence of EConcatMarked.
614  bool accepting_eword:1; // Accepts the empty word.
615  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
616  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
617  };
618  union
619  {
620  // Use an unsigned for fast computation of all properties.
621  unsigned props;
622  ltl_prop is_;
623  };
624 
625  const fnode* children[1];
626  };
627 
629  SPOT_API
630  int atomic_prop_cmp(const fnode* f, const fnode* g);
631 
633  {
634  bool
635  operator()(const fnode* left, const fnode* right) const
636  {
637  SPOT_ASSERT(left);
638  SPOT_ASSERT(right);
639  if (left == right)
640  return false;
641 
642  // We want Boolean formulae first.
643  bool lib = left->is_boolean();
644  if (lib != right->is_boolean())
645  return lib;
646 
647  // We have two Boolean formulae
648  if (lib)
649  {
650  bool lconst = left->is_constant();
651  if (lconst != right->is_constant())
652  return lconst;
653  if (!lconst)
654  {
655  auto get_literal = [](const fnode* f) -> const fnode*
656  {
657  if (f->is(op::Not))
658  f = f->nth(0);
659  if (f->is(op::ap))
660  return f;
661  return nullptr;
662  };
663  // Literals should come first
664  const fnode* litl = get_literal(left);
665  const fnode* litr = get_literal(right);
666  if (!litl != !litr)
667  return litl;
668  if (litl)
669  {
670  // And they should be sorted alphabetically
671  int cmp = atomic_prop_cmp(litl, litr);
672  if (cmp)
673  return cmp < 0;
674  }
675  }
676  }
677 
678  size_t l = left->id();
679  size_t r = right->id();
680  if (l != r)
681  return l < r;
682  // Because the hash code assigned to each formula is the
683  // number of formulae constructed so far, it is very unlikely
684  // that we will ever reach a case were two different formulae
685  // have the same hash. This will happen only ever with have
686  // produced 256**sizeof(size_t) formulae (i.e. max_count has
687  // looped back to 0 and started over). In that case we can
688  // order two formulas by looking at their text representation.
689  // We could be more efficient and look at their AST, but it's
690  // not worth the burden. (Also ordering pointers is ruled out
691  // because it breaks the determinism of the implementation.)
692  std::ostringstream old;
693  left->dump(old);
694  std::ostringstream ord;
695  right->dump(ord);
696  return old.str() < ord.str();
697  }
698  };
699 
700 #endif // SWIG
701 
704  class SPOT_API formula final
705  {
706  const fnode* ptr_;
707  public:
712  explicit formula(const fnode* f) noexcept
713  : ptr_(f)
714  {
715  }
716 
722  formula(std::nullptr_t) noexcept
723  : ptr_(nullptr)
724  {
725  }
726 
728  formula() noexcept
729  : ptr_(nullptr)
730  {
731  }
732 
734  formula(const formula& f) noexcept
735  : ptr_(f.ptr_)
736  {
737  if (ptr_)
738  ptr_->clone();
739  }
740 
742  formula(formula&& f) noexcept
743  : ptr_(f.ptr_)
744  {
745  f.ptr_ = nullptr;
746  }
747 
750  {
751  if (ptr_)
752  ptr_->destroy();
753  }
754 
762  const formula& operator=(std::nullptr_t)
763  {
764  this->~formula();
765  ptr_ = nullptr;
766  return *this;
767  }
768 
769  const formula& operator=(const formula& f)
770  {
771  this->~formula();
772  if ((ptr_ = f.ptr_))
773  ptr_->clone();
774  return *this;
775  }
776 
777  const formula& operator=(formula&& f) noexcept
778  {
779  std::swap(f.ptr_, ptr_);
780  return *this;
781  }
782 
783  bool operator<(const formula& other) const noexcept
784  {
785  if (SPOT_UNLIKELY(!other.ptr_))
786  return false;
787  if (SPOT_UNLIKELY(!ptr_))
788  return true;
789  if (id() < other.id())
790  return true;
791  if (id() > other.id())
792  return false;
793  // The case where id()==other.id() but ptr_ != other.ptr_ is
794  // very unlikely (we would need to build more than UINT_MAX
795  // formulas), so let's just compare pointers, and ignore the
796  // fact that it may introduce some nondeterminism.
797  return ptr_ < other.ptr_;
798  }
799 
800  bool operator<=(const formula& other) const noexcept
801  {
802  return *this == other || *this < other;
803  }
804 
805  bool operator>(const formula& other) const noexcept
806  {
807  return !(*this <= other);
808  }
809 
810  bool operator>=(const formula& other) const noexcept
811  {
812  return !(*this < other);
813  }
814 
815  bool operator==(const formula& other) const noexcept
816  {
817  return other.ptr_ == ptr_;
818  }
819 
820  bool operator==(std::nullptr_t) const noexcept
821  {
822  return ptr_ == nullptr;
823  }
824 
825  bool operator!=(const formula& other) const noexcept
826  {
827  return other.ptr_ != ptr_;
828  }
829 
830  bool operator!=(std::nullptr_t) const noexcept
831  {
832  return ptr_ != nullptr;
833  }
834 
835  operator bool() const
836  {
837  return ptr_ != nullptr;
838  }
839 
841  // Forwarded functions //
843 
845  static constexpr uint8_t unbounded()
846  {
847  return fnode::unbounded();
848  }
849 
851  static formula ap(const std::string& name)
852  {
853  return formula(fnode::ap(name));
854  }
855 
861  static formula ap(const formula& a)
862  {
863  if (SPOT_UNLIKELY(a.kind() != op::ap))
864  report_ap_invalid_arg();
865  return a;
866  }
867 
872  static formula unop(op o, const formula& f)
873  {
874  return formula(fnode::unop(o, f.ptr_->clone()));
875  }
876 
877 #ifndef SWIG
878  static formula unop(op o, formula&& f)
879  {
880  return formula(fnode::unop(o, f.to_node_()));
881  }
882 #endif // !SWIG
883 
885 #ifdef SWIG
886 #define SPOT_DEF_UNOP(Name) \
887  static formula Name(const formula& f) \
888  { \
889  return unop(op::Name, f); \
890  }
891 #else // !SWIG
892 #define SPOT_DEF_UNOP(Name) \
893  static formula Name(const formula& f) \
894  { \
895  return unop(op::Name, f); \
896  } \
897  static formula Name(formula&& f) \
898  { \
899  return unop(op::Name, std::move(f)); \
900  }
901 #endif // !SWIG
902  SPOT_DEF_UNOP(Not);
906 
909  SPOT_DEF_UNOP(X);
911 
915  static formula X(unsigned level, const formula& f)
916  {
917  return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
918  }
919 
920 #if SPOT_WANT_STRONG_X
921  SPOT_DEF_UNOP(strong_X);
925 
929  static formula strong_X(unsigned level, const formula& f)
930  {
931  return nested_unop_range(op::strong_X, op::Or /* unused */,
932  level, level, f);
933  }
934 #endif
935 
938  SPOT_DEF_UNOP(F);
940 
947  static formula F(unsigned min_level, unsigned max_level, const formula& f)
948  {
949  return nested_unop_range(op::X, op::Or, min_level, max_level, f);
950  }
951 
958  static formula G(unsigned min_level, unsigned max_level, const formula& f)
959  {
960  return nested_unop_range(op::X, op::And, min_level, max_level, f);
961  }
962 
965  SPOT_DEF_UNOP(G);
967 
970  SPOT_DEF_UNOP(Closure);
972 
975  SPOT_DEF_UNOP(NegClosure);
977 
980  SPOT_DEF_UNOP(NegClosureMarked);
982 
985  SPOT_DEF_UNOP(first_match);
987 #undef SPOT_DEF_UNOP
988 
994  static formula binop(op o, const formula& f, const formula& g)
995  {
996  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
997  }
998 
999 #ifndef SWIG
1000  static formula binop(op o, const formula& f, formula&& g)
1001  {
1002  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
1003  }
1004 
1005  static formula binop(op o, formula&& f, const formula& g)
1006  {
1007  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
1008  }
1009 
1010  static formula binop(op o, formula&& f, formula&& g)
1011  {
1012  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
1013  }
1015 
1016 #endif //SWIG
1017 
1018 #ifdef SWIG
1019 #define SPOT_DEF_BINOP(Name) \
1020  static formula Name(const formula& f, const formula& g) \
1021  { \
1022  return binop(op::Name, f, g); \
1023  }
1024 #else // !SWIG
1025 #define SPOT_DEF_BINOP(Name) \
1026  static formula Name(const formula& f, const formula& g) \
1027  { \
1028  return binop(op::Name, f, g); \
1029  } \
1030  static formula Name(const formula& f, formula&& g) \
1031  { \
1032  return binop(op::Name, f, std::move(g)); \
1033  } \
1034  static formula Name(formula&& f, const formula& g) \
1035  { \
1036  return binop(op::Name, std::move(f), g); \
1037  } \
1038  static formula Name(formula&& f, formula&& g) \
1039  { \
1040  return binop(op::Name, std::move(f), std::move(g)); \
1041  }
1042 #endif // !SWIG
1043  SPOT_DEF_BINOP(Xor);
1047 
1050  SPOT_DEF_BINOP(Implies);
1052 
1055  SPOT_DEF_BINOP(Equiv);
1057 
1060  SPOT_DEF_BINOP(U);
1062 
1065  SPOT_DEF_BINOP(R);
1067 
1070  SPOT_DEF_BINOP(W);
1072 
1075  SPOT_DEF_BINOP(M);
1077 
1080  SPOT_DEF_BINOP(EConcat);
1082 
1085  SPOT_DEF_BINOP(EConcatMarked);
1087 
1090  SPOT_DEF_BINOP(UConcat);
1092 #undef SPOT_DEF_BINOP
1093 
1099  static formula multop(op o, const std::vector<formula>& l)
1100  {
1101  std::vector<const fnode*> tmp;
1102  tmp.reserve(l.size());
1103  for (auto f: l)
1104  if (f.ptr_)
1105  tmp.emplace_back(f.ptr_->clone());
1106  return formula(fnode::multop(o, std::move(tmp)));
1107  }
1108 
1109 #ifndef SWIG
1110  static formula multop(op o, std::vector<formula>&& l)
1111  {
1112  std::vector<const fnode*> tmp;
1113  tmp.reserve(l.size());
1114  for (auto f: l)
1115  if (f.ptr_)
1116  tmp.emplace_back(f.to_node_());
1117  return formula(fnode::multop(o, std::move(tmp)));
1118  }
1119 #endif // !SWIG
1120 
1122 #ifdef SWIG
1123 #define SPOT_DEF_MULTOP(Name) \
1124  static formula Name(const std::vector<formula>& l) \
1125  { \
1126  return multop(op::Name, l); \
1127  }
1128 #else // !SWIG
1129 #define SPOT_DEF_MULTOP(Name) \
1130  static formula Name(const std::vector<formula>& l) \
1131  { \
1132  return multop(op::Name, l); \
1133  } \
1134  \
1135  static formula Name(std::vector<formula>&& l) \
1136  { \
1137  return multop(op::Name, std::move(l)); \
1138  }
1139 #endif // !SWIG
1140  SPOT_DEF_MULTOP(Or);
1144 
1147  SPOT_DEF_MULTOP(OrRat);
1149 
1152  SPOT_DEF_MULTOP(And);
1154 
1157  SPOT_DEF_MULTOP(AndRat);
1159 
1162  SPOT_DEF_MULTOP(AndNLM);
1164 
1167  SPOT_DEF_MULTOP(Concat);
1169 
1172  SPOT_DEF_MULTOP(Fusion);
1174 #undef SPOT_DEF_MULTOP
1175 
1180  static formula bunop(op o, const formula& f,
1181  uint8_t min = 0U,
1182  uint8_t max = unbounded())
1183  {
1184  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1185  }
1186 
1187 #ifndef SWIG
1188  static formula bunop(op o, formula&& f,
1189  uint8_t min = 0U,
1190  uint8_t max = unbounded())
1191  {
1192  return formula(fnode::bunop(o, f.to_node_(), min, max));
1193  }
1194 #endif // !SWIG
1195 
1197 #if SWIG
1198 #define SPOT_DEF_BUNOP(Name) \
1199  static formula Name(const formula& f, \
1200  uint8_t min = 0U, \
1201  uint8_t max = unbounded()) \
1202  { \
1203  return bunop(op::Name, f, min, max); \
1204  }
1205 #else // !SWIG
1206 #define SPOT_DEF_BUNOP(Name) \
1207  static formula Name(const formula& f, \
1208  uint8_t min = 0U, \
1209  uint8_t max = unbounded()) \
1210  { \
1211  return bunop(op::Name, f, min, max); \
1212  } \
1213  static formula Name(formula&& f, \
1214  uint8_t min = 0U, \
1215  uint8_t max = unbounded()) \
1216  { \
1217  return bunop(op::Name, std::move(f), min, max); \
1218  }
1219 #endif
1220  SPOT_DEF_BUNOP(Star);
1224 
1230  SPOT_DEF_BUNOP(FStar);
1232 #undef SPOT_DEF_BUNOP
1233 
1245  static const formula nested_unop_range(op uo, op bo, unsigned min,
1246  unsigned max, formula f)
1247  {
1248  return formula(fnode::nested_unop_range(uo, bo, min, max,
1249  f.ptr_->clone()));
1250  }
1251 
1257  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1258 
1264  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1265 
1287  static formula sugar_delay(const formula& a, const formula& b,
1288  unsigned min, unsigned max);
1289  static formula sugar_delay(const formula& b,
1290  unsigned min, unsigned max);
1292 
1293 #ifndef SWIG
1294  const fnode* to_node_()
1304  {
1305  auto tmp = ptr_;
1306  ptr_ = nullptr;
1307  return tmp;
1308  }
1309 #endif
1310 
1312  op kind() const
1313  {
1314  return ptr_->kind();
1315  }
1316 
1318  std::string kindstr() const
1319  {
1320  return ptr_->kindstr();
1321  }
1322 
1324  bool is(op o) const
1325  {
1326  return ptr_->is(o);
1327  }
1328 
1329 #ifndef SWIG
1330  bool is(op o1, op o2) const
1332  {
1333  return ptr_->is(o1, o2);
1334  }
1335 
1337  bool is(std::initializer_list<op> l) const
1338  {
1339  return ptr_->is(l);
1340  }
1341 #endif
1342 
1347  {
1348  auto f = ptr_->get_child_of(o);
1349  if (f)
1350  f->clone();
1351  return formula(f);
1352  }
1353 
1354 #ifndef SWIG
1355  formula get_child_of(std::initializer_list<op> l) const
1362  {
1363  auto f = ptr_->get_child_of(l);
1364  if (f)
1365  f->clone();
1366  return formula(f);
1367  }
1368 #endif
1369 
1373  unsigned min() const
1374  {
1375  return ptr_->min();
1376  }
1377 
1381  unsigned max() const
1382  {
1383  return ptr_->max();
1384  }
1385 
1387  unsigned size() const
1388  {
1389  return ptr_->size();
1390  }
1391 
1396  bool is_leaf() const
1397  {
1398  return ptr_->is_leaf();
1399  }
1400 
1409  size_t id() const
1410  {
1411  return ptr_->id();
1412  }
1413 
1414 #ifndef SWIG
1415  class SPOT_API formula_child_iterator final
1417  {
1418  const fnode*const* ptr_;
1419  public:
1420  formula_child_iterator()
1421  : ptr_(nullptr)
1422  {
1423  }
1424 
1425  formula_child_iterator(const fnode*const* f)
1426  : ptr_(f)
1427  {
1428  }
1429 
1430  bool operator==(formula_child_iterator o)
1431  {
1432  return ptr_ == o.ptr_;
1433  }
1434 
1435  bool operator!=(formula_child_iterator o)
1436  {
1437  return ptr_ != o.ptr_;
1438  }
1439 
1440  formula operator*()
1441  {
1442  return formula((*ptr_)->clone());
1443  }
1444 
1445  formula_child_iterator operator++()
1446  {
1447  ++ptr_;
1448  return *this;
1449  }
1450 
1451  formula_child_iterator operator++(int)
1452  {
1453  auto tmp = *this;
1454  ++ptr_;
1455  return tmp;
1456  }
1457  };
1458 
1460  formula_child_iterator begin() const
1461  {
1462  return ptr_->begin();
1463  }
1464 
1466  formula_child_iterator end() const
1467  {
1468  return ptr_->end();
1469  }
1470 
1472  formula operator[](unsigned i) const
1473  {
1474  return formula(ptr_->nth(i)->clone());
1475  }
1476 #endif
1477 
1479  static formula ff()
1480  {
1481  return formula(fnode::ff());
1482  }
1483 
1485  bool is_ff() const
1486  {
1487  return ptr_->is_ff();
1488  }
1489 
1491  static formula tt()
1492  {
1493  return formula(fnode::tt());
1494  }
1495 
1497  bool is_tt() const
1498  {
1499  return ptr_->is_tt();
1500  }
1501 
1503  static formula eword()
1504  {
1505  return formula(fnode::eword());
1506  }
1507 
1509  bool is_eword() const
1510  {
1511  return ptr_->is_eword();
1512  }
1513 
1515  bool is_constant() const
1516  {
1517  return ptr_->is_constant();
1518  }
1519 
1524  bool is_Kleene_star() const
1525  {
1526  return ptr_->is_Kleene_star();
1527  }
1528 
1531  {
1532  return formula(fnode::one_star()->clone());
1533  }
1534 
1537  bool is_literal()
1538  {
1539  return (is(op::ap) ||
1540  // If f is in nenoform, Not can only occur in front of
1541  // an atomic proposition. So this way we do not have
1542  // to check the type of the child.
1543  (is(op::Not) && is_boolean() && is_in_nenoform()));
1544  }
1545 
1549  const std::string& ap_name() const
1550  {
1551  return ptr_->ap_name();
1552  }
1553 
1558  std::ostream& dump(std::ostream& os) const
1559  {
1560  return ptr_->dump(os);
1561  }
1562 
1568  formula all_but(unsigned i) const
1569  {
1570  return formula(ptr_->all_but(i));
1571  }
1572 
1582  unsigned boolean_count() const
1583  {
1584  return ptr_->boolean_count();
1585  }
1586 
1600  formula boolean_operands(unsigned* width = nullptr) const
1601  {
1602  return formula(ptr_->boolean_operands(width));
1603  }
1604 
1605 #define SPOT_DEF_PROP(Name) \
1606  bool Name() const \
1607  { \
1608  return ptr_->Name(); \
1609  }
1610  // Properties //
1613 
1615  SPOT_DEF_PROP(is_boolean);
1617  SPOT_DEF_PROP(is_sugar_free_boolean);
1622  SPOT_DEF_PROP(is_in_nenoform);
1624  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1626  SPOT_DEF_PROP(is_sugar_free_ltl);
1628  SPOT_DEF_PROP(is_ltl_formula);
1630  SPOT_DEF_PROP(is_psl_formula);
1632  SPOT_DEF_PROP(is_sere_formula);
1635  SPOT_DEF_PROP(is_finite);
1643  SPOT_DEF_PROP(is_eventual);
1651  SPOT_DEF_PROP(is_universal);
1653  SPOT_DEF_PROP(is_syntactic_safety);
1655  SPOT_DEF_PROP(is_syntactic_guarantee);
1657  SPOT_DEF_PROP(is_syntactic_obligation);
1659  SPOT_DEF_PROP(is_syntactic_recurrence);
1661  SPOT_DEF_PROP(is_syntactic_persistence);
1664  SPOT_DEF_PROP(is_marked);
1666  SPOT_DEF_PROP(accepts_eword);
1672  SPOT_DEF_PROP(has_lbt_atomic_props);
1681  SPOT_DEF_PROP(has_spin_atomic_props);
1682 #undef SPOT_DEF_PROP
1683 
1687  template<typename Trans, typename... Args>
1688  formula map(Trans trans, Args&&... args)
1689  {
1690  switch (op o = kind())
1691  {
1692  case op::ff:
1693  case op::tt:
1694  case op::eword:
1695  case op::ap:
1696  return *this;
1697  case op::Not:
1698  case op::X:
1699 #if SPOT_HAS_STRONG_X
1700  case op::strong_X:
1701 #endif
1702  case op::F:
1703  case op::G:
1704  case op::Closure:
1705  case op::NegClosure:
1706  case op::NegClosureMarked:
1707  case op::first_match:
1708  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1709  case op::Xor:
1710  case op::Implies:
1711  case op::Equiv:
1712  case op::U:
1713  case op::R:
1714  case op::W:
1715  case op::M:
1716  case op::EConcat:
1717  case op::EConcatMarked:
1718  case op::UConcat:
1719  {
1720  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1721  return binop(o, tmp,
1722  trans((*this)[1], std::forward<Args>(args)...));
1723  }
1724  case op::Or:
1725  case op::OrRat:
1726  case op::And:
1727  case op::AndRat:
1728  case op::AndNLM:
1729  case op::Concat:
1730  case op::Fusion:
1731  {
1732  std::vector<formula> tmp;
1733  tmp.reserve(size());
1734  for (auto f: *this)
1735  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1736  return multop(o, std::move(tmp));
1737  }
1738  case op::Star:
1739  case op::FStar:
1740  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1741  min(), max());
1742  }
1743  SPOT_UNREACHABLE();
1744  }
1745 
1754  template<typename Func, typename... Args>
1755  void traverse(Func func, Args&&... args)
1756  {
1757  if (func(*this, std::forward<Args>(args)...))
1758  return;
1759  for (auto f: *this)
1760  f.traverse(func, std::forward<Args>(args)...);
1761  }
1762 
1763  private:
1764 #ifndef SWIG
1765  [[noreturn]] static void report_ap_invalid_arg();
1766 #endif
1767  };
1768 
1770  SPOT_API
1771  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1772  bool abbreviated = false);
1773 
1775  SPOT_API
1776  std::list<std::string> list_formula_props(const formula& f);
1777 
1779  SPOT_API
1780  std::ostream& operator<<(std::ostream& os, const formula& f);
1781 }
1782 
1783 #ifndef SWIG
1784 namespace std
1785 {
1786  template <>
1787  struct hash<spot::formula>
1788  {
1789  size_t operator()(const spot::formula& x) const noexcept
1790  {
1791  return x.id();
1792  }
1793  };
1794 }
1795 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1099
const fnode *const * begin() const
Definition: formula.hh:271
Definition: automata.hh:26
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1530
~formula()
Destroy a formula.
Definition: formula.hh:749
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1010
bool is_boolean() const
Definition: formula.hh:387
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1460
static const fnode * eword()
Definition: formula.hh:315
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:1515
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1558
unsigned max() const
Definition: formula.hh:245
size_t id() const
Definition: formula.hh:265
PSL Closure.
bool is(op o) const
Definition: formula.hh:189
bool is_psl_formula() const
Definition: formula.hh:423
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1381
bool is_leaf() const
Definition: formula.hh:259
bool is_finite() const
Definition: formula.hh:435
bool is_eword() const
Definition: formula.hh:321
unsigned boolean_count() const
Definition: formula.hh:358
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:851
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition: formula.hh:947
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:734
static formula tt()
Return the true constant.
Definition: formula.hh:1491
const fnode * get_child_of(op o) const
Definition: formula.hh:214
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition: formula.hh:958
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1373
Definition: bitset.hh:405
Empty word.
bool is_syntactic_guarantee() const
Definition: formula.hh:459
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1485
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1549
static const fnode * tt()
Definition: formula.hh:303
bool is_syntactic_persistence() const
Definition: formula.hh:477
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1005
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1000
const fnode * nth(unsigned i) const
Definition: formula.hh:283
bool is_marked() const
Definition: formula.hh:483
Concatenation.
bool is_syntactic_recurrence() const
Definition: formula.hh:471
bool is(std::initializer_list< op > l) const
Definition: formula.hh:201
Main class for temporal logic formula.
Definition: formula.hh:704
bool is_syntactic_obligation() const
Definition: formula.hh:465
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:195
bool has_spin_atomic_props() const
Definition: formula.hh:501
release (dual of until)
bool is_constant() const
Definition: formula.hh:327
unsigned size() const
Return the number of children.
Definition: formula.hh:1387
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1537
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:878
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:405
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:1337
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1524
size_t id() const
Return the id of a formula.
Definition: formula.hh:1409
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1324
void destroy() const
Dereference an fnode.
Definition: formula.hh:148
static formula ff()
Return the false constant.
Definition: formula.hh:1479
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:1245
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1110
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:291
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:1509
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:1188
static const fnode * one_star()
Definition: formula.hh:341
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:722
bool is_syntactic_safety() const
Definition: formula.hh:453
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1318
Exclusive Or.
marked version of the Negated PSL Closure
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition: formula.hh:915
bool is_sugar_free_boolean() const
Definition: formula.hh:393
static formula eword()
Return the empty word constant.
Definition: formula.hh:1503
bool is_ltl_formula() const
Definition: formula.hh:417
Definition: formula.hh:632
bool is_in_nenoform() const
Definition: formula.hh:399
first_match(sere)
bool is_ff() const
Definition: formula.hh:297
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1497
(omega-Rational) Or
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:712
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:845
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:224
static constexpr uint8_t unbounded()
Definition: formula.hh:158
unsigned size() const
Definition: formula.hh:253
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:762
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:134
bool has_lbt_atomic_props() const
Definition: formula.hh:495
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1472
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1303
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:861
bool is_sugar_free_ltl() const
Definition: formula.hh:411
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:429
op
Operator types.
Definition: formula.hh:78
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:872
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1396
bool is_tt() const
Definition: formula.hh:309
const fnode *const * end() const
Definition: formula.hh:277
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:1180
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1346
Implication.
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1582
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1755
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:180
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1466
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
bool is_eventual() const
Definition: formula.hh:441
unsigned min() const
Definition: formula.hh:237
bool is_universal() const
Definition: formula.hh:447
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1600
Negated PSL Closure.
Rational And.
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1568
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:994
op kind() const
Return top-most operator.
Definition: formula.hh:1312
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:489
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:333
Atomic proposition.
Eventually.
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:742
(omega-Rational) And
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1688
Rational Or.
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:728

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