Commit 42ebf8b1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

postproc: introduce --parity output

* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add parity
  options.
* bin/common_post.cc: Add support for --parity.
* NEWS: Mention it.
* tests/core/parity2.test: New file.
* tests/Makefile.am: Add it.
parent 412c2059
...@@ -47,6 +47,11 @@ New in spot 2.4.4.dev (net yet released) ...@@ -47,6 +47,11 @@ New in spot 2.4.4.dev (net yet released)
- ltlsynt is a new tool for synthesizing a controller from LTL/PSL - ltlsynt is a new tool for synthesizing a controller from LTL/PSL
specifications. specifications.
- ltl2tgba, autfilt, and dstar2tgba have a new '--parity' option to
force parity acceptance on the output. Different styles can be
requested using for instance --parity='min odd' or --parity='max
even'.
- ltldo learned to limit the number of automata it outputs using -n. - ltldo learned to limit the number of automata it outputs using -n.
- autcross, ltlcross, and ltldo learned --fail-on-timeout. - autcross, ltlcross, and ltldo learned --fail-on-timeout.
...@@ -176,6 +181,11 @@ New in spot 2.4.4.dev (net yet released) ...@@ -176,6 +181,11 @@ New in spot 2.4.4.dev (net yet released)
optimization for stutter-invariant automata that may produce slightly optimization for stutter-invariant automata that may produce slightly
smaller automata. smaller automata.
- spot::postprocessor::set_type() can now request different forms of
parity acceptance as output. However currently the conversions
are not very smart: if the input does not already have parity
acceptance, it will simply be degeneralized or determinized.
- acc_cond::name(fmt) is a new method that name well-known acceptance - acc_cond::name(fmt) is a new method that name well-known acceptance
conditions. The fmt parameter specify the format to use for that conditions. The fmt parameter specify the format to use for that
name (e.g. to the style used in HOA, or that used by print_dot()). name (e.g. to the style used in HOA, or that used by print_dot()).
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche // Copyright (C) 2012-2016, 2018 Laboratoire de Recherche et
// et Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -21,6 +21,7 @@ ...@@ -21,6 +21,7 @@
#include "common_r.hh" #include "common_r.hh"
#include "common_aoutput.hh" #include "common_aoutput.hh"
#include "error.h" #include "error.h"
#include "argmatch.h"
spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_type type = spot::postprocessor::TGBA;
spot::postprocessor::output_pref pref = spot::postprocessor::Small; spot::postprocessor::output_pref pref = spot::postprocessor::Small;
...@@ -55,6 +56,10 @@ static constexpr const argp_option options[] = ...@@ -55,6 +56,10 @@ static constexpr const argp_option options[] =
{ "state-based-acceptance", 'S', nullptr, 0, { "state-based-acceptance", 'S', nullptr, 0,
"define the acceptance using states", 0 }, "define the acceptance using states", 0 },
{ "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "parity", 'P',
"any|min|max|odd|even|min odd|min even|max odd|max even",
OPTION_ARG_OPTIONAL,
"automaton with parity acceptance", 0, },
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 },
...@@ -105,6 +110,10 @@ static const argp_option options_disabled[] = ...@@ -105,6 +110,10 @@ static const argp_option options_disabled[] =
{ "state-based-acceptance", 'S', nullptr, 0, { "state-based-acceptance", 'S', nullptr, 0,
"define the acceptance using states", 0 }, "define the acceptance using states", 0 },
{ "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "parity", 'P',
"[any|min|max|odd|even|min odd|min even|max odd|max even]",
OPTION_ARG_OPTIONAL,
"automaton with parity acceptance", 0, },
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 },
...@@ -123,7 +132,7 @@ static const argp_option options_disabled[] = ...@@ -123,7 +132,7 @@ static const argp_option options_disabled[] =
}; };
static int static int
parse_opt_post(int key, char*, struct argp_state*) parse_opt_post(int key, char* arg, struct argp_state*)
{ {
// This switch is alphabetically-ordered. // This switch is alphabetically-ordered.
switch (key) switch (key)
...@@ -148,6 +157,40 @@ parse_opt_post(int key, char*, struct argp_state*) ...@@ -148,6 +157,40 @@ parse_opt_post(int key, char*, struct argp_state*)
case 'M': case 'M':
type = spot::postprocessor::Monitor; type = spot::postprocessor::Monitor;
break; break;
case 'P':
{
static char const *const parity_args[] =
{
"any", "min", "max", "odd", "even",
"min odd", "odd min",
"min even", "even min",
"max odd", "odd max",
"max even", "even max",
nullptr
};
static spot::postprocessor::output_type const parity_types[] =
{
spot::postprocessor::Parity,
spot::postprocessor::ParityMin,
spot::postprocessor::ParityMax,
spot::postprocessor::ParityOdd,
spot::postprocessor::ParityEven,
spot::postprocessor::ParityMinOdd,
spot::postprocessor::ParityMinOdd,
spot::postprocessor::ParityMinEven,
spot::postprocessor::ParityMinEven,
spot::postprocessor::ParityMaxOdd,
spot::postprocessor::ParityMaxOdd,
spot::postprocessor::ParityMaxEven,
spot::postprocessor::ParityMaxEven,
};
ARGMATCH_VERIFY(parity_args, parity_types);
if (arg)
type = XARGMATCH("--parity", arg, parity_args, parity_types);
else
type = spot::postprocessor::Parity;
}
break;
case 'S': case 'S':
sbacc = spot::postprocessor::SBAcc; sbacc = spot::postprocessor::SBAcc;
break; break;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement // Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -35,6 +35,7 @@ ...@@ -35,6 +35,7 @@
#include <spot/twaalgos/sepsets.hh> #include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/determinize.hh> #include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/alternation.hh> #include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/parity.hh>
namespace spot namespace spot
{ {
...@@ -147,6 +148,15 @@ namespace spot ...@@ -147,6 +148,15 @@ namespace spot
return do_sba_simul(d, ba_simul_); return do_sba_simul(d, ba_simul_);
} }
twa_graph_ptr
postprocessor::do_degen_tba(const twa_graph_ptr& a)
{
return degeneralize_tba(a,
degen_reset_, degen_order_,
degen_cache_, degen_lskip_,
degen_lowinit_, degen_remscc_);
}
twa_graph_ptr twa_graph_ptr
postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg)
{ {
...@@ -183,6 +193,33 @@ namespace spot ...@@ -183,6 +193,33 @@ namespace spot
if (type_ == BA || SBACC_) if (type_ == BA || SBACC_)
state_based_ = true; state_based_ = true;
bool want_parity = (type_ & Parity) == Parity;
auto finalize = [&](twa_graph_ptr tmp)
{
if (COMP_)
tmp = complete(tmp);
if (want_parity && tmp->acc().is_generalized_buchi())
tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp);
if (SBACC_)
tmp = sbacc(tmp);
if (want_parity)
{
parity_kind kind = parity_kind_any;
parity_style style = parity_style_any;
if ((type_ & ParityMin) == ParityMin)
kind = parity_kind_min;
else if ((type_ & ParityMax) == ParityMax)
kind = parity_kind_max;
if ((type_ & ParityOdd) == ParityOdd)
style = parity_style_odd;
else if ((type_ & ParityEven) == ParityEven)
style = parity_style_even;
change_parity_here(tmp, kind, style);
}
return tmp;
};
if (!a->is_existential() && if (!a->is_existential() &&
// We will probably have to revisit this condition later. // We will probably have to revisit this condition later.
// Currently, the intent is that postprocessor should never // Currently, the intent is that postprocessor should never
...@@ -191,7 +228,8 @@ namespace spot ...@@ -191,7 +228,8 @@ namespace spot
!(type_ == Generic && PREF_ == Any && level_ == Low)) !(type_ == Generic && PREF_ == Any && level_ == Low))
a = remove_alternation(a); a = remove_alternation(a);
if (type_ != Generic && !a->acc().is_generalized_buchi()) if ((type_ != Generic && !a->acc().is_generalized_buchi())
|| (want_parity && !a->acc().is_parity()))
{ {
a = to_generalized_buchi(a); a = to_generalized_buchi(a);
if (PREF_ == Any && level_ == Low) if (PREF_ == Any && level_ == Low)
...@@ -202,14 +240,9 @@ namespace spot ...@@ -202,14 +240,9 @@ namespace spot
&& (type_ == Generic && (type_ == Generic
|| type_ == TGBA || type_ == TGBA
|| (type_ == BA && a->is_sba()) || (type_ == BA && a->is_sba())
|| (type_ == Monitor && a->num_sets() == 0))) || (type_ == Monitor && a->num_sets() == 0)
{ || (want_parity && a->acc().is_parity())))
if (COMP_) return finalize(a);
a = complete(a);
if (SBACC_)
a = sbacc(a);
return a;
}
int original_acc = a->num_sets(); int original_acc = a->num_sets();
...@@ -244,20 +277,14 @@ namespace spot ...@@ -244,20 +277,14 @@ namespace spot
} }
a->remove_unused_ap(); a->remove_unused_ap();
} }
if (COMP_) return finalize(a);
a = complete(a);
return a;
} }
if (PREF_ == Any) if (PREF_ == Any)
{ {
if (type_ == BA) if (type_ == BA)
a = do_degen(a); a = do_degen(a);
if (COMP_) return finalize(a);
a = complete(a);
if (SBACC_)
a = sbacc(a);
return a;
} }
bool dba_is_wdba = false; bool dba_is_wdba = false;
...@@ -305,6 +332,8 @@ namespace spot ...@@ -305,6 +332,8 @@ namespace spot
// No need to do that if tba_determinisation_ will be used. // No need to do that if tba_determinisation_ will be used.
if (type_ == BA && !tba_determinisation_) if (type_ == BA && !tba_determinisation_)
sim = do_degen(sim); sim = do_degen(sim);
else if (want_parity && !sim->acc().is_parity())
sim = do_degen_tba(sim);
else if (SBACC_ && !tba_determinisation_) else if (SBACC_ && !tba_determinisation_)
sim = sbacc(sim); sim = sbacc(sim);
} }
...@@ -382,7 +411,7 @@ namespace spot ...@@ -382,7 +411,7 @@ namespace spot
} }
} }
if (PREF_ == Deterministic && type_ == Generic && !dba) if ((PREF_ == Deterministic && (type_ == Generic || want_parity)) && !dba)
{ {
dba = tgba_determinize(to_generalized_buchi(sim), dba = tgba_determinize(to_generalized_buchi(sim),
false, det_scc_, det_simul_, det_stutter_); false, det_scc_, det_simul_, det_stutter_);
...@@ -517,12 +546,6 @@ namespace spot ...@@ -517,12 +546,6 @@ namespace spot
sim = dba ? dba : sim; sim = dba ? dba : sim;
sim->remove_unused_ap(); sim->remove_unused_ap();
return finalize(sim);
if (COMP_)
sim = complete(sim);
if (SBACC_)
sim = sbacc(sim);
return sim;
} }
} }
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement // Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -72,7 +72,20 @@ namespace spot ...@@ -72,7 +72,20 @@ namespace spot
/// options used for debugging or benchmarking. /// options used for debugging or benchmarking.
postprocessor(const option_map* opt = nullptr); postprocessor(const option_map* opt = nullptr);
enum output_type { TGBA, BA, Monitor, Generic }; enum output_type { TGBA = 0,
BA = 1,
Monitor = 2,
Generic = 3,
Parity = 4,
ParityMin = Parity | 8,
ParityMax = Parity | 16,
ParityOdd = Parity | 32,
ParityEven = Parity | 64,
ParityMinOdd = ParityMin | ParityOdd,
ParityMaxOdd = ParityMax | ParityOdd,
ParityMinEven = ParityMin | ParityEven,
ParityMaxEven = ParityMax | ParityEven,
};
/// \brief Select the desired output type. /// \brief Select the desired output type.
/// ///
...@@ -96,11 +109,17 @@ namespace spot ...@@ -96,11 +109,17 @@ namespace spot
/// SystemC" (Deian Tabakov and Moshe Y. Vardi, Proceedings of /// SystemC" (Deian Tabakov and Moshe Y. Vardi, Proceedings of
/// RV’10, LNCS 6418). /// RV’10, LNCS 6418).
/// ///
/// Finally \c Generic remove all constraints about the acceptance /// \c Generic removes all constraints about the acceptance
/// condition. Using \c Generic can be needed to force the /// condition. Using \c Generic (or \c Parity below) can be
/// determinization of some automata (e.g., not all TGBA can be /// needed to force the determinization of some automata (e.g.,
/// degeneralized, using \c Generic will allow parity acceptance /// not all TGBA can be degeneralized, using \c Generic will allow
/// to be used instead). /// parity acceptance to be used instead).
///
/// \a Parity and its variants request the acceptance condition to
/// be of some parity type. Note that the determinization
/// algorithm used by Spot produces "parity min odd" acceptance,
/// but other parity types can be obtained from there by minor
/// adjustments.
/// ///
/// If set_type() is not called, the default \c output_type is \c TGBA. /// If set_type() is not called, the default \c output_type is \c TGBA.
void void
...@@ -195,6 +214,7 @@ namespace spot ...@@ -195,6 +214,7 @@ namespace spot
twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt);
twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt);
twa_graph_ptr do_degen(const twa_graph_ptr& input); twa_graph_ptr do_degen(const twa_graph_ptr& input);
twa_graph_ptr do_degen_tba(const twa_graph_ptr& input);
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg);
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a);
......
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 ## Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
## Laboratoire de Recherche et Développement de l'Epita (LRDE). ## de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
## Université Pierre et Marie Curie. ## Pierre et Marie Curie.
## ##
## This file is part of Spot, a model checking library. ## This file is part of Spot, a model checking library.
## ##
...@@ -310,6 +310,7 @@ TESTS_twa = \ ...@@ -310,6 +310,7 @@ TESTS_twa = \
core/dca.test \ core/dca.test \
core/dnfstreett.test \ core/dnfstreett.test \
core/parity.test \ core/parity.test \
core/parity2.test \
core/ltlsynt.test core/ltlsynt.test
############################## PYTHON ############################## ############################## PYTHON ##############################
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2018 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/>.
. ./defs
set -e
rm -rf res res2
for x in P 'Pmin odd' 'Pmax even'; do
ltl2tgba "-$x" FGa 'GFa & GFb' >>res
ltl2tgba FGa 'GFa & GFb' | autfilt --name=%M --high "-$x" >>res2
ltl2tgba -D "-$x" FGa 'GFa & GFb' >>res3
ltl2tgba FGa 'GFa & GFb' | autfilt -D --name=%M --high "-$x" >>res4
done
cat >expected<<EOF
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
--BODY--
State: 0
[t] 0
[0] 1
State: 1 {0}
[0] 1
--END--
HOA: v1
name: "G(Fa & Fb)"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {0}
[!1] 0
[!0&1] 1
State: 1
[0] 0 {0}
[!0] 1
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
--BODY--
State: 0
[t] 0
[0] 1
State: 1 {1}
[0] 1
--END--
HOA: v1
name: "G(Fa & Fb)"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {1}
[!1] 0
[!0&1] 1
State: 1
[0] 0 {1}
[!0] 1
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
--BODY--
State: 0
[t] 0
[0] 1
State: 1 {0}
[0] 1
--END--
HOA: v1
name: "G(Fa & Fb)"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {0}
[!1] 0
[!0&1] 1
State: 1
[0] 0 {0}
[!0] 1
--END--
EOF
diff expected res
diff expected res2
cat >expected2<<EOF
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 1 {1}
State: 1
[!0] 0 {0}
[0] 1 {1}
--END--
HOA: v1
name: "G(Fa & Fb)"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {0}
[!1] 0
[!0&1] 1
State: 1
[0] 0 {0}
[!0] 1
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 1 {1}
State: 1
[!0] 0 {0}
[0] 1 {1}
--END--
HOA: v1
name: "G(Fa & Fb)"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {1}
[!1] 0
[!<