From 48edfd80c29955097358793993abce7d6a3e770d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Dec 2020 17:55:50 +0100 Subject: [PATCH] powerset: deal with accepting sinks more effectively Part of #444. * spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh: Implement accepting sink handling. * spot/twaalgos/minimize.cc (minimize_wdba): Pass sinks to tgba_powerset. * spot/misc/bitvect.hh: Add an interesects method. * tests/core/ltl2tgba2.test: More tests. * NEWS: Mention this new feature. --- NEWS | 4 ++++ spot/misc/bitvect.hh | 12 +++++++++++- spot/twaalgos/minimize.cc | 20 +++++++++++++++++++- spot/twaalgos/powerset.cc | 27 ++++++++++++++++++++++++--- spot/twaalgos/powerset.hh | 11 +++++++++-- tests/core/ltl2tgba2.test | 9 ++++++++- 6 files changed, 75 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 19c4701bd..42b2cf712 100644 --- a/NEWS +++ b/NEWS @@ -141,6 +141,10 @@ New in spot 2.9.5.dev (not yet released) automata-based implication checks for formula simplifications. Defaults to 64. + - tgba_powerset() now takes an extra optional argument to specify a + list of accepting sinks states if some are known. Doing so can + cut the size of the powerset automaton by 2^|sinks| in favorable + cases. Python: diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh index 330f6045f..7c54658a5 100644 --- a/spot/misc/bitvect.hh +++ b/spot/misc/bitvect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -255,6 +255,16 @@ namespace spot return *this; } + bool intersects(const bitvect& other) + { + SPOT_ASSERT(other.size_ <= size_); + unsigned m = std::min(other.block_count_, block_count_); + for (size_t i = 0; i < m; ++i) + if (storage_[i] & other.storage_[i]) + return true; + return false; + } + bitvect& operator^=(const bitvect& other) { SPOT_ASSERT(other.size_ <= size_); diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index be603c7f1..bbae0ad0c 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -393,7 +393,25 @@ namespace spot } else { - det_a = tgba_powerset(a, aborter); + // Find any accepting sink state, to speed up the + // determinization by merging all states containing a sink + // state. + // + // We only as consider as "accepting sink" any state + // that have an accepting self-loop labeled by true. + std::vector acc_sinks; + unsigned ns = a->num_states(); + for (unsigned n = 0; n < ns; ++n) + { + for (auto& e: a->out(n)) + if (e.dst == n && e.cond == bddtrue + && a->acc().accepting(e.acc)) + { + acc_sinks.push_back(n); + break; + } + } + det_a = tgba_powerset(a, aborter, &acc_sinks); if (!det_a) return nullptr; } diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index 04c334b4d..5093d885a 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -82,7 +82,8 @@ namespace spot twa_graph_ptr tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge, - const output_aborter* aborter) + const output_aborter* aborter, + std::vector* accepting_sinks) { unsigned ns = aut->num_states(); unsigned nap = aut->ap().size(); @@ -207,6 +208,23 @@ namespace spot auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); + bitvect* acc_sinks = nullptr; + if (accepting_sinks) + { + acc_sinks = make_bitvect(ns); + for (unsigned s: *accepting_sinks) + acc_sinks->set(s); + toclean.emplace_back(acc_sinks); + + // The accepting sink is the first registered state by + // convention. + power_state ps = bv_to_ps(acc_sinks); + unsigned num = res->new_state(); + seen[acc_sinks] = num; + assert(pm.map_.size() == num); + pm.map_.emplace_back(std::move(ps)); + } + { unsigned init_num = aut->get_init_state_number(); auto bvi = make_bitvect(ns); @@ -239,6 +257,8 @@ namespace spot auto dst = &om->at(c); if (dst->is_fully_clear()) continue; + if (acc_sinks && dst->intersects(*acc_sinks)) + *dst = *acc_sinks; auto i = seen.find(dst); unsigned dst_num; if (i != seen.end()) @@ -274,10 +294,11 @@ namespace spot twa_graph_ptr tgba_powerset(const const_twa_graph_ptr& aut, - const output_aborter* aborter) + const output_aborter* aborter, + std::vector* accepting_sinks) { power_map pm; - return tgba_powerset(aut, pm, true, aborter); + return tgba_powerset(aut, pm, true, aborter, accepting_sinks); } diff --git a/spot/twaalgos/powerset.hh b/spot/twaalgos/powerset.hh index a0d41eeb7..00f3efc51 100644 --- a/spot/twaalgos/powerset.hh +++ b/spot/twaalgos/powerset.hh @@ -94,14 +94,21 @@ namespace spot /// /// If ab \a aborter is given, abort the construction whenever it /// would build an automaton that is too large, and return nullptr. + /// + /// If a vector of accepting sinks is given, all power-state that + /// contains any accepting sink will be merged into a single state + /// with number 0. + /// //@{ SPOT_API twa_graph_ptr tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge = true, - const output_aborter* aborter = nullptr); + const output_aborter* aborter = nullptr, + std::vector* accepting_sinks = nullptr); SPOT_API twa_graph_ptr tgba_powerset(const const_twa_graph_ptr& aut, - const output_aborter* aborter = nullptr); + const output_aborter* aborter = nullptr, + std::vector* accepting_sinks = nullptr); //@} diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index c8f53c53c..3c087de35 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -477,4 +477,11 @@ test 28 = `ltl2tgba -D -G -S --stats=%s "$f"` # Issue #443. This used to be too long. f='(!(G({(a)} |=> {(b)[*32]})))' -test 34 = `ltl2tgba -B --stats=%s "$f"` +test 34,0 = `ltl2tgba -B --stats=%s,%d "$f"` +# Issue #444. Because WDBA-minimization disables itself for large +# automata, the output is only deterministic up to a certain point, +# and the goal is to raise that point. +f='(!(G({(a)} |=> {(b)[*9]})))' +test 11,1 = `ltl2tgba -B --stats=%s,%d "$f"` +f='(!(G({(a)} |=> {(b)[*10]})))' +test 12,0 = `ltl2tgba -B --stats=%s,%d "$f"`