diff --git a/NEWS b/NEWS index d24d911fc..d63e07b4c 100644 --- a/NEWS +++ b/NEWS @@ -13,6 +13,10 @@ New in spot 2.3.0.dev (not yet released) - spot::twa_run::as_twa() has an option to preserve state names. + - the method spot::twa::is_alternating(), introduced in Spot 2.3 was + badly named and has been deprecated. Use the negation of the new + spot::twa::is_existential() instead. + Bugs fixed: - spot::otf_product() was incorrectly registering atomic diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 41ce76c9f..3142dcf84 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -485,7 +485,7 @@ static bool opt_highlight_languages = false; static spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) { - if (!(nonalt && aut->is_alternating()) && spot::is_deterministic(aut)) + if ((!nonalt || aut->is_existential()) && spot::is_deterministic(aut)) return aut; spot::postprocessor p; p.set_type(spot::postprocessor::Generic); @@ -1044,7 +1044,7 @@ namespace matched &= opt_used_ap_n.contains(aut->ap().size() - unused); } if (matched && opt_is_alternating) - matched &= aut->is_alternating(); + matched &= !aut->is_existential(); if (matched && opt_is_complete) matched &= is_complete(aut); if (matched && (opt_sccs_set | opt_art_sccs_set)) diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 5a55df9d3..5cbed97a1 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -648,7 +648,7 @@ namespace if (verbose) std::cerr << "info: getting statistics\n"; st->ok = true; - st->alternating = res->is_alternating(); + st->alternating = !res->is_existential(); spot::twa_sub_statistics s = sub_stats_reachable(res); st->states = s.states; st->edges = s.edges; @@ -1118,7 +1118,7 @@ namespace std::cerr << "info: " << prefix << i << "\t("; printsize(x[i]); std::cerr << ')'; - if (x[i]->is_alternating()) + if (!x[i]->is_existential()) std::cerr << " univ-edges"; if (is_deterministic(x[i])) std::cerr << " deterministic"; @@ -1142,7 +1142,7 @@ namespace auto unalt = [&](std::vector& x, unsigned i, char prefix) { - if (!(x[i] && x[i]->is_alternating())) + if (!x[i] || x[i]->is_existential()) return; if (verbose) { diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 4dd47b37c..31e7f264d 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -656,11 +656,23 @@ namespace spot return edges_.size() - killed_edge_ - 1; } - /// Whether the automaton is alternating + /// Whether the automaton uses only existential branching. + bool is_existential() const + { + return dests_.empty(); + } + +#ifndef SWIG + /// \brief Whether the automaton has universal branching + /// + /// The name of this function is confusing since non-deterministic + /// automata should be a subclass of alternating automata. + SPOT_DEPRECATED("use !is_existential() instead") bool is_alternating() const { - return !dests_.empty(); + return !is_existential(); } +#endif /// \brief Create a new states /// diff --git a/spot/misc/common.hh b/spot/misc/common.hh index 94ed98234..554644615 100644 --- a/spot/misc/common.hh +++ b/spot/misc/common.hh @@ -32,17 +32,21 @@ #endif #ifdef __has_cpp_attribute -# if __has_cpp_attribute(deprecated) -# define SPOT_DEPRECATED [[deprecated]] +# if __has_cpp_attribute(deprecated) && __cplusplus >= 201402L +# define SPOT_DEPRECATED(msg) [[deprecated(msg)]] +# elif __has_cpp_attribute(gnu::deprecated) +# define SPOT_DEPRECATED(msg) [[gnu::deprecated(msg)]] +# elif __has_cpp_attribute(clang::deprecated) +# define SPOT_DEPRECATED(msg) [[clang::deprecated(msg)]] # endif #endif #ifndef SPOT_DEPRECATED # ifdef __GNUC__ -# define SPOT_DEPRECATED __attribute__ ((deprecated)) +# define SPOT_DEPRECATED(msg) __attribute__ ((deprecated)) # elif defined(_MSC_VER) -# define SPOT_DEPRECATED __declspec(deprecated) +# define SPOT_DEPRECATED(msg) __declspec(deprecated) # else -# define SPOT_DEPRECATED +# define SPOT_DEPRECATED(msg) # endif #endif diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 63de3bf1d..a3a81f75c 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -2436,7 +2436,7 @@ namespace spot fix_acceptance(r); fix_initial_state(r); fix_properties(r); - if (r.h->aut && r.h->aut->is_alternating()) + if (r.h->aut && !r.h->aut->is_existential()) r.h->aut->merge_univ_dests(); return r.h; }; diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 75b6e721d..81dd490ee 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2016 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2014-2017 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -53,7 +53,7 @@ namespace spot const_twa_ptr remove_fin_maybe(const const_twa_ptr& a) { auto aa = std::dynamic_pointer_cast(a); - if ((!aa || !aa->is_alternating()) && !a->acc().uses_fin_acceptance()) + if ((!aa || aa->is_existential()) && !a->acc().uses_fin_acceptance()) return a; if (!aa) aa = make_twa_graph(a, twa::prop_set::all()); diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 04ea0cb81..28733cab6 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -86,7 +86,7 @@ namespace spot { set_named_prop("highlight-edges", nullptr); g_.remove_dead_edges_(); - if (is_alternating()) + if (!is_existential()) merge_univ_dests(); typedef graph_t::edge_storage_t tr_t; @@ -245,7 +245,7 @@ namespace spot std::vector order; order.reserve(num_states); - if (!is_alternating()) + if (is_existential()) { std::vector> todo; // state, edge useful[get_init_state_number()] = 1; @@ -399,7 +399,7 @@ namespace spot void twa_graph::defrag_states(std::vector&& newst, unsigned used_states) { - if (is_alternating()) + if (!is_existential()) { auto& g = get_graph(); auto& dests = g.dests_vector(); diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 9c3f77014..18732b7f0 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -294,7 +294,7 @@ namespace spot virtual const twa_graph_state* get_init_state() const override { unsigned n = get_init_state_number(); - if (SPOT_UNLIKELY(is_alternating())) + if (SPOT_UNLIKELY(!is_existential())) throw std::runtime_error ("the abstract interface does not support alternating automata"); return state_from_number(n); @@ -479,10 +479,23 @@ namespace spot return g_.univ_dests(e); } + /// Whether the automaton uses only existential branching. + bool is_existential() const + { + return g_.is_existential(); + } + +#ifndef SWIG + /// \brief Whether the automaton has universal branching + /// + /// The name of this function is confusing since non-deterministic + /// automata should be a subclass of alternating automata. + SPOT_DEPRECATED("use !is_existential() instead") bool is_alternating() const { - return g_.is_alternating(); + return !is_existential(); } +#endif #ifndef SWIG auto states() const diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 9af21b332..0f4f0492c 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -479,7 +479,7 @@ namespace spot twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, bool named_states) { - if (!aut->is_alternating()) + if (aut->is_existential()) // Nothing to do, why was this function called at all? return std::const_pointer_cast(aut); diff --git a/spot/twaalgos/are_isomorphic.cc b/spot/twaalgos/are_isomorphic.cc index fbb327822..4876def46 100644 --- a/spot/twaalgos/are_isomorphic.cc +++ b/spot/twaalgos/are_isomorphic.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -132,7 +132,7 @@ namespace spot bool isomorphism_checker::is_isomorphic_(const const_twa_graph_ptr aut) { - if (aut->is_alternating()) + if (!aut->is_existential()) throw std::runtime_error ("isomorphism_checker does not yet support alternation"); trival autdet = aut->prop_deterministic(); diff --git a/spot/twaalgos/canonicalize.cc b/spot/twaalgos/canonicalize.cc index 5bc93235b..9b3cbaa39 100644 --- a/spot/twaalgos/canonicalize.cc +++ b/spot/twaalgos/canonicalize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -// Developpement de l Epita (LRDE). +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -73,7 +73,7 @@ namespace spot twa_graph_ptr canonicalize(twa_graph_ptr aut) { - if (aut->is_alternating()) + if (!aut->is_existential()) throw std::runtime_error ("canonicalize does not yet support alternation"); std::vector state2class(aut->num_states(), 0); diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index fb67593f4..e38c208fc 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -1,5 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. +// Copyright (C) 2016-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -219,7 +220,7 @@ namespace spot state_t initial_state(const const_twa_graph_ptr& twa_p) { - if (twa_p->is_alternating()) + if (!twa_p->is_existential()) throw std::runtime_error ("couvreur99_new does not support alternation"); return twa_p->get_init_state_number(); diff --git a/spot/twaalgos/cycles.cc b/spot/twaalgos/cycles.cc index 2d52aaeed..90deed5b3 100644 --- a/spot/twaalgos/cycles.cc +++ b/spot/twaalgos/cycles.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2012, 2014-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -27,7 +27,7 @@ namespace spot info_(aut_->num_states(), aut_->num_states()), sm_(map) { - if (aut_->is_alternating()) + if (!aut_->is_existential()) throw std::runtime_error ("enumerate_cycles does not support alternation"); } diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 9256afc1b..175c10e83 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita. +// Copyright (C) 2012-2017 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -197,7 +197,7 @@ namespace spot if (!a->acc().is_generalized_buchi()) throw std::runtime_error ("degeneralize() can only works with generalized Büchi acceptance"); - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("degeneralize() does not support alternation"); diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 37e9ede1f..3f4f68dbf 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2015-2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -579,7 +579,7 @@ namespace spot bool pretty_print, bool use_scc, bool use_simulation, bool use_stutter) { - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("tgba_determinize() does not support alternation"); if (a->prop_deterministic()) diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 274fa9031..1fec69255 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2012, 2014-2017 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -707,7 +707,7 @@ namespace spot start(); if (si) { - if (!aut->is_alternating()) + if (aut->is_existential()) si->determine_unknown_acceptance(); unsigned sccs = si->scc_count(); diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index e9b2e029e..908e7dcd8 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -715,7 +715,7 @@ namespace spot dtba_sat_synthetize(const const_twa_graph_ptr& a, int target_state_number, bool state_based) { - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("dtba_sat_synthetize() does not support alternating automata"); if (!a->acc().is_buchi()) diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index e5ad46210..5e6ed6d1b 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -992,7 +992,7 @@ namespace spot int target_state_number, bool state_based, bool colored) { - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("dtwa_sat_synthetize() does not support alternating automata"); if (target_state_number == 0) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 7a6c416a7..469b66a32 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -445,7 +445,7 @@ namespace spot // property. The "univ-branch" property seems more important to // announce that the automaton might not be parsable by tools that // do not support alternating automata. - if (aut->is_alternating()) + if (!aut->is_existential()) { prop(" univ-branch"); } diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index c481a910c..fe22ce140 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -37,7 +37,7 @@ namespace spot // we used to have, was motivated by issue #188. bool is_unambiguous(const const_twa_graph_ptr& aut) { - if (aut->is_alternating()) + if (!aut->is_existential()) throw std::runtime_error ("is_unambiguous() does not support alternation"); diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc index b9c03cb3f..feafb2cd3 100644 --- a/spot/twaalgos/isweakscc.cc +++ b/spot/twaalgos/isweakscc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -27,7 +27,7 @@ namespace spot scc_has_rejecting_cycle(scc_info& map, unsigned scc) { auto aut = map.get_aut(); - if (aut->is_alternating()) + if (!aut->is_existential()) throw std::runtime_error ("scc_has_rejecting_cycle() does not support alternation"); // We check that by cloning the SCC and complementing its @@ -45,7 +45,7 @@ namespace spot bool is_inherently_weak_scc(scc_info& map, unsigned scc) { - if (map.get_aut()->is_alternating()) + if (!map.get_aut()->is_existential()) throw std::runtime_error ("is_inherently_weak_scc() does not support alternation"); // Weak SCCs are inherently weak. @@ -60,7 +60,7 @@ namespace spot bool is_weak_scc(scc_info& map, unsigned scc) { - if (map.get_aut()->is_alternating()) + if (!map.get_aut()->is_existential()) throw std::runtime_error ("is_weak_scc() does not support alternation"); @@ -75,7 +75,7 @@ namespace spot is_complete_scc(scc_info& map, unsigned scc) { auto a = map.get_aut(); - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("is_complete_scc() does not support alternation"); for (auto s: map.states_of(scc)) @@ -99,7 +99,7 @@ namespace spot bool is_terminal_scc(scc_info& map, unsigned scc) { - if (map.get_aut()->is_alternating()) + if (!map.get_aut()->is_existential()) throw std::runtime_error ("is_terminal_scc() does not support alternation"); diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 83b5404a5..3ce03b700 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -43,7 +43,7 @@ namespace spot twa_graph_ptr& cpy, Trans trans, unsigned int init) { - if (old->is_alternating()) + if (!old->is_existential()) throw std::runtime_error ("transform_accessible() does not support alternation"); @@ -105,7 +105,7 @@ namespace spot twa_graph_ptr& cpy, Trans trans, unsigned int init) { - if (old->is_alternating()) + if (!old->is_existential()) throw std::runtime_error ("transform_copy() does not support alternation"); diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 39685caf3..4a199fbd5 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -474,7 +474,7 @@ namespace spot twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a) { - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("minimize_monitor() does not support alternation"); @@ -495,7 +495,7 @@ namespace spot twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a) { - if (a->is_alternating()) + if (!a->is_existential()) throw std::runtime_error ("minimize_wdba() does not support alternation"); @@ -610,7 +610,7 @@ namespace spot const_twa_graph_ptr aut_neg_f, bool reject_bigger) { - if (aut_f->is_alternating()) + if (!aut_f->is_existential()) throw std::runtime_error ("minimize_obligation() does not support alternation"); diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index e9f8b6f16..2191b8924 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -182,7 +182,7 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; - if (a->is_alternating() && + if (!a->is_existential() && // We will probably have to revisit this condition later. // Currently, the intent is that postprocessor should never // return an alternating automaton, unless it is called with diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index cd3752aca..601b23a1d 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -46,7 +46,7 @@ namespace spot unsigned right_state, bool and_acc) { - if (left->is_alternating() || right->is_alternating()) + if (!(left->is_existential() && right->is_existential())) throw std::runtime_error ("product() does not support alternating automata"); std::unordered_map s2n; diff --git a/spot/twaalgos/randomize.cc b/spot/twaalgos/randomize.cc index 963751101..a38435ba9 100644 --- a/spot/twaalgos/randomize.cc +++ b/spot/twaalgos/randomize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -29,7 +29,7 @@ namespace spot randomize(twa_graph_ptr& aut, bool randomize_states, bool randomize_edges) { - if (aut->is_alternating()) + if (!aut->is_existential()) throw std::runtime_error ("randomize() does not yet support alternation"); diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 26c6919e4..87d8c90ef 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -494,7 +494,7 @@ namespace spot if (aut->prop_weak().is_true()) return remove_fin_weak(aut); - if (aut->is_alternating()) + if (!aut->is_existential()) return remove_fin(remove_alternation(aut)); if (auto maybe = streett_to_generalized_buchi_maybe(aut)) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 7ad03f0ca..b4df91026 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -29,7 +29,7 @@ namespace spot { if (old->prop_state_acc()) return old; - if (old->is_alternating()) + if (!old->is_existential()) throw std::runtime_error ("sbacc() does not support alternation"); diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 9ce0cffee..b2ca23908 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 -// Laboratoire de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -276,7 +276,7 @@ namespace spot twa_graph_ptr scc_filter_apply(const_twa_graph_ptr aut, scc_info* given_si, Args&&... args) { - if (aut->is_alternating()) + if (!aut->is_existential()) throw std::runtime_error ("scc_filter() does yet not support alternation"); diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index c806552da..c15308403 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -353,7 +353,7 @@ namespace spot void scc_info::determine_unknown_acceptance() { - if (aut_->is_alternating()) + if (!aut_->is_existential()) throw std::runtime_error("scc_info::determine_unknown_acceptance() " "does not support alternating automata"); std::vector k; diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 3db2c06f8..e59ed5e4a 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -160,7 +160,7 @@ namespace spot if (!has_separate_sets(in)) throw std::runtime_error ("direct_simulation() requires separate Inf and Fin sets"); - if (in->is_alternating()) + if (!in->is_existential()) throw std::runtime_error ("direct_simulation() does not yet support alternation"); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 926da171c..8826ee92d 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -172,7 +172,7 @@ namespace spot void check_strength(const twa_graph_ptr& aut, scc_info* si) { - if (aut->is_alternating()) + if (!aut->is_existential()) is_type_automaton(aut, si); else is_type_automaton(aut, si); diff --git a/tests/core/graph.cc b/tests/core/graph.cc index 1de3b6481..3de1d51f0 100644 --- a/tests/core/graph.cc +++ b/tests/core/graph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -225,7 +225,7 @@ f6() f += t.first; h += t.second; } - return f == 3 && (h > 2.49 && h < 2.51) && !g.is_alternating(); + return f == 3 && (h > 2.49 && h < 2.51) && g.is_existential(); } static bool @@ -247,7 +247,7 @@ f7() g.dump_storage(std::cout); - return f == 15 && g.is_alternating(); + return f == 15 && !g.is_existential(); } diff --git a/tests/core/ngraph.cc b/tests/core/ngraph.cc index 793329981..8ae18c963 100644 --- a/tests/core/ngraph.cc +++ b/tests/core/ngraph.cc @@ -264,7 +264,7 @@ static bool f6() f += t.first; h += t.second; } - return f == 3 && (h > 2.49 && h < 2.51) && !g.is_alternating(); + return f == 3 && (h > 2.49 && h < 2.51) && g.is_existential(); } static bool f7() @@ -287,7 +287,7 @@ static bool f7() for (unsigned tt: g.univ_dests(t.dst)) f += t.label * g.state_data(tt); - return f == 15 && g.is_alternating(); + return f == 15 && !g.is_existential(); } diff --git a/tests/python/alternating.py b/tests/python/alternating.py index d1bb47f9a..1ed9d1567 100755 --- a/tests/python/alternating.py +++ b/tests/python/alternating.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -40,7 +40,7 @@ tr = [(s, [[x for x in aut.univ_dests(i)] for i in aut.out(s)]) for s in range(3)] print(tr) assert [(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])] == tr -assert aut.is_alternating() +assert not aut.is_existential() received = False try: