Commit 96531f29 authored by Florian Renkin's avatar Florian Renkin

CAR: new algorithm for paritizing

* NEWS: Mention it.
* spot/twaalgos/car.cc, spot/twaalgos/car.hh, tests/python/car.py:
New files.
* spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
* python/spot/impl.i: Include CAR.
* spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/twagraph.cc,
spot/twa/twagraph.hh: Add supporting methods.
parent 5d021a18
......@@ -88,6 +88,9 @@ New in spot 2.8.6.dev (not yet released)
same transition structure (where the ..._maybe() variant would
modify the Rabin automaton if needed).
- car() is a new variant of LAR algorithm that combines several
strategies for paritazing any automaton.
New in spot 2.8.6 (2020-02-19)
Bugs fixed:
......
......@@ -162,6 +162,7 @@
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/rabin2parity.hh>
#include <spot/twaalgos/toparity.hh>
#include <spot/twaalgos/car.hh>
#include <spot/parseaut/public.hh>
......@@ -683,6 +684,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/are_isomorphic.hh>
%include <spot/twaalgos/rabin2parity.hh>
%include <spot/twaalgos/toparity.hh>
%include <spot/twaalgos/car.hh>
%pythonprepend spot::twa::dtwa_complement %{
from warnings import warn
......
......@@ -25,6 +25,7 @@
#include <cctype>
#include <cstring>
#include <map>
#include <numeric>
#include <spot/twa/acc.hh>
#include "spot/priv/bddalloc.hh"
#include <spot/misc/minato.hh>
......@@ -1059,6 +1060,38 @@ namespace spot
return res;
}
bool
acc_cond::has_parity_prefix(acc_cond& new_cond,
std::vector<unsigned>& colors) const
{
return code_.has_parity_prefix(new_cond, colors);
}
bool
acc_cond::is_parity_max_equiv(std::vector<int>&permut, bool even) const
{
bool result = code_.is_parity_max_equiv(permut, 0, even);
int max_value = *std::max_element(std::begin(permut), std::end(permut));
for (unsigned i = 0; i < permut.size(); ++i)
if (permut[i] != -1)
permut[i] = max_value - permut[i];
else
permut[i] = i;
return result;
}
std::vector<unsigned>
acc_cond::colors_inf_conj(unsigned min_nb_colors)
{
return code_.colors_inf_conj(min_nb_colors);
}
std::vector<unsigned>
acc_cond::colors_fin_disj(unsigned min_nb_colors)
{
return code_.colors_fin_disj(min_nb_colors);
}
bool acc_cond::is_parity(bool& max, bool& odd, bool equiv) const
{
unsigned sets = num_;
......@@ -1250,6 +1283,110 @@ namespace spot
return rescode;
}
bool
acc_cond::acc_code::is_parity_max_equiv(std::vector<int>& permut,
unsigned new_color,
bool even) const
{
auto conj = top_conjuncts();
auto disj = top_disjuncts();
if (conj.size() == 1)
{
if (disj.size() == 1)
{
acc_cond::acc_code elem = conj[0];
if ((even && elem.back().sub.op == acc_cond::acc_op::Inf)
|| (!even && elem.back().sub.op == acc_cond::acc_op::Fin))
{
for (auto color : disj[0][0].mark.sets())
{
if (permut[color] != -1
&& ((unsigned) permut[color]) != new_color)
return false;
permut[color] = new_color;
}
return true;
}
return false;
}
else
{
std::sort(disj.begin(), disj.end(),
[](acc_code c1, acc_code c2)
{
(void) c2;
return c1.back().sub.op == acc_cond::acc_op::Inf;
});
unsigned i = 0;
for (; i < disj.size() - 1; ++i)
{
if (disj[i].back().sub.op != acc_cond::acc_op::Inf
|| disj[i][0].mark.count() != 1)
return false;
for (auto color : disj[i][0].mark.sets())
{
if (permut[color] != -1
&& ((unsigned) permut[color]) != new_color)
return false;
permut[color] = new_color;
}
}
if (disj[i].back().sub.op == acc_cond::acc_op::Inf)
{
if (!even || disj[i][0].mark.count() != 1)
return false;
for (auto color : disj[i][0].mark.sets())
{
if (permut[color] != -1
&& ((unsigned) permut[color]) != new_color)
return false;
permut[color] = new_color;
}
return true;
}
return disj[i].is_parity_max_equiv(permut, new_color + 1, even);
}
}
else
{ std::sort(conj.begin(), conj.end(),
[](acc_code c1, acc_code c2)
{
(void) c2;
return c1.back().sub.op == acc_cond::acc_op::Fin;
});
unsigned i = 0;
for (; i < conj.size() - 1; i++)
{
if (conj[i].back().sub.op != acc_cond::acc_op::Fin
|| conj[i][0].mark.count() != 1)
return false;
for (auto color : conj[i][0].mark.sets())
{
if (permut[color] != -1 && permut[color != new_color])
return false;
permut[color] = new_color;
}
}
if (conj[i].back().sub.op == acc_cond::acc_op::Fin)
{
if (even)
return 0;
if (conj[i][0].mark.count() != 1)
return false;
for (auto color : conj[i][0].mark.sets())
{
if (permut[color] != -1 && permut[color != new_color])
return false;
permut[color] = new_color;
}
return true;
}
return conj[i].is_parity_max_equiv(permut, new_color + 1, even);
}
}
namespace
{
template<typename Fun>
......
......@@ -23,6 +23,8 @@
#include <sstream>
#include <vector>
#include <iostream>
#include <algorithm>
#include <numeric>
#include <spot/misc/_config.h>
#include <spot/misc/bitset.hh>
......@@ -58,12 +60,22 @@ namespace spot
class SPOT_API acc_cond
{
public:
bool
has_parity_prefix(acc_cond& new_acc, std::vector<unsigned>& colors) const;
#ifndef SWIG
private:
[[noreturn]] static void report_too_many_sets();
#endif
public:
std::vector<unsigned>
colors_inf_conj(unsigned min_nb_colors);
std::vector<unsigned>
colors_fin_disj(unsigned min_nb_colors);
/// \brief An acceptance mark
///
/// This type is used to represent a set of acceptance sets. It
......@@ -95,6 +107,9 @@ namespace spot
/// Initialize an empty mark_t.
mark_t() = default;
mark_t
apply_permutation(std::vector<unsigned> permut);
#ifndef SWIG
/// Create a mark_t from a range of set numbers.
template<class iterator>
......@@ -453,7 +468,174 @@ namespace spot
/// provided methods instead.
struct SPOT_API acc_code: public std::vector<acc_word>
{
bool operator==(const acc_code& other) const
std::vector<unsigned>
colors_inf_conj(unsigned min_nb_colors = 2)
{
auto result = std::vector<unsigned>();
auto conj = top_conjuncts();
if (conj.size() != 1)
{
std::sort(conj.begin(), conj.end(),
[](acc_code c1, acc_code c2)
{
(void)c2;
return c1.back().sub.op == acc_cond::acc_op::Inf;
});
unsigned i = 0;
while (i < conj.size())
{
acc_cond::acc_code elem = conj[i];
if (elem.back().sub.op == acc_cond::acc_op::Inf)
{
if (elem[0].mark.count() == 1)
result.insert(result.end(), elem[0].mark.min_set() - 1);
} else
break;
++i;
}
if (result.size() >= min_nb_colors)
return result;
while (i < conj.size())
{
result = conj[i].colors_inf_conj();
if (result.size() >= min_nb_colors)
return result;
result.clear();
++i;
}
}
else
{
auto disj = top_disjuncts();
if (disj.size() > 1)
{
for (auto elem : disj)
{
result = elem.colors_inf_conj();
if (result.size() >= min_nb_colors)
return result;
result.clear();
}
}
else
return {};
}
return result;
}
std::vector<unsigned>
colors_fin_disj(unsigned min_nb_colors = 2)
{
auto result = std::vector<unsigned>();
auto disj = top_disjuncts();
if (disj.size() != 1)
{
std::sort(disj.begin(), disj.end(),
[](acc_code c1, acc_code c2)
{
(void) c2;
return c1.back().sub.op == acc_cond::acc_op::Fin;
});
unsigned i = 0;
while (i < disj.size())
{
acc_cond::acc_code elem = disj[i];
if (elem.back().sub.op == acc_cond::acc_op::Fin)
{
if (elem[0].mark.count() == 1)
result.insert(result.end(), elem[0].mark.min_set() - 1);
} else
break;
++i;
}
if (result.size() >= min_nb_colors)
return result;
while (i < disj.size())
{
result = disj[i].colors_fin_disj();
if (result.size() >= min_nb_colors)
return result;
result.clear();
++i;
}
}
else
{
auto disj = top_conjuncts();
if (disj.size() > 1)
{
for (auto elem : disj)
{
result = elem.colors_fin_disj();
if (result.size() >= min_nb_colors)
return result;
result.clear();
}
}
else
return {};
}
return result;
}
bool
has_parity_prefix_aux(spot::acc_cond& new_cond,
std::vector<unsigned>& colors, std::vector<acc_code> elements,
acc_cond::acc_op op) const
{
mark_t empty_m = { };
if (elements.size() > 2)
{
new_cond = (*this);
return false;
}
if (elements.size() == 2)
{
// Vaut 1 si si c'est le 2e qui est bon
unsigned pos = elements[1].back().sub.op == op
&& elements[1][0].mark.count() == 1;
if (!(elements[0].back().sub.op == op || pos))
{
new_cond = (*this);
return false;
}
if ((elements[1 - pos].used_sets() & elements[pos][0].mark)
!= empty_m)
{
new_cond = (*this);
return false;
}
if (elements[pos][0].mark.count() != 1)
{
return false;
}
colors.push_back(elements[pos][0].mark.min_set() - 1);
elements[1 - pos].has_parity_prefix(new_cond, colors);
return true;
}
return false;
}
bool has_parity_prefix(spot::acc_cond& new_cond,
std::vector<unsigned>& colors) const
{
auto disj = top_disjuncts();
if (!
(has_parity_prefix_aux(new_cond, colors,
top_conjuncts(), acc_cond::acc_op::Fin) ||
has_parity_prefix_aux(new_cond, colors,
disj, acc_cond::acc_op::Inf)))
new_cond = spot::acc_cond(*this);
return disj.size() == 2;
}
bool
is_parity_max_equiv(std::vector<int>& permut,
unsigned new_color,
bool even) const;
bool operator==(const acc_code& other) const
{
unsigned pos = size();
if (other.size() != pos)
......@@ -1669,6 +1851,9 @@ namespace spot
/// HOA format will be accepted.
bool is_parity(bool& max, bool& odd, bool equiv = false) const;
bool is_parity_max_equiv(std::vector<int>& permut, bool even) const;
/// \brief check is the acceptance condition matches one of the
/// four type of parity acceptance defined in the HOA format.
bool is_parity() const
......@@ -1838,6 +2023,57 @@ namespace spot
return all_;
}
acc_cond
apply_permutation(std::vector<unsigned>permut)
{
return acc_cond(apply_permutation_aux(permut));
}
acc_code
apply_permutation_aux(std::vector<unsigned>permut)
{
auto conj = top_conjuncts();
auto disj = top_disjuncts();
if (conj.size() > 1)
{
auto transformed = std::vector<acc_code>();
for (auto elem : conj)
transformed.push_back(elem.apply_permutation_aux(permut));
std::sort(transformed.begin(), transformed.end());
auto uniq = std::unique(transformed.begin(), transformed.end());
auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
[](acc_code c1, acc_code c2)
{
return c1 & c2;
});
return result;
}
else if (disj.size() > 1)
{
auto transformed = std::vector<acc_code>();
for (auto elem : disj)
transformed.push_back(elem.apply_permutation_aux(permut));
std::sort(transformed.begin(), transformed.end());
auto uniq = std::unique(transformed.begin(), transformed.end());
auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
[](acc_code c1, acc_code c2)
{
return c1 | c2;
});
return result;
}
else
{
if (code_.back().sub.op == acc_cond::acc_op::Fin)
return fin(code_[0].mark.apply_permutation(permut));
if (code_.back().sub.op == acc_cond::acc_op::Inf)
return inf(code_[0].mark.apply_permutation(permut));
}
SPOT_ASSERT(false);
return {};
}
/// \brief Check whether visiting *exactly* all sets \a inf
/// infinitely often satisfies the acceptance condition.
bool accepting(mark_t inf) const
......@@ -2219,6 +2455,16 @@ namespace spot
{
return {*this};
}
inline acc_cond::mark_t
acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
{
mark_t result { };
for (auto color : sets())
if (color < permut.size())
result.set(permut[color]);
return result;
}
}
namespace std
......
......@@ -31,6 +31,15 @@ using namespace std::string_literals;
namespace spot
{
void
twa_graph::apply_permutation(std::vector<unsigned> permut)
{
for (auto& e : edges())
{
e.acc.apply_permutation(permut);
}
}
std::string twa_graph::format_state(unsigned n) const
{
if (is_univ_dest(n))
......
......@@ -219,6 +219,9 @@ namespace spot
mutable unsigned init_number_;
public:
void apply_permutation(std::vector<unsigned> permut);
twa_graph(const bdd_dict_ptr& dict)
: twa(dict),
init_number_(0)
......
......@@ -59,6 +59,7 @@ twaalgos_HEADERS = \
isunamb.hh \
isweakscc.hh \
langmap.hh \
car.hh \
lbtt.hh \
ltl2taa.hh \
ltl2tgba_fm.hh \
......@@ -128,6 +129,7 @@ libtwaalgos_la_SOURCES = \
isunamb.cc \
isweakscc.cc \
langmap.cc \
car.cc \
lbtt.cc \
ltl2taa.cc \
ltl2tgba_fm.cc \
......
This diff is collapsed.
// -*- 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
{
/// \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
car(const twa_graph_ptr &aut,
bool search_ex = true,
bool partial_degen = true,
bool scc_acc_clean = true,
bool parity_equiv = true,
bool use_last = true,
bool parity_prefix = true,
bool rabin_to_buchi = true,
bool pretty_print = false);
} // namespace spot
\ No newline at end of file
......@@ -372,6 +372,7 @@ TESTS_python = \
python/bdditer.py \
python/bddnqueen.py \
python/bugdet.py \
python/car.py \
python/complement_semidet.py \
python/declenv.py \
python/decompose_scc.py \
......
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2018, 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/>.
import spot
import time
a = spot.automaton("""
HOA: v1
name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) &
F(Gp1 | G!p0))"
States: 14
Start: 0
AP: 2 "p1" "p0"
Acceptance: 6 (Fin(0) & Fin(1)) | ((Fin(4)|Fin(5)) & (Inf(2)&Inf(3)))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0] 1
[0] 2
State: 1
[!0&!1] 1 {0 1 2 3 5}
[0&!1] 3
[!0&1] 4
[0&1] 5
State: 2
[0&!1] 2 {1}
[!0&1] 4
[!0&!1] 6
[0&1] 7
State: 3
[0&!1] 3 {1 3}
[!0&1] 4
[!0&!1] 6 {0 1 2 3 5}