spot  2.9
twa.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2009, 2011, 2013-2020 Laboratoire de Recherche et
3 // Développement de l'Epita (LRDE).
4 // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
5 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6 // Pierre et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // under the terms of the GNU General Public License as published by
12 // the Free Software Foundation; either version 3 of the License, or
13 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // You should have received a copy of the GNU General Public License
21 // along with this program. If not, see <http://www.gnu.org/licenses/>.
22 
23 #pragma once
24 
25 #include <cstddef>
26 #include <spot/twa/fwd.hh>
27 #include <spot/twa/acc.hh>
28 #include <spot/twa/bdddict.hh>
29 #include <cassert>
30 #include <memory>
31 #include <unordered_map>
32 #include <functional>
33 #include <array>
34 #include <vector>
35 #include <spot/misc/casts.hh>
36 #include <spot/misc/hash.hh>
37 #include <spot/tl/formula.hh>
38 #include <spot/misc/trival.hh>
39 
40 namespace spot
41 {
42  struct twa_run;
43  typedef std::shared_ptr<twa_run> twa_run_ptr;
44 
45  struct twa_word;
46  typedef std::shared_ptr<twa_word> twa_word_ptr;
47 
50  class SPOT_API state
51  {
52  public:
63  virtual int compare(const state* other) const = 0;
64 
84  virtual size_t hash() const = 0;
85 
87  virtual state* clone() const = 0;
88 
98  virtual void destroy() const
99  {
100  delete this;
101  }
102 
103  protected:
110  virtual ~state()
111  {
112  }
113  };
114 
128  {
129  bool
130  operator()(const state* left, const state* right) const
131  {
132  SPOT_ASSERT(left);
133  return left->compare(right) < 0;
134  }
135  };
136 
151  {
152  bool
153  operator()(const state* left, const state* right) const
154  {
155  SPOT_ASSERT(left);
156  return 0 == left->compare(right);
157  }
158  };
159 
175  {
176  size_t
177  operator()(const state* that) const
178  {
179  SPOT_ASSERT(that);
180  return that->hash();
181  }
182  };
183 
189  typedef std::unordered_set<const state*,
190  state_ptr_hash, state_ptr_equal> state_set;
191 
195  template<class val>
196  using state_map = std::unordered_map<const state*, val,
197  state_ptr_hash, state_ptr_equal>;
198 
201  class SPOT_API state_unicity_table
202  {
203  state_set m;
204  public:
205 
214  const state* operator()(const state* s)
215  {
216  auto p = m.insert(s);
217  if (!p.second)
218  s->destroy();
219  return *p.first;
220  }
221 
226  const state* is_new(const state* s)
227  {
228  auto p = m.insert(s);
229  if (!p.second)
230  {
231  s->destroy();
232  return nullptr;
233  }
234  return *p.first;
235  }
236 
238  {
239  for (state_set::iterator i = m.begin(); i != m.end();)
240  {
241  // Advance the iterator before destroying its key. This
242  // avoids issues with old g++ implementations.
243  state_set::iterator old = i++;
244  (*old)->destroy();
245  }
246  }
247 
248  size_t
249  size()
250  {
251  return m.size();
252  }
253  };
254 
255 
256 
257  // Functions related to shared_ptr.
259 
260  typedef std::shared_ptr<const state> shared_state;
261 
262  inline void shared_state_deleter(state* s) { s->destroy(); }
263 
278  {
279  bool
280  operator()(shared_state left,
281  shared_state right) const
282  {
283  SPOT_ASSERT(left);
284  return left->compare(right.get()) < 0;
285  }
286  };
287 
306  {
307  bool
308  operator()(shared_state left,
309  shared_state right) const
310  {
311  SPOT_ASSERT(left);
312  return 0 == left->compare(right.get());
313  }
314  };
315 
335  {
336  size_t
337  operator()(shared_state that) const
338  {
339  SPOT_ASSERT(that);
340  return that->hash();
341  }
342  };
343 
345  typedef std::unordered_set<shared_state,
347  state_shared_ptr_equal> shared_state_set;
348 
397  class SPOT_API twa_succ_iterator
398  {
399  public:
400  virtual
402  {
403  }
404 
407 
422  virtual bool first() = 0;
423 
434  virtual bool next() = 0;
435 
451  virtual bool done() const = 0;
452 
454 
457 
467  virtual const state* dst() const = 0;
471  virtual bdd cond() const = 0;
474  virtual acc_cond::mark_t acc() const = 0;
475 
477  };
478 
479  namespace internal
480  {
486  struct SPOT_API succ_iterator
487  {
488  protected:
489  twa_succ_iterator* it_;
490  public:
491 
493  it_(it)
494  {
495  }
496 
497  bool operator==(succ_iterator o) const
498  {
499  return it_ == o.it_;
500  }
501 
502  bool operator!=(succ_iterator o) const
503  {
504  return it_ != o.it_;
505  }
506 
507  const twa_succ_iterator* operator*() const
508  {
509  return it_;
510  }
511 
512  void operator++()
513  {
514  if (!it_->next())
515  it_ = nullptr;
516  }
517  };
518 
519 #ifndef SWIG
520  class twa_succ_iterable
526  {
527  protected:
528  const twa* aut_;
529  twa_succ_iterator* it_;
530  public:
531  twa_succ_iterable(const twa* aut, twa_succ_iterator* it)
532  : aut_(aut), it_(it)
533  {
534  }
535 
536  twa_succ_iterable(twa_succ_iterable&& other) noexcept
537  : aut_(other.aut_), it_(other.it_)
538  {
539  other.it_ = nullptr;
540  }
541 
542  ~twa_succ_iterable(); // Defined in this file after twa
543 
545  {
546  return it_->first() ? it_ : nullptr;
547  }
548 
550  {
551  return nullptr;
552  }
553  };
554 #endif // SWIG
555  }
556 
566 
569 
622  class SPOT_API twa: public std::enable_shared_from_this<twa>
623  {
624  protected:
625  twa(const bdd_dict_ptr& d);
629  bdd_dict_ptr dict_;
630  public:
631 
632  virtual ~twa();
633 
639  virtual const state* get_init_state() const = 0;
640 
648  virtual twa_succ_iterator*
649  succ_iter(const state* local_state) const = 0;
650 
651 #ifndef SWIG
676  succ(const state* s) const
677  {
678  return {this, succ_iter(s)};
679  }
680  #endif
681 
687  {
688  if (iter_cache_)
689  delete i;
690  else
691  iter_cache_ = i;
692  }
693 
710  bdd_dict_ptr get_dict() const
711  {
712  return dict_;
713  }
714 
728  {
729  int res = dict_->has_registered_proposition(ap, this);
730  if (res < 0)
731  {
732  aps_.emplace_back(ap);
733  res = dict_->register_proposition(ap, this);
734  bddaps_ &= bdd_ithvar(res);
735  }
736  return res;
737  }
738 
739  int register_ap(std::string ap)
740  {
741  return register_ap(formula::ap(ap));
742  }
744 
748  void unregister_ap(int num);
749 
762  {
763  if (!aps_.empty())
764  throw std::runtime_error("register_ap_from_dict() may not be"
765  " called on an automaton that has already"
766  " registered some AP");
767  auto& m = get_dict()->bdd_map;
768  unsigned s = m.size();
769  for (unsigned n = 0; n < s; ++n)
770  if (m[n].refs.find(this) != m[n].refs.end())
771  {
772  aps_.emplace_back(m[n].f);
773  bddaps_ &= bdd_ithvar(n);
774  }
775  }
776 
779  const std::vector<formula>& ap() const
780  {
781  return aps_;
782  }
783 
785  bdd ap_vars() const
786  {
787  return bddaps_;
788  }
789 
796  virtual std::string format_state(const state* s) const = 0;
797 
811  virtual state* project_state(const state* s,
812  const const_twa_ptr& t) const;
813 
816  const acc_cond& acc() const
817  {
818  return acc_;
819  }
820 
822  {
823  return acc_;
824  }
826 
836  virtual bool is_empty() const;
837 
849  virtual twa_run_ptr accepting_run() const;
850 
862  virtual twa_word_ptr accepting_word() const;
863 
870  virtual bool intersects(const_twa_ptr other) const;
871 
882  virtual twa_run_ptr intersecting_run(const_twa_ptr other) const;
883 
884  // (undocumented)
885  //
886  // If \a from_other is true, the returned run will be over the
887  // \a other automaton. Otherwise, the run will be over this
888  // automaton.
889  //
890  // This function was deprecated in Spot 2.8.
891  SPOT_DEPRECATED("replace a->intersecting_run(b, true) "
892  "by b->intersecting_run(a).")
893  twa_run_ptr intersecting_run(const_twa_ptr other,
894  bool from_other) const
895  {
896  if (from_other)
897  return other->intersecting_run(shared_from_this());
898  else
899  return this->intersecting_run(other);
900  }
901 
905  virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
906 
916  virtual twa_run_ptr exclusive_run(const_twa_ptr other) const;
917 
927  virtual twa_word_ptr exclusive_word(const_twa_ptr other) const;
928 
929  private:
930  acc_cond acc_;
931 
932  void set_num_sets_(unsigned num)
933  {
934  if (num < acc_.num_sets())
935  {
936  acc_.~acc_cond();
937  new (&acc_) acc_cond;
938  }
939  acc_.add_sets(num - acc_.num_sets());
940  }
941 
942  public:
944  unsigned num_sets() const
945  {
946  return acc_.num_sets();
947  }
948 
951  {
952  return acc_.get_acceptance();
953  }
954 
959  void set_acceptance(unsigned num, const acc_cond::acc_code& c)
960  {
961  set_num_sets_(num);
962  acc_.set_acceptance(c);
963  }
964 
968  void set_acceptance(const acc_cond& c)
969  {
970  acc_ = c;
971  }
972 
974  void copy_acceptance_of(const const_twa_ptr& a)
975  {
976  acc_ = a->acc();
977  }
978 
980  void copy_ap_of(const const_twa_ptr& a)
981  {
982  for (auto f: a->ap())
983  this->register_ap(f);
984  }
985 
998  void set_generalized_buchi(unsigned num)
999  {
1000  set_num_sets_(num);
1001  acc_.set_generalized_buchi();
1002  }
1003 
1016  void set_generalized_co_buchi(unsigned num)
1017  {
1018  set_num_sets_(num);
1019  acc_.set_generalized_co_buchi();
1020  }
1021 
1038  {
1039  set_generalized_buchi(1);
1040  return acc_.mark(0);
1041  }
1042 
1059  {
1060  set_generalized_co_buchi(1);
1061  return acc_.mark(0);
1062  }
1063 
1064  private:
1065  std::vector<formula> aps_;
1066  bdd bddaps_;
1067 
1069  struct bprop
1070  {
1071  trival::repr_t state_based_acc:2; // State-based acceptance.
1072  trival::repr_t inherently_weak:2; // Inherently Weak automaton.
1073  trival::repr_t weak:2; // Weak automaton.
1074  trival::repr_t terminal:2; // Terminal automaton.
1075  trival::repr_t universal:2; // Universal automaton.
1076  trival::repr_t unambiguous:2; // Unambiguous automaton.
1077  trival::repr_t stutter_invariant:2; // Stutter invariant language.
1078  trival::repr_t very_weak:2; // very-weak, or 1-weak
1079  trival::repr_t semi_deterministic:2; // semi-deterministic automaton.
1080  trival::repr_t complete:2; // Complete automaton.
1081  };
1082  union
1083  {
1084  unsigned props;
1085  bprop is;
1086  };
1087 
1088  protected:
1089 #ifndef SWIG
1090  // Dynamic properties, are given with a name and a destructor function.
1091  std::unordered_map<std::string,
1092  std::pair<void*,
1093  std::function<void(void*)>>> named_prop_;
1094 #endif
1095  void* get_named_prop_(std::string s) const;
1096 
1097  public:
1098 
1099 #ifndef SWIG
1100  void set_named_prop(std::string s,
1116  void* val, std::function<void(void*)> destructor);
1117 
1133  template<typename T>
1134  void set_named_prop(std::string s, T* val)
1135  {
1136  set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
1137  }
1138 
1149  void set_named_prop(std::string s, std::nullptr_t);
1150 
1166  template<typename T>
1167  T* get_named_prop(std::string s) const
1168  {
1169  if (void* p = get_named_prop_(s))
1170  return static_cast<T*>(p);
1171  else
1172  return nullptr;
1173  }
1174 
1187  template<typename T>
1188  T* get_or_set_named_prop(std::string s)
1189  {
1190  if (void* p = get_named_prop_(s))
1191  return static_cast<T*>(p);
1192 
1193  auto tmp = new T;
1194  set_named_prop(s, tmp);
1195  return tmp;
1196  }
1197 
1198 #endif
1199 
1205  {
1206  // Destroy all named properties.
1207  for (auto& np: named_prop_)
1208  np.second.second(np.second.first);
1209  named_prop_.clear();
1210  }
1211 
1219  {
1220  if (num_sets() == 0)
1221  return trival(true);
1222  return trival::from_repr_t(is.state_based_acc);
1223  }
1224 
1230  {
1231  is.state_based_acc = val.val();
1232  }
1233 
1238  trival is_sba() const
1239  {
1240  return prop_state_acc() && acc().is_buchi();
1241  }
1242 
1252  {
1253  return trival::from_repr_t(is.inherently_weak);
1254  }
1255 
1264  {
1265  is.inherently_weak = val.val();
1266  if (!val)
1267  is.very_weak = is.terminal = is.weak = val.val();
1268  }
1269 
1282  {
1283  return trival::from_repr_t(is.terminal);
1284  }
1285 
1294  {
1295  is.terminal = val.val();
1296  if (val)
1297  is.inherently_weak = is.weak = val.val();
1298  }
1299 
1308  {
1309  return trival::from_repr_t(is.weak);
1310  }
1311 
1320  void prop_weak(trival val)
1321  {
1322  is.weak = val.val();
1323  if (val)
1324  is.inherently_weak = val.val();
1325  if (!val)
1326  is.very_weak = is.terminal = val.val();
1327  }
1328 
1338  {
1339  return trival::from_repr_t(is.very_weak);
1340  }
1341 
1350  {
1351  is.very_weak = val.val();
1352  if (val)
1353  is.weak = is.inherently_weak = val.val();
1354  }
1355 
1356 
1369  {
1370  return trival::from_repr_t(is.complete);
1371  }
1372 
1377  {
1378  is.complete = val.val();
1379  }
1380 
1393  {
1394  return trival::from_repr_t(is.universal);
1395  }
1396 
1405  {
1406  is.universal = val.val();
1407  if (val)
1408  // universal implies unambiguous and semi-deterministic
1409  is.unambiguous = is.semi_deterministic = val.val();
1410  }
1411 
1412  // Starting with Spot 2.4, an automaton is deterministic if it is
1413  // both universal and existential, but as we already have
1414  // twa::is_existential(), we only need to additionally record the
1415  // universal property. Before that, the deterministic property
1416  // was just a synonym for universal, hence we keep the deprecated
1417  // function prop_deterministic() with this meaning.
1418  SPOT_DEPRECATED("use prop_universal() instead")
1419  void prop_deterministic(trival val)
1420  {
1421  prop_universal(val);
1422  }
1423 
1424  SPOT_DEPRECATED("use prop_universal() instead")
1425  trival prop_deterministic() const
1426  {
1427  return prop_universal();
1428  }
1429 
1444  {
1445  return trival::from_repr_t(is.unambiguous);
1446  }
1447 
1455  {
1456  is.unambiguous = val.val();
1457  if (!val)
1458  is.universal = val.val();
1459  }
1460 
1474  {
1475  return trival::from_repr_t(is.semi_deterministic);
1476  }
1477 
1485  {
1486  is.semi_deterministic = val.val();
1487  if (!val)
1488  is.universal = val.val();
1489  }
1490 
1504  {
1505  return trival::from_repr_t(is.stutter_invariant);
1506  }
1507 
1510  {
1511  is.stutter_invariant = val.val();
1512  }
1513 
1553  struct prop_set
1554  {
1555  bool state_based;
1556  bool inherently_weak;
1557  bool deterministic;
1558  bool improve_det;
1559  bool complete;
1560  bool stutter_inv;
1561 
1562  prop_set()
1563  : state_based(false),
1564  inherently_weak(false),
1565  deterministic(false),
1566  improve_det(false),
1567  complete(false),
1568  stutter_inv(false)
1569  {
1570  }
1571 
1572  prop_set(bool state_based,
1573  bool inherently_weak,
1574  bool deterministic,
1575  bool improve_det,
1576  bool complete,
1577  bool stutter_inv)
1578  : state_based(state_based),
1579  inherently_weak(inherently_weak),
1580  deterministic(deterministic),
1581  improve_det(improve_det),
1582  complete(complete),
1583  stutter_inv(stutter_inv)
1584  {
1585  }
1586 
1587 #ifndef SWIG
1588  // The "complete" argument was added in Spot 2.4
1589  SPOT_DEPRECATED("prop_set() now takes 6 arguments")
1590  prop_set(bool state_based,
1591  bool inherently_weak,
1592  bool deterministic,
1593  bool improve_det,
1594  bool stutter_inv)
1595  : state_based(state_based),
1596  inherently_weak(inherently_weak),
1597  deterministic(deterministic),
1598  improve_det(improve_det),
1599  complete(false),
1600  stutter_inv(stutter_inv)
1601  {
1602  }
1603 #endif
1604 
1620  static prop_set all()
1621  {
1622  return { true, true, true, true, true, true };
1623  }
1624  };
1625 
1636  void prop_copy(const const_twa_ptr& other, prop_set p)
1637  {
1638  if (p.state_based)
1639  prop_state_acc(other->prop_state_acc());
1640  if (p.inherently_weak)
1641  {
1642  prop_terminal(other->prop_terminal());
1643  prop_weak(other->prop_weak());
1644  prop_very_weak(other->prop_very_weak());
1645  prop_inherently_weak(other->prop_inherently_weak());
1646  }
1647  if (p.deterministic)
1648  {
1649  prop_universal(other->prop_universal());
1650  prop_semi_deterministic(other->prop_semi_deterministic());
1651  prop_unambiguous(other->prop_unambiguous());
1652  }
1653  else if (p.improve_det)
1654  {
1655  if (other->prop_universal().is_true())
1656  {
1657  prop_universal(true);
1658  }
1659  else
1660  {
1661  if (other->prop_semi_deterministic().is_true())
1662  prop_semi_deterministic(true);
1663  if (other->prop_unambiguous().is_true())
1664  prop_unambiguous(true);
1665  }
1666  }
1667  if (p.complete)
1668  prop_complete(other->prop_complete());
1669  if (p.stutter_inv)
1670  prop_stutter_invariant(other->prop_stutter_invariant());
1671  }
1672 
1678  void prop_keep(prop_set p)
1679  {
1680  if (!p.state_based)
1681  prop_state_acc(trival::maybe());
1682  if (!p.inherently_weak)
1683  {
1684  prop_terminal(trival::maybe());
1685  prop_weak(trival::maybe());
1686  prop_very_weak(trival::maybe());
1687  prop_inherently_weak(trival::maybe());
1688  }
1689  if (!p.deterministic)
1690  {
1691  if (!(p.improve_det && prop_universal().is_true()))
1692  prop_universal(trival::maybe());
1693  if (!(p.improve_det && prop_semi_deterministic().is_true()))
1694  prop_semi_deterministic(trival::maybe());
1695  if (!(p.improve_det && prop_unambiguous().is_true()))
1696  prop_unambiguous(trival::maybe());
1697  }
1698  if (!p.complete)
1699  prop_complete(trival::maybe());
1700  if (!p.stutter_inv)
1701  prop_stutter_invariant(trival::maybe());
1702  }
1703 
1704  void prop_reset()
1705  {
1706  prop_keep({});
1707  }
1708  };
1709 
1710 #ifndef SWIG
1711  namespace internal
1712  {
1713  inline twa_succ_iterable::~twa_succ_iterable()
1714  {
1715  if (it_)
1716  aut_->release_iter(it_);
1717  }
1718  }
1719 #endif // SWIG
1720 
1723 
1726 
1729 
1732 
1735 
1738 
1741 
1744 
1747 
1750 }
Helper class to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:525
virtual ~state()
Destructor.
Definition: twa.hh:110
Definition: automata.hh:26
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1281
Helper structure to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:486
An Equivalence Relation for state*.
Definition: twa.hh:150
Render state pointers unique via a hash table.
Definition: twa.hh:201
internal::twa_succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:676
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1320
void prop_complete(trival val)
Set the complete property.
Definition: twa.hh:1376
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:785
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1855
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1307
void prop_inherently_weak(trival val)
Set the "inherently weak" property.
Definition: twa.hh:1263
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1879
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:851
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:627
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:629
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1469
A Transition-based ω-Automaton.
Definition: twa.hh:622
LTL/PSL formula interface.
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1509
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:821
Abstract class for states.
Definition: twa.hh:50
Strict Weak Ordering for shared_state (shared_ptr<const state*>).
Definition: twa.hh:277
T * get_or_set_named_prop(std::string s)
Create or retrieve a named property.
Definition: twa.hh:1188
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:710
Main class for temporal logic formula.
Definition: formula.hh:704
virtual bool next()=0
Jump to the next successor (if any).
void set_generalized_buchi(unsigned num)
Set generalized Büchi acceptance.
Definition: twa.hh:998
void set_generalized_co_buchi(unsigned num)
Set generalized co-Büchi acceptance.
Definition: twa.hh:1016
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:974
void prop_universal(trival val)
Set the universal property.
Definition: twa.hh:1404
virtual bool first()=0
Position the iterator on the first successor (if any).
void set_acceptance(const acc_cond &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:968
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:950
void set_named_prop(std::string s, T *val)
Declare a named property.
Definition: twa.hh:1134
const std::vector< formula > & ap() const
The vector of atomic propositions registered by this automaton.
Definition: twa.hh:779
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:816
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:959
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1229
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1462
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1251
void prop_unambiguous(trival val)
Set the unambiguous property.
Definition: twa.hh:1454
Hash Function for shared_state (shared_ptr<const state*>).
Definition: twa.hh:334
Iterate over the successors of a state.
Definition: twa.hh:397
void prop_semi_deterministic(trival val)
Set the semi-deterministic property.
Definition: twa.hh:1484
acc_cond::mark_t set_co_buchi()
Set co-Büchi acceptance.
Definition: twa.hh:1058
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1204
An acceptance condition.
Definition: acc.hh:60
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1555
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:727
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:214
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1293
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1503
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:226
Hash Function for state*.
Definition: twa.hh:174
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1218
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1443
void register_aps_from_dict()
Register all atomic propositions that have already been registered by the bdd_dict for this automaton...
Definition: twa.hh:761
Definition: twa.hh:1711
trival prop_very_weak() const
Whether the automaton is very-weak.
Definition: twa.hh:1337
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2019
trival prop_complete() const
Whether the automaton is complete.
Definition: twa.hh:1368
void release_iter(twa_succ_iterator *i) const
Release an iterator after usage.
Definition: twa.hh:686
virtual int compare(const state *other) const =0
Compares two states (that come from the same automaton).
int register_ap(std::string ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:739
trival prop_semi_deterministic() const
Whether the automaton is semi-deterministic.
Definition: twa.hh:1473
virtual size_t hash() const =0
Hash a state.
virtual void destroy() const
Release a state.
Definition: twa.hh:98
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1238
static prop_set all()
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1620
An acceptance formula.
Definition: acc.hh:486
Strict Weak Ordering for state*.
Definition: twa.hh:127
Atomic proposition.
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:944
trival prop_universal() const
Whether the automaton is universal.
Definition: twa.hh:1392
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:1037
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1548
An acceptance mark.
Definition: acc.hh:87
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:980
void prop_very_weak(trival val)
Set the very-weak property.
Definition: twa.hh:1349
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:1167
An Equivalence Relation for shared_state (shared_ptr<const state*>).
Definition: twa.hh:305

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