diff --git a/NEWS b/NEWS index 0cd10ab2b..70319502c 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,14 @@ New in spot 2.3.5.dev (not yet released) Tools: + - genaut is a new binary that produces families of automata defined + in the literature (in the same way as we have genltl for LTL + formulas). + + - autcross is a new binary that compares the output of tools + transforming automata (in the same way as we have ltlcross for + LTL translators). + - autfilt learned to build the union (--sum) or the intersection (--sum-and) of two language by putting two automata side-by-side and fiddling with the initial states. This complement the already @@ -11,9 +19,6 @@ New in spot 2.3.5.dev (not yet released) - autfilt learned to complement any alternating automaton with option --dualize. - - genaut is a binary to produce families of automata defined in the - literature (in the same way as we have genltl for LTL formulas). - - autfilt learned --split-edges to convert labels that are Boolean formulas into labels that are min-terms. (See spot::split_edges() below.) diff --git a/bin/.gitignore b/bin/.gitignore index 27ff66e07..e993c0a55 100644 --- a/bin/.gitignore +++ b/bin/.gitignore @@ -1,3 +1,4 @@ +autcross autfilt dstar2tgba genaut diff --git a/bin/Makefile.am b/bin/Makefile.am index 09f84f932..9469b535f 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -59,6 +59,7 @@ libcommon_a_SOURCES = \ common_trans.hh bin_PROGRAMS = \ + autcross \ autfilt \ dstar2tgba \ genaut \ @@ -77,6 +78,7 @@ bin_PROGRAMS = \ # version number that is automatically updated). noinst_PROGRAMS = spot-x spot +autcross_SOURCES = autcross.cc autfilt_SOURCES = autfilt.cc ltlfilt_SOURCES = ltlfilt.cc genaut_SOURCES = genaut.cc diff --git a/bin/autcross.cc b/bin/autcross.cc new file mode 100644 index 000000000..b75f277c1 --- /dev/null +++ b/bin/autcross.cc @@ -0,0 +1,898 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 . + + +#include "common_sys.hh" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include "error.h" +#include "argmatch.h" + +#include "common_setup.hh" +#include "common_hoaread.hh" +#include "common_finput.hh" +#include "common_color.hh" +#include "common_trans.hh" +#include "common_cout.hh" +#include "common_aoutput.hh" +#include "common_post.hh" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +const char argp_program_doc[] ="\ +Call several tools that process automata and cross-compare their output \ +to detect bugs, or to gather statistics. The list of automata to use \ +should be supplied on standard input, or using the -f or -F options.\v\ +Exit status:\n\ + 0 everything went fine (timeouts are OK too)\n\ + 1 some tools failed to output something we understand, or failed\n\ + sanity checks (statistics were output nonetheless)\n\ + 2 autcross aborted on error\n\ +"; + +enum { + OPT_BOGUS = 256, + OPT_CSV, + OPT_HIGH, + OPT_IGNORE_EXEC_FAIL, + OPT_LANG, + OPT_LOW, + OPT_MEDIUM, + OPT_NOCHECKS, + OPT_OMIT, + OPT_STOP_ERR, + OPT_VERBOSE, +}; + +static const argp_option options[] = + { + { nullptr, 0, nullptr, 0, "Input:", 1 }, + { "file", 'F', "FILENAME", 0, + "process automata from FILENAME", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "autcross behavior:", 5 }, + { "stop-on-error", OPT_STOP_ERR, nullptr, 0, + "stop on first execution error or failure to pass" + " sanity checks (timeouts are OK)", 0 }, + { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0, + "ignore automata from translators that return with a non-zero exit code," + " but do not flag this as an error", 0 }, + { "language-preserved", OPT_LANG, nullptr, 0, + "expect that each tool preserves the input language", 0 }, + { "no-checks", OPT_NOCHECKS, nullptr, 0, + "do not perform any sanity checks", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Statistics output:", 7 }, + { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL, + "output statistics as CSV in FILENAME or on standard output " + "(if '>>' is used to request append mode, the header line is " + "not output)", 0 }, + { "omit-missing", OPT_OMIT, nullptr, 0, + "do not output statistics for timeouts or failed translations", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Simplification level (for complementation):", + 21 }, + { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 }, + { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 }, + { "high", OPT_HIGH, nullptr, 0, + "all available optimizations (slow, default)", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Miscellaneous options:", -2 }, + { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0, + "save formulas for which problems were detected in FILENAME", 0 }, + { "verbose", OPT_VERBOSE, nullptr, 0, + "print what is being done, for debugging", 0 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } + }; + +const struct argp_child children[] = + { + { &autproc_argp, 0, nullptr, 0 }, + { &hoaread_argp, 0, "Parsing of automata:", 4 }, + { &misc_argp, 0, nullptr, -2 }, + { &color_argp, 0, nullptr, 0 }, + { nullptr, 0, nullptr, 0 } + }; + +static bool verbose = false; +static bool ignore_exec_fail = false; +static unsigned ignored_exec_fail = 0; +static bool stop_on_error = false; +static bool no_checks = false; +static bool opt_language_preserved = false; +static bool opt_omit = false; +static const char* csv_output = nullptr; +static unsigned round_num = 0; +static const char* bogus_output_filename = nullptr; +static output_file* bogus_output = nullptr; + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + switch (key) + { + case 'F': + jobs.emplace_back(arg, true); + break; + case OPT_BOGUS: + { + bogus_output = new output_file(arg); + bogus_output_filename = arg; + break; + } + case OPT_CSV: + csv_output = arg ? arg : "-"; + break; + case OPT_HIGH: + level = spot::postprocessor::High; + level_set = true; + break; + case OPT_IGNORE_EXEC_FAIL: + ignore_exec_fail = true; + break; + case OPT_LANG: + opt_language_preserved = true; + break; + case OPT_LOW: + level = spot::postprocessor::Low; + level_set = true; + break; + case OPT_MEDIUM: + level = spot::postprocessor::Medium; + level_set = true; + break; + case OPT_NOCHECKS: + no_checks = true; + break; + case OPT_OMIT: + opt_omit = true; + break; + case OPT_STOP_ERR: + stop_on_error = true; + break; + case OPT_VERBOSE: + verbose = true; + break; + case ARGP_KEY_ARG: + if (arg[0] == '-' && !arg[1]) + jobs.emplace_back(arg, true); + else + tools_push_autproc(arg); + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +static bool global_error_flag = false; +// static unsigned oom_count = 0U; + +static std::ostream& +global_error() +{ + global_error_flag = true; + std::cerr << bright_red; + return std::cerr; +} + +static void +end_error() +{ + std::cerr << reset_color; +} + +static std::ostream& +example() +{ + std::cerr << bold_std; + return std::cerr; +} + + +struct aut_statistics +{ + unsigned ap; + unsigned states; + unsigned edges; + unsigned transitions; + unsigned acc_sets; + unsigned scc; + unsigned nondetstates; + bool nondeterministic; + bool alternating; + + aut_statistics() + { + } + + void set(const spot::const_twa_graph_ptr& aut) + { + if (!csv_output) + // Do not waste time. + return; + ap = aut->ap().size(); + spot::twa_sub_statistics s = sub_stats_reachable(aut); + states = s.states; + edges = s.edges; + transitions = s.transitions; + spot::scc_info m(aut); + acc_sets = aut->num_sets(); + unsigned c = m.scc_count(); + scc = c; + nondetstates = spot::count_nondet_states(aut); + nondeterministic = nondetstates != 0; + alternating = !aut->is_existential(); + } + + void to_csv(std::ostream& os) const + { + os << ap << ',' + << states << ',' + << edges << ',' + << transitions << ',' + << acc_sets << ',' + << scc << ',' + << nondetstates << ',' + << nondeterministic << ',' + << alternating; + } + + void empty(std::ostream& os) const + { + os << ",,,,,,,,"; + } + + static void fields(std::ostream& os, const char* prefix) + { + os << '"' + << prefix << "ap\",\"" + << prefix << "states\",\"" + << prefix << "edges\",\"" + << prefix << "transitions\",\"" + << prefix << "acc_sets\",\"" + << prefix << "scc\",\"" + << prefix << "nondetstates\",\"" + << prefix << "nondeterministic\",\"" + << prefix << "alternating\""; + } +}; + +struct in_statistics +{ + std::string input_source; + std::string input_name; + aut_statistics input; + + static void fields(std::ostream& os) + { + os << "\"input.source\",\"input.name\","; + aut_statistics::fields(os, "input."); + } + + void to_csv(std::ostream& os) const + { + spot::escape_rfc4180(os << '"', input_source) << "\","; + if (!input_name.empty()) + spot::escape_rfc4180(os << '"', input_name) << "\","; + else + os << ','; + input.to_csv(os); + } +}; + +struct out_statistics +{ + + // If OK is false, output statistics are not available. + bool ok; + const char* status_str; + int status_code; + double time; + aut_statistics output; + + out_statistics() + : ok(false), + status_str(nullptr), + status_code(0), + time(0) + { + } + + static void fields(std::ostream& os) + { + os << "\"exit_status\",\"exit_code\",\"time\","; + aut_statistics::fields(os, "output."); + } + + void to_csv(std::ostream& os) const + { + os << '"' << status_str << "\"," << status_code << ',' + << time << ','; + if (ok) + output.to_csv(os); + else + output.empty(os); + } +}; + +std::vector input_statistics; +typedef std::vector vector_tool_statistics; +std::vector output_statistics; + +namespace +{ + class autcross_runner final: public autproc_runner + { + spot::bdd_dict_ptr dict; + public: + autcross_runner(spot::bdd_dict_ptr dict) + : dict(dict) + { + } + + spot::twa_graph_ptr + run_tool(unsigned int tool_num, char l, bool& problem, + out_statistics& stats) + { + output.reset(tool_num); + + std::ostringstream command; + format(command, tools[tool_num].cmd); + + std::string cmd = command.str(); + std::cerr << "Running [" << l << tool_num << "]: " + << cmd << std::endl; + process_timer timer; + timer.start(); + int es = exec_with_timeout(cmd.c_str()); + timer.stop(); + const char* status_str = nullptr; + + spot::twa_graph_ptr res = nullptr; + if (timed_out) + { + // This is not considered to be a global error. + std::cerr << "warning: timeout during execution of command\n"; + ++timeout_count; + status_str = "timeout"; + problem = false; // A timeout is not a sign of a bug + es = -1; + } + else if (WIFSIGNALED(es)) + { + status_str = "signal"; + problem = true; + es = WTERMSIG(es); + global_error() << "error: execution terminated by signal " + << es << ".\n"; + end_error(); + } + else if (WIFEXITED(es) && WEXITSTATUS(es) != 0) + { + es = WEXITSTATUS(es); + status_str = "exit code"; + if (!ignore_exec_fail) + { + problem = true; + global_error() << "error: execution returned exit code " + << es << ".\n"; + end_error(); + } + else + { + problem = false; + std::cerr << "warning: execution returned exit code " + << es << ".\n"; + ++ignored_exec_fail; + } + } + else + { + status_str = "ok"; + problem = false; + es = 0; + + auto aut = spot::parse_aut(output.val()->name(), dict, + spot::default_environment::instance(), + opt_parse); + if (!aut->errors.empty()) + { + status_str = "parse error"; + problem = true; + es = -1; + std::ostream& err = global_error(); + err << "error: failed to parse the produced automaton.\n"; + aut->format_errors(err); + end_error(); + res = nullptr; + } + else if (aut->aborted) + { + status_str = "aborted"; + problem = true; + es = -1; + global_error() << "error: aborted HOA file.\n"; + end_error(); + res = nullptr; + } + else + { + res = aut->aut; + } + } + output.cleanup(); + + stats.status_str = status_str; + stats.status_code = es; + stats.time = timer.get_lap_sw(); + if (res) + { + stats.ok = true; + stats.output.set(res); + } + return res; + } + }; + + static std::string + autname(unsigned i, bool complemented = false) + { + std::ostringstream str; + if (complemented) + str << "Comp("; + if (i < tools.size()) + str << 'A' << i; + else + str << "input"; + if (complemented) + str << ')'; + return str.str(); + } + + static bool + check_empty_prod(const spot::const_twa_graph_ptr& aut_i, + const spot::const_twa_graph_ptr& aut_j, + size_t i, size_t j) + { + if (aut_i->num_sets() + aut_j->num_sets() + > 8 * sizeof(spot::acc_cond::mark_t::value_t)) + { + std::cerr << "info: building " << autname(i) + << '*' << autname(j, true) + << " requires more acceptance sets than supported\n"; + return false; + } + + auto prod = spot::product(aut_i, aut_j); + + if (verbose) + std::cerr << "info: check_empty " + << autname(i) << '*' << autname(j, true) << '\n'; + + auto w = prod->accepting_word(); + if (w) + { + std::ostream& err = global_error(); + err << "error: " << autname(i) << '*' << autname(j, true) + << (" is nonempty; both automata accept the infinite word:\n" + " "); + example() << *w << '\n'; + end_error(); + } + return !!w; + } + + class autcross_processor final: public hoa_processor + { + autcross_runner runner; + public: + autcross_processor() + : hoa_processor(spot::make_bdd_dict()), runner(dict_) + { + } + + int + process_automaton(const spot::const_parsed_aut_ptr& haut) override + { + auto printsize = [](const spot::const_twa_graph_ptr& aut, + bool props) + { + std::cerr << '(' << aut->num_states() << " st.," + << aut->num_edges() << " ed.," + << aut->num_sets() << " sets)"; + if (props) + { + if (!aut->is_existential()) + std::cerr << " univ-edges"; + if (is_deterministic(aut)) + std::cerr << " deterministic"; + if (is_complete(aut)) + std::cerr << " complete"; + std::cerr << '\n'; + } + }; + + spot::twa_graph_ptr input = haut->aut; + runner.round_automaton(input, round_num); + + std::string source = [&]() + { + std::ostringstream src; + src << haut->filename << ':' << haut->loc; + return src.str(); + }(); + + 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.set(input); + + int problems = 0; + size_t m = tools.size(); + size_t mi = m + opt_language_preserved; + std::vector pos(mi); + std::vector neg(mi); + vector_tool_statistics stats(m); + + if (opt_language_preserved) + pos[mi - 1] = input; + + if (verbose) + { + std::cerr << "info: input\t"; + printsize(input, true); + } + + for (size_t n = 0; n < m; ++n) + { + bool prob; + pos[n] = runner.run_tool(n, 'A', prob, stats[n]); + problems += prob; + } + spot::cleanup_tmpfiles(); + ++round_num; + output_statistics.push_back(std::move(stats)); + + if (verbose) + { + std::cerr << "info: collected automata:\n"; + for (unsigned i = 0; i < m; ++i) + if (pos[i]) + { + std::cerr << "info: A" << i << '\t'; + printsize(pos[i], true); + } + } + + if (!no_checks) + { + std::cerr << "Performing sanity checks and gathering statistics..." + << std::endl; + + { + bool print_first = true; + for (unsigned i = 0; i < mi; ++i) + { + if (!pos[i]) + continue; + if (!pos[i]->is_existential()) + { + if (verbose) + { + if (print_first) + { + std::cerr << + "info: getting rid of universal edges...\n"; + print_first = false; + } + std::cerr << "info: " + << std::setw(8) << autname(i) << '\t'; + printsize(pos[i], false); + std::cerr << " -> "; + } + pos[i] = remove_alternation(pos[i]); + if (verbose) + { + printsize(pos[i], false); + std::cerr << '\n'; + } + } + if (is_universal(pos[i])) + neg[i] = dualize(pos[i]); + } + } + + { + bool print_first = verbose; + for (unsigned i = 0; i < mi; ++i) + { + if (pos[i] && !neg[i]) + { + if (print_first) + { + std::cerr << "info: complementing non-deterministic " + "automata via determinization...\n"; + print_first = false; + } + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(level); + neg[i] = dualize(p.run(pos[i])); + if (verbose) + { + std::cerr << "info: " + << std::setw(8) << autname(i) << '\t'; + printsize(pos[i], false); + std::cerr << " -> "; + printsize(neg[i], false); + std::cerr << '\t' << autname(i, true) << '\n'; + } + } + }; + } + + { + bool print_first = true; + auto tmp = [&](std::vector& x, unsigned i, + bool neg) + { + if (!x[i]) + return; + if (x[i]->acc().uses_fin_acceptance()) + { + if (verbose) + { + if (print_first) + { + std::cerr << + "info: getting rid of any Fin acceptance...\n"; + print_first = false; + } + std::cerr << "info: " + << std::setw(8) << autname(i, neg) << '\t'; + printsize(x[i], false); + std::cerr << " ->"; + } + cleanup_acceptance_here(x[i]); + x[i] = remove_fin(x[i]); + if (verbose) + { + std::cerr << ' '; + printsize(x[i], false); + std::cerr << '\n'; + } + } + else + { + // Remove useless sets nonetheless. + cleanup_acceptance_here(x[i]); + } + }; + for (unsigned i = 0; i < mi; ++i) + { + tmp(pos, i, false); + tmp(neg, i, true); + } + } + + // Just make a circular implication check + // A0 <= A1, A1 <= A2, ..., AN <= A0 + unsigned ok = 0; + for (size_t i = 0; i < mi; ++i) + if (pos[i]) + { + size_t j = ((i + 1) % mi); + if (i != j && neg[j]) + { + int res = check_empty_prod(pos[i], neg[j], i, j); + problems += res; + ok += !res; + } + } + // If the circular check failed, do the rest of all + // mi(mi-1)/2 checks, as this will help diagnose the issue. + if (ok != mi) + for (size_t i = 0; i < mi; ++i) + if (pos[i]) + { + size_t k = ((i + 1) % mi); + for (size_t j = 0; j < mi; ++j) + if (i != j && j != k && neg[j]) + problems += check_empty_prod(pos[i], neg[j], i, j); + } + } + else + { + std::cerr << "Gathering statistics..." << std::endl; + } + + + if (problems && bogus_output) + print_hoa(bogus_output->ostream(), input) << std::endl; + + std::cerr << std::endl; + + // Shall we stop processing now? + abort_run = global_error_flag && stop_on_error; + return problems; + } + }; +} + +// Output an RFC4180-compatible CSV file. +static void +print_stats_csv(const char* filename) +{ + if (verbose) + std::cerr << "info: writing CSV to " << filename << '\n'; + + output_file outf(filename); + std::ostream& out = outf.ostream(); + + unsigned ntools = tools.size(); + assert(round_num == output_statistics.size()); + assert(round_num == input_statistics.size()); + + if (!outf.append()) + { + // Do not output the header line if we append to a file. + // (Even if that file was empty initially.) + in_statistics::fields(out); + out << ",\"tool\","; + out_statistics::fields(out); + out << '\n'; + } + for (unsigned r = 0; r < round_num; ++r) + for (unsigned t = 0; t < ntools; ++t) + if (!opt_omit || output_statistics[r][t].ok) + { + input_statistics[r].to_csv(out); + out << ",\""; + spot::escape_rfc4180(out, tools[t].name); + out << "\","; + output_statistics[r][t].to_csv(out); + out << '\n'; + } + outf.close(filename); +} + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, parse_opt, "[COMMANDFMT...]", + argp_program_doc, children, nullptr, nullptr }; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + check_no_automaton(); + + auto s = tools.size(); + if (s == 0) + error(2, 0, "No tool to run? Run '%s --help' for usage.", + program_name); + + if (s == 1 && !opt_language_preserved && !no_checks) + error(2, 0, "Since --language-preserved is not used, you need " + "at least two tools to compare."); + + + setup_color(); + setup_sig_handler(); + + autcross_processor p; + if (p.run()) + return 2; + + if (round_num == 0) + { + error(2, 0, "no automaton to translate"); + } + else + { + if (global_error_flag) + { + std::ostream& err = global_error(); + if (bogus_output) + err << ("error: some error was detected during the above runs.\n" + " Check file ") + << bogus_output_filename + << " for problematic automata."; + else + err << ("error: some error was detected during the above runs,\n" + " please search for 'error:' messages in the above" + " trace."); + err << std::endl; + end_error(); + } + else if (timeout_count == 0 && ignored_exec_fail == 0) + { + std::cerr << "No problem detected." << std::endl; + } + else + { + std::cerr << "No major problem detected." << std::endl; + } + + unsigned additional_errors = 0U; + additional_errors += timeout_count > 0; + additional_errors += ignored_exec_fail > 0; + if (additional_errors) + { + std::cerr << (global_error_flag ? "Additionally, " : "However, "); + if (timeout_count) + { + if (additional_errors > 1) + std::cerr << "\n - "; + if (timeout_count == 1) + std::cerr << "1 timeout occurred"; + else + std::cerr << timeout_count << " timeouts occurred"; + } + + if (ignored_exec_fail) + { + if (additional_errors > 1) + std::cerr << "\n - "; + if (ignored_exec_fail == 1) + std::cerr << "1 non-zero exit status was ignored"; + else + std::cerr << ignored_exec_fail + << " non-zero exit statuses were ignored"; + } + if (additional_errors == 1) + std::cerr << '.'; + std::cerr << std::endl; + } + } + + if (csv_output) + print_stats_csv(csv_output); + + return global_error_flag; +} diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e321b8c62..555e1a67c 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -515,7 +515,7 @@ static bool opt_highlight_languages = false; static spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) { - if ((!nonalt || aut->is_existential()) && spot::is_deterministic(aut)) + if ((!nonalt || aut->is_existential()) && spot::is_universal(aut)) return aut; spot::postprocessor p; p.set_type(spot::postprocessor::Generic); diff --git a/bin/common_hoaread.hh b/bin/common_hoaread.hh index 8e8516585..b7ddc47a4 100644 --- a/bin/common_hoaread.hh +++ b/bin/common_hoaread.hh @@ -43,6 +43,7 @@ read_automaton(const char* filename, spot::bdd_dict_ptr& dict); class hoa_processor: public job_processor { +protected: spot::bdd_dict_ptr dict_; public: diff --git a/bin/common_trans.cc b/bin/common_trans.cc index 9b029b550..9af739e1d 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -33,14 +33,17 @@ #include #include "common_conv.hh" #include +#include +#include +#include // A set of tools for which we know the correct output -static struct shorthands_t +struct shorthands_t { const char* prefix; const char* suffix; -} - shorthands[] = { +}; +static shorthands_t shorthands_ltl[] = { { "lbt", " <%L>%O" }, { "ltl2ba", " -f %s>%O" }, { "ltl2da", " %f>%O" }, @@ -55,25 +58,30 @@ static struct shorthands_t { "spin", " -f %s>%O" }, }; -static void show_shorthands() +static shorthands_t shorthands_autproc[] = { + { "autfilt", " %H>%O" }, + { "dstar2tgba", " %H>%O" }, + { "ltl2dstar", " -B %H %O" }, + { "nba2ldpa", " <%H>%O" }, + { "seminator", " %H>%O" }, + }; + +static void show_shorthands(shorthands_t* begin, shorthands_t* end) { std::cout << ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n" "the following words, then the string on the right is appended.\n\n"); - for (auto& s: shorthands) - std::cout << " " - << std::left << std::setw(12) << s.prefix - << s.suffix << '\n'; - std::cout - << ("\nAny {name} and directory component is skipped for the purpose of\n" - "matching those prefixes. So for instance\n" - " '{DRA} ~/mytools/ltl2dstar-0.5.2'\n" - "will changed into\n" - " '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'\n"); + while (begin != end) + { + std::cout << " " + << std::left << std::setw(12) << begin->prefix + << begin->suffix << '\n'; + ++begin; + } } -tool_spec::tool_spec(const char* spec) +tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end) : spec(spec), cmd(spec), name(spec) { if (*cmd == '{') @@ -114,8 +122,9 @@ tool_spec::tool_spec(const char* spec) ++pos; } // Match a shorthand. - for (auto& p: shorthands) + while (begin != end) { + auto& p = *begin++; int n = strlen(p.prefix); if (strncmp(basename, p.prefix, n) == 0) { @@ -165,6 +174,20 @@ tool_spec::~tool_spec() std::vector tools; +void tools_push_trans(const char* trans) +{ + tools.emplace_back(trans, + std::begin(shorthands_ltl), + std::end(shorthands_ltl)); +} + +void tools_push_autproc(const char* proc) +{ + tools.emplace_back(proc, + std::begin(shorthands_autproc), + std::end(shorthands_autproc)); +} + void quoted_string::print(std::ostream& os, const char*) const { @@ -254,16 +277,8 @@ printable_result_filename::print(std::ostream& os, const char*) const spot::quote_shell_string(os, val()->name()); } -void -filed_formula::print(std::ostream& os, const char* pos) const -{ - std::ostringstream ss; - f_.print(ss, pos); - os << '\'' << string_to_tmp(ss.str(), serial_) << '\''; -} - -std::string -filed_formula::string_to_tmp(const std::string str, unsigned n) const +static std::string +string_to_tmp(const std::string str, unsigned n) { char prefix[30]; snprintf(prefix, sizeof prefix, "lcr-i%u-", n); @@ -278,6 +293,43 @@ filed_formula::string_to_tmp(const std::string str, unsigned n) const return tmpname; } +void +filed_formula::print(std::ostream& os, const char* pos) const +{ + std::ostringstream ss; + f_.print(ss, pos); + os << '\'' << string_to_tmp(ss.str(), serial_) << '\''; +} + +void +filed_automaton::print(std::ostream& os, const char* pos) const +{ + std::ostringstream ss; + char* opt = nullptr; + if (*pos == '[') + { + ++pos; + auto end = strchr(pos, ']'); + opt = strndup(pos, end - pos); + pos = end + 1; + } + switch (*pos) + { + case 'H': + spot::print_hoa(ss, aut_, opt); + break; + case 'S': + spot::print_never_claim(ss, aut_, opt); + break; + case 'L': + spot::print_lbtt(ss, aut_, opt); + break; + } + if (opt) + free(opt); + os << '\'' << string_to_tmp(ss.str(), serial_) << '\''; +} + translator_runner::translator_runner(spot::bdd_dict_ptr dict, bool no_output_allowed) : dict(dict) @@ -345,6 +397,42 @@ translator_runner::round_formula(spot::formula f, unsigned serial) filename_formula.new_round(serial); } + +autproc_runner::autproc_runner(bool no_output_allowed) +{ + declare('H', &filename_automaton); + declare('S', &filename_automaton); + declare('L', &filename_automaton); + declare('O', &output); + + size_t s = tools.size(); + assert(s); + for (size_t n = 0; n < s; ++n) + { + // Check that each translator uses at least one input and + // one output. + std::vector has(256); + const tool_spec& t = tools[n]; + scan(t.cmd, has); + if (!(has['H'] || has['S'] || has['L'])) + error(2, 0, "no input %%-sequence in '%s'.\n Use " + "one of %%H,%%S,%%L to indicate the input automaton filename.", + t.spec); + if (!no_output_allowed && !has['O']) + error(2, 0, "no output %%-sequence in '%s'.\n Use " + "%%O to indicate where the automaton is output.", + t.spec); + // Remember the %-sequences used by all tools. + prime(t.cmd); + } +} + +void +autproc_runner::round_automaton(spot::const_twa_graph_ptr aut, unsigned serial) +{ + filename_automaton.new_round(aut, serial); +} + volatile bool timed_out = false; unsigned timeout_count = 0; @@ -553,7 +641,7 @@ exec_command(const char* cmd) int fd0 = open(stdin, O_RDONLY, 0644); if (fd0 < 0) error(2, errno, "failed to open '%s'", stdin); - if (dup2(fd0, 0) < 0) + if (dup2(fd0, STDIN_FILENO) < 0) error(2, errno, "dup2() failed"); if (close(fd0) < 0) error(2, errno, "close() failed"); @@ -563,7 +651,7 @@ exec_command(const char* cmd) int fd1 = creat(stdout, 0644); if (fd1 < 0) error(2, errno, "failed to open '%s'", stdout); - if (dup2(fd1, 1) < 0) + if (dup2(fd1, STDOUT_FILENO) < 0) error(2, errno, "dup2() failed"); if (close(fd1) < 0) error(2, errno, "close() failed"); @@ -602,6 +690,11 @@ exec_with_timeout(const char* cmd) if (child_pid == 0) { setpgid(0, 0); + // Close stdin so that children may not read our input. We had + // this nice surprise with Seminator, who greedily consumes its + // stdin (which was also ours) even if it does not use it + // because it was given a file. + close(STDIN_FILENO); exec_command(cmd); // never reached return -1; @@ -675,7 +768,7 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) switch (key) { case 't': - tools.push_back(arg); + tools_push_trans(arg); break; case 'T': timeout = to_pos_int(arg); @@ -685,7 +778,14 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) #endif break; case OPT_LIST: - show_shorthands(); + show_shorthands(std::begin(shorthands_ltl), std::end(shorthands_ltl)); + std::cout + << ("\nAny {name} and directory component is skipped for the purpose " + "of\nmatching those prefixes. So for instance\n " + "'{DRA} ~/mytools/ltl2dstar-0.5.2'\n" + "will be changed into\n " + "'{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MW]L %O'" + "\n"); exit(0); case OPT_RELABEL: opt_relabel = true; @@ -698,3 +798,61 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) const struct argp trans_argp = { options, parse_opt_trans, nullptr, nullptr, nullptr, nullptr, nullptr }; + + + +static const argp_option options_aut[] = +{ + /**************************************************/ + { nullptr, 0, nullptr, 0, "Specifying tools to call:", 2 }, + { "tool", 't', "COMMANDFMT", 0, + "register one tool to call", 0 }, + { "timeout", 'T', "NUMBER", 0, "kill tools after NUMBER seconds", 0 }, + { "list-shorthands", OPT_LIST, nullptr, 0, + "list availabled shorthands to use in COMMANDFMT", 0}, + /**************************************************/ + { nullptr, 0, nullptr, 0, + "COMMANDFMT should specify input and output arguments using the " + "following character sequences:", 3 }, + { "%H,%S,%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "filename for the input automaton in (H) HOA, (S) Spin's neverclaim, " + "or (L) LBTT's format", 0 }, + { "%O", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "filename for the automaton output in HOA, never claim, LBTT, or " + "ltl2dstar's format", 0 }, + { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } +}; + +static int parse_opt_autproc(int key, char* arg, struct argp_state*) +{ + switch (key) + { + case 't': + tools_push_autproc(arg); + break; + case 'T': + timeout = to_pos_int(arg); +#if !ENABLE_TIMEOUT + std::cerr << "warning: setting a timeout is not supported " + << "on your platform" << std::endl; +#endif + break; + case OPT_LIST: + show_shorthands(std::begin(shorthands_autproc), + std::end(shorthands_autproc)); + std::cout + << ("\nAny {name} and directory component is skipped for the purpose " + "of\nmatching those prefixes. So for instance\n " + "'{AF} ~/mytools/autfilt-2.4 --remove-fin'\n" + "will be changed into\n " + "'{AF} ~/mytools/autfilt-2.4 --remove-fin %H>%O'\n"); + exit(0); + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +const struct argp autproc_argp = { options_aut, parse_opt_autproc, nullptr, + nullptr, nullptr, nullptr, nullptr }; diff --git a/bin/common_trans.hh b/bin/common_trans.hh index 6054a21d8..2811ebc61 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -28,9 +28,13 @@ #include -extern const struct argp trans_argp; +extern const struct argp trans_argp; // ltlcross, ltldo +extern const struct argp autproc_argp; // autcross + extern bool opt_relabel; +struct shorthands_t; + struct tool_spec { // The translator command, as specified on the command-line. @@ -44,7 +48,7 @@ struct tool_spec // name of the translator (or spec) const char* name; - tool_spec(const char* spec); + tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end); tool_spec(const tool_spec& other); tool_spec& operator=(const tool_spec& other); ~tool_spec(); @@ -52,6 +56,9 @@ struct tool_spec extern std::vector tools; +void tools_push_trans(const char* trans); +void tools_push_autproc(const char* proc); + struct quoted_string final: public spot::printable_value { using spot::printable_value::operator=; @@ -80,7 +87,25 @@ struct filed_formula final: public spot::printable private: const quoted_formula& f_; unsigned serial_; - std::string string_to_tmp(const std::string str, unsigned n) const; +}; + +struct filed_automaton final: public spot::printable +{ + filed_automaton() + { + } + + void print(std::ostream& os, const char* pos) const override; + + void new_round(spot::const_twa_graph_ptr aut, unsigned serial) + { + aut_ = aut; + serial_ = serial; + } + + private: + spot::const_twa_graph_ptr aut_; + unsigned serial_; }; struct printable_result_filename final: @@ -118,6 +143,23 @@ public: }; +class autproc_runner: protected spot::formater +{ +protected: + // Round-specific variables + filed_automaton filename_automaton; + // Run-specific variables + printable_result_filename output; +public: + using spot::formater::has; + + autproc_runner(// whether we accept the absence of output + // specifier + bool no_output_allowed = false); + void round_automaton(spot::const_twa_graph_ptr aut, unsigned serial); +}; + + // Disable handling of timeout on systems that miss kill() or alarm(). // For instance MinGW. #if HAVE_KILL && HAVE_ALARM diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 7252bd319..d6cb397a1 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -219,7 +219,6 @@ example() return std::cerr; } - static void end_error() { @@ -423,7 +422,7 @@ parse_opt(int key, char* arg, struct argp_state*) if (arg[0] == '-' && !arg[1]) jobs.emplace_back(arg, true); else - tools.push_back(arg); + tools_push_trans(arg); break; case OPT_AUTOMATA: opt_automata = true; @@ -1111,7 +1110,7 @@ namespace std::vector& comp, unsigned i) { - if (!no_complement && x[i] && is_deterministic(x[i])) + if (!no_complement && x[i] && is_universal(x[i])) comp[i] = dualize(x[i]); }; diff --git a/bin/ltldo.cc b/bin/ltldo.cc index dfae4a0a6..0916e8195 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -171,7 +171,7 @@ parse_opt(int key, char* arg, struct argp_state*) if (arg[0] == '-' && !arg[1]) jobs.emplace_back(arg, true); else - tools.push_back(arg); + tools_push_trans(arg); break; default: return ARGP_ERR_UNKNOWN; diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am index bbf314adf..e2a704eed 100644 --- a/bin/man/Makefile.am +++ b/bin/man/Makefile.am @@ -25,6 +25,7 @@ convman7 = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ "$(PERL)" "$(top_srcdir)/tools/help2man -s7 -N" dist_man1_MANS = \ + autcross.1 \ autfilt.1 \ dstar2tgba.1 \ genaut.1 \ @@ -44,6 +45,9 @@ dist_man7_MANS = \ MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS) EXTRA_DIST = $(dist_man1_MANS:.1=.x) $(dist_man7_MANS:.7=.x) +autcross.1: $(common_dep) $(srcdir)/autcross.x $(srcdir)/../autcross.cc + $(convman) ../autcross$(EXEEXT) $(srcdir)/autcross.x $@ + autfilt.1: $(common_dep) $(srcdir)/autfilt.x $(srcdir)/../autfilt.cc $(convman) ../autfilt$(EXEEXT) $(srcdir)/autfilt.x $@ diff --git a/bin/man/autcross.x b/bin/man/autcross.x new file mode 100644 index 000000000..4158aca11 --- /dev/null +++ b/bin/man/autcross.x @@ -0,0 +1,97 @@ +.\" -*- coding: utf-8 -*- +[NAME] +autcross \- cross-compare tools that process automata + +[ENVIRONMENT VARIABLES] +.TP +\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR +These variables control in which directory temporary files (e.g., +those who contain the input and output when interfacing with +translators) are created. \fBTMPDIR\fR is only read if +\fBSPOT_TMPDIR\fR does not exist. If none of these environment +variables exist, or if their value is empty, files are created in the +current directory. +.TP +\fBSPOT_TMPKEEP\fR +When this variable is defined, temporary files are not removed. +This is mostly useful for debugging. + +[OUTPUT DATA] +The following columns are output in the CSV files. +.TP +\fBinput.source\fR +Location of the input automaton fed to the tool. +.TP +\fBinput.name\fR +Name of the input automaton, if any. This is supported +by the HOA format. +.TP +\fBinput.ap\fR,\fBoutput.ap\fR, +Number of atomic proposition in the input and output automata. +.TP +\fBinput.states\fR,\fBoutput.states\fR +Number of states in the input and output automata. +.TP +\fBinput.edges\fR,\fBoutput.edges\fR +Number of edges in the input and output automata. +.TP +\fBinput.transitions\fR,\fBoutput.transitions\fR +Number of transitions in the input and output automata. +.TP +\fBinput.acc_sets\fR,\fBoutput.acc_sets\fR +Number of acceptance sets in the input and output automata. +.TP +\fBinput.scc\fR,\fBoutput.scc\fR +Number of strongly connected components in the input and output automata. +.TP +\fBinput.nondetstates\fR,\fBoutput.nondetstates\fR +Number of nondeterministic states in the input and output automata. +.TP +\fBinput.nondeterministic\fR,\fBoutput.nondetstates\fR +1 if the automaton is nondeterministic, 0 if it is deterministic. +.TP +\fBinput.alternating\fR,\fBoutput.alternating\fR +1 if the automaton has some universal branching, 0 otherwise. + +\fBexit_status\fR, \fBexit_code\fR +Information about how the execution of the tool went. +\fBexit_status\fR is a string that can take the following +values: +.RS +.TP +\f(CW"ok"\fR +The tool ran succesfully (this does not imply that the produced +automaton is correct) and autcross could parse the resulting +automaton. In this case \fBexit_code\fR is always 0. +.TP +\f(CW"timeout"\fR +The tool ran for more than the number of seconds +specified with the \fB\-\-timeout\fR option. In this +case \fBexit_code\fR is always -1. +.TP +\f(CW"exit code"\fR +The tool terminated with a non-zero exit code. +\fBexit_code\fR contains that value. +.TP +\f(CW"signal"\fR +The tool terminated with a signal. +\fBexit_code\fR contains that signal's number. +.TP +\f(CW"parse error"\fR +The tool terminated normally, but autcross could not +parse its output. In this case \fBexit_code\fR is always -1. +.TP +\f(CW"no output"\fR +The tool terminated normally, but without creating the specified +output file. In this case \fBexit_code\fR is always -1. +.RE +.TP +\fBtime\fR +A floating point number giving the run time of the tool in seconds. +This is reported for all executions, even failling ones. + +[SEE ALSO] +.BR randaut (1), +.BR genaut (1), +.BR autfilt (1), +.BR ltlcross (1) diff --git a/doc/Makefile.am b/doc/Makefile.am index 220ab4b36..a63221a08 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -78,6 +78,7 @@ ORG_FILES = \ org/spot.css \ org/arch.tex \ $(srcdir)/org/arch.png \ + org/autcross.org \ org/autfilt.org \ org/csv.org \ org/citing.org \ diff --git a/doc/org/autcross.org b/doc/org/autcross.org new file mode 100644 index 000000000..c0f04a6c5 --- /dev/null +++ b/doc/org/autcross.org @@ -0,0 +1,388 @@ +# -*- coding: utf-8 -*- +#+TITLE: =autcross= +#+DESCRIPTION: Spot command-line tool for cross-comparing the output of automaton processors. +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tools.html + +=autcross= is a tool for cross-comparing the output of tools that +transform automata. It works similarly to [[file:ltlcross.org][=ltlcross=]] except that +inputs are automata. + +The core of =autcross= is a loop that does the following steps: + - Input an automaton + - Process that input automaton with all the configured tools. + If there are 3 translators, the automata produced by those tools + will be named =A0=, =A1=, and =A2=. + - Ensure that all produced automata are equivalent. + +Statistics about the results of each tools can optionally be saved in +a CSV file. And in case only those statistics matters, it is also +possible to disable the equivalence checks. + +* Input automata + +The input automata can be supplied either on standard input, or in +files specified with option =-F=. + +If an input automaton is expressed in the HOA format and has a name, +that name will be displayed by =autcross= when processing the automaton, +and will appear in the CSV file if such a file is output. + +* Specifying the tools to test + +Each tool should be specified as a string that uses some of the +following character sequences: + +#+BEGIN_SRC sh :results verbatim :exports results + autcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: %% a single % +: %H,%S,%L filename for the input automaton in (H) HOA, (S) +: Spin's neverclaim, or (L) LBTT's format +: %O filename for the automaton output in HOA, never +: claim, LBTT, or ltl2dstar's format + +For instance we can use =autfilt --complement %H >%O= to indicate that +=autfilt= reads one file (=%H=) in the HOA format, and to redirect the +output in file so that =autcross= can find it. The output format is +automatically detected, so a generic =%O= is used for the output file +regardless of its format. + +Another tool that can complement automata is =ltl2dstar=, using +the syntax =ltl2dstar -B --complement-input=yes %H %O=. So to +compare the results of these two tools we could use: + +#+BEGIN_SRC sh :results verbatim :exports code +randaut -B -n 3 a b | +autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O' +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports output +randaut -B -n 3 a b | +autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O' 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +-:1.1-45.7 +Running [A0]: autfilt --complement 'lcr-i0-Nr1xZO' >'lcr-o0-urHakt' +Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i0-mmkgH7' 'lcr-o1-ABdm4L' +Performing sanity checks and gathering statistics... + +-:46.1-92.7 +Running [A0]: autfilt --complement 'lcr-i1-5kMYrq' >'lcr-o0-9kvBP4' +Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i1-lVlGfJ' 'lcr-o1-BexLFn' +Performing sanity checks and gathering statistics... + +-:93.1-137.7 +Running [A0]: autfilt --complement 'lcr-i2-rjvy61' >'lcr-o0-rKKlxG' +Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i2-Musr0k' 'lcr-o1-LyAxtZ' +Performing sanity checks and gathering statistics... + +No problem detected. +#+end_example + +In this example, we generate 3 random Büchi automata (because +=ltl2dstar= expects Büchi automata as input) using [[file:randaut.org][=randaut=]], and pipe +them to =autcross=. For each of those automata, =autcross= display +the source location of that automaton (here =-= indicate that the +automaton is read from standard input, and this is followed by +=beginline.column-endline.colum= specifying the position of that +automaton in the input. If the automata had names, they would +be displayed as well. + +Then, each tool is called using temporary files to exchange the +automata, and the resulting automata are then compared. The last line +specifies that no problem was detected. + + +To simplify the use of some known tools, a set of predefined +shorthands are available. Those can be listed with the +=--list-shorthands= option. + +#+BEGIN_SRC sh :results verbatim :exports both +autcross --list-shorthands +#+END_SRC +#+RESULTS: +#+begin_example +If a COMMANDFMT does not use any %-sequence, and starts with one of +the following words, then the string on the right is appended. + + autfilt %H>%O + seminator %H>%O + ltl2dstar -B %H %O + nba2ldpa <%H>%O + +Any {name} and directory component is skipped for the purpose of +matching those prefixes. So for instance + '{AF} ~/mytools/autfilt-2.4 --remove-fin' +will be changed into + '{AF} ~/mytools/autfilt-2.4 --remove-fin %H>%O' +#+end_example + +What this implies is our previous example could be shortened to: + +#+BEGIN_SRC sh :results verbatim :exports code +randaut -B -n 3 a b | +autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' +#+END_SRC + +* Getting statistics + +Detailed statistics about the result of each translation, and the +product of that resulting automaton with the random state-space, can +be obtained using the =--csv=FILE= option. + +** CSV output + +Let's take our example and modify it in two ways. First we pass a +=--name= option to =randaut= to give each automaton a name (in +=randaut=, =%L= denotes the serial number of the automaton); this is +mostly a cosmetic change, so that =autcross= will display names. +Second, we pass a =--csv= option to =autcross= to save statistics in a +file. + + +#+BEGIN_SRC sh :results verbatim :exports code +randaut -B -n 3 a b --name="automaton %L" | +autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --csv=autcross.csv +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +randaut -B -n 3 a b --name="automaton %L" | +autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --csv=autcross.csv 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +-:1.1-46.7 automaton 0 +Running [A0]: autfilt --complement 'lcr-i0-QHReWu'>'lcr-o0-0eTOmZ' +Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-jsoPPt' 'lcr-o1-66bQiY' +Performing sanity checks and gathering statistics... + +-:47.1-94.7 automaton 1 +Running [A0]: autfilt --complement 'lcr-i1-IubpMs'>'lcr-o0-dfmYfX' +Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i1-13NXLr' 'lcr-o1-zSwXhW' +Performing sanity checks and gathering statistics... + +-:95.1-140.7 automaton 2 +Running [A0]: autfilt --complement 'lcr-i2-g5bDOq'>'lcr-o0-X71ilV' +Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i2-og1mUp' 'lcr-o1-QVurtU' +Performing sanity checks and gathering statistics... + +No problem detected. +#+end_example + +After this execution, the file =autcross.csv= contains the following: + +#+BEGIN_SRC sh :results verbatim :exports results +cat autcross.csv +#+END_SRC +#+RESULTS: +: "input.source","input.name","input.ap","input.states","input.edges","input.transitions","input.acc_sets","input.scc","input.nondetstates","input.nondeterministic","input.alternating","tool","exit_status","exit_code","time","output.ap","output.states","output.edges","output.transitions","output.acc_sets","output.scc","output.nondetstates","output.nondeterministic","output.alternating" +: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"autfilt --complement","ok",0,0.0129685,2,27,95,108,3,2,0,0,0 +: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"ltl2dstar --complement-input=yes","ok",0,0.00202496,2,34,121,136,6,2,0,9,0 +: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"autfilt --complement","ok",0,0.0128458,2,58,216,232,3,2,0,9,0 +: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"ltl2dstar --complement-input=yes","ok",0,0.0026184,2,74,268,296,6,2,0,8,0 +: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"autfilt --complement","ok",0,0.0127144,2,21,69,84,2,4,0,20,0 +: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"ltl2dstar --complement-input=yes","ok",0,0.00180888,2,24,74,96,2,4,0,35,0 + +This file can then be loaded in any spreadsheet or statistical application. + +When computing such statistics, you should be aware that inputs for +which a tool failed to generate an automaton (e.g. it crashed, or it +was killed if you used =autcross='s =--timeout= option to limit run +time) will appear with empty columns at the end of the CSV line. +Those lines with missing data can be omitted with the =--omit-missing= +option. + +However data for bogus automata are still included: as shown below +=autcross= will report inconsistencies between automata as errors, but +it does not try to guess who is incorrect. + +The column names should be almost self-explanatory. See the [[./man/autcross.1.html][man page]] +for a description of the columns. + +** Changing the name of the translators + +By default, the names used in the CSV output to designate the +tools are the command specified on the command line. Like with +=ltlcross=, this can be adjusted by using a command specification of +the form ={short name}actual command=. + +For instance + +#+BEGIN_SRC sh :results verbatim :exports both +randaut -B -n 3 a b --name="automaton %L" | +autcross '{AF}autfilt --complement' '{L2D}ltl2dstar --complement-input=yes' --csv +#+END_SRC + +#+RESULTS: +: "input.source","input.name","input.ap","input.states","input.edges","input.transitions","input.acc_sets","input.scc","input.nondetstates","input.nondeterministic","input.alternating","tool","exit_status","exit_code","time","output.ap","output.states","output.edges","output.transitions","output.acc_sets","output.scc","output.nondetstates","output.nondeterministic","output.alternating" +: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"AF","ok",0,0.039722,2,27,95,108,3,2,0,0,0 +: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"L2D","ok",0,0.00640371,2,34,121,136,6,2,0,9,0 +: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"AF","ok",0,0.0400776,2,58,216,232,3,2,0,9,0 +: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"L2D","ok",0,0.00489558,2,74,268,296,6,2,0,20,0 +: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"AF","ok",0,0.0220585,2,21,69,84,2,4,0,7,0 +: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"L2D","ok",0,0.00329786,2,24,74,96,2,4,0,23,0 + +* Language preserving transformation + +By default =autcross= assumes that for a given input the automata +produced by all tools should be equivalent. However it does not +assume that those language should be equivalent to the input (it is +clearly not the case in our complementation test above). + +If the transformation being tested does preserve the language of an +automaton, it is worth to pass the =--language-preserved= option to +=autfilt=. Doing so a bit like adding =cat %H>%O= as another tool: it +will also ensure that the output is equivalent to the input. + +* Detecting problems + :PROPERTIES: + :CUSTOM_ID: checks + :END: + +If a translator exits with a non-zero status code, or fails to output +an automaton =autcross= can read, and error will be displayed and the +result of the tool will be discarded. + +Otherwise =autcross= performs equivalence checks between each pair of +automata. This is done in two steps. First, all produced automata +=A0=, =A1=, etc. are complemented: the complement automata are +named =Comp(A0)=, =Comp(A1)= etc. Second, =autcross= ensures +that =Ai*Comp(Aj)= is empty for all =i= and =j=. + +If the =--language-preserved= option is passed, the =input= automaton +also participate to these equivalence checks. + + +To simulate a problem, let's compare pretend we want verify that +=autfilt --complement= preserves the input language (clearly it does +not, since it actually complement the language of the automaton). + +#+BEGIN_SRC sh :results verbatim :exports code +randaut -B -n 3 a b --name="automaton %L" | +autcross --language-preserved 'autfilt --complement' +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports output +randaut -B -n 3 a b --name="automaton %L" | +autcross --language-preserved 'autfilt --complement' 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +-:1.1-46.7 automaton 0 +Running [A0]: autfilt --complement 'lcr-i0-3gRqrd'>'lcr-o0-ubUpHb' +Performing sanity checks and gathering statistics... +error: A0*Comp(input) is nonempty; both automata accept the infinite word: + !a & !b; a & !b; cycle{!a & !b; a & !b; !a & b; !a & b; !a & !b; !a & b; !a & b; !a & !b} +error: input*Comp(A0) is nonempty; both automata accept the infinite word: + !a & !b; !a & !b; cycle{!a & !b; !a & b; a & b} + +-:47.1-94.7 automaton 1 +Running [A0]: autfilt --complement 'lcr-i1-JxFi09'>'lcr-o0-oQGbj8' +Performing sanity checks and gathering statistics... +error: A0*Comp(input) is nonempty; both automata accept the infinite word: + !a & b; cycle{a & !b} +error: input*Comp(A0) is nonempty; both automata accept the infinite word: + !a & b; a & !b; cycle{!a & b; a & b} + +-:95.1-140.7 automaton 2 +Running [A0]: autfilt --complement 'lcr-i2-SQT7E6'>'lcr-o0-kWt404' +Performing sanity checks and gathering statistics... +error: A0*Comp(input) is nonempty; both automata accept the infinite word: + a & !b; !a & !b; cycle{a & !b; !a & b} +error: input*Comp(A0) is nonempty; both automata accept the infinite word: + cycle{!a & b; !a & b; !a & !b; a & !b; a & !b; !a & !b} + +error: some error was detected during the above runs, + please search for 'error:' messages in the above trace. +#+end_example + +Here, for each automaton, we get an example of word that is accepted +by the automaton and rejected by the input (i.e., accepted by +=Comp(input)=), as well as an example of word accepted by the input +but rejected by the automaton (i.e. accepted by =Comp(A0)=). Those +examples would not exit if the language was really preserved by the +tool. + +Incoherence between the output of several tools (even with +=--language-preserved=) are reported in a similar way. + +* Miscellaneous options + +** =--stop-on-error= + +The =--stop-on-error= option will cause =autcross= to abort on the +first detected error. This include failure to start some tool, +read its output, or failure to passe the sanity checks. Timeouts are +allowed. + +One use for this option is when =autcross= is used in combination with +=randaut= to check tools on an infinite stream of formulas. + +** =--save-bogus=FILENAME= + +The =--save-bogus=FILENAME= will save any automaton for which an error +was detected (either some tool failed, or some problem was +detected using the resulting automata) in =FILENAME=. Again, timeouts +are not considered to be errors, and therefore not reported in this +file. + +The main use for this feature is in conjunction with =randaut='s +generation of random formulas. For instance the following command +will run the translators on an infinite number of formulas, saving +any problematic formula in =bugs.ltl=. + +** =--no-check= + +The =--no-check= option disables all sanity checks. This +makes sense if you only care about the output of =--csv=. + +** =--verbose= + +The verbose option can be useful to troubleshoot problems or simply +follow the list of transformations and tests performed by =autcross=. + +#+BEGIN_SRC sh :results verbatim :exports code +randaut -B -n 1 a b --name="automaton %L" | +autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --verbose +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +randaut -B -n 1 a b --name="automaton %L" | +autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --verbose 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +-:1.1-46.7 automaton 0 +info: input (10 st.,26 ed.,1 sets) +Running [A0]: autfilt --complement 'lcr-i0-oZm5P2'>'lcr-o0-O4P0IB' +Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-gEwlJa' 'lcr-o1-wSaHJJ' +info: collected automata: +info: A0 (27 st.,95 ed.,3 sets) deterministic complete +info: A1 (34 st.,121 ed.,6 sets) deterministic complete +Performing sanity checks and gathering statistics... +info: getting rid of any Fin acceptance... +info: A0 (27 st.,95 ed.,3 sets) -> (58 st.,203 ed.,2 sets) +info: Comp(A0) (27 st.,95 ed.,3 sets) -> (51 st.,188 ed.,1 sets) +info: A1 (34 st.,121 ed.,6 sets) -> (64 st.,228 ed.,3 sets) +info: Comp(A1) (34 st.,121 ed.,6 sets) -> (34 st.,121 ed.,1 sets) +info: check_empty A0*Comp(A1) +info: check_empty A1*Comp(A0) + +No problem detected. +#+end_example + +# 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 +# LocalWords: COMMANDFMT seminator nba ldpa QHReWu eTOmZ jsoPPt ilV +# LocalWords: bQiY IubpMs dfmYfX NXLr zSwXhW bDOq og mUp QVurtU ap +# LocalWords: ok complementation Ai Aj gRqrd ubUpHb JxFi oQGbj SQT +# LocalWords: kWt Eo Xsc WXgCB vLwKMQ tI SXF qqlE KXplk ZFTCz PNY +# LocalWords: hUAK IjnFhD cWys ZqjdQh diff --git a/doc/org/tools.org b/doc/org/tools.org index 9c9339c5c..9925367dc 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -47,13 +47,14 @@ corresponding commands are hidden. - [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-automata translators. - [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL formula. +- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]] + and [[file:oaut.org][output]] interfaces. - [[file:dstar2tgba.org][=dstar2tgba=]] Convert \omega-automata with any acceptance into variants of Büchi automata. - [[file:randaut.org][=randaut=]] Generate random \omega-automata. - [[file:genaut.org][=genaut=]] Generate ω-automata from scalable patterns. - [[file:autfilt.org][=autfilt=]] Filter, convert, and transform \omega-automata. -- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]] - and [[file:oaut.org][output]] interfaces. +- [[file:autcross.org][=autcross=]] Cross-compare tools that process automata. * Man pages @@ -63,6 +64,7 @@ automatically from the =--help= output of each tool, and often completed with additional text (like examples or bibliography). For convenience, you can browse their HTML versions: +[[./man/autcross.1.html][=autcross=]](1), [[./man/autfilt.1.html][=autfilt=]](1), [[./man/dstar2tgba.1.html][=dstar2tgba=]](1), [[./man/genaut.1.html][=genaut=]](1), diff --git a/tests/Makefile.am b/tests/Makefile.am index 9410309b5..02c30ff45 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -293,6 +293,8 @@ TESTS_twa = \ core/ltlcross.test \ core/spotlbtt2.test \ core/ltlcross2.test \ + core/autcross.test \ + core/autcross2.test \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ diff --git a/tests/core/autcross.test b/tests/core/autcross.test new file mode 100755 index 000000000..87bace1d2 --- /dev/null +++ b/tests/core/autcross.test @@ -0,0 +1,45 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 + +# Skip this test if ltl2dstar is not installed. +(ltl2dstar --version) || exit 77 + +randaut -n10 2 | +autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ + --csv=out.csv 2>stderr + +# 5 lines per input automaton, and 1 "No problem detected" line. +test 51 = `wc -l < stderr` +grep -q 'sanity check' stderr + +# --no-check still allows to build a CSV +randaut -n10 2 | +autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ + --csv=out2.csv --no-check 2>stderr +test 51 = `wc -l < stderr` +grep -q 'sanity check' stderr && exit 1 + +for f in out.csv out2.csv; do + sed 's/,[0-9]*\.[0-9]*,/,TIME,/' $f > _$f +done +diff _out.csv _out2.csv diff --git a/tests/core/autcross2.test b/tests/core/autcross2.test new file mode 100755 index 000000000..81e037cd1 --- /dev/null +++ b/tests/core/autcross2.test @@ -0,0 +1,30 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 + +randaut -n10 2 | tee input | +autcross --language-preserve 'autfilt' 'autfilt --complement' \ + --save-bogus=bogus.hoa 2>stderr && exit 1 +cat stderr +# We should have 4 counterexample per input automaton +test 40 = `grep 'both automata accept the infinite word:' stderr | wc -l` +diff input bogus.hoa diff --git a/tests/core/dra2dba.test b/tests/core/dra2dba.test index 20b6586f5..6ecb52957 100755 --- a/tests/core/dra2dba.test +++ b/tests/core/dra2dba.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2014, 2017 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -329,5 +329,5 @@ Acc-Sig: +2 13 EOF -test `dstar2tgba -D in.dra --stats="%d:%s:%e"` = "1:23:143" - +autcross 'dstar2tgba -D' --language-preserved -F in.dra --csv=out.csv +grep '3,23,143,184,1,2,0,0,0$' out.csv diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index c2c715581..5102d659a 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -163,7 +163,7 @@ test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s` # Test case from Thibaud Michaud. This used to fail, because sbacc() # would remove acceptance marks from all rejecting SCCS... -cat >tm.hoa < out.hoa -autfilt -q --equivalent-to out.hoa tm.hoa # Tautological acceptances are converted to "t" cat >taut.hoa < out.hoa -autfilt -q --equivalent-to streett.hoa out.hoa +run 0 autcross --language-preserved \ + 'autfilt --tgba %H | tee out.hoa >%O' -F streett.hoa grep 'generalized-Buchi 2' out.hoa