twaalgos/cobuchi: Add dnf_to_nca() method
* NEWS: Update. * spot/twaalgos/cobuchi.hh: Declare dnf_to_nca(). * spot/twaalgos/cobuchi.cc: Implement it. * tests/core/dca.test: Add tests.
This commit is contained in:
Alexandre GBAGUIDI AISSE
parent
50e99cdca7
commit
f2616069be
4 changed files with 343 additions and 12 deletions
15
NEWS
15
NEWS
|
|
@ -23,18 +23,19 @@ New in spot 2.4.0.dev (not yet released)
|
|||
specified SCC. It must only be called on automata with a
|
||||
Streett-like acceptance condition.
|
||||
|
||||
- The new function nsa_to_nca() is able to convert when possible an
|
||||
automaton with a Streett-like acceptance to an equivalent
|
||||
automaton with a co-Büchi acceptance. Actually the resulting
|
||||
automaton will always recognize at least the same language. It can
|
||||
recognize more if the original language can not be expressed with
|
||||
a co-Büchi acceptance condition.
|
||||
|
||||
- The new function dnf_to_streett() is able to convert any automaton
|
||||
with an acceptance condition in Disjunctive Normal Form to a
|
||||
Streett-like automaton. This is used by the new option
|
||||
'--streett-like' of autfilt.
|
||||
|
||||
- The new functions nsa_to_nca() and nra_to_nca() are able to convert
|
||||
when possible respectively an automaton with a Streett-like
|
||||
acceptance or a Rabin-like acceptance to an equivalent automaton
|
||||
with a co-Büchi acceptance. Actually the resulting automaton will
|
||||
always recognize at least the same language. It can recognize more
|
||||
if the original language can not be expressed with a co-Büchi
|
||||
acceptance condition.
|
||||
|
||||
Deprecation notices:
|
||||
|
||||
(These functions still work but compilers emit warnings.)
|
||||
|
|
|
|||
|
|
@ -28,6 +28,13 @@
|
|||
#include <stack>
|
||||
#include <unordered_map>
|
||||
|
||||
#define DEBUG 0
|
||||
#if DEBUG
|
||||
#define debug std::cerr
|
||||
#else
|
||||
#define debug while (0) std::cout
|
||||
#endif
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
|
|
@ -249,14 +256,45 @@ namespace spot
|
|||
}
|
||||
|
||||
|
||||
twa_graph_ptr
|
||||
dnf_to_nca(const const_twa_graph_ptr& ref,
|
||||
bool named_states,
|
||||
vect_nca_info* nca_info)
|
||||
{
|
||||
const acc_cond::acc_code& code = ref->get_acceptance();
|
||||
if (!code.is_dnf())
|
||||
throw std::runtime_error("dnf_to_nca() only works with DNF acceptance "
|
||||
"condition");
|
||||
|
||||
auto streett_aut = spot::dnf_to_streett(ref, true);
|
||||
|
||||
std::vector<acc_cond::rs_pair> pairs;
|
||||
if (!streett_aut->acc().is_streett_like(pairs))
|
||||
throw std::runtime_error("dnf_to_nca() could not convert the original "
|
||||
"automaton into an intermediate Streett-like automaton");
|
||||
|
||||
nsa_to_nca_converter nca_converter(streett_aut,
|
||||
ref,
|
||||
pairs,
|
||||
named_states,
|
||||
true,
|
||||
ref->num_states());
|
||||
return nca_converter.run(nca_info);
|
||||
}
|
||||
|
||||
|
||||
twa_graph_ptr
|
||||
to_dca(const const_twa_graph_ptr& aut, bool named_states)
|
||||
{
|
||||
const acc_cond::acc_code& code = aut->get_acceptance();
|
||||
|
||||
std::vector<acc_cond::rs_pair> pairs;
|
||||
if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity())
|
||||
return nsa_to_nca(aut, named_states);
|
||||
else if (code.is_dnf())
|
||||
return dnf_to_nca(aut, named_states);
|
||||
else
|
||||
throw std::runtime_error("to_dca() only works with Streett-like or Parity"
|
||||
" acceptance condition");
|
||||
throw std::runtime_error("to_dca() only works with Streett-like, Parity "
|
||||
"or any acceptance condition in DNF");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,9 +26,10 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// A vector of nca_st_info is given as argument to nsa_to_nca(). Each
|
||||
/// nca_st_info has information about a state that must be seen infinitely
|
||||
/// often. For a state 's' visited infinitely often by a run, the information
|
||||
/// A vector of nca_st_info is given as argument to nsa_to_nca() or
|
||||
/// dnf_to_nca(). Each nca_st_info has information about a state that must be
|
||||
/// seen infinitely often.
|
||||
/// For a state 's' visited infinitely often by a run, the information
|
||||
/// provided is:
|
||||
/// - the clause number satisfied by the run (from left to right)
|
||||
/// - the state number of 's'
|
||||
|
|
@ -81,6 +82,31 @@ namespace spot
|
|||
bool named_states = false,
|
||||
vect_nca_info* nca_info = nullptr);
|
||||
|
||||
/// \brief Converts an aut. with acceptance in DNF to a nondet. co-Büchi aut.
|
||||
///
|
||||
/// This function converts the Rabin-like automaton into a Strett-like
|
||||
/// automaton and then calls nsa_to_nca() on it. It is described in section
|
||||
/// 3.2 of:
|
||||
/** \verbatim
|
||||
@Article{boker.2009.lcs,
|
||||
author = {Udi Boker and Orna Kupferman},
|
||||
title = {Co-Büching Them All},
|
||||
booktitle = {Foundations of Software Science and Computational
|
||||
Structures - 14th International Conference, FOSSACS 2011}
|
||||
year = {2011},
|
||||
pages = {184--198},
|
||||
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
|
||||
}
|
||||
\endverbatim */
|
||||
///
|
||||
/// \a aut The automaton to convert.
|
||||
/// \a named_states name each state for easier debugging.
|
||||
/// \a nca_info retrieve information about state visited infinitely often.
|
||||
SPOT_API twa_graph_ptr
|
||||
dnf_to_nca(const const_twa_graph_ptr& aut,
|
||||
bool named_states = false,
|
||||
vect_nca_info* nca_info = nullptr);
|
||||
|
||||
/// \brief Converts any ω-automata to det. co-buchi (when possible)
|
||||
///
|
||||
/// The resulting automaton will always recognize at least the same language.
|
||||
|
|
|
|||
|
|
@ -197,3 +197,269 @@ do
|
|||
autfilt input.hoa --included-in=res.hoa
|
||||
done
|
||||
done
|
||||
|
||||
cat formulas | ltlcross \
|
||||
--timeout=60 \
|
||||
'{1} ltl2tgba %f | autfilt --gra >%T' \
|
||||
'{2} case `ltlfilt -f %f --format=%\[w]h` in *P*) ltl2tgba -B %f | autfilt\
|
||||
--gra | autfilt --dca ;; *) ltl2tgba -B %f;; esac >%O'
|
||||
|
||||
cat > bigtest.hoa << EOF
|
||||
HOA: v1
|
||||
States: 29
|
||||
Start: 7
|
||||
AP: 3 "a" "b" "c"
|
||||
Acceptance: 5 Fin(0) & (Inf(1) | Fin(2)) & (Inf(3) | Fin(4))
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0 {3}
|
||||
[0&!1&!2] 0
|
||||
[0&1&!2] 1
|
||||
[0&!1&2] 4
|
||||
[!0&1&2] 13
|
||||
[!0&!1&2] 15
|
||||
[!0&1&!2] 20
|
||||
[!0&!1&!2] 21
|
||||
[0&1&2] 22
|
||||
State: 1 {3}
|
||||
[0&!1&!2] 0
|
||||
[0&1&!2] 1
|
||||
[!0&2] 13
|
||||
[!0&1&!2] 20
|
||||
[!0&!1&!2] 21
|
||||
[0&2] 22
|
||||
State: 2 {3}
|
||||
[0&!1&2] 2
|
||||
[0&!1&!2] 3
|
||||
[0&1&!2] 12
|
||||
[!0&1] 13
|
||||
[0&1&2] 14
|
||||
[!0&!1] 15
|
||||
State: 3 {3}
|
||||
[0&!1&2] 2
|
||||
[0&!1&!2] 3
|
||||
[0&1&!2] 12
|
||||
[!0&1&2] 13
|
||||
[0&1&2] 14
|
||||
[!0&!1&2] 15
|
||||
[!0&!1&!2] 16
|
||||
[!0&1&!2] 20
|
||||
State: 4 {3}
|
||||
[0&!1&!2] 3
|
||||
[0&!1&2] 4
|
||||
[0&1&!2] 12
|
||||
[!0&1] 13
|
||||
[!0&!1] 15
|
||||
[0&1&2] 22
|
||||
State: 5 {3}
|
||||
[0&!1&2] 5
|
||||
[0&1&!2] 12
|
||||
[!0&1] 13
|
||||
[0&1&2] 14
|
||||
[!0&!1] 15
|
||||
[0&!1&!2] 17
|
||||
State: 6 {3}
|
||||
[0&!1&2] 5
|
||||
[0&!1&!2] 6
|
||||
[!0&1&2] 13
|
||||
[0&1&2] 14
|
||||
[!0&!1&2] 15
|
||||
[0&1&!2] 18
|
||||
[!0&1&!2] 20
|
||||
[!0&!1&!2] 28
|
||||
State: 7 {1 3}
|
||||
[!0 | 2] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
State: 8 {1 3}
|
||||
[0&1&!2] 1
|
||||
[0&!1&2] 8
|
||||
[0&!1&!2] 9
|
||||
[!0&1] 13
|
||||
[0&1&2] 22
|
||||
[!0&!1] 23
|
||||
State: 9 {1 3}
|
||||
[0&1&!2] 1
|
||||
[0&!1&2] 8
|
||||
[0&!1&!2] 9
|
||||
[!0&1&2] 13
|
||||
[!0&1&!2] 20
|
||||
[0&1&2] 22
|
||||
[!0&!1&2] 23
|
||||
[!0&!1&!2] 24
|
||||
State: 10 {1 3}
|
||||
[0&1&!2] 10
|
||||
[0&!1&!2] 11
|
||||
[!0&2] 13
|
||||
[0&2] 22
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 11 {1 3}
|
||||
[0&!1&2] 8
|
||||
[0&1&!2] 10
|
||||
[0&!1&!2] 11
|
||||
[!0&1&2] 13
|
||||
[0&1&2] 22
|
||||
[!0&!1&2] 23
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 12 {0 1 3}
|
||||
[0&!1&!2] 0
|
||||
[0&1&!2] 1
|
||||
[!0&2] 13
|
||||
[!0&1&!2] 20
|
||||
[!0&!1&!2] 21
|
||||
[0&2] 22
|
||||
State: 13 {0 1 3}
|
||||
[0&1&!2] 10
|
||||
[0&!1&!2] 11
|
||||
[!0 | 2] 13
|
||||
State: 14 {0 1 3}
|
||||
[!0] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
[0&2] 22
|
||||
State: 15 {0 1 3}
|
||||
[0&!1&!2] 6
|
||||
[!0&1 | 1&2] 13
|
||||
[0&1&!2] 18
|
||||
[!0&!1 | !1&2] 23
|
||||
State: 16 {0 1 3}
|
||||
[0&!1&!2] 6
|
||||
[1&2] 13
|
||||
[0&1&!2] 18
|
||||
[!0&1&!2] 20
|
||||
[!1&2] 23
|
||||
[!0&!1&!2] 24
|
||||
State: 17 {0 1 3}
|
||||
[0&1&!2] 1
|
||||
[0&!1&2] 8
|
||||
[0&!1&!2] 9
|
||||
[!0&1&2] 13
|
||||
[!0&1&!2] 20
|
||||
[0&1&2] 22
|
||||
[!0&!1&2] 23
|
||||
[!0&!1&!2] 24
|
||||
State: 18 {0 1 3}
|
||||
[0&1&!2] 10
|
||||
[0&!1&!2] 11
|
||||
[!0&2] 13
|
||||
[0&2] 22
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 19 {0 1 3}
|
||||
[0&!1&2] 8
|
||||
[0&1&!2] 10
|
||||
[0&!1&!2] 11
|
||||
[!0&1&2] 13
|
||||
[0&1&2] 22
|
||||
[!0&!1&2] 23
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 20 {0 1 3}
|
||||
[2] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 21 {0 1 3}
|
||||
[1&2] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
[!1&2] 23
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 22 {2 3}
|
||||
[!0] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
[0&2] 22
|
||||
State: 23 {2 3}
|
||||
[0&!1&!2] 6
|
||||
[!0&1 | 1&2] 13
|
||||
[0&1&!2] 18
|
||||
[!0&!1 | !1&2] 23
|
||||
State: 24 {2 3}
|
||||
[0&!1&!2] 6
|
||||
[1&2] 13
|
||||
[0&1&!2] 18
|
||||
[!0&1&!2] 20
|
||||
[!1&2] 23
|
||||
[!0&!1&!2] 24
|
||||
State: 25 {2 3}
|
||||
[2] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 26 {2 3}
|
||||
[1&2] 13
|
||||
[0&1&!2] 18
|
||||
[0&!1&!2] 19
|
||||
[!1&2] 23
|
||||
[!0&1&!2] 25
|
||||
[!0&!1&!2] 26
|
||||
State: 27 {2 3}
|
||||
[0&!1&2] 5
|
||||
[0&!1&!2] 6
|
||||
[!0&1&2] 13
|
||||
[0&1&2] 14
|
||||
[!0&!1&2] 15
|
||||
[0&1&!2] 18
|
||||
[!0&1&!2] 20
|
||||
[!0&!1&!2] 28
|
||||
State: 28 {4}
|
||||
[1&2] 13
|
||||
[!1&2] 15
|
||||
[0&1&!2] 18
|
||||
[!0&1&!2] 20
|
||||
[0&!1&!2] 27
|
||||
[!0&!1&!2] 28
|
||||
--END--
|
||||
EOF
|
||||
autfilt bigtest.hoa --dca > res.hoa
|
||||
autfilt bigtest.hoa --equivalent-to='res.hoa'
|
||||
|
||||
cat >empty.hoa<<EOF
|
||||
HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" acc-name: Rabin 3 Acceptance:
|
||||
6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)) properties:
|
||||
trans-labels explicit-labels trans-acc --BODY-- State: 0 [0&!1] 8 {0}
|
||||
[!0&!1] 6 {0 1} State: 1 [!0&1] 4 {2} [0&1] 8 {2} State: 2 [0&1] 6 {1 4}
|
||||
[!0&!1] 3 {1 4} State: 3 [!0&!1] 8 {2 4} [0&1] 4 State: 4 [!0&!1] 8 {4}
|
||||
[!0&!1] 7 State: 5 [!0&!1] 2 {0 5} [!0&!1] 8 {0 4} [!0&!1] 9 {4} State:
|
||||
6 [!0&1] 1 {2 3 4} State: 7 [0&!1] 5 {0} [0&!1] 7 State: 8 [!0&1] 4 {0 2}
|
||||
State: 9 [0&1] 3 {4} [!0&1] 5 {4} --END--
|
||||
EOF
|
||||
autfilt empty.hoa --dca > res.hoa
|
||||
autfilt empty.hoa --equivalent-to='res.hoa'
|
||||
|
||||
cat >empty.hoa<<EOF
|
||||
HOA: v1 States: 11 Start: 0 AP: 3 "a" "b" "c" Acceptance: 5 (Fin(0)
|
||||
| Inf(1)) & (Fin(2) | Inf(3)) & Fin(4) properties: trans-labels
|
||||
explicit-labels trans-acc --BODY-- State: 0 [0&!1&!2] 1 {1} [0&!1&!2]
|
||||
2 {1} [!0&!2] 3 {1} [0&1&!2] 4 {1} [0&1&!2] 5 {1} [0&!1&2] 6 {1} [!0&2 |
|
||||
1&2] 7 {1} State: 1 [0&!1&!2] 1 {0 2} [!0&!2] 3 {0 2} [0&1&!2] 4 {0 2}
|
||||
State: 2 [0&!1&!2] 2 {0 2} [!0&!2] 8 {0 2 4} [0&1&!2] 5 {0 2 4} [0&!1&2]
|
||||
6 {0 2} [!0&2 | 1&2] 7 {0 2 4} State: 3 [0&!1] 9 {1 2} [!0 | 1] 3 {1 2}
|
||||
State: 4 [0&!1&!2] 1 {1 2} [!0&!2] 3 {1 2} [0&1&!2] 4 {1 2} State: 5
|
||||
[0&!1&!2] 2 {1 2} [!0&!2] 8 {1 2 4} [0&1&!2] 5 {1 2 4} [0&!1&2] 6 {1 2}
|
||||
[!0&2 | 1&2] 7 {1 2 4} State: 6 [0&!1] 6 {0 3} [!0 | 1] 7 {0 3 4} State:
|
||||
7 [0&!1] 6 {1 3} [!0 | 1] 7 {1 3 4} State: 8 [0&!1] 10 {1 2} [!0 | 1]
|
||||
8 {1 2 4} State: 9 [0&!1] 9 {0 2} [!0 | 1] 3 {0 2} State: 10 [0&!1]
|
||||
10 {0 2} [!0 | 1] 8 {0 2 4} --END--
|
||||
EOF
|
||||
autfilt empty.hoa --dca > res.hoa
|
||||
autfilt empty.hoa --equivalent-to='res.hoa'
|
||||
|
||||
cat >empty.hoa<<EOF
|
||||
HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" acc-name: Streett 3 Acceptance:
|
||||
6 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) properties:
|
||||
trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0
|
||||
[0&1] 1 [0&!1] 9 {0 5} State: 1 [0&!1] 5 State: 2 [!0&!1] 4 {1} State: 3
|
||||
[!0&!1] 8 {0} State: 4 [0&1] 6 {0 3} State: 5 [!0&!1] 7 State: 6 [!0&1]
|
||||
4 State: 7 [!0&!1] 3 {2 5} State: 8 [0&!1] 1 {2} [!0&!1] 2 {2} State:
|
||||
9 [!0&1] 6 {2 4} --END--
|
||||
EOF
|
||||
autfilt empty.hoa --dca > res.hoa
|
||||
autfilt empty.hoa --equivalent-to='res.hoa'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue