Commit bd6dc7a8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

postproc: add support for colored-parity

* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Add support
for a colored option.
* bin/common_post.cc, bin/common_post.hh bin/autfilt.cc,
bin/ltl2tgba.cc, bin/dstar2tgba.cc: Add support for --colored-parity.
* bin/ltldo.cc: Adjust as well for consistency, even if --parity and
--colored-parity is not used here.
* tests/core/parity2.test: Add tests.
* doc/org/autfilt.org, doc/org/ltl2tgba.org: Add examples.
* NEWS: Mention --colored-parity.
parent 6bad8aeb
......@@ -47,10 +47,10 @@ New in spot 2.4.4.dev (net yet released)
- ltlsynt is a new tool for synthesizing a controller from LTL/PSL
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'.
- ltl2tgba, autfilt, and dstar2tgba have some new '--parity' and
'--colored-parity' options 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.
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -1540,8 +1540,8 @@ main(int argc, char** argv)
spot::srand(opt_seed);
spot::postprocessor post(&extra_options);
post.set_pref(pref | comp | sbacc);
post.set_type(type);
post.set_pref(pref | comp | sbacc | colored);
post.set_level(level);
autfilt_processor processor(post, o.dict);
......
......@@ -27,6 +27,7 @@ spot::postprocessor::output_type type = spot::postprocessor::TGBA;
spot::postprocessor::output_pref pref = spot::postprocessor::Small;
spot::postprocessor::output_pref comp = spot::postprocessor::Any;
spot::postprocessor::output_pref sbacc = spot::postprocessor::Any;
spot::postprocessor::output_pref colored = spot::postprocessor::Any;
spot::postprocessor::optimization_level level = spot::postprocessor::High;
bool level_set = false;
......@@ -60,6 +61,10 @@ static constexpr const argp_option options[] =
"any|min|max|odd|even|min odd|min even|max odd|max even",
OPTION_ARG_OPTIONAL,
"automaton with parity acceptance", 0, },
{ "colored-parity", 'p',
"any|min|max|odd|even|min odd|min even|max odd|max even",
OPTION_ARG_OPTIONAL,
"colored automaton with parity acceptance", 0, },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 },
......@@ -111,9 +116,13 @@ static const argp_option options_disabled[] =
"define the acceptance using states", 0 },
{ "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "parity", 'P',
"[any|min|max|odd|even|min odd|min even|max odd|max even]",
"any|min|max|odd|even|min odd|min even|max odd|max even",
OPTION_ARG_OPTIONAL,
"automaton with parity acceptance", 0, },
{ "colored-parity", 'p',
"any|min|max|odd|even|min odd|min even|max odd|max even",
OPTION_ARG_OPTIONAL,
"colored automaton with parity acceptance", 0, },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 },
......@@ -143,6 +152,7 @@ parse_opt_post(int key, char* arg, struct argp_state*)
break;
case 'B':
type = spot::postprocessor::BA;
colored = spot::postprocessor::Any;
break;
case 'C':
comp = spot::postprocessor::Complete;
......@@ -153,11 +163,14 @@ parse_opt_post(int key, char* arg, struct argp_state*)
break;
case 'G':
type = spot::postprocessor::Generic;
colored = spot::postprocessor::Any;
break;
case 'M':
type = spot::postprocessor::Monitor;
colored = spot::postprocessor::Any;
break;
case 'P':
case 'p':
{
static char const *const parity_args[] =
{
......@@ -186,9 +199,12 @@ parse_opt_post(int key, char* arg, struct argp_state*)
};
ARGMATCH_VERIFY(parity_args, parity_types);
if (arg)
type = XARGMATCH("--parity", arg, parity_args, parity_types);
type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity",
arg, parity_args, parity_types);
else
type = spot::postprocessor::Parity;
if (key == 'p')
colored = spot::postprocessor::Colored;
}
break;
case 'S':
......@@ -217,6 +233,7 @@ parse_opt_post(int key, char* arg, struct argp_state*)
if (automaton_format == Spin)
error(2, 0, "--spin and --tgba are incompatible");
type = spot::postprocessor::TGBA;
colored = spot::postprocessor::Any;
break;
default:
return ARGP_ERR_UNKNOWN;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -31,6 +31,7 @@ extern spot::postprocessor::output_type type;
extern spot::postprocessor::output_pref pref;
extern spot::postprocessor::output_pref comp;
extern spot::postprocessor::output_pref sbacc;
extern spot::postprocessor::output_pref colored;
extern spot::postprocessor::optimization_level level;
// True if --low, --medium, or --high has been given
extern bool level_set;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -147,7 +147,7 @@ main(int argc, char** argv)
check_no_automaton();
spot::postprocessor post(&extra_options);
post.set_pref(pref | comp | sbacc);
post.set_pref(pref | comp | sbacc | colored);
post.set_type(type);
post.set_level(level);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -176,8 +176,8 @@ main(int argc, char** argv)
try
{
spot::translator trans(&extra_options);
trans.set_pref(pref | comp | sbacc | unambig);
trans.set_type(type);
trans.set_pref(pref | comp | sbacc | unambig | colored);
trans.set_level(level);
trans_processor processor(trans);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -466,7 +466,7 @@ main(int argc, char** argv)
setup_sig_handler();
spot::postprocessor post;
post.set_pref(pref | comp | sbacc);
post.set_pref(pref | comp | sbacc | colored);
post.set_type(type);
post.set_level(level);
......
......@@ -11,7 +11,7 @@ The tool operates a loop over 5 phases:
- optionally preprocess the automaton
- optionally filter the automaton (i.e., decide whether to ignore the
automaton or continue with it)
- optionally postprocess the automaton
- optionally postprocess the automaton (to simply it or change its acceptance)
- output the automaton
The simplest way to use the tool is simply to use it for input and
......@@ -242,14 +242,20 @@ This set of options controls the desired type of output automaton:
autfilt --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
: -B, --ba Büchi Automaton (with state-based acceptance)
: -C, --complete output a complete automaton
: -G, --generic any acceptance is allowed (default)
: -M, --monitor Monitor (accepts all finite prefixes of the given
: property)
: -S, --state-based-acceptance, --sbacc
: define the acceptance using states
: --tgba Transition-based Generalized Büchi Automaton
#+begin_example
-B, --ba Büchi Automaton (with state-based acceptance)
-C, --complete output a complete automaton
-G, --generic any acceptance is allowed (default)
-M, --monitor Monitor (accepts all finite prefixes of the given
property)
-p, --colored-parity[=any|min|max|odd|even|min odd|min even|max odd|max
even] colored automaton with parity acceptance
-P, --parity[=any|min|max|odd|even|min odd|min even|max odd|max even]
automaton with parity acceptance
-S, --state-based-acceptance, --sbacc
define the acceptance using states
--tgba Transition-based Generalized Büchi Automaton
#+end_example
These options specify any simplification goal:
......@@ -286,10 +292,11 @@ if you want to try to make (or keep) it deterministic use
Note that the =--deterministic= flag has two possible behaviors
depending on the constraints on the acceptance conditions:
- When =autfilt= is configured to work with generic acceptance (the
=--generic= option, which is the default), then the
=--deterministic= flag will do whatever it takes to output a
deterministic automaton, and this includes changing the acceptance
condition if needed (see below).
=--generic= option, which is the default) or parity acceptance
(using =--parity= or =--colored-parity=), then the =--deterministic=
flag will do whatever it takes to output a deterministic automaton,
and this includes changing the acceptance condition if needed (see
below).
- If options =--tgba= or =--ba= are used, the =--deterministic= option
is taken as a /preference/: =autfilt= will try to favor determinism
in the output, but it may not always succeed and may output
......@@ -319,10 +326,15 @@ attempted on any supplied automaton. (It's even attempted for
deterministic automata, because that might reduce them.)
If that first procedure failed, and the input automaton is not
deterministic and =--generic= (the default for =autfilt=) is used,
then the second procedure is used. In this case, automata will be
first converted to transition-based Büchi automata if their condition
is more complex.
deterministic and =--generic= (the default for =autfilt=), =--parity=
or =--colorized-parity= is used, then the second procedure is used.
In this case, automata will be first converted to transition-based
Büchi automata if their acceptance condition is more complex.
The difference between =--parity= and =--colored-parity= parity is
that the latter requests all transitions (or all states when
state-based acceptance is used) to belong to exactly one acceptance
set.
* Transformations
......
......@@ -16,10 +16,12 @@ a quick summary:
- =--tgba= (the default) outputs Transition-based Generalized Büchi
Automata
- =--ba= (or =-B=) outputs state-based Büchi automata
- =--monitor= (or =-M=) outputs Monitors
- =--generic --deterministic= (or =-GD=) will do whatever it takes to
- =--monitor= (or =-M=) outputs monitors
- =--generic --deterministic= (or =-DG=) will do whatever it takes to
produce a deterministic automaton, and may output generalized Büchi,
or parity acceptance.
- =--parity --deterministic= (or =-DP=) will produce a deterministic
automaton with parity acceptance.
* TGBA and BA
......@@ -716,7 +718,7 @@ to experiment with the different settings on a small version of the
pattern, and select the lowest setting that satisfies your
expectations.
* Deterministic automata with =--generic=
* Deterministic automata with =--generic --deterministic=
:PROPERTIES:
:CUSTOM_ID: generic
:END:
......@@ -793,6 +795,127 @@ ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d.a
#+RESULTS:
[[file:ltl2tgba-det2.svg]]
While the =--generic= option currently only builds automata with
generalized-Büchi or parity acceptance, this is very likely to change
in the future.
* Deterministic automata with =--parity --deterministic=
Using the =--parity= (or upper-case =-P=) option will force the
acceptance condition to be of a parity type. This has to be
understood in the sense of the HOA format, where:
- multiple parity types are defined (=min odd n=, =min even n=, =max
odd n=, and =max even n= where =n= is the number of acceptance
sets), and
- the parity acceptance is only a type of acceptance condition, i.e.,
a formula expressed in terms of acceptance sets, and does not have
additional constraints on these sets. In particular it is not
necessary the case that each transition or state belongs to exactly
one acceptance set (this is the "colored" property, see below).
Under these assumptions, Büchi acceptance is just one kind of parity
(in HOA =Buchi= is equivalent to =parity max even 1= or =parity min
even 1=), Rabin with one pair is also a parity acceptance (=Rabin 1=
is equivalent to =parity min odd 2=), and Streett with one pair as
well (=Streett 1= is equivalent to =parity max odd 2=).
In the current implementation, using =ltl2tgba --parity= (without
=--deterministic=) will always produce a Büchi automaton, and when
=--deterministic= (or =-D=) is added, it will produce an deterministic
automaton with Büchi acceptance (=parity min even 1=) or with =parity
min odd n= acceptance, because the latter is the type of parity
acceptance that our determinization procedure outputs.
For instance, =FGa= gets translated into an automaton with =Rabin 1=
acceptance (another name for =parity min odd 2=):
#+NAME: ltl2tgba-dp1
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "FGa" -D -P -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-dp1.svg :var txt=ltl2tgba-dp1 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-dp1.svg]]
And =GFa & GFb= gets translated into a =Büchi= automaton (another name
for =parity min even 1=):
#+NAME: ltl2tgba-dp2
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "GFa & GFb" -D -P -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-dp2.svg :var txt=ltl2tgba-dp2 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-dp2.svg]]
If we really want to use the same style of parity acceptance for all outputs,
we can specify it as an argument to the =--parity= option. For instance
#+NAME: ltl2tgba-dp3
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "GFa & GFb" -D -P'min odd' -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-dp3.svg :var txt=ltl2tgba-dp3 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-dp3.svg]]
The =--colored-parity= (or lower-case =-p=) option works similarly to
=--parity=, but additionally requests that the automaton be colored.
I.e., each transition (or state if state-based acceptance is
requested) should belong to exactly one acceptance set.
#+NAME: ltl2tgba-dp4
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "GFa & GFb" -D -p -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-dp4.svg :var txt=ltl2tgba-dp4 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-dp4.svg]]
#+NAME: ltl2tgba-dp5
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "GFa & GFb" -D -p'min odd' -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-dp5.svg :var txt=ltl2tgba-dp5 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-dp5.svg]]
Note that all these options can be combined with state-based
acceptance if needed:
#+NAME: ltl2tgba-dp6
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "GFa & GFb" -D -S -p'max even' -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-dp6.svg :var txt=ltl2tgba-dp6 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-dp6.svg]]
* Translating multiple formulas for statistics
If multiple formulas are given to =ltl2tgba=, the corresponding
......
......@@ -180,6 +180,7 @@ namespace spot
#define PREF_ (pref_ & (Small | Deterministic))
#define COMP_ (pref_ & Complete)
#define SBACC_ (pref_ & SBAcc)
#define COLORED_ (pref_ & Colored)
twa_graph_ptr
postprocessor::run(twa_graph_ptr a, formula f)
......@@ -194,6 +195,9 @@ namespace spot
state_based_ = true;
bool want_parity = (type_ & Parity) == Parity;
if (COLORED_ && !want_parity)
throw std::runtime_error("postprocessor: the Colored setting only works "
"for parity acceptance");
auto finalize = [&](twa_graph_ptr tmp)
{
......@@ -205,6 +209,8 @@ namespace spot
tmp = sbacc(tmp);
if (want_parity)
{
if (COLORED_)
colorize_parity_here(tmp);
parity_kind kind = parity_kind_any;
parity_style style = parity_style_any;
if ((type_ & ParityMin) == ParityMin)
......
......@@ -136,6 +136,7 @@ namespace spot
Complete = 4,
SBAcc = 8, // State-based acceptance.
Unambiguous = 16,
Colored = 32, // Colored parity; requires parity acceptance
};
typedef int output_pref;
......@@ -163,7 +164,9 @@ namespace spot
///
/// The above options can be combined with \c Complete and \c
/// SBAcc, to request a complete automaton, and an automaton with
/// state-based acceptance.
/// state-based acceptance. Automata with parity acceptance may
/// also be required to be \c Colored, ensuring that each
/// transition (or state) belong to exactly one acceptance set.
///
/// Note 1: the \c Unambiguous option is not actually supported by
/// spot::postprocessor; it is only honored by spot::translator.
......
......@@ -23,7 +23,7 @@ set -e
rm -rf res res2
for x in P 'Pmin odd' 'Pmax even'; do
for x in P 'Pmin odd' 'Pmax even' 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
......@@ -133,6 +133,108 @@ State: 1
[0] 0 {0}
[!0] 1
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels state-acc colored
properties: stutter-invariant inherently-weak
--BODY--
State: 0 {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: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {1}
[!1] 0 {0}
[!0&1] 1 {0}
State: 1
[0] 0 {1}
[!0] 1 {0}
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels state-acc colored
properties: stutter-invariant inherently-weak
--BODY--
State: 0 {2}
[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: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {1}
[!1] 0 {2}
[!0&1] 1 {2}
State: 1
[0] 0 {1}
[!0] 1 {2}
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: parity max even 3
Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))
properties: trans-labels explicit-labels state-acc colored
properties: stutter-invariant inherently-weak
--BODY--
State: 0 {1}
[t] 0
[0] 1
State: 1 {2}
[0] 1
--END--
HOA: v1
name: "G(Fa & Fb)"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: parity max even 3
Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {2}
[!1] 0 {1}
[!0&1] 1 {1}
State: 1
[0] 0 {2}
[!0] 1 {1}
--END--
EOF
diff expected res
......@@ -244,9 +346,115 @@ State: 1
[0] 0 {0}
[!0] 1
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0 {2}
[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: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {1}
[!1] 0 {0}
[!0&1] 1 {0}
State: 1
[0] 0 {1}
[!0] 1 {0}
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0 {2}
[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: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {1}
[!1] 0 {2}
[!0&1] 1 {2}
State: 1
[0] 0 {1}
[!0] 1 {2}
--END--
HOA: v1
name: "FGa"
States: 2
Start: 0
AP: 1 "a"
acc-name: parity max even 4
Acceptance: 4 Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0