Commit 1ebd86de authored by Maximilien Colange's avatar Maximilien Colange
Browse files

Improve IAR construction

spot::iar() was fixed to handle correctly Rabin-like conditions.
It also now supports Streett-like conditions.

* NEWS, spot/twaalgos/postproc.cc: document it
* spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
  implement it
* tests/core/rabin2parity.test, tests/python/except.py: test it
parent ff2a96cc
New in spot 2.5.0.dev (not yet released) New in spot 2.5.0.dev (not yet released)
Library:
- iar() and iar_maybe() now also handle Streett-like conditions.
Bugs fixed: Bugs fixed:
- streett_to_generalized_buchi() could produce incorrect result on - streett_to_generalized_buchi() could produce incorrect result on
Streett-like input with acceptance like (Inf(0)|Fin(1))&Fin(1) Streett-like input with acceptance like (Inf(0)|Fin(1))&Fin(1)
where some Fin(x) is used both with and without a paired Fin(y). where some Fin(x) is used both with and without a paired Fin(y).
- iar() and iar_maybe() properly handle Rabin-like conditions.
New in spot 2.5 (2018-01-20) New in spot 2.5 (2018-01-20)
Build: Build:
...@@ -92,7 +98,7 @@ New in spot 2.5 (2018-01-20) ...@@ -92,7 +98,7 @@ New in spot 2.5 (2018-01-20)
New functions in the library: New functions in the library:
- spot::iar() and spot::iar_maybe() use index appearance records (IAR) - spot::iar() and spot::iar_maybe() use index appearance records (IAR)
to translate Rabin-like automata into equivalent parity automaton. to translate Rabin-like automata into equivalent parity automata.
This translation preserves determinism and is especially useful when This translation preserves determinism and is especially useful when
the input automaton is deterministic. the input automaton is deterministic.
......
...@@ -242,10 +242,12 @@ namespace spot ...@@ -242,10 +242,12 @@ namespace spot
|| (want_parity && !a->acc().is_parity())) || (want_parity && !a->acc().is_parity()))
{ {
twa_graph_ptr b = nullptr; twa_graph_ptr b = nullptr;
if (want_parity && is_deterministic(a)) if (want_parity && is_deterministic(a) &&
!a->acc().is_generalized_buchi())
b = iar_maybe(a); b = iar_maybe(a);
// possible only if a was deterministic and Rabin-like and // possible only if a was deterministic and (Rabin-like or Streett-like)
// we want parity // and we want parity and a is not a TGBA
// NB: on a TGBA, degeneralization is better than IAR
if (b) if (b)
a = b; a = b;
else else
......
...@@ -21,7 +21,6 @@ ...@@ -21,7 +21,6 @@
#include <spot/twaalgos/rabin2parity.hh> #include <spot/twaalgos/rabin2parity.hh>
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isdet.hh>
namespace spot namespace spot
{ {
...@@ -41,8 +40,27 @@ namespace spot ...@@ -41,8 +40,27 @@ namespace spot
} }
}; };
template<bool is_rabin>
class iar_generator class iar_generator
{ {
// helper functions: access fin and inf parts of the pairs
// these functions negate the Streett condition to see it as a Rabin one
const acc_cond::mark_t&
fin(unsigned k) const
{
if (is_rabin)
return pairs_[k].fin;
else
return pairs_[k].inf;
}
acc_cond::mark_t
inf(unsigned k) const
{
if (is_rabin)
return pairs_[k].inf;
else
return pairs_[k].fin;
}
public: public:
explicit iar_generator(const const_twa_graph_ptr& a, explicit iar_generator(const const_twa_graph_ptr& a,
const std::vector<acc_cond::rs_pair>& p) const std::vector<acc_cond::rs_pair>& p)
...@@ -60,10 +78,14 @@ namespace spot ...@@ -60,10 +78,14 @@ namespace spot
build_iar_scc(scc_.initial()); build_iar_scc(scc_.initial());
// resulting automaton has acceptance condition: parity max odd // resulting automaton has acceptance condition: parity max odd
// with priorities ranging from 0 to 2*(nb Rabin pairs) // with priorities ranging from 0 to 2*(nb pairs)
// /!\ priorities are shifted by -1 compared to the original paper // /!\ priorities are shifted by -1 compared to the original paper
res_->set_acceptance(2*pairs_.size() + 1, if (is_rabin)
acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1)); res_->set_acceptance(2*pairs_.size() + 1,
acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1));
else
res_->set_acceptance(2*pairs_.size() + 1,
acc_cond::acc_code::parity(true, false, 2*pairs_.size() + 1));
// set initial state // set initial state
res_->set_init_state( res_->set_init_state(
...@@ -117,11 +139,11 @@ namespace spot ...@@ -117,11 +139,11 @@ namespace spot
return; return;
} }
// determine the Rabin pairs that appear in the SCC // determine the pairs that appear in the SCC
auto colors = scc_.acc_sets_of(scc_num); auto colors = scc_.acc_sets_of(scc_num);
std::set<unsigned> scc_pairs; std::set<unsigned> scc_pairs;
for (unsigned k = 0; k != pairs_.size(); ++k) for (unsigned k = 0; k != pairs_.size(); ++k)
if (colors & (pairs_[k].fin | pairs_[k].inf)) if (inf(k) == 0U || (colors & (pairs_[k].fin | pairs_[k].inf)))
scc_pairs.insert(k); scc_pairs.insert(k);
perm_t p0; perm_t p0;
...@@ -150,10 +172,9 @@ namespace spot ...@@ -150,10 +172,9 @@ namespace spot
perm_t new_perm = current.perm; perm_t new_perm = current.perm;
// Count pairs whose fin-part is seen on this transition // Count pairs whose fin-part is seen on this transition
unsigned seen_nb = 0; unsigned seen_nb = 0;
std::vector<unsigned> seen;
// consider the pairs for this SCC only // consider the pairs for this SCC only
for (unsigned k : scc_pairs) for (unsigned k : scc_pairs)
if (e.acc & pairs_[k].fin) if (e.acc & fin(k))
{ {
++seen_nb; ++seen_nb;
auto it = std::find(new_perm.begin(), auto it = std::find(new_perm.begin(),
...@@ -192,7 +213,8 @@ namespace spot ...@@ -192,7 +213,8 @@ namespace spot
for (unsigned k = 0; k != current.perm.size(); ++k) for (unsigned k = 0; k != current.perm.size(); ++k)
{ {
unsigned pk = current.perm[k]; unsigned pk = current.perm[k];
if (e.acc & (pairs_[pk].fin | pairs_[pk].inf)) if (inf(pk) == 0U ||
(e.acc & (pairs_[pk].fin | pairs_[pk].inf)))
// k increases in the loop, so k > maxint necessarily // k increases in the loop, so k > maxint necessarily
maxint = k; maxint = k;
} }
...@@ -200,7 +222,7 @@ namespace spot ...@@ -200,7 +222,7 @@ namespace spot
acc_cond::mark_t acc = 0U; acc_cond::mark_t acc = 0U;
if (maxint == -1U) if (maxint == -1U)
acc = {0}; acc = {0};
else if (e.acc & pairs_[current.perm[maxint]].fin) else if (e.acc & fin(current.perm[maxint]))
acc = {2*maxint+2}; acc = {2*maxint+2};
else else
acc = {2*maxint+1}; acc = {2*maxint+1};
...@@ -271,12 +293,20 @@ namespace spot ...@@ -271,12 +293,20 @@ namespace spot
twa_graph_ptr twa_graph_ptr
iar_maybe(const const_twa_graph_ptr& aut) iar_maybe(const const_twa_graph_ptr& aut)
{ {
std::vector<acc_cond::rs_pair> rabin_pairs; std::vector<acc_cond::rs_pair> pairs;
if (!aut->acc().is_rabin_like(rabin_pairs)) if (!aut->acc().is_rabin_like(pairs))
return nullptr; if (!aut->acc().is_streett_like(pairs))
return nullptr;
iar_generator gen(aut, rabin_pairs); else
return gen.run(); {
iar_generator<false> gen(aut, pairs);
return gen.run();
}
else
{
iar_generator<true> gen(aut, pairs);
return gen.run();
}
} }
twa_graph_ptr twa_graph_ptr
...@@ -284,6 +314,6 @@ namespace spot ...@@ -284,6 +314,6 @@ namespace spot
{ {
if (auto res = iar_maybe(aut)) if (auto res = iar_maybe(aut))
return res; return res;
throw std::runtime_error("iar() expects Rabin-like input"); throw std::runtime_error("iar() expects Rabin-like or Streett-like input");
} }
} }
...@@ -23,30 +23,32 @@ ...@@ -23,30 +23,32 @@
namespace spot namespace spot
{ {
/// \ingroup twa_acc_transform /// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like automaton into a parity automaton based on the /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
/// index appearence record (IAR) /// based on the index appearence record (IAR)
/// ///
/// If the input automaton has n states and k pairs, the output automaton has /// If the input automaton has n states and k pairs, the output automaton has
/// at most k!*n states and 2k+1 colors. If the input automaton is /// at most k!*n states and 2k+1 colors. If the input automaton is
/// deterministic, the output automaton is deterministic as well, which is the /// deterministic, the output automaton is deterministic as well, which is the
/// intended use case for this function. If the input automaton is /// intended use case for this function. If the input automaton is
/// non-deterministic, the result is still correct, but way larger than an /// non-deterministic, the result is still correct, but way larger than an
/// equivalent Büchi automaton. The output parity automaton has max odd /// equivalent Büchi automaton.
/// acceptance condition. /// If the input automaton is Rabin-like (resp. Streett-like), the output
/// automaton has max odd (resp. min even) acceptance condition.
/// Details on the algorithm can be found in: /// Details on the algorithm can be found in:
/// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017) /// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
/// ///
/// Throws an std::runtime_error if the input is not Rabin-like. /// Throws an std::runtime_error if the input is neither Rabin-like nor
/// Street-like.
SPOT_API SPOT_API
twa_graph_ptr twa_graph_ptr
iar(const const_twa_graph_ptr& aut); iar(const const_twa_graph_ptr& aut);
/// \ingroup twa_acc_transform /// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like automaton into a parity automaton based on the /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
/// index appearence record (IAR) /// based on the index appearence record (IAR)
/// ///
/// Return nullptr if the input automaton is not Rabin-like, and /// Returns nullptr if the input automaton is neither Rabin-like nor
/// calls spot::iar() otherwise. /// Streett-like, and calls spot::iar() otherwise.
SPOT_API SPOT_API
twa_graph_ptr twa_graph_ptr
iar_maybe(const const_twa_graph_ptr& aut); iar_maybe(const const_twa_graph_ptr& aut);
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et # Copyright (C) 2017-2018 Laboratoire de Recherche 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.
...@@ -39,9 +39,39 @@ State: 1 ...@@ -39,9 +39,39 @@ State: 1
[0] 1 {1 } [0] 1 {1 }
[!0] 1 {0 1 } [!0] 1 {0 1 }
--END-- --END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[t] 0
--END--
HOA: v1
States: 3
Start: 0
AP: 1 "a"
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] 0 {1 3}
[0] 1 {}
State: 1
[0] 2 {2}
State: 2
[!0] 0 {0 4}
[0] 2 {}
--END--
EOF EOF
# random automata # random automata
randaut 5 -n100 -u -D --acceptance="Rabin 0..6" randaut 4 -n100 -u -D --acceptance="Rabin 0..6"
randaut 4 -n100 -u -D --acceptance="Streett 0..6"
) | \ ) | \
autcross \ autcross \
"autfilt --parity" \ "autfilt --parity" \
......
...@@ -27,7 +27,7 @@ import spot ...@@ -27,7 +27,7 @@ import spot
try: try:
spot.iar(spot.translate('GFa & GFb & GFc')) spot.iar(spot.translate('GFa & GFb & GFc'))
except RuntimeError as e: except RuntimeError as e:
assert 'iar() expects Rabin-like input' in str(e) assert 'iar() expects Rabin-like or Streett-like input' in str(e)
alt = spot.dualize(spot.translate('FGa | FGb')) alt = spot.dualize(spot.translate('FGa | FGb'))
......
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