alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Moved IAR and the new version of to_parity in toparity.cc

Browse source 
* python/spot/__init__.py: Use keyword arguments in to_parity()
* python/spot/impl.i: remove useless includes.
* spot/twaalgos/car.cc, spot/twaalgos/car.hh,
spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh,
tests/Makefile.am, spot/twaalgos/Makefile.am:
content moved to toparity.
* spot/twaalgos/postproc.cc: Use the new version of to_parity in
postprocessor::run.
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: Add the
content of rabin2parity and car.
* tests/python/car.py, tests/python/toparity.py: Moved all tests
from car.py to toparity.py.
* tests/python/except.py: Change iar() to iar_old().
This commit is contained in:
Florian Renkin 2020-03-16 16:20:07 +01:00
parent dddc7920e4
commit 75990063f0
14 changed files with 2027 additions and 2105 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/Makefile.am
View file

@ -59,7 +59,6 @@ twaalgos_HEADERS = \
isunamb.hh \
isweakscc.hh \
langmap.hh \
car.hh \
lbtt.hh \
ltl2taa.hh \
ltl2tgba_fm.hh \
@ -72,7 +71,6 @@ twaalgos_HEADERS = \
postproc.hh \
powerset.hh \
product.hh \
rabin2parity.hh \
randomgraph.hh \
randomize.hh \
reachiter.hh \
@ -129,7 +127,6 @@ libtwaalgos_la_SOURCES = \
isunamb.cc \
isweakscc.cc \
langmap.cc \
car.cc \
lbtt.cc \
ltl2taa.cc \
ltl2tgba_fm.cc \
@ -143,7 +140,6 @@ libtwaalgos_la_SOURCES = \
postproc.cc \
powerset.cc \
product.cc \
rabin2parity.cc \
randomgraph.cc \
randomize.cc \
reachiter.cc \

1291
spot/twaalgos/car.cc
View file

File diff suppressed because it is too large Load diff

69
spot/twaalgos/car.hh
View file

@ -1,69 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 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/>.
#pragma once
#include <spot/twa/twagraph.hh>
namespace spot
{
struct car_option
{
bool search_ex = true;
bool use_last = true;
bool force_order = true;
bool partial_degen = true;
bool acc_clean = true;
bool parity_equiv = true;
bool parity_prefix = true;
bool rabin_to_buchi = true;
bool reduce_col_deg = false;
bool propagate_col = true;
bool pretty_print = true;
};
/// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return an
/// equivalent parity automaton.
///
/// The parity condition of the returned automaton is max even or
/// max odd.
/// If \a search_ex is true, when we move several elements, we
/// try to find an order such that the new permutation already exists.
/// If \a partial_degen is true, we apply a partial degeneralization to remove
// occurences of Fin | Fin and Inf & Inf.
/// If \a scc_acc_clean is true, we remove for each SCC the colors that don't
// appear.
/// If \a parity_equiv is true, we check if there exists a permutations of
// colors such that the acceptance
/// condition is a partity condition.
/// If \a use_last is true, we use the most recent state when looking for an
// existing state.
/// If \a pretty_print is true, we give a name to the states describing the
// state of the aut_ and the permutation.
SPOT_API twa_graph_ptr
remove_false_transitions(const twa_graph_ptr a);
SPOT_API twa_graph_ptr
to_parity(const twa_graph_ptr &aut, const car_option options = car_option());
} // namespace spot

4
spot/twaalgos/postproc.cc
View file

@ -38,8 +38,8 @@
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/parity.hh>
#include <spot/twaalgos/cobuchi.hh>
#include <spot/twaalgos/rabin2parity.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/toparity.hh>
namespace spot
{
@ -280,7 +280,7 @@ namespace spot
twa_graph_ptr b = nullptr;
if (want_parity && is_deterministic(a) &&
!a->acc().is_generalized_buchi())
b = iar_maybe(a);
b = to_parity(a);
// possible only if a was deterministic and (Rabin-like or Streett-like)
// and we want parity and a is not a TGBA
// NB: on a TGBA, degeneralization is better than IAR

361
spot/twaalgos/rabin2parity.cc
View file

@ -1,361 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// de l'Epita.
//
// 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/>.
#include "config.h"
#include <deque>
#include <spot/twaalgos/rabin2parity.hh>
#include <spot/twaalgos/sccinfo.hh>
namespace spot
{
namespace
{
using perm_t = std::vector<unsigned>;
struct iar_state
{
unsigned state;
perm_t perm;
bool
operator<(const iar_state& other) const
{
return state == other.state ? perm < other.perm : state < other.state;
}
};
template<bool is_rabin>
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:
explicit iar_generator(const const_twa_graph_ptr& a,
const std::vector<acc_cond::rs_pair>& p,
const bool pretty_print)
: aut_(a)
, pairs_(p)
, scc_(scc_info(a))
, pretty_print_(pretty_print)
, state2pos_iar_states(aut_->num_states(), -1U)
{}
twa_graph_ptr
run()
{
res_ = make_twa_graph(aut_->get_dict());
res_->copy_ap_of(aut_);
build_iar_scc(scc_.initial());
{
// resulting automaton has acceptance condition: parity max odd
// for Rabin-like input and parity max even for Streett-like input.
// with priorities ranging from 0 to 2*(nb pairs)
// /!\ priorities are shifted by -1 compared to the original paper
unsigned sets = 2 * pairs_.size() + 1;
res_->set_acceptance(sets, acc_cond::acc_code::parity_max(is_rabin,
sets));
}
{
unsigned s = iar2num.at(state2iar.at(aut_->get_init_state_number()));
res_->set_init_state(s);
}
// there could be quite a number of unreachable states, prune them
res_->purge_unreachable_states();
if (pretty_print_)
{
unsigned nstates = res_->num_states();
auto names = new std::vector<std::string>(nstates);
for (auto e : res_->edges())
{
unsigned s = e.src;
iar_state iar = num2iar.at(s);
std::ostringstream st;
st << iar.state << ' ';
if (iar.perm.empty())
st << '[';
char sep = '[';
for (unsigned h: iar.perm)
{
st << sep << h;
sep = ',';
}
st << ']';
(*names)[s] = st.str();
}
res_->set_named_prop("state-names", names);
}
return res_;
}
void
build_iar_scc(unsigned scc_num)
{
// we are working on an SCC: the state we start from does not matter
unsigned init = scc_.one_state_of(scc_num);
std::deque<iar_state> todo;
auto get_state = [&](const iar_state& s)
{
auto it = iar2num.find(s);
if (it == iar2num.end())
{
unsigned nb = res_->new_state();
iar2num[s] = nb;
num2iar[nb] = s;
unsigned iar_pos = iar_states.size();
unsigned old_newest_pos = state2pos_iar_states[s.state];
state2pos_iar_states[s.state] = iar_pos;
iar_states.push_back(
std::pair<iar_state, unsigned>(s, old_newest_pos));
todo.push_back(s);
return nb;
}
return it->second;
};
auto get_other_scc = [this](unsigned state)
{
auto it = state2iar.find(state);
// recursively build the destination SCC if we detect that it has
// not been already built.
if (it == state2iar.end())
build_iar_scc(scc_.scc_of(state));
return iar2num.at(state2iar.at(state));
};
if (scc_.is_trivial(scc_num))
{
iar_state iar_s{init, perm_t()};
state2iar[init] = iar_s;
unsigned src_num = get_state(iar_s);
// Do not forget to connect to subsequent SCCs
for (const auto& e : aut_->out(init))
res_->new_edge(src_num, get_other_scc(e.dst), e.cond);
return;
}
// determine the pairs that appear in the SCC
auto colors = scc_.acc_sets_of(scc_num);
std::set<unsigned> scc_pairs;
for (unsigned k = 0; k != pairs_.size(); ++k)
if (!inf(k) || (colors & (pairs_[k].fin | pairs_[k].inf)))
scc_pairs.insert(k);
perm_t p0;
for (unsigned k : scc_pairs)
p0.push_back(k);
iar_state s0{init, p0};
get_state(s0); // put s0 in todo
// the main loop
while (!todo.empty())
{
iar_state current = todo.front();
todo.pop_front();
unsigned src_num = get_state(current);
for (const auto& e : aut_->out(current.state))
{
// connect to the appropriate state
if (scc_.scc_of(e.dst) != scc_num)
res_->new_edge(src_num, get_other_scc(e.dst), e.cond);
else
{
// find the new permutation
perm_t new_perm = current.perm;
// Count pairs whose fin-part is seen on this transition
unsigned seen_nb = 0;
// consider the pairs for this SCC only
for (unsigned k : scc_pairs)
if (e.acc & fin(k))
{
++seen_nb;
auto it = std::find(new_perm.begin(),
new_perm.end(),
k);
// move the pair in front of the permutation
std::rotate(new_perm.begin(), it, it+1);
}
iar_state dst;
unsigned dst_num = -1U;
// Optimization: when several indices are seen in the
// transition, they move at the front of new_perm in any
// order. Check whether there already exists an iar_state
// that matches this condition.
auto iar_pos = state2pos_iar_states[e.dst];
while (iar_pos != -1U)
{
iar_state& tmp = iar_states[iar_pos].first;
iar_pos = iar_states[iar_pos].second;
if (std::equal(new_perm.begin() + seen_nb,
new_perm.end(),
tmp.perm.begin() + seen_nb))
{
dst = tmp;
dst_num = iar2num[dst];
break;
}
}
// if such a state was not found, build it
if (dst_num == -1U)
{
dst = iar_state{e.dst, new_perm};
dst_num = get_state(dst);
}
// find the maximal index encountered by this transition
unsigned maxint = -1U;
for (int k = current.perm.size() - 1; k >= 0; --k)
{
unsigned pk = current.perm[k];
if (!inf(pk) ||
(e.acc & (pairs_[pk].fin | pairs_[pk].inf))) {
maxint = k;
break;
}
}
acc_cond::mark_t acc = {};
if (maxint == -1U)
acc = {0};
else if (e.acc & fin(current.perm[maxint]))
acc = {2*maxint+2};
else
acc = {2*maxint+1};
res_->new_edge(src_num, dst_num, e.cond, acc);
}
}
}
// Optimization: find the bottom SCC of the sub-automaton we have just
// built. To that end, we have to ignore edges going out of scc_num.
auto leaving_edge = [&](unsigned d)
{
return scc_.scc_of(num2iar.at(d).state) != scc_num;
};
auto filter_edge = [](const twa_graph::edge_storage_t&,
unsigned dst,
void* filter_data)
{
decltype(leaving_edge)* data =
static_cast<decltype(leaving_edge)*>(filter_data);
if ((*data)(dst))
return scc_info::edge_filter_choice::ignore;
return scc_info::edge_filter_choice::keep;
};
scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge);
// SCCs are numbered in reverse topological order, so the bottom SCC has
// index 0.
const unsigned bscc = 0;
assert(sub_scc.succ(0).empty());
assert(
[&]()
{
for (unsigned s = 1; s != sub_scc.scc_count(); ++s)
if (sub_scc.succ(s).empty())
return false;
return true;
} ());
assert(sub_scc.states_of(bscc).size()
>= scc_.states_of(scc_num).size());
// update state2iar
for (unsigned scc_state : sub_scc.states_of(bscc))
{
iar_state& iar = num2iar.at(scc_state);
if (state2iar.find(iar.state) == state2iar.end())
state2iar[iar.state] = iar;
}
}
private:
const const_twa_graph_ptr& aut_;
const std::vector<acc_cond::rs_pair>& pairs_;
const scc_info scc_;
twa_graph_ptr res_;
bool pretty_print_;
// to be used when entering a new SCC
// maps a state of aut_ onto an iar_state with the appropriate perm
std::map<unsigned, iar_state> state2iar;
std::map<iar_state, unsigned> iar2num;
std::map<unsigned, iar_state> num2iar;
std::vector<unsigned> state2pos_iar_states;
std::vector<std::pair<iar_state, unsigned>> iar_states;
};
}
twa_graph_ptr
iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print)
{
std::vector<acc_cond::rs_pair> pairs;
if (!aut->acc().is_rabin_like(pairs))
if (!aut->acc().is_streett_like(pairs))
return nullptr;
else
{
iar_generator<false> gen(aut, pairs, pretty_print);
return gen.run();
}
else
{
iar_generator<true> gen(aut, pairs, pretty_print);
return gen.run();
}
}
twa_graph_ptr
iar(const const_twa_graph_ptr& aut, bool pretty_print)
{
if (auto res = iar_maybe(aut, pretty_print))
return res;
throw std::runtime_error("iar() expects Rabin-like or Streett-like input");
}
}

55
spot/twaalgos/rabin2parity.hh
View file

@ -1,55 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement de l'Epita.
//
// 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/>.
#pragma once
#include <spot/twa/twagraph.hh>
namespace spot
{
/// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
/// based on the index appearence record (IAR)
///
/// 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
/// deterministic, the output automaton is deterministic as well, which is the
/// intended use case for this function. If the input automaton is
/// non-deterministic, the result is still correct, but way larger than an
/// equivalent Büchi automaton.
/// 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:
/// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
///
/// Throws an std::runtime_error if the input is neither Rabin-like nor
/// Street-like.
SPOT_API
twa_graph_ptr
iar(const const_twa_graph_ptr& aut, bool pretty_print = false);
/// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
/// based on the index appearence record (IAR)
///
/// Returns nullptr if the input automaton is neither Rabin-like nor
/// Streett-like, and calls spot::iar() otherwise.
SPOT_API
twa_graph_ptr
iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false);
}

1614
spot/twaalgos/toparity.cc
View file

File diff suppressed because it is too large Load diff

88
spot/twaalgos/toparity.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2018 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -23,11 +23,91 @@
namespace spot
{
// The version that combines CAR, IAR and multiple optimizations.
struct car_option
{
bool search_ex = true;
bool use_last = true;
bool force_order = true;
bool partial_degen = true;
bool acc_clean = true;
bool parity_equiv = true;
bool parity_prefix = true;
bool rabin_to_buchi = true;
bool reduce_col_deg = false;
bool propagate_col = true;
bool pretty_print = false;
};
/// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return an
/// equivalent parity automaton.
///
/// The parity condition of the returned automaton is max even or
/// max odd.
/// If \a search_ex is true, when we move several elements, we
/// try to find an order such that the new permutation already exists.
/// If \a partial_degen is true, we apply a partial degeneralization to remove
// occurences of Fin | Fin and Inf & Inf.
/// If \a scc_acc_clean is true, we remove for each SCC the colors that don't
// appear.
/// If \a parity_equiv is true, we check if there exists a permutations of
// colors such that the acceptance
/// condition is a partity condition.
/// If \a use_last is true, we use the most recent state when looking for an
// existing state.
/// If \a pretty_print is true, we give a name to the states describing the
// state of the aut_ and the permutation.
SPOT_API twa_graph_ptr
remove_false_transitions(const twa_graph_ptr a);
SPOT_API twa_graph_ptr
to_parity(const twa_graph_ptr &aut, const car_option options = car_option());
// Old version of CAR
/// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return an
/// equivalent parity automaton.
///
/// The parity condition of the returned automaton is max even.
SPOT_API twa_graph_ptr
to_parity(const const_twa_graph_ptr& aut, bool pretty_print=false);
}
to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print=false);
// Old version of IAR
/// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
/// based on the index appearence record (IAR)
///
/// 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
/// deterministic, the output automaton is deterministic as well, which is the
/// intended use case for this function. If the input automaton is
/// non-deterministic, the result is still correct, but way larger than an
/// equivalent Büchi automaton.
/// 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:
/// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
///
/// Throws an std::runtime_error if the input is neither Rabin-like nor
/// Street-like.
SPOT_API
twa_graph_ptr
iar_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
/// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
/// based on the index appearence record (IAR)
///
/// Returns nullptr if the input automaton is neither Rabin-like nor
/// Streett-like, and calls spot::iar() otherwise.
SPOT_API
twa_graph_ptr
iar_maybe_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
} // namespace spot