diff --git a/NEWS b/NEWS index 503f638ab..0c96871fc 100644 --- a/NEWS +++ b/NEWS @@ -201,6 +201,12 @@ New in spot 2.5.3.dev (not yet released) looking for differences. See also https://spot.lrde.epita.fr/ipynb/contains.html + - spot::complement_semidet(aut) is a new function that returns the + complement of aut, where aut is a semideterministic automaton. The + function uses the NCSB complementation algorithm proposed by + F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and MH. Tsai + (TACAS'16). + - spot::remove_alternation() was slightly improved on very-weak alternating automata: the labeling of the outgoing transitions in the resulting TGBA makes it more likely that simulation-based diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 446052b44..d90fe90ec 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -18,10 +18,12 @@ // along with this program. If not, see . #include "config.h" +#include +#include #include #include #include - +#include namespace spot { @@ -34,4 +36,488 @@ namespace spot return dualize(aut); } + + namespace + { + enum ncsb + { + ncsb_n = 0, // non deterministic + ncsb_c = 2, // needs check + ncsb_cb = 3, // needs check AND in breakpoint + ncsb_s = 4, // safe + ncsb_m = 1, // missing + }; + + typedef std::vector mstate; + typedef std::vector> small_mstate; + + struct small_mstate_hash + { + size_t + operator()(small_mstate s) const noexcept + { + size_t hash = 0; + for (const auto& p: s) + { + hash = wang32_hash(hash ^ ((p.first<<2) | p.second)); + } + return hash; + } + }; + + class ncsb_complementation + { + private: + // The source automaton. + const const_twa_graph_ptr aut_; + + // SCCs information of the source automaton. + scc_info si_; + + // Number of states in the input automaton. + unsigned nb_states_; + + // The complement being built. + twa_graph_ptr res_; + + // Association between NCSB states and state numbers of the + // complement. + std::unordered_map ncsb2n_; + + // States to process. + std::deque> todo_; + + // Support for each state of the source automaton. + std::vector support_; + + // Propositions compatible with all transitions of a state. + std::vector compat_; + + // Whether a SCC is deterministic or not + std::vector is_deter_; + + // Whether a state only has accepting transitions + std::vector is_accepting_; + + // State names for graphviz display + std::vector* names_; + + // Show NCSB states in state name to help debug + bool show_names_; + + std::string + get_name(const small_mstate& ms) + { + std::string res = "{"; + + bool first_state = true; + for (const auto& p: ms) + if (p.second == ncsb_n) + { + if (!first_state) + res += ","; + first_state = false; + res += std::to_string(p.first); + } + + res += "},{"; + + first_state = true; + for (const auto& p: ms) + if (p.second & ncsb_c) + { + if (!first_state) + res += ","; + first_state = false; + res += std::to_string(p.first); + } + + res += "},{"; + + first_state = true; + for (const auto& p: ms) + if (p.second == ncsb_s) + { + if (!first_state) + res += ","; + first_state = false; + res += std::to_string(p.first); + } + + res += "},{"; + + first_state = true; + for (const auto& p: ms) + if (p.second == ncsb_cb) + { + if (!first_state) + res += ","; + first_state = false; + res += std::to_string(p.first); + } + + return res + "}"; + } + + small_mstate + to_small_mstate(const mstate& ms) + { + unsigned count = 0; + for (unsigned i = 0; i < nb_states_; ++i) + count+= (ms[i] != ncsb_m); + small_mstate small; + small.reserve(count); + for (unsigned i = 0; i < nb_states_; ++i) + if (ms[i] != ncsb_m) + small.emplace_back(i, ms[i]); + return small; + } + + // From a NCSB state, looks for a duplicate in the map before + // creating a new state if needed. + unsigned + new_state(mstate&& s) + { + auto p = ncsb2n_.emplace(to_small_mstate(s), 0); + if (p.second) // This is a new state + { + p.first->second = res_->new_state(); + if (show_names_) + names_->push_back(get_name(p.first->first)); + todo_.emplace_back(std::move(s), p.first->second); + } + return p.first->second; + } + + void + ncsb_successors(mstate&& ms, unsigned origin, bdd letter) + { + std::vector succs; + succs.emplace_back(nb_states_, ncsb_m); + + // Handle S states. + // + // Treated first because we can escape early if the letter + // leads to an accepting transition for a Safe state. + for (unsigned i = 0; i < nb_states_; ++i) + { + if (ms[i] != ncsb_s) + continue; + + for (const auto& t: aut_->out(i)) + { + if (!bdd_implies(letter, t.cond)) + continue; + if (t.acc || is_accepting_[t.dst]) + // Exit early; transition is forbidden for safe + // state. + return; + + succs[0][t.dst] = ncsb_s; + + // No need to look for other compatible transitions + // for this state; it's in the deterministic part of + // the automaton + break; + } + } + + // Handle C states. + for (unsigned i = 0; i < nb_states_; ++i) + { + if (!(ms[i] & ncsb_c)) + continue; + + bool has_succ = false; + for (const auto& t: aut_->out(i)) + { + if (!bdd_implies(letter, t.cond)) + continue; + + has_succ = true; + + // state can become safe, if transition is accepting + // and destination isn't an accepting state + if (t.acc) + { + // double all the current possible states + unsigned length = succs.size(); + for (unsigned j = 0; j < length; ++j) + { + if (succs[j][t.dst] == ncsb_m) + { + if (!is_accepting_[t.dst]) + { + succs.push_back(succs[j]); + succs.back()[t.dst] = ncsb_s; + } + succs[j][t.dst] = ncsb_c; + } + } + } + else // state stays in check + { + auto it = succs.begin(); + while (it != succs.end()) + { + // remove state if it should stay in s + if ((*it)[t.dst] == ncsb_s) + { + std::iter_swap(it, succs.end() - 1); + succs.pop_back(); + continue; + } + (*it)[t.dst] = ncsb_c; + ++it; + } + } + // No need to look for other compatible transitions + // for this state; it's in the deterministic part of + // the automaton + break; + } + if (!has_succ && !is_accepting_[i]) + return; + } + + // Handle N states. + for (unsigned i = 0; i < nb_states_; ++i) + { + if (ms[i] != ncsb_n) + continue; + for (const auto& t: aut_->out(i)) + { + if (!bdd_implies(letter, t.cond)) + continue; + + if (is_deter_[si_.scc_of(t.dst)]) + { + // double all the current possible states + unsigned length = succs.size(); + for (unsigned j = 0; j < length; ++j) + { + if (succs[j][t.dst] == ncsb_m) + { + // Can become safe if the destination is + // not an accepting state. + if (!is_accepting_[t.dst]) + { + succs.push_back(succs[j]); + succs.back()[t.dst] = ncsb_s; + } + succs[j][t.dst] = ncsb_c; + } + } + } + else + { + auto it = succs.begin(); + while (it != succs.end()) + { + // remove state if it should stay in s or c + if ((*it)[t.dst] == ncsb_s + || (*it)[t.dst] == ncsb_c) + { + std::iter_swap(it, succs.end() - 1); + succs.pop_back(); + continue; + } + (*it)[t.dst] = ncsb_n; + ++it; + } + } + } + } + + // Revisit B states to see if they still exist in successors. + // This is done at the end because we need to know all of the + // states present in C before this stage + bool b_empty = true; + for (unsigned i = 0; i < nb_states_; ++i) + { + if (ms[i] != ncsb_cb) + continue; + + // The original B set wasn't empty + b_empty = false; + + for (const auto& t: aut_->out(i)) + { + if (!bdd_implies(letter, t.cond)) + continue; + + for (auto& succ: succs) + { + if (succ[t.dst] == ncsb_c) + succ[t.dst] = ncsb_cb; + } + + // No need to look for other compatible transitions + // for this state; it's in the deterministic part of + // the automaton + break; + } + } + + // If B was empty, then set every c_not_b to cb in successors + if (b_empty) + for (auto& succ: succs) + for (unsigned i = 0; i < succ.size(); ++i) + if (succ[i] == ncsb_c) + succ[i] = ncsb_cb; + + // create the automaton states + for (auto& succ: succs) + { + bool b_empty = true; + for (const auto& state: succ) + if (state == ncsb_cb) + { + b_empty = false; + break; + } + if (b_empty) // becomes accepting + { + for (unsigned i = 0; i < succ.size(); ++i) + if (succ[i] == ncsb_c) + succ[i] = ncsb_cb; + unsigned dst = new_state(std::move(succ)); + res_->new_edge(origin, dst, letter, {0}); + } + else + { + unsigned dst = new_state(std::move(succ)); + res_->new_edge(origin, dst, letter); + } + } + } + + public: + ncsb_complementation(const const_twa_graph_ptr& aut, bool show_names) + : aut_(aut), + si_(aut), + nb_states_(aut->num_states()), + support_(nb_states_), + compat_(nb_states_), + is_accepting_(nb_states_), + show_names_(show_names) + { + res_ = make_twa_graph(aut->get_dict()); + res_->copy_ap_of(aut); + res_->set_buchi(); + + // Generate bdd supports and compatible options for each state. + // Also check if all its transitions are accepting. + for (unsigned i = 0; i < nb_states_; ++i) + { + bdd res_support = bddtrue; + bdd res_compat = bddfalse; + bool accepting = true; + bool has_transitions = false; + for (const auto& out: aut->out(i)) + { + has_transitions = true; + res_support &= bdd_support(out.cond); + res_compat |= out.cond; + if (!out.acc) + accepting = false; + } + support_[i] = res_support; + compat_[i] = res_compat; + is_accepting_[i] = accepting && has_transitions; + } + + + + // Compute which SCCs are part of the deterministic set. + is_deter_ = semidet_sccs(si_); + + if (show_names_) + { + names_ = new std::vector(); + res_->set_named_prop("state-names", names_); + } + + // Because we only handle one initial state, we assume it + // belongs to the N set. (otherwise the automaton would be + // deterministic) + unsigned init_state = aut->get_init_state_number(); + mstate new_init_state(nb_states_, ncsb_m); + new_init_state[init_state] = ncsb_n; + res_->set_init_state(new_state(std::move(new_init_state))); + } + + twa_graph_ptr + run() + { + // Main stuff happens here + + while (!todo_.empty()) + { + auto top = todo_.front(); + todo_.pop_front(); + + mstate ms = top.first; + + // Compute support of all available states. + bdd msupport = bddtrue; + bdd n_s_compat = bddfalse; + bdd c_compat = bddtrue; + bool c_empty = true; + for (unsigned i = 0; i < nb_states_; ++i) + if (ms[i] != ncsb_m) + { + msupport &= support_[i]; + if (ms[i] == ncsb_n || ms[i] == ncsb_s || is_accepting_[i]) + n_s_compat |= compat_[i]; + else + { + c_empty = false; + c_compat &= compat_[i]; + } + } + + bdd all; + if (!c_empty) + all = c_compat; + else + { + all = n_s_compat; + if (all != bddtrue) + { + mstate empty_state(nb_states_, ncsb_m); + res_->new_edge(top.second, + new_state(std::move(empty_state)), + !all, + {0}); + } + } + while (all != bddfalse) + { + bdd one = bdd_satoneset(all, msupport, bddfalse); + all -= one; + + // Compute all new states available from the generated + // letter. + ncsb_successors(std::move(ms), top.second, one); + } + } + + res_->merge_edges(); + return res_; + } + }; + + } + + twa_graph_ptr + complement_semidet(const const_twa_graph_ptr& aut, bool show_names) + { + if (!is_semi_deterministic(aut)) + throw std::runtime_error + ("complement_semidet() requires a semi-deterministic input"); + + auto ncsb = ncsb_complementation(aut, show_names); + return ncsb.run(); + } } diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 0b64b43fa..55f7da10c 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -43,4 +43,13 @@ namespace spot SPOT_DEPRECATED("use spot::dualize() instead") SPOT_API twa_graph_ptr dtwa_complement(const const_twa_graph_ptr& aut); + + /// \brief Complement a semideterministic TωA + /// + /// The automaton \a aut should be semideterministic. + /// + /// Uses the NCSB algorithm described by F. Blahoudek, M. Heizmann, + /// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). + SPOT_API twa_graph_ptr + complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false); } diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 51a43661c..37d8ee0dd 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -138,6 +138,24 @@ namespace spot aut->prop_universal(universal); } + void highlight_semidet_sccs(scc_info& si, unsigned color) + { + auto det_sccs = semidet_sccs(si); + if (det_sccs.empty()) + return; + auto aut = si.get_aut(); + auto* highlight = std::const_pointer_cast(aut) + ->get_or_set_named_prop>("highlight-states"); + for (unsigned scc = 0; scc < si.scc_count(); scc++) + { + if (det_sccs[scc]) + { + for (auto& t : si.states_of(scc)) + (*highlight)[t] = color; + } + } + } + bool is_complete(const const_twa_graph_ptr& aut) { @@ -238,6 +256,49 @@ namespace spot } } + std::vector semidet_sccs(scc_info& si) + { + const_twa_graph_ptr aut = si.get_aut(); + trival sd = aut->prop_semi_deterministic(); + if (sd.is_known() && sd.is_false()) + return std::vector(); + si.determine_unknown_acceptance(); + unsigned nscc = si.scc_count(); + assert(nscc); + std::vector reachable_from_acc(nscc); + std::vector res(nscc); + bool semi_det = true; + do // iterator of SCCs in reverse topological order + { + --nscc; + if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc]) + { + for (unsigned succ: si.succ(nscc)) + reachable_from_acc[succ] = true; + for (unsigned src: si.states_of(nscc)) + { + bdd available = bddtrue; + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + { + semi_det = false; + goto done; + } + else + { + available -= t.cond; + } + } + res[nscc] = true; + } + } + while (nscc); + done: + if (!semi_det) + return std::vector(); + return res; + } + bool is_semi_deterministic(const const_twa_graph_ptr& aut) { diff --git a/spot/twaalgos/isdet.hh b/spot/twaalgos/isdet.hh index 1f750bdfb..92161a19e 100644 --- a/spot/twaalgos/isdet.hh +++ b/spot/twaalgos/isdet.hh @@ -19,6 +19,7 @@ #pragma once +#include #include namespace spot @@ -77,6 +78,16 @@ namespace spot highlight_nondet_edges(twa_graph_ptr& aut, unsigned color); /// @} + /// \brief Highlight the deterministic part of the automaton + /// + /// In the case of a semideterministic automaton, highlights the + /// states reachable from any accepting SCC. + /// + /// \param aut the automaton to process + /// \param color the color to give to states reachable from accepting SCCs. + SPOT_API void + highlight_semidet_sccs(scc_info& si, unsigned color); + /// \brief Return true iff \a aut is complete. /// /// An automaton is complete if its translation relation is total, @@ -91,6 +102,10 @@ namespace spot SPOT_API bool is_semi_deterministic(const const_twa_graph_ptr& aut); + /// \brief Whether an SCC is in the deterministic part of an automaton + SPOT_API std::vector + semidet_sccs(scc_info& si); + /// \brief Set the deterministic and semi-deterministic properties /// appropriately. SPOT_API void check_determinism(twa_graph_ptr aut); diff --git a/tests/Makefile.am b/tests/Makefile.am index 8d9a67fd1..6e2a48ff3 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -366,6 +366,7 @@ TESTS_python = \ python/bdditer.py \ python/bddnqueen.py \ python/bugdet.py \ + python/complement_semidet.py \ python/declenv.py \ python/_word.ipynb \ python/decompose_scc.py \ diff --git a/tests/python/complement_semidet.py b/tests/python/complement_semidet.py new file mode 100644 index 000000000..5ab4557bc --- /dev/null +++ b/tests/python/complement_semidet.py @@ -0,0 +1,38 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2018 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 . + +import spot +import buddy + + +def complement(aut): + return spot.dualize(aut.postprocess('det', 'gen')) + + +n = 10000 + +for aut in spot.automata( + "randltl -n-1 a b " + "| ltl2tgba " + "| autfilt --is-semi-deterministic --acceptance-is=Buchi -n{} |" + .format(n)): + + comp = complement(aut) + semidet_comp = spot.complement_semidet(aut, True) + assert(comp.equivalent_to(semidet_comp))