Commit 571f0112 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bin: add options for --stats=%c

* spot/twaalgos/stats.cc: Implement options.
* bin/common_aoutput.cc, NEWS: Document them.
* tests/core/format.test: Add some quick tests.
parent 4f0a630d
......@@ -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)
......
......@@ -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,
......
......@@ -27,7 +27,8 @@
#include <spot/twaalgos/reachiter.hh>
#include <spot/tl/print.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <cstring>
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;
};
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment