spot  2.12.2
word.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 <spot/twaalgos/emptiness.hh>
22 
23 namespace spot
24 {
33  struct SPOT_API twa_word final
34  {
35  twa_word(const bdd_dict_ptr& dict) noexcept;
36  twa_word(const twa_run_ptr& run) noexcept;
37  ~twa_word()
38  {
39  dict_->unregister_all_my_variables(this);
40  }
41 
62  void simplify();
63 
69  void use_all_aps(bdd aps, bool positive = false);
70 
71  typedef std::list<bdd> seq_t;
72  seq_t prefix;
73  seq_t cycle;
74 
75  bdd_dict_ptr get_dict() const
76  {
77  return dict_;
78  }
79 
86  twa_graph_ptr as_automaton() const;
87 
93  bool intersects(const_twa_ptr aut) const
94  {
95  return as_automaton()->intersects(aut);
96  }
97 
108  SPOT_API
109  friend std::ostream& operator<<(std::ostream& os, const twa_word& w);
110  private:
111  bdd_dict_ptr dict_;
112  };
113 
119  inline twa_word_ptr make_twa_word(const bdd_dict_ptr& dict)
120  {
121  return std::make_shared<twa_word>(dict);
122  }
123 
125  inline twa_word_ptr make_twa_word(const twa_run_ptr& run)
126  {
127  return std::make_shared<twa_word>(run);
128  }
129 
141  SPOT_API
142  twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict);
143 }
Definition: automata.hh:26
twa_word_ptr parse_word(const std::string &word, const bdd_dict_ptr &dict)
Parse a twa_word.
twa_word_ptr make_twa_word(const bdd_dict_ptr &dict)
Create an empty twa_word.
Definition: word.hh:119
An infinite word stored as a lasso.
Definition: word.hh:34
twa_graph_ptr as_automaton() const
Convert the twa_word as an automaton.
friend std::ostream & operator<<(std::ostream &os, const twa_word &w)
Print a twa_word.
bool intersects(const_twa_ptr aut) const
Check if a the twa_word intersect another automaton.
Definition: word.hh:93
void use_all_aps(bdd aps, bool positive=false)
Use all atomic proposition.
void simplify()
Simplify a lasso-shaped word.

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