spot  2.8.6
stutter.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2017, 2019 Laboratoire de Recherche
3 // et Développement de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <spot/twa/twagraph.hh>
23 
25 
26 namespace spot
27 {
34  SPOT_API twa_graph_ptr
35  sl(const_twa_graph_ptr aut);
36 
47  SPOT_API twa_graph_ptr
48  sl2_inplace(twa_graph_ptr aut);
49 
50  SPOT_API twa_graph_ptr
51  sl2(const_twa_graph_ptr aut);
53 
66  SPOT_API twa_graph_ptr
67  closure_inplace(twa_graph_ptr aut);
68 
69  SPOT_API twa_graph_ptr
70  closure(const_twa_graph_ptr aut);
72 
91  SPOT_API bool
92  is_stutter_invariant(formula f, twa_graph_ptr aut_f = nullptr);
93 
107  SPOT_API bool
108  is_stutter_invariant(twa_graph_ptr aut_f,
109  const_twa_graph_ptr aut_nf = nullptr,
110  int algo = 0);
111 
127  SPOT_API trival
128  check_stutter_invariance(twa_graph_ptr aut_f,
129  formula f = nullptr,
130  bool do_not_determinize = false);
131 
132 
144  SPOT_API std::vector<bool>
145  stutter_invariant_states(const_twa_graph_ptr pos,
146  const_twa_graph_ptr neg = nullptr);
147 
148  SPOT_API std::vector<bool>
149  stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos);
151 
169  SPOT_API void
170  highlight_stutter_invariant_states(twa_graph_ptr pos,
171  formula f_pos, unsigned color = 0);
172  SPOT_API void
173  highlight_stutter_invariant_states(twa_graph_ptr pos,
174  const_twa_graph_ptr neg = nullptr,
175  unsigned color = 0);
177 
190  SPOT_API std::vector<bdd>
191  stutter_invariant_letters(const_twa_graph_ptr pos,
192  const_twa_graph_ptr neg = nullptr);
193 
194  SPOT_API std::vector<bdd>
195  stutter_invariant_letters(const_twa_graph_ptr pos, formula f_pos);
197 
198 
213  SPOT_API int
214  is_stutter_invariant_forward_closed(twa_graph_ptr aut,
215  const std::vector<bool>& sistates);
216 
232  SPOT_API std::vector<bool>
234  (twa_graph_ptr aut, const std::vector<bool>& sistates);
235 
236 }
Definition: automata.hh:26
std::vector< bool > stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos)
Determinate the states that are stutter-invariant in pos.
std::vector< bool > make_stutter_invariant_forward_closed_inplace(twa_graph_ptr aut, const std::vector< bool > &sistates)
Change the automaton so its set of stutter-invariant state is forward-closed.
trival check_stutter_invariance(twa_graph_ptr aut_f, formula f=nullptr, bool do_not_determinize=false)
Check whether aut is stutter-invariant.
twa_graph_ptr sl2_inplace(twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
void highlight_stutter_invariant_states(twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr, unsigned color=0)
Highlight the states of pos that are stutter-invariant.
twa_graph_ptr sl(const_twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
int is_stutter_invariant_forward_closed(twa_graph_ptr aut, const std::vector< bool > &sistates)
Test if the set of stutter-invariant states is forward-closed.
twa_graph_ptr closure_inplace(twa_graph_ptr aut)
Close the automaton by allowing duplicate letter removal.
twa_graph_ptr sl2(const_twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
twa_graph_ptr closure(const_twa_graph_ptr aut)
Close the automaton by allowing duplicate letter removal.
bool is_stutter_invariant(twa_graph_ptr aut_f, const_twa_graph_ptr aut_nf=nullptr, int algo=0)
Check if an automaton has the stutter invariance property.
std::vector< bdd > stutter_invariant_letters(const_twa_graph_ptr pos, formula f_pos)
Determinate the letters with which each state is stutter-invariant.

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.8.13