diff --git a/NEWS b/NEWS index ba1ed63c0..2b74f9c36 100644 --- a/NEWS +++ b/NEWS @@ -111,6 +111,9 @@ New in spot 2.3.4.dev (not yet released) some simplifications on an acceptance condition, and might lead to the removal of some acceptance sets. + - The function spot::streett_to_generalized_buchi() is now able to + work on automatons with Streett-like acceptance. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 01e53598c..4ec8fa0ed 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -444,7 +444,9 @@ namespace spot twa_graph_ptr street_strategy(const const_twa_graph_ptr& aut) { - return streett_to_generalized_buchi_maybe(aut); + return (aut->get_acceptance().used_inf_fin_sets().first) + ? streett_to_generalized_buchi_maybe(aut) + : nullptr; } twa_graph_ptr rabin_strategy(const const_twa_graph_ptr& aut) diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 4505f99ab..d74d1d27c 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -116,17 +116,35 @@ namespace spot // do not do anything. if (in->acc().is_generalized_buchi()) return std::const_pointer_cast(in); - int p = in->acc().is_streett(); - if (p <= 0) + + std::vector pairs; + bool res = in->acc().is_streett_like(pairs); + if (!res) throw std::runtime_error("streett_to_generalized_buchi() should only be" - " called on automata with Streett acceptance"); + " called on automata with Streett-like" + " acceptance"); // In Streett acceptance, inf sets are odd, while fin sets are // even. acc_cond::mark_t inf; acc_cond::mark_t fin; std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets(); - assert((inf >> 1U) == fin); + unsigned p = inf.count(); + + if (!p) + return remove_fin(in); + + unsigned numsets = in->acc().num_sets(); + std::vector fin_to_infpairs(numsets, 0U); + std::vector inf_to_finpairs(numsets, 0U); + for (auto pair: pairs) + { + for (unsigned mark: pair.fin.sets()) + fin_to_infpairs[mark] |= pair.inf; + + for (unsigned mark: pair.inf.sets()) + inf_to_finpairs[mark] |= pair.fin; + } scc_info si(in); @@ -139,8 +157,16 @@ namespace spot auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9} auto acc_fin = acc & fin; // {0, 2, 4,6} auto acc_inf = acc & inf; // { 1, 3, 7,9} - auto fin_wo_inf = acc_fin - (acc_inf >> 1U); // {4} - auto inf_wo_fin = acc_inf - (acc_fin << 1U); // {9} + acc_cond::mark_t fin_wo_inf = 0U; + for (unsigned mark: acc_fin.sets()) + if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf)) + fin_wo_inf |= {mark}; + + acc_cond::mark_t inf_wo_fin = 0U; + for (unsigned mark: acc_inf.sets()) + if (!inf_to_finpairs[mark] || (inf_to_finpairs[mark] - acc_fin)) + inf_wo_fin |= {mark}; + sccfi.emplace_back(fin_wo_inf, inf_wo_fin, acc_fin == 0U); } @@ -199,12 +225,14 @@ namespace spot continue; // For any Fin set we see, we want to see the // corresponding Inf set. - pend |= (t.acc & fin) << 1U; + for (unsigned mark: (t.acc & fin).sets()) + pend |= fin_to_infpairs[mark]; + pend -= t.acc & inf; // Label this transition with all non-pending // inf sets. The strip will shift everything // to the correct numbers in the targets. - acc = (inf - pend).strip(fin) & outall; + acc = (inf - pend).strip(fin - inf) & outall; // Adjust the pending sets to what will be necessary // required on the destination state. if (sbacc) @@ -212,7 +240,9 @@ namespace spot auto a = in->state_acc_sets(t.dst); if (a & scc_fin_wo_inf) continue; - pend |= (a & fin) << 1U; + for (unsigned m: (a & fin).sets()) + pend |= fin_to_infpairs[m]; + pend -= a & inf; } pend |= scc_inf_wo_fin; @@ -244,16 +274,18 @@ namespace spot // this has to occur at least once per cycle. if (pend == orig_copy && (t.src >= t.dst) && maybe_acc && !no_fin) { - acc_cond::mark_t pend = 0U; + acc_cond::mark_t stpend = 0U; if (sbacc) { auto a = in->state_acc_sets(t.dst); if (a & scc_fin_wo_inf) continue; - pend = (a & fin) << 1U; - pend -= a & inf; + for (unsigned m: (a & fin).sets()) + stpend |= fin_to_infpairs[m]; + + stpend -= a & inf; } - st2gba_state d(t.dst, pend | scc_inf_wo_fin); + st2gba_state d(t.dst, stpend | scc_inf_wo_fin); // Have we already seen this destination? unsigned dest; auto dres = bs2num.emplace(d, 0); @@ -287,7 +319,7 @@ namespace spot twa_graph_ptr streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in) { - static int min = [&]() { + static unsigned min = [&]() { const char* c = getenv("SPOT_STREETT_CONV_MIN"); if (!c) return 3; @@ -297,12 +329,16 @@ namespace spot throw std::runtime_error("unexpected value for SPOT_STREETT_CONV_MIN"); return val; }(); - if (min == 0 || min > in->acc().is_streett()) + + std::vector pairs; + in->acc().is_streett_like(pairs); + if (min == 0 || min > pairs.size()) return nullptr; else return streett_to_generalized_buchi(in); } + /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Büchi automaton. twa_graph_ptr diff --git a/tests/Makefile.am b/tests/Makefile.am index 3da8475f2..739675455 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -365,6 +365,7 @@ TESTS_python = \ python/setacc.py \ python/setxor.py \ python/simstate.py \ + python/streett_totgba.py \ python/rs_like.py \ python/sum.py \ python/trival.py \ diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 6bd214bbf..007e0ff96 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -579,7 +579,7 @@ Start: 0 AP: 2 "a" "b" acc-name: generalized-Buchi 12 Acceptance: 12 $acctwelve -properties: trans-labels explicit-labels trans-acc complete +properties: trans-labels explicit-labels state-acc complete --BODY-- State: 0 [!0] 0 @@ -594,8 +594,8 @@ State: 1 [1] 4 State: 2 [t] 2 -[1] 4 [!1] 5 +[1] 4 State: 3 [t] 3 [1] 4 @@ -607,8 +607,8 @@ State: 4 [!1] 9 State: 5 [t] 5 -[1] 7 [1] 10 +[1] 7 [1] 11 State: 6 [t] 6 @@ -617,8 +617,8 @@ State: 6 [1] 13 State: 7 [t] 7 -[!1] 9 [1] 11 +[!1] 9 State: 8 [t] 8 [!1] 9 @@ -630,12 +630,12 @@ State: 9 [1] 16 State: 10 [t] 10 -[1] 11 [!1] 17 +[1] 11 State: 11 [t] 11 -[!1] 14 [!1] 18 +[!1] 14 [!1] 19 State: 12 [t] 12 @@ -648,8 +648,8 @@ State: 13 [!1] 22 State: 14 [t] 14 -[1] 16 [!1] 19 +[1] 16 State: 15 [t] 15 [1] 16 @@ -660,40 +660,40 @@ State: 16 [!1] 24 [!1] 25 State: 17 -[!1] 17 [1] 26 +[!1] 17 [1] 27 State: 18 +[1] 27 [!1] 18 [!1] 19 -[1] 27 State: 19 -[!1] 19 [1] 28 +[!1] 19 [1] 29 State: 20 -[!1] 20 [1] 30 [1] 31 +[!1] 20 State: 21 +[1] 31 [!1] 21 [!1] 22 -[1] 31 State: 22 -[!1] 22 [1] 32 [1] 33 +[!1] 22 State: 23 +[1] 29 [!1] 23 [!1] 25 -[1] 29 State: 24 +[1] 33 [!1] 24 [!1] 25 -[1] 33 State: 25 -[!1] 25 {0 1 2 3 4 6 7 8 9 10} [1] 34 +[!1] 25 State: 26 [t] 26 [1] 27 @@ -718,14 +718,14 @@ State: 32 State: 33 [t] 33 [!1] 36 -State: 34 -[t] 34 {0 1 2 3 4 5 6 7 8 9 10 11} +State: 34 {0 1 2 3 4 5 6 7 8 9 10 11} +[t] 34 State: 35 [1] 34 -[!1] 35 {0 1 2 3 4 6 7 8 9 10 11} +[!1] 35 State: 36 [1] 34 -[!1] 36 {0 1 2 3 4 5 6 7 8 9 10} +[!1] 36 --END-- HOA: v1 States: 2 diff --git a/tests/python/streett_totgba.py b/tests/python/streett_totgba.py new file mode 100644 index 000000000..30e5847eb --- /dev/null +++ b/tests/python/streett_totgba.py @@ -0,0 +1,84 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# l'EPITA. +# +# 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 os +import shutil +import sys + +def parse_multiple_auts(hoa): + l = hoa.split('--END--') + a = [] + cpt = 0 + for x in l: + if x.isspace() or x == '': + continue + x = x + "--END--" + a.append(spot.automaton(x)) + + return a + +def ensure_deterministic(a): + if a.is_existential() and spot.is_deterministic(a): + return a + + return a.postprocess('Generic', 'deterministic', 'Low') + +def equivalent(a1, a2): + na1 = spot.dualize(ensure_deterministic(a1)) + na2 = spot.dualize(ensure_deterministic(a2)) + return (not a1.intersects(na2)) and (not a2.intersects(na1)) + +def tgba(a): + if not a.is_existential(): + a = spot.remove_alternation(a) + a = spot.to_generalized_buchi(a) + return a + +def test_aut(aut): + stgba = tgba(aut) + assert equivalent(stgba, aut) + os.environ["SPOT_STREETT_CONV_MIN"] = '1' + sftgba = tgba(aut) + del os.environ["SPOT_STREETT_CONV_MIN"] + assert equivalent(stgba, sftgba) + + slike = spot.simplify_acceptance(aut) + + sltgba = tgba(slike) + os.environ["SPOT_STREETT_CONV_MIN"] = "1" + slftgba = tgba(slike) + del os.environ["SPOT_STREETT_CONV_MIN"] + assert equivalent(sltgba, slftgba) + +# Those automatons are generated with ltl2dstar, which is NOT part of spot, +# using the following command: +# genltl --eh-patterns --dac-patterns --hkrss-patterns --sb-patterns |\ +# ltldo "ltl2dstar --automata=streett --output-format=hoa\ +# --ltl2nba=spin:ltl2tgba@-s %L ->%O" -F- --name=%f -H" + +if shutil.which('ltl2dstar') is None: + sys.exit(77) +for a in spot.automata('genltl --eh-patterns --dac-patterns --hkrss-patterns\ + --sb-patterns |\ + ltldo "ltl2dstar --automata=streett --output-format=hoa\ + --ltl2nba=spin:ltl2tgba@-s %L ->%O"\ + -T5 -F- --name=%f -H|'): + test_aut(a)