diff --git a/NEWS b/NEWS index 81aaf9a22..78a14561b 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 2.10.4.dev (net yet released) associated option --sonf-aps allows listing the newly introduced atomic propositions. + - autcross learned a --language-complemented option to assist in the + case one is testing tools that complement automata. (issue #504). + Library: - The new function suffix_operator_normal_form() implements diff --git a/THANKS b/THANKS index 9eb566483..b49b3eb95 100644 --- a/THANKS +++ b/THANKS @@ -41,6 +41,7 @@ Michael Weber Mikuláš Klokočka Ming-Hsien Tsai Nikos Gorogiannis +Ondřej Lengál Paul Guénézan Reuben Rowe Roei Nahum diff --git a/bin/autcross.cc b/bin/autcross.cc index 81b6bcef5..2aade5e49 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement de +// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -64,6 +64,7 @@ Exit status:\n\ enum { OPT_BOGUS = 256, + OPT_COMPLEMENTED, OPT_CSV, OPT_HIGH, OPT_FAIL_ON_TIMEOUT, @@ -94,6 +95,8 @@ static const argp_option options[] = "consider timeouts as errors", 0 }, { "language-preserved", OPT_LANG, nullptr, 0, "expect that each tool preserves the input language", 0 }, + { "language-complemented", OPT_COMPLEMENTED, nullptr, 0, + "expect that each tool complements the input language", 0 }, { "no-checks", OPT_NOCHECKS, nullptr, 0, "do not perform any sanity checks", 0 }, /**************************************************/ @@ -144,6 +147,7 @@ static bool fail_on_timeout = false; static bool stop_on_error = false; static bool no_checks = false; static bool opt_language_preserved = false; +static bool opt_language_complemented = false; static bool opt_omit = false; static const char* csv_output = nullptr; static unsigned round_num = 0; @@ -170,6 +174,9 @@ parse_opt(int key, char* arg, struct argp_state*) bogus_output_filename = arg; break; } + case OPT_COMPLEMENTED: + opt_language_complemented = true; + break; case OPT_CSV: csv_output = arg ? arg : "-"; break; @@ -533,25 +540,32 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j) { + auto is_really_comp = [lc = opt_language_complemented, + ts = tools.size()](unsigned i) { + return lc && i == ts; + }; + if (aut_i->num_sets() + aut_j->num_sets() > spot::acc_cond::mark_t::max_accsets()) { if (!quiet) - std::cerr << "info: building " << autname(i) - << '*' << autname(j, true) + std::cerr << "info: building " << autname(i, is_really_comp(i)) + << '*' << autname(j, true ^ is_really_comp(j)) << " requires more acceptance sets than supported\n"; return false; } if (verbose) std::cerr << "info: check_empty " - << autname(i) << '*' << autname(j, true) << '\n'; + << autname(i, is_really_comp(i)) + << '*' << autname(j, true ^ is_really_comp(j)) << '\n'; auto w = aut_i->intersecting_word(aut_j); if (w) { std::ostream& err = global_error(); - err << "error: " << autname(i) << '*' << autname(j, true) + err << "error: " << autname(i, is_really_comp(i)) + << '*' << autname(j, true ^ is_really_comp(j)) << (" is nonempty; both automata accept the infinite word:\n" " "); example() << *w << '\n'; @@ -621,12 +635,15 @@ namespace int problems = 0; size_t m = tools.size(); - size_t mi = m + opt_language_preserved; + size_t mi = m + opt_language_preserved + opt_language_complemented; std::vector pos(mi); std::vector neg(mi); vector_tool_statistics stats(m); - if (opt_language_preserved) + // For --language-complemented, we store the input automata in + // pos and will compute its complement in neg. Before running + // checks we will swap both automata. + if (opt_language_preserved || opt_language_complemented) pos[mi - 1] = input; if (verbose) @@ -718,6 +735,9 @@ namespace }; } + if (opt_language_complemented) + std::swap(pos[mi - 1], neg[mi - 1]); + // Just make a circular implication check // A0 <= A1, A1 <= A2, ..., AN <= A0 unsigned ok = 0; @@ -824,10 +844,15 @@ main(int argc, char** argv) check_no_automaton(); - 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."); + if (s == 1 && !no_checks + && !opt_language_preserved + && !opt_language_complemented) + error(2, 0, "Since --language-preserved and --language-complemented " + "are not used, you need at least two tools to compare."); + if (opt_language_preserved && opt_language_complemented) + error(2, 0, "Options --language-preserved and --language-complemented " + "are incompatible."); setup_color(); setup_sig_handler(); diff --git a/doc/org/autcross.org b/doc/org/autcross.org index 90a268b44..9e4972cf6 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -249,7 +249,7 @@ EOF | -:95.1-140.7 | automaton 2 | 2 | 10 | 26 | 26 | 1 | 2 | 6 | 1 | 0 | AF | ok | 0 | 0.0211636 | 2 | 21 | 66 | 84 | 2 | 4 | 0 | 0 | 0 | | -:95.1-140.7 | automaton 2 | 2 | 10 | 26 | 26 | 1 | 2 | 6 | 1 | 0 | L2D | ok | 0 | 0.0028508 | 2 | 24 | 74 | 96 | 2 | 4 | 0 | 0 | 0 | -* Language preserving transformation +* Transformation that preserve or complement languages By default =autcross= assumes that for a given input the automata produced by all tools should be equivalent. However it does not @@ -261,6 +261,13 @@ 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. +Similarly, if the tools being tested implement complementation +algorithm, adding the =--language-complemented= will additionally +compare the outputs using this own complementation algorithm. Using +this option is more efficient than passing =autfilt --complement= as a +tool, since =autcross= can save on complementation by using the input +automaton. + * Detecting problems :PROPERTIES: :CUSTOM_ID: checks diff --git a/tests/core/autcross.test b/tests/core/autcross.test index 2ac14eb34..b3d27ec0a 100755 --- a/tests/core/autcross.test +++ b/tests/core/autcross.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2018, 2022 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -46,3 +46,17 @@ for f in out.csv out2.csv; do sed 's/,[0-9]*\.[0-9]*,/,TIME,/' $f > _$f done diff _out.csv _out2.csv + + +# The {autfilt {complement}} name makes sure we can nest braces. +randaut -n10 2 | + autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ + --language-complemented --csv=out3.csv --verbose 2>stderr +test 10 = `grep 'check_empty Comp(input)\*Comp(A0)' stderr | wc -l` + + +randaut -n1 2 | + autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ + --language-complemented --language-preserved 2> stderr && exit 1 +cat stderr +grep 'preserved.*complemented.*incompatible' stderr