diff --git a/python/spot/impl.i b/python/spot/impl.i index d723a70f12b0827969b4cec3b5b31dc0483793a7..11dd17120f1d2f0d56ae585fd83fb49b4107b0c5 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -113,6 +113,7 @@ #include #include +#include #include #include #include @@ -507,6 +508,7 @@ def state_is_accepting(self, src) -> "bool": // Should come after the definition of twa_graph +%include %include %include %include @@ -932,6 +934,13 @@ unblock_signal(int signum) return sigprocmask(SIG_UNBLOCK, &set, 0); } +// for alternation.hh +unsigned states_and(const spot::twa_graph_ptr& aut, + const std::vector& il) +{ + return states_and(aut, il.begin(), il.end()); +} + %} %extend spot::parse_error_list { diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 5f7f17928488afdf38f83c4a2a92099e61e4638f..00d3b8bb470e5bd2ba42a37b181b7ffdaf50d758 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -28,6 +28,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) twaalgosdir = $(pkgincludedir)/twaalgos twaalgos_HEADERS = \ + alternation.hh \ are_isomorphic.hh \ bfssteps.hh \ canonicalize.hh \ @@ -84,6 +85,7 @@ twaalgos_HEADERS = \ noinst_LTLIBRARIES = libtwaalgos.la libtwaalgos_la_SOURCES = \ + alternation.cc \ are_isomorphic.cc \ bfssteps.cc \ canonicalize.cc \ diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc new file mode 100644 index 0000000000000000000000000000000000000000..7208c73cbe3cd121b6816f440a995888f8f6c6b6 --- /dev/null +++ b/spot/twaalgos/alternation.cc @@ -0,0 +1,88 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 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 . + +#include +#include +#include + +namespace spot +{ + outedge_combiner::outedge_combiner(const twa_graph_ptr& aut) + : aut_(aut), vars_(bddtrue) + { + } + + outedge_combiner::~outedge_combiner() + { + aut_->get_dict()->unregister_all_my_variables(this); + } + + bdd outedge_combiner::operator()(unsigned st) + { + const auto& dict = aut_->get_dict(); + bdd res = bddtrue; + for (unsigned d1: aut_->univ_dests(st)) + { + bdd res2 = bddfalse; + for (auto& e: aut_->out(d1)) + { + bdd out = bddtrue; + for (unsigned d: aut_->univ_dests(e.dst)) + { + auto p = state_to_var.emplace(d, 0); + if (p.second) + { + int v = dict->register_anonymous_variables(1, this); + p.first->second = v; + var_to_state.emplace(v, d); + vars_ &= bdd_ithvar(v); + } + out &= bdd_ithvar(p.first->second); + } + res2 |= e.cond & out; + } + res &= res2; + } + return res; + } + + void outedge_combiner::new_dests(unsigned st, bdd out) const + { + minato_isop isop(out); + bdd cube; + std::vector univ_dest; + while ((cube = isop.next()) != bddfalse) + { + bdd cond = bdd_exist(cube, vars_); + bdd dest = bdd_existcomp(cube, vars_); + while (dest != bddtrue) + { + assert(bdd_low(dest) == bddfalse); + auto it = var_to_state.find(bdd_var(dest)); + assert(it != var_to_state.end()); + univ_dest.push_back(it->second); + dest = bdd_high(dest); + } + std::sort(univ_dest.begin(), univ_dest.end()); + aut_->new_univ_edge(st, univ_dest.begin(), univ_dest.end(), cond); + univ_dest.clear(); + } + } + +} diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh new file mode 100644 index 0000000000000000000000000000000000000000..a54123106c031ed6f63e47da66af8cb1420b5f41 --- /dev/null +++ b/spot/twaalgos/alternation.hh @@ -0,0 +1,96 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 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 . + +#pragma once + +#include +#include + +namespace spot +{ + /// \brief Helper class combine outgoing edges in alternating + /// automata + /// + /// The idea is that you can the operator() on some state to get an + /// BDD representation of its outgoing edges (labels and + /// destinations, but not acceptance marks). The BDD representation + /// of different states can combined using & or | to build a new + /// representation of some outgoing edges that can be attached to + /// some state with new_dests. The use of BDDs helps removing + /// superfluous edges. + /// + /// Beware that new_dests() just *appends* the transitions to the + /// supplied state, it does not remove existing ones. + /// + /// operator() can be called on states with universal branching + /// (that's actually the point), and can be called on state number + /// that designate groupes of destination states (in that case the + /// conjunction of all those states are taken). + class SPOT_API outedge_combiner + { + private: + const twa_graph_ptr& aut_; + std::map state_to_var; + std::map var_to_state; + bdd vars_; + public: + outedge_combiner(const twa_graph_ptr& aut); + ~outedge_combiner(); + bdd operator()(unsigned st); + void new_dests(unsigned st, bdd out) const; + }; + + /// @{ + /// \brief Combine two states in a conjunction. + /// + /// This creates a new state whose outgoing transitions are the + /// conjunctions of the compatible transitions of s1 and s2. + /// + /// Acceptance marks are dropped. + /// + /// The results is very likely to be alternating. + template + SPOT_API + unsigned states_and(const twa_graph_ptr& aut, I begin, I end) + { + if (begin == end) + throw std::runtime_error + ("state_and() expects an non-empty list of states"); + outedge_combiner combiner(aut); + bdd combination = bddtrue; + while (begin != end) + combination &= combiner(*begin++); + unsigned new_s = aut->new_state(); + combiner.new_dests(new_s, combination); + return new_s; + } + + template + SPOT_API + unsigned states_and(const twa_graph_ptr& aut, + const std::initializer_list& il) + { + return states_and(aut, il.begin(), il.end()); + } + /// @} + + + + +} diff --git a/tests/python/alternating.py b/tests/python/alternating.py index 51b958338e3d5932ed89f5a0efadd25d9ebfe04f..a2ed3c7e533dc3a5cde9f825bdf471a80837de3d 100755 --- a/tests/python/alternating.py +++ b/tests/python/alternating.py @@ -94,3 +94,41 @@ State: 1 State: 2 [0 | 1] 2 --END--""" + +st = spot.states_and(aut, [0, 2]) +st2 = spot.states_and(aut, [1, st]) +st3 = spot.states_and(aut, [0, 1, 2]) +assert (st, st2, st3) == (3, 4, 5) + +received = False +try: + st4 = spot.states_and(aut, []) +except RuntimeError: + received = True +assert received + +h = aut.to_str('hoa') +print(h) +assert h == """HOA: v1 +States: 6 +Start: 0 +AP: 2 "p1" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: univ-branch trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1&2 {0} +[1] 0&1 +State: 1 +[0&1] 0&2&1 +State: 2 +[0 | 1] 2 +State: 3 +[0] 1&2 +[1] 0&1&2 +State: 4 +[0&1] 0&1&2 +State: 5 +[0&1] 0&1&2 +--END--"""