From 61b457a37ed8c991bfc75b9231475fe4f1f70d40 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 21 Jul 2023 17:06:01 +0200 Subject: [PATCH] bin: allow %l to be used to print serial numbers * NEWS: Mention it. * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc, bin/common_output.hh, bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc, bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Implement it. * doc/org/oaut.org: Add a short example. * tests/core/serial.test: New file. * tests/Makefile.am: Add it. --- NEWS | 12 +++++++ bin/autfilt.cc | 6 ++-- bin/common_aoutput.cc | 20 ++++++++---- bin/common_aoutput.hh | 17 ++++++---- bin/common_output.cc | 19 ++++++++--- bin/common_output.hh | 4 ++- bin/dstar2tgba.cc | 4 ++- bin/genaut.cc | 3 +- bin/genltl.cc | 8 +++-- bin/ltl2tgba.cc | 5 +-- bin/ltldo.cc | 7 ++--- bin/ltlfilt.cc | 5 ++- bin/ltlgrind.cc | 9 ++++-- bin/randaut.cc | 5 +-- bin/randltl.cc | 9 ++++-- doc/org/oaut.org | 19 +++++++++-- tests/Makefile.am | 1 + tests/core/serial.test | 71 ++++++++++++++++++++++++++++++++++++++++++ 18 files changed, 183 insertions(+), 41 deletions(-) create mode 100755 tests/core/serial.test diff --git a/NEWS b/NEWS index 9a2b7ccbd..c840cea18 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,17 @@ New in spot 2.11.5.dev (not yet released) + Command-line tools: + + - In places that accept format strings with '%' sequences, like + options --stats, --name, or --output, the new '%l' can now be used + to produce the 0-based serial number of the produced object. This + differs from the existing '%L' that is usually related to the line + number of the input (when that makes sense). For instance to + split a file that contains many automaton into several files, one + per automata, do + + autfilt input.hoa -o output-%l.hoa + Library: - The following new trivial simplifications have been implemented for SEREs: diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 4487fad8b..eec2246b3 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1680,8 +1680,6 @@ namespace return 0; } - ++match_count; - if (aliases) { if (opt_aliases) @@ -1690,7 +1688,9 @@ namespace set_aliases(aut, {}); } printer.print(aut, timer, nullptr, haut->filename.c_str(), -1, - haut, prefix, suffix); + match_count, haut, prefix, suffix); + + ++match_count; if (opt_max_count >= 0 && match_count >= opt_max_count) abort_run = true; diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 60f83289e..b3a26c410 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -198,6 +198,8 @@ static const argp_option io_options[] = " minuscules for output):", 4 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "serial number of the output automaton (0-based)", 0 }, { "%H, %h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the automaton in HOA format on a single line (use %[opt]H or %[opt]h " "to specify additional options as in --hoa=opt)", 0 }, @@ -269,6 +271,8 @@ static const argp_option o_options[] = "the following interpreted sequences:", 4 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "serial number of the output automaton (0-based)", 0 }, { "%h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the automaton in HOA format on a single line (use %[opt]h " "to specify additional options as in --hoa=opt)", 0 }, @@ -442,6 +446,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, if (input != ltl_input) declare('f', &filename_); // Override the formula printer. declare('h', &output_aut_); + declare('l', &index_); declare('m', &aut_name_); declare('u', &aut_univbranch_); declare('w', &aut_word_); @@ -453,11 +458,12 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, const char* filename, int loc, + unsigned index, const spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix) { timer_ = ptimer; - + index_ = index; filename_ = filename ? filename : ""; csv_prefix_ = csv_prefix ? csv_prefix : ""; csv_suffix_ = csv_suffix ? csv_suffix : ""; @@ -599,6 +605,7 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, // Input location for errors and statistics. const char* filename, int loc, + unsigned index, // input automaton for statistics const spot::const_parsed_aut_ptr& haut, const char* csv_prefix, @@ -622,7 +629,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, if (opt_name) { name.str(""); - namer.print(haut, aut, f, filename, loc, ptimer, csv_prefix, csv_suffix); + namer.print(haut, aut, f, filename, loc, index, + ptimer, csv_prefix, csv_suffix); aut->set_named_prop("automaton-name", new std::string(name.str())); } @@ -630,8 +638,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, if (opt_output) { outputname.str(""); - outputnamer.print(haut, aut, f, filename, loc, ptimer, - csv_prefix, csv_suffix); + outputnamer.print(haut, aut, f, filename, loc, index, + ptimer, csv_prefix, csv_suffix); std::string fname = outputname.str(); auto [it, b] = outputfiles.try_emplace(fname, nullptr); if (b) @@ -660,8 +668,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, break; case Stats: statistics.set_output(*out); - statistics.print(haut, aut, f, filename, loc, ptimer, - csv_prefix, csv_suffix) << '\n'; + statistics.print(haut, aut, f, filename, loc, index, + ptimer, csv_prefix, csv_suffix) << '\n'; break; } flush_cout(); diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index f57beae84..051212b3d 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -133,10 +133,10 @@ public: void print(std::ostream& os, const char* pos) const override; }; -/// \brief prints various statistics about a TGBA +/// \brief prints various statistics about a TwA /// /// This object can be configured to display various statistics -/// about a TGBA. Some %-sequence of characters are interpreted in +/// about a TwA. Some %-sequence of characters are interpreted in /// the format string, and replaced by the corresponding statistics. class hoa_stat_printer: protected spot::stat_printer { @@ -153,10 +153,12 @@ public: /// to be output. std::ostream& print(const spot::const_parsed_aut_ptr& haut, - const spot::const_twa_graph_ptr& aut, - spot::formula f, - const char* filename, int loc, const spot::process_timer& ptimer, - const char* csv_prefix, const char* csv_suffix); + const spot::const_twa_graph_ptr& aut, + spot::formula f, + const char* filename, int loc, + unsigned index, + const spot::process_timer& ptimer, + const char* csv_prefix, const char* csv_suffix); private: spot::printable_value filename_; @@ -165,6 +167,7 @@ private: spot::printable_value aut_name_; spot::printable_value aut_word_; spot::printable_value haut_word_; + spot::printable_value index_; spot::printable_acc_cond haut_gen_acc_; spot::printable_size haut_states_; spot::printable_size haut_edges_; @@ -206,6 +209,8 @@ public: // Input location for errors and statistics. const char* filename = nullptr, int loc = -1, + // serial numbner + unsigned index = 0, // Time and input automaton for statistics const spot::const_parsed_aut_ptr& haut = nullptr, const char* csv_prefix = nullptr, diff --git a/bin/common_output.cc b/bin/common_output.cc index 93cb2dfaf..6d414583a 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -160,6 +160,7 @@ namespace spot::formula f; const char* filename; const char* line; + unsigned index; const char* prefix; const char* suffix; }; @@ -237,6 +238,7 @@ namespace declare('R', &timer_); declare('r', &timer_); declare('L', &line_); + declare('l', &index_); declare('s', &size_); declare('h', &class_); declare('n', &nesting_); @@ -248,7 +250,8 @@ namespace } std::ostream& - print(const formula_with_location& fl, spot::process_timer* ptimer) + print(const formula_with_location& fl, + spot::process_timer* ptimer) { if (has('R') || has('r')) timer_ = *ptimer; @@ -256,6 +259,7 @@ namespace fl_ = &fl; filename_ = fl.filename ? fl.filename : ""; line_ = fl.line; + index_ = fl.index; prefix_ = fl.prefix ? fl.prefix : ""; suffix_ = fl.suffix ? fl.suffix : ""; auto f = fl_.val()->f; @@ -288,6 +292,7 @@ namespace printable_timer timer_; spot::printable_value filename_; spot::printable_value line_; + spot::printable_value index_; spot::printable_value prefix_; spot::printable_value suffix_; spot::printable_value size_; @@ -356,6 +361,7 @@ static void output_formula(std::ostream& out, spot::formula f, spot::process_timer* ptimer, const char* filename, const char* linenum, + unsigned index, const char* prefix, const char* suffix) { if (!format) @@ -391,7 +397,8 @@ output_formula(std::ostream& out, } else { - formula_with_location fl = { f, filename, linenum, prefix, suffix }; + formula_with_location fl = { f, filename, linenum, + index, prefix, suffix }; format->print(fl, ptimer); } } @@ -399,6 +406,7 @@ output_formula(std::ostream& out, void output_formula_checked(spot::formula f, spot::process_timer* ptimer, const char* filename, const char* linenum, + unsigned index, const char* prefix, const char* suffix) { if (output_format == count_output) @@ -414,7 +422,8 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer, if (outputnamer) { outputname.str(""); - formula_with_location fl = { f, filename, linenum, prefix, suffix }; + formula_with_location fl = { f, filename, linenum, + index, prefix, suffix }; outputnamer->print(fl, ptimer); std::string fname = outputname.str(); auto [it, b] = outputfiles.try_emplace(fname, nullptr); @@ -422,7 +431,7 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer, it->second.reset(new output_file(fname.c_str())); out = &it->second->ostream(); } - output_formula(*out, f, ptimer, filename, linenum, prefix, suffix); + output_formula(*out, f, ptimer, filename, linenum, index, prefix, suffix); *out << output_terminator; // Make sure we abort if we can't write to std::cout anymore // (like disk full or broken pipe with SIGPIPE ignored). @@ -432,10 +441,12 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer, void output_formula_checked(spot::formula f, spot::process_timer* ptimer, const char* filename, int linenum, + unsigned index, const char* prefix, const char* suffix) { output_formula_checked(f, ptimer, filename, std::to_string(linenum).c_str(), + index, prefix, suffix); } diff --git a/bin/common_output.hh b/bin/common_output.hh index 1cff67229..3b08db27f 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -81,11 +81,13 @@ void output_formula_checked(spot::formula f, spot::process_timer* ptimer = nullptr, const char* filename = nullptr, const char* linenum = nullptr, + unsigned output_index = 0U, const char* prefix = nullptr, const char* suffix = nullptr); void output_formula_checked(spot::formula f, spot::process_timer* ptimer, const char* filename, int linenum, + unsigned output_index, const char* prefix = nullptr, const char* suffix = nullptr); diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 4b2ec9662..6d7414587 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -129,7 +129,9 @@ namespace timer.start(); auto aut = post.run(haut->aut, nullptr); timer.stop(); - printer.print(aut, timer, nullptr, haut->filename.c_str(), -1, haut); + static unsigned index = 0; + printer.print(aut, timer, nullptr, haut->filename.c_str(), -1, + index++, haut); flush_cout(); return 0; } diff --git a/bin/genaut.cc b/bin/genaut.cc index f8d6b93ff..fbcffb48d 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -122,7 +122,8 @@ output_pattern(gen::aut_pattern_id pattern, int n) twa_graph_ptr aut = spot::gen::aut_pattern(pattern, n); timer.stop(); automaton_printer printer; - printer.print(aut, timer, nullptr, aut_pattern_name(pattern), n); + static unsigned serial = 0; + printer.print(aut, timer, nullptr, aut_pattern_name(pattern), n, serial++); } static void diff --git a/bin/genltl.cc b/bin/genltl.cc index ef8049171..79b71b699 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -192,6 +192,8 @@ static const argp_option options[] = "the formula (in the selected syntax)", 0 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the name of the pattern", 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "serial number of the output formula (0-based)", 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the argument of the pattern", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -287,6 +289,8 @@ parse_opt(int key, char* arg, struct argp_state*) } +static unsigned output_count = 0U; + static void output_pattern(gen::ltl_pattern_id pattern, int n, int n2) { @@ -303,14 +307,14 @@ output_pattern(gen::ltl_pattern_id pattern, int n, int n2) if (opt_positive || !opt_negative) { output_formula_checked(f, nullptr, gen::ltl_pattern_name(pattern), - args.c_str()); + args.c_str(), output_count++); } if (opt_negative) { std::string tmp = "!"; tmp += gen::ltl_pattern_name(pattern); output_formula_checked(formula::Not(f), nullptr, tmp.c_str(), - args.c_str()); + args.c_str(), output_count++); } } diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 73a9a23c6..1229cd422 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -155,8 +155,9 @@ namespace auto aut = trans.run(&f); timer.stop(); - printer.print(aut, timer, f, filename, linenum, nullptr, - prefix, suffix); + static unsigned index = 0; + printer.print(aut, timer, f, filename, linenum, index++, + nullptr, prefix, suffix); // If we keep simplification caches around, atomic propositions // will still be defined, and one translation may influence the // variable order of the next one. diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 6e7bf5ec7..c695631df 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -360,8 +360,7 @@ namespace const char* csv_prefix, const char* csv_suffix) { static long int output_count = 0; - ++output_count; - printer.print(aut, ptimer, f, filename, loc, nullptr, + printer.print(aut, ptimer, f, filename, loc, output_count++, nullptr, csv_prefix, csv_suffix); if (opt_max_count >= 0 && output_count >= opt_max_count) abort_run = true; @@ -420,8 +419,8 @@ namespace aut = post.run(aut, f); if (best_type) { - best_printer.print(nullptr, aut, f, filename, linenum, timer, - prefix, suffix); + best_printer.print(nullptr, aut, f, filename, linenum, 0, + timer, prefix, suffix); std::string aut_stats = best_stream.str(); if (!best_aut || (strverscmp(best_stats.c_str(), aut_stats.c_str()) diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 81e895d42..ed2f2d08d 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -254,6 +254,8 @@ static const argp_option options[] = "the formula (in the selected syntax)", 0 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the name of the input file", 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the serial number of the output formula", 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the original line number in the input file", 0 }, { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -852,7 +854,8 @@ namespace std::to_string(linenum).c_str()) << ")\n"; } one_match = true; - output_formula_checked(f, &timer, filename, linenum, prefix, suffix); + output_formula_checked(f, &timer, filename, linenum, + match_count, prefix, suffix); ++match_count; } return 0; diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index b59569a59..5e56f7d2c 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2019, 2022 Laboratoire de Recherche et +// Copyright (C) 2014-2019, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -87,6 +87,8 @@ static const argp_option options[] = { "the formula (in the selected syntax)", 0 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the name of the input file", 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the serial number of the output formula (0-based)", 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the original line number in the input file", 0 }, { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -112,6 +114,8 @@ static const argp_child children[] = { namespace { + static unsigned output_count = 0; + class mutate_processor final: public job_processor { public: @@ -122,7 +126,8 @@ namespace auto mutations = spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort); for (auto g: mutations) - output_formula_checked(g, nullptr, filename, linenum, prefix, suffix); + output_formula_checked(g, nullptr, filename, linenum, + output_count++, prefix, suffix); return 0; } }; diff --git a/bin/randaut.cc b/bin/randaut.cc index 1ceb82ee0..4e2065c2a 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018-2020, 2022 Laboratoire de Recherche +// Copyright (C) 2012-2016, 2018-2020, 2022, 2023 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -406,7 +406,8 @@ main(int argc, char** argv) timer.stop(); printer.print(aut, timer, nullptr, - opt_seed_str, automaton_num, nullptr); + opt_seed_str, automaton_num, + automaton_num, nullptr); ++automaton_num; if (opt_automata > 0 && automaton_num >= opt_automata) diff --git a/bin/randltl.cc b/bin/randltl.cc index 749fcf373..4dacf5264 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -115,8 +115,10 @@ static const argp_option options[] = "the following interpreted sequences:", -19 }, { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the formula (in the selected syntax)", 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the (serial) number of the formula (0-based)", 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "the (serial) number of the formula", 0 }, + "the (serial) number of the formula (1-based)", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, COMMON_LTL_OUTPUT_SPECS, @@ -305,9 +307,9 @@ main(int argc, char** argv) exit(0); } + int count = 0; while (opt_formulas < 0 || opt_formulas--) { - static int count = 0; spot::formula f = rg.next(); if (!f) { @@ -316,7 +318,8 @@ main(int argc, char** argv) } else { - output_formula_checked(f, nullptr, nullptr, ++count); + output_formula_checked(f, nullptr, nullptr, count + 1, count); + ++count; } }; flush_cout(); diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 65687e493..1d5d8a7cb 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -725,7 +725,8 @@ randaut --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' (iw) inherently weak. Use uppercase letters to negate them. %d 1 if the output is deterministic, 0 otherwise - %e number of reachable edges + %e, %[LETTER]e number of edges (add one LETTER to select (r) + reachable [default], (u) unreachable, (a) all). %F seed number %g, %[LETTERS]g acceptance condition (in HOA syntax); add brackets to print an acceptance name instead and LETTERS to @@ -740,6 +741,7 @@ randaut --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' %[opt]h to specify additional options as in --hoa=opt) %L automaton number + %l serial number of the output automaton (0-based) %m name of the automaton %n number of nondeterministic states in output %p 1 if the output is complete, 0 otherwise @@ -749,8 +751,11 @@ randaut --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' LETTERS to restrict to(u) user time, (s) system time, (p) parent process, or (c) children processes. - %s number of reachable states - %t number of reachable transitions + %s, %[LETTER]s number of states (add one LETTER to select (r) + reachable [default], (u) unreachable, (a) all). + %t, %[LETTER]t number of transitions (add one LETTER to select + (r) reachable [default], (u) unreachable, (a) + all). %u, %[e]u number of states (or [e]dges) with universal branching %u, %[LETTER]u 1 if the automaton contains some universal @@ -996,6 +1001,14 @@ randaut -D -n 20 -Q2 1 -o '>>out-det%d.hoa' (You need the quotes so that the shell does not interpret =>>=.) +The =%l= sequence is a number that is incremented for each output +automaton. For instance if =input.hoa= contains multiple automata, +you can separate them into separate files with: + +#+BEGIN_SRC sh :exports code +autilt input.hoa -o output-%l.hoa +#+END_SRC + #+BEGIN_SRC sh :results silent :exports results rm -f out-det0.hoa out-det1.hoa #+END_SRC diff --git a/tests/Makefile.am b/tests/Makefile.am index 3bd43d5f4..7e8a42347 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -230,6 +230,7 @@ TESTS_twa = \ core/cube.test \ core/alternating.test \ core/gamehoa.test \ + core/serial.test \ core/ltlcross3.test \ core/ltlcross5.test \ core/taatgba.test \ diff --git a/tests/core/serial.test b/tests/core/serial.test new file mode 100755 index 000000000..285c04807 --- /dev/null +++ b/tests/core/serial.test @@ -0,0 +1,71 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +# all tools should be able to use %l as serial number for their output + +# Make sure serial numbers count the output automata +randaut -n10 --name='aut %l' 2 | + autfilt -N3..5 --name='%M/out %l' | + autfilt --stats=%M >out +cat >exp < aut.hoa +rm aut-?.hoa +autfilt aut.hoa -o aut-%l.hoa + +# check serial output in various tools +genaut --m-nba=2..3 --name='%F=%L/%l' | autfilt --stats=%M >out +genltl --and-f=2..3 --stats=%F=%L/%l >> out +ltl2tgba a b --name=%f/%l | autfilt --stats=%M >> out +ltldo -f a -f b ltl2tgba --name=%f/%l | autfilt --stats=%M >> out +genltl --or-g=2..5 --stats=%L,%l,%f | + ltlfilt -F -/3 -N 2..3 --stats='%<,%l' >>out +randltl -n10 3 --stats=%l,%f | + ltlfilt -F -/2 -N 2..3 --stats='%<,%l' >> out +cat >exp<