alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

stats: add options to count unreachable states and transitions

Browse source 
Based on a request from Pierre Ganty.

* spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
bin/common_aoutput.cc, bin/common_aoutput.hh: Implement those
options.
* tests/core/format.test: Add test case.
* doc/org/autfilt.org: Update doc.
* NEWS: Mention them.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-19 16:30:00 +02:00
parent 52ed3d1e8f
commit de29ba9e4c
7 changed files with 197 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -1,5 +1,12 @@
New in spot 2.11.1.dev (not yet released)
Command-line tools:
- The --stats specifications %s, %e, %t for printing the number of
(reachable) states, edges, and transitions, learned to support
options [r], [u], [a] to indicate if only reachable, unreachable,
or all elements should be counted.
Library:
- spot::reduce_parity() now has a "layered" option to force all

43
bin/common_aoutput.cc
View file

@ -203,12 +203,18 @@ static const argp_option io_options[] =
"to specify additional options as in --hoa=opt)", 0 },
{ "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"name of the automaton", 0 },
{ "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of reachable states", 0 },
{ "%E, %e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of reachable edges", 0 },
{ "%T, %t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of reachable transitions", 0 },
{ "%S, %s, %[LETTER]S, %[LETTER]s",
0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of states (add one LETTER to select (r) reachable [default], "
"(u) unreachable, (a) all).", 0 },
{ "%E, %e, %[LETTER]E, %[LETTER]e",
0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of edges (add one LETTER to select (r) reachable [default], "
"(u) unreachable, (a) all).", 0 },
{ "%T, %t, %[LETTER]E, %[LETTER]e",
0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of transitions (add one LETTER to select (r) reachable "
"[default], (u) unreachable, (a) all).", 0 },
{ "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance sets", 0 },
{ "%G, %g, %[LETTERS]G, %[LETTERS]g", 0, nullptr,
@ -268,12 +274,15 @@ static const argp_option o_options[] =
"to specify additional options as in --hoa=opt)", 0 },
{ "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"name of the automaton", 0 },
{ "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of reachable states", 0 },
{ "%e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of reachable edges", 0 },
{ "%t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of reachable transitions", 0 },
{ "%s, %[LETTER]s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of states (add one LETTER to select (r) reachable [default], "
"(u) unreachable, (a) all).", 0 },
{ "%e, %[LETTER]e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of edges (add one LETTER to select (r) reachable [default], "
"(u) unreachable, (a) all).", 0 },
{ "%t, %[LETTER]t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of transitions (add one LETTER to select (r) reachable "
"[default], (u) unreachable, (a) all).", 0 },
{ "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance sets", 0 },
{ "%g, %[LETTERS]g", 0, nullptr,
@ -472,15 +481,15 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
if (has('T'))
{
spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
haut_states_ = s.states;
haut_edges_ = s.edges;
haut_trans_ = s.transitions;
haut_states_.set(s.states, haut->aut->num_states());
haut_edges_.set(s.edges, haut->aut->num_edges());
haut_trans_.set(s.transitions, count_all_transitions(haut->aut));
}
else if (has('E') || has('S'))
{
spot::twa_statistics s = stats_reachable(haut->aut);
haut_states_ = s.states;
haut_edges_ = s.edges;
haut_states_.set(s.states, haut->aut->num_states());
haut_edges_.set(s.edges, haut->aut->num_edges());
}
if (has('M'))
{

6
bin/common_aoutput.hh
View file

@ -166,9 +166,9 @@ private:
spot::printable_value<std::string> aut_word_;
spot::printable_value<std::string> haut_word_;
spot::printable_acc_cond haut_gen_acc_;
spot::printable_value<unsigned> haut_states_;
spot::printable_value<unsigned> haut_edges_;
spot::printable_value<unsigned long long> haut_trans_;
spot::printable_size haut_states_;
spot::printable_size haut_edges_;
spot::printable_long_size haut_trans_;
spot::printable_value<unsigned> haut_acc_;
printable_varset haut_ap_;
printable_varset aut_ap_;

10
doc/org/autfilt.org
View file

@ -145,7 +145,8 @@ ltl2tgba --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 the formula, in Spot's syntax
%F name of the input file
%g, %[LETTERS]g acceptance condition (in HOA syntax); add brackets
@ -170,8 +171,11 @@ ltl2tgba --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

90
spot/twaalgos/stats.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011-2018, 2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2011-2018, 2020, 2022 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -33,6 +33,16 @@
namespace spot
{
unsigned long long
count_all_transitions(const const_twa_graph_ptr& g)
{
unsigned long long tr = 0;
bdd v = g->ap_vars();
for (auto& e: g->edges())
tr += bdd_satcountset(e.cond, v);
return tr;
}
namespace
{
class stats_bfs: public twa_reachable_iterator_breadth_first
@ -82,6 +92,7 @@ namespace spot
};
template<typename SU, typename EU>
void dfs(const const_twa_graph_ptr& ge, SU state_update, EU edge_update)
{
@ -344,10 +355,73 @@ namespace spot
<< std::string(beg, end + 2) << ", ";
tmp << e.what();
throw std::runtime_error(tmp.str());
}
}
void printable_size::print(std::ostream& os, const char* pos) const
{
char p = 'r';
if (*pos == '[')
{
p = pos[1];
if (pos[2] != ']' || !(p == 'r' || p == 'u' || p == 'a'))
{
const char* end = strchr(pos + 1, ']');
std::ostringstream tmp;
tmp << "while processing %"
<< std::string(pos, end + 2) << ", "
<< "only [a], [r], or [u] is supported.";
throw std::runtime_error(tmp.str());
}
}
switch (p)
{
case 'r':
os << reachable_;
return;
case 'a':
os << all_;
return;
case 'u':
os << all_ - reachable_;
return;
}
SPOT_UNREACHABLE();
return;
}
void printable_long_size::print(std::ostream& os, const char* pos) const
{
char p = 'r';
if (*pos == '[')
{
p = pos[1];
if (pos[2] != ']' || !(p == 'r' || p == 'u' || p == 'a'))
{
const char* end = strchr(pos + 1, ']');
std::ostringstream tmp;
tmp << "while processing %"
<< std::string(pos, end + 2) << ", "
<< "only [a], [r], or [u] is supported.";
throw std::runtime_error(tmp.str());
}
}
switch (p)
{
case 'r':
os << reachable_;
return;
case 'a':
os << all_;
return;
case 'u':
os << all_ - reachable_;
return;
}
SPOT_UNREACHABLE();
return;
}
stat_printer::stat_printer(std::ostream& os, const char* format)
: format_(format)
@ -376,15 +450,15 @@ namespace spot
if (has('t'))
{
twa_sub_statistics s = sub_stats_reachable(aut);
states_ = s.states;
edges_ = s.edges;
trans_ = s.transitions;
states_.set(s.states, aut->num_states());
edges_.set(s.edges, aut->num_edges());
trans_.set(s.transitions, count_all_transitions(aut));
}
else if (has('s') || has('e'))
{
twa_statistics s = stats_reachable(aut);
states_ = s.states;
edges_ = s.edges;
states_.set(s.states, aut->num_states());
edges_.set(s.edges, aut->num_edges());
}
if (has('a'))

43
spot/twaalgos/stats.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011-2017, 2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2011-2017, 2020, 2022 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -55,6 +55,9 @@ namespace spot
/// \brief Compute sub statistics for an automaton.
SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g);
/// \brief Count all transtitions, even unreachable ones.
SPOT_API unsigned long long
count_all_transitions(const const_twa_graph_ptr& g);
class SPOT_API printable_formula: public printable_value<formula>
{
@ -102,6 +105,36 @@ namespace spot
void print(std::ostream& os, const char* pos) const override;
};
class SPOT_API printable_size final:
public spot::printable
{
unsigned reachable_ = 0;
unsigned all_ = 0;
public:
void set(unsigned reachable, unsigned all)
{
reachable_ = reachable;
all_ = all;
}
void print(std::ostream& os, const char* pos) const override;
};
class SPOT_API printable_long_size final:
public spot::printable
{
unsigned long long reachable_ = 0;
unsigned long long all_ = 0;
public:
void set(unsigned long long reachable, unsigned long long all)
{
reachable_ = reachable;
all_ = all;
}
void print(std::ostream& os, const char* pos) const override;
};
/// \brief prints various statistics about a TGBA
///
/// This object can be configured to display various statistics
@ -123,9 +156,9 @@ namespace spot
const char* format_;
printable_formula form_;
printable_value<unsigned> states_;
printable_value<unsigned> edges_;
printable_value<unsigned long long> trans_;
printable_size states_;
printable_size edges_;
printable_long_size trans_;
printable_value<unsigned> acc_;
printable_scc_info scc_;
printable_value<unsigned> nondetstates_;

50
tests/core/format.test
View file

@ -1,7 +1,7 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2016, 2017, 2022 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -139,18 +139,36 @@ test 3,5 = `ltl2tgba --low --any --stats=%s,%e "$f"`
test 3,4 = `ltl2tgba --stats=%s,%e "$f"`
cat >foo <<EOF
HOA: v1
States: 3
Start: 0
AP: 0
Acceptance: 0 t
--BODY--
State: 0
[t] 1
State: 1
[t] 0
State: 2
[t] 2
--END--
HOA: v1 States: 7 Start: 5 AP: 1 "a" acc-name: Buchi
Acceptance: 1 Inf(0) properties: trans-labels explicit-labels
state-acc deterministic properties: terminal --BODY-- State: 0 [0] 6
State: 1 [t] 0 State: 2 [t] 1 State: 3 [f] 2 State: 4 [t] 3 State: 5
[t] 4 State: 6 {0} [t] 6 --END--
EOF
test 2,2 = `autfilt --stats=%S,%s foo`
(
autfilt --stats='%s,%[r]s,%[u]s,%[a]s' foo;
autfilt --remove-dead --stats='%s,%[r]s,%[u]s,%[a]s' foo;
autfilt --remove-dead --stats='%S,%[r]S,%[u]S,%[a]S' foo;
autfilt --stats='%e,%[r]e,%[u]e,%[a]e' foo;
autfilt --remove-dead --stats='%e,%[r]e,%[u]e,%[a]e' foo;
autfilt --remove-dead --stats='%E,%[r]E,%[u]E,%[a]E' foo;
autfilt --stats='%t,%[r]t,%[u]t,%[a]t' foo;
autfilt --remove-dead --stats='%t,%[r]t,%[u]t,%[a]t' foo;
autfilt --remove-dead --stats='%T,%[r]T,%[u]T,%[a]T' foo;
) > stats
cat >expected <<EOF
3,3,4,7
1,1,0,1
3,3,4,7
2,2,4,6
0,0,0,0
2,2,4,6
4,4,7,11
0,0,0,0
4,4,7,11
EOF
diff stats expected
autfilt --stats='%[x]T' foo 2>err && exit 1
grep 'only \[a\], \[r\], or \[u\] is supported' err