Commit 7b5b8f34 authored by Thomas Medioni's avatar Thomas Medioni

streett_to_generalized_buchi() now works on Streett-like

* NEWS: Mention the modification.
* spot/twaalgos/remfin.cc: Adapt to avoid infinite recursion.
* spot/twaalgos/totgba.cc: Work on Streett-like.
* tests/Makefile.am, tests/python/streett_totgba.py: Tests the
  modification.
* tests/core/remfin.test: Fix one test case that is now handled by
  the modification.
parent 570c4331
......@@ -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.
......
......@@ -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)
......
......@@ -116,17 +116,35 @@ namespace spot
// do not do anything.
if (in->acc().is_generalized_buchi())
return std::const_pointer_cast<twa_graph>(in);
int p = in->acc().is_streett();
if (p <= 0)
std::vector<acc_cond::rs_pair> 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<acc_cond::mark_t> fin_to_infpairs(numsets, 0U);
std::vector<acc_cond::mark_t> 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<acc_cond::rs_pair> 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
......
......@@ -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 \
......
......@@ -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
......
#!/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 <http://www.gnu.org/licenses/>.
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)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment