spot  2.6.2
formulas.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement de
3 // 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 
24 
25 // Families defined here come from the following papers:
26 //
27 // @InProceedings{cichon.09.depcos,
28 // author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski},
29 // title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} Formulas},
30 // booktitle = {Proceedings of the Fourth International Conference on
31 // Dependability of Computer Systems},
32 // pages = {17--24},
33 // year = 2009,
34 // publisher = {IEEE Computer Society},
35 // }
36 //
37 // @InProceedings{geldenhuys.06.spin,
38 // author = {Jaco Geldenhuys and Henri Hansen},
39 // title = {Larger Automata and Less Work for LTL Model Checking},
40 // booktitle = {Proceedings of the 13th International SPIN Workshop},
41 // year = {2006},
42 // pages = {53--70},
43 // series = {Lecture Notes in Computer Science},
44 // volume = {3925},
45 // publisher = {Springer}
46 // }
47 //
48 // @InProceedings{gastin.01.cav,
49 // author = {Paul Gastin and Denis Oddoux},
50 // title = {Fast {LTL} to {B\"u}chi Automata Translation},
51 // booktitle = {Proceedings of the 13th International Conference on
52 // Computer Aided Verification (CAV'01)},
53 // pages = {53--65},
54 // year = 2001,
55 // editor = {G. Berry and H. Comon and A. Finkel},
56 // volume = {2102},
57 // series = {Lecture Notes in Computer Science},
58 // address = {Paris, France},
59 // publisher = {Springer-Verlag}
60 // }
61 //
62 // @InProceedings{rozier.07.spin,
63 // author = {Kristin Y. Rozier and Moshe Y. Vardi},
64 // title = {LTL Satisfiability Checking},
65 // booktitle = {Proceedings of the 12th International SPIN Workshop on
66 // Model Checking of Software (SPIN'07)},
67 // pages = {149--167},
68 // year = {2007},
69 // volume = {4595},
70 // series = {Lecture Notes in Computer Science},
71 // publisher = {Springer-Verlag}
72 // }
73 //
74 // @InProceedings{dwyer.98.fmsp,
75 // author = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett},
76 // title = {Property Specification Patterns for Finite-state
77 // Verification},
78 // booktitle = {Proceedings of the 2nd Workshop on Formal Methods in
79 // Software Practice (FMSP'98)},
80 // publisher = {ACM Press},
81 // address = {New York},
82 // editor = {Mark Ardis},
83 // month = mar,
84 // year = {1998},
85 // pages = {7--15}
86 // }
87 //
88 // @InProceedings{etessami.00.concur,
89 // author = {Kousha Etessami and Gerard J. Holzmann},
90 // title = {Optimizing {B\"u}chi Automata},
91 // booktitle = {Proceedings of the 11th International Conference on
92 // Concurrency Theory (Concur'00)},
93 // pages = {153--167},
94 // year = {2000},
95 // editor = {C. Palamidessi},
96 // volume = {1877},
97 // series = {Lecture Notes in Computer Science},
98 // address = {Pennsylvania, USA},
99 // publisher = {Springer-Verlag}
100 // }
101 //
102 // @InProceedings{somenzi.00.cav,
103 // author = {Fabio Somenzi and Roderick Bloem},
104 // title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
105 // booktitle = {Proceedings of the 12th International Conference on
106 // Computer Aided Verification (CAV'00)},
107 // pages = {247--263},
108 // year = {2000},
109 // volume = {1855},
110 // series = {Lecture Notes in Computer Science},
111 // address = {Chicago, Illinois, USA},
112 // publisher = {Springer-Verlag}
113 // }
114 //
115 // @InProceedings{tabakov.10.rv,
116 // author = {Deian Tabakov and Moshe Y. Vardi},
117 // title = {Optimized Temporal Monitors for {SystemC}},
118 // booktitle = {Proceedings of the 1st International Conference on Runtime
119 // Verification (RV'10)},
120 // pages = {436--451},
121 // year = 2010,
122 // volume = {6418},
123 // series = {Lecture Notes in Computer Science},
124 // month = nov,
125 // publisher = {Springer}
126 // }
127 //
128 // @InProceedings{kupferman.10.mochart,
129 // author = {Orna Kupferman and And Rosenberg},
130 // title = {The Blow-Up in Translating LTL do Deterministic Automata},
131 // booktitle = {Proceedings of the 6th International Workshop on Model
132 // Checking and Artificial Intelligence (MoChArt 2010)},
133 // pages = {85--94},
134 // year = 2011,
135 // volume = {6572},
136 // series = {Lecture Notes in Artificial Intelligence},
137 // month = nov,
138 // publisher = {Springer}
139 // }
140 //
141 // @techreport{holevek.04.tr,
142 // title = {Verification Results in {Liberouter} Project},
143 // author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak
144 // and D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek},
145 // month = {September},
146 // year = 2004,
147 // number = 03,
148 // institution = {CESNET}
149 // }
150 //
151 // @InProceedings{pelanek.07.spin,
152 // author = {Radek Pel\'{a}nek},
153 // title = {{BEEM}: benchmarks for explicit model checkers},
154 // booktitle = {Proceedings of the 14th international SPIN conference on
155 // Model checking software},
156 // year = 2007,
157 // pages = {263--267},
158 // numpages = {5},
159 // volume = {4595},
160 // series = {Lecture Notes in Computer Science},
161 // publisher = {Springer-Verlag}
162 // }
163 //
164 // @InProceedings{muller.17.gandalf,
165 // author = {David M\"uller and Salomon Sickert},
166 // title = {{LTL} to Deterministic {E}merson-{L}ei Automata},
167 // booktitle = {Proceedings of the 8th International Sumposium on Games,
168 // Automata, Logics and Formal Verification (GandALF'17)},
169 // year = 2017,
170 // publisher = {Springer-Verlag}
171 // series = {Electronic Proceedings in Theoretical Computer Science},
172 // volume = {256},
173 // publisher = {Open Publishing Association},
174 // pages = {180--194},
175 // doi = {10.4204/EPTCS.256.13}
176 // }
177 //
178 // @InProceedings{sickert.16.cav,
179 // author = {Salomon Sickert and Javier Esparza and Stefaan Jaax
180 // and Jan K{\v{r}}et{\'i}nsk{\'y}},
181 // title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal Logic}
182 // booktitle = {Proceedings of the 28th International Conference on
183 // Computer Aided Verification (CAV'16)},
184 // year = 2016,
185 // publisher = {Springer-Verlag}
186 // series = {Lecture Notes in Computer Science},
187 // volume = {9780},
188 // pages = {312--332},
189 // doi = {10.1007/978-3-319-41540-6_17}
190 // }
191 //
192 // @InProceedings{kretisnky.12.cav,
193 // author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
194 // title = {Deterministic Automata for the {(F,G)}-Fragment of
195 // {LTL}},
196 // booktitle = {24th International Conference on Computer Aided
197 // Verification (CAV'12)},
198 // year = 2012,
199 // pages = {7--22},
200 // doi = {10.1007/978-3-642-31424-7_7},
201 // url = {https://doi.org/10.1007/978-3-642-31424-7_7},
202 // isbn = {978-3-642-31424-7},
203 // publisher = {Springer},
204 // }
205 
206 
207 namespace spot
208 {
209  namespace gen
210  {
211  enum ltl_pattern_id {
212  LTL_BEGIN = 256,
213  LTL_AND_F = LTL_BEGIN,
214  LTL_AND_FG,
215  LTL_AND_GF,
216  LTL_CCJ_ALPHA,
217  LTL_CCJ_BETA,
218  LTL_CCJ_BETA_PRIME,
219  LTL_DAC_PATTERNS,
220  LTL_EH_PATTERNS,
221  LTL_FXG_OR,
222  LTL_GF_EQUIV,
223  LTL_GF_EQUIV_XN,
224  LTL_GF_IMPLIES,
225  LTL_GF_IMPLIES_XN,
226  LTL_GH_Q,
227  LTL_GH_R,
228  LTL_GO_THETA,
229  LTL_GXF_AND,
230  LTL_HKRSS_PATTERNS,
231  LTL_KR_N,
232  LTL_KR_NLOGN,
233  LTL_KV_PSI,
234  LTL_MS_EXAMPLE,
235  LTL_MS_PHI_H,
236  LTL_MS_PHI_R,
237  LTL_MS_PHI_S,
238  LTL_OR_FG,
239  LTL_OR_G,
240  LTL_OR_GF,
241  LTL_P_PATTERNS,
242  LTL_R_LEFT,
243  LTL_R_RIGHT,
244  LTL_RV_COUNTER,
245  LTL_RV_COUNTER_CARRY,
246  LTL_RV_COUNTER_CARRY_LINEAR,
247  LTL_RV_COUNTER_LINEAR,
248  LTL_SB_PATTERNS,
249  LTL_SEJK_F,
250  LTL_SEJK_J,
251  LTL_SEJK_K,
252  LTL_SEJK_PATTERNS,
253  LTL_TV_F1,
254  LTL_TV_F2,
255  LTL_TV_G1,
256  LTL_TV_G2,
257  LTL_TV_UU,
258  LTL_U_LEFT,
259  LTL_U_RIGHT,
260  LTL_END
261  };
262 
268  SPOT_API formula ltl_pattern(ltl_pattern_id pattern, int n, int m = -1);
269 
274  SPOT_API const char* ltl_pattern_name(ltl_pattern_id pattern);
275 
280  SPOT_API int ltl_pattern_max(ltl_pattern_id pattern);
281 
285  SPOT_API int ltl_pattern_argc(ltl_pattern_id pattern);
286  }
287 }
Definition: automata.hh:26
LTL/PSL formula interface.

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