spot  2.0.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
twa.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de
3 // Recherche et Développement de l'Epita (LRDE).
4 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
5 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
6 // Université 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 <spot/twa/fwd.hh>
26 #include <spot/twa/acc.hh>
27 #include <spot/twa/bdddict.hh>
28 #include <cassert>
29 #include <memory>
30 #include <unordered_map>
31 #include <functional>
32 #include <array>
33 #include <vector>
34 #include <spot/misc/casts.hh>
35 #include <spot/misc/hash.hh>
36 #include <spot/tl/formula.hh>
37 #include <spot/misc/trival.hh>
38 
39 namespace spot
40 {
43  class SPOT_API state
44  {
45  public:
56  virtual int compare(const state* other) const = 0;
57 
77  virtual size_t hash() const = 0;
78 
80  virtual state* clone() const = 0;
81 
91  virtual void destroy() const
92  {
93  delete this;
94  }
95 
96  protected:
103  virtual ~state()
104  {
105  }
106  };
107 
121  {
122  bool
123  operator()(const state* left, const state* right) const
124  {
125  assert(left);
126  return left->compare(right) < 0;
127  }
128  };
129 
144  {
145  bool
146  operator()(const state* left, const state* right) const
147  {
148  assert(left);
149  return 0 == left->compare(right);
150  }
151  };
152 
168  {
169  size_t
170  operator()(const state* that) const
171  {
172  assert(that);
173  return that->hash();
174  }
175  };
176 
182  typedef std::unordered_set<const state*,
183  state_ptr_hash, state_ptr_equal> state_set;
184 
188  template<class val>
189  using state_map = std::unordered_map<const state*, val,
190  state_ptr_hash, state_ptr_equal>;
191 
194  class SPOT_API state_unicity_table
195  {
196  state_set m;
197  public:
198 
207  const state* operator()(const state* s)
208  {
209  auto p = m.insert(s);
210  if (!p.second)
211  s->destroy();
212  return *p.first;
213  }
214 
219  const state* is_new(const state* s)
220  {
221  auto p = m.insert(s);
222  if (!p.second)
223  {
224  s->destroy();
225  return nullptr;
226  }
227  return *p.first;
228  }
229 
231  {
232  for (state_set::iterator i = m.begin(); i != m.end();)
233  {
234  // Advance the iterator before destroying its key. This
235  // avoid issues with old g++ implementations.
236  state_set::iterator old = i++;
237  (*old)->destroy();
238  }
239  }
240 
241  size_t
242  size()
243  {
244  return m.size();
245  }
246  };
247 
248 
249 
250  // Functions related to shared_ptr.
252 
253  typedef std::shared_ptr<const state> shared_state;
254 
255  inline void shared_state_deleter(state* s) { s->destroy(); }
256 
271  {
272  bool
273  operator()(shared_state left,
274  shared_state right) const
275  {
276  assert(left);
277  return left->compare(right.get()) < 0;
278  }
279  };
280 
299  {
300  bool
301  operator()(shared_state left,
302  shared_state right) const
303  {
304  assert(left);
305  return 0 == left->compare(right.get());
306  }
307  };
308 
328  {
329  size_t
330  operator()(shared_state that) const
331  {
332  assert(that);
333  return that->hash();
334  }
335  };
336 
338  typedef std::unordered_set<shared_state,
340  state_shared_ptr_equal> shared_state_set;
341 
390  class SPOT_API twa_succ_iterator
391  {
392  public:
393  virtual
395  {
396  }
397 
400 
415  virtual bool first() = 0;
416 
427  virtual bool next() = 0;
428 
444  virtual bool done() const = 0;
445 
447 
450 
460  virtual const state* dst() const = 0;
464  virtual bdd cond() const = 0;
467  virtual acc_cond::mark_t acc() const = 0;
468 
470  };
471 
472  namespace internal
473  {
479  struct SPOT_API succ_iterator
480  {
481  protected:
482  twa_succ_iterator* it_;
483  public:
484 
486  it_(it)
487  {
488  }
489 
490  bool operator==(succ_iterator o) const
491  {
492  return it_ == o.it_;
493  }
494 
495  bool operator!=(succ_iterator o) const
496  {
497  return it_ != o.it_;
498  }
499 
500  const twa_succ_iterator* operator*() const
501  {
502  return it_;
503  }
504 
505  void operator++()
506  {
507  if (!it_->next())
508  it_ = nullptr;
509  }
510  };
511  }
512 
522 
525 
577  class SPOT_API twa: public std::enable_shared_from_this<twa>
578  {
579  protected:
580  twa(const bdd_dict_ptr& d);
584  bdd_dict_ptr dict_;
585  public:
586 
587 #ifndef SWIG
588  class succ_iterable
594  {
595  protected:
596  const twa* aut_;
597  twa_succ_iterator* it_;
598  public:
599  succ_iterable(const twa* aut, twa_succ_iterator* it)
600  : aut_(aut), it_(it)
601  {
602  }
603 
605  : aut_(other.aut_), it_(other.it_)
606  {
607  other.it_ = nullptr;
608  }
609 
610  ~succ_iterable()
611  {
612  if (it_)
613  aut_->release_iter(it_);
614  }
615 
617  {
618  return it_->first() ? it_ : nullptr;
619  }
620 
622  {
623  return nullptr;
624  }
625  };
626 #endif
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
648  succ_iterable
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_.push_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_ap_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_.push_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 
824  virtual bool is_empty() const;
825 
826  private:
827  acc_cond acc_;
828 
829  void set_num_sets_(unsigned num)
830  {
831  if (num < acc_.num_sets())
832  {
833  acc_.~acc_cond();
834  new (&acc_) acc_cond;
835  }
836  acc_.add_sets(num - acc_.num_sets());
837  }
838 
839  public:
841  unsigned num_sets() const
842  {
843  return acc_.num_sets();
844  }
845 
848  {
849  return acc_.get_acceptance();
850  }
851 
856  void set_acceptance(unsigned num, const acc_cond::acc_code& c)
857  {
858  set_num_sets_(num);
859  acc_.set_acceptance(c);
860  if (num == 0)
861  prop_state_acc(true);
862  }
863 
865  void copy_acceptance_of(const const_twa_ptr& a)
866  {
867  acc_ = a->acc();
868  unsigned num = acc_.num_sets();
869  if (num == 0)
870  prop_state_acc(true);
871  }
872 
874  void copy_ap_of(const const_twa_ptr& a)
875  {
876  for (auto f: a->ap())
877  this->register_ap(f);
878  }
879 
892  void set_generalized_buchi(unsigned num)
893  {
894  set_num_sets_(num);
895  acc_.set_generalized_buchi();
896  if (num == 0)
897  prop_state_acc(true);
898  }
899 
916  {
917  set_generalized_buchi(1);
918  return acc_.mark(0);
919  }
920 
921  private:
922  std::vector<formula> aps_;
923  bdd bddaps_;
924 
926  struct bprop
927  {
928  trival::repr_t state_based_acc:2; // State-based acceptance.
929  trival::repr_t inherently_weak:2; // Inherently Weak automaton.
930  trival::repr_t weak:2; // Weak automaton.
931  trival::repr_t terminal:2; // Terminal automaton.
932  trival::repr_t deterministic:2; // Deterministic automaton.
933  trival::repr_t unambiguous:2; // Unambiguous automaton.
934  trival::repr_t stutter_invariant:2; // Stutter invariant language.
935  };
936  union
937  {
938  unsigned props;
939  bprop is;
940  };
941 
942 #ifndef SWIG
943  // Dynamic properties, are given with a name and a destructor function.
944  std::unordered_map<std::string,
945  std::pair<void*,
946  std::function<void(void*)>>> named_prop_;
947 #endif
948  void* get_named_prop_(std::string s) const;
949 
950  public:
951 
952 #ifndef SWIG
953  void set_named_prop(std::string s,
965  void* val, std::function<void(void*)> destructor);
966 
978  template<typename T>
979  void set_named_prop(std::string s, T* val)
980  {
981  set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
982  }
983 
996  template<typename T>
997  T* get_named_prop(std::string s) const
998  {
999  void* p = get_named_prop_(s);
1000  if (!p)
1001  return nullptr;
1002  return static_cast<T*>(p);
1003  }
1004 #endif
1005 
1011  {
1012  // Destroy all named properties.
1013  for (auto& np: named_prop_)
1014  np.second.second(np.second.first);
1015  named_prop_.clear();
1016  }
1017 
1025  {
1026  return is.state_based_acc;
1027  }
1028 
1034  {
1035  is.state_based_acc = val.val();
1036  }
1037 
1042  trival is_sba() const
1043  {
1044  return prop_state_acc() && acc().is_buchi();
1045  }
1046 
1056  {
1057  return is.inherently_weak;
1058  }
1059 
1068  {
1069  is.inherently_weak = val.val();
1070  if (!val)
1071  is.terminal = is.weak = val.val();
1072  }
1073 
1084  {
1085  return is.terminal;
1086  }
1087 
1096  {
1097  is.terminal = val.val();
1098  if (val)
1099  is.inherently_weak = is.weak = val.val();
1100  }
1101 
1110  {
1111  return is.weak;
1112  }
1113 
1122  void prop_weak(trival val)
1123  {
1124  is.weak = val.val();
1125  if (val)
1126  is.inherently_weak = val.val();
1127  if (!val)
1128  is.terminal = val.val();
1129  }
1130 
1143  {
1144  return is.deterministic;
1145  }
1146 
1154  {
1155  is.deterministic = val.val();
1156  if (val)
1157  // deterministic implies unambiguous
1158  is.unambiguous = val.val();
1159  }
1160 
1175  {
1176  return is.unambiguous;
1177  }
1178 
1186  {
1187  is.unambiguous = val.val();
1188  if (!val)
1189  is.deterministic = val.val();
1190  }
1191 
1205  {
1206  return is.stutter_invariant;
1207  }
1208 
1211  {
1212  is.stutter_invariant = val.val();
1213  }
1214 
1248  struct prop_set
1249  {
1254 
1270  static prop_set all()
1271  {
1272  return { true, true, true, true };
1273  }
1274  };
1275 
1286  void prop_copy(const const_twa_ptr& other, prop_set p)
1287  {
1288  if (p.state_based)
1289  prop_state_acc(other->prop_state_acc());
1290  if (p.inherently_weak)
1291  {
1292  prop_terminal(other->prop_terminal());
1293  prop_weak(other->prop_weak());
1294  prop_inherently_weak(other->prop_inherently_weak());
1295  }
1296  if (p.deterministic)
1297  {
1298  prop_deterministic(other->prop_deterministic());
1299  prop_unambiguous(other->prop_unambiguous());
1300  }
1301  if (p.stutter_inv)
1302  prop_stutter_invariant(other->prop_stutter_invariant());
1303  }
1304 
1311  {
1312  if (!p.state_based)
1313  prop_state_acc(trival::maybe());
1314  if (!p.inherently_weak)
1315  {
1316  prop_terminal(trival::maybe());
1317  prop_weak(trival::maybe());
1318  prop_inherently_weak(trival::maybe());
1319  }
1320  if (!p.deterministic)
1321  {
1322  prop_deterministic(trival::maybe());
1323  prop_unambiguous(trival::maybe());
1324  }
1325  if (!p.stutter_inv)
1326  prop_stutter_invariant(trival::maybe());
1327  }
1328 
1329  };
1330 
1333 
1336 
1339 
1342 
1345 
1348 
1351 
1354 }
virtual ~state()
Destructor.
Definition: twa.hh:103
Definition: graph.hh:32
bool stutter_inv
preserve stutter invariance
Definition: twa.hh:1253
Helper structure to iterate over the successor of a state using the on-the-fly interface.
Definition: twa.hh:479
bool inherently_weak
preserve inherently weak, weak, & terminal
Definition: twa.hh:1251
An Equivalence Relation for state*.
Definition: twa.hh:143
Render state pointers unique via a hash table.
Definition: twa.hh:194
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1122
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:781
void prop_inherently_weak(trival val)
Set the "inherently weak" proeprty.
Definition: twa.hh:1067
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:797
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:582
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:584
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1055
A Transition-based ω-Automaton.
Definition: twa.hh:577
LTL/PSL formula interface.
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1210
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:817
Abstract class for states.
Definition: twa.hh:43
Strict Weak Ordering for shared_state (shared_ptr).
Definition: twa.hh:270
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1174
bool deterministic
preserve deterministic and unambiguous
Definition: twa.hh:1252
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1024
Helper class to iterate over the successor of a state using the on-the-fly interface.
Definition: twa.hh:593
Main class for temporal logic formula.
Definition: formula.hh:650
virtual bool next()=0
Jump to the next successor (if any).
succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:672
void set_generalized_buchi(unsigned num)
Set generalized Büchi acceptance.
Definition: twa.hh:892
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:865
static prop_set all()
An all-true prop_set.
Definition: twa.hh:1270
virtual bool first()=0
Position the iterator on the first successor (if any).
void set_named_prop(std::string s, T *val)
Declare a named property.
Definition: twa.hh:979
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:856
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1033
virtual void destroy() const
Release a state.
Definition: twa.hh:91
void prop_unambiguous(trival val)
Sets the unambiguous property.
Definition: twa.hh:1185
Hash Function for shared_state (shared_ptr).
Definition: twa.hh:327
Iterate over the successors of a state.
Definition: twa.hh:390
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1204
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1010
void prop_deterministic(trival val)
Set the deterministic property.
Definition: twa.hh:1153
Definition: acc.hh:31
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1083
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:847
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1109
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:723
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:207
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1095
bool state_based
preserve state-based acceptnace
Definition: twa.hh:1250
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
void release_iter(twa_succ_iterator *i) const
Release an iterator after usage.
Definition: twa.hh:682
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1248
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:219
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:841
Hash Function for state*.
Definition: twa.hh:167
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:812
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:997
void register_aps_from_dict()
Register all atomic propositions that have already be register 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
void prop_keep(prop_set p)
Keep only a subset of properties of the current automaton.
Definition: twa.hh:1310
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:735
virtual size_t hash() const =0
Hash a state.
trival prop_deterministic() const
Whether the automaton is deterministic.
Definition: twa.hh:1142
void prop_copy(const const_twa_ptr &other, prop_set p)
Copy the properties of another automaton.
Definition: twa.hh:1286
Definition: acc.hh:300
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1042
Strict Weak Ordering for state*.
Definition: twa.hh:120
Atomic proposition.
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:706
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:915
Definition: acc.hh:34
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:874
An Equivalence Relation for shared_state (shared_ptr).
Definition: twa.hh:298

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