alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

new partial_degeneralize() algorithm

Browse source 
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it.
* tests/python/pdegen.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new function.
This commit is contained in:
Alexandre Duret-Lutz 2019-12-11 17:09:55 +01:00
parent 894fda21f9
commit bf7ccfe7e6
5 changed files with 372 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -54,6 +54,10 @@ New in spot 2.8.4.dev (not yet released)
parity_min_odd(n) = parity_min(true, n)
parity_min_even(n) = parity_min(false, n)
- partial_degeneralize() is a new function performing partial
degeneralization to get rid of conjunction of Inf terms in
acceptance conditions.
New in spot 2.8.4 (2019-12-08)
Bugs fixed:

287
spot/twaalgos/degen.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2018 Laboratoire de Recherche
// Copyright (C) 2012-2019 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -237,6 +237,62 @@ namespace spot
}
};
namespace
{
static void
keep_bottommost_copies(twa_graph_ptr& res,
scc_info& si_orig,
std::vector<unsigned>* orig_states)
{
unsigned res_ns = res->num_states();
auto a = si_orig.get_aut();
if (res_ns <= a->num_states())
return;
scc_info si_res(res, scc_info_options::TRACK_STATES);
unsigned res_scc_count = si_res.scc_count();
if (res_scc_count <= si_orig.scc_count())
return;
// If we reach this place, we have more SCCs in the output than
// in the input. This means that we have created some redundant
// SCCs. Often, these are trivial SCCs created in front of
// their larger sisters, because we did not pick the correct
// level when entering the SCC for the first time, and the level
// we picked has not been seen again when exploring the SCC.
// But it could also be the case that by entering the SCC in two
// different ways, we create two clones of the SCC (I haven't
// encountered any such case, but I do not want to rule it out
// in the code below).
//
// Now we will iterate over the SCCs in topological order to
// remember the "bottommost" SCCs that contain each original
// state. If an original state is duplicated in a higher SCC,
// it can be shunted away. Amen.
std::vector<unsigned>
bottommost_occurence(a->num_states());
{
unsigned n = res_scc_count;
do
for (unsigned s: si_res.states_of(--n))
bottommost_occurence[(*orig_states)[s]] = s;
while (n);
}
std::vector<unsigned> retarget(res_ns);
for (unsigned n = 0; n < res_ns; ++n)
{
unsigned other = bottommost_occurence[(*orig_states)[n]];
retarget[n] =
(si_res.scc_of(n) != si_res.scc_of(other)) ? other : n;
}
for (auto& e: res->edges())
e.dst = retarget[e.dst];
res->set_init_state(retarget[res->get_init_state_number()]);
res->purge_unreachable_states();
}
}
template<bool want_sba>
twa_graph_ptr
degeneralize_aux(const const_twa_graph_ptr& a, bool use_z_lvl,
@ -617,48 +673,8 @@ namespace spot
orders.print();
#endif
res->merge_edges();
unsigned res_ns = res->num_states();
if (!remove_extra_scc || res_ns <= a->num_states())
return res;
scc_info si_res(res, scc_info_options::TRACK_STATES);
unsigned res_scc_count = si_res.scc_count();
if (res_scc_count <= m->scc_count())
return res;
// If we reach this place, we have more SCCs in the output than
// in the input. This means that we have created some redundant
// SCCs. Often, these are trivial SCCs created in front of
// their larger sisters, because we did not pick the correct
// level when entering the SCC for the first time, and the level
// we picked has not been seen again when exploring the SCC.
// But it could also be the case that by entering the SCC in two
// different ways, we create two clones of the SCC (I haven't
// encountered any such case, but I do not want to rule it out
// in the code below).
//
// Now we will iterate over the SCCs in topological order to
// remember the "bottomost" SCCs that contain each original
// state. If an original state is duplicated in a higher SCC,
// it can be shunted away. Amen.
std::vector<unsigned> bottomost_occurence(a->num_states());
{
unsigned n = res_scc_count;
do
for (unsigned s: si_res.states_of(--n))
bottomost_occurence[(*orig_states)[s]] = s;
while (n);
}
std::vector<unsigned> retarget(res_ns);
for (unsigned n = 0; n < res_ns; ++n)
{
unsigned other = bottomost_occurence[(*orig_states)[n]];
retarget[n] = (si_res.scc_of(n) != si_res.scc_of(other)) ? other : n;
}
for (auto& e: res->edges())
e.dst = retarget[e.dst];
res->purge_unreachable_states();
if (remove_extra_scc)
keep_bottommost_copies(res, *(m.get()), orig_states);
return res;
}
}
@ -694,4 +710,189 @@ namespace spot
use_lvl_cache, skip_levels, ignaccsl,
remove_extra_scc);
}
namespace
{
static acc_cond::mark_t
to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen)
{
if (code.empty())
return todegen;
acc_cond::mark_t tostrip = todegen;
unsigned pos = code.size();
do
{
switch (code[pos - 1].sub.op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
--pos;
break;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
pos -= 2;
if (code[pos].mark != todegen)
tostrip -= code[pos].mark;
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg:
pos -= 2;
tostrip -= code[pos].mark;
break;
}
}
while (pos > 0);
return tostrip;
}
static void
update_acc_for_partial_degen(acc_cond::acc_code& code,
acc_cond::mark_t todegen,
acc_cond::mark_t tostrip,
acc_cond::mark_t accmark)
{
if (!todegen)
{
code &= acc_cond::acc_code::inf(accmark);
return;
}
if (code.empty())
return;
unsigned pos = code.size();
do
{
switch (code[pos - 1].sub.op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
--pos;
break;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
pos -= 2;
if (code[pos].mark == todegen)
code[pos].mark = accmark;
else
code[pos].mark = code[pos].mark.strip(tostrip);
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg:
pos -= 2;
code[pos].mark = code[pos].mark.strip(tostrip);
break;
}
}
while (pos > 0);
}
}
twa_graph_ptr
partial_degeneralize(const const_twa_graph_ptr& a,
acc_cond::mark_t todegen)
{
auto res = make_twa_graph(a->get_dict());
res->copy_ap_of(a);
acc_cond::acc_code acc = a->get_acceptance();
acc_cond::mark_t tostrip = to_strip(acc, todegen);
acc_cond::mark_t keep = a->acc().all_sets() - tostrip;
acc_cond::mark_t degenmark = {keep.count()};
update_acc_for_partial_degen(acc, todegen, tostrip, degenmark);
res->set_acceptance(acc);
std::vector<unsigned> order;
for (unsigned set: todegen.sets())
order.push_back(set);
//auto* names = new std::vector<std::string>;
//res->set_named_prop("state-names", names);
auto orig_states = new std::vector<unsigned>();
auto levels = new std::vector<unsigned>();
orig_states->reserve(a->num_states()); // likely more are needed.
levels->reserve(a->num_states());
res->set_named_prop("original-states", orig_states);
res->set_named_prop("degen-levels", levels);
scc_info si_orig(a, scc_info_options::NONE);
// degen_states -> new state numbers
ds2num_map ds2num;
queue_t todo;
auto new_state = [&](degen_state ds)
{
auto di = ds2num.find(ds);
if (di != ds2num.end())
return di->second;
unsigned ns = res->new_state();
ds2num[ds] = ns;
todo.emplace_back(ds);
//std::ostringstream os;
//os << ds.first << ',' << ds.second;
//names->push_back(os.str());
assert(ns == orig_states->size());
orig_states->emplace_back(ds.first);
levels->emplace_back(ds.second);
return ns;
};
degen_state s(a->get_init_state_number(), 0);
new_state(s);
while (!todo.empty())
{
s = todo.front();
todo.pop_front();
int src = ds2num[s];
unsigned slevel = s.second;
unsigned orig_src = s.first;
unsigned scc_src = si_orig.scc_of(orig_src);
for (auto& e: a->out(orig_src))
{
unsigned nextlvl = slevel;
acc_cond::mark_t accepting = {};
if (si_orig.scc_of(e.dst) == scc_src)
{
while (nextlvl < order.size() && e.acc.has(order[nextlvl]))
++nextlvl;
if (nextlvl == order.size())
{
accepting = degenmark;
nextlvl = 0;
if ((e.acc & todegen) != todegen)
while (nextlvl < order.size()
&& e.acc.has(order[nextlvl]))
++nextlvl;
}
accepting |= e.acc.strip(tostrip);
}
else
{
nextlvl = 0;
}
degen_state ds_dst(e.dst, nextlvl);
unsigned dst = new_state(ds_dst);
res->new_edge(src, dst, e.cond, accepting);
}
}
res->merge_edges();
keep_bottommost_copies(res, si_orig, orig_states);
return res;
}
}

27
spot/twaalgos/degen.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2015, 2017, 2018 Laboratoire de
// Copyright (C) 2012-2015, 2017-2019 Laboratoire de
// Recherche et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -27,7 +27,7 @@ namespace spot
/// \brief Degeneralize a spot::tgba into an equivalent sba with
/// only one acceptance condition.
///
/// This algorithms will build a new explicit automaton that has
/// This algorithm will build a new explicit automaton that has
/// at most (N+1) times the number of states of the original automaton.
///
/// When \a use_z_lvl is set, the level of the degeneralized
@ -78,4 +78,27 @@ namespace spot
bool ignaccsl = false,
bool remove_extra_scc = true);
/// \@}
/// \ingroup twa_acc_transform
/// \brief Partial degeneralization of a TwA
///
/// Given an automaton whose acceptance contains a conjunction of
/// Inf terms, perform a partial degeneralization to replace this
/// conjunction by a single Inf term.
///
/// For instance if the input has acceptance
/// (Fin(0)&Inf(1)&Inf(3))|Fin(2)
/// calling partial_degeneralize with \a todegen set to `{1,3}`
/// will build an equivalent automaton with acceptance
/// (Fin(0)&Inf(2))|Fin(1)
///
/// where Inf(2) tracks the acceptance of the original
/// Inf(1)&Inf(3), and Fin(1) tracks the acceptance of the original
/// Fin(2).
///
/// Cases where the sets listed in \a todegen also occur outside
/// of the Inf-conjunction are also supported.
SPOT_API twa_graph_ptr
partial_degeneralize(const const_twa_graph_ptr& a,
acc_cond::mark_t todegen);
}

1
tests/Makefile.am
View file

@ -393,6 +393,7 @@ TESTS_python = \
python/otfcrash.py \
python/parsetgba.py \
python/parity.py \
python/pdegen.py \
python/prodexpt.py \
python/_product_weak.ipynb \
python/_product_susp.ipynb \

98
tests/python/pdegen.py Normal file
View file

@ -0,0 +1,98 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2019 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 <http://www.gnu.org/licenses/>.
# 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
a, b, d = spot.automata("""
HOA: v1
States: 2
Start: 0
AP: 1 "p0"
Acceptance: 3 Inf(0)&Inf(1)|Fin(2)
--BODY--
State: 0
[0] 1 {1 2}
State: 1
[0] 0 {0}
--END--
HOA: v1
States: 3
Start: 2
AP: 1 "p0"
Acceptance: 3 Inf(0)&Inf(1)|Fin(2)
--BODY--
State: 0
[0] 1 {1 2}
State: 1
[0] 0 {0}
State: 2
[0] 0 {0}
[0] 0 {1}
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "p0"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[0] 0 {0}
--END--
""")
da = spot.partial_degeneralize(a, [0, 1])
assert da.equivalent_to(a)
assert da.num_states() == 2
db = spot.partial_degeneralize(b, [0, 1])
assert db.equivalent_to(b)
assert db.num_states() == 3
db.copy_state_names_from(b)
dbhoa = db.to_str('hoa')
assert dbhoa == """HOA: v1
States: 3
Start: 0
AP: 1 "p0"
acc-name: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 "2#0"
[0] 2
State: 1 "1#0"
[0] 2
State: 2 "0#1" {0 1}
[0] 1
--END--"""
c = spot.automaton("randaut -A'(Fin(0)&Inf(1)&Inf(2))|Fin(2)' 1 |")
dc = spot.partial_degeneralize(c, [1, 2])
assert dc.equivalent_to(c)
assert str(dc.get_acceptance()) == '(Fin(0) & Inf(2)) | Fin(1)'
dd = spot.partial_degeneralize(d, [])
assert dd.equivalent_to(d)
assert dd.num_states() == 1
assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)'