diff --git a/NEWS b/NEWS index b37d87907..abc0b43f8 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,12 @@ New in spot 2.8.0.dev (not yet released) - genltl learned --pps-arbiter-standard and --pps-arbiter-strict. + - ltlcross and autcross have learned a new option -q (--quiet) to + remain quiet until an error is found. This helps for instance in + scenarios where multiple instances of ltlcross/autcross are run in + parallel (using "xargs -P" or "GNU Parallel", for instance). See + https://spot.lrde.epita.fr/ltlcross.html#parallel for examples. + Bugs fixed: - When complement() was called with an output_aborter, it could diff --git a/bin/autcross.cc b/bin/autcross.cc index 97183db92..8a1394ddb 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -113,10 +113,12 @@ static const argp_option options[] = "all available optimizations (slow, default)", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", -15 }, + { "quiet", 'q', nullptr, 0, + "suppress all normal output in absence of errors", 0 }, { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0, - "save formulas for which problems were detected in FILENAME", -1 }, + "save formulas for which problems were detected in FILENAME", 0 }, { "verbose", OPT_VERBOSE, nullptr, 0, - "print what is being done, for debugging", -1 }, + "print what is being done, for debugging", 0 }, { nullptr, 0, nullptr, 0, "If an output FILENAME is prefixed with '>>', it is open " "in append mode instead of being truncated.", -14 }, @@ -135,6 +137,7 @@ const struct argp_child children[] = }; static bool verbose = false; +static bool quiet = false; static bool ignore_exec_fail = false; static unsigned ignored_exec_fail = 0; static bool fail_on_timeout = false; @@ -155,6 +158,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'F': jobs.emplace_back(arg, true); break; + case 'q': + quiet = true; + verbose = false; + break; case OPT_BOGUS: { bogus_output = new output_file(arg); @@ -196,6 +203,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_VERBOSE: verbose = true; + quiet = false; break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) @@ -385,7 +393,12 @@ namespace format(command, tools[tool_num].cmd); std::string cmd = command.str(); - std::cerr << "Running [" << l << tool_num << "]: " << cmd << '\n'; + auto disp_cmd = [&]() { + std::cerr << "Running [" << l << tool_num + << "]: " << cmd << '\n'; + }; + if (!quiet) + disp_cmd(); spot::process_timer timer; timer.start(); int es = exec_with_timeout(cmd.c_str()); @@ -397,12 +410,15 @@ namespace { if (fail_on_timeout) { + if (quiet) + disp_cmd(); global_error() << "error: timeout during execution of command\n"; end_error(); } else { - std::cerr << "warning: timeout during execution of command\n"; + if (!quiet) + std::cerr << "warning: timeout during execution of command\n"; ++timeout_count; } status_str = "timeout"; @@ -411,6 +427,8 @@ namespace } else if (WIFSIGNALED(es)) { + if (quiet) + disp_cmd(); status_str = "signal"; problem = true; es = WTERMSIG(es); @@ -424,6 +442,8 @@ namespace status_str = "exit code"; if (!ignore_exec_fail) { + if (quiet) + disp_cmd(); problem = true; global_error() << "error: execution returned exit code " << es << ".\n"; @@ -432,8 +452,9 @@ namespace else { problem = false; - std::cerr << "warning: execution returned exit code " - << es << ".\n"; + if (!quiet) + std::cerr << "warning: execution returned exit code " + << es << ".\n"; ++ignored_exec_fail; } } @@ -448,6 +469,8 @@ namespace opt_parse); if (!aut->errors.empty()) { + if (quiet) + disp_cmd(); status_str = "parse error"; problem = true; es = -1; @@ -459,6 +482,8 @@ namespace } else if (aut->aborted) { + if (quiet) + disp_cmd(); status_str = "aborted"; problem = true; es = -1; @@ -508,9 +533,10 @@ namespace if (aut_i->num_sets() + aut_j->num_sets() > spot::acc_cond::mark_t::max_accsets()) { - std::cerr << "info: building " << autname(i) - << '*' << autname(j, true) - << " requires more acceptance sets than supported\n"; + if (!quiet) + std::cerr << "info: building " << autname(i) + << '*' << autname(j, true) + << " requires more acceptance sets than supported\n"; return false; } @@ -573,14 +599,21 @@ namespace input_statistics.push_back(in_statistics()); - std::cerr << bold << source << reset_color; input_statistics[round_num].input_source = std::move(source); if (auto name = input->get_named_prop("automaton-name")) - { - std::cerr << '\t' << *name; - input_statistics[round_num].input_name = *name; - } - std::cerr << '\n'; + input_statistics[round_num].input_name = *name; + + auto disp_src = [&]() { + std::cerr << bold + << input_statistics[round_num].input_source + << reset_color; + if (!input_statistics[round_num].input_name.empty()) + std::cerr << '\t' + << input_statistics[round_num].input_name; + std::cerr << '\n'; + }; + if (!quiet) + disp_src(); input_statistics[round_num].input.set(input); int problems = 0; @@ -606,7 +639,6 @@ namespace problems += prob; } spot::cleanup_tmpfiles(); - ++round_num; output_statistics.push_back(std::move(stats)); if (verbose) @@ -622,7 +654,9 @@ namespace if (!no_checks) { - std::cerr << "Performing sanity checks and gathering statistics...\n"; + if (!quiet) + std::cerr + << "Performing sanity checks and gathering statistics...\n"; { bool print_first = true; for (unsigned i = 0; i < mi; ++i) @@ -709,15 +743,23 @@ namespace } else { - std::cerr << "Gathering statistics...\n"; + if (!quiet) + std::cerr << "Gathering statistics...\n"; } if (problems && bogus_output) print_hoa(bogus_output->ostream(), input) << std::endl; - std::cerr << '\n'; + if (problems && quiet) + { + std::cerr << "input automaton was "; + disp_src(); + } + if (!quiet || problems) + std::cerr << '\n'; + ++round_num; // Shall we stop processing now? abort_run = global_error_flag && stop_on_error; return problems; @@ -794,7 +836,7 @@ main(int argc, char** argv) { error(2, 0, "no automaton to translate"); } - else + else if (!quiet) { if (global_error_flag) { diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index c575011a5..edb5caa41 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -176,6 +176,8 @@ static const argp_option options[] = { "grind", OPT_GRIND, "[>>]FILENAME", 0, "for each formula for which a problem was detected, write a simpler " \ "formula that fails on the same test in FILENAME", 0 }, + { "quiet", 'q', nullptr, 0, + "suppress all normal output in absence of error", 0 }, { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0, "save formulas for which problems were detected in FILENAME", 0 }, { "verbose", OPT_VERBOSE, nullptr, 0, @@ -220,6 +222,7 @@ static const char* bogus_output_filename = nullptr; static output_file* bogus_output = nullptr; static output_file* grind_output = nullptr; static bool verbose = false; +static bool quiet = false; static bool ignore_exec_fail = false; static unsigned ignored_exec_fail = 0; static bool fail_on_timeout = false; @@ -452,6 +455,10 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "Options --determinize-max-edges and " "--determinize are incompatible."); break; + case 'q': + verbose = false; + quiet = true; + break; case OPT_DET_MAX_EDGES: max_det_edges_given = true; max_det_states = to_pos_int(arg, "--determinize-max-edges"); @@ -544,6 +551,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_VERBOSE: verbose = true; + quiet = false; break; default: return ARGP_ERR_UNKNOWN; @@ -571,7 +579,12 @@ namespace format(command, tools[translator_num].cmd); std::string cmd = command.str(); - std::cerr << "Running [" << l << translator_num << "]: " << cmd << '\n'; + auto disp_cmd = [&]() { + std::cerr << "Running [" << l << translator_num + << "]: " << cmd << '\n'; + }; + if (!quiet) + disp_cmd(); spot::process_timer timer; timer.start(); int es = exec_with_timeout(cmd.c_str()); @@ -583,12 +596,15 @@ namespace { if (fail_on_timeout) { + if (quiet) + disp_cmd(); global_error() << "error: timeout during execution of command\n"; end_error(); } else { - std::cerr << "warning: timeout during execution of command\n"; + if (!quiet) + std::cerr << "warning: timeout during execution of command\n"; ++timeout_count; } status_str = "timeout"; @@ -597,6 +613,8 @@ namespace } else if (WIFSIGNALED(es)) { + if (quiet) + disp_cmd(); status_str = "signal"; problem = true; es = WTERMSIG(es); @@ -610,6 +628,8 @@ namespace status_str = "exit code"; if (!ignore_exec_fail) { + if (quiet) + disp_cmd(); problem = true; global_error() << "error: execution returned exit code " << es << ".\n"; @@ -618,8 +638,9 @@ namespace else { problem = false; - std::cerr << "warning: execution returned exit code " - << es << ".\n"; + if (!quiet) + std::cerr << "warning: execution returned exit code " + << es << ".\n"; ++ignored_exec_fail; } } @@ -634,6 +655,8 @@ namespace opt_parse); if (!aut->errors.empty()) { + if (quiet) + disp_cmd(); status_str = "parse error"; problem = true; es = -1; @@ -645,6 +668,8 @@ namespace } else if (aut->aborted) { + if (quiet) + disp_cmd(); status_str = "aborted"; problem = true; es = -1; @@ -735,16 +760,19 @@ namespace // complemented, or the --verbose option is used, if (!verbose && (icomp || jcomp)) return false; - std::cerr << "info: building "; - if (icomp) - std::cerr << "Comp(N" << i << ')'; - else - std::cerr << 'P' << i; - if (jcomp) - std::cerr << "*Comp(P" << j << ')'; - else - std::cerr << "*N" << j; - std::cerr << " requires more acceptance sets than supported\n"; + if (!quiet) + { + std::cerr << "info: building "; + if (icomp) + std::cerr << "Comp(N" << i << ')'; + else + std::cerr << 'P' << i; + if (jcomp) + std::cerr << "*Comp(P" << j << ')'; + else + std::cerr << "*N" << j; + std::cerr << " requires more acceptance sets than supported\n"; + } return false; } @@ -931,16 +959,18 @@ namespace unsigned mutation_max; while (res) { - std::cerr << "Trying to find a bogus mutation of " << bold - << bogus << reset_color << "...\n"; + if (!quiet) + std::cerr << "Trying to find a bogus mutation of " << bold + << bogus << reset_color << "...\n"; mutations = mutate(f); mutation_count = 1; mutation_max = mutations.size(); res = 0; for (auto g: mutations) { - std::cerr << "Mutation " << mutation_count << '/' - << mutation_max << ": "; + if (!quiet) + std::cerr << "Mutation " << mutation_count << '/' + << mutation_max << ": "; f = g; res = process_formula(g); if (res) @@ -957,9 +987,10 @@ namespace bogus_output->ostream() << bogus << std::endl; } } - std::cerr << "Smallest bogus mutation found for " - << bold << input << reset_color << " is " - << bold << bogus << reset_color << ".\n\n"; + if (!quiet) + std::cerr << "Smallest bogus mutation found for " + << bold << input << reset_color << " is " + << bold << bogus << reset_color << ".\n\n"; grind_output->ostream() << bogus << std::endl; } return 0; @@ -1014,23 +1045,27 @@ namespace // Call formula() before printing anything else, in case it // complains. std::string fstr = runner.formula(); - if (filename) - std::cerr << filename << ':'; - if (linenum) - std::cerr << linenum << ':'; - if (filename || linenum) - std::cerr << ' '; - std::cerr << bold << fstr << reset_color << '\n'; + if (!quiet) + { + if (filename) + std::cerr << filename << ':'; + if (linenum) + std::cerr << linenum << ':'; + if (filename || linenum) + std::cerr << ' '; + std::cerr << bold << fstr << reset_color << '\n'; + } // Make sure we do not translate the same formula twice. if (!allow_dups) { if (!unique_set.insert(f).second) { - std::cerr - << ("warning: This formula or its negation has already" - " been checked.\n Use --allow-dups if it " - "should not be ignored.\n\n"); + if (!quiet) + std::cerr + << ("warning: This formula or its negation has already" + " been checked.\n Use --allow-dups if it " + "should not be ignored.\n\n"); return 0; } } @@ -1134,7 +1169,9 @@ namespace if (!no_checks) { - std::cerr << "Performing sanity checks and gathering statistics...\n"; + if (!quiet) + std::cerr + << "Performing sanity checks and gathering statistics...\n"; // If we have reference tools, pick the smallest of their // automata for positive and negative references. @@ -1564,7 +1601,11 @@ namespace delete pos_map[i]; ++seed; } - std::cerr << '\n'; + if (problems && quiet) + std::cerr << "input formula was " + << bold << fstr << reset_color << "\n\n"; + if (!quiet) + std::cerr << '\n'; delete ap; // Shall we stop processing formulas now? @@ -1685,7 +1726,7 @@ main(int argc, char** argv) { error(2, 0, "no formula to translate"); } - else + else if (!quiet) { if (global_error_flag) { diff --git a/doc/org/autcross.org b/doc/org/autcross.org index 201be9abc..eec479e33 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -472,6 +472,18 @@ an alternate filename to load, or some key to look up somewhere. rm -f autcross.csv #+END_SRC +* Running =autcross= in parallel. + :PROPERTIES: + :CUSTOM_ID: parallel + :END: + + While the =autcross= command itself has no built-in support for + parallelization (patches welcome), its interface allows easy + parallelization with third party tools such as: =xargs -P= ([[https://www.gnu.org/software/findutils/][GNU + findutils]]), =parallel= ([[https://www.gnu.org/software/parallel/][GNU parallel]] or [[https://joeyh.name/code/moreutils/][moreutils]]), or even =make=. + See [[file:ltlcross.org::#parallel][running =ltlcross= in parallel]] for inspiration. + + # LocalWords: utf autcross SETUPFILE html HOA neverclaim dstar's Nr # LocalWords: autfilt dstar randaut lcr xZO urHakt mmkgH ABdm kMYrq # LocalWords: kvBP lVlGfJ BexLFn rjvy rKKlxG Musr LyAxtZ shorthands diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 352fb3f7d..e54ab66ce 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -876,7 +876,6 @@ ggplot(dt2, aes(x=states.small, y=states.deter)) + #+RESULTS: [[file:ltlcross-r2.svg]] - * Miscellaneous options ** =--stop-on-error= @@ -1301,8 +1300,92 @@ info: cross_checks and consistency_checks unnecessary No problem detected. #+end_example +* Running =ltlcross= in parallel + :PROPERTIES: + :CUSTOM_ID: parallel + :END: + + The =ltlcross= command itself has no built-in support for + parallelization (patches welcome). However its interface makes it + rather easy to parallelize =ltlcross= runs with third-party tools + such as: + + - =xargs= from [[https://www.gnu.org/software/findutils/][GNU findutils]]. The [[https://www.gnu.org/software/findutils/manual/html_node/find_html/Controlling-Parallelism.html#Controlling-Parallelism][=-P n= option]] is a GNU extension + to specify that n commands should be run in parallel. + + For instance the following command tests =ltl2tgba= and =ltl3ba= + against 1000 formulas, running 8 formulas in parallel. + + #+begin_src sh :exports code + randltl -n-1 3 | ltlfilt --relabel=pnn --unique -n1000 | + xargs -P8 -I'{}' ltlcross -q --save-bogus='>>bugs.ltl' ltl2tgba ltl3ba -f '{}' + #+end_src + + #+RESULTS: + + The above pipeline uses =randltl= to generate an infinite number + of LTL formulas (=-n-1=) over three atomic propositions. Those + formules are then relabeled with =ltlfilt= (so that =a U b= and =b + U a= both get mapped to the same =p0 U p1=) and filtered for + duplicates (=--unique=). This first 1000 formulas (=-n1000=) are + then passed on to =xargs=. The command =xargs -I'{}' ltlcross...= + takes each line of input, and executes the command =ltlcross...= + with ={}= replaced by the input line. The option =-P8= does this + with 8 processes in parallel. Here =ltlcross= is called with + option =-q= to silence most its regular output as the 8 instances + of =ltlcross= would be otherwise writing to the same terminal. + With =-q=, only errors are displayed. Additionally =--save-bogus= + is used to keep track of all formulas causing errors. The =>>bugs.ltl= + syntax means to open =bugs.ltl= in append mode, so that =bugs.ltl= does + not get overwritten each time a new =ltlcross= instance finds a bug. + + - [[https://www.gnu.org/software/parallel/][GNU parallel]] or [[https://joeyh.name/code/moreutils/][moreutils's parallel]] can also be used similarly. + + - =make -j n= is another option: first convert the list of formulas + into a =Makefile= that calls =ltlcross= for each of them. + + For instance here is how to build a makefile called =ltlcross.mk= + testing ltl2tgbaand ltl3ba against all formulas produced by + =genltl --eh=, and gathering statistics from all runs in =all.csv=. + + #+NAME: ltlcross.mk + #+begin_src sh :epilogue "cat ltlcross.mk" :wrap src makefile + echo 'LTLCROSS=ltlcross -q ltl2tgba ltl3ba' > ltlcross.mk + echo "ALL= $(echo $(genltl --eh --format="%F%L.csv"))" >> ltlcross.mk + echo "all.csv: \$(ALL); cat \$(ALL) | sed -e 1n -e '/^\"formula\"/d' > \$@" >>ltlcross.mk + genltl --eh --format="%F%L.csv:; \$(LTLCROSS) --csv=\$@ -f '%f'" >>ltlcross.mk + #+end_src + + This creates =ltlcross.mk=: + #+RESULTS: ltlcross.mk + #+begin_src makefile + LTLCROSS=ltlcross -q ltl2tgba ltl3ba + ALL= eh-patterns1.csv eh-patterns2.csv eh-patterns3.csv eh-patterns4.csv eh-patterns5.csv eh-patterns6.csv eh-patterns7.csv eh-patterns8.csv eh-patterns9.csv eh-patterns10.csv eh-patterns11.csv eh-patterns12.csv + all.csv: $(ALL); cat $(ALL) | sed -e 1n -e '/^"formula"/d' > $@ + eh-patterns1.csv:; $(LTLCROSS) --csv=$@ -f 'p0 U (p1 & Gp2)' + eh-patterns2.csv:; $(LTLCROSS) --csv=$@ -f 'p0 U (p1 & X(p2 U p3))' + eh-patterns3.csv:; $(LTLCROSS) --csv=$@ -f 'p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))' + eh-patterns4.csv:; $(LTLCROSS) --csv=$@ -f 'F(p0 & XGp1)' + eh-patterns5.csv:; $(LTLCROSS) --csv=$@ -f 'F(p0 & X(p1 & XFp2))' + eh-patterns6.csv:; $(LTLCROSS) --csv=$@ -f 'F(p0 & X(p1 U p2))' + eh-patterns7.csv:; $(LTLCROSS) --csv=$@ -f 'FGp0 | GFp1' + eh-patterns8.csv:; $(LTLCROSS) --csv=$@ -f 'G(p0 -> (p1 U p2))' + eh-patterns9.csv:; $(LTLCROSS) --csv=$@ -f 'G(p0 & XF(p1 & XF(p2 & XFp3)))' + eh-patterns10.csv:; $(LTLCROSS) --csv=$@ -f 'GFp0 & GFp1 & GFp2 & GFp3 & GFp4' + eh-patterns11.csv:; $(LTLCROSS) --csv=$@ -f '(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))' + eh-patterns12.csv:; $(LTLCROSS) --csv=$@ -f 'G(p0 -> (p1 U (Gp2 | Gp3)))' + #+end_src + + This makefile could be executed for instance with =make -f + ltlcross.mk -j 4=, where =-j 4= specifies that 4 processes can be + executed in parallel. Using different =csv= files for each + process avoids potential race conditions that could occur if each + instance of =ltlcross= was appending to the same file. The =sed= + command used while merging all =csv= files keeps the first header + line (=1n=) while removing all subsequent ones (=/"formula"/d=). + #+BEGIN_SRC sh :results silent :exports results -rm -f results.csv results.json ltlcross.csv bogus-grind bogus +rm -f results.csv results.json ltlcross.csv bogus-grind bogus ltlcross.mk #+END_SRC # LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed diff --git a/doc/org/spot.css b/doc/org/spot.css index 5602cc6c7..c6c5e813e 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -50,6 +50,8 @@ thead tr{background:#ffe35e} .org-keyword,.org-builtin,.org-preprocessor,.org-py-import-from,.org-py-def-class{font-weight:bold} .org-string{font-weight:bold;color:#00adad} .src-hoa .org-string{font-weight:bold;color:#d70079} +.src-makefile .org-variable-name{font-weight:bold;color:#d70079} +.org-makefile-targets{font-weight:bold;color:#00adad} .org-function-name{font-weight:bold;color:#d70079} .org-type{font-weight:bold;color:#00adad} .org-comment-delimiter{font-weight:bold;color:#a13672} diff --git a/tests/core/autcross4.test b/tests/core/autcross4.test index 6b6b1335f..9e0d68638 100755 --- a/tests/core/autcross4.test +++ b/tests/core/autcross4.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -26,6 +26,10 @@ ltl2tgba -f FGa '"a = b"U!c' | test 2 = `grep -c '"FGa"' out.csv` test 2 = `grep -c '"""a = b"" U !c"' out.csv` +ltl2tgba -f FGa '"a = b"U!c' | + autcross -q 'autfilt' 'ltl2tgba -B %M >%O' 2>out +test 0 -eq `wc -l in <%O' 'false %H %O' 2>err -Fin && exit 1 +cat err +test 4 = `wc -l err && exit 1 cat err grep 'autcross: No tool to run' err diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 3b8019647..275467149 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -281,6 +281,20 @@ run 1 ltlcross 'echo HOA: --ABORT-- %f > %H' \ -f a --csv=out.csv 2>stderr grep '"exit_status"' out.csv grep '"exit_code"' out.csv +test `grep ': echo HOA' stderr | wc -l` -eq 2 +grep -q -i 'performing' stderr +test `grep 'error:.*aborted' stderr | wc -l` -eq 2 +test `grep '"aborted",-1' out.csv | wc -l` -eq 2 +test 3 = `wc -l < out.csv` +check_csv out.csv + +# Support for --ABORT-- in HOA. +run 1 ltlcross -q 'echo HOA: --ABORT-- %f > %H' \ + -f a --csv=out.csv 2>stderr +grep '"exit_status"' out.csv +grep '"exit_code"' out.csv +test `grep ': echo HOA' stderr | wc -l` -eq 2 +grep -q -i 'performing' stderr && exit 1 test `grep 'error:.*aborted' stderr | wc -l` -eq 2 test `grep '"aborted",-1' out.csv | wc -l` -eq 2 test 3 = `wc -l < out.csv` diff --git a/tests/core/ltlcrossce.test b/tests/core/ltlcrossce.test index cfeaef361..5fcbcf47d 100755 --- a/tests/core/ltlcrossce.test +++ b/tests/core/ltlcrossce.test @@ -101,3 +101,7 @@ grep 'error: P1\*N0 is nonempty' errors grep 'error: P1\*N1 is nonempty' errors test `grep cycle errors | wc -l` = 3 test `grep '^error:' errors | wc -l` = 4 + +ltlcross -q -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \ + "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors && exit 1 +test 8 -eq `wc -l