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

add a newer version of the generic emptiness check

Browse source 
As discussed with Jan Strejček.

* spot/twa/acc.cc, spot/twa/acc.hh (fin_unit_one_split): New function.
(fin_one_extract): Return the simplified acceptance condition as an
optimization.
* python/spot/impl.i: Bind this new function.
* tests/python/acc.py: New file, to test it.
* tests/Makefile.am: Add acc.py.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Implement the
spot211 variant of the emptiness check.
* tests/python/genem.py: Test it.
* tests/python/acc_cond.ipynb: Adjust test for fin_one_extract.
This commit is contained in:
Alexandre Duret-Lutz 2022-05-25 17:02:38 +02:00
parent aca6bd9042
commit 721d5695ec
9 changed files with 308 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

99
spot/twa/acc.cc
View file

@ -2707,6 +2707,35 @@ namespace spot
return false;
}
// Check wheter pos looks like Fin(f) or Fin(f)&rest
bool is_conj_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
{
auto sub = pos - pos->sub.size;
do
{
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
--pos;
break;
case acc_cond::acc_op::Or:
pos -= pos->sub.size + 1;
break;
case acc_cond::acc_op::Fin:
if (pos[-1].mark & f)
return true;
SPOT_FALLTHROUGH;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
case acc_cond::acc_op::FinNeg:
pos -= 2;
break;
}
}
while (sub < pos);
return false;
}
acc_cond::acc_code extract_fin(const acc_cond::acc_word* pos,
acc_cond::mark_t f)
{
@ -2716,7 +2745,7 @@ namespace spot
case acc_cond::acc_op::And:
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::Inf:
return pos;
return strip_rec(pos, f, true, false);
case acc_cond::acc_op::Or:
{
--pos;
@ -2725,7 +2754,7 @@ namespace spot
{
if (uses_fin(pos, f))
{
acc_cond::acc_code tmp(pos);
auto tmp = strip_rec(pos, f, true, false);
tmp |= std::move(res);
std::swap(tmp, res);
}
@ -2742,6 +2771,52 @@ namespace spot
SPOT_UNREACHABLE();
return {};
}
std::pair<acc_cond::acc_code, acc_cond::acc_code>
split_top_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
{
auto start = pos - pos->sub.size;
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Fin:
if (is_conj_fin(pos, f))
return {pos, acc_cond::acc_code::f()};
SPOT_FALLTHROUGH;
case acc_cond::acc_op::Inf:
return {acc_cond::acc_code::f(), pos};
case acc_cond::acc_op::Or:
{
--pos;
auto left = acc_cond::acc_code::f();
auto right = acc_cond::acc_code::f();
do
{
if (is_conj_fin(pos, f))
{
auto tmp = strip_rec(pos, f, true, false);
tmp |= std::move(left);
std::swap(tmp, left);
}
else
{
acc_cond::acc_code tmp(pos);
tmp |= std::move(right);
std::swap(tmp, right);
}
pos -= pos->sub.size + 1;
}
while (pos > start);
return {std::move(left), std::move(right)};
}
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
return {acc_cond::acc_code::f(), acc_cond::acc_code::f()};
}
SPOT_UNREACHABLE();
return {acc_cond::acc_code::f(), acc_cond::acc_code::f()};
}
}
std::pair<int, acc_cond::acc_code>
@ -2756,6 +2831,26 @@ namespace spot
return {selected_fin, extract_fin(pos, {(unsigned) selected_fin})};
}
std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
acc_cond::acc_code::fin_unit_one_split() const
{
if (SPOT_UNLIKELY(is_t() || is_f()))
err:
throw std::runtime_error("fin_unit_one_split(): no Fin");
const acc_cond::acc_word* pos = &back();
int selected_fin = has_top_fin(pos);
if (selected_fin >= 0)
{
auto [left, right] = split_top_fin(pos, {(unsigned) selected_fin});
return {selected_fin, std::move(left), std::move(right)};
}
selected_fin = fin_one();
if (selected_fin < 0)
goto err;
acc_cond::mark_t fo_m = {(unsigned) selected_fin};
return {selected_fin, extract_fin(pos, fo_m), force_inf(fo_m)};
}
namespace
{
bool

75
spot/twa/acc.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -26,6 +26,7 @@
#include <algorithm>
#include <numeric>
#include <bddx.h>
#include <tuple>
#include <spot/misc/_config.h>
#include <spot/misc/bitset.hh>
#include <spot/misc/trival.hh>
@ -1271,7 +1272,8 @@ namespace spot
int fin_one() const;
/// \brief Return one acceptance set i that appears as `Fin(i)`
/// in the condition, and all disjuncts containing it.
/// in the condition, and all disjuncts containing it with
/// Fin(i) changed to true and Inf(i) to false.
///
/// If the condition is a disjunction and one of the disjunct
/// has the shape `...&Fin(i)&...`, then `i` will be prefered
@ -1282,13 +1284,34 @@ namespace spot
/// `Fin(i)` have been removed.
///
/// For example on
/// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))`
/// the output would be the pair
/// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`.
/// On that example `Fin(1)` is prefered to `Fin(7)` because
/// it appears at the top-level.
/// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` the
/// output would be the pair, we would select `Fin(1)` over
/// `Fin(7)` because it appears at the top-level. Then we would
/// collect the disjuncts containing `Fin(1)`, that is,
/// `Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. Finally we would
/// replace `Fin(1)` by true and `Inf(1)` by false. The return
/// value would then be `(1, Inf(2)|Inf(5))`.
std::pair<int, acc_code> fin_one_extract() const;
/// \brief Split an acceptance condition, trying to select one
/// unit-Fin.
///
/// If the condition is a disjunction and one of the disjunct as
/// has the shape `...&Fin(i)&...`, then this will return
/// (i, left, right), where left is all disjunct of this form, and
/// right are all the others.
///
/// If the input formula has the shape `...&Fin(i)&...` then left
/// is set to the entire formula, and right is empty.
///
/// If no disjunct has the right shape, then a random Fin(i) is
/// searched in the formula, and the output (i, left, right).
/// is such that left contains all disjuncts containing Fin(i)
/// (at any depth), and right contains the original formlula
/// where Fin(i) has been replaced by false.
std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
fin_unit_one_split() const;
/// \brief Help closing accepting or rejecting cycle.
///
/// Assuming you have a partial cycle visiting all acceptance
@ -2203,7 +2226,8 @@ namespace spot
}
/// \brief Return one acceptance set i that appears as `Fin(i)`
/// in the condition, and all disjuncts containing it.
/// in the condition, and all disjuncts containing it with
/// Fin(i) changed to true and Inf(i) to false.
///
/// If the condition is a disjunction and one of the disjunct
/// has the shape `...&Fin(i)&...`, then `i` will be prefered
@ -2214,17 +2238,42 @@ namespace spot
/// `Fin(i)` have been removed.
///
/// For example on
/// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))`
/// the output would be the pair
/// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`.
/// On that example `Fin(1)` is prefered to `Fin(7)` because
/// it appears at the top-level.
/// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` the
/// output would be the pair, we would select `Fin(1)` over
/// `Fin(7)` because it appears at the top-level. Then we would
/// collect the disjuncts containing `Fin(1)`, that is,
/// `Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. Finally we would
/// replace `Fin(1)` by true and `Inf(1)` by false. The return
/// value would then be `(1, Inf(2)|Inf(5))`.
std::pair<int, acc_cond> fin_one_extract() const
{
auto [f, c] = code_.fin_one_extract();
return {f, {num_sets(), std::move(c)}};
}
/// \brief Split an acceptance condition, trying to select one
/// unit-Fin.
///
/// If the condition is a disjunction and one of the disjunct as
/// has the shape `...&Fin(i)&...`, then this will return
/// (i, left, right), where left is all disjunct of this form, and
/// right are all the others.
///
/// If the input formula has the shape `...&Fin(i)&...` then left
/// is set to the entire formula, and right is empty.
///
/// If no disjunct has the right shape, then a random Fin(i) is
/// searched in the formula, and the output (i, left, right).
/// is such that left contains all disjuncts containing Fin(i)
/// (at any depth), and right contains the original formlula
/// where Fin(i) has been replaced by false.
std::tuple<int, acc_cond, acc_cond>
fin_unit_one_split() const
{
auto [f, l, r] = code_.fin_unit_one_split();
return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
}
/// \brief Return the top-level disjuncts.
///
/// For instance, if the formula is

27
spot/twaalgos/genem.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2021 Laboratoire de Recherche et Developpement
// Copyright (C) 2017-2022 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -25,7 +25,7 @@ namespace spot
{
namespace
{
enum genem_version_t { spot28, atva19, spot29, spot210 };
enum genem_version_t { spot28, atva19, spot29, spot210, spot211 };
static genem_version_t genem_version = spot29;
}
@ -33,6 +33,8 @@ namespace spot
{
if (emversion == nullptr || !strcasecmp(emversion, "spot29"))
genem_version = spot29;
else if (!strcasecmp(emversion, "spot211"))
genem_version = spot211;
else if (!strcasecmp(emversion, "spot210"))
genem_version = spot210;
else if (!strcasecmp(emversion, "spot28"))
@ -41,7 +43,8 @@ namespace spot
genem_version = atva19;
else
throw std::invalid_argument("generic_emptiness_check version should be "
"one of {spot28, atva19, spot29, spot210}");
"one of {spot28, atva19, spot29, spot210, "
"spot211}");
}
namespace
@ -84,6 +87,8 @@ namespace spot
scc_split_check(const scc_info& si, unsigned scc, const acc_cond& acc,
Extra extra, acc_cond::mark_t tocut)
{
if (genem_version == spot211 || genem_version == spot210)
tocut |= acc.fin_unit();
scc_and_mark_filter filt(si, scc, tocut);
filt.override_acceptance(acc);
scc_info upper_si(filt, EarlyStop
@ -118,13 +123,27 @@ namespace spot
// Try to accept when Fin(fo) == true
acc_cond::mark_t fo_m = {(unsigned) fo};
if (!scc_split_check<EarlyStop, Extra>
(si, scc, fpart.remove(fo_m, true), extra, fo_m))
(si, scc, fpart, extra, fo_m))
if constexpr (EarlyStop)
return false;
// Try to accept when Fin(fo) == false
acc = acc.force_inf(fo_m);
}
while (!acc.is_f());
else if (genem_version == spot211)
{
do
{
auto [fo, fpart, rest] = acc.fin_unit_one_split();
acc_cond::mark_t fo_m = {(unsigned) fo};
if (!scc_split_check<EarlyStop, Extra>
(si, scc, fpart, extra, fo_m))
if constexpr (EarlyStop)
return false;
acc = rest;
}
while (!acc.is_f());
}
else if (genem_version == spot29)
do
{

10
spot/twaalgos/genem.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2021 Laboratoire de Recherche et Developpement
// Copyright (C) 2017-2022 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -100,7 +100,13 @@ namespace spot
/// - "spot29" improves upon the worst case of atva19. This is
/// the default.
/// - "spot210" improves upon "spot29" in a few cases where a Fin
/// is shared by multiple disjuncts.
/// is shared by multiple disjuncts. This improve the worst
/// case complexity of EL-automata in the general case, but worsen
/// the complexity of Hyper-Rabin in particular.
/// - "spot211" is another attempt at fixing worst case complexities.
/// Compared to atva19, this improves the complexities for Rabin,
/// GeneralizedRabin, and EL without worsening the complexity of
/// Hyper-Rabin.
SPOT_API void
generic_emptiness_check_select_version(const char* emversion = nullptr);