spot  2.7
hierarchy.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
3 // 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/tl/formula.hh>
23 #include <spot/twa/fwd.hh>
24 
25 namespace spot
26 {
45  enum class prcheck
46  {
47  Auto,
48  via_CoBuchi,
49  via_Rabin,
50  };
51 
58  SPOT_API bool
60  twa_graph_ptr aut = nullptr,
61  prcheck algo = prcheck::Auto);
62 
71  SPOT_API bool
73  twa_graph_ptr aut = nullptr,
74  prcheck algo = prcheck::Auto);
75 
77  enum class ocheck
78  {
79  Auto,
80  via_CoBuchi,
81  via_Rabin,
82  via_WDBA,
83  };
84 
105  SPOT_API bool
107  twa_graph_ptr aut = nullptr,
108  ocheck algo = ocheck::Auto);
109 
124  SPOT_API char mp_class(formula f);
125 
126 
140  SPOT_API std::string mp_class(formula f, const char* opt);
141 
156  SPOT_API std::string mp_class(char mpc, const char* opt);
157 
158 
163  SPOT_API unsigned nesting_depth(formula f, op oper);
164 
165 #ifndef SWIG
166  SPOT_API unsigned nesting_depth(formula f, const op* begin, const op* end);
171 #endif
172 
186  SPOT_API unsigned nesting_depth(formula f, const char* opers);
187 
188 
196  SPOT_API bool is_liveness(formula f);
197 }
Definition: automata.hh:26
LTL/PSL formula interface.
prcheck
Enum used to change the behavior of is_persistence() or is_recurrence().
Definition: hierarchy.hh:45
Main class for temporal logic formula.
Definition: formula.hh:685
bool is_recurrence(formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
Return true if f represents a recurrence property.
bool is_persistence(formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
Return true if f represents a persistence property.
op
Operator types.
Definition: formula.hh:64
std::string mp_class(char mpc, const char *opt)
Expand a class in the temporal hierarchy of Manna and Pnueli (PODC&#39;90).
bool is_obligation(formula f, twa_graph_ptr aut=nullptr, ocheck algo=ocheck::Auto)
Return true if f has the recurrence property.

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