From 96531f29f21a87877ca8f362435a36b72fad7adb Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Fri, 21 Feb 2020 11:00:47 +0100 Subject: [PATCH] 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. --- NEWS | 3 + python/spot/impl.i | 2 + spot/twa/acc.cc | 137 +++++ spot/twa/acc.hh | 248 ++++++++- spot/twa/twagraph.cc | 9 + spot/twa/twagraph.hh | 3 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/car.cc | 1043 +++++++++++++++++++++++++++++++++++++ spot/twaalgos/car.hh | 59 +++ tests/Makefile.am | 1 + tests/python/car.py | 157 ++++++ 11 files changed, 1663 insertions(+), 1 deletion(-) create mode 100644 spot/twaalgos/car.cc create mode 100644 spot/twaalgos/car.hh create mode 100644 tests/python/car.py diff --git a/NEWS b/NEWS index bff1ab036..4f689eeca 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/python/spot/impl.i b/python/spot/impl.i index 131e49a76..d9296f76f 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -162,6 +162,7 @@ #include #include #include +#include #include @@ -683,6 +684,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %pythonprepend spot::twa::dtwa_complement %{ from warnings import warn diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 9b946f48a..c6b53ef89 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -25,6 +25,7 @@ #include #include #include +#include #include #include "spot/priv/bddalloc.hh" #include @@ -1059,6 +1060,38 @@ namespace spot return res; } + bool + acc_cond::has_parity_prefix(acc_cond& new_cond, + std::vector& colors) const + { + return code_.has_parity_prefix(new_cond, colors); + } + + bool + acc_cond::is_parity_max_equiv(std::vector&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 + acc_cond::colors_inf_conj(unsigned min_nb_colors) + { + return code_.colors_inf_conj(min_nb_colors); + } + + std::vector + 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& 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 diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 10513ac87..aab9953ba 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -23,6 +23,8 @@ #include #include #include +#include +#include #include #include @@ -58,12 +60,22 @@ namespace spot class SPOT_API acc_cond { + public: + bool + has_parity_prefix(acc_cond& new_acc, std::vector& colors) const; + #ifndef SWIG private: [[noreturn]] static void report_too_many_sets(); #endif public: + std::vector + colors_inf_conj(unsigned min_nb_colors); + + std::vector + 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 permut); + #ifndef SWIG /// Create a mark_t from a range of set numbers. template @@ -453,7 +468,174 @@ namespace spot /// provided methods instead. struct SPOT_API acc_code: public std::vector { - bool operator==(const acc_code& other) const + + std::vector + colors_inf_conj(unsigned min_nb_colors = 2) + { + auto result = std::vector(); + 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 + colors_fin_disj(unsigned min_nb_colors = 2) + { + auto result = std::vector(); + 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& colors, std::vector 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& 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& 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& 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::vectorpermut) + { + return acc_cond(apply_permutation_aux(permut)); + } + + acc_code + apply_permutation_aux(std::vectorpermut) + { + auto conj = top_conjuncts(); + auto disj = top_disjuncts(); + + if (conj.size() > 1) + { + auto transformed = std::vector(); + 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(); + 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 permut) + { + mark_t result { }; + for (auto color : sets()) + if (color < permut.size()) + result.set(permut[color]); + return result; + } } namespace std diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index ee9fa13b9..37d6f7c5b 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -31,6 +31,15 @@ using namespace std::string_literals; namespace spot { + void + twa_graph::apply_permutation(std::vector permut) + { + for (auto& e : edges()) + { + e.acc.apply_permutation(permut); + } + } + std::string twa_graph::format_state(unsigned n) const { if (is_univ_dest(n)) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 090736096..bc8e42eee 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -219,6 +219,9 @@ namespace spot mutable unsigned init_number_; public: + + void apply_permutation(std::vector permut); + twa_graph(const bdd_dict_ptr& dict) : twa(dict), init_number_(0) diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 01adf944a..f3bd3d717 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -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 \ diff --git a/spot/twaalgos/car.cc b/spot/twaalgos/car.cc new file mode 100644 index 000000000..868a1d397 --- /dev/null +++ b/spot/twaalgos/car.cc @@ -0,0 +1,1043 @@ +// -*- 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 . + +#include "config.h" +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +unsigned long max_choices = 0; +unsigned long nb_choices = 0; +unsigned long total_choices = 0; + +namespace spot +{ + namespace + { +// A simple tree. Each node stores a list of children and a color or a +// state of res_. We construct a tree to find an existing state and such that +// it's easy to have the most recent among a set of compatible states. + struct node + { + // A color of the permutation or a state. + unsigned label; + std::vector children; + // is_leaf is true if the label is a state of res_. + bool is_leaf; + + node() + : node(0, 0){ } + + node(int label_, bool is_leaf_) + : label(label_) + , children(0) + , is_leaf(is_leaf_){ } + + ~node() + { + for (auto c : children) + delete c; + } + + // Add a permutation to the tree. + void + add_new_perm(std::vector permu, int pos, unsigned state) + { + if (pos == -1) + children.push_back(new node(state, true)); + else + { + auto lab = permu[pos]; + auto child = std::find_if(children.begin(), children.end(), + [lab](node* n){ return n->label == lab; }); + if (child == children.end()) + { + node* new_child = new node(lab, false); + children.push_back(new_child); + new_child->add_new_perm(permu, pos - 1, state); + } + else + (*child)->add_new_perm(permu, pos - 1, state); + } + } + + // Gives a state of res_ (if it exists) reachable from this node. + // If use_last is true, we take the most recent, otherwise we take + // the oldest. + unsigned + get_end(bool use_last) + { + if (children.empty()) + { + if (!is_leaf) + return -1U; + return label; + } + if (use_last) + return children[children.size() - 1]->get_end(use_last); + return children[0]->get_end(use_last); + } + + // Try to find a state compatible with the permu when seen_nb colors are + // moved. + unsigned + get_existing(std::vector permu, unsigned seen_nb, int pos, + bool use_last) + { + if (pos < (int) seen_nb) + return get_end(use_last); + else + { + auto lab = permu[pos]; + auto child = std::find_if(children.begin(), children.end(), + [lab](node* n){ return n->label == lab; }); + if (child == children.end()) + return -1U; + return (*child)->get_existing(permu, seen_nb, pos - 1, use_last); + } + } + }; + +// Link between a state and a car_state. We construct this structure for +// each SCC so a state is the state of the SCC and not of aut_. + class state_2_car_scc + { + // Link between a state of the SCC and a tree. + std::vector nodes; + +public: + state_2_car_scc(unsigned nb_states) + : nodes(nb_states, node()){ } + + unsigned + get_res_state(unsigned state, std::vector permu, + unsigned seen_nb, bool use_last) + { + return nodes[state].get_existing(permu, seen_nb, + permu.size() - 1, use_last); + } + + void + add_res_state(unsigned initial, unsigned state, + std::vector permu) + { + nodes[initial].add_new_perm(permu, ((int) permu.size()) - 1, state); + } + }; + + class car_generator + { + enum algorithm { + // Try to have a Büchi condition if we have Rabin. + Rabin_to_Buchi, + Streett_to_Buchi, + // IAR + IAR_Streett, + IAR_Rabin, + // CAR + CAR, + // Changing colors transforms acceptance to max even/odd copy. + Copy_even, + Copy_odd, + // If a condition is "t" or "f", we just have to copy the automaton. + False_clean, + True_clean, + None + }; + + static std::string + algorithm_to_str(algorithm algo) + { + std::string algo_str; + switch (algo) + { + case IAR_Streett: + algo_str = "IAR (Streett)"; + break; + case IAR_Rabin: + algo_str = "IAR (Rabin)"; + break; + case CAR: + algo_str = "CAR"; + break; + case Copy_even: + algo_str = "Copy even"; + break; + case Copy_odd: + algo_str = "Copy odd"; + break; + case False_clean: + algo_str = "False clean"; + break; + case True_clean: + algo_str = "True clean"; + break; + case Streett_to_Buchi: + algo_str = "Streett to Büchi"; + break; + case Rabin_to_Buchi: + algo_str = "Rabin to Büchi"; + break; + default: + algo_str = "None"; + break; + } + return algo_str; + } + + using perm_t = std::vector; + struct car_state + { + // State of the original automaton + unsigned state; + // We create a new automaton for each SCC of the original automaton + // so we keep a link between a car_state and the state of the + // subautomaton. + unsigned state_scc; + // Permutation used by IAR and CAR. + perm_t perm; + + bool + operator<(const car_state &other) const + { + if (state < other.state) + return true; + if (state > other.state) + return false; + if (perm < other.perm) + return true; + if (perm > other.perm) + return false; + return state_scc < other.state_scc; + } + + std::string + to_string(algorithm algo) const + { + std::stringstream s; + s << state; + unsigned ps = perm.size(); + if (ps > 0) + { + s << " ["; + for (unsigned i = 0; i != ps; ++i) + { + if (i > 0) + s << ','; + s << perm[i]; + } + s << ']'; + } + s << ", "; + s << algorithm_to_str(algo); + return s.str(); + } + }; + + const acc_cond::mark_t & + fin(std::vector pairs, unsigned k, + algorithm algo) const + { + if (algo == IAR_Rabin) + return pairs[k].fin; + else + return pairs[k].inf; + } + + acc_cond::mark_t + inf(std::vector pairs, unsigned k, + algorithm algo) const + { + if (algo == IAR_Rabin) + return pairs[k].inf; + else + return pairs[k].fin; + } + + // Create a permutation for the first state of a SCC (IAR) + void + initial_perm_iar(std::set &perm_elem, perm_t &p0, + algorithm algo, const acc_cond::mark_t &colors, + const std::vector &pairs) + { + for (unsigned k = 0; k != pairs.size(); ++k) + if (!inf(pairs, k, algo) || (colors & (pairs[k].fin | pairs[k].inf))) + { + perm_elem.insert(k); + p0.push_back(k); + } + } + + // Create a permutation for the first state of a SCC (CAR) + void + initial_perm_car(perm_t &p0, const acc_cond::mark_t &colors) + { + auto cont = colors.sets(); + p0.assign(cont.begin(), cont.end()); + } + + void + find_new_perm_iar(perm_t &new_perm, + const std::vector &pairs, + const acc_cond::mark_t &acc, + algorithm algo, const std::set &perm_elem, + unsigned &seen_nb) + { + for (unsigned k : perm_elem) + if (acc & fin(pairs, k, algo)) + { + ++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); + } + } + + // Given the set acc of colors appearing on an edge, create a new + // permutation new_perm, and give the number seen_nb of colors moved to + // the head of the permutation. + void + find_new_perm_car(perm_t &new_perm, const acc_cond::mark_t &acc, + unsigned &seen_nb, unsigned &h) + { + for (unsigned k : acc.sets()) + { + auto it = std::find(new_perm.begin(), new_perm.end(), k); + if (it != new_perm.end()) + { + h = std::max(h, unsigned(it - new_perm.begin()) + 1); + std::rotate(new_perm.begin(), it, it + 1); + ++seen_nb; + } + } + } + + void + get_acceptance_iar(algorithm algo, const perm_t ¤t_perm, + const std::vector &pairs, + const acc_cond::mark_t &e_acc, acc_cond::mark_t &acc) + { + unsigned delta_acc = (algo == IAR_Streett) && is_odd; + + // 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(pairs, pk, + algo) + || (e_acc & (pairs[pk].fin | pairs[pk].inf))) + { + maxint = k; + break; + } + } + unsigned value; + + if (maxint == -1U) + value = delta_acc; + else if (e_acc & fin(pairs, current_perm[maxint], algo)) + value = 2 * maxint + 2 + delta_acc; + else + value = 2 * maxint + 1 + delta_acc; + acc = { value }; + max_color = std::max(max_color, value); + } + + void + get_acceptance_car(const acc_cond &sub_aut_cond, const perm_t &new_perm, + unsigned h, acc_cond::mark_t &acc) + { + acc_cond::mark_t m(new_perm.begin(), new_perm.begin() + h); + bool rej = !sub_aut_cond.accepting(m); + unsigned value = 2 * h + rej + is_odd; + acc = { value }; + max_color = std::max(max_color, value); + } + + // Copy the given automaton and add 0 or 1 to all transitions. + void + apply_false_true_clean(const twa_graph_ptr &sub_automaton, bool is_true, + std::vector inf_fin_prefix, unsigned max_free_color) + { + std::vector* init_states = sub_automaton + ->get_named_prop>("original-states"); + + for (unsigned state = 0; state < sub_automaton->num_states(); ++state) + { + unsigned s_aut = (*init_states)[state]; + + car_state new_car = { s_aut, state, perm_t() }; + auto new_state = res_->new_state(); + car2num[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + algorithm algo = is_true ? True_clean : False_clean; + if (pretty_print) + names->push_back(new_car.to_string(algo)); + state2car[s_aut] = new_car; + } + for (unsigned state = 0; state < sub_automaton->num_states(); ++state) + { + auto col = is_true ^ !is_odd; + if (((unsigned) col) > max_free_color) + throw std::runtime_error("CAR needs more sets"); + unsigned s_aut = (*init_states)[state]; + car_state src = { s_aut, state, perm_t() }; + unsigned src_state = car2num[src]; + for (auto e : aut_->out(s_aut)) + { + for (auto c : e.acc.sets()) + { + if (inf_fin_prefix[c] + is_odd > col) + col = inf_fin_prefix[c] + is_odd; + } + acc_cond::mark_t cond = { (unsigned) col }; + max_color = std::max(max_color, (unsigned) col); + if (scc_.scc_of(s_aut) == scc_.scc_of(e.dst)) + res_->new_edge(src_state, car2num[state2car[e.dst]], e.cond, + cond); + } + } + } + + void + apply_lar(const twa_graph_ptr &sub_automaton, unsigned init, + const std::vector &pairs, + algorithm algo, unsigned scc_num, std::vector inf_fin_prefix, + unsigned max_free_color) + { + auto state_2_car = state_2_car_scc(sub_automaton->num_states()); + std::vector* init_states = sub_automaton-> + get_named_prop>("original-states"); + std::deque todo; + auto get_state = + [&](const car_state &s){ + auto it = car2num.find(s); + + if (it == car2num.end()) + { + unsigned nb = res_->new_state(); + if (search_ex) + state_2_car.add_res_state(s.state_scc, nb, s.perm); + car2num[s] = nb; + num2car.insert(num2car.begin() + nb, s); + + todo.push_back(s); + if (pretty_print) + names->push_back(s.to_string(algo)); + return nb; + } + return it->second; + }; + + auto colors = sub_automaton->acc().get_acceptance().used_sets(); + std::set perm_elem; + + perm_t p0 = { }; + switch (algo) + { + case IAR_Streett: + case IAR_Rabin: + initial_perm_iar(perm_elem, p0, algo, colors, pairs); + break; + case CAR: + initial_perm_car(p0, colors); + break; + default: + assert(false); + break; + } + + car_state s0{ (*init_states)[init], init, p0 }; + get_state(s0); // put s0 in todo + + // the main loop + while (!todo.empty()) + { + car_state current = todo.front(); + todo.pop_front(); + + unsigned src_num = get_state(current); + + for (const auto &e : sub_automaton->out(current.state_scc)) + { + 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 + unsigned h = 0; + + switch (algo) + { + case IAR_Rabin: + case IAR_Streett: + find_new_perm_iar(new_perm, pairs, e.acc, algo, + perm_elem, seen_nb); + break; + case CAR: + find_new_perm_car(new_perm, e.acc, seen_nb, h); + break; + default: + assert(false); + } + + // 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 car_state + // that matches this condition. + + car_state dst; + unsigned dst_num = -1U; + + if (search_ex) + { + dst_num = state_2_car.get_res_state(e.dst, new_perm, seen_nb, + use_last); + } + + if (dst_num == -1U) + { + auto dst = car_state{ (*init_states)[e.dst], e.dst, new_perm }; + dst_num = get_state(dst); + } + + acc_cond::mark_t acc = { }; + + switch (algo) + { + case IAR_Rabin: + case IAR_Streett: + get_acceptance_iar(algo, current.perm, pairs, e.acc, acc); + break; + case CAR: + get_acceptance_car(sub_automaton->acc(), new_perm, h, acc); + break; + default: + assert(false); + } + + unsigned acc_col = acc.min_set() - 1; + if (parity_prefix) + { + if (acc_col > max_free_color) + throw std::runtime_error("CAR needs more sets"); + // parity prefix + for (auto col : e.acc.sets()) + { + if (inf_fin_prefix[col] + is_odd > (int) acc_col) + { + max_color = std::max(max_color, + (unsigned) inf_fin_prefix[col] + is_odd); + acc_col = (unsigned) inf_fin_prefix[col] + is_odd; + } + } + } + res_->new_edge(src_num, dst_num, e.cond, { acc_col }); + } + } + auto leaving_edge = + [&](unsigned d){ + return scc_.scc_of(num2car.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(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.scc_count() != 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() >= sub_automaton->num_states()); + + // update state2car + for (unsigned scc_state : sub_scc.states_of(bscc)) + { + car_state &car = num2car.at(scc_state); + + if (state2car.find(car.state) == state2car.end()) + state2car[car.state] = car; + } + } + + // Copy a given automaton replacing i by permut[i]. + void + apply_copy(const twa_graph_ptr &sub_automaton, + const std::vector &permut, + bool copy_odd, std::vector inf_fin_prefix) + { + std::vector* init_states = sub_automaton + ->get_named_prop>("original-states"); + for (unsigned state = 0; state < sub_automaton->num_states(); ++state) + { + car_state new_car = { (*init_states)[state], state, perm_t() }; + auto new_state = res_->new_state(); + car2num[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + state2car[(*init_states)[state]] = new_car; + if (pretty_print) + names->push_back( + new_car.to_string(copy_odd ? Copy_odd : Copy_even)); + } + auto cond_col = sub_automaton->acc().get_acceptance().used_sets(); + for (unsigned s = 0; s < sub_automaton->num_states(); ++s) + { + for (auto e : sub_automaton->out(s)) + { + acc_cond::mark_t mark = { }; + int max_edge = -1; + for (auto col : e.acc.sets()) + { + if (cond_col.has(col)) + max_edge = std::max(max_edge, (int) permut[col]); + if (inf_fin_prefix[col] + is_odd > max_edge) + max_edge = inf_fin_prefix[col] + is_odd; + } + if (max_edge != -1) + { + mark.set((unsigned) max_edge); + max_color = std::max(max_color, (unsigned) max_edge); + } + car_state src = { (*init_states)[s], s, perm_t() }, + dst = { (*init_states)[e.dst], e.dst, perm_t() }; + unsigned src_state = car2num[src], + dst_state = car2num[dst]; + res_->new_edge(src_state, dst_state, e.cond, mark); + } + } + } + + void apply_to_Buchi(twa_graph_ptr sub_automaton, + bool is_streett_to_buchi, std::vector inf_fin_prefix, + unsigned max_free_color) + { + // TODO: Régler ça. + (void) inf_fin_prefix; + (void) max_free_color; + + std::vector* init_states = sub_automaton + ->get_named_prop>("original-states"); + auto sub_cond = sub_automaton->get_acceptance(); + if (is_streett_to_buchi) + sub_automaton->set_acceptance(sub_cond.complement()); + auto buchi = rabin_to_buchi_if_realizable(sub_automaton); + if (is_streett_to_buchi) + { + max_color = std::max(max_color, 2U); + sub_automaton->set_acceptance(sub_cond); + } + + for (unsigned state = 0; state < buchi->num_states(); ++state) + { + car_state new_car = { (*init_states)[state], state, perm_t() }; + auto new_state = res_->new_state(); + car2num[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + state2car[(*init_states)[state]] = new_car; + if (pretty_print) + names->push_back(new_car.to_string( + is_streett_to_buchi ? Streett_to_Buchi : Rabin_to_Buchi)); + } + for (unsigned s = 0; s < buchi->num_states(); ++s) + { + for (auto e : buchi->out(s)) + { + auto acc = e.acc; + acc <<= (is_odd + is_streett_to_buchi); + if ((is_odd || is_streett_to_buchi) && acc == acc_cond::mark_t{}) + acc = { (is_streett_to_buchi && is_odd) }; + car_state src = { (*init_states)[s], s, perm_t() }, + dst = { (*init_states)[e.dst], e.dst, perm_t() }; + unsigned src_state = car2num[src], + dst_state = car2num[dst]; + res_->new_edge(src_state, dst_state, e.cond, acc); + } + } + } + + // Given an automaton, determine the algorithm that we will apply + algorithm + chooseAlgo(twa_graph_ptr &sub_automaton, + std::vector &pairs, + std::vector &permut) + { + auto scc_condition = sub_automaton->acc(); + if (parity_equiv) + { + if (scc_condition.is_f()) + return False_clean; + if (scc_condition.is_t()) + return True_clean; + auto permut_tmp = std::vector( + scc_condition.all_sets().max_set(), -1); + + if (!is_odd && scc_condition.is_parity_max_equiv(permut_tmp, true)) + { + for (auto c : permut_tmp) + permut.push_back((unsigned) c); + + scc_condition.apply_permutation(permut); + sub_automaton->apply_permutation(permut); + return Copy_even; + } + std::fill(permut_tmp.begin(), permut_tmp.end(), -1); + if (scc_condition.is_parity_max_equiv(permut_tmp, false)) + { + for (auto c : permut_tmp) + permut.push_back((unsigned) c); + scc_condition.apply_permutation(permut); + sub_automaton->apply_permutation(permut); + return Copy_odd; + } + } + + if (rabin_to_buchi) + { + if (rabin_to_buchi_if_realizable(sub_automaton) != nullptr) + { + return Rabin_to_Buchi; + } + else + { + bool streett_buchi = false; + auto sub_cond = sub_automaton->get_acceptance(); + sub_automaton->set_acceptance(sub_cond.complement()); + streett_buchi = + (rabin_to_buchi_if_realizable(sub_automaton) != nullptr); + sub_automaton->set_acceptance(sub_cond); + if (streett_buchi) + { + return Streett_to_Buchi; + } + } + } + + auto pairs1 = std::vector(); + auto pairs2 = std::vector(); + std::sort(pairs1.begin(), pairs1.end()); + pairs1.erase(std::unique(pairs1.begin(), pairs1.end()), pairs1.end()); + std::sort(pairs2.begin(), pairs2.end()); + pairs2.erase(std::unique(pairs2.begin(), pairs2.end()), pairs2.end()); + bool is_r_like = scc_condition.is_rabin_like(pairs1); + bool is_s_like = scc_condition.is_streett_like(pairs2); + unsigned num_cols = scc_condition.get_acceptance().used_sets().count(); + if (is_r_like) + { + if ((is_s_like && pairs1.size() < pairs2.size()) || !is_s_like) + { + if (pairs1.size() > num_cols) + return CAR; + pairs = pairs1; + return IAR_Rabin; + } + else if (is_s_like) + { + if (pairs2.size() > num_cols) + return CAR; + pairs = pairs2; + return IAR_Streett; + } + } + else + { + if (is_s_like) + { + if (pairs2.size() > num_cols) + return CAR; + pairs = pairs2; + return IAR_Streett; + } + } + return CAR; + } + + void + build_scc(twa_graph_ptr &sub_automaton, unsigned scc_num, + std::vector inf_fin_prefix, unsigned max_free_color) + { + unsigned init = 0; + + std::vector pairs = { }; + auto permut = std::vector(); + auto algo = chooseAlgo(sub_automaton, pairs, permut); + if ((algo == IAR_Rabin || algo == Copy_odd) && !is_odd) + { + is_odd = true; + ++max_color; + for (auto &edge : res_->edges()) + { + if (edge.acc == acc_cond::mark_t{}) + edge.acc = {0}; + else + edge.acc <<= 1; + } + } + switch (algo) + { + case False_clean: + case True_clean: + apply_false_true_clean(sub_automaton, (algo == True_clean), + inf_fin_prefix, max_free_color); + break; + case IAR_Streett: + case IAR_Rabin: + case CAR: + apply_lar(sub_automaton, init, pairs, algo, scc_num, + inf_fin_prefix, max_free_color); + break; + case Copy_odd: + case Copy_even: + apply_copy(sub_automaton, permut, algo == Copy_odd, + inf_fin_prefix); + break; + case Rabin_to_Buchi: + case Streett_to_Buchi: + apply_to_Buchi(sub_automaton, (algo == Streett_to_Buchi), + inf_fin_prefix, max_free_color); + break; + default: + break; + } + } + +public: + twa_graph_ptr + run() + { + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + for (unsigned scc = 0; scc < scc_.scc_count(); ++scc) + { + if (!scc_.is_useful_scc(scc)) + continue; + auto sub_automata = scc_.split_on_sets(scc, { }, true); + if (sub_automata.empty()) + { + for (auto state : scc_.states_of(scc)) + { + auto new_state = res_->new_state(); + car_state new_car = { state, state, perm_t() }; + car2num[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + if (pretty_print) + names->push_back(new_car.to_string(None)); + state2car[state] = new_car; + } + continue; + } + auto sub_automaton = sub_automata[0]; + if (scc_acc_clean) + { + simplify_acceptance_here(sub_automaton); + } + if (partial_degen) + { + sub_automaton = partial_degeneralize(sub_automaton); + simplify_acceptance_here(sub_automaton); + } + std::vector parity_prefix_colors (SPOT_MAX_ACCSETS, -1); + unsigned min_prefix_color = SPOT_MAX_ACCSETS; + if (parity_prefix) + { + auto new_acc = sub_automaton->acc(); + auto colors = std::vector(); + bool inf_start = + sub_automaton->acc().has_parity_prefix(new_acc, colors); + sub_automaton->set_acceptance(new_acc); + for (unsigned i = 0; i < colors.size(); ++i) + parity_prefix_colors[colors[i]] = + SPOT_MAX_ACCSETS - 2 - i - !inf_start; + min_prefix_color = + SPOT_MAX_ACCSETS - 2 - colors.size() - 1 - !inf_start; + } + build_scc(sub_automaton, scc, parity_prefix_colors, + min_prefix_color - 1); + } + + for (unsigned state = 0; state < res_->num_states(); ++state) + { + unsigned original_state = num2car.at(state).state; + auto state_scc = scc_.scc_of(original_state); + for (auto edge : aut_->out(original_state)) + { + if (scc_.scc_of(edge.dst) != state_scc) + { + auto car = state2car.find(edge.dst); + if (car != state2car.end()) + { + unsigned res_dst = car2num.at(car->second); + res_->new_edge(state, res_dst, edge.cond, { }); + } + } + } + } + unsigned initial_state = aut_->get_init_state_number(); + auto initial_car = state2car.find(initial_state); + auto initial_state_res = car2num.find(initial_car->second); + if (initial_state_res != car2num.end()) + res_->set_init_state(initial_state_res->second); + else + res_->new_state(); + res_->set_acceptance( + acc_cond::acc_code::parity_max(is_odd, max_color + 1)); + if (pretty_print) + res_->set_named_prop("state-names", names); + reduce_parity_here(res_); + res_->purge_unreachable_states(); + return res_; + } + + explicit car_generator(const const_twa_graph_ptr &a, bool search_ex, + bool partial_degen, bool scc_acc_clean, + bool parity_equiv, bool use_last, bool parity_prefix, + bool rabin_to_buchi, bool pretty_print) + : aut_(a) + , scc_(scc_info(a)) + , is_odd(false) + , max_color(0) + , search_ex(search_ex) + , partial_degen(partial_degen) + , scc_acc_clean(scc_acc_clean) + , parity_equiv(parity_equiv) + , use_last(use_last) + , parity_prefix(parity_prefix) + , rabin_to_buchi(rabin_to_buchi) + , pretty_print(pretty_print) + { + if (pretty_print) + names = new std::vector(); + else + names = nullptr; + } + +private: + // Automaton to transform + const const_twa_graph_ptr &aut_; + // scc_info of aut + const scc_info scc_; + // Result + twa_graph_ptr res_; + // true if the acceptance condition of the result is max odd, + // false otherwise + bool is_odd; + // The maximum color appearing in the result + unsigned max_color; + + // Link between a state of res_ and a car_state + std::vector num2car; + // Link between a state of aut_ and a car_state + std::map state2car; + // Link between a car_state and a state of aut_ + std::map car2num; + + // Options : + // When we move several elements, we can try to find an order + // such that the new permutation already exists. + const bool search_ex; + // Apply a partial degeneralization to remove occurences + // of Fin | Fin and Inf & Inf. + const bool partial_degen; + // Remove for each SCC the colors that don't appear. It implies that we + // can use different algorithms for each SCC. + const bool scc_acc_clean; + // Check if there exists a permutations of colors such that the acceptance + // condition is a partity condition. + const bool parity_equiv; + // Use the most recent state when looking for an existing state. + const bool use_last; + // Try to "copy" the part of the acceptance condition similar to parity. + const bool parity_prefix; + + const bool rabin_to_buchi; + + // Give a name to the states describing the state of the aut_ and the + // permutation. + const bool pretty_print; + + // Names of the states. + std::vector* names; + }; + } // namespace + + twa_graph_ptr + remove_false_transitions(const twa_graph_ptr a) + { + auto res_ = make_twa_graph(a->get_dict()); + res_->copy_ap_of(a); + for (unsigned state = 0; state < a->num_states(); ++state) + res_->new_state(); + for (unsigned state = 0; state < a->num_states(); ++state) + for (auto edge : a->out(state)) + if (edge.cond != bddfalse) + res_->new_edge(state, edge.dst, edge.cond, edge.acc); + res_->set_init_state(a->get_init_state_number()); + res_->set_acceptance(a->get_acceptance()); + return res_; + } + + twa_graph_ptr + car(const twa_graph_ptr &aut, + bool search_ex, + bool partial_degen, + bool scc_acc_clean, bool parity_equiv, bool use_last, bool parity_prefix, + bool rabin_to_buchi, bool pretty_print) + { + auto new_aut = remove_false_transitions(aut); + return car_generator(new_aut, search_ex, partial_degen, scc_acc_clean, + parity_equiv, use_last, parity_prefix, + rabin_to_buchi, pretty_print) + .run(); + } +} // namespace spot \ No newline at end of file diff --git a/spot/twaalgos/car.hh b/spot/twaalgos/car.hh new file mode 100644 index 000000000..6ab450cce --- /dev/null +++ b/spot/twaalgos/car.hh @@ -0,0 +1,59 @@ +// -*- 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 . + +#pragma once + +#include + +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 diff --git a/tests/Makefile.am b/tests/Makefile.am index 30a46d9a0..7fafd738d 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/python/car.py b/tests/python/car.py new file mode 100644 index 000000000..3d15b1fd4 --- /dev/null +++ b/tests/python/car.py @@ -0,0 +1,157 @@ +#!/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 . + +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} +[0&1] 8 +State: 4 +[!0&!1] 4 {1 2 3 5} +[!0&1] 4 {2 4 5} +[0&!1] 5 {1 3} +[0&1] 5 {4} +State: 5 +[!0&1] 4 {2 4 5} +[0&!1] 5 {1 3} +[0&1] 8 {2 4} +[!0&!1] 9 {1 2 3 5} +State: 6 +[0&!1] 3 {1 3} +[!0&1] 4 +[0&1] 5 +[!0&!1] 10 +State: 7 +[!0&1] 4 +[0&!1] 7 {1 3} +[!0&!1] 11 +[0&1] 12 {0 4} +State: 8 +[!0&1] 4 {2 4 5} +[0&1] 5 {4} +[0&!1] 8 {1 3} +[!0&!1] 11 {1 3 5} +State: 9 +[!0&1] 4 {2 4 5} +[0&!1] 5 {1 3} +[0&1] 5 {4} +[!0&!1] 11 {1 3 5} +State: 10 +[!0&1] 4 +[0&1] 8 +[!0&!1] 10 {0 1 2 3 5} +[0&!1] 13 {1 2 3} +State: 11 +[!0&1] 4 {2 4 5} +[0&!1] 8 {1 2 3} +[0&1] 8 {2 4} +[!0&!1] 11 {1 2 3 5} +State: 12 +[!0&1] 4 +[0&1] 7 {0 2 4} +[!0&!1] 9 +[0&!1] 12 {1 3} +State: 13 +[!0&1] 4 +[0&1] 5 +[!0&!1] 10 {0 1 3 5} +[0&!1] 13 {1 3} +--END--""") +scc_ = spot.scc_info(a) +spot.partial_degeneralize(scc_.split_on_sets(2, [])[0]) + + +a = spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 5 (Inf(0)&Inf(1)) | ((Fin(2)|Fin(3)) & Fin(4)) +--BODY-- +State: 0 +[!0 & 1] 0 {2 3} +[!0 & !1] 0 {3} +[0] 1 +State: 1 +[0&1] 1 {1 2 4} +[0&!1] 1 {4} +[!0&1] 1 {0 1 2 3} +[!0&!1] 1 {0 3} +--END--""") +p = spot.car(a, False, False, False, False, False, False, True) +assert spot.are_equivalent(a, p) +a = spot.automaton(""" +HOA: v1 States: 6 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 Inf(5) | +Fin(2) | Inf(1) | (Inf(0) & Fin(3)) | Inf(4) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} +[!0&!1] 3 {3 5} State: 1 [0&!1] 3 {1 5} [!0&!1] 5 {0 1} State: 2 [!0&!1] +0 {0 3} [0&!1] 1 {0} State: 3 [!0&1] 4 {1 2 3} [0&1] 3 {3 4 5} State: +4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END-- +""") +p = spot.car(a, False, False, False, False, False, False, True) +if (not p.num_states() == 8): + print(p.num_states()) +assert spot.are_equivalent(a, p) + +for f in spot.randltl(15, 1000): + print(f) + d = spot.translate(f, "det", "G") + p = spot.car(d, False, False, False, False, False, False, True) + p2 = spot.car(d, False, False, False, False, False, False, True) + if(not spot.are_equivalent(p, d)): + print(f) + assert(False) + +for f in spot.randltl(5, 10000): + print(f) + n = spot.translate(f) + p = spot.car(n, False, False, False, False, False, False, True) + assert(spot.are_equivalent(n, p)) + +a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') +b = spot.car(a, False, False, False, False, False, False, True) +assert spot.are_equivalent(a, b)