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

hierarchy: add a new way to check DBA-realizability via DPA

* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here.
* tests/core/hierarchy.test: Test it.
* bin/man/spot-x.x: Document SPOT_PR_CHECK.
* doc/org/hierarchy.org, NEWS: Update.
parent 2617c17b
Pipeline #9944 failed with stages
in 135 minutes and 56 seconds
......@@ -24,6 +24,12 @@ New in spot 2.7.5.dev (not yet released)
- genaut learned --m-nba=N to generate Max Michel's NBA familly.
(NBAs with N+1 states whose determinized have at least N! states.)
- Due to some new simplification of parity acceptance, the output of
"ltl2tgba -P -D" is now using a minimal number of colors. This
means that recurrence properties have an acceptance condition
amongst "Inf(0)", "t", or "f", and persistance properties have an
acceptance condition among "Fin(0)", "t", or "f".
Library:
- Add generic_accepting_run() as a variant of generic_emptiness_check() that
......@@ -117,6 +123,13 @@ New in spot 2.7.5.dev (not yet released)
- The postprocessor and translator classes are now using
reduce_parity() for further simplifications.
- The code for checking recurrence/persistence properties can also
use the fact the reduce_parity() with return "Inf(0)" (or "t" or
"f") for deterministic automata corresponding to recurrence
properties, and "Fin(0)" (or "t" or "f") for persistence
properties. This can be altered with the SPOT_PR_CHECK
environment variable.
New in spot 2.7.5 (2019-06-05)
Build:
......
......@@ -132,8 +132,8 @@ ignoring them), and setting this variable will interfer with that.
.TP
\fBSPOT_PR_CHECK\fR
Select the default algorithm that must be used to check the persistence
or recurrence property of a formula f. The values it can take are 1
or 2. Both methods work either on f or !f thanks to the duality of
or recurrence property of a formula f. The values it can take are between
1 and 3. All methods work either on f or !f thanks to the duality of
persistence and recurrence classes. See
.UR https://spot.lrde.epita.fr/hierarchy.html
this page
......@@ -145,8 +145,13 @@ for more details. If it is set to:
It will try to check if f (or !f) is co-Büchi realizable in order to
tell if f belongs to the persistence (or the recurrence) class.
.IP 2
It checks if f (or !f) is det-Büchi realizable to tell if f belongs
to the recurrence (or the persistence) class.
It checks if f (or !f) is det-Büchi realizable via a reduction
to deterministic-Rabin in order to tell if f belongs to the
recurrence (or the persistance) class.
.IP 3
It checks if f (or !f) is det-Büchi realizable via a reduction
to deterministic-parity in order to tell if f belongs to the
recurrence (or the persistance) class.
.RE
.RE
......
......@@ -520,7 +520,7 @@ automata.
For the subclass of /obligation/ properties, using =-D= is a sure way
to obain a deterministic automaton (and even a minimal one), but for
the /recurrence/ properties that are not /obligations/ the translator
does not make any special effort to produce deterministic automata,
does not make /too much/ effort to produce deterministic automata,
even with =-D= (this might change in the future).
All properties that are not in the /persistence/ class (this includes
......@@ -585,106 +585,40 @@ $txt
[[file:hier-recurrence-3.svg]]
One way to obtain a deterministic Büchi automaton (it has to exist, since this is
a /recurrence/ property), is to chain a few algorithms implemented in Spot:
1. Determinize the non-deterministic automaton to obtain a
deterministic automaton with parity acceptance: this is done by
using =ltl2tgba -P -D=, with option =-P= indicating that parity
acceptance is desired.
#+NAME: hier-recurrence-4
#+BEGIN_SRC sh :exports code
ltl2tgba -P -D 'G(Gb | Fa)' -d
#+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-recurrence-4.svg]]
2. Transform the parity acceptance into Rabin acceptance: this is
done with =autfilt --generalized-rabin=. Because of the type of
parity acceptance used, the result will actually be Rabin and not
generalized Rabin.
#+NAME: hier-recurrence-5
#+BEGIN_SRC sh :exports code
ltl2tgba -P -D 'G(Gb | Fa)' |
autfilt --generalized-rabin -d
#+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-recurrence-5.svg]]
(The only change here is in the acceptance condition.)
3. In step 4 we are going to convert the automaton to state-based
Büchi, and this sometimes works better if the input Rabin automaton
also uses state-based acceptance. So let us add =-S= to the
previous command:
#+NAME: hier-recurrence-6
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -P -D 'G(Gb | Fa)' |
autfilt -S --generalized-rabin -d
#+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-6.svg :var txt=hier-recurrence-6 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-recurrence-6.svg]]
4. Finally, convert the resulting automaton to BA, using =autfilt
-B=. Spot can convert automata with any acceptance condition to
BA, but when the input is a deterministic Rabin automaton, it uses
a dedicated algorithm that preserves determinism whenever possible
(and we know it is possible, because we are working on a
recurrence formula). Adding =-D= here to suggest that we are
trying to obtain a deterministic automaton does not hurt, as it
will enable simplifications as a side-effect (without =-D= we
simply get a larger deterministic automaton).
#+NAME: hier-recurrence-7
#+BEGIN_SRC sh :exports code
ltl2tgba -P -D 'G(Gb | Fa)' |
autfilt -S --generalized-rabin |
autfilt -B -D -d
#+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-7.svg :var txt=hier-recurrence-7 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-recurrence-7.svg]]
Here we are lucky that the deterministic Büchi automaton is even
smaller than the original non-deterministic version. As said earlier,
passing =-S= to the first =autfilt= was optional, but in this case it
helps producing a smaller automaton. Here is what we get without it:
#+NAME: hier-recurrence-8
a /recurrence/ property), is to request a deterministic automaton with parity
acceptance using =-P=. The number of color output with =-P= is always reduced
to the minimal number possible, so for a /recurrence/ property the output
automaton can only have one of three possible acceptance: =Inf(0)=, =t=, or =f=.
#+NAME: hier-recurrence-4
#+BEGIN_SRC sh :exports code
ltl2tgba -P -D 'G(Gb | Fa)' |
autfilt --generalized-rabin |
autfilt -B -D -d
ltl2tgba -P -D 'G(Gb | Fa)' -d
#+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-8.svg :var txt=hier-recurrence-8 :exports results
#+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-recurrence-4.svg]]
Note that if the acceptance is =t=, the property is a monitor, and if
its =f=, the property is =false=. In any way, if you would like to
obtain a DBA for any recurrent property, a sure way to avoid these
difference is to pipe the result through =autfilt -B=
#+NAME: hier-recurrence-5
#+BEGIN_SRC sh :exports code
ltl2tgba -P -D 'G(Gb | Fa)' | autfilt -B -d
#+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-recurrence-8.svg]]
[[file:hier-recurrence-5.svg]]
It is likely that =ltl2tgba -B -D= will implement all this processing
chain in the future, but so originally =-D= was only expressing a
preference not a requirement.
It is likely that =ltl2tgba -B -D= will implement these steps in the
future, but so originally =-D= was only expressing a preference not a
requirement.
** Persistence
......@@ -725,8 +659,9 @@ $txt
Note that in this example, we know that =GFa= is trivial enough that
=ltl2tgba -D GFa= will generate a deterministic automaton. In the
general case we might have to determinize the automaton as we did in
the previous section (we will do it again below).
general case we might have to determinize the automaton using =-P -D= as
we did in the previous section. For persistence properties, =-P -D= should
return an automaton whose acceptance is one of =Fin(0)=, =t=, or =f=.
/Persistence/ properties can be represented by weak Büchi automata.
The translator is aware of that, so when it detects that the input
......@@ -739,10 +674,8 @@ optimization is simply not applied.)
If the input is a weak property that is not syntactically weak, the
output will not necessarily be weak. One costly way to obtain a weak
automaton for a formula $\varphi$ would be to first compute a
deterministic Büchi automaton of the recurrence $\lnot\varphi$ then
complement the acceptance of the resulting automaton, yielding a
deterministic co-Büchi automaton, and then transform that into a Büchi
automaton.
deterministic co-Büchi automaton $\varphi$ then transform that into a
Büchi automaton.
Let's do that on the persistence formula =F(G!a | G(b U a))=, just for
the fun of it.
......@@ -766,15 +699,11 @@ $txt
#+RESULTS:
[[file:hier-persistence-3.svg]]
Furthermore it appears that =ltl2tgba -D= does generate a deterministic
Büchi automaton for the complement, instead we get a non-deterministic
generalized Büchi automaton:
So let's determinize using parity acceptance:
#+NAME: hier-persistence-4
#+BEGIN_SRC sh :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
ltl2tgba -D |
autfilt --highlight-nondet=5 -d
ltl2tgba -P -D 'F(G!a | G(b U a))' -d
#+END_SRC
#+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results
$txt
......@@ -783,58 +712,16 @@ $txt
#+RESULTS:
[[file:hier-persistence-4.svg]]
So let us use the same tricks as in the previous section,
determinizing this automaton into a Rabin automaton, and then back to
deterministic Büchi:
#+NAME: hier-persistence-5
#+BEGIN_SRC sh :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
ltl2tgba -P -D |
autfilt --generalized-rabin |
autfilt --tgba -D -d
#+END_SRC
#+BEGIN_SRC dot :file hier-persistence-5.svg :var txt=hier-persistence-5 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-persistence-5.svg]]
This is a deterministic Büchi automaton for the negation of our formula.
Now we can complement it to obtain a deterministic co-Büchi automaton for =F(G!a | G(b U a))=:
#+NAME: hier-persistence-6
#+BEGIN_SRC sh :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
ltl2tgba -P -D |
autfilt --generalized-rabin |
autfilt --tgba -D |
autfilt --complement -d
#+END_SRC
#+BEGIN_SRC dot :file hier-persistence-6.svg :var txt=hier-persistence-6 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-persistence-6.svg]]
And finally we convert the result back to Büchi:
And finally we convert the result back to Büchi with =autfilt -B=.
#+NAME: hier-persistence-7
#+BEGIN_SRC sh :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
ltl2tgba -P -D |
autfilt --generalized-rabin |
autfilt --tgba -D |
autfilt --complement -B -d
ltl2tgba -P -D 'F(G!a | G(b U a))' | autfilt -B --highlight-nondet --small -d
#+END_SRC
#+BEGIN_SRC dot :file hier-persistence-7.svg :var txt=hier-persistence-7 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:hier-persistence-7.svg]]
That is indeed, a weak automaton.
That is indeed, a weak non-deterministic automaton.
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -65,79 +65,91 @@ namespace spot
return !cobuchi->intersects(not_aut);
}
[[noreturn]] static void invalid_spot_pr_check()
{
throw std::runtime_error("invalid value for SPOT_PR_CHECK "
"(should be 1, 2, or 3)");
}
static prcheck
algo_to_perform(bool is_persistence, bool aut_given)
{
static unsigned value = [&]()
{
int val;
try
{
auto s = getenv("SPOT_PR_CHECK");
val = s ? std::stoi(s) : 0;
}
catch (const std::exception& e)
{
invalid_spot_pr_check();
}
if (val < 0 || val > 3)
invalid_spot_pr_check();
return val;
}();
switch (value)
{
case 0:
if (aut_given && !is_persistence)
return prcheck::via_Parity;
else
return prcheck::via_CoBuchi;
case 1:
return prcheck::via_CoBuchi;
case 2:
return prcheck::via_Rabin;
case 3:
return prcheck::via_Parity;
default:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
return prcheck::via_Parity;
}
static bool
detbuchi_realizable(const twa_graph_ptr& aut)
{
if (is_universal(aut))
return true;
// if aut is a non-deterministic TGBA, we do
// TGBA->DPA->DRA->(D?)BA. The conversion from DRA to
// BA will preserve determinism if possible.
bool want_old = algo_to_perform(false, true) == prcheck::via_Rabin;
if (want_old)
{
// if aut is a non-deterministic TGBA, we do
// TGBA->DPA->DRA->(D?)BA. The conversion from DRA to
// BA will preserve determinism if possible.
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low);
auto dpa = p.run(aut);
if (dpa->acc().is_generalized_buchi())
{
assert(is_deterministic(dpa));
return true;
}
else
{
auto dra = to_generalized_rabin(dpa);
return rabin_is_buchi_realizable(dra);
}
}
// Converting reduce_parity() will produce a Büchi automaton (or
// an automaton with "t" or "f" acceptance) if the parity
// automaton is DBA-realizable.
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_type(spot::postprocessor::Parity);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low);
auto dpa = p.run(aut);
if (dpa->acc().is_generalized_buchi())
{
assert(is_deterministic(dpa));
return true;
}
else
{
auto dra = to_generalized_rabin(dpa);
return rabin_is_buchi_realizable(dra);
}
return dpa->acc().is_f() || dpa->acc().is_generalized_buchi();
}
}
[[noreturn]] static void invalid_spot_pr_check()
{
throw std::runtime_error("invalid value for SPOT_PR_CHECK "
"(should be 1 or 2)");
}
static prcheck
algo_to_perform(bool is_persistence, bool aut_given)
{
static prcheck env_algo = [&]()
{
int val;
try
{
auto s = getenv("SPOT_PR_CHECK");
val = s ? std::stoi(s) : 0;
}
catch (const std::exception& e)
{
invalid_spot_pr_check();
}
if (val == 0)
{
if (aut_given && !is_persistence)
return prcheck::via_Rabin;
else if (is_persistence || !aut_given)
return prcheck::via_CoBuchi;
else
SPOT_UNREACHABLE();
}
else if (val == 1)
{
return prcheck::via_CoBuchi;
}
else if (val == 2)
{
return prcheck::via_Rabin;
}
else
{
invalid_spot_pr_check();
}
}();
return env_algo;
}
bool
is_persistence(formula f, twa_graph_ptr aut, prcheck algo)
{
......@@ -161,6 +173,7 @@ namespace spot
ltl_to_tgba_fm(f, make_bdd_dict(), true));
case prcheck::via_Rabin:
case prcheck::via_Parity:
return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f),
make_bdd_dict(), true));
......@@ -195,6 +208,7 @@ namespace spot
make_bdd_dict(), true));
case prcheck::via_Rabin:
case prcheck::via_Parity:
return detbuchi_realizable(aut ? aut :
ltl_to_tgba_fm(f, make_bdd_dict(), true));
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -37,6 +37,9 @@ namespace spot
///
/// If PR_via_CoBuchi, they will check if the formula is cobuchi_realizable.
///
/// If PR_via_Parity, they will check if the formula is
/// detbuchi/cobuchi-realizable by calling reduce_parity() on a DPA.
///
/// Note that is_persistence() and is_recurrence() will work on a formula f
/// or its negation because of the duality of both classes
/// (see https://spot.lrde.epita.fr/hierarchy.html for details).
......@@ -47,6 +50,7 @@ namespace spot
Auto,
via_CoBuchi,
via_Rabin,
via_Parity,
};
/// \ingroup tl_hier
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -70,31 +70,33 @@ ltlfilt -q --safety --guarantee -f '(Gb R (b xor Gb)) W (a W Xa)'
# make sure SPOT_PR_CHECK is read.
randltl -n -1 a b c | ltlfilt -v --syntactic-safety --syntactic-guarantee \
--syntactic-obligation --syntactic-recurrence --syntactic-persistence \
-n 100 > res
cat res | SPOT_PR_CHECK=x ltlfilt --recurrence 2>err && exit 1
cat res | SPOT_PR_CHECK=9 ltlfilt --recurrence 2>err && exit 1
-n 500 > res
SPOT_PR_CHECK=x ltlfilt res --recurrence 2>err && exit 1
SPOT_PR_CHECK=9 ltlfilt res --recurrence 2>err && exit 1
grep SPOT_PR_CHECK err
# Testing Recurrence.
cat res | ltlfilt --recurrence > r0
for i in 1 2; do
cat res | SPOT_PR_CHECK=$i ltlfilt --recurrence > r$i
ltlfilt res --recurrence > r0
for i in 1 2 3; do
SPOT_PR_CHECK=$i ltlfilt res --recurrence > r$i
done
diff r0 r2
diff r1 r2
cat res | ltlfilt -o %h.ltl
diff r2 r3
ltlfilt res -o %h.ltl
cat R.ltl O.ltl G.ltl S.ltl B.ltl | sort > rogsb.ltl
sort r2 > r3
diff r3 rogsb.ltl
# Testing Persistence.
cat res | ltlfilt --persistence > p0
for i in 1 2; do
cat res | SPOT_PR_CHECK=$i ltlfilt --persistence > p$i
ltlfilt res --persistence > p0
for i in 1 2 3; do
SPOT_PR_CHECK=$i ltlfilt res --persistence > p$i
done
diff p0 p2
diff p1 p2
cat res | ltlfilt -o %h.ltl
diff p2 p3
ltlfilt res -o %h.ltl
cat P.ltl O.ltl G.ltl S.ltl B.ltl | sort > pogsb.ltl
sort p2 > p3
diff p3 pogsb.ltl
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment