diff --git a/NEWS b/NEWS index 535dee5fa..f6ec9ad15 100644 --- a/NEWS +++ b/NEWS @@ -142,6 +142,15 @@ New in spot 2.10.6.dev (not yet released) succesors, should be called before running simulation-based reductions. + - A new function delay_branching_here(aut) can be used to simplify + some non-deterministic branching. If two transitions (q₁,ℓ,M,q₂) + and (q₁,ℓ,M,q₃) differ only by their destination state, and are + the only incoming transitions of their destination states, then q₂ + and q₃ can be merged (taking the union of their outgoing + transitions). This is cheap function is automatically called by + spot::translate() after translation of a formula to GBA, before + further simplification. + - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only diff --git a/python/spot/impl.i b/python/spot/impl.i index 23c07c4e8..88bdcf5c4 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -114,13 +114,14 @@ #include #include #include -#include -#include -#include #include #include #include #include +#include +#include +#include +#include #include #include #include @@ -678,11 +679,14 @@ def state_is_accepting(self, src) -> "bool": %include %include %include -%include -%include %include %include %include +%include +%include +%include +%include +%include %feature("flatnested") spot::twa_run::step; %include %template(list_step) std::list; @@ -694,8 +698,6 @@ def state_is_accepting(self, src) -> "bool": %include %include %include -%include -%include %include %include %include diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 4d0009e93..2a72702f3 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1323,18 +1323,6 @@ namespace spot } init_number_ = newst[init_number_]; g_.defrag_states(newst, used_states); - // Make sure we did not mess up the structure - assert([&]() - { - if (auto sp = get_named_prop>("state-player")) - { - for (const auto& e : edges()) - if (sp->at(e.src) == sp->at(e.dst)) - return false; - return true; - } - return true; - }() && "Game not alternating!"); } void twa_graph::remove_unused_ap() diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index ff71982b5..57ae8ce9f 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008-2018, 2020-2021 Laboratoire de Recherche et +## Copyright (C) 2008-2018, 2020-2022 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -42,6 +42,7 @@ twaalgos_HEADERS = \ contains.hh \ copy.hh \ cycles.hh \ + dbranch.hh \ degen.hh \ determinize.hh \ dot.hh \ @@ -115,6 +116,7 @@ libtwaalgos_la_SOURCES = \ compsusp.cc \ contains.cc \ cycles.cc \ + dbranch.cc \ degen.cc \ determinize.cc \ dot.cc \ diff --git a/spot/twaalgos/dbranch.cc b/spot/twaalgos/dbranch.cc new file mode 100644 index 000000000..465f8326e --- /dev/null +++ b/spot/twaalgos/dbranch.cc @@ -0,0 +1,163 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2022 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 "config.h" + +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + typedef std::pair bdd_color; + + struct bdd_color_hash + { + size_t + operator()(const bdd_color& bc) const noexcept + { + return bc.first.id() ^ bc.second.hash(); + } + }; + + template + bool delay_branching_aux(const twa_graph_ptr& aut, std::vector* owner) + { + unsigned ns = aut->num_states(); + // number of predecessors of each state + std::vector pred_count(ns, 0); + unsigned init = aut->get_init_state_number(); + pred_count[init] = 2; // pretend the initial state has too many + // predecessors, so it does not get fused. + // for each state, number of successors that have a single predecessors + std::vector succ_cand(ns, 0); + for (auto& e: aut->edges()) + for (unsigned d: aut->univ_dests(e)) + { + // Note that e.dst might be a destination group in + // alternating automata. + unsigned pc = ++pred_count[d]; + succ_cand[e.src] += (pc == 1) - (pc == 2); + } + bool changed = false; + typedef robin_hood::unordered_map hashmap_t; + hashmap_t first_dest[1 + is_game]; + auto& g = aut->get_graph(); + + // setup a DFS + std::vector seen(ns); + std::stack todo; + auto push_state = [&](unsigned state) + { + todo.push(state); + seen[state] = true; + }; + push_state(init); + + while (!todo.empty()) + { + unsigned src = todo.top(); + todo.pop(); + if (succ_cand[src] < 2) // nothing to merge + { + for (auto& e: aut->out(src)) + for (unsigned d: aut->univ_dests(e)) + if (!seen[d]) + push_state(d); + continue; + } + first_dest[0].clear(); + if constexpr (is_game) + first_dest[1].clear(); + auto it = g.out_iteraser(src); + while (it) + { + unsigned canddst = it->dst; + for (unsigned d: aut->univ_dests(canddst)) + if (!seen[d]) + push_state(d); + if (aut->is_univ_dest(canddst) || pred_count[canddst] != 1) + { + ++it; + continue; + } + if (it->cond == bddfalse) + { + it.erase(); + continue; + } + unsigned mapidx = is_game ? (*owner)[canddst] : 0; + auto [it2, inserted] = + first_dest[mapidx].emplace(bdd_color{it->cond, it->acc}, + canddst); + if (inserted) + { + ++it; + continue; + } + unsigned mergedst = it2->second; + // we have to merge canddst into mergedst. This is as + // simple as: + // 1) connecting their list of transitions + unsigned& mergedfirst = g.state_storage(mergedst).succ; + unsigned& mergedlast = g.state_storage(mergedst).succ_tail; + unsigned& candfirst = g.state_storage(canddst).succ; + unsigned& candlast = g.state_storage(canddst).succ_tail; + if (mergedlast) + aut->edge_storage(mergedlast).next_succ = candfirst; + else // mergedst had now successor + mergedfirst = candfirst; + mergedlast = candlast; + // 2) updating the source of the merged transitions + for (unsigned e2 = candfirst; e2 != 0;) + { + auto& edge = aut->edge_storage(e2); + edge.src = mergedst; + e2 = edge.next_succ; + } + // 3) deleting the edge to canddst. + candfirst = candlast = 0; + it.erase(); + // 4) updating succ_cand + succ_cand[mergedst] += succ_cand[canddst]; + succ_cand[canddst] = 0; + changed = true; + } + } + return changed; + } + } + + bool delay_branching_here(const twa_graph_ptr& aut) + { + if (aut->prop_universal()) + return false; + auto owner = aut->get_named_prop>("state-player"); + if (SPOT_UNLIKELY(owner)) + return delay_branching_aux(aut, owner); + else + return delay_branching_aux(aut, nullptr); + } +} diff --git a/spot/twaalgos/dbranch.hh b/spot/twaalgos/dbranch.hh new file mode 100644 index 000000000..9cd0efa5e --- /dev/null +++ b/spot/twaalgos/dbranch.hh @@ -0,0 +1,36 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2022 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 + +namespace spot +{ + /// \ingroup twa_algorithms + /// \brief Merge states to delay + /// + /// If a state (x) has two outgoing transitions (x,l,m,y) and + /// (x,l,m,z) going to states (x) and (y) that have no other + /// incoming edges, then (y) and (z) can be merged (keeping the + /// union of their outgoing destinations). + /// + /// \return true iff the automaton was modified. + SPOT_API bool delay_branching_here(const twa_graph_ptr& aut); +} diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 4db8643f9..a5a84a10b 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018, 2020-2021 Laboratoire de Recherche et +// Copyright (C) 2013-2018, 2020-2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -29,6 +29,7 @@ #include #include #include +#include namespace spot { @@ -401,6 +402,11 @@ namespace spot aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop, true, false, false, nullptr, nullptr, unambiguous); + if (delay_branching_here(aut)) + { + aut->purge_unreachable_states(); + aut->merge_edges(); + } } aut = this->postprocessor::run(aut, r); diff --git a/tests/Makefile.am b/tests/Makefile.am index 91d3f10ea..9570f7dcd 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -405,6 +405,7 @@ TESTS_python = \ python/bddnqueen.py \ python/bugdet.py \ python/complement_semidet.py \ + python/dbranch.py \ python/declenv.py \ python/decompose_scc.py \ python/det.py \ diff --git a/tests/core/genltl.test b/tests/core/genltl.test index d5efb0236..d943c4cae 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016-2021 Laboratoire de Recherche et Développement +# Copyright (C) 2016-2022 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -134,8 +134,8 @@ genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \ --pps-arbiter-standard=2..3 --pps-arbiter-strict=2..3 --format=%F=%L,%f | ltl2tgba --low --det -F-/2 --stats='%<,%s' > out cat >exp<. + +# 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 +from unittest import TestCase +tc = TestCase() + +aut5 = spot.automaton("""HOA: v1 States: 28 Start: 0 AP: 4 "alive" "b" +"a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels +explicit-labels state-acc very-weak --BODY-- State: 0 [0] 1 [0] 2 [0] +3 [0] 4 [0] 5 [0&!1] 6 [0] 7 State: 1 [0] 8 State: 2 [!0] 9 [0] 10 +State: 3 [!0] 9 [0] 11 State: 4 [!0] 9 [0] 12 State: 5 [!0] 9 [0] 13 +State: 6 [!0] 9 [0&!1] 14 State: 7 [!0] 9 [0&!1&!2] 14 State: 8 [0] 15 +State: 9 {0} [!0] 9 State: 10 [!0] 9 [0] 16 State: 11 [!0] 9 [0] 17 +State: 12 [!0] 9 [0] 18 State: 13 [!0] 9 [0&!1&!2] 19 State: 14 [!0] 9 +[0&!1] 19 State: 15 [0] 20 State: 16 [!0] 9 [0] 21 State: 17 [!0] 9 +[0] 22 State: 18 [!0] 9 [0&!1&!2] 23 State: 19 [!0] 9 [0&!1] 23 State: +20 [0] 24 State: 21 [!0] 9 [0] 25 State: 22 [!0] 9 [0&!1&!2] 26 State: +23 [!0] 9 [0&!1] 26 State: 24 [0&3] 27 State: 25 [!0] 9 [0&!1&!2] 27 +State: 26 [!0] 9 [0&!1] 27 State: 27 [!0] 9 [0] 27 --END--""") + +copy = spot.make_twa_graph(aut5, spot.twa_prop_set.all()) + +tc.assertFalse(spot.is_deterministic(aut5)) +if spot.delay_branching_here(aut5): + aut5.purge_unreachable_states() + aut5.merge_edges() +tc.assertEqual(aut5.num_states(), 13) +tc.assertEqual(aut5.num_edges(), 29) +tc.assertTrue(spot.are_equivalent(copy, aut5)) + +a = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" +Acceptance: 0 t --BODY-- State: 0 [0] 1 [0] 2 [0] 3 State: 1 [!1] 4&5 +[1] 5&6 State: 2 [0] 4&6 State: 3 [0] 3&6 State: 4 [!0] 7 State: 5 +[!0] 7 State: 6 [!0] 6 State: 7 [0] 7 --END--""") + +copy = spot.make_twa_graph(a, spot.twa_prop_set.all()) +if spot.delay_branching_here(a): + a.purge_unreachable_states() + a.merge_edges() +tc.assertEqual(a.to_str(), """HOA: v1 +States: 7 +Start: 0 +AP: 3 "b" "a" "c" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc univ-branch +--BODY-- +State: 0 +[1] 1 +[1] 2 +State: 1 +[1] 3&5 +[0] 4&5 +[!0] 3&4 +State: 2 +[1] 2&5 +State: 3 +[!1] 6 +State: 4 +[!1] 6 +State: 5 +[!1] 5 +State: 6 +[1] 6 +--END--""") + +a = spot.automaton("""HOA: v1 +States: 9 +Start: 0 AP: 2 "a" "b" +spot.state-player: 0 1 1 0 0 0 0 1 1 +Acceptance: 0 t +--BODY-- +State: 0 +[0] 1 +[0] 2 +[0] 3 +[0] 4 +State: 1 +[1] 5 +State: 2 +[!1] 6 +State: 3 +[1] 7 +State: 4 +[!1] 8 +State: 5 +[t] 5 +State: 6 +[t] 6 +State: 7 +[t] 7 +State: 8 +[t] 8 +--END--""") +copy = spot.make_twa_graph(a, spot.twa_prop_set.all()) +if spot.delay_branching_here(a): + a.purge_unreachable_states() +tc.assertTrue(spot.are_equivalent(a, copy)) +tc.assertEqual(a.to_str(), """HOA: v1 +States: 7 +Start: 0 +AP: 2 "b" "a" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc very-weak +spot-state-player: 0 1 0 0 0 1 1 +--BODY-- +State: 0 +[1] 1 +[1] 2 +State: 1 +[0] 3 +[!0] 4 +State: 2 +[0] 5 +[!0] 6 +State: 3 +[t] 3 +State: 4 +[t] 4 +State: 5 +[t] 5 +State: 6 +[t] 6 +--END--""")