From cf18c06940d22b0ca87d04902802b11a18f1e7ed Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Sat, 17 Jun 2017 19:33:26 +0200 Subject: [PATCH] twaalgos/cobuchi: Add nsa_to_nca() MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * NEWS: Update. * spot/twaalgos/cobuchi.hh: Declare to_dca() and nsa_to_nca(). * spot/twaalgos/cobuchi.cc: Implement them. * python/spot/impl.i: Include new file for python bindings. * spot/twaalgos/Makefile.am: Add new file. * bin/autfilt.cc: Add --dca command line option. This option does not return a deterministic automaton yet, but it will. * tests/core/dca.test: Add tests for Büchi automata. * tests/python/dca.py: Add a python script that builds a nondet. Streett automaton. * tests/python/dca.test: Add tests for Streett automata. * tests/Makefile.am: Add all tests. --- NEWS | 7 + bin/autfilt.cc | 14 ++ python/spot/impl.i | 4 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/cobuchi.cc | 262 ++++++++++++++++++++++++++++++++++++++ spot/twaalgos/cobuchi.hh | 91 +++++++++++++ tests/Makefile.am | 5 +- tests/core/dca.test | 199 +++++++++++++++++++++++++++++ tests/python/dca.py | 37 ++++++ tests/python/dca.test | 58 +++++++++ 10 files changed, 678 insertions(+), 1 deletion(-) create mode 100644 spot/twaalgos/cobuchi.cc create mode 100644 spot/twaalgos/cobuchi.hh create mode 100644 tests/core/dca.test create mode 100755 tests/python/dca.py create mode 100755 tests/python/dca.test diff --git a/NEWS b/NEWS index 76c98a759..3745c5629 100644 --- a/NEWS +++ b/NEWS @@ -19,6 +19,13 @@ New in spot 2.4.0.dev (not yet released) specified SCC. It must only be called on automata with a Streett-like acceptance condition. + - The new function nsa_to_nca() is able to convert when possible an + automaton with a Streett-like acceptance to an equivalent + automaton with a co-Büchi acceptance. Actually the resulting + automaton will always recognize at least the same language. It can + recognize more if the original language can not be expressed with + a co-Büchi acceptance condition. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 29a6e5333..fd81c51af 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -47,6 +47,7 @@ #include #include #include +#include #include #include #include @@ -89,6 +90,7 @@ enum { OPT_COMPLEMENT, OPT_COMPLEMENT_ACC, OPT_COUNT, + OPT_DCA, OPT_DECOMPOSE_SCC, OPT_DESTUT, OPT_DUALIZE, @@ -350,6 +352,12 @@ static const argp_option options[] = "solver can be set thanks to the SPOT_SATSOLVER environment variable" "(see spot-x)." , 0 }, + { "dca", OPT_DCA, nullptr, 0, + "convert to deterministic co-Büchi. The resulting automaton will always " + "recognize at least the same language. Actually, it can recognize " + "more if the original language can not be expressed using a co-Büchi " + "acceptance condition." + , 0 }, { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 }, { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM", @@ -511,6 +519,7 @@ static const char* opt_sat_minimize = nullptr; 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 spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) @@ -594,6 +603,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_COMPLEMENT_ACC: opt_complement_acc = true; break; + case OPT_DCA: + opt_dca = true; + break; case OPT_DECOMPOSE_SCC: opt_decompose_scc = arg; break; @@ -1190,6 +1202,8 @@ namespace aut = spot::to_generalized_rabin(aut, opt_gra == GRA_SHARE_INF); if (opt_gsa) aut = spot::to_generalized_streett(aut, opt_gsa == GSA_SHARE_FIN); + if (opt_dca) + aut = spot::to_dca(aut, false); if (opt_simplify_exclusive_ap && !opt->excl_ap.empty()) aut = opt->excl_ap.constrain(aut, true); diff --git a/python/spot/impl.i b/python/spot/impl.i index 771da0fb3..e7546eae8 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -121,6 +121,8 @@ #include #include #include +#include +#include #include #include #include @@ -537,6 +539,8 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include +%include %include %feature("flatnested") spot::twa_run::step; %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index ab43d0bab..e372d75fd 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -33,6 +33,7 @@ twaalgos_HEADERS = \ bfssteps.hh \ canonicalize.hh \ cleanacc.hh \ + cobuchi.hh \ complete.hh \ complement.hh \ compsusp.hh \ @@ -95,6 +96,7 @@ libtwaalgos_la_SOURCES = \ bfssteps.cc \ canonicalize.cc \ cleanacc.cc \ + cobuchi.cc \ complete.cc \ complement.cc \ compsusp.cc \ diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc new file mode 100644 index 000000000..e416f6b3a --- /dev/null +++ b/spot/twaalgos/cobuchi.cc @@ -0,0 +1,262 @@ +// -*- 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 . + +#include + +#include +#include +#include +#include +#include + +#include +#include + +namespace spot +{ + namespace + { + typedef std::pair pair_state_nca; + + // Helper function that returns the called 'augmented subset construction' + // of the given automaton, i.e. the product of the automaton with its + // powerset construction. + // + // 'aut_power' is the automaton that will be used for the powerset + // construction and 'aut_prod' is the one that will be used for the + // product. They may be confusing in the sense that why the same automaton + // is not used for the product and the powerset construction. Actually, + // when dealing with an automaton A with Rabin acceptance, it is firstly + // converted into an automaton B with Streett-like acceptance. The powerset + // construction of B happens to be isomorphic with the powerset construction + // of A. Therefore, you would like to use A (which is smaller than B) for + // the powerset construction and B for the product. + static + twa_graph_ptr + aug_subset_cons(const const_twa_graph_ptr& aut_prod, + const const_twa_graph_ptr& aut_power, + bool named_states, + struct power_map& pmap) + { + twa_graph_ptr res = product(aut_prod, tgba_powerset(aut_power, pmap)); + + if (named_states) + { + const product_states* res_map = res->get_named_prop + ("product-states"); + + auto v = new std::vector; + res->set_named_prop("state-names", v); + + auto get_st_name = + [&](const pair_state_nca& x) + { + std::stringstream os; + os << x.first << ",{"; + bool not_first = false; + for (auto& a : pmap.states_of(x.second)) + { + if (not_first) + os << ','; + else + not_first = true; + os << a; + } + os << '}'; + return os.str(); + }; + + unsigned num_states = res->num_states(); + for (unsigned i = 0; i < num_states; ++i) + v->emplace_back(get_st_name((*res_map)[i])); + } + return res; + } + + class nsa_to_nca_converter final + { + protected: + struct power_map pmap_; // Sets of sts (powerset cons.). + + const_twa_graph_ptr aut_; // The given automaton. + bool state_based_; // Is it state based? + std::vector pairs_; // All pairs of the acc. cond. + unsigned nb_pairs_; // Nb pair in the acc. cond. + bool named_states_; // Name states for display? + twa_graph_ptr res_; // The augmented subset const. + product_states* res_map_; // States of the aug. sub. cons. + scc_info si_; // SCC information. + unsigned nb_states_; // Number of states. + unsigned was_rabin_; // Was it Rabin before Streett? + std::vector* orig_states_; // Match old Rabin st. from new. + unsigned orig_num_st_; // Rabin original nb states. + + // Keep information of states that are wanted to be seen infinitely + // often (cf Header). + void save_inf_nca_st(unsigned s, acc_cond::mark_t m, + vect_nca_info* nca_info) + { + if (was_rabin_ && m) + { + for (unsigned p = 0; p < nb_pairs_; ++p) + if (pairs_[p].fin || m & pairs_[p].inf) + { + const pair_state_nca& st = (*res_map_)[s]; + auto bv = make_bitvect(orig_num_st_); + for (unsigned state : pmap_.states_of(st.second)) + bv->set(state); + assert(!was_rabin_ + || ((int)(*orig_states_)[st.first] >= 0)); + unsigned state = was_rabin_ ? (*orig_states_)[st.first] + : st.first; + unsigned clause_nb = was_rabin_ ? p / 2 : p; + nca_info->push_back(new nca_st_info(clause_nb, state, bv)); + } + } + else if (!was_rabin_) + { + const pair_state_nca& st = (*res_map_)[s]; + auto bv = make_bitvect(aut_->num_states()); + for (unsigned state : pmap_.states_of(st.second)) + bv->set(state); + nca_info->push_back(new nca_st_info(0, st.first, bv)); + } + } + + // Helper function that marks states that we want to see finitely often + // and save some information about states that we want to see infinitely + // often (cf Header). + void set_marks_using(std::vector& nca_is_inf_state, + vect_nca_info* nca_info) + { + for (unsigned s = 0; s < nb_states_; ++s) + { + unsigned src_scc = si_.scc_of(s); + if (nca_is_inf_state[s]) + { + acc_cond::mark_t m = 0u; + for (auto& e : res_->out(s)) + { + if (nca_info && e.acc && (si_.scc_of(e.dst) == src_scc + || state_based_)) + m |= e.acc; + e.acc = 0u; + } + + if (nca_info) + save_inf_nca_st(s, m, nca_info); + } + else + { + for (auto& e : res_->out(s)) + { + if (si_.scc_of(e.dst) == src_scc || state_based_) + e.acc = acc_cond::mark_t({0}); + else + e.acc = 0u; + } + } + } + } + + public: + + nsa_to_nca_converter(const const_twa_graph_ptr ref_prod, + const const_twa_graph_ptr ref_power, + std::vector& pairs, + bool named_states = false, + bool was_rabin = false, + unsigned orig_num_st = 0) + : aut_(ref_prod), + state_based_((bool)aut_->prop_state_acc()), + pairs_(pairs), + nb_pairs_(pairs.size()), + named_states_(named_states), + res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)), + res_map_(res_->get_named_prop("product-states")), + si_(scc_info(res_)), + nb_states_(res_->num_states()), + was_rabin_(was_rabin), + orig_num_st_(orig_num_st) + { + if (was_rabin) + orig_states_ = ref_prod->get_named_prop> + ("original-states"); + } + + ~nsa_to_nca_converter() + {} + + twa_graph_ptr run(vect_nca_info* nca_info) + { + std::vector nca_is_inf_state; // Accepting or rejecting sts. + nca_is_inf_state.resize(nb_states_, false); + + // Iterate over all SCCs and check for accepting states. A state 's' + // is accepting if there is a cycle containing 's' that visits + // finitely often all acceptance sets marked as Fin or infinitely + // often acceptance sets marked by Inf. + unsigned nb_scc = si_.scc_count(); + for (unsigned scc = 0; scc < nb_scc; ++scc) + for (unsigned st : si_.states_on_acc_cycle_of(scc)) + nca_is_inf_state[st] = true; + + set_marks_using(nca_is_inf_state, nca_info); + + res_->prop_state_acc(state_based_); + res_->set_co_buchi(); + res_->merge_edges(); + return res_; + } + }; + } + + + twa_graph_ptr + nsa_to_nca(const const_twa_graph_ptr& ref, + bool named_states, + vect_nca_info* nca_info) + { + twa_graph_ptr ref_tmp = ref->acc().is_parity() ? to_generalized_streett(ref) + : nullptr; + std::vector pairs; + if (!(ref_tmp ? ref_tmp : ref)->acc().is_streett_like(pairs)) + throw std::runtime_error("nsa_to_nca() only works with Streett-like or " + "Parity acceptance condition"); + + nsa_to_nca_converter nca_converter(ref_tmp ? ref_tmp : ref, + ref_tmp ? ref_tmp : ref, + pairs, + named_states, + false); + return nca_converter.run(nca_info); + } + + + twa_graph_ptr + to_dca(const const_twa_graph_ptr& aut, bool named_states) + { + std::vector pairs; + if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) + return nsa_to_nca(aut, named_states); + else + throw std::runtime_error("to_dca() only works with Streett-like or Parity" + " acceptance condition"); + } +} diff --git a/spot/twaalgos/cobuchi.hh b/spot/twaalgos/cobuchi.hh new file mode 100644 index 000000000..861f63544 --- /dev/null +++ b/spot/twaalgos/cobuchi.hh @@ -0,0 +1,91 @@ +// -*- 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 . + +#pragma once + +#include +#include + +#include + +namespace spot +{ + /// A vector of nca_st_info is given as argument to nsa_to_nca(). Each + /// nca_st_info has information about a state that must be seen infinitely + /// often. For a state 's' visited infinitely often by a run, the information + /// provided is: + /// - the clause number satisfied by the run (from left to right) + /// - the state number of 's' + /// - destinations of all outgoing edges of 's' (represented as a bitvect) + struct nca_st_info + { + unsigned clause_num; + unsigned state_num; + bitvect* all_dst; + + nca_st_info(unsigned clause, unsigned st, bitvect* dst) + { + clause_num = clause; + state_num = st; + all_dst = dst; + } + + ~nca_st_info() + { + delete all_dst; + } + }; + + typedef std::vector vect_nca_info; + + /// \brief Converts a nondet Streett-like aut. to a nondet. co-Büchi aut. + /// + /// This function works in top of the augmented subset construction algorithm + /// and is described in section 3.1 of: + /** \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 */ + /// This implementation is quite different from the described algorithm. It + /// is made to work with automaton with Street-like acceptance (including + /// Büchi). + /// + /// \a aut The automaton to convert. + /// \a named_states name each state for easier debugging. + /// \a nca_info retrieve information about state visited infinitely often. + SPOT_API twa_graph_ptr + nsa_to_nca(const const_twa_graph_ptr& aut, + bool named_states = false, + vect_nca_info* nca_info = nullptr); + + /// \brief Converts any ω-automata to det. co-buchi (when possible) + /// + /// The resulting automaton will always recognize at least the same language. + /// Actually, it can recognize more if the original language can not be + /// expressed using a co-Büchi acceptance condition. + SPOT_API twa_graph_ptr + to_dca(const const_twa_graph_ptr& aut, bool named_states = false); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index c23b200ad..79e3bdd42 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -299,7 +299,8 @@ TESTS_twa = \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ - core/acc_word.test + core/acc_word.test \ + core/dca.test ############################## PYTHON ############################## @@ -340,6 +341,7 @@ TESTS_python = \ python/bdditer.py \ python/bddnqueen.py \ python/bugdet.py \ + python/dca.test \ python/declenv.py \ python/decompose_scc.py \ python/dualize.py \ @@ -390,6 +392,7 @@ nb-html: $(TESTS_ipython:.ipynb=.html) EXTRA_DIST = \ $(TESTS) \ python/ltl2tgba.py \ + python/dca.py \ python/ipnbdoctest.py diff --git a/tests/core/dca.test b/tests/core/dca.test new file mode 100644 index 000000000..64641c8e7 --- /dev/null +++ b/tests/core/dca.test @@ -0,0 +1,199 @@ +#!/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 . + +. ./defs +set -e + +cat >formulas <<'EOF' +0 +F!(!b <-> FGb) +1 +a W F(a -> b) +((0 R Xa) R a) -> Fa +!Xa & (Gb R (Xa W 0)) +(1 U b) | F(Fb W (a <-> FXa)) +(a M 1) | (!a W a) +(G!a W ((b M 1) -> Fa)) -> !a +!a xor (a <-> b) +b & (a <-> b) +b +(a | b | (a -> b)) R b +Xa +!b +!Fb | !Xb +!(b | Gb) +XXX(b | Gb) +(a & F(a | FG(a W b))) U a +FGXb M (!b M b) +a +((a & !b) W Ga) W a +(b <-> FGb) M 1 +X!b +FX!(a xor !a) +Fb R (a & (a <-> b)) +XXb | (b W 0) +1 U (b xor !b) +G!(b M 1) W (1 U b) +!(Fa M Xa) + + +(!b U b) U X(!a -> Fb) +(b | (Fa R (b W a))) M 1 +1 U (a xor b) +XF!b +X(!(!b | (a M b)) -> XXa) +(FXXF(a R Fa) R Xb) U XFb +!Gb +F(Xb xor XXb) +F(XF!a & (Fb U !a)) +!b M 1 +b M Fb +!(a xor (b xor ((b W Ga) -> b))) +!(a -> (a & !a)) xor !(a U !b) +!(0 R !b) +Fa M FXb +Fa & (Fa | (!a -> Gb)) +Xb M X!a +Gb xor (b W !b) +F!(a | (b W a)) +F(1 U b) +F(!a M 1) +XF((b <-> (a <-> b)) | Fb) +F(a U !b) +(!a | b) U (1 U F(a M !b)) +!(Xb -> (b W a)) +!(0 R !X(Fb U a)) +X((a -> b) M 1) +Fb M F(a W b) +FXF(a <-> (Xb -> b)) +Xa | !((b W 0) & (a | Fb)) + + +!(F!b M 1) +X(!a W Xb) +!Fb xor G((b xor (Xa M b)) U b) +(0 R b) R (a R Xa) +Gb +a W X(b | Xb) +a W b +X(Xb & (!Ga R Ga)) +!Fb +a & GXa +XX(X(a xor b) W 0) +!a -> ((a xor !GFa) W 0) +b M Gb +Xa R XXG(!a & (Fa W Gb)) +G!b W b +G(b | G!a) +a xor ((!Xb M 1) & (b M a)) + +G(b xor (a <-> !a)) +!((a | (XXa & (a M Gb))) U b) +!(!b -> b) W a +b | !(b M 1) +G((Fa W !a) xor !(0 R b)) +0 R ((Ga xor Xb) -> (0 R a)) +G!Xa +!(X!b M a) +!(!b M a) W !a +G(a & X!Xb) +Xb -> Gb +(b | X!b) W a +b W (!b xor (!a M FXb)) + + +((b M 1) M 1) xor (a xor Ga) +b <-> (a M 1) +a xor F(!X!Fa xor (b U Xa)) +G!(!b R (Xb W b)) +(Fa & Xb) | G(b U Ga) +!(a R Gb) R !a +!(Gb U a) +(FXb & XGa) xor F(Xa M 1) +Gb <-> !((1 U a) -> b) +(a U b) & ((b U a) R FX!Ga) +Xb <-> F!a +!(a xor F(1 U Fb)) +Fa <-> G(a R b) +a | (Fb <-> XXFa) +(a U b) & (b <-> FX!b) +X!a -> (((b -> a) xor (a W 0)) M Gb) +XX!(b U (X(0 R b) R a)) +XX(Ga <-> (Xa | !(b U Xa))) +b xor Fa +(Fb M a) xor X(Fa U Fb) +b xor (Fb | (a W Gb)) +!a & X(Ga -> G(a xor b)) +(a xor XF!a) | X((a | (b R a)) -> b) +((a U XFb) W Fb) -> FX!a +X(a U Fb) -> !G!a +Fa R X(b & X(X(b R a) -> b)) +a M (G!b R Xb) +(!a R a) | (Fa xor XFb) +XF(b | Gb) M ((b R a) R !a) +!a xor (0 R ((b -> a) -> Gb)) + +(Ga | Fb) M 1 +!G(F(b & Fa) W b) +F!b -> (1 U (b W a)) +((0 R b) M 1) U XXa +1 U (b & Ga) +a & F(!b W Gb) +!((a <-> Gb) R (Fa -> Fb)) +!G(!a M 1) +FG(b & Ga) +(Xa W 0) M 1 +a xor !(Fb W Fa) +1 U (a & Ga) +a W ((a M G(0 R Fb)) -> a) +F((b -> F(a W 0)) W 0) +G(1 U Ga) +!(Fb W 0) +F(!XFXb M Xa) +b | (Gb M F(a & Fa)) +a R !(0 R G(b & Fa)) +b W F(b R a) +((a <-> b) W G!a) U !(!b M 1) +F(Fb xor !Xa) +!FX(G(1 U b) R (1 U Xa)) +X(F!Fb M Xa) +FGa +FGXb +Fa -> XXG(1 U Gb) +XXFa U Ga +a & F!X(a | XFa) +F(a | Gb) +EOF + +cat formulas | ltlcross \ + --timeout=60 \ + '{1} ltl2tgba %f >%T' \ + '{2} case `ltlfilt -f %f --format=%%[w]h` in *P*) ltl2tgba -B %f | autfilt\ + --dca ;; *) ltl2tgba -B %f;; esac >%O' + +for i in 4 5 6 7 8 9 10 +do + for acc in "min even" "min odd" "max even" "max odd"; + do + randaut -A "parity $acc $i" a b c > input.hoa + autfilt --dca input.hoa > res.hoa + autfilt input.hoa --included-in=res.hoa + done +done diff --git a/tests/python/dca.py b/tests/python/dca.py new file mode 100755 index 000000000..456b915ab --- /dev/null +++ b/tests/python/dca.py @@ -0,0 +1,37 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 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 sys +import spot + + +def gen_streett(formula): + aut = spot.translate(formula, 'BA') + aut.set_acceptance(2, 'Fin(0) | Inf(1)') + for e in aut.edges(): + if (e.acc): + e.acc = spot.mark_t([0,1]) + else: + e.acc = spot.mark_t([0]) + return aut + + +aut = gen_streett(sys.argv[1]) +print(aut.to_str('hoa')) diff --git a/tests/python/dca.test b/tests/python/dca.test new file mode 100755 index 000000000..894988951 --- /dev/null +++ b/tests/python/dca.test @@ -0,0 +1,58 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 . + +set -e + +# Skip this test if ltl2dstar is not installed. +(ltl2dstar --version) || exit 77 + +cat >ba_formulas << 'EOF' +FG((Xc & XXa) <-> !(b xor (c M b))) +F!FGFb +XF(b & Ga) +FG(F(b R Fc) R Gc) +(!c M F(b M Ga)) W (b U a) +(c xor Gb) M 1 +X!Gc M ((Fb R a) M 1) +!a | F(b W 0) +F(!a -> Gb) +(Gb <-> X(b W Xb)) M (b xor !c) +(c R (X!c W Fb)) M 1 +!a -> (FX!(0 R F(b | c)) W c) +XF((!c R a) W !Fb) +(!a <-> !(c <-> Gb)) M 1 +((0 R a) M c) M ((b xor Fb) M F(b -> a)) +EOF +cat >dsa_formulas <<'EOF' +(!b U b) U X(!a -> Fb) +1 U (a xor b) +X(!(!b | (a M b)) -> XXa) +!Gb +F(XF!a & (Fb U !a)) +EOF +while read ba_f; do + $srcdir/../run "$srcdir/dca.py" "$ba_f" > ba + while read dsa_f; do + ltldo -f "$dsa_f" "ltl2dstar --automata=streett\ + --ltl2nba=spin:ltl2tgba@-Ds" -H | autfilt --product=ba > input.hoa + autfilt --dca input.hoa > res.hoa + autfilt input.hoa --equivalent-to res.hoa + done