spot  2.12
twa.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <cstddef>
22 #include <spot/twa/fwd.hh>
23 #include <spot/twa/acc.hh>
24 #include <spot/twa/bdddict.hh>
25 #include <cassert>
26 #include <memory>
27 #include <unordered_map>
28 #include <functional>
29 #include <array>
30 #include <vector>
31 #include <spot/misc/casts.hh>
32 #include <spot/misc/hash.hh>
33 #include <spot/tl/formula.hh>
34 #include <spot/misc/trival.hh>
35 
36 namespace spot
37 {
38  struct twa_run;
39  typedef std::shared_ptr<twa_run> twa_run_ptr;
40 
41  struct twa_word;
42  typedef std::shared_ptr<twa_word> twa_word_ptr;
43 
46  class SPOT_API state
47  {
48  public:
59  virtual int compare(const state* other) const = 0;
60 
80  virtual size_t hash() const = 0;
81 
83  virtual state* clone() const = 0;
84 
94  virtual void destroy() const
95  {
96  delete this;
97  }
98 
99  protected:
106  virtual ~state()
107  {
108  }
109  };
110 
124  {
125  bool
126  operator()(const state* left, const state* right) const
127  {
128  SPOT_ASSERT(left);
129  return left->compare(right) < 0;
130  }
131  };
132 
147  {
148  bool
149  operator()(const state* left, const state* right) const
150  {
151  SPOT_ASSERT(left);
152  return 0 == left->compare(right);
153  }
154  };
155 
171  {
172  size_t
173  operator()(const state* that) const
174  {
175  SPOT_ASSERT(that);
176  return that->hash();
177  }
178  };
179 
185  typedef std::unordered_set<const state*,
187 
191  template<class val>
192  using state_map = std::unordered_map<const state*, val,
194 
197  class SPOT_API state_unicity_table
198  {
199  state_set m;
200  public:
201 
210  const state* operator()(const state* s)
211  {
212  auto p = m.insert(s);
213  if (!p.second)
214  s->destroy();
215  return *p.first;
216  }
217 
222  const state* is_new(const state* s)
223  {
224  auto p = m.insert(s);
225  if (!p.second)
226  {
227  s->destroy();
228  return nullptr;
229  }
230  return *p.first;
231  }
232 
234  {
235  for (state_set::iterator i = m.begin(); i != m.end();)
236  {
237  // Advance the iterator before destroying its key. This
238  // avoids issues with old g++ implementations.
239  state_set::iterator old = i++;
240  (*old)->destroy();
241  }
242  }
243 
244  size_t
245  size()
246  {
247  return m.size();
248  }
249  };
250 
251 
252 
253  // Functions related to shared_ptr.
255 
256  typedef std::shared_ptr<const state> shared_state;
257 
258  inline void shared_state_deleter(state* s) { s->destroy(); }
259 
274  {
275  bool
276  operator()(shared_state left,
277  shared_state right) const
278  {
279  SPOT_ASSERT(left);
280  return left->compare(right.get()) < 0;
281  }
282  };
283 
302  {
303  bool
304  operator()(shared_state left,
305  shared_state right) const
306  {
307  SPOT_ASSERT(left);
308  return 0 == left->compare(right.get());
309  }
310  };
311 
331  {
332  size_t
333  operator()(shared_state that) const
334  {
335  SPOT_ASSERT(that);
336  return that->hash();
337  }
338  };
339 
341  typedef std::unordered_set<shared_state,
344 
393  class SPOT_API twa_succ_iterator
394  {
395  public:
396  virtual
398  {
399  }
400 
403 
418  virtual bool first() = 0;
419 
430  virtual bool next() = 0;
431 
447  virtual bool done() const = 0;
448 
450 
453 
463  virtual const state* dst() const = 0;
467  virtual bdd cond() const = 0;
470  virtual acc_cond::mark_t acc() const = 0;
471 
473  };
474 
475  namespace internal
476  {
482  struct SPOT_API succ_iterator
483  {
484  protected:
485  twa_succ_iterator* it_;
486  public:
487 
489  it_(it)
490  {
491  }
492 
493  bool operator==(succ_iterator o) const
494  {
495  return it_ == o.it_;
496  }
497 
498  bool operator!=(succ_iterator o) const
499  {
500  return it_ != o.it_;
501  }
502 
503  const twa_succ_iterator* operator*() const
504  {
505  return it_;
506  }
507 
508  void operator++()
509  {
510  if (!it_->next())
511  it_ = nullptr;
512  }
513  };
514 
515 #ifndef SWIG
522  {
523  protected:
524  const twa* aut_;
525  twa_succ_iterator* it_;
526  public:
527  twa_succ_iterable(const twa* aut, twa_succ_iterator* it)
528  : aut_(aut), it_(it)
529  {
530  }
531 
532  twa_succ_iterable(twa_succ_iterable&& other) noexcept
533  : aut_(other.aut_), it_(other.it_)
534  {
535  other.it_ = nullptr;
536  }
537 
538  ~twa_succ_iterable(); // Defined in this file after twa
539 
541  {
542  return it_->first() ? it_ : nullptr;
543  }
544 
546  {
547  return nullptr;
548  }
549  };
550 #endif // SWIG
551  }
552 
562 
565 
618  class SPOT_API twa: public std::enable_shared_from_this<twa>
619  {
620  protected:
621  twa(const bdd_dict_ptr& d);
625  bdd_dict_ptr dict_;
626  public:
627 
628  virtual ~twa();
629 
635  virtual const state* get_init_state() const = 0;
636 
644  virtual twa_succ_iterator*
645  succ_iter(const state* local_state) const = 0;
646 
647 #ifndef SWIG
672  succ(const state* s) const
673  {
674  return {this, succ_iter(s)};
675  }
676  #endif
677 
683  {
684  if (iter_cache_)
685  delete i;
686  else
687  iter_cache_ = i;
688  }
689 
706  bdd_dict_ptr get_dict() const
707  {
708  return dict_;
709  }
710 
724  {
725  int res = dict_->has_registered_proposition(ap, this);
726  if (res < 0)
727  {
728  aps_.emplace_back(ap);
729  res = dict_->register_proposition(ap, this);
730  bddaps_ &= bdd_ithvar(res);
731  }
732  return res;
733  }
734 
735  int register_ap(std::string ap)
736  {
737  return register_ap(formula::ap(ap));
738  }
740 
744  void unregister_ap(int num);
745 
758  {
759  if (!aps_.empty())
760  throw std::runtime_error("register_aps_from_dict() may not be"
761  " called on an automaton that has already"
762  " registered some AP");
763  auto& m = get_dict()->bdd_map;
764  unsigned s = m.size();
765  for (unsigned n = 0; n < s; ++n)
766  if (m[n].refs.find(this) != m[n].refs.end())
767  {
768  aps_.emplace_back(m[n].f);
769  bddaps_ &= bdd_ithvar(n);
770  }
771  }
772 
775  const std::vector<formula>& ap() const
776  {
777  return aps_;
778  }
779 
781  bdd ap_vars() const
782  {
783  return bddaps_;
784  }
785 
792  virtual std::string format_state(const state* s) const = 0;
793 
807  virtual state* project_state(const state* s,
808  const const_twa_ptr& t) const;
809 
812  const acc_cond& acc() const
813  {
814  return acc_;
815  }
816 
818  {
819  return acc_;
820  }
822 
832  virtual bool is_empty() const;
833 
845  virtual twa_run_ptr accepting_run() const;
846 
858  virtual twa_word_ptr accepting_word() const;
859 
866  virtual bool intersects(const_twa_ptr other) const;
867 
873  virtual bool intersects(const_twa_word_ptr w) const;
874 
885  virtual twa_run_ptr intersecting_run(const_twa_ptr other) const;
886 
887  // (undocumented)
888  //
889  // If \a from_other is true, the returned run will be over the
890  // \a other automaton. Otherwise, the run will be over this
891  // automaton.
892  //
893  // This function was deprecated in Spot 2.8.
894  SPOT_DEPRECATED("replace a->intersecting_run(b, true) "
895  "by b->intersecting_run(a).")
896  twa_run_ptr intersecting_run(const_twa_ptr other,
897  bool from_other) const
898  {
899  if (from_other)
900  return other->intersecting_run(shared_from_this());
901  else
902  return this->intersecting_run(other);
903  }
904 
908  virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
909 
919  virtual twa_run_ptr exclusive_run(const_twa_ptr other) const;
920 
930  virtual twa_word_ptr exclusive_word(const_twa_ptr other) const;
931 
932  private:
933  acc_cond acc_;
934 
935  public:
937  unsigned num_sets() const
938  {
939  return acc_.num_sets();
940  }
941 
944  {
945  return acc_.get_acceptance();
946  }
947 
952  void set_acceptance(unsigned num, const acc_cond::acc_code& c)
953  {
954  acc_ = acc_cond(num, c);
955  }
956 
960  void set_acceptance(const acc_cond& c)
961  {
962  acc_ = c;
963  }
964 
966  void copy_acceptance_of(const const_twa_ptr& a)
967  {
968  acc_ = a->acc();
969  }
970 
972  void copy_ap_of(const const_twa_ptr& a)
973  {
974  for (auto f: a->ap())
975  this->register_ap(f);
976  }
977 
979  void copy_named_properties_of(const const_twa_ptr& a);
980 
993  void set_generalized_buchi(unsigned num)
994  {
996  }
997 
1010  void set_generalized_co_buchi(unsigned num)
1011  {
1013  }
1014 
1031  {
1032  acc_ = acc_cond(1, acc_cond::acc_code::buchi());
1033  return {0};
1034  }
1035 
1052  {
1054  return {0};
1055  }
1056 
1057  private:
1058  std::vector<formula> aps_;
1059  bdd bddaps_;
1060 
1062  struct bprop
1063  {
1064  trival::repr_t state_based_acc:2; // State-based acceptance.
1065  trival::repr_t inherently_weak:2; // Inherently Weak automaton.
1066  trival::repr_t weak:2; // Weak automaton.
1067  trival::repr_t terminal:2; // Terminal automaton.
1068  trival::repr_t universal:2; // Universal automaton.
1069  trival::repr_t unambiguous:2; // Unambiguous automaton.
1070  trival::repr_t stutter_invariant:2; // Stutter invariant language.
1071  trival::repr_t very_weak:2; // very-weak, or 1-weak
1072  trival::repr_t semi_deterministic:2; // semi-deterministic automaton.
1073  trival::repr_t complete:2; // Complete automaton.
1074  };
1075  union
1076  {
1077  unsigned props;
1078  bprop is;
1079  };
1080 
1081  protected:
1082 #ifndef SWIG
1083  // Dynamic properties, are given with a name and a destructor function.
1084  std::unordered_map<std::string,
1085  std::pair<void*,
1086  std::function<void(void*)>>> named_prop_;
1087 #endif
1088  void* get_named_prop_(std::string s) const;
1089 
1090  public:
1091 
1092 #ifndef SWIG
1108  void set_named_prop(std::string s,
1109  void* val, std::function<void(void*)> destructor);
1110 
1126  template<typename T>
1127  void set_named_prop(std::string s, T* val)
1128  {
1129  set_named_prop(s, val,
1130  [](void *p) noexcept { delete static_cast<T*>(p); });
1131  }
1132 
1143  void set_named_prop(std::string s, std::nullptr_t);
1144 
1160  template<typename T>
1161  T* get_named_prop(std::string s) const
1162  {
1163  if (void* p = get_named_prop_(s))
1164  return static_cast<T*>(p);
1165  else
1166  return nullptr;
1167  }
1168 
1181  template<typename T>
1182  T* get_or_set_named_prop(std::string s)
1183  {
1184  if (void* p = get_named_prop_(s))
1185  return static_cast<T*>(p);
1186 
1187  auto tmp = new T;
1188  set_named_prop(s, tmp);
1189  return tmp;
1190  }
1191 
1192 #endif
1193 
1199  {
1200  // Destroy all named properties.
1201  for (auto& np: named_prop_)
1202  np.second.second(np.second.first);
1203  named_prop_.clear();
1204  }
1205 
1213  {
1214  if (num_sets() == 0)
1215  return trival(true);
1216  return trival::from_repr_t(is.state_based_acc);
1217  }
1218 
1224  {
1225  is.state_based_acc = val.val();
1226  }
1227 
1232  trival is_sba() const
1233  {
1234  return prop_state_acc() && acc().is_buchi();
1235  }
1236 
1246  {
1247  return trival::from_repr_t(is.inherently_weak);
1248  }
1249 
1258  {
1259  is.inherently_weak = val.val();
1260  if (!val)
1261  is.very_weak = is.terminal = is.weak = val.val();
1262  }
1263 
1276  {
1277  return trival::from_repr_t(is.terminal);
1278  }
1279 
1288  {
1289  is.terminal = val.val();
1290  if (val)
1291  is.inherently_weak = is.weak = val.val();
1292  }
1293 
1302  {
1303  return trival::from_repr_t(is.weak);
1304  }
1305 
1314  void prop_weak(trival val)
1315  {
1316  is.weak = val.val();
1317  if (val)
1318  is.inherently_weak = val.val();
1319  if (!val)
1320  is.very_weak = is.terminal = val.val();
1321  }
1322 
1332  {
1333  return trival::from_repr_t(is.very_weak);
1334  }
1335 
1344  {
1345  is.very_weak = val.val();
1346  if (val)
1347  is.weak = is.inherently_weak = val.val();
1348  }
1349 
1350 
1363  {
1364  return trival::from_repr_t(is.complete);
1365  }
1366 
1371  {
1372  is.complete = val.val();
1373  }
1374 
1387  {
1388  return trival::from_repr_t(is.universal);
1389  }
1390 
1399  {
1400  is.universal = val.val();
1401  if (val)
1402  // universal implies unambiguous and semi-deterministic
1403  is.unambiguous = is.semi_deterministic = val.val();
1404  }
1405 
1406  // Starting with Spot 2.4, an automaton is deterministic if it is
1407  // both universal and existential, but as we already have
1408  // twa::is_existential(), we only need to additionally record the
1409  // universal property. Before that, the deterministic property
1410  // was just a synonym for universal, hence we keep the deprecated
1411  // function prop_deterministic() with this meaning.
1412  SPOT_DEPRECATED("use prop_universal() instead")
1413  void prop_deterministic(trival val)
1414  {
1415  prop_universal(val);
1416  }
1417 
1418  SPOT_DEPRECATED("use prop_universal() instead")
1419  trival prop_deterministic() const
1420  {
1421  return prop_universal();
1422  }
1423 
1438  {
1439  return trival::from_repr_t(is.unambiguous);
1440  }
1441 
1449  {
1450  is.unambiguous = val.val();
1451  if (!val)
1452  is.universal = val.val();
1453  }
1454 
1468  {
1469  return trival::from_repr_t(is.semi_deterministic);
1470  }
1471 
1479  {
1480  is.semi_deterministic = val.val();
1481  if (!val)
1482  is.universal = val.val();
1483  }
1484 
1498  {
1499  return trival::from_repr_t(is.stutter_invariant);
1500  }
1501 
1504  {
1505  is.stutter_invariant = val.val();
1506  }
1507 
1547  struct prop_set
1548  {
1549  bool state_based;
1550  bool inherently_weak;
1551  bool deterministic;
1552  bool improve_det;
1553  bool complete;
1554  bool stutter_inv;
1555 
1556  prop_set()
1557  : state_based(false),
1558  inherently_weak(false),
1559  deterministic(false),
1560  improve_det(false),
1561  complete(false),
1562  stutter_inv(false)
1563  {
1564  }
1565 
1566  prop_set(bool state_based,
1567  bool inherently_weak,
1568  bool deterministic,
1569  bool improve_det,
1570  bool complete,
1571  bool stutter_inv)
1572  : state_based(state_based),
1573  inherently_weak(inherently_weak),
1574  deterministic(deterministic),
1575  improve_det(improve_det),
1576  complete(complete),
1577  stutter_inv(stutter_inv)
1578  {
1579  }
1580 
1581 #ifndef SWIG
1582  // The "complete" argument was added in Spot 2.4
1583  SPOT_DEPRECATED("prop_set() now takes 6 arguments")
1584  prop_set(bool state_based,
1585  bool inherently_weak,
1586  bool deterministic,
1587  bool improve_det,
1588  bool stutter_inv)
1589  : state_based(state_based),
1590  inherently_weak(inherently_weak),
1591  deterministic(deterministic),
1592  improve_det(improve_det),
1593  complete(false),
1594  stutter_inv(stutter_inv)
1595  {
1596  }
1597 #endif
1598 
1614  static prop_set all()
1615  {
1616  return { true, true, true, true, true, true };
1617  }
1618  };
1619 
1630  void prop_copy(const const_twa_ptr& other, prop_set p)
1631  {
1632  if (p.state_based)
1633  prop_state_acc(other->prop_state_acc());
1634  if (p.inherently_weak)
1635  {
1636  prop_terminal(other->prop_terminal());
1637  prop_weak(other->prop_weak());
1638  prop_very_weak(other->prop_very_weak());
1639  prop_inherently_weak(other->prop_inherently_weak());
1640  }
1641  if (p.deterministic)
1642  {
1643  prop_universal(other->prop_universal());
1644  prop_semi_deterministic(other->prop_semi_deterministic());
1645  prop_unambiguous(other->prop_unambiguous());
1646  }
1647  else if (p.improve_det)
1648  {
1649  if (other->prop_universal().is_true())
1650  {
1651  prop_universal(true);
1652  }
1653  else
1654  {
1655  if (other->prop_semi_deterministic().is_true())
1656  prop_semi_deterministic(true);
1657  if (other->prop_unambiguous().is_true())
1658  prop_unambiguous(true);
1659  }
1660  }
1661  if (p.complete)
1662  prop_complete(other->prop_complete());
1663  if (p.stutter_inv)
1664  prop_stutter_invariant(other->prop_stutter_invariant());
1665  }
1666 
1672  void prop_keep(prop_set p)
1673  {
1674  if (!p.state_based)
1675  prop_state_acc(trival::maybe());
1676  if (!p.inherently_weak)
1677  {
1678  prop_terminal(trival::maybe());
1679  prop_weak(trival::maybe());
1680  prop_very_weak(trival::maybe());
1681  prop_inherently_weak(trival::maybe());
1682  }
1683  if (!p.deterministic)
1684  {
1685  if (!(p.improve_det && prop_universal().is_true()))
1686  prop_universal(trival::maybe());
1687  if (!(p.improve_det && prop_semi_deterministic().is_true()))
1688  prop_semi_deterministic(trival::maybe());
1689  if (!(p.improve_det && prop_unambiguous().is_true()))
1690  prop_unambiguous(trival::maybe());
1691  }
1692  if (!p.complete)
1693  prop_complete(trival::maybe());
1694  if (!p.stutter_inv)
1695  prop_stutter_invariant(trival::maybe());
1696  }
1697 
1698  void prop_reset()
1699  {
1700  prop_keep({});
1701  }
1702  };
1703 
1704 #ifndef SWIG
1705  namespace internal
1706  {
1707  inline twa_succ_iterable::~twa_succ_iterable()
1708  {
1709  if (it_)
1710  aut_->release_iter(it_);
1711  }
1712  }
1713 #endif // SWIG
1714 
1717 
1720 
1723 
1726 
1729 
1732 
1735 
1738 
1741 
1744 }
An acceptance condition.
Definition: acc.hh:61
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1544
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2035
Main class for temporal logic formula.
Definition: formula.hh:732
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:879
Helper class to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:522
Render state pointers unique via a hash table.
Definition: twa.hh:198
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:222
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:210
Abstract class for states.
Definition: twa.hh:47
virtual size_t hash() const =0
Hash a state.
virtual state * clone() const =0
Duplicate a state.
virtual void destroy() const
Release a state.
Definition: twa.hh:94
virtual ~state()
Destructor.
Definition: twa.hh:106
virtual int compare(const state *other) const =0
Compares two states (that come from the same automaton).
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
Iterate over the successors of a state.
Definition: twa.hh:394
virtual acc_cond::mark_t acc() const =0
Get the acceptance mark of the edge leading to this successor.
virtual const state * dst() const =0
Get the destination state of the current edge.
virtual bool done() const =0
Check whether the iteration is finished.
virtual bool first()=0
Position the iterator on the first successor (if any).
virtual bool next()=0
Jump to the next successor (if any).
virtual bdd cond() const =0
Get the condition on the edge leading to this successor.
A Transition-based ω-Automaton.
Definition: twa.hh:619
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1287
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:966
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:952
virtual twa_run_ptr intersecting_run(const_twa_ptr other) const
Return an accepting run recognizing a word accepted by two automata.
virtual bool intersects(const_twa_word_ptr w) const
Check if this automaton _word intersects a word.
virtual const state * get_init_state() const =0
Get the initial state of the automaton.
void prop_inherently_weak(trival val)
Set the "inherently weak" property.
Definition: twa.hh:1257
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:817
trival prop_universal() const
Whether the automaton is universal.
Definition: twa.hh:1386
void set_generalized_buchi(unsigned num)
Set generalized Büchi acceptance.
Definition: twa.hh:993
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:1030
void set_generalized_co_buchi(unsigned num)
Set generalized co-Büchi acceptance.
Definition: twa.hh:1010
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1198
void set_named_prop(std::string s, void *val, std::function< void(void *)> destructor)
Declare a named property.
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:625
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1314
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:1161
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1437
T * get_or_set_named_prop(std::string s)
Create or retrieve a named property.
Definition: twa.hh:1182
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1497
void set_named_prop(std::string s, std::nullptr_t)
Erase a named property.
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:781
virtual state * project_state(const state *s, const const_twa_ptr &t) const
Project a state on an automaton.
void set_named_prop(std::string s, T *val)
Declare a named property.
Definition: twa.hh:1127
virtual twa_run_ptr accepting_run() const
Return an accepting run if one exists.
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1503
void copy_named_properties_of(const const_twa_ptr &a)
Copy all the named properties of a into this automaton.
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1275
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1212
void set_acceptance(const acc_cond &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:960
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:972
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1245
void prop_semi_deterministic(trival val)
Set the semi-deterministic property.
Definition: twa.hh:1478
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:937
virtual twa_word_ptr exclusive_word(const_twa_ptr other) const
Return a word accepted by exactly one of the two automata.
void prop_complete(trival val)
Set the complete property.
Definition: twa.hh:1370
void prop_unambiguous(trival val)
Set the unambiguous property.
Definition: twa.hh:1448
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:812
virtual twa_succ_iterator * succ_iter(const state *local_state) const =0
Get an iterator over the successors of local_state.
void unregister_ap(int num)
Unregister an atomic proposition.
trival prop_very_weak() const
Whether the automaton is very-weak.
Definition: twa.hh:1331
virtual std::string format_state(const state *s) const =0
Format the state as a string for printing.
acc_cond::mark_t set_co_buchi()
Set co-Büchi acceptance.
Definition: twa.hh:1051
void prop_very_weak(trival val)
Set the very-weak property.
Definition: twa.hh:1343
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1223
trival prop_complete() const
Whether the automaton is complete.
Definition: twa.hh:1362
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:706
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1301
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1232
void prop_universal(trival val)
Set the universal property.
Definition: twa.hh:1398
virtual bool is_empty() const
Check whether the language of the automaton is empty.
static prop_set all()
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1614
void register_aps_from_dict()
Register all atomic propositions that have already been registered by the bdd_dict for this automaton...
Definition: twa.hh:757
const std::vector< formula > & ap() const
The vector of atomic propositions registered by this automaton.
Definition: twa.hh:775
virtual twa_run_ptr exclusive_run(const_twa_ptr other) const
Return an accepting run recognizing a word accepted by exactly one of the two automata.
virtual twa_word_ptr accepting_word() const
Return an accepting word if one exists.
trival prop_semi_deterministic() const
Whether the automaton is semi-deterministic.
Definition: twa.hh:1467
virtual twa_word_ptr intersecting_word(const_twa_ptr other) const
Return a word accepted by two automata.
void release_iter(twa_succ_iterator *i) const
Release an iterator after usage.
Definition: twa.hh:682
int register_ap(std::string ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:735
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:623
virtual bool intersects(const_twa_ptr other) const
Check whether the language of this automaton intersects that of the other automaton.
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:943
internal::twa_succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:672
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:723
LTL/PSL formula interface.
@ ap
Atomic proposition.
Definition: automata.hh:26
void prop_keep(prop_set p)
Keep only a subset of properties of the current automaton.
Definition: twa.hh:1672
std::unordered_set< shared_state, state_shared_ptr_hash, state_shared_ptr_equal > shared_state_set
Unordered set of shared states.
Definition: twa.hh:343
void prop_copy(const const_twa_ptr &other, prop_set p)
Copy the properties of another automaton.
Definition: twa.hh:1630
std::unordered_map< const state *, val, state_ptr_hash, state_ptr_equal > state_map
Unordered map of abstract states.
Definition: twa.hh:193
std::unordered_set< const state *, state_ptr_hash, state_ptr_equal > state_set
Unordered set of abstract states.
Definition: twa.hh:186
twa_graph_ptr complete(const const_twa_ptr &aut)
Clone a twa and complete it.
An acceptance formula.
Definition: acc.hh:470
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:761
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:751
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:743
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:775
An acceptance mark.
Definition: acc.hh:84
Helper structure to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:483
An Equivalence Relation for state*.
Definition: twa.hh:147
Hash Function for state*.
Definition: twa.hh:171
Strict Weak Ordering for state*.
Definition: twa.hh:124
An Equivalence Relation for shared_state (shared_ptr<const state*>).
Definition: twa.hh:302
Hash Function for shared_state (shared_ptr<const state*>).
Definition: twa.hh:331
Strict Weak Ordering for shared_state (shared_ptr<const state*>).
Definition: twa.hh:274

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