spot  2.1.1
 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 <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  // avoid 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)
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 
544  internal::succ_iterator begin()
545  {
546  return it_->first() ? it_ : nullptr;
547  }
548 
549  internal::succ_iterator end()
550  {
551  return nullptr;
552  }
553  };
554 #endif // SWIG
555  }
556 
566 
569 
621  class SPOT_API twa: public std::enable_shared_from_this<twa>
622  {
623  protected:
624  twa(const bdd_dict_ptr& d);
628  bdd_dict_ptr dict_;
629  public:
630 
631  virtual ~twa();
632 
638  virtual const state* get_init_state() const = 0;
639 
647  virtual twa_succ_iterator*
648  succ_iter(const state* local_state) const = 0;
649 
650 #ifndef SWIG
675  succ(const state* s) const
676  {
677  return {this, succ_iter(s)};
678  }
679  #endif
680 
686  {
687  if (iter_cache_)
688  delete i;
689  else
690  iter_cache_ = i;
691  }
692 
709  bdd_dict_ptr get_dict() const
710  {
711  return dict_;
712  }
713 
727  {
728  int res = dict_->has_registered_proposition(ap, this);
729  if (res < 0)
730  {
731  aps_.push_back(ap);
732  res = dict_->register_proposition(ap, this);
733  bddaps_ &= bdd_ithvar(res);
734  }
735  return res;
736  }
737 
738  int register_ap(std::string ap)
739  {
740  return register_ap(formula::ap(ap));
741  }
743 
747  void unregister_ap(int num);
748 
761  {
762  if (!aps_.empty())
763  throw std::runtime_error("register_ap_from_dict() may not be"
764  " called on an automaton that has already"
765  " registered some AP");
766  auto& m = get_dict()->bdd_map;
767  unsigned s = m.size();
768  for (unsigned n = 0; n < s; ++n)
769  if (m[n].refs.find(this) != m[n].refs.end())
770  {
771  aps_.push_back(m[n].f);
772  bddaps_ &= bdd_ithvar(n);
773  }
774  }
775 
778  const std::vector<formula>& ap() const
779  {
780  return aps_;
781  }
782 
784  bdd ap_vars() const
785  {
786  return bddaps_;
787  }
788 
795  virtual std::string format_state(const state* s) const = 0;
796 
810  virtual state* project_state(const state* s,
811  const const_twa_ptr& t) const;
812 
815  const acc_cond& acc() const
816  {
817  return acc_;
818  }
819 
821  {
822  return acc_;
823  }
825 
827  virtual bool is_empty() const;
828 
838  virtual twa_run_ptr accepting_run() const;
839 
846  virtual twa_word_ptr accepting_word() const;
847 
848  private:
849  acc_cond acc_;
850 
851  void set_num_sets_(unsigned num)
852  {
853  if (num < acc_.num_sets())
854  {
855  acc_.~acc_cond();
856  new (&acc_) acc_cond;
857  }
858  acc_.add_sets(num - acc_.num_sets());
859  }
860 
861  public:
863  unsigned num_sets() const
864  {
865  return acc_.num_sets();
866  }
867 
870  {
871  return acc_.get_acceptance();
872  }
873 
878  void set_acceptance(unsigned num, const acc_cond::acc_code& c)
879  {
880  set_num_sets_(num);
881  acc_.set_acceptance(c);
882  if (num == 0)
883  prop_state_acc(true);
884  }
885 
887  void copy_acceptance_of(const const_twa_ptr& a)
888  {
889  acc_ = a->acc();
890  unsigned num = acc_.num_sets();
891  if (num == 0)
892  prop_state_acc(true);
893  }
894 
896  void copy_ap_of(const const_twa_ptr& a)
897  {
898  for (auto f: a->ap())
899  this->register_ap(f);
900  }
901 
914  void set_generalized_buchi(unsigned num)
915  {
916  set_num_sets_(num);
917  acc_.set_generalized_buchi();
918  if (num == 0)
919  prop_state_acc(true);
920  }
921 
938  {
939  set_generalized_buchi(1);
940  return acc_.mark(0);
941  }
942 
943  private:
944  std::vector<formula> aps_;
945  bdd bddaps_;
946 
948  struct bprop
949  {
950  trival::repr_t state_based_acc:2; // State-based acceptance.
951  trival::repr_t inherently_weak:2; // Inherently Weak automaton.
952  trival::repr_t weak:2; // Weak automaton.
953  trival::repr_t terminal:2; // Terminal automaton.
954  trival::repr_t deterministic:2; // Deterministic automaton.
955  trival::repr_t unambiguous:2; // Unambiguous automaton.
956  trival::repr_t stutter_invariant:2; // Stutter invariant language.
957  };
958  union
959  {
960  unsigned props;
961  bprop is;
962  };
963 
964 #ifndef SWIG
965  // Dynamic properties, are given with a name and a destructor function.
966  std::unordered_map<std::string,
967  std::pair<void*,
968  std::function<void(void*)>>> named_prop_;
969 #endif
970  void* get_named_prop_(std::string s) const;
971 
972  public:
973 
974 #ifndef SWIG
975  void set_named_prop(std::string s,
991  void* val, std::function<void(void*)> destructor);
992 
1008  template<typename T>
1009  void set_named_prop(std::string s, T* val)
1010  {
1011  set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
1012  }
1013 
1024  void set_named_prop(std::string s, std::nullptr_t);
1025 
1041  template<typename T>
1042  T* get_named_prop(std::string s) const
1043  {
1044  if (void* p = get_named_prop_(s))
1045  return static_cast<T*>(p);
1046  else
1047  return nullptr;
1048  }
1049 
1062  template<typename T>
1063  T* get_or_set_named_prop(std::string s)
1064  {
1065  if (void* p = get_named_prop_(s))
1066  return static_cast<T*>(p);
1067 
1068  auto tmp = new T;
1069  set_named_prop(s, tmp);
1070  return tmp;
1071  }
1072 
1073 #endif
1074 
1080  {
1081  // Destroy all named properties.
1082  for (auto& np: named_prop_)
1083  np.second.second(np.second.first);
1084  named_prop_.clear();
1085  }
1086 
1094  {
1095  return is.state_based_acc;
1096  }
1097 
1103  {
1104  is.state_based_acc = val.val();
1105  }
1106 
1111  trival is_sba() const
1112  {
1113  return prop_state_acc() && acc().is_buchi();
1114  }
1115 
1125  {
1126  return is.inherently_weak;
1127  }
1128 
1137  {
1138  is.inherently_weak = val.val();
1139  if (!val)
1140  is.terminal = is.weak = val.val();
1141  }
1142 
1153  {
1154  return is.terminal;
1155  }
1156 
1165  {
1166  is.terminal = val.val();
1167  if (val)
1168  is.inherently_weak = is.weak = val.val();
1169  }
1170 
1179  {
1180  return is.weak;
1181  }
1182 
1191  void prop_weak(trival val)
1192  {
1193  is.weak = val.val();
1194  if (val)
1195  is.inherently_weak = val.val();
1196  if (!val)
1197  is.terminal = val.val();
1198  }
1199 
1212  {
1213  return is.deterministic;
1214  }
1215 
1223  {
1224  is.deterministic = val.val();
1225  if (val)
1226  // deterministic implies unambiguous
1227  is.unambiguous = val.val();
1228  }
1229 
1244  {
1245  return is.unambiguous;
1246  }
1247 
1255  {
1256  is.unambiguous = val.val();
1257  if (!val)
1258  is.deterministic = val.val();
1259  }
1260 
1274  {
1275  return is.stutter_invariant;
1276  }
1277 
1280  {
1281  is.stutter_invariant = val.val();
1282  }
1283 
1317  struct prop_set
1318  {
1323 
1339  static prop_set all()
1340  {
1341  return { true, true, true, true };
1342  }
1343  };
1344 
1355  void prop_copy(const const_twa_ptr& other, prop_set p)
1356  {
1357  if (p.state_based)
1358  prop_state_acc(other->prop_state_acc());
1359  if (p.inherently_weak)
1360  {
1361  prop_terminal(other->prop_terminal());
1362  prop_weak(other->prop_weak());
1363  prop_inherently_weak(other->prop_inherently_weak());
1364  }
1365  if (p.deterministic)
1366  {
1367  prop_deterministic(other->prop_deterministic());
1368  prop_unambiguous(other->prop_unambiguous());
1369  }
1370  if (p.stutter_inv)
1371  prop_stutter_invariant(other->prop_stutter_invariant());
1372  }
1373 
1380  {
1381  if (!p.state_based)
1382  prop_state_acc(trival::maybe());
1383  if (!p.inherently_weak)
1384  {
1385  prop_terminal(trival::maybe());
1386  prop_weak(trival::maybe());
1387  prop_inherently_weak(trival::maybe());
1388  }
1389  if (!p.deterministic)
1390  {
1391  prop_deterministic(trival::maybe());
1392  prop_unambiguous(trival::maybe());
1393  }
1394  if (!p.stutter_inv)
1395  prop_stutter_invariant(trival::maybe());
1396  }
1397 
1398  };
1399 
1400 #ifndef SWIG
1401  namespace internal
1402  {
1403  inline twa_succ_iterable::~twa_succ_iterable()
1404  {
1405  if (it_)
1406  aut_->release_iter(it_);
1407  }
1408  }
1409 #endif // SWIG
1410 
1413 
1416 
1419 
1422 
1425 
1428 
1431 
1434 }
Helper class to iterate over the successor of a state using the on-the-fly interface.
Definition: twa.hh:525
virtual ~state()
Destructor.
Definition: twa.hh:110
Definition: graph.hh:32
bool stutter_inv
preserve stutter invariance
Definition: twa.hh:1322
Helper structure to iterate over the successor of a state using the on-the-fly interface.
Definition: twa.hh:486
bool inherently_weak
preserve inherently weak, weak, & terminal
Definition: twa.hh:1320
An Equivalence Relation for state*.
Definition: twa.hh:150
Render state pointers unique via a hash table.
Definition: twa.hh:201
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1191
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:784
void prop_inherently_weak(trival val)
Set the "inherently weak" proeprty.
Definition: twa.hh:1136
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:803
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:626
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:628
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1124
A Transition-based ω-Automaton.
Definition: twa.hh:621
LTL/PSL formula interface.
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1279
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:820
Abstract class for states.
Definition: twa.hh:50
Strict Weak Ordering for shared_state (shared_ptr).
Definition: twa.hh:277
T * get_or_set_named_prop(std::string s)
Create or retrieve a named property.
Definition: twa.hh:1063
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1243
bool deterministic
preserve deterministic and unambiguous
Definition: twa.hh:1321
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1093
Main class for temporal logic formula.
Definition: formula.hh:656
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:914
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:887
static prop_set all()
An all-true prop_set.
Definition: twa.hh:1339
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:1009
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:878
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1102
virtual void destroy() const
Release a state.
Definition: twa.hh:98
void prop_unambiguous(trival val)
Sets the unambiguous property.
Definition: twa.hh:1254
Hash Function for shared_state (shared_ptr).
Definition: twa.hh:334
Iterate over the successors of a state.
Definition: twa.hh:397
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1273
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1079
void prop_deterministic(trival val)
Set the deterministic property.
Definition: twa.hh:1222
Definition: acc.hh:31
internal::twa_succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:675
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1152
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:869
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1178
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:726
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:214
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1164
bool state_based
preserve state-based acceptnace
Definition: twa.hh:1319
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:685
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1317
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:226
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:863
Hash Function for state*.
Definition: twa.hh:174
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:815
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:1042
void register_aps_from_dict()
Register all atomic propositions that have already be register by the bdd_dict for this automaton...
Definition: twa.hh:760
const std::vector< formula > & ap() const
The vector of atomic propositions registered by this automaton.
Definition: twa.hh:778
void prop_keep(prop_set p)
Keep only a subset of properties of the current automaton.
Definition: twa.hh:1379
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:738
virtual size_t hash() const =0
Hash a state.
trival prop_deterministic() const
Whether the automaton is deterministic.
Definition: twa.hh:1211
void prop_copy(const const_twa_ptr &other, prop_set p)
Copy the properties of another automaton.
Definition: twa.hh:1355
Definition: acc.hh:300
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1111
Strict Weak Ordering for state*.
Definition: twa.hh:127
Atomic proposition.
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:709
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:937
Definition: acc.hh:34
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:896
An Equivalence Relation for shared_state (shared_ptr).
Definition: twa.hh:305

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Sep 20 2016 07:13:02 for spot by doxygen 1.8.8