1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et
3 // 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 #include "common_post.hh"
21 #include "common_r.hh"
22 #include "common_aoutput.hh"
23 #include "common_setup.hh"
24 #include "error.h"
25 #include "argmatch.h"
26
27 spot::postprocessor::output_type type = spot::postprocessor::GeneralizedBuchi;
28 spot::postprocessor::output_pref pref = spot::postprocessor::Small;
29 spot::postprocessor::output_pref comp = spot::postprocessor::Any;
30 spot::postprocessor::output_pref sbacc = spot::postprocessor::Any;
31 spot::postprocessor::output_pref colored = spot::postprocessor::Any;
32 spot::postprocessor::optimization_level level = spot::postprocessor::High;
33
34 bool level_set = false;
35 bool pref_set = false;
36
37 enum {
38 OPT_COBUCHI = 256,
39 OPT_HIGH,
40 OPT_LOW,
41 OPT_MEDIUM,
42 OPT_SMALL,
43 OPT_TGBA,
44 };
45
46 static constexpr const argp_option options[] =
47 {
48 /**************************************************/
49 { nullptr, 0, nullptr, 0, "Output automaton type:", 2 },
50 { "generic", 'G', nullptr, 0,
51 "any acceptance condition is allowed", 0 },
52 { "tgba", OPT_TGBA, nullptr, 0,
53 "automaton with Generalized Büchi acceptance (default)", 0 },
54 { "gba", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
55 { "sba", 'B', nullptr, 0,
56 "state-based Büchi Automaton (same as -S -b)", 0 },
57 // Historical name of the --sba option.
58 { "ba", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
59 { "buchi", 'b', nullptr, 0,
60 "automaton with Büchi acceptance", 0 },
61 { "Buchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
62 { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes "
63 "of the given property)", 0 },
64 { "complete", 'C', nullptr, 0, "output a complete automaton", 0 },
65 { "state-based-acceptance", 'S', nullptr, 0,
66 "define the acceptance using states", 0 },
67 { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
68 { "parity", 'P',
69 "any|min|max|odd|even|min odd|min even|max odd|max even",
70 OPTION_ARG_OPTIONAL,
71 "automaton with parity acceptance", 0, },
72 { "colored-parity", 'p',
73 "any|min|max|odd|even|min odd|min even|max odd|max even",
74 OPTION_ARG_OPTIONAL,
75 "colored automaton with parity acceptance", 0, },
76 { "cobuchi", OPT_COBUCHI, nullptr, 0,
77 "automaton with co-Büchi acceptance (will recognize "
78 "a superset of the input language if not co-Büchi "
79 "realizable)", 0 },
80 { "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
81 /**************************************************/
82 { nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
83 { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 },
84 { "deterministic", 'D', nullptr, 0, "prefer deterministic automata "
85 "(combine with --generic to be sure to obtain a deterministic "
86 "automaton)", 0 },
87 { "any", 'a', nullptr, 0, "no preference, do not bother making it small "
88 "or deterministic", 0 },
89 /**************************************************/
90 { nullptr, 0, nullptr, 0, "Simplification level:", 21 },
91 { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 },
92 { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
93 { "high", OPT_HIGH, nullptr, 0,
94 "all available optimizations (slow, default)", 0 },
95 { nullptr, 0, nullptr, 0, nullptr, 0 }
96 };
97
98 static constexpr const argp_option options_nooutput[] =
99 {
100 /**************************************************/
101 { nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
102 { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 },
103 { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 },
104 { "any", 'a', nullptr, 0, "no preference, do not bother making it small "
105 "or deterministic", 0 },
106 /**************************************************/
107 { nullptr, 0, nullptr, 0, "Simplification level:", 21 },
108 { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 },
109 { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
110 { "high", OPT_HIGH, nullptr, 0,
111 "all available optimizations (slow, default)", 0 },
112 { nullptr, 0, nullptr, 0, nullptr, 0 }
113 };
114
115 static const argp_option options_disabled[] =
116 {
117 /**************************************************/
118 { nullptr, 0, nullptr, 0, "Output automaton type:", 2 },
119 { "generic", 'G', nullptr, 0,
120 "any acceptance is allowed (default)", 0 },
121 { "tgba", OPT_TGBA, nullptr, 0,
122 "automaton with Generalized Büchi acceptance", 0 },
123 { "gba", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
124 { "sba", 'B', nullptr, 0,
125 "state-based Büchi Automaton (same as -S -b)", 0 },
126 // Historical name of the --sba option.
127 { "ba", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
128 { "buchi", 'b', nullptr, 0,
129 "automaton with Büchi acceptance", 0 },
130 { "Buchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
131 { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes "
132 "of the given property)", 0 },
133 { "complete", 'C', nullptr, 0, "output a complete automaton", 0 },
134 { "state-based-acceptance", 'S', nullptr, 0,
135 "define the acceptance using states", 0 },
136 { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
137 { "parity", 'P',
138 "any|min|max|odd|even|min odd|min even|max odd|max even",
139 OPTION_ARG_OPTIONAL,
140 "automaton with parity acceptance", 0, },
141 { "colored-parity", 'p',
142 "any|min|max|odd|even|min odd|min even|max odd|max even",
143 OPTION_ARG_OPTIONAL,
144 "colored automaton with parity acceptance", 0, },
145 { "cobuchi", OPT_COBUCHI, nullptr, 0,
146 "automaton with co-Büchi acceptance (will recognize "
147 "a superset of the input language if not co-Büchi "
148 "realizable)", 0 },
149 { "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
150 /**************************************************/
151 { nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
152 { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 },
153 { "deterministic", 'D', nullptr, 0, "prefer deterministic automata "
154 "(combine with --generic to be sure to obtain a deterministic "
155 "automaton)", 0 },
156 { "any", 'a', nullptr, 0, "no preference, do not bother making it small "
157 "or deterministic", 0 },
158 /**************************************************/
159 { nullptr, 0, nullptr, 0, "Simplification level:", 21 },
160 { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 },
161 { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
162 { "high", OPT_HIGH, nullptr, 0,
163 "all available optimizations (slow)", 0 },
164 { nullptr, 0, nullptr, 0, nullptr, 0 }
165 };
166
167 static int
parse_opt_post(int key,char * arg,struct argp_state *)168 parse_opt_post(int key, char* arg, struct argp_state*)
169 {
170 // Called from C code, so should not raise any exception.
171 BEGIN_EXCEPTION_PROTECT;
172 // This switch is alphabetically-ordered.
173 switch (key)
174 {
175 case 'a':
176 pref = spot::postprocessor::Any;
177 pref_set = true;
178 break;
179 case 'b':
180 type = spot::postprocessor::Buchi;
181 colored = spot::postprocessor::Any;
182 break;
183 case 'B':
184 type = spot::postprocessor::Buchi;
185 colored = spot::postprocessor::Any;
186 sbacc = spot::postprocessor::SBAcc;
187 break;
188 case 'C':
189 comp = spot::postprocessor::Complete;
190 break;
191 case 'D':
192 pref = spot::postprocessor::Deterministic;
193 pref_set = true;
194 break;
195 case 'G':
196 type = spot::postprocessor::Generic;
197 colored = spot::postprocessor::Any;
198 break;
199 case 'M':
200 type = spot::postprocessor::Monitor;
201 colored = spot::postprocessor::Any;
202 break;
203 case 'P':
204 case 'p':
205 {
206 static char const *const parity_args[] =
207 {
208 "any", "min", "max", "odd", "even",
209 "min odd", "odd min",
210 "min even", "even min",
211 "max odd", "odd max",
212 "max even", "even max",
213 nullptr
214 };
215 static spot::postprocessor::output_type const parity_types[] =
216 {
217 spot::postprocessor::Parity,
218 spot::postprocessor::ParityMin,
219 spot::postprocessor::ParityMax,
220 spot::postprocessor::ParityOdd,
221 spot::postprocessor::ParityEven,
222 spot::postprocessor::ParityMinOdd,
223 spot::postprocessor::ParityMinOdd,
224 spot::postprocessor::ParityMinEven,
225 spot::postprocessor::ParityMinEven,
226 spot::postprocessor::ParityMaxOdd,
227 spot::postprocessor::ParityMaxOdd,
228 spot::postprocessor::ParityMaxEven,
229 spot::postprocessor::ParityMaxEven,
230 };
231 ARGMATCH_VERIFY(parity_args, parity_types);
232 if (arg)
233 type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity",
234 arg, parity_args, parity_types);
235 else
236 type = spot::postprocessor::Parity;
237 if (key == 'p')
238 colored = spot::postprocessor::Colored;
239 }
240 break;
241 case 'S':
242 sbacc = spot::postprocessor::SBAcc;
243 break;
244 case OPT_COBUCHI:
245 type = spot::postprocessor::CoBuchi;
246 break;
247 case OPT_HIGH:
248 level = spot::postprocessor::High;
249 simplification_level = 3;
250 level_set = true;
251 break;
252 case OPT_LOW:
253 level = spot::postprocessor::Low;
254 simplification_level = 1;
255 level_set = true;
256 break;
257 case OPT_MEDIUM:
258 level = spot::postprocessor::Medium;
259 simplification_level = 2;
260 level_set = true;
261 break;
262 case OPT_SMALL:
263 pref = spot::postprocessor::Small;
264 pref_set = true;
265 break;
266 case OPT_TGBA:
267 if (automaton_format == Spin)
268 error(2, 0, "--spin and --tgba are incompatible");
269 type = spot::postprocessor::GeneralizedBuchi;
270 colored = spot::postprocessor::Any;
271 break;
272 default:
273 return ARGP_ERR_UNKNOWN;
274 }
275 END_EXCEPTION_PROTECT;
276 return 0;
277 }
278
279 const struct argp post_argp = { options, parse_opt_post,
280 nullptr, nullptr, nullptr, nullptr, nullptr };
281 const struct argp post_argp_disabled = { options_disabled, parse_opt_post,
282 nullptr, nullptr, nullptr,
283 nullptr, nullptr };
284 const struct argp post_argp_nooutput = { options_nooutput, parse_opt_post,
285 nullptr, nullptr, nullptr,
286 nullptr, nullptr };
287