twaalgos/totgba: Add dnf_to_streett() method

* NEWS: Update.
* spot/twaalgos/totgba.hh: Declare dnf_to_streett().
* spot/twaalgos/totgba.cc: Implement dnf_to_streett().
* bin/autfilt.cc: Add --dnf-to-streett cmd line option.
* tests/core/dnfstreett.test: Add test.
* tests/Makefile.am: Add test file.
parent cf18c069
......@@ -9,6 +9,10 @@ New in spot 2.4.0.dev (not yet released)
--ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))
--ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))
- autfilt learned --streett-like to convert an automaton in order to
have a Streett-like acceptance condition. It only works with
ω-automata having an acceptance in disjunctive normal form.
Library:
- Rename three methods of spot::scc_info. New names are clearer. The
......@@ -26,6 +30,11 @@ New in spot 2.4.0.dev (not yet released)
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.
Deprecation notices:
(These functions still work but compilers emit warnings.)
......
......@@ -142,6 +142,7 @@ enum {
OPT_SIMPLIFY_EXCLUSIVE_AP,
OPT_SPLIT_EDGES,
OPT_STATES,
OPT_STREETT_LIKE,
OPT_STRIPACC,
OPT_SUM_OR,
OPT_SUM_AND,
......@@ -275,6 +276,9 @@ static const argp_option options[] =
"initial state. Implies --remove-unreachable-states.", 0 },
{ "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
"put the acceptance condition in Disjunctive Normal Form", 0 },
{ "streett-like", OPT_STREETT_LIKE, nullptr, 0,
"convert to an automaton with Streett-like acceptance. Works only with "
"acceptance condition in DNF", 0 },
{ "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
"put the acceptance condition in Conjunctive Normal Form", 0 },
{ "remove-fin", OPT_REM_FIN, nullptr, 0,
......@@ -520,6 +524,7 @@ static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
static bool opt_highlight_languages = false;
static bool opt_dca = false;
static bool opt_streett_like = false;
static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
......@@ -622,6 +627,9 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_dnf_acc = true;
opt_cnf_acc = false;
break;
case OPT_STREETT_LIKE:
opt_streett_like = true;
break;
case OPT_EDGES:
opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
......@@ -1205,6 +1213,9 @@ namespace
if (opt_dca)
aut = spot::to_dca(aut, false);
if (opt_streett_like)
aut = spot::dnf_to_streett(aut);
if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
aut = opt->excl_ap.constrain(aut, true);
else if (opt_rem_unused_ap) // constrain(aut, true) already does that
......
......@@ -25,8 +25,411 @@
#include <deque>
#include <tuple>
#define DEBUG 0
#if DEBUG
#define debug std::cerr
#else
#define debug while (0) std::cerr
#endif
namespace spot
{
namespace
{
class dnf_to_streett_converter
{
private:
typedef std::pair<acc_cond::mark_t, acc_cond::mark_t> mark_pair;
const const_twa_graph_ptr& in_; // The given aut.
scc_info si_; // SCC information.
unsigned nb_scc_; // Number of SCC.
unsigned max_set_in_; // Max acc. set nb of in_.
bool state_based_; // Is in_ state_based ?
unsigned init_st_in_; // Initial state of in_.
bool init_reachable_; // Init reach from itself?
twa_graph_ptr res_; // Resulting automaton.
acc_cond::mark_t all_fin_; // All acc. set marked as
// Fin.
acc_cond::mark_t all_inf_; // All acc. set marked as
// Inf.
unsigned num_sets_res_; // Future nb of acc. set.
std::vector<mark_pair> all_clauses_; // All clauses.
std::vector<acc_cond::mark_t> set_to_keep_; // Set to keep for each clause
std::vector<acc_cond::mark_t> set_to_add_; // New set for each clause.
acc_cond::mark_t all_set_to_add_; // All new set to add.
std::vector<unsigned> assigned_sets_; // Set that will be add.
std::vector<std::vector<unsigned>> acc_clauses_; // Acc. clauses.
unsigned res_init_; // Future initial st.
// A state can be copied at most as many times as their are clauses for
// which it is not rejecting and must be copied one time (to remain
// consistent with the recognized language). This vector records each
// created state following this format:
// st_repr_[orig_st_nb] gives a vector<pair<clause, state>>.
std::vector<std::vector<std::pair<unsigned, unsigned>>> st_repr_;
// Split the DNF acceptance condition and get all the sets used in each
// clause. It separates those that must be seen finitely often from
// those that must be seen infinitely often.
void
split_dnf_clauses(const acc_cond::acc_code& code)
{
bool one_conjunction = false;
const acc_cond::acc_op root_op = code.back().sub.op;
auto s = code.back().sub.size;
while (s)
{
--s;
if (code[s].sub.op == acc_cond::acc_op::And
|| ((one_conjunction = root_op == acc_cond::acc_op::And)))
{
debug << "WABA" << std::endl;
s = one_conjunction ? s + 1 : s;
const unsigned short size = code[s].sub.size;
acc_cond::mark_t fin = 0u;
acc_cond::mark_t inf = 0u;
for (unsigned i = 1; i <= size; i += 2)
{
if (code[s-i].sub.op == acc_cond::acc_op::Fin)
fin |= code[s-i-1].mark;
else if (code[s-i].sub.op == acc_cond::acc_op::Inf)
inf |= code[s-i-1].mark;
else
SPOT_UNREACHABLE();
}
all_clauses_.emplace_back(fin, inf);
set_to_keep_.emplace_back(fin | inf);
s -= size;
}
else if (code[s].sub.op == acc_cond::acc_op::Fin) // Fin
{
auto m1 = code[--s].mark;
for (unsigned int s : m1.sets())
{
all_clauses_.emplace_back(acc_cond::mark_t({s}), 0u);
set_to_keep_.emplace_back(acc_cond::mark_t({s}));
}
}
else if (code[s].sub.op == acc_cond::acc_op::Inf) // Inf
{
auto m2 = code[--s].mark;
all_clauses_.emplace_back(0u, m2);
set_to_keep_.emplace_back(m2);
}
else
{
SPOT_UNREACHABLE();
}
}
#if DEBUG
debug << "\nPrinting all clauses\n";
for (unsigned i = 0; i < all_clauses_.size(); ++i)
{
debug << i << " Fin:" << all_clauses_[i].first << " Inf:"
<< all_clauses_[i].second << std::endl;
}
#endif
}
// Compute all the acceptance sets that will be needed:
// -Inf(x) will be converted to (Inf(x) | Fin(y)) with y appearing
// on every edge.
// -Fin(x) will be converted to (Inf(y) | Fin(x)) with y appearing
// nowhere.
//
// All the previous 'y' are the new sets assigned.
void
assign_new_sets()
{
unsigned int next_set = 0;
unsigned int missing_set = -1U;
assigned_sets_.resize(max_set_in_, -1U);
acc_cond::mark_t all_m = all_fin_ | all_inf_;
for (unsigned set = 0; set < max_set_in_; ++set)
if (all_fin_.has(set))
{
if ((int)missing_set < 0)
{
while (all_m & acc_cond::mark_t({next_set}))
++next_set;
missing_set = next_set++;
}
assigned_sets_[set] = missing_set;
}
else if (all_inf_.has(set))
{
while (all_m & acc_cond::mark_t({next_set}))
++next_set;
assigned_sets_[set] = next_set++;
}
num_sets_res_ = next_set > max_set_in_ ? next_set : max_set_in_;
}
// Precompute:
// -the sets to add for each clause,
// -all sets to add.
void
find_set_to_add()
{
assign_new_sets();
unsigned nb_clause = all_clauses_.size();
for (unsigned clause = 0; clause < nb_clause; ++clause)
{
if (all_clauses_[clause].second)
{
acc_cond::mark_t m = 0u;
for (unsigned set = 0; set < max_set_in_; ++set)
if (all_clauses_[clause].second.has(set))
{
assert((int)assigned_sets_[set] >= 0);
m |= acc_cond::mark_t({assigned_sets_[set]});
}
set_to_add_.push_back(m);
}
else
{
set_to_add_.emplace_back(0u);
}
}
all_set_to_add_ = 0u;
for (unsigned s = 0; s < max_set_in_; ++s)
if (all_inf_.has(s))
{
assert((int)assigned_sets_[s] >= 0);
all_set_to_add_.set(assigned_sets_[s]);
}
}
// Check whether the initial state is reachable from itself.
bool
is_init_reachable()
{
for (const auto& e : in_->edges())
for (unsigned d : in_->univ_dests(e))
if (d == init_st_in_)
return true;
return false;
}
// Get all non rejecting scc for each clause of the acceptance
// condition. Actually, for each clause, an scc will be kept if it
// contains all the 'Inf' acc. sets of the clause.
void
find_probably_accepting_scc(std::vector<std::vector<unsigned>>& res)
{
res.resize(nb_scc_);
unsigned nb_clause = all_clauses_.size();
for (unsigned scc = 0; scc < nb_scc_; ++scc)
{
if (si_.is_rejecting_scc(scc))
continue;
acc_cond::mark_t acc = si_.acc_sets_of(scc);
for (unsigned clause = 0; clause < nb_clause; ++clause)
{
if ((acc & all_clauses_[clause].second)
== all_clauses_[clause].second)
res[scc].push_back(clause);
}
}
#if DEBUG
debug << "accepting clauses" << std::endl;
for (unsigned i = 0; i < res.size(); ++i)
{
debug << "scc(" << i << ") --> ";
for (auto elt : res[i])
debug << elt << ',';
debug << std::endl;
}
debug << std::endl;
#endif
}
// Add all possible representatives of the original state provided.
// Actually, this state will be copied as many times as there are clauses
// for which its SCC is not rejecting.
void
add_state(unsigned st)
{
debug << "add_state(" << st << ')' << std::endl;
if (st_repr_[st].empty())
{
unsigned st_scc = si_.scc_of(st);
if (st == init_st_in_ && !init_reachable_)
st_repr_[st].emplace_back(-1U, res_init_);
else if (!acc_clauses_[st_scc].empty())
for (const auto& clause : acc_clauses_[st_scc])
st_repr_[st].emplace_back(clause, res_->new_state());
else
st_repr_[st].emplace_back(-1U, res_->new_state());
debug << "added" << std::endl;
}
}
// Compute the mark that will be set (instead of the provided e_acc)
// according to the current clause in process. This function is only
// called for accepting SCC.
acc_cond::mark_t
get_edge_mark(const acc_cond::mark_t& e_acc,
unsigned clause)
{
assert((int)clause >= 0);
return (e_acc & set_to_keep_[clause]) | set_to_add_[clause];
}
// Set the acceptance condition once the resulting automaton is ready.
void
set_acc_condition()
{
acc_cond::acc_code p_code;
for (unsigned set = 0; set < max_set_in_; ++set)
{
if (all_fin_.has(set))
p_code &=
acc_cond::acc_code::inf(acc_cond::mark_t({assigned_sets_[set]}))
| acc_cond::acc_code::fin(acc_cond::mark_t({set}));
else if (all_inf_.has(set))
p_code &=
acc_cond::acc_code::inf(acc_cond::mark_t({set}))
| acc_cond::acc_code::fin(
acc_cond::mark_t({assigned_sets_[set]}));
}
res_->set_acceptance(num_sets_res_, p_code);
}
public:
dnf_to_streett_converter(const const_twa_graph_ptr& in,
const acc_cond::acc_code& code)
: in_(in),
si_(scc_info(in)),
nb_scc_(si_.scc_count()),
max_set_in_(code.used_sets().max_set()),
state_based_(in->prop_state_acc() == true),
init_st_in_(in->get_init_state_number()),
init_reachable_(is_init_reachable())
{
debug << "State based ? " << state_based_ << std::endl;
std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets();
split_dnf_clauses(code);
find_set_to_add();
find_probably_accepting_scc(acc_clauses_);
}
~dnf_to_streett_converter()
{}
twa_graph_ptr run(bool original_states)
{
res_ = make_twa_graph(in_->get_dict());
res_->copy_ap_of(in_);
st_repr_.resize(in_->num_states());
res_init_ = res_->new_state();
res_->set_init_state(res_init_);
for (unsigned scc = 0; scc < nb_scc_; ++scc)
{
bool rej_scc = acc_clauses_[scc].empty();
for (auto st : si_.states_of(scc))
{
add_state(st);
for (const auto& e : in_->out(st))
{
debug << "working_on_edge(" << st << ',' << e.dst << ')'
<< std::endl;
add_state(e.dst);
bool same_scc = scc == si_.scc_of(e.dst);
if (st == init_st_in_)
{
for (const auto& p_dst : st_repr_[e.dst])
res_->new_edge(res_init_, p_dst.second, e.cond, 0u);
if (!init_reachable_)
continue;
}
if (!rej_scc)
for (const auto& p_src : st_repr_[st])
for (const auto& p_dst : st_repr_[e.dst])
{
debug << "repr(" << p_src.second << ','
<< p_dst.second << ')' << std::endl;
if (same_scc && p_src.first == p_dst.first)
res_->new_edge(p_src.second, p_dst.second, e.cond,
get_edge_mark(e.acc, p_src.first));
else if (!same_scc)
res_->new_edge(p_src.second, p_dst.second, e.cond,
state_based_ ?
get_edge_mark(e.acc, p_src.first)
: 0u);
}
else
{
assert(st_repr_[st].size() == 1);
unsigned src = st_repr_[st][0].second;
acc_cond::mark_t m = 0u;
if (same_scc || state_based_)
m = all_set_to_add_;
for (const auto& p_dst : st_repr_[e.dst])
res_->new_edge(src, p_dst.second, e.cond, m);
}
}
}
}
// Mapping between each state of the resulting automaton and the
// original state of the input automaton.
if (original_states)
{
auto orig_states = new std::vector<unsigned>();
orig_states->resize(res_->num_states(), -1U);
res_->set_named_prop("original-states", orig_states);
unsigned orig_num_states = in_->num_states();
for (unsigned orig = 0; orig < orig_num_states; ++orig)
for (const auto& p : st_repr_[orig])
(*orig_states)[p.second] = orig;
#if DEBUG
for (unsigned i = 1; i < orig_states->size(); ++i)
assert((int)(*orig_states)[i] >= 0);
#endif
}
set_acc_condition();
res_->prop_state_acc(state_based_);
return res_;
}
};
}
twa_graph_ptr
dnf_to_streett(const const_twa_graph_ptr& in, bool original_states)
{
const acc_cond::acc_code& code = in->get_acceptance();
if (!code.is_dnf())
throw std::runtime_error("dnf_to_streett() should only be"
" called on automata with DNF acceptance");
if (code.is_t() || code.is_f() || in->acc().is_streett() > 0)
return make_twa_graph(in, twa::prop_set::all());
dnf_to_streett_converter dnf_to_streett(in, code);
return dnf_to_streett.run(original_states);
}
namespace
{
struct st2gba_state
......
......@@ -21,6 +21,8 @@
#include <spot/twa/twagraph.hh>
#include <unordered_map>
namespace spot
{
/// \brief Take an automaton with any acceptance condition and return
......@@ -66,4 +68,38 @@ namespace spot
SPOT_API twa_graph_ptr
to_generalized_streett(const const_twa_graph_ptr& aut,
bool share_fin = false);
/// \brief Converts any DNF acceptance condition into Streett-like.
///
/// This function is an optimized version of the construction described
/// by Lemma 4 and 5 of the paper below.
/** \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 */
///
/// In the described construction, as many copies as there are minterms in
/// the acceptance condition are made and the union of all those copies is
/// returned.
/// Instead of cloning the automaton for each minterm and end up with many
/// rejecting and useless SCC, we construct the automaton SCC by SCC. Each SCC
/// is copied at most as many times as there are minterms for which it is not
/// rejecting and at least one time if it is always rejecting (to be
/// consistent with the recognized language).
///
/// \a aut The automaton to convert.
/// \a original_states Enable mapping between each state of the resulting
/// automaton and the original state of the input automaton. This is stored
/// in the "original-states" named property of the produced automaton. Call
/// `aut->get_named_prop<std::vector<unsigned>>("original-states")`
/// to retrieve it.
SPOT_API twa_graph_ptr
dnf_to_streett(const const_twa_graph_ptr& aut, bool original_states = false);
}
......@@ -300,7 +300,8 @@ TESTS_twa = \
core/randpsl.test \
core/cycles.test \
core/acc_word.test \
core/dca.test
core/dca.test \
core/dnfstreett.test
############################## PYTHON ##############################
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 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
cat >accs << 'EOF'
(Fin(0) & Inf(1)) | Fin(2)
(Fin(0) & Inf(1)) | Inf(2)
(Fin(0) & Fin(1) & Fin(2) & Inf(3)) | Inf(4) | Fin(5)
Rabin1
Rabin2
Rabin3
(Fin(0) & Inf(1)) | (Fin(2) & Fin(3) & Fin(4)) | (Inf(5) & Inf(6) & Inf(7))
Fin(0) | (Fin(1) & Fin(2) & Inf(3)) | (Inf(4) & Inf(5) & Fin(6))
Fin(0) | Inf(1) | Inf(2) | Fin(3)
EOF
while read line
do
randaut -A "$line" a b c > input.hoa
autfilt --streett-like input.hoa > res.hoa
autfilt input.hoa --equivalent-to='res.hoa'
autfilt --complement input.hoa > input_comp.hoa
autfilt --complement res.hoa > res_comp.hoa
autfilt input_comp.hoa --equivalent-to='res_comp.hoa'
done < accs
cat >random_ltl<< 'EOF'
F(a R !c)
XXF(a R b)
FG(Xa xor !(a W c))
XX(1 U ((X(b W a) M 1) R c))
(b | GFXb) -> (a xor b)
F(!a R c) | (b <-> XX(!Gb R b))
X!G(0 R (b M 1))
XF((Fc <-> (!b W c)) <-> (Gc M 1))
F((!b | FGc) -> (b W (!c <-> Xc)))
((a xor b) -> a) U (Ga & (b R c))
F((a M Xc) | FG(Xb <-> X(b | c)))
XFG!a
((b R c) | F!XGF(b | c)) R !b
Xc U Ga
(Fa & Xc) | G(b U Ga)
X!(((c <-> (!a M b)) W 0) W 0)
b U (c W Fa)
F(Xa W (b xor (Ga U !Xb)))
!(G(c R Gc) U X(Fc W !Xb))
F(0 R (c W a))
EOF
ltlcross -F random_ltl \
--timeout=60 \
'{1} ltl2tgba %f | autfilt --gra >%T' \
'{2} ltl2tgba %f | autfilt --gra | autfilt --streett-like >%T'
cat >input.hoa<< 'EOF'
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
--BODY--
State: 0
[!0&!1] 3
[!0&!1] 1
State: 1
[0&1] 2 {1 2 4}
State: 2
[0&1] 1
State: 3
[!0&1] 0 {0 3 5}
[!0&!1] 2 {1 2 4}
--END--
EOF
autfilt --streett-like input.hoa > res.hoa
autfilt input.hoa --equivalent-to='res.hoa'
autfilt --complement input.hoa > input_comp.hoa
autfilt --complement res.hoa > res_comp.hoa
autfilt input_comp.hoa --equivalent-to='res_comp.hoa'