spot  2.10.0.dev
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015-2021 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
127  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  unsigned min, unsigned 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 
190  bool is(op o) const
191  {
192  return op_ == o;
193  }
194 
195  bool is(op o1, op o2) const
196  {
197  return op_ == o1 || op_ == o2;
198  }
199 
200  bool is(op o1, op o2, op o3) const
201  {
202  return op_ == o1 || op_ == o2 || op_ == o3;
203  }
204 
205  bool is(op o1, op o2, op o3, op o4) const
206  {
207  return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
208  }
209 
210  bool is(std::initializer_list<op> l) const
211  {
212  const fnode* n = this;
213  for (auto o: l)
214  {
215  if (!n->is(o))
216  return false;
217  n = n->nth(0);
218  }
219  return true;
220  }
222 
224  const fnode* get_child_of(op o) const
225  {
226  if (op_ != o)
227  return nullptr;
228  if (SPOT_UNLIKELY(size_ != 1))
229  report_get_child_of_expecting_single_child_node();
230  return nth(0);
231  }
232 
234  const fnode* get_child_of(std::initializer_list<op> l) const
235  {
236  auto c = this;
237  for (auto o: l)
238  {
239  c = c->get_child_of(o);
240  if (c == nullptr)
241  return c;
242  }
243  return c;
244  }
245 
247  unsigned min() const
248  {
249  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
250  report_min_invalid_arg();
251  return min_;
252  }
253 
255  unsigned max() const
256  {
257  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
258  report_max_invalid_arg();
259  return max_;
260  }
261 
263  unsigned size() const
264  {
265  return size_;
266  }
267 
269  bool is_leaf() const
270  {
271  return size_ == 0;
272  }
273 
275  size_t id() const
276  {
277  return id_;
278  }
279 
281  const fnode*const* begin() const
282  {
283  return children;
284  }
285 
287  const fnode*const* end() const
288  {
289  return children + size();
290  }
291 
293  const fnode* nth(unsigned i) const
294  {
295  if (SPOT_UNLIKELY(i >= size()))
296  report_non_existing_child();
297  return children[i];
298  }
299 
301  static const fnode* ff()
302  {
303  return ff_;
304  }
305 
307  bool is_ff() const
308  {
309  return op_ == op::ff;
310  }
311 
313  static const fnode* tt()
314  {
315  return tt_;
316  }
317 
319  bool is_tt() const
320  {
321  return op_ == op::tt;
322  }
323 
325  static const fnode* eword()
326  {
327  return ew_;
328  }
329 
331  bool is_eword() const
332  {
333  return op_ == op::eword;
334  }
335 
337  bool is_constant() const
338  {
339  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
340  }
341 
343  bool is_Kleene_star() const
344  {
345  if (op_ != op::Star)
346  return false;
347  return min_ == 0 && max_ == unbounded();
348  }
349 
351  static const fnode* one_star()
352  {
353  if (!one_star_)
354  one_star_ = bunop(op::Star, tt(), 0);
355  return one_star_;
356  }
357 
359  const std::string& ap_name() const;
360 
362  std::ostream& dump(std::ostream& os) const;
363 
365  const fnode* all_but(unsigned i) const;
366 
368  unsigned boolean_count() const
369  {
370  unsigned pos = 0;
371  unsigned s = size();
372  while (pos < s && children[pos]->is_boolean())
373  ++pos;
374  return pos;
375  }
376 
378  const fnode* boolean_operands(unsigned* width = nullptr) const;
379 
390  static bool instances_check();
391 
393  // Properties //
395 
397  bool is_boolean() const
398  {
399  return is_.boolean;
400  }
401 
404  {
405  return is_.sugar_free_boolean;
406  }
407 
409  bool is_in_nenoform() const
410  {
411  return is_.in_nenoform;
412  }
413 
416  {
417  return is_.syntactic_si;
418  }
419 
421  bool is_sugar_free_ltl() const
422  {
423  return is_.sugar_free_ltl;
424  }
425 
427  bool is_ltl_formula() const
428  {
429  return is_.ltl_formula;
430  }
431 
433  bool is_psl_formula() const
434  {
435  return is_.psl_formula;
436  }
437 
439  bool is_sere_formula() const
440  {
441  return is_.sere_formula;
442  }
443 
445  bool is_finite() const
446  {
447  return is_.finite;
448  }
449 
451  bool is_eventual() const
452  {
453  return is_.eventual;
454  }
455 
457  bool is_universal() const
458  {
459  return is_.universal;
460  }
461 
463  bool is_syntactic_safety() const
464  {
465  return is_.syntactic_safety;
466  }
467 
470  {
471  return is_.syntactic_guarantee;
472  }
473 
476  {
477  return is_.syntactic_obligation;
478  }
479 
482  {
483  return is_.syntactic_recurrence;
484  }
485 
488  {
489  return is_.syntactic_persistence;
490  }
491 
493  bool is_marked() const
494  {
495  return !is_.not_marked;
496  }
497 
499  bool accepts_eword() const
500  {
501  return is_.accepting_eword;
502  }
503 
505  bool has_lbt_atomic_props() const
506  {
507  return is_.lbt_atomic_props;
508  }
509 
512  {
513  return is_.spin_atomic_props;
514  }
515 
516  private:
517  static size_t bump_next_id();
518  void setup_props(op o);
519  void destroy_aux() const;
520 
521  [[noreturn]] static void report_non_existing_child();
522  [[noreturn]] static void report_too_many_children();
523  [[noreturn]] static void
524  report_get_child_of_expecting_single_child_node();
525  [[noreturn]] static void report_min_invalid_arg();
526  [[noreturn]] static void report_max_invalid_arg();
527 
528  static const fnode* unique(fnode*);
529 
530  // Destruction may only happen via destroy().
531  ~fnode() = default;
532  // Disallow copies.
533  fnode(const fnode&) = delete;
534  fnode& operator=(const fnode&) = delete;
535 
536 
537 
538  template<class iter>
539  fnode(op o, iter begin, iter end)
540  // Clang has some optimization where is it able to combine the
541  // 4 movb initializing op_,min_,max_,saturated_ into a single
542  // movl. Also it can optimize the three byte-comparisons of
543  // is_Kleene_star() into a single masked 32-bit comparison.
544  // The latter optimization triggers warnings from valgrind if
545  // min_ and max_ are not initialized. So to benefit from the
546  // initialization optimization and the is_Kleene_star()
547  // optimization in Clang, we always initialize min_ and max_
548  // with this compiler. Do not do it the rest of the time,
549  // since the optimization is not done.
550  : op_(o),
551 #if __llvm__
552  min_(0), max_(0),
553 #endif
554  saturated_(0)
555  {
556  size_t s = std::distance(begin, end);
557  if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
558  report_too_many_children();
559  size_ = s;
560  auto pos = children;
561  for (auto i = begin; i != end; ++i)
562  *pos++ = *i;
563  setup_props(o);
564  }
565 
566  fnode(op o, std::initializer_list<const fnode*> l)
567  : fnode(o, l.begin(), l.end())
568  {
569  }
570 
571  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
572  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
573  {
574  children[0] = f;
575  setup_props(o);
576  }
577 
578  static const fnode* ff_;
579  static const fnode* tt_;
580  static const fnode* ew_;
581  static const fnode* one_star_;
582 
583  op op_; // operator
584  uint8_t min_; // range minimum (for star-like operators)
585  uint8_t max_; // range maximum;
586  mutable uint8_t saturated_;
587  uint16_t size_; // number of children
588  mutable uint16_t refs_ = 0; // reference count - 1;
589  size_t id_; // Also used as hash.
590  static size_t next_id_;
591 
592  struct ltl_prop
593  {
594  // All properties here should be expressed in such a a way
595  // that property(f && g) is just property(f)&property(g).
596  // This allows us to compute all properties of a compound
597  // formula in one operation.
598  //
599  // For instance we do not use a property that says "has
600  // temporal operator", because it would require an OR between
601  // the two arguments. Instead we have a property that
602  // says "no temporal operator", and that one is computed
603  // with an AND between the arguments.
604  //
605  // Also choose a name that makes sense when prefixed with
606  // "the formula is".
607  bool boolean:1; // No temporal operators.
608  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
609  bool in_nenoform:1; // Negative Normal Form.
610  bool syntactic_si:1; // LTL-X or siPSL
611  bool sugar_free_ltl:1; // No F and G operators.
612  bool ltl_formula:1; // Only LTL operators.
613  bool psl_formula:1; // Only PSL operators.
614  bool sere_formula:1; // Only SERE operators.
615  bool finite:1; // Finite SERE formulae, or Bool+X forms.
616  bool eventual:1; // Purely eventual formula.
617  bool universal:1; // Purely universal formula.
618  bool syntactic_safety:1; // Syntactic Safety Property.
619  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
620  bool syntactic_obligation:1; // Syntactic Obligation Property.
621  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
622  bool syntactic_persistence:1; // Syntactic Persistence Property.
623  bool not_marked:1; // No occurrence of EConcatMarked.
624  bool accepting_eword:1; // Accepts the empty word.
625  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
626  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
627  };
628  union
629  {
630  // Use an unsigned for fast computation of all properties.
631  unsigned props;
632  ltl_prop is_;
633  };
634 
635  const fnode* children[1];
636  };
637 
639  SPOT_API
640  int atomic_prop_cmp(const fnode* f, const fnode* g);
641 
643  {
644  bool
645  operator()(const fnode* left, const fnode* right) const
646  {
647  SPOT_ASSERT(left);
648  SPOT_ASSERT(right);
649  if (left == right)
650  return false;
651 
652  // We want Boolean formulae first.
653  bool lib = left->is_boolean();
654  if (lib != right->is_boolean())
655  return lib;
656 
657  // We have two Boolean formulae
658  if (lib)
659  {
660  bool lconst = left->is_constant();
661  if (lconst != right->is_constant())
662  return lconst;
663  if (!lconst)
664  {
665  auto get_literal = [](const fnode* f) -> const fnode*
666  {
667  if (f->is(op::Not))
668  f = f->nth(0);
669  if (f->is(op::ap))
670  return f;
671  return nullptr;
672  };
673  // Literals should come first
674  const fnode* litl = get_literal(left);
675  const fnode* litr = get_literal(right);
676  if (!litl != !litr)
677  return litl;
678  if (litl)
679  {
680  // And they should be sorted alphabetically
681  int cmp = atomic_prop_cmp(litl, litr);
682  if (cmp)
683  return cmp < 0;
684  }
685  }
686  }
687 
688  size_t l = left->id();
689  size_t r = right->id();
690  if (l != r)
691  return l < r;
692  // Because the hash code assigned to each formula is the
693  // number of formulae constructed so far, it is very unlikely
694  // that we will ever reach a case were two different formulae
695  // have the same hash. This will happen only ever with have
696  // produced 256**sizeof(size_t) formulae (i.e. max_count has
697  // looped back to 0 and started over). In that case we can
698  // order two formulas by looking at their text representation.
699  // We could be more efficient and look at their AST, but it's
700  // not worth the burden. (Also ordering pointers is ruled out
701  // because it breaks the determinism of the implementation.)
702  std::ostringstream old;
703  left->dump(old);
704  std::ostringstream ord;
705  right->dump(ord);
706  return old.str() < ord.str();
707  }
708  };
709 
710 #endif // SWIG
711 
714  class SPOT_API formula final
715  {
716  const fnode* ptr_;
717  public:
722  explicit formula(const fnode* f) noexcept
723  : ptr_(f)
724  {
725  }
726 
732  formula(std::nullptr_t) noexcept
733  : ptr_(nullptr)
734  {
735  }
736 
738  formula() noexcept
739  : ptr_(nullptr)
740  {
741  }
742 
744  formula(const formula& f) noexcept
745  : ptr_(f.ptr_)
746  {
747  if (ptr_)
748  ptr_->clone();
749  }
750 
752  formula(formula&& f) noexcept
753  : ptr_(f.ptr_)
754  {
755  f.ptr_ = nullptr;
756  }
757 
760  {
761  if (ptr_)
762  ptr_->destroy();
763  }
764 
772  const formula& operator=(std::nullptr_t)
773  {
774  this->~formula();
775  ptr_ = nullptr;
776  return *this;
777  }
778 
779  const formula& operator=(const formula& f)
780  {
781  this->~formula();
782  if ((ptr_ = f.ptr_))
783  ptr_->clone();
784  return *this;
785  }
786 
787  const formula& operator=(formula&& f) noexcept
788  {
789  std::swap(f.ptr_, ptr_);
790  return *this;
791  }
792 
793  bool operator<(const formula& other) const noexcept
794  {
795  if (SPOT_UNLIKELY(!other.ptr_))
796  return false;
797  if (SPOT_UNLIKELY(!ptr_))
798  return true;
799  if (id() < other.id())
800  return true;
801  if (id() > other.id())
802  return false;
803  // The case where id()==other.id() but ptr_ != other.ptr_ is
804  // very unlikely (we would need to build more than UINT_MAX
805  // formulas), so let's just compare pointers, and ignore the
806  // fact that it may introduce some nondeterminism.
807  return ptr_ < other.ptr_;
808  }
809 
810  bool operator<=(const formula& other) const noexcept
811  {
812  return *this == other || *this < other;
813  }
814 
815  bool operator>(const formula& other) const noexcept
816  {
817  return !(*this <= other);
818  }
819 
820  bool operator>=(const formula& other) const noexcept
821  {
822  return !(*this < other);
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  bool operator!=(const formula& other) const noexcept
836  {
837  return other.ptr_ != ptr_;
838  }
839 
840  bool operator!=(std::nullptr_t) const noexcept
841  {
842  return ptr_ != nullptr;
843  }
844 
845  explicit operator bool() const noexcept
846  {
847  return ptr_ != nullptr;
848  }
849 
851  // Forwarded functions //
853 
855  static constexpr uint8_t unbounded()
856  {
857  return fnode::unbounded();
858  }
859 
861  static formula ap(const std::string& name)
862  {
863  return formula(fnode::ap(name));
864  }
865 
871  static formula ap(const formula& a)
872  {
873  if (SPOT_UNLIKELY(a.kind() != op::ap))
874  report_ap_invalid_arg();
875  return a;
876  }
877 
882  static formula unop(op o, const formula& f)
883  {
884  return formula(fnode::unop(o, f.ptr_->clone()));
885  }
886 
887 #ifndef SWIG
888  static formula unop(op o, formula&& f)
889  {
890  return formula(fnode::unop(o, f.to_node_()));
891  }
892 #endif // !SWIG
894 
895 #ifdef SWIG
896 #define SPOT_DEF_UNOP(Name) \
897  static formula Name(const formula& f) \
898  { \
899  return unop(op::Name, f); \
900  }
901 #else // !SWIG
902 #define SPOT_DEF_UNOP(Name) \
903  static formula Name(const formula& f) \
904  { \
905  return unop(op::Name, f); \
906  } \
907  static formula Name(formula&& f) \
908  { \
909  return unop(op::Name, std::move(f)); \
910  }
911 #endif // !SWIG
914  SPOT_DEF_UNOP(Not);
916 
919  SPOT_DEF_UNOP(X);
921 
925  static formula X(unsigned level, const formula& f)
926  {
927  return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
928  }
929 
930 #if SPOT_WANT_STRONG_X
933  SPOT_DEF_UNOP(strong_X);
935 
939  static formula strong_X(unsigned level, const formula& f)
940  {
941  return nested_unop_range(op::strong_X, op::Or /* unused */,
942  level, level, f);
943  }
944 #endif
945 
948  SPOT_DEF_UNOP(F);
950 
957  static formula F(unsigned min_level, unsigned max_level, const formula& f)
958  {
959  return nested_unop_range(op::X, op::Or, min_level, max_level, f);
960  }
961 
968  static formula G(unsigned min_level, unsigned max_level, const formula& f)
969  {
970  return nested_unop_range(op::X, op::And, min_level, max_level, f);
971  }
972 
975  SPOT_DEF_UNOP(G);
977 
980  SPOT_DEF_UNOP(Closure);
982 
985  SPOT_DEF_UNOP(NegClosure);
987 
990  SPOT_DEF_UNOP(NegClosureMarked);
992 
995  SPOT_DEF_UNOP(first_match);
997 #undef SPOT_DEF_UNOP
998 
1004  static formula binop(op o, const formula& f, const formula& g)
1005  {
1006  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
1007  }
1008 
1009 #ifndef SWIG
1010  static formula binop(op o, const formula& f, formula&& g)
1011  {
1012  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
1013  }
1014 
1015  static formula binop(op o, formula&& f, const formula& g)
1016  {
1017  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
1018  }
1019 
1020  static formula binop(op o, formula&& f, formula&& g)
1021  {
1022  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
1023  }
1025 
1026 #endif //SWIG
1027 
1028 #ifdef SWIG
1029 #define SPOT_DEF_BINOP(Name) \
1030  static formula Name(const formula& f, const formula& g) \
1031  { \
1032  return binop(op::Name, f, g); \
1033  }
1034 #else // !SWIG
1035 #define SPOT_DEF_BINOP(Name) \
1036  static formula Name(const formula& f, const formula& g) \
1037  { \
1038  return binop(op::Name, f, g); \
1039  } \
1040  static formula Name(const formula& f, formula&& g) \
1041  { \
1042  return binop(op::Name, f, std::move(g)); \
1043  } \
1044  static formula Name(formula&& f, const formula& g) \
1045  { \
1046  return binop(op::Name, std::move(f), g); \
1047  } \
1048  static formula Name(formula&& f, formula&& g) \
1049  { \
1050  return binop(op::Name, std::move(f), std::move(g)); \
1051  }
1052 #endif // !SWIG
1055  SPOT_DEF_BINOP(Xor);
1057 
1060  SPOT_DEF_BINOP(Implies);
1062 
1065  SPOT_DEF_BINOP(Equiv);
1067 
1070  SPOT_DEF_BINOP(U);
1072 
1075  SPOT_DEF_BINOP(R);
1077 
1080  SPOT_DEF_BINOP(W);
1082 
1085  SPOT_DEF_BINOP(M);
1087 
1090  SPOT_DEF_BINOP(EConcat);
1092 
1095  SPOT_DEF_BINOP(EConcatMarked);
1097 
1100  SPOT_DEF_BINOP(UConcat);
1102 #undef SPOT_DEF_BINOP
1103 
1109  static formula multop(op o, const std::vector<formula>& l)
1110  {
1111  std::vector<const fnode*> tmp;
1112  tmp.reserve(l.size());
1113  for (auto f: l)
1114  if (f.ptr_)
1115  tmp.emplace_back(f.ptr_->clone());
1116  return formula(fnode::multop(o, std::move(tmp)));
1117  }
1118 
1119 #ifndef SWIG
1120  static formula multop(op o, std::vector<formula>&& l)
1121  {
1122  std::vector<const fnode*> tmp;
1123  tmp.reserve(l.size());
1124  for (auto f: l)
1125  if (f.ptr_)
1126  tmp.emplace_back(f.to_node_());
1127  return formula(fnode::multop(o, std::move(tmp)));
1128  }
1129 #endif // !SWIG
1131 
1132 #ifdef SWIG
1133 #define SPOT_DEF_MULTOP(Name) \
1134  static formula Name(const std::vector<formula>& l) \
1135  { \
1136  return multop(op::Name, l); \
1137  }
1138 #else // !SWIG
1139 #define SPOT_DEF_MULTOP(Name) \
1140  static formula Name(const std::vector<formula>& l) \
1141  { \
1142  return multop(op::Name, l); \
1143  } \
1144  \
1145  static formula Name(std::vector<formula>&& l) \
1146  { \
1147  return multop(op::Name, std::move(l)); \
1148  }
1149 #endif // !SWIG
1152  SPOT_DEF_MULTOP(Or);
1154 
1157  SPOT_DEF_MULTOP(OrRat);
1159 
1162  SPOT_DEF_MULTOP(And);
1164 
1167  SPOT_DEF_MULTOP(AndRat);
1169 
1172  SPOT_DEF_MULTOP(AndNLM);
1174 
1177  SPOT_DEF_MULTOP(Concat);
1179 
1182  SPOT_DEF_MULTOP(Fusion);
1184 #undef SPOT_DEF_MULTOP
1185 
1190  static formula bunop(op o, const formula& f,
1191  unsigned min = 0U,
1192  unsigned max = unbounded())
1193  {
1194  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1195  }
1196 
1197 #ifndef SWIG
1198  static formula bunop(op o, formula&& f,
1199  unsigned min = 0U,
1200  unsigned max = unbounded())
1201  {
1202  return formula(fnode::bunop(o, f.to_node_(), min, max));
1203  }
1204 #endif // !SWIG
1206 
1207 #if SWIG
1208 #define SPOT_DEF_BUNOP(Name) \
1209  static formula Name(const formula& f, \
1210  unsigned min = 0U, \
1211  unsigned max = unbounded()) \
1212  { \
1213  return bunop(op::Name, f, min, max); \
1214  }
1215 #else // !SWIG
1216 #define SPOT_DEF_BUNOP(Name) \
1217  static formula Name(const formula& f, \
1218  unsigned min = 0U, \
1219  unsigned max = unbounded()) \
1220  { \
1221  return bunop(op::Name, f, min, max); \
1222  } \
1223  static formula Name(formula&& f, \
1224  unsigned min = 0U, \
1225  unsigned max = unbounded()) \
1226  { \
1227  return bunop(op::Name, std::move(f), min, max); \
1228  }
1229 #endif
1232  SPOT_DEF_BUNOP(Star);
1234 
1240  SPOT_DEF_BUNOP(FStar);
1242 #undef SPOT_DEF_BUNOP
1243 
1255  static const formula nested_unop_range(op uo, op bo, unsigned min,
1256  unsigned max, formula f)
1257  {
1258  return formula(fnode::nested_unop_range(uo, bo, min, max,
1259  f.ptr_->clone()));
1260  }
1261 
1267  static formula sugar_goto(const formula& b, unsigned min, unsigned max);
1268 
1274  static formula sugar_equal(const formula& b, unsigned min, unsigned max);
1275 
1297  static formula sugar_delay(const formula& a, const formula& b,
1298  unsigned min, unsigned max);
1299  static formula sugar_delay(const formula& b,
1300  unsigned min, unsigned max);
1302 
1303 #ifndef SWIG
1313  const fnode* to_node_()
1314  {
1315  auto tmp = ptr_;
1316  ptr_ = nullptr;
1317  return tmp;
1318  }
1319 #endif
1320 
1322  op kind() const
1323  {
1324  return ptr_->kind();
1325  }
1326 
1328  std::string kindstr() const
1329  {
1330  return ptr_->kindstr();
1331  }
1332 
1334  bool is(op o) const
1335  {
1336  return ptr_->is(o);
1337  }
1338 
1339 #ifndef SWIG
1341  bool is(op o1, op o2) const
1342  {
1343  return ptr_->is(o1, o2);
1344  }
1345 
1347  bool is(op o1, op o2, op o3) const
1348  {
1349  return ptr_->is(o1, o2, o3);
1350  }
1351 
1354  bool is(op o1, op o2, op o3, op o4) const
1355  {
1356  return ptr_->is(o1, o2, o3, o4);
1357  }
1358 
1360  bool is(std::initializer_list<op> l) const
1361  {
1362  return ptr_->is(l);
1363  }
1364 #endif
1365 
1370  {
1371  auto f = ptr_->get_child_of(o);
1372  if (f)
1373  f->clone();
1374  return formula(f);
1375  }
1376 
1377 #ifndef SWIG
1384  formula get_child_of(std::initializer_list<op> l) const
1385  {
1386  auto f = ptr_->get_child_of(l);
1387  if (f)
1388  f->clone();
1389  return formula(f);
1390  }
1391 #endif
1392 
1396  unsigned min() const
1397  {
1398  return ptr_->min();
1399  }
1400 
1404  unsigned max() const
1405  {
1406  return ptr_->max();
1407  }
1408 
1410  unsigned size() const
1411  {
1412  return ptr_->size();
1413  }
1414 
1419  bool is_leaf() const
1420  {
1421  return ptr_->is_leaf();
1422  }
1423 
1432  size_t id() const
1433  {
1434  return ptr_->id();
1435  }
1436 
1437 #ifndef SWIG
1439  class SPOT_API formula_child_iterator final
1440  {
1441  const fnode*const* ptr_;
1442  public:
1444  : ptr_(nullptr)
1445  {
1446  }
1447 
1448  formula_child_iterator(const fnode*const* f)
1449  : ptr_(f)
1450  {
1451  }
1452 
1453  bool operator==(formula_child_iterator o)
1454  {
1455  return ptr_ == o.ptr_;
1456  }
1457 
1458  bool operator!=(formula_child_iterator o)
1459  {
1460  return ptr_ != o.ptr_;
1461  }
1462 
1463  formula operator*()
1464  {
1465  return formula((*ptr_)->clone());
1466  }
1467 
1468  formula_child_iterator operator++()
1469  {
1470  ++ptr_;
1471  return *this;
1472  }
1473 
1474  formula_child_iterator operator++(int)
1475  {
1476  auto tmp = *this;
1477  ++ptr_;
1478  return tmp;
1479  }
1480  };
1481 
1484  {
1485  return ptr_->begin();
1486  }
1487 
1490  {
1491  return ptr_->end();
1492  }
1493 
1495  formula operator[](unsigned i) const
1496  {
1497  return formula(ptr_->nth(i)->clone());
1498  }
1499 #endif
1500 
1502  static formula ff()
1503  {
1504  return formula(fnode::ff());
1505  }
1506 
1508  bool is_ff() const
1509  {
1510  return ptr_->is_ff();
1511  }
1512 
1514  static formula tt()
1515  {
1516  return formula(fnode::tt());
1517  }
1518 
1520  bool is_tt() const
1521  {
1522  return ptr_->is_tt();
1523  }
1524 
1526  static formula eword()
1527  {
1528  return formula(fnode::eword());
1529  }
1530 
1532  bool is_eword() const
1533  {
1534  return ptr_->is_eword();
1535  }
1536 
1538  bool is_constant() const
1539  {
1540  return ptr_->is_constant();
1541  }
1542 
1547  bool is_Kleene_star() const
1548  {
1549  return ptr_->is_Kleene_star();
1550  }
1551 
1554  {
1555  return formula(fnode::one_star()->clone());
1556  }
1557 
1560  bool is_literal()
1561  {
1562  return (is(op::ap) ||
1563  // If f is in nenoform, Not can only occur in front of
1564  // an atomic proposition. So this way we do not have
1565  // to check the type of the child.
1566  (is(op::Not) && is_boolean() && is_in_nenoform()));
1567  }
1568 
1572  const std::string& ap_name() const
1573  {
1574  return ptr_->ap_name();
1575  }
1576 
1581  std::ostream& dump(std::ostream& os) const
1582  {
1583  return ptr_->dump(os);
1584  }
1585 
1591  formula all_but(unsigned i) const
1592  {
1593  return formula(ptr_->all_but(i));
1594  }
1595 
1605  unsigned boolean_count() const
1606  {
1607  return ptr_->boolean_count();
1608  }
1609 
1623  formula boolean_operands(unsigned* width = nullptr) const
1624  {
1625  return formula(ptr_->boolean_operands(width));
1626  }
1627 
1628 #define SPOT_DEF_PROP(Name) \
1629  bool Name() const \
1630  { \
1631  return ptr_->Name(); \
1632  }
1634  // Properties //
1636 
1638  SPOT_DEF_PROP(is_boolean);
1640  SPOT_DEF_PROP(is_sugar_free_boolean);
1645  SPOT_DEF_PROP(is_in_nenoform);
1647  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1649  SPOT_DEF_PROP(is_sugar_free_ltl);
1651  SPOT_DEF_PROP(is_ltl_formula);
1653  SPOT_DEF_PROP(is_psl_formula);
1655  SPOT_DEF_PROP(is_sere_formula);
1658  SPOT_DEF_PROP(is_finite);
1666  SPOT_DEF_PROP(is_eventual);
1674  SPOT_DEF_PROP(is_universal);
1676  SPOT_DEF_PROP(is_syntactic_safety);
1678  SPOT_DEF_PROP(is_syntactic_guarantee);
1680  SPOT_DEF_PROP(is_syntactic_obligation);
1682  SPOT_DEF_PROP(is_syntactic_recurrence);
1684  SPOT_DEF_PROP(is_syntactic_persistence);
1687  SPOT_DEF_PROP(is_marked);
1689  SPOT_DEF_PROP(accepts_eword);
1695  SPOT_DEF_PROP(has_lbt_atomic_props);
1704  SPOT_DEF_PROP(has_spin_atomic_props);
1705 #undef SPOT_DEF_PROP
1706 
1710  template<typename Trans, typename... Args>
1711  formula map(Trans trans, Args&&... args)
1712  {
1713  switch (op o = kind())
1714  {
1715  case op::ff:
1716  case op::tt:
1717  case op::eword:
1718  case op::ap:
1719  return *this;
1720  case op::Not:
1721  case op::X:
1722 #if SPOT_HAS_STRONG_X
1723  case op::strong_X:
1724 #endif
1725  case op::F:
1726  case op::G:
1727  case op::Closure:
1728  case op::NegClosure:
1729  case op::NegClosureMarked:
1730  case op::first_match:
1731  return unop(o, trans((*this)[0], std::forward<Args>(args)...));
1732  case op::Xor:
1733  case op::Implies:
1734  case op::Equiv:
1735  case op::U:
1736  case op::R:
1737  case op::W:
1738  case op::M:
1739  case op::EConcat:
1740  case op::EConcatMarked:
1741  case op::UConcat:
1742  {
1743  formula tmp = trans((*this)[0], std::forward<Args>(args)...);
1744  return binop(o, tmp,
1745  trans((*this)[1], std::forward<Args>(args)...));
1746  }
1747  case op::Or:
1748  case op::OrRat:
1749  case op::And:
1750  case op::AndRat:
1751  case op::AndNLM:
1752  case op::Concat:
1753  case op::Fusion:
1754  {
1755  std::vector<formula> tmp;
1756  tmp.reserve(size());
1757  for (auto f: *this)
1758  tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1759  return multop(o, std::move(tmp));
1760  }
1761  case op::Star:
1762  case op::FStar:
1763  return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
1764  min(), max());
1765  }
1766  SPOT_UNREACHABLE();
1767  }
1768 
1777  template<typename Func, typename... Args>
1778  void traverse(Func func, Args&&... args)
1779  {
1780  if (func(*this, std::forward<Args>(args)...))
1781  return;
1782  for (auto f: *this)
1783  f.traverse(func, std::forward<Args>(args)...);
1784  }
1785 
1786  private:
1787 #ifndef SWIG
1788  [[noreturn]] static void report_ap_invalid_arg();
1789 #endif
1790  };
1791 
1793  SPOT_API
1794  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1795  bool abbreviated = false);
1796 
1798  SPOT_API
1799  std::list<std::string> list_formula_props(const formula& f);
1800 
1802  SPOT_API
1803  std::ostream& operator<<(std::ostream& os, const formula& f);
1804 }
1805 
1806 #ifndef SWIG
1807 namespace std
1808 {
1809  template <>
1810  struct hash<spot::formula>
1811  {
1812  size_t operator()(const spot::formula& x) const noexcept
1813  {
1814  return x.id();
1815  }
1816  };
1817 }
1818 #endif
Actual storage for formula nodes.
Definition: formula.hh:128
const fnode *const * begin() const
Definition: formula.hh:281
const fnode *const * end() const
Definition: formula.hh:287
std::string kindstr() const
std::ostream & dump(std::ostream &os) const
bool is_boolean() const
Definition: formula.hh:397
size_t id() const
Definition: formula.hh:275
bool is_ff() const
Definition: formula.hh:307
bool is_sugar_free_boolean() const
Definition: formula.hh:403
bool is_Kleene_star() const
Definition: formula.hh:343
unsigned min() const
Definition: formula.hh:247
bool is_syntactic_safety() const
Definition: formula.hh:463
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:415
unsigned size() const
Definition: formula.hh:263
static constexpr uint8_t unbounded()
Definition: formula.hh:158
static const fnode * eword()
Definition: formula.hh:325
const fnode * get_child_of(op o) const
Definition: formula.hh:224
unsigned max() const
Definition: formula.hh:255
static const fnode * ff()
Definition: formula.hh:301
const fnode * boolean_operands(unsigned *width=nullptr) const
bool accepts_eword() const
Definition: formula.hh:499
bool is_eventual() const
Definition: formula.hh:451
const std::string & ap_name() const
bool is(op o1, op o2, op o3, op o4) const
Definition: formula.hh:205
static bool instances_check()
safety check for the reference counters
bool is_leaf() const
Definition: formula.hh:269
bool has_spin_atomic_props() const
Definition: formula.hh:511
bool is_eword() const
Definition: formula.hh:331
static const fnode * tt()
Definition: formula.hh:313
bool is(op o1, op o2, op o3) const
Definition: formula.hh:200
op kind() const
Definition: formula.hh:180
bool has_lbt_atomic_props() const
Definition: formula.hh:505
bool is_sugar_free_ltl() const
Definition: formula.hh:421
bool is_syntactic_persistence() const
Definition: formula.hh:487
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
unsigned boolean_count() const
Definition: formula.hh:368
bool is_universal() const
Definition: formula.hh:457
bool is_tt() const
Definition: formula.hh:319
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:234
const fnode * nth(unsigned i) const
Definition: formula.hh:293
bool is_constant() const
Definition: formula.hh:337
static const fnode * binop(op o, const fnode *f, const fnode *g)
static const fnode * one_star()
Definition: formula.hh:351
const fnode * all_but(unsigned i) const
bool is_syntactic_recurrence() const
Definition: formula.hh:481
bool is(std::initializer_list< op > l) const
Definition: formula.hh:210
bool is_syntactic_obligation() const
Definition: formula.hh:475
static const fnode * unop(op o, const fnode *f)
bool is_ltl_formula() const
Definition: formula.hh:427
bool is_finite() const
Definition: formula.hh:445
bool is_psl_formula() const
Definition: formula.hh:433
static const fnode * multop(op o, std::vector< const fnode * > l)
bool is_marked() const
Definition: formula.hh:493
void destroy() const
Dereference an fnode.
Definition: formula.hh:148
static const fnode * bunop(op o, const fnode *f, unsigned min, unsigned max=unbounded())
bool is(op o1, op o2) const
Definition: formula.hh:195
bool is_in_nenoform() const
Definition: formula.hh:409
static const fnode * ap(const std::string &name)
bool is_syntactic_guarantee() const
Definition: formula.hh:469
bool is_sere_formula() const
Definition: formula.hh:439
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:134
bool is(op o) const
Definition: formula.hh:190
Allow iterating over children.
Definition: formula.hh:1440
Main class for temporal logic formula.
Definition: formula.hh:715
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1605
bool is_leaf() const
Whether the formula is a leaf.
Definition: formula.hh:1419
size_t id() const
Return the id of a formula.
Definition: formula.hh:1432
static formula bunop(op o, formula &&f, unsigned min=0U, unsigned max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1198
formula map(Trans trans, Args &&... args)
Clone this node after applying trans to its children.
Definition: formula.hh:1711
static formula bunop(op o, const formula &f, unsigned min=0U, unsigned max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1190
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1560
static formula G(unsigned min_level, unsigned max_level, const formula &f)
Construct G[n:m].
Definition: formula.hh:968
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1004
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1334
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1120
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:752
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:722
bool is(op o1, op o2) const
Return true if the formula is of kind o1 or o2.
Definition: formula.hh:1341
static formula sugar_delay(const formula &b, unsigned min, unsigned max)
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1553
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1396
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:855
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:888
static formula eword()
Return the empty word constant.
Definition: formula.hh:1526
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1591
static formula ff()
Return the false constant.
Definition: formula.hh:1502
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1010
op kind() const
Return top-most operator.
Definition: formula.hh:1322
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1109
unsigned size() const
Return the number of children.
Definition: formula.hh:1410
static formula sugar_goto(const formula &b, unsigned min, unsigned max)
Create a SERE equivalent to b[->min..max].
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1520
bool is(op o1, op o2, op o3, op o4) const
Definition: formula.hh:1354
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1328
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:744
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1489
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:1020
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:871
formula get_child_of(std::initializer_list< op > l) const
Remove all operators in l and return the child.
Definition: formula.hh:1384
bool is_eword() const
Whether the formula is the empty word constant.
Definition: formula.hh:1532
static formula sugar_delay(const formula &a, const formula &b, unsigned min, unsigned max)
void traverse(Func func, Args &&... args)
Apply func to each subformula.
Definition: formula.hh:1778
static formula F(unsigned min_level, unsigned max_level, const formula &f)
Construct F[n:m].
Definition: formula.hh:957
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:732
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:861
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1572
bool is(op o1, op o2, op o3) const
Return true if the formula is of kind o1 or o2 or o3.
Definition: formula.hh:1347
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:772
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1404
static formula X(unsigned level, const formula &f)
Construct an X[n].
Definition: formula.hh:925
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1508
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1483
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition: formula.hh:1538
~formula()
Destroy a formula.
Definition: formula.hh:759
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1581
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1369
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1313
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition: formula.hh:1360
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1495
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1547
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:1015
static formula tt()
Return the true constant.
Definition: formula.hh:1514
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:738
static formula sugar_equal(const formula &b, unsigned min, unsigned max)
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:882
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1623
static const formula nested_unop_range(op uo, op bo, unsigned min, unsigned max, formula f)
Nested operator construction (syntactic sugar).
Definition: formula.hh:1255
op
Operator types.
Definition: formula.hh:79
@ X
Next.
@ first_match
first_match(sere)
@ EConcatMarked
Seq, Marked.
@ Star
Star.
@ UConcat
Triggers.
@ Or
(omega-Rational) Or
@ Equiv
Equivalence.
@ NegClosure
Negated PSL Closure.
@ U
until
@ EConcat
Seq.
@ FStar
Fustion Star.
@ W
weak until
@ ap
Atomic proposition.
@ ff
False.
@ M
strong release (dual of weak until)
@ NegClosureMarked
marked version of the Negated PSL Closure
@ Xor
Exclusive Or.
@ F
Eventually.
@ OrRat
Rational Or.
@ Not
Negation.
@ tt
True.
@ Fusion
Fusion.
@ Closure
PSL Closure.
@ And
(omega-Rational) And
@ AndNLM
Non-Length-Matching Rational-And.
@ eword
Empty word.
@ AndRat
Rational And.
@ G
Globally.
@ R
release (dual of until)
@ Concat
Concatenation.
@ Implies
Implication.
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
Definition: automata.hh:27
int atomic_prop_cmp(const fnode *f, const fnode *g)
Order two atomic propositions.
std::list< std::string > list_formula_props(const formula &f)
List the properties of formula f.
std::ostream & print_formula_props(std::ostream &out, const formula &f, bool abbreviated=false)
Print the properties of formula f on stream out.
Definition: formula.hh:643

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.9.1