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

translate, postproc: improve parity output

Browse source 
* spot/twaalgos/translate.cc: When producing Parity output, split LTL
as we do in the Generic case.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use
acd_transform() and add an "acd" option to disable this.
* bin/spot-x.cc, NEWS: Document this.
* tests/core/genltl.test, tests/core/minusx.test,
tests/core/parity2.test: Adjust test cases for improved outputs.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-05 11:08:19 +02:00
parent e867242cf6
commit 344e01d4e2
8 changed files with 189 additions and 241 deletions
Download patch file Download diff file Expand all files Collapse all files

31
spot/twaalgos/postproc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -40,6 +40,7 @@
#include <spot/twaalgos/cobuchi.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/toparity.hh>
#include <spot/twaalgos/zlktree.hh>
namespace spot
{
@ -92,6 +93,7 @@ namespace spot
merge_states_min_ = opt->get("merge-states-min", 128);
wdba_det_max_ = opt->get("wdba-det-max", 4096);
simul_trans_pruning_ = opt->get("simul-trans-pruning", 512);
acd_ = opt->get("acd", 1);
if (sat_acc_ && sat_minimize_ == 0)
sat_minimize_ = 1; // Dicho.
@ -250,7 +252,8 @@ namespace spot
tmp = ensure_ba(tmp);
if (want_parity)
{
reduce_parity_here(tmp, COLORED_);
if (!acd_was_used_)
reduce_parity_here(tmp, COLORED_);
parity_kind kind = parity_kind_any;
parity_style style = parity_style_any;
if ((type_ & ParityMin) == ParityMin)
@ -295,6 +298,8 @@ namespace spot
bool via_gba =
(type_ == Buchi) || (type_ == GeneralizedBuchi) || (type_ == Monitor);
bool want_parity = type_ & Parity;
acd_was_used_ = false;
if (COLORED_ && !want_parity)
throw std::runtime_error("postprocessor: the Colored setting only works "
"for parity acceptance");
@ -340,18 +345,26 @@ namespace spot
!(type_ == Generic && PREF_ == Any && level_ == Low))
a = remove_alternation(a);
// If we do want a parity automaton, we can use to_parity().
// However (1) degeneralization is faster if the input is
// GBA, and (2) if we want a deterministic parity automaton and the
// input is not deterministic, that is useless here. We need
// to determinize it first, and our deterministization
// function only deal with TGBA as input.
if ((via_gba || (want_parity && !a->acc().is_parity()))
&& !a->acc().is_generalized_buchi())
{
// If we do want a parity automaton, we can use to_parity().
// However (1) degeneralization is better if the input is
// GBA, and (2) if we want a deterministic parity automaton and the
// input is not deterministic, that is useless here. We need
// to determinize it first, and our deterministization
// function only deal with TGBA as input.
if (want_parity && (PREF_ != Deterministic || is_deterministic(a)))
{
a = to_parity(a);
if (acd_)
{
a = acd_transform(a, COLORED_);
acd_was_used_ = true;
}
else
{
a = to_parity(a);
}
}
else
{

2
spot/twaalgos/postproc.hh
View file

@ -270,6 +270,8 @@ namespace spot
int simul_max_ = 4096;
int merge_states_min_ = 128;
int wdba_det_max_ = 4096;
bool acd_ = false;
bool acd_was_used_;
};
/// @}
}

20
spot/twaalgos/translate.cc
View file

@ -137,6 +137,9 @@ namespace spot
twa_graph_ptr aut;
twa_graph_ptr aut2 = nullptr;
bool split_hard =
type_ == Generic || (type_ & Parity) || type_ == GeneralizedBuchi;
if (ltl_split_ && !r.is_syntactic_obligation())
{
formula r2 = r;
@ -146,11 +149,11 @@ namespace spot
r2 = r2[0];
++leading_x;
}
if (type_ == Generic || type_ == GeneralizedBuchi)
if (split_hard)
{
// F(q|u|f) = q|F(u)|F(f) only for generic acceptance
// F(q|u|f) = q|F(u)|F(f) disabled for GeneralizedBuchi
// G(q&e&f) = q&G(e)&G(f)
bool want_u = r2.is({op::F, op::Or}) && (type_ == Generic);
bool want_u = r2.is({op::F, op::Or}) && (type_ != GeneralizedBuchi);
if (want_u || r2.is({op::G, op::And}))
{
std::vector<formula> susp;
@ -213,20 +216,19 @@ namespace spot
oblg.erase(i, oblg.end());
}
// The only cases where we accept susp and rest to be both
// non-empty is when doing Generic/Parity/TGBA
if (!susp.empty())
{
// The only cases where we accept susp and rest to be both
// non-empty is when doing Generic acceptance or TGBA.
if (!rest.empty()
&& !(type_ == Generic || type_ == GeneralizedBuchi))
if (!rest.empty() && !split_hard)
{
rest.insert(rest.end(), susp.begin(), susp.end());
susp.clear();
}
// For Parity, we want to translate all suspendable
// formulas at once.
if (rest.empty() && type_ & Parity)
susp = { formula::multop(r2.kind(), susp) };
//if (rest.empty() && type_ & Parity)
// susp = { formula::multop(r2.kind(), susp) };
}
// For TGBA and BA, we only split if there is something to
// suspend.