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
23namespace 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.4