diff --git a/NEWS b/NEWS index 834f17ea9..d2836f658 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 0f1103152..1b2e7ae41 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,6 +1,6 @@ // -*- 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 haut_states_; spot::printable_value haut_edges_; - spot::printable_value haut_trans_; + spot::printable_value haut_trans_; spot::printable_value haut_acc_; printable_varset haut_ap_; printable_varset aut_ap_; diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index d588217d7..a7f9fa1da 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -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; diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index 2d0a7a849..ddccba5db 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -1,5 +1,5 @@ // -*- 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; diff --git a/spot/twaalgos/stats.hh b/spot/twaalgos/stats.hh index 6f8655134..1caa8324b 100644 --- a/spot/twaalgos/stats.hh +++ b/spot/twaalgos/stats.hh @@ -1,5 +1,5 @@ // -*- 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 states_; printable_value edges_; - printable_value trans_; + printable_value trans_; printable_value acc_; printable_scc_info scc_; printable_value nondetstates_; diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 010398468..2f9b424f9 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -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 <