From bf7ccfe7e6ed3df245667df5b8712180a13dc739 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Dec 2019 17:09:55 +0100 Subject: [PATCH] new partial_degeneralize() algorithm * spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it. * tests/python/pdegen.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the new function. --- NEWS | 4 + spot/twaalgos/degen.cc | 287 +++++++++++++++++++++++++++++++++++------ spot/twaalgos/degen.hh | 27 +++- tests/Makefile.am | 1 + tests/python/pdegen.py | 98 ++++++++++++++ 5 files changed, 372 insertions(+), 45 deletions(-) create mode 100644 tests/python/pdegen.py diff --git a/NEWS b/NEWS index 39e22b6ea..f46ba9e62 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,10 @@ New in spot 2.8.4.dev (not yet released) parity_min_odd(n) = parity_min(true, n) parity_min_even(n) = parity_min(false, n) + - partial_degeneralize() is a new function performing partial + degeneralization to get rid of conjunction of Inf terms in + acceptance conditions. + New in spot 2.8.4 (2019-12-08) Bugs fixed: diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 397ec33da..0c9951e65 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche +// Copyright (C) 2012-2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -237,6 +237,62 @@ namespace spot } }; + + namespace + { + static void + keep_bottommost_copies(twa_graph_ptr& res, + scc_info& si_orig, + std::vector* orig_states) + { + unsigned res_ns = res->num_states(); + auto a = si_orig.get_aut(); + if (res_ns <= a->num_states()) + return; + + scc_info si_res(res, scc_info_options::TRACK_STATES); + unsigned res_scc_count = si_res.scc_count(); + if (res_scc_count <= si_orig.scc_count()) + return; + + // If we reach this place, we have more SCCs in the output than + // in the input. This means that we have created some redundant + // SCCs. Often, these are trivial SCCs created in front of + // their larger sisters, because we did not pick the correct + // level when entering the SCC for the first time, and the level + // we picked has not been seen again when exploring the SCC. + // But it could also be the case that by entering the SCC in two + // different ways, we create two clones of the SCC (I haven't + // encountered any such case, but I do not want to rule it out + // in the code below). + // + // Now we will iterate over the SCCs in topological order to + // remember the "bottommost" SCCs that contain each original + // state. If an original state is duplicated in a higher SCC, + // it can be shunted away. Amen. + std::vector + bottommost_occurence(a->num_states()); + { + unsigned n = res_scc_count; + do + for (unsigned s: si_res.states_of(--n)) + bottommost_occurence[(*orig_states)[s]] = s; + while (n); + } + std::vector retarget(res_ns); + for (unsigned n = 0; n < res_ns; ++n) + { + unsigned other = bottommost_occurence[(*orig_states)[n]]; + retarget[n] = + (si_res.scc_of(n) != si_res.scc_of(other)) ? other : n; + } + for (auto& e: res->edges()) + e.dst = retarget[e.dst]; + res->set_init_state(retarget[res->get_init_state_number()]); + res->purge_unreachable_states(); + } + } + template twa_graph_ptr degeneralize_aux(const const_twa_graph_ptr& a, bool use_z_lvl, @@ -617,48 +673,8 @@ namespace spot orders.print(); #endif res->merge_edges(); - - unsigned res_ns = res->num_states(); - if (!remove_extra_scc || res_ns <= a->num_states()) - return res; - - scc_info si_res(res, scc_info_options::TRACK_STATES); - unsigned res_scc_count = si_res.scc_count(); - if (res_scc_count <= m->scc_count()) - return res; - - // If we reach this place, we have more SCCs in the output than - // in the input. This means that we have created some redundant - // SCCs. Often, these are trivial SCCs created in front of - // their larger sisters, because we did not pick the correct - // level when entering the SCC for the first time, and the level - // we picked has not been seen again when exploring the SCC. - // But it could also be the case that by entering the SCC in two - // different ways, we create two clones of the SCC (I haven't - // encountered any such case, but I do not want to rule it out - // in the code below). - // - // Now we will iterate over the SCCs in topological order to - // remember the "bottomost" SCCs that contain each original - // state. If an original state is duplicated in a higher SCC, - // it can be shunted away. Amen. - std::vector bottomost_occurence(a->num_states()); - { - unsigned n = res_scc_count; - do - for (unsigned s: si_res.states_of(--n)) - bottomost_occurence[(*orig_states)[s]] = s; - while (n); - } - std::vector retarget(res_ns); - for (unsigned n = 0; n < res_ns; ++n) - { - unsigned other = bottomost_occurence[(*orig_states)[n]]; - retarget[n] = (si_res.scc_of(n) != si_res.scc_of(other)) ? other : n; - } - for (auto& e: res->edges()) - e.dst = retarget[e.dst]; - res->purge_unreachable_states(); + if (remove_extra_scc) + keep_bottommost_copies(res, *(m.get()), orig_states); return res; } } @@ -694,4 +710,189 @@ namespace spot use_lvl_cache, skip_levels, ignaccsl, remove_extra_scc); } + + namespace + { + static acc_cond::mark_t + to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen) + { + if (code.empty()) + return todegen; + + acc_cond::mark_t tostrip = todegen; + unsigned pos = code.size(); + do + { + switch (code[pos - 1].sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + pos -= 2; + if (code[pos].mark != todegen) + tostrip -= code[pos].mark; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + pos -= 2; + tostrip -= code[pos].mark; + break; + } + } + while (pos > 0); + return tostrip; + } + + static void + update_acc_for_partial_degen(acc_cond::acc_code& code, + acc_cond::mark_t todegen, + acc_cond::mark_t tostrip, + acc_cond::mark_t accmark) + { + if (!todegen) + { + code &= acc_cond::acc_code::inf(accmark); + return; + } + + if (code.empty()) + return; + + unsigned pos = code.size(); + do + { + switch (code[pos - 1].sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + pos -= 2; + if (code[pos].mark == todegen) + code[pos].mark = accmark; + else + code[pos].mark = code[pos].mark.strip(tostrip); + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + pos -= 2; + code[pos].mark = code[pos].mark.strip(tostrip); + break; + } + } + while (pos > 0); + } + + + + } + + + twa_graph_ptr + partial_degeneralize(const const_twa_graph_ptr& a, + acc_cond::mark_t todegen) + { + auto res = make_twa_graph(a->get_dict()); + res->copy_ap_of(a); + acc_cond::acc_code acc = a->get_acceptance(); + + acc_cond::mark_t tostrip = to_strip(acc, todegen); + acc_cond::mark_t keep = a->acc().all_sets() - tostrip; + acc_cond::mark_t degenmark = {keep.count()}; + + update_acc_for_partial_degen(acc, todegen, tostrip, degenmark); + res->set_acceptance(acc); + + std::vector order; + for (unsigned set: todegen.sets()) + order.push_back(set); + + //auto* names = new std::vector; + //res->set_named_prop("state-names", names); + auto orig_states = new std::vector(); + auto levels = new std::vector(); + orig_states->reserve(a->num_states()); // likely more are needed. + levels->reserve(a->num_states()); + res->set_named_prop("original-states", orig_states); + res->set_named_prop("degen-levels", levels); + + scc_info si_orig(a, scc_info_options::NONE); + + // degen_states -> new state numbers + ds2num_map ds2num; + + queue_t todo; + + auto new_state = [&](degen_state ds) + { + auto di = ds2num.find(ds); + if (di != ds2num.end()) + return di->second; + + unsigned ns = res->new_state(); + ds2num[ds] = ns; + todo.emplace_back(ds); + + //std::ostringstream os; + //os << ds.first << ',' << ds.second; + //names->push_back(os.str()); + assert(ns == orig_states->size()); + orig_states->emplace_back(ds.first); + levels->emplace_back(ds.second); + return ns; + }; + degen_state s(a->get_init_state_number(), 0); + new_state(s); + + while (!todo.empty()) + { + s = todo.front(); + todo.pop_front(); + + int src = ds2num[s]; + unsigned slevel = s.second; + unsigned orig_src = s.first; + unsigned scc_src = si_orig.scc_of(orig_src); + for (auto& e: a->out(orig_src)) + { + unsigned nextlvl = slevel; + acc_cond::mark_t accepting = {}; + if (si_orig.scc_of(e.dst) == scc_src) + { + while (nextlvl < order.size() && e.acc.has(order[nextlvl])) + ++nextlvl; + + if (nextlvl == order.size()) + { + accepting = degenmark; + nextlvl = 0; + + if ((e.acc & todegen) != todegen) + while (nextlvl < order.size() + && e.acc.has(order[nextlvl])) + ++nextlvl; + } + accepting |= e.acc.strip(tostrip); + } + else + { + nextlvl = 0; + } + + degen_state ds_dst(e.dst, nextlvl); + unsigned dst = new_state(ds_dst); + res->new_edge(src, dst, e.cond, accepting); + } + } + + res->merge_edges(); + keep_bottommost_copies(res, si_orig, orig_states); + return res; + } + } diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 6063bf4b7..7caa4ee21 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2015, 2017, 2018 Laboratoire de +// Copyright (C) 2012-2015, 2017-2019 Laboratoire de // Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -27,7 +27,7 @@ namespace spot /// \brief Degeneralize a spot::tgba into an equivalent sba with /// only one acceptance condition. /// - /// This algorithms will build a new explicit automaton that has + /// This algorithm will build a new explicit automaton that has /// at most (N+1) times the number of states of the original automaton. /// /// When \a use_z_lvl is set, the level of the degeneralized @@ -78,4 +78,27 @@ namespace spot bool ignaccsl = false, bool remove_extra_scc = true); /// \@} + + /// \ingroup twa_acc_transform + /// \brief Partial degeneralization of a TwA + /// + /// Given an automaton whose acceptance contains a conjunction of + /// Inf terms, perform a partial degeneralization to replace this + /// conjunction by a single Inf term. + /// + /// For instance if the input has acceptance + /// (Fin(0)&Inf(1)&Inf(3))|Fin(2) + /// calling partial_degeneralize with \a todegen set to `{1,3}` + /// will build an equivalent automaton with acceptance + /// (Fin(0)&Inf(2))|Fin(1) + /// + /// where Inf(2) tracks the acceptance of the original + /// Inf(1)&Inf(3), and Fin(1) tracks the acceptance of the original + /// Fin(2). + /// + /// Cases where the sets listed in \a todegen also occur outside + /// of the Inf-conjunction are also supported. + SPOT_API twa_graph_ptr + partial_degeneralize(const const_twa_graph_ptr& a, + acc_cond::mark_t todegen); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 309a28b58..84113c3eb 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -393,6 +393,7 @@ TESTS_python = \ python/otfcrash.py \ python/parsetgba.py \ python/parity.py \ + python/pdegen.py \ python/prodexpt.py \ python/_product_weak.ipynb \ python/_product_susp.ipynb \ diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py new file mode 100644 index 000000000..02f7ed0c8 --- /dev/null +++ b/tests/python/pdegen.py @@ -0,0 +1,98 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2019 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# Test that the spot.gen package works, in particular, we want +# to make sure that the objects created from spot.gen methods +# are usable with methods from the spot package. + + +import spot + +a, b, d = spot.automata(""" +HOA: v1 +States: 2 +Start: 0 +AP: 1 "p0" +Acceptance: 3 Inf(0)&Inf(1)|Fin(2) +--BODY-- +State: 0 +[0] 1 {1 2} +State: 1 +[0] 0 {0} +--END-- +HOA: v1 +States: 3 +Start: 2 +AP: 1 "p0" +Acceptance: 3 Inf(0)&Inf(1)|Fin(2) +--BODY-- +State: 0 +[0] 1 {1 2} +State: 1 +[0] 0 {0} +State: 2 +[0] 0 {0} +[0] 0 {1} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 1 "p0" +Acceptance: 1 Fin(0) +--BODY-- +State: 0 +[0] 0 {0} +--END-- +""") + +da = spot.partial_degeneralize(a, [0, 1]) +assert da.equivalent_to(a) +assert da.num_states() == 2 + +db = spot.partial_degeneralize(b, [0, 1]) +assert db.equivalent_to(b) +assert db.num_states() == 3 + +db.copy_state_names_from(b) +dbhoa = db.to_str('hoa') +assert dbhoa == """HOA: v1 +States: 3 +Start: 0 +AP: 1 "p0" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 "2#0" +[0] 2 +State: 1 "1#0" +[0] 2 +State: 2 "0#1" {0 1} +[0] 1 +--END--""" + +c = spot.automaton("randaut -A'(Fin(0)&Inf(1)&Inf(2))|Fin(2)' 1 |") +dc = spot.partial_degeneralize(c, [1, 2]) +assert dc.equivalent_to(c) +assert str(dc.get_acceptance()) == '(Fin(0) & Inf(2)) | Fin(1)' + +dd = spot.partial_degeneralize(d, []) +assert dd.equivalent_to(d) +assert dd.num_states() == 1 +assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)'