diff --git a/NEWS b/NEWS index 28a6d6305..86707167b 100644 --- a/NEWS +++ b/NEWS @@ -13,10 +13,15 @@ New in spot 2.1.0a (not yet released) * autfilt --stats learned the missing %D, %N, %P, and %W sequences, to complete the existing %d, %n, %p, and %w. + * The --stats %c option of ltl2tgba, autfilt, ltldo, and dstar2tgba + now accepts option to filter the SCCs to count. For instance + --stats='%[awT]c' will count the SCCs that are (a)ccepting and + (w)eak, but (not t)erminal. See --help for all supported filters. + Bugs fixed: * Fix several cases where command-line tools would fail to diagnose - write errors (e.g. when writing to filesystem that is full). + write errors (e.g. when writing to a filesystem that is full). New in spot 2.1 (2016-08-08) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 46b6ad6fd..d2c37b15e 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -167,8 +167,12 @@ static const argp_option io_options[] = "number of acceptance sets", 0 }, { "%G, %g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "acceptance condition (in HOA syntax)", 0 }, - { "%C, %c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of SCCs", 0 }, + { "%C, %c, %[LETTERS]C, %[LETTERS]c", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, + "number of SCCs; you may filter the SCCs to count " + "using the following LETTERS, possibly concatenated: (a) accepting, " + "(r) rejecting, (v) trivial, (t) terminal, (w) weak, " + "(iw) inherently weak. Use uppercase letters to negate them.", 0 }, { "%N, %n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of nondeterministic states", 0 }, { "%D, %d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -216,8 +220,11 @@ static const argp_option o_options[] = "number of acceptance sets", 0 }, { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "acceptance condition (in HOA syntax)", 0 }, - { "%c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of SCCs", 0 }, + { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of SCCs; you may filter the SCCs to count " + "using the following LETTERS, possibly concatenated: (a) accepting, " + "(r) rejecting, (v) trivial, (t) terminal, (w) weak, " + "(iw) inherently weak. Use uppercase letters to negate them.", 0 }, { "%n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of nondeterministic states in output", 0 }, { "%d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index 64cffef3b..e0ec92e3d 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -27,7 +27,8 @@ #include #include #include -#include +#include +#include namespace spot { @@ -123,9 +124,119 @@ namespace spot print_psl(os, val_); }; - void printable_scc_info::print(std::ostream& os, const char*) const + void printable_scc_info::print(std::ostream& os, const char* pos) const { - os << val_->scc_count(); + unsigned n = val_->scc_count(); + if (*pos != '[') + { + os << n; + return; + } + bool accepting = false; + bool rejecting = false; + bool trivial = false; + bool non_trivial = false; + bool terminal = false; + bool non_terminal = false; + bool weak = false; + bool non_weak = false; + bool inherently_weak = false; + bool non_inherently_weak = false; + + const char* beg = pos; + auto error = [&](std::string str) + { + std::ostringstream tmp; + const char* end = std::strchr(pos, ']'); + tmp << "unknown option '" << str << "' in '%" + << std::string(beg, end + 2) << '\''; + throw std::runtime_error(tmp.str()); + }; + + do + { + ++pos; + switch (*pos) + { + case 'a': + case 'R': + accepting = true; + break; + case 'A': + case 'r': + rejecting = true; + break; + case 'v': + trivial = true; + break; + case 'V': + non_trivial = true; + break; + case 't': + terminal = true; + break; + case 'T': + non_terminal = true; + break; + case 'w': + weak = true; + break; + case 'W': + non_weak = true; + break; + case 'i': + if (pos[1] == 'w') + inherently_weak = true; + else + error(std::string(pos, pos + 2)); + break; + case 'I': + if (pos[1] == 'W') + non_inherently_weak = true; + else + error(std::string(pos, pos + 2)); + break; + case ' ': + case '\t': + case '\n': + case ',': + case ']': + break; + default: + error(std::string(pos, pos + 1)); + } + } + while (*pos != ']'); + + val_->determine_unknown_acceptance(); + unsigned count = 0U; + + for (unsigned i = 0; i < n; ++i) + { + if (accepting && val_->is_rejecting_scc(i)) + continue; + if (rejecting && val_->is_accepting_scc(i)) + continue; + if (trivial && !val_->is_trivial(i)) + continue; + if (non_trivial && val_->is_trivial(i)) + continue; + if (terminal && !is_terminal_scc(*val_, i)) + continue; + if (non_terminal && is_terminal_scc(*val_, i)) + continue; + if (weak && !is_weak_scc(*val_, i)) + continue; + if (non_weak && is_weak_scc(*val_, i)) + continue; + if (inherently_weak && !is_inherently_weak_scc(*val_, i)) + continue; + if (non_inherently_weak && is_inherently_weak_scc(*val_, i)) + continue; + ++count; + } + + os << count; }; diff --git a/tests/core/format.test b/tests/core/format.test index ce56666ab..67a7ce0b3 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -59,3 +59,10 @@ test "1,0" = "`ltl2tgba FGa | autfilt -D --stats='%N,%n'`" test "4" = "`ltl2tgba '(Ga -> Gb)W c' --stats=%c`" test "4,5" = "`ltl2tgba '(Ga -> Gb)W c' | autfilt -C --stats=%C,%c`" + +out=`ltl2tgba '(Ga->Gb)W c' --stats=%[r]c,%[a]c,%[t]c,%[w]c,%[wT]c,%[W]c,%[Wt]c` +test "1,3,1,3,2,1,0" = "$out" + +ltl2tgba 'a' --stats='%[z]c' 2>stderr && exit 1 +cat stderr +grep -F "ltl2tgba: unknown option 'z' in '%[z]c'" stderr