1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015-2020 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 #include "common_sys.hh"
21
22 #include <string>
23 #include <iostream>
24 #include <sstream>
25 #include <fstream>
26 #include <sys/wait.h>
27
28 #include "error.h"
29 #include "argmatch.h"
30
31 #include "common_setup.hh"
32 #include "common_cout.hh"
33 #include "common_conv.hh"
34 #include "common_finput.hh"
35 #include "common_aoutput.hh"
36 #include "common_output.hh"
37 #include "common_post.hh"
38 #include "common_trans.hh"
39 #include "common_hoaread.hh"
40
41 #include <spot/tl/relabel.hh>
42 #include <spot/tl/print.hh>
43 #include <spot/misc/bareword.hh>
44 #include <spot/misc/timer.hh>
45 #include <spot/twaalgos/lbtt.hh>
46 #include <spot/twaalgos/relabel.hh>
47 #include <spot/twaalgos/totgba.hh>
48 #include <spot/parseaut/public.hh>
49
50 const char argp_program_doc[] ="\
51 Run LTL/PSL formulas through another program, performing conversion\n\
52 of input and output as required.";
53
54 enum {
55 OPT_ERRORS = 256,
56 OPT_FAIL_ON_TIMEOUT,
57 OPT_GREATEST,
58 OPT_NEGATE,
59 OPT_SMALLEST,
60 };
61
62 static const argp_option options[] =
63 {
64 { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 1 },
65 /**************************************************/
66 { nullptr, 0, nullptr, 0, "Error handling:", 4 },
67 { "errors", OPT_ERRORS, "abort|warn|ignore", 0,
68 "how to deal with tools returning with non-zero exit codes or "
69 "automata that ltldo cannot parse (default: abort)", 0 },
70 { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0,
71 "consider timeouts as errors", 0 },
72 /**************************************************/
73 { nullptr, 0, nullptr, 0, "Output selection:", 5 },
74 { "smallest", OPT_SMALLEST, "FORMAT", OPTION_ARG_OPTIONAL,
75 "for each formula select the smallest automaton given by all "
76 "translators, using FORMAT for ordering (default is %s,%e)", 0 },
77 { "greatest", OPT_GREATEST, "FORMAT", OPTION_ARG_OPTIONAL,
78 "for each formula select the greatest automaton given by all "
79 "translators, using FORMAT for ordering (default is %s,%e)", 0 },
80 { "max-count", 'n', "NUM", 0, "output at most NUM automata", 0 },
81 /**************************************************/
82 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
83 { nullptr, 0, nullptr, 0, nullptr, 0 }
84 };
85
86
87 static const argp_option more_o_format[] =
88 {
89 { "%#", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
90 "serial number of the formula translated", 0 },
91 { "%T", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
92 "tool used for translation", 0 },
93 { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
94 "formula translated", 0 },
95 { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
96 "the part of the line before the formula if it "
97 "comes from a column extracted from a CSV file", 4 },
98 { "%>", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
99 "the part of the line after the formula if it "
100 "comes from a column extracted from a CSV file", 4 },
101 { nullptr, 0, nullptr, 0, nullptr, 0 }
102 };
103
104 // This is not very elegant, but we need to add the above %-escape
105 // sequences to those of aoutput_o_fromat_argp for the --help output.
106 // So far I've failed to instruct argp to merge those two lists into a
107 // single block.
108 static const struct argp*
build_percent_list()109 build_percent_list()
110 {
111 const argp_option* iter = aoutput_o_format_argp.options;
112 unsigned count = 0;
113 while (iter->name || iter->doc)
114 {
115 ++count;
116 ++iter;
117 }
118
119 unsigned s = count * sizeof(argp_option);
120 argp_option* d =
121 static_cast<argp_option*>(malloc(sizeof(more_o_format) + s));
122 memcpy(d, aoutput_o_format_argp.options, s);
123 memcpy(d + count, more_o_format, sizeof(more_o_format));
124
125 static const struct argp more_o_format_argp =
126 { d, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr };
127 return &more_o_format_argp;
128 }
129
130 enum errors_type { errors_abort, errors_warn, errors_ignore };
131 static errors_type errors_opt;
132 static bool fail_on_timeout = false;
133 static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection
134 static const char* best_format = "%s,%e";
135 static int opt_max_count = -1;
136 static bool negate = false;
137
138 static char const *const errors_args[] =
139 {
140 "stop", "abort",
141 "warn", "print",
142 "ignore", "silent", nullptr
143 };
144
145 static errors_type const errors_types[] =
146 {
147 errors_abort, errors_abort,
148 errors_warn, errors_warn,
149 errors_ignore, errors_ignore
150 };
151
152 ARGMATCH_VERIFY(errors_args, errors_types);
153
154 const struct argp_child children[] =
155 {
156 { &hoaread_argp, 0, "Parsing of automata:", 3 },
157 { &finput_argp, 0, nullptr, 0 },
158 { &trans_argp, 0, nullptr, 3 },
159 { &aoutput_argp, 0, nullptr, 6 },
160 { build_percent_list(), 0, nullptr, 7 },
161 { &misc_argp, 0, nullptr, -1 },
162 { nullptr, 0, nullptr, 0 }
163 };
164
165 static int
parse_opt(int key,char * arg,struct argp_state *)166 parse_opt(int key, char* arg, struct argp_state*)
167 {
168 // Called from C code, so should not raise any exception.
169 BEGIN_EXCEPTION_PROTECT;
170 switch (key)
171 {
172 case OPT_ERRORS:
173 errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types);
174 break;
175 case OPT_FAIL_ON_TIMEOUT:
176 fail_on_timeout = true;
177 break;
178 case OPT_GREATEST:
179 best_type = 1;
180 if (arg)
181 best_format = arg;
182 break;
183 case OPT_NEGATE:
184 negate = true;
185 break;
186 case OPT_SMALLEST:
187 best_type = -1;
188 if (arg)
189 best_format = arg;
190 break;
191 case 'n':
192 opt_max_count = to_pos_int(arg, "-n/--max-count");
193 break;
194 case ARGP_KEY_ARG:
195 if (arg[0] == '-' && !arg[1])
196 jobs.emplace_back(arg, true);
197 else
198 tools_push_trans(arg);
199 break;
200 default:
201 return ARGP_ERR_UNKNOWN;
202 }
203 END_EXCEPTION_PROTECT;
204 return 0;
205 }
206
207 namespace
208 {
209 class xtranslator_runner final: public translator_runner
210 {
211 public:
xtranslator_runner(spot::bdd_dict_ptr dict)212 xtranslator_runner(spot::bdd_dict_ptr dict)
213 : translator_runner(dict, true)
214 {
215 }
216
217 spot::twa_graph_ptr
translate(unsigned int translator_num,bool & problem,spot::process_timer & timer)218 translate(unsigned int translator_num, bool& problem,
219 spot::process_timer& timer)
220 {
221 output.reset(translator_num);
222
223 std::ostringstream command;
224 format(command, tools[translator_num].cmd);
225
226 std::string cmd = command.str();
227 //std::cerr << "Running [" << l << translator_num << "]: "
228 // << cmd << std::endl;
229 timer.start();
230 int es = exec_with_timeout(cmd.c_str());
231 timer.stop();
232
233 spot::twa_graph_ptr res = nullptr;
234 problem = false;
235 if (timed_out)
236 {
237 // A timeout is considered benign, unless --fail-on-timeout.
238 if (fail_on_timeout)
239 problem = true;
240 else
241 ++timeout_count;
242 std::cerr << program_name
243 << ": timeout during execution of command \""
244 << cmd << "\"\n";
245 }
246 else if (WIFSIGNALED(es))
247 {
248 if (errors_opt != errors_ignore)
249 {
250 problem = true;
251 es = WTERMSIG(es);
252 std::cerr << program_name << ": execution of command \"" << cmd
253 << "\" terminated by signal " << es << ".\n";
254 }
255 }
256 else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
257 {
258 if (errors_opt != errors_ignore)
259 {
260 problem = true;
261 es = WEXITSTATUS(es);
262 std::cerr << program_name << ": execution of command \"" << cmd
263 << "\" returned exit code " << es << ".\n";
264 }
265 }
266 else if (output.val())
267 {
268 auto aut = spot::parse_aut(output.val()->name(), dict,
269 spot::default_environment::instance(),
270 opt_parse);
271 if (!aut->errors.empty() && errors_opt != errors_ignore)
272 {
273 problem = true;
274 std::cerr << program_name << ": failed to parse the automaton "
275 "produced by \"" << cmd << "\".\n";
276 aut->format_errors(std::cerr);
277 }
278 else if (aut->aborted && errors_opt != errors_ignore)
279 {
280 problem = true;
281 std::cerr << program_name << ": command \"" << cmd
282 << "\" aborted its output.\n";
283 }
284 else
285 {
286 res = aut->aut;
287 }
288 }
289 // Note that res can stay empty if no automaton was output.
290
291 if (problem && errors_opt == errors_ignore)
292 {
293 problem = false;
294 res = nullptr;
295 }
296 output.cleanup();
297 return res;
298 }
299 };
300
301
302 class processor final: public job_processor
303 {
304 spot::bdd_dict_ptr dict = spot::make_bdd_dict();
305 xtranslator_runner runner;
306 automaton_printer printer;
307 hoa_stat_printer best_printer;
308 std::ostringstream best_stream;
309 spot::postprocessor& post;
310 spot::printable_value<std::string> cmdname;
311 spot::printable_value<unsigned> roundval;
312 spot::printable_value<std::string> inputf;
313
314 public:
processor(spot::postprocessor & post)315 processor(spot::postprocessor& post)
316 : runner(dict), best_printer(best_stream, best_format), post(post)
317 {
318 printer.add_stat('T', &cmdname);
319 printer.add_stat('#', &roundval);
320 printer.add_stat('f', &inputf);
321 best_printer.declare('T', &cmdname);
322 best_printer.declare('#', &roundval);
323 best_printer.declare('f', &inputf);
324 }
325
~processor()326 ~processor()
327 {
328 }
329
330 int
process_string(const std::string & input,const char * filename,int linenum)331 process_string(const std::string& input,
332 const char* filename,
333 int linenum) override
334 {
335 spot::parsed_formula pf = parse_formula(input);
336
337 if (!pf.f || !pf.errors.empty())
338 {
339 if (filename)
340 error_at_line(0, 0, filename, linenum, "parse error:");
341 pf.format_errors(std::cerr);
342 return 1;
343 }
344
345 if (negate)
346 {
347 pf.f = spot::formula::Not(pf.f);
348 std::ostringstream os;
349 stream_formula(os, pf.f, filename, std::to_string(linenum).c_str());
350 inputf = os.str();
351 }
352 else
353 {
354 inputf = input;
355 }
356 process_formula(pf.f, filename, linenum);
357 return 0;
358 }
359
output_aut(const spot::twa_graph_ptr & aut,spot::process_timer & ptimer,spot::formula f,const char * filename,int loc,const char * csv_prefix,const char * csv_suffix)360 void output_aut(const spot::twa_graph_ptr& aut,
361 spot::process_timer& ptimer,
362 spot::formula f,
363 const char* filename, int loc,
364 const char* csv_prefix, const char* csv_suffix)
365 {
366 static long int output_count = 0;
367 ++output_count;
368 printer.print(aut, ptimer, f, filename, loc, nullptr,
369 csv_prefix, csv_suffix);
370 if (opt_max_count >= 0 && output_count >= opt_max_count)
371 abort_run = true;
372 }
373
374 int
process_formula(spot::formula f,const char * filename=nullptr,int linenum=0)375 process_formula(spot::formula f,
376 const char* filename = nullptr, int linenum = 0) override
377 {
378 std::unique_ptr<spot::relabeling_map> relmap;
379
380 // If atomic propositions are incompatible with one of the
381 // output, relabel the formula.
382 if (opt_relabel
383 || (!f.has_lbt_atomic_props() &&
384 (runner.has('l') || runner.has('L') || runner.has('T')))
385 || (!f.has_spin_atomic_props() &&
386 (runner.has('s') || runner.has('S'))))
387 {
388 relmap.reset(new spot::relabeling_map);
389 f = spot::relabel(f, spot::Pnn, relmap.get());
390 }
391
392 static unsigned round = 1;
393 runner.round_formula(f, round);
394
395 unsigned ts = tools.size();
396 spot::twa_graph_ptr best_aut = nullptr;
397 std::string best_stats;
398 std::string best_cmdname;
399 spot::process_timer best_timer;
400
401 roundval = round;
402 for (unsigned t = 0; t < ts; ++t)
403 {
404 bool problem;
405 spot::process_timer timer;
406 auto aut = runner.translate(t, problem, timer);
407 if (problem)
408 {
409 // An error message already occurred about the problem,
410 // but this additional one will print filename &
411 // linenum, and possibly exit.
412 std::string sf = spot::str_psl(f);
413 error_at_line(errors_opt == errors_abort ? 2 : 0, 0,
414 filename, linenum,
415 "failed to run `%s' on `%s'",
416 tools[t].name, sf.c_str());
417 }
418 if (aut)
419 {
420 if (relmap)
421 relabel_here(aut, relmap.get());
422
423 cmdname = tools[t].name;
424 aut = post.run(aut, f);
425 if (best_type)
426 {
427 best_printer.print(nullptr, aut, f, filename, linenum, timer,
428 prefix, suffix);
429 std::string aut_stats = best_stream.str();
430 if (!best_aut ||
431 (strverscmp(best_stats.c_str(), aut_stats.c_str())
432 * best_type) < 0)
433 {
434 best_aut = aut;
435 best_stats = aut_stats;
436 best_cmdname = tools[t].name;
437 best_timer = timer;
438 }
439 best_stream.str("");
440 }
441 else
442 {
443 output_aut(aut, timer, f, filename, linenum,
444 prefix, suffix);
445 if (abort_run)
446 break;
447 }
448 }
449 }
450 if (best_aut)
451 {
452 cmdname = best_cmdname;
453 output_aut(best_aut, best_timer, f, filename, linenum,
454 prefix, suffix);
455 }
456
457 spot::cleanup_tmpfiles();
458 ++round;
459 return 0;
460 }
461 };
462 }
463
464 int
main(int argc,char ** argv)465 main(int argc, char** argv)
466 {
467 return protected_main(argv, [&] {
468 const argp ap = { options, parse_opt, "[COMMANDFMT...]",
469 argp_program_doc, children, nullptr, nullptr };
470
471 // Disable post-processing as much as possible by default.
472 level = spot::postprocessor::Low;
473 pref = spot::postprocessor::Any;
474 type = spot::postprocessor::Generic;
475 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
476 exit(err);
477
478 check_no_formula();
479
480 if (tools.empty())
481 error(2, 0, "No translator to run? Run '%s --help' for usage.",
482 program_name);
483
484 setup_sig_handler();
485
486 // Usually we print the formula as it was given to us, but
487 // if --negate is used we have to reformat it. We don't know
488 // was the input format unless --lbt-input was given, and in
489 // that case we keep it for output.
490 output_format = lbt_input ? lbt_output : spot_output;
491
492 spot::postprocessor post;
493 post.set_pref(pref | comp | sbacc | colored);
494 post.set_type(type);
495 post.set_level(level);
496
497 processor p(post);
498 if (p.run())
499 return 2;
500 return 0;
501 });
502 }
503