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

is_alternating() -> !is_existential()

Browse source 
Part of #212.

* spot/misc/common.hh (SPOT_DEPRECATED): Improve support current
compilers and options flags.
* spot/twa/twagraph.hh, spot/graph/graph.hh (is_alternating): Mark it
as deprecated.
(is_existential): New method.
* bin/autfilt.cc, bin/ltlcross.cc, spot/parseaut/parseaut.yy,
spot/twa/twa.cc, spot/twa/twagraph.cc, spot/twaalgos/alternation.cc,
spot/twaalgos/are_isomorphic.cc, spot/twaalgos/canonicalize.cc,
spot/twaalgos/couvreurnew.cc, spot/twaalgos/cycles.cc,
spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc,
spot/twaalgos/dot.cc, spot/twaalgos/dtbasat.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
spot/twaalgos/mask.hh, spot/twaalgos/minimize.cc,
spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
spot/twaalgos/randomize.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/sccinfo.cc, spot/twaalgos/simulation.cc,
spot/twaalgos/strength.cc, tests/core/graph.cc, tests/core/ngraph.cc,
tests/python/alternating.py: Adjust all uses.
* NEWS: Mention the renaming.
This commit is contained in:
Alexandre Duret-Lutz 2017-02-12 13:36:35 +01:00
parent 7f7d078f2f
commit fefb375d5f
36 changed files with 127 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

16
spot/graph/graph.hh
View file

@ -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
///

14
spot/misc/common.hh
View file

@ -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

2
spot/parseaut/parseaut.yy
View file

@ -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;
};

4
spot/twa/twa.cc
View file

@ -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<const twa_graph>(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());

6
spot/twa/twagraph.cc
View file

@ -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<unsigned> order;
order.reserve(num_states);
if (!is_alternating())
if (is_existential())
{
std::vector<std::pair<unsigned, unsigned>> todo; // state, edge
useful[get_init_state_number()] = 1;
@ -399,7 +399,7 @@ namespace spot
void twa_graph::defrag_states(std::vector<unsigned>&& newst,
unsigned used_states)
{
if (is_alternating())
if (!is_existential())
{
auto& g = get_graph();
auto& dests = g.dests_vector();

17
spot/twa/twagraph.hh
View file

@ -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

2
spot/twaalgos/alternation.cc
View file

@ -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<twa_graph>(aut);

6
spot/twaalgos/are_isomorphic.cc
View file

@ -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();

6
spot/twaalgos/canonicalize.cc
View file

@ -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<unsigned> state2class(aut->num_states(), 0);

5
spot/twaalgos/couvreurnew.cc
View file

@ -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();

6
spot/twaalgos/cycles.cc
View file

@ -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");
}

6
spot/twaalgos/degen.cc
View file

@ -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");

4
spot/twaalgos/determinize.cc
View file

@ -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())

6
spot/twaalgos/dot.cc
View file

@ -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();

2
spot/twaalgos/dtbasat.cc
View file

@ -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())

2
spot/twaalgos/dtwasat.cc
View file

@ -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)

4
spot/twaalgos/hoa.cc
View file

@ -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");
}

6
spot/twaalgos/isunamb.cc
View file

@ -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");

14
spot/twaalgos/isweakscc.cc
View file

@ -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");

6
spot/twaalgos/mask.hh
View file

@ -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");

10
spot/twaalgos/minimize.cc
View file

@ -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");

6
spot/twaalgos/postproc.cc
View file

@ -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

6
spot/twaalgos/product.cc
View file

@ -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<product_state, unsigned, product_state_hash> s2n;

4
spot/twaalgos/randomize.cc
View file

@ -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");

6
spot/twaalgos/remfin.cc
View file

@ -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))

6
spot/twaalgos/sbacc.cc
View file

@ -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");

6
spot/twaalgos/sccfilter.cc
View file

@ -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");

6
spot/twaalgos/sccinfo.cc
View file

@ -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<bool> k;

6
spot/twaalgos/simulation.cc
View file

@ -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");

2
spot/twaalgos/strength.cc
View file

@ -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<false, false, true>(aut, si);
else
is_type_automaton<true, true, true>(aut, si);