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.
This commit is contained in:
Thomas Medioni
parent
570c433122
commit
7b5b8f34f0
6 changed files with 162 additions and 36 deletions
3
NEWS
3
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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
84
tests/python/streett_totgba.py
Normal file
84
tests/python/streett_totgba.py
Normal file
|
|
@ -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 <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)
|
||||
Loading…
Add table
Add a link
Reference in a new issue