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

stats: speed up the computation of transitions

Juraj Major reported a case with 32 APs where ltlcross would take
forever to gather statistics.  It turns out that for each edge,
twa_sub_statistics was enumerating all compatible assignments of 32
APs.  This uses bdd_satcountset() instead, and also store the result
in a long long to avoid overflows.

* spot/twaalgos/stats.cc (twa_sub_statistics): Improve the code for
counting transitions.
* bin/common_aoutput.hh, bin/ltlcross.cc, spot/twaalgos/stats.hh:
Store transition counts are long long.
* tests/core/readsave.test: Add test case.
* NEWS: Mention the bug.
parent 4608d9a5
......@@ -21,6 +21,14 @@ New in spot 2.9.0.dev (not yet released)
spot::translator class when creating deterministic automata with
generic acceptance.
Bugs fixed:
- spot::twa_sub_statistics was very slow at computing the number of
transitons, and could overflow. It is now avoiding some costly
loop of BDD operations, and storing the result using at least 64
bits. This affects the output of "ltlcross --csv" and
"--stats=%t" for many tools.
New in spot 2.9 (2020-04-30)
Command-line tools:
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -167,7 +167,7 @@ private:
spot::printable_acc_cond haut_gen_acc_;
spot::printable_value<unsigned> haut_states_;
spot::printable_value<unsigned> haut_edges_;
spot::printable_value<unsigned> haut_trans_;
spot::printable_value<unsigned long long> haut_trans_;
spot::printable_value<unsigned> haut_acc_;
printable_varset haut_ap_;
printable_varset aut_ap_;
......
......@@ -296,7 +296,7 @@ struct statistics
double time;
unsigned states;
unsigned edges;
unsigned transitions;
unsigned long long transitions;
unsigned acc;
unsigned scc;
unsigned nonacc_scc;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011-2018 Laboratoire de Recherche et
// Copyright (C) 2008, 2011-2018, 2020 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
......@@ -64,7 +64,7 @@ namespace spot
{
public:
sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s)
: stats_bfs(a, s), s_(s), seen_(a->ap_vars())
: stats_bfs(a, s), s_(s), apvars_(a->ap_vars())
{
}
......@@ -73,17 +73,12 @@ namespace spot
const twa_succ_iterator* it) override
{
++s_.edges;
bdd cond = it->cond();
while (cond != bddfalse)
{
cond -= bdd_satoneset(cond, seen_, bddtrue);
++s_.transitions;
}
s_.transitions += bdd_satcountset(it->cond(), apvars_);
}
private:
twa_sub_statistics& s_;
bdd seen_;
bdd apvars_;
};
......@@ -180,11 +175,7 @@ namespace spot
[&s, &ge](bdd cond)
{
++s.edges;
while (cond != bddfalse)
{
cond -= bdd_satoneset(cond, ge->ap_vars(), bddtrue);
++s.transitions;
}
s.transitions += bdd_satcountset(cond, ge->ap_vars());
});
}
return s;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011-2017 Laboratoire de Recherche et
// Copyright (C) 2008, 2011-2017, 2020 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
......@@ -44,7 +44,7 @@ namespace spot
struct SPOT_API twa_sub_statistics: public twa_statistics
{
unsigned transitions;
unsigned long long transitions;
twa_sub_statistics() { transitions = 0; }
std::ostream& dump(std::ostream& out) const;
......@@ -125,7 +125,7 @@ namespace spot
printable_formula form_;
printable_value<unsigned> states_;
printable_value<unsigned> edges_;
printable_value<unsigned> trans_;
printable_value<unsigned long long> trans_;
printable_value<unsigned> acc_;
printable_scc_info scc_;
printable_value<unsigned> nondetstates_;
......
......@@ -1119,3 +1119,28 @@ f="{{!a;!b}:{{c <-> d} && {e xor f} && {m | {l && {k | {j <-> {i xor {g && h}"
f="$f}}}}} && {{n && o} | {!n && p}} && {q -> {r <-> s}}}:{[*0..1];t}}[]-> u"
ltl2tgba -f "$f" --dot=bar > out.dot
grep 'label too long' out.dot
# genltl --and-fg=32 | ltlfilt --relabel=abc | ltldo ltl3ba produces a
# few edges equivalent to a lot of transitions. The code used to
# count those transitions used to be very inefficient.
cat >andfg32.hoa <<EOF
HOA: v1
States: 2
Start: 0
AP: 32 "a" "ab" "b" "bb" "c" "cb" "d" "db" "e" "eb" "f" "fb" "g" "h"
"i" "j" "k" "l" "m" "n" "o" "p" "q" "r" "s" "t" "u" "v" "w" "x" "y" "z"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[t] 0
[0&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15&16&17
&18&19&20&21&22&23&24&25&26&27&28&29&30&31] 1
State: 1 {0}
[0&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15&16&17
&18&19&20&21&22&23&24&25&26&27&28&29&30&31] 1
--END--
EOF
test `autfilt andfg32.hoa --stats=%t` = 4294967298 # 2^32 + 2
Supports Markdown
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