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

Fix various typos

Browse source 
* bin/autfilt.cc, bin/common_post.cc, spot/graph/graph.hh,
  spot/twa/twa.hh, spot/twa/twagraph.hh, spot/twaalgos/remfin.cc: typos
* spot/twaalgos/toweak.cc: incorrect types when invoking std::hash
This commit is contained in:
Maximilien Colange 2017-10-11 15:08:48 +02:00
parent 62b86d3049
commit 5b2ce2736b
7 changed files with 77 additions and 77 deletions
Download patch file Download diff file Expand all files Collapse all files

2
bin/autfilt.cc
View file

@ -212,7 +212,7 @@ static const argp_option options[] =
"keep automata whose languages are included in that of the " "keep automata whose languages are included in that of the "
"automaton from FILENAME", 0 }, "automaton from FILENAME", 0 },
{ "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0, { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
"keep automata thare are equivalent (language-wise) to the automaton " "keep automata that are equivalent (language-wise) to the automaton "
"in FILENAME", 0 }, "in FILENAME", 0 },
{ "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 }, { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
{ "states", OPT_STATES, "RANGE", 0, { "states", OPT_STATES, "RANGE", 0,

4
bin/common_post.cc
View file

@ -67,7 +67,7 @@ static constexpr const argp_option options[] =
OPTION_ARG_OPTIONAL, OPTION_ARG_OPTIONAL,
"colored automaton with parity acceptance", 0, }, "colored automaton with parity acceptance", 0, },
{ "cobuchi", OPT_COBUCHI, nullptr, 0, { "cobuchi", OPT_COBUCHI, nullptr, 0,
"automaton with co-Büchi acceptance (will recognize" "automaton with co-Büchi acceptance (will recognize "
"a superset of the input language if not co-Büchi " "a superset of the input language if not co-Büchi "
"realizable)", 0 }, "realizable)", 0 },
{ "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
@ -130,7 +130,7 @@ static const argp_option options_disabled[] =
OPTION_ARG_OPTIONAL, OPTION_ARG_OPTIONAL,
"colored automaton with parity acceptance", 0, }, "colored automaton with parity acceptance", 0, },
{ "cobuchi", OPT_COBUCHI, nullptr, 0, { "cobuchi", OPT_COBUCHI, nullptr, 0,
"automaton with co-Büchi acceptance (will recognize" "automaton with co-Büchi acceptance (will recognize "
"a superset of the input language if not co-Büchi " "a superset of the input language if not co-Büchi "
"realizable)", 0 }, "realizable)", 0 },
{ "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },

4
spot/graph/graph.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Copyright (C) 2014-2018 Laboratoire de Recherche et
// Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -1076,7 +1076,7 @@ namespace spot
killed_edge_ = 0; killed_edge_ = 0;
} }
/// \brief Sort all edge according to a predicate /// \brief Sort all edges according to a predicate
/// ///
/// This will invalidate all iterators, and also destroy edge /// This will invalidate all iterators, and also destroy edge
/// chains. Call chain_edges_() immediately afterwards unless you /// chains. Call chain_edges_() immediately afterwards unless you

130
spot/twa/twa.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013-2017 Laboratoire de Recherche et // Copyright (C) 2009, 2011, 2013-2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -92,7 +92,7 @@ namespace spot
/// new state that you should deallocate with this function. /// new state that you should deallocate with this function.
/// Before Spot 0.7, you had to "delete" your state directly. /// Before Spot 0.7, you had to "delete" your state directly.
/// Starting with Spot 0.7, you should update your code to use /// Starting with Spot 0.7, you should update your code to use
/// this function instead. destroy() usually call delete, except /// this function instead. destroy() usually calls delete, except
/// in subclasses that destroy() to allow better memory management /// in subclasses that destroy() to allow better memory management
/// (e.g., no memory allocation for explicit automata). /// (e.g., no memory allocation for explicit automata).
virtual void destroy() const virtual void destroy() const
@ -116,7 +116,7 @@ namespace spot
/// \brief Strict Weak Ordering for \c state*. /// \brief Strict Weak Ordering for \c state*.
/// ///
/// This is meant to be used as a comparison functor for /// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c state*. /// STL \c map whose keys are of type \c state*.
/// ///
/// For instance here is how one could declare /// For instance here is how one could declare
/// a map of \c state*. /// a map of \c state*.
@ -138,7 +138,7 @@ namespace spot
/// \brief An Equivalence Relation for \c state*. /// \brief An Equivalence Relation for \c state*.
/// ///
/// This is meant to be used as a comparison functor for /// This is meant to be used as a comparison functor for
/// an \c unordered_map whose key are of type \c state*. /// an \c unordered_map whose keys are of type \c state*.
/// ///
/// For instance here is how one could declare /// For instance here is how one could declare
/// a map of \c state*. /// a map of \c state*.
@ -162,7 +162,7 @@ namespace spot
/// \brief Hash Function for \c state*. /// \brief Hash Function for \c state*.
/// ///
/// This is meant to be used as a hash functor for /// This is meant to be used as a hash functor for
/// an \c unordered_map whose key are of type \c state*. /// an \c unordered_map whose keys are of type \c state*.
/// ///
/// For instance here is how one could declare /// For instance here is how one could declare
/// a map of \c state*. /// a map of \c state*.
@ -205,9 +205,9 @@ namespace spot
/// \brief Canonicalize state pointer. /// \brief Canonicalize state pointer.
/// ///
/// If this is the first time a state is seen, this return the /// If this is the first time a state is seen, this returns the
/// state pointer as-is, otherwise it frees the state and returns /// state pointer as-is, otherwise it frees the state and returns
/// a point to the previously seen copy. /// a pointer to the previously seen copy.
/// ///
/// States are owned by the table and will be freed on /// States are owned by the table and will be freed on
/// destruction. /// destruction.
@ -239,7 +239,7 @@ namespace spot
for (state_set::iterator i = m.begin(); i != m.end();) for (state_set::iterator i = m.begin(); i != m.end();)
{ {
// Advance the iterator before destroying its key. This // Advance the iterator before destroying its key. This
// avoid issues with old g++ implementations. // avoids issues with old g++ implementations.
state_set::iterator old = i++; state_set::iterator old = i++;
(*old)->destroy(); (*old)->destroy();
} }
@ -266,7 +266,7 @@ namespace spot
/// (shared_ptr<const state*>). /// (shared_ptr<const state*>).
/// ///
/// This is meant to be used as a comparison functor for /// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c shared_state. /// STL \c map whose keys are of type \c shared_state.
/// ///
/// For instance here is how one could declare /// For instance here is how one could declare
/// a map of \c shared_state. /// a map of \c shared_state.
@ -290,7 +290,7 @@ namespace spot
/// (shared_ptr<const state*>). /// (shared_ptr<const state*>).
/// ///
/// This is meant to be used as a comparison functor for /// This is meant to be used as a comparison functor for
/// an \c unordered_map whose key are of type \c shared_state. /// an \c unordered_map whose keys are of type \c shared_state.
/// ///
/// For instance here is how one could declare /// For instance here is how one could declare
/// a map of \c shared_state /// a map of \c shared_state
@ -318,7 +318,7 @@ namespace spot
/// \brief Hash Function for \c shared_state (shared_ptr<const state*>). /// \brief Hash Function for \c shared_state (shared_ptr<const state*>).
/// ///
/// This is meant to be used as a hash functor for /// This is meant to be used as a hash functor for
/// an \c unordered_map whose key are of type /// an \c unordered_map whose keys are of type
/// \c shared_state. /// \c shared_state.
/// ///
/// For instance here is how one could declare /// For instance here is how one could declare
@ -365,7 +365,7 @@ namespace spot
/// The twa_succ_iterator is usually subclassed so that iteration /// The twa_succ_iterator is usually subclassed so that iteration
/// methods and accessor methods can be implemented differently in /// methods and accessor methods can be implemented differently in
/// different automata. In particular, this interface allows /// different automata. In particular, this interface allows
/// computing the set of successor on the fly if needed. /// computing the set of successors on the fly if needed.
/// ///
/// The iterator can be used to iterate over all successors in a /// The iterator can be used to iterate over all successors in a
/// loop as follows: /// loop as follows:
@ -392,7 +392,7 @@ namespace spot
/// while(i->next()); /// while(i->next());
/// \endcode /// \endcode
/// ///
/// This loops uses the return value of first() and next() to save /// This loop uses the return value of first() and next() to save
/// n+1 calls to done(). /// n+1 calls to done().
class SPOT_API twa_succ_iterator class SPOT_API twa_succ_iterator
{ {
@ -424,7 +424,7 @@ namespace spot
/// \brief Jump to the next successor (if any). /// \brief Jump to the next successor (if any).
/// ///
/// \warning Again, one should always call \c done() (or better: /// \warning Again, one should always call \c done() (or better:
/// check the return value of next()) ensure there is a successor. /// check the return value of next()) to ensure there is a successor.
/// ///
/// \return true if the iterator moved to a new successor, false /// \return true if the iterator moved to a new successor, false
/// if the iterator could not move to a new successor. /// if the iterator could not move to a new successor.
@ -459,7 +459,7 @@ namespace spot
/// ///
/// Each call to dst() (even several times on the same edge) /// Each call to dst() (even several times on the same edge)
/// creates a new state that has to be destroyed (see /// creates a new state that has to be destroyed (see
/// state::destroy()). by the caller after it is no longer used. /// state::destroy()) by the caller after it is no longer used.
/// ///
/// Note that the same state may occur at different points in the /// Note that the same state may occur at different points in the
/// iteration, as different outgoing edges (usually with different /// iteration, as different outgoing edges (usually with different
@ -467,7 +467,7 @@ namespace spot
virtual const state* dst() const = 0; virtual const state* dst() const = 0;
/// \brief Get the condition on the edge leading to this successor. /// \brief Get the condition on the edge leading to this successor.
/// ///
/// This is a boolean function of atomic propositions. /// This is a Boolean function of atomic propositions.
virtual bdd cond() const = 0; virtual bdd cond() const = 0;
/// \brief Get the acceptance mark of the edge leading to this /// \brief Get the acceptance mark of the edge leading to this
/// successor. /// successor.
@ -478,7 +478,7 @@ namespace spot
namespace internal namespace internal
{ {
/// \brief Helper structure to iterate over the successor of a /// \brief Helper structure to iterate over the successors of a
/// state using the on-the-fly interface. /// state using the on-the-fly interface.
/// ///
/// This one emulates an STL-like iterator over the /// This one emulates an STL-like iterator over the
@ -517,7 +517,7 @@ namespace spot
}; };
#ifndef SWIG #ifndef SWIG
/// \brief Helper class to iterate over the successor of a state /// \brief Helper class to iterate over the successors of a state
/// using the on-the-fly interface /// using the on-the-fly interface
/// ///
/// This one emulates an STL-like container with begin()/end() /// This one emulates an STL-like container with begin()/end()
@ -575,9 +575,9 @@ namespace spot
/// w is just a non-utf8 replacement for ω that should not be /// w is just a non-utf8 replacement for ω that should not be
/// capitalized. /// capitalized.
/// ///
/// TωAs are transition-based automata, meanings that not-only do /// TωAs are transition-based automata, meaning that not-only do
/// they have labels on edges, but they also have an acceptance /// they have labels on edges, but they also have an acceptance
/// condition defined in term of sets of transitions. The /// condition defined in terms of sets of transitions. The
/// acceptance condition can be anything supported by the HOA format /// acceptance condition can be anything supported by the HOA format
/// (http://adl.github.io/hoaf/). The only restriction w.r.t. the /// (http://adl.github.io/hoaf/). The only restriction w.r.t. the
/// format is that this class does not support alternating automata. /// format is that this class does not support alternating automata.
@ -598,7 +598,7 @@ namespace spot
/// of any given state. A TωA is always assumed to have at least /// of any given state. A TωA is always assumed to have at least
/// one state, the initial one. /// one state, the initial one.
/// ///
/// Note that although this is a transition-based automata, we never /// Note that although this is a transition-based automaton, we never
/// represent edges in the API. Information about edges can be /// represent edges in the API. Information about edges can be
/// obtained by querying the iterator over the successors of a /// obtained by querying the iterator over the successors of a
/// state. /// state.
@ -617,7 +617,7 @@ namespace spot
/// graph in memory, use the spot::twa_graph subclass instead. A /// graph in memory, use the spot::twa_graph subclass instead. A
/// twa_graph object can be used as a spot::twa (using the /// twa_graph object can be used as a spot::twa (using the
/// on-the-fly interface, even though nothing needs to be /// on-the-fly interface, even though nothing needs to be
/// constructed), but it also offers a faster interface that do not /// constructed), but it also offers a faster interface that does not
/// use virtual methods. /// use virtual methods.
class SPOT_API twa: public std::enable_shared_from_this<twa> class SPOT_API twa: public std::enable_shared_from_this<twa>
{ {
@ -694,7 +694,7 @@ namespace spot
/// \brief Get the dictionary associated to the automaton. /// \brief Get the dictionary associated to the automaton.
/// ///
/// Automata are labeled by Boolean formulas over atomic /// Automata are labeled by Boolean formulas over atomic
/// propositions. These Boolean formula are represented as BDDs. /// propositions. These Boolean formulas are represented as BDDs.
/// The dictionary allows to map BDD variables back to atomic /// The dictionary allows to map BDD variables back to atomic
/// propositions, and vice versa. /// propositions, and vice versa.
/// ///
@ -704,7 +704,7 @@ namespace spot
/// ///
/// It is however possible to declare automata that use different /// It is however possible to declare automata that use different
/// sets of atomic propositions with different dictionaries. That /// sets of atomic propositions with different dictionaries. That
/// way a BDD variable associated to some atomic proposition in /// way, a BDD variable associated to some atomic proposition in
/// one automaton might be reused for another atomic proposition /// one automaton might be reused for another atomic proposition
/// in the other automaton. /// in the other automaton.
bdd_dict_ptr get_dict() const bdd_dict_ptr get_dict() const
@ -719,7 +719,7 @@ namespace spot
/// a given atomic proposition. /// a given atomic proposition.
/// ///
/// This adds the atomic proposition to the list of atomic /// This adds the atomic proposition to the list of atomic
/// proposition of the automaton, and also register it to the /// proposition of the automaton, and also registers it to the
/// bdd_dict. /// bdd_dict.
/// ///
/// \return The BDD variable number assigned for this atomic /// \return The BDD variable number assigned for this atomic
@ -748,10 +748,10 @@ namespace spot
void unregister_ap(int num); void unregister_ap(int num);
/// \brief Register all atomic propositions that have /// \brief Register all atomic propositions that have
/// already be register by the bdd_dict for this automaton. /// already been registered by the bdd_dict for this automaton.
/// ///
/// This method may only be called on an automaton with an empty /// This method may only be called on an automaton with an empty
/// list of AP. It will fetch all atomic proposition that have /// list of AP. It will fetch all atomic propositions that have
/// been set in the bdd_dict for this particular automaton. /// been set in the bdd_dict for this particular automaton.
/// ///
/// The typical use-case for this function is when the labels of /// The typical use-case for this function is when the labels of
@ -799,7 +799,7 @@ namespace spot
/// ///
/// This converts \a s, into that corresponding spot::state for \a /// This converts \a s, into that corresponding spot::state for \a
/// t. This is useful when you have the state of a product, and /// t. This is useful when you have the state of a product, and
/// want restrict this state to a specific automata occuring in /// want to restrict this state to a specific automata occuring in
/// the product. /// the product.
/// ///
/// It goes without saying that \a s and \a t should be compatible /// It goes without saying that \a s and \a t should be compatible
@ -985,7 +985,7 @@ namespace spot
/// ///
/// This declares a single acceptance set, and \c Inf(0) /// This declares a single acceptance set, and \c Inf(0)
/// acceptance. The returned mark \c {0} can be used to tag /// acceptance. The returned mark \c {0} can be used to tag
/// accepting transition. /// accepting transitions.
/// ///
/// Note that this does not mark the automaton as using /// Note that this does not mark the automaton as using
/// state-based acceptance. If you want to create a Büchi /// state-based acceptance. If you want to create a Büchi
@ -1006,7 +1006,7 @@ namespace spot
/// ///
/// This declares a single acceptance set, and \c Fin(0) /// This declares a single acceptance set, and \c Fin(0)
/// acceptance. The returned mark \c {0} can be used to tag /// acceptance. The returned mark \c {0} can be used to tag
/// non-accepting transition. /// non-accepting transitions.
/// ///
/// Note that this does not mark the automaton as using /// Note that this does not mark the automaton as using
/// state-based acceptance. If you want to create a co-Büchi /// state-based acceptance. If you want to create a co-Büchi
@ -1030,16 +1030,16 @@ namespace spot
/// Helper structure used to store property flags. /// Helper structure used to store property flags.
struct bprop struct bprop
{ {
trival::repr_t state_based_acc:2; // State-based acceptance. trival::repr_t state_based_acc:2; // State-based acceptance.
trival::repr_t inherently_weak:2; // Inherently Weak automaton. trival::repr_t inherently_weak:2; // Inherently Weak automaton.
trival::repr_t weak:2; // Weak automaton. trival::repr_t weak:2; // Weak automaton.
trival::repr_t terminal:2; // Terminal automaton. trival::repr_t terminal:2; // Terminal automaton.
trival::repr_t universal:2; // Universal automaton. trival::repr_t universal:2; // Universal automaton.
trival::repr_t unambiguous:2; // Unambiguous automaton. trival::repr_t unambiguous:2; // Unambiguous automaton.
trival::repr_t stutter_invariant:2; // Stutter invariant language. trival::repr_t stutter_invariant:2; // Stutter invariant language.
trival::repr_t very_weak:2; // very-weak, or 1-weak trival::repr_t very_weak:2; // very-weak, or 1-weak
trival::repr_t semi_deterministic:2; // semi-deterministic automaton. trival::repr_t semi_deterministic:2; // semi-deterministic automaton.
trival::repr_t complete:2; // Complete automaton. trival::repr_t complete:2; // Complete automaton.
}; };
union union
{ {
@ -1062,10 +1062,10 @@ namespace spot
/// ///
/// Arbitrary objects can be attached to automata. Those are called /// Arbitrary objects can be attached to automata. Those are called
/// named properties. They are used for instance to name all the /// named properties. They are used for instance to name all the
/// state of an automaton. /// states of an automaton.
/// ///
/// This function attaches the object \a val to the current /// This function attaches the object \a val to the current
/// automaton, under the name \a s and destroy any previous /// automaton, under the name \a s and destroys any previous
/// property with the same name. /// property with the same name.
/// ///
/// When the automaton is destroyed, the \a destructor function will /// When the automaton is destroyed, the \a destructor function will
@ -1080,10 +1080,10 @@ namespace spot
/// ///
/// Arbitrary objects can be attached to automata. Those are called /// Arbitrary objects can be attached to automata. Those are called
/// named properties. They are used for instance to name all the /// named properties. They are used for instance to name all the
/// state of an automaton. /// states of an automaton.
/// ///
/// This function attaches the object \a val to the current /// This function attaches the object \a val to the current
/// automaton, under the name \a s and destroy any previous /// automaton, under the name \a s and destroys any previous
/// property with the same name. /// property with the same name.
/// ///
/// When the automaton is destroyed, the attached object will be /// When the automaton is destroyed, the attached object will be
@ -1101,7 +1101,7 @@ namespace spot
/// ///
/// Arbitrary objects can be attached to automata. Those are called /// Arbitrary objects can be attached to automata. Those are called
/// named properties. They are used for instance to name all the /// named properties. They are used for instance to name all the
/// state of an automaton. /// states of an automaton.
/// ///
/// This function removes the property \a s if it exists. /// This function removes the property \a s if it exists.
/// ///
@ -1137,11 +1137,11 @@ namespace spot
/// ///
/// Arbitrary objects can be attached to automata. Those are called /// Arbitrary objects can be attached to automata. Those are called
/// named properties. They are used for instance to name all the /// named properties. They are used for instance to name all the
/// state of an automaton. /// states of an automaton.
/// ///
/// This function create a property object of a given type, and /// This function creates a property object of a given type, and
/// attached it to \a name if not such property exist, or it /// attaches it to \a name if no such property exists, or it
/// returns /// returns the found object.
/// ///
/// See https://spot.lrde.epita.fr/concepts.html#named-properties /// See https://spot.lrde.epita.fr/concepts.html#named-properties
/// for a list of named properties used by Spot. /// for a list of named properties used by Spot.
@ -1161,7 +1161,7 @@ namespace spot
/// \brief Destroy all named properties. /// \brief Destroy all named properties.
/// ///
/// This is used by the automaton destructor, but it could be used /// This is used by the automaton destructor, but it could be used
/// by any algorithm that want to get rid of all named properties. /// by any algorithm that wants to get rid of all named properties.
void release_named_properties() void release_named_properties()
{ {
// Destroy all named properties. // Destroy all named properties.
@ -1214,7 +1214,7 @@ namespace spot
return is.inherently_weak; return is.inherently_weak;
} }
/// \brief Set the "inherently weak" proeprty. /// \brief Set the "inherently weak" property.
/// ///
/// Setting "inherently weak" to false automatically /// Setting "inherently weak" to false automatically
/// disables "terminal", "very weak", and "weak". /// disables "terminal", "very weak", and "weak".
@ -1235,7 +1235,7 @@ namespace spot
/// to a non-accepting SCC. /// to a non-accepting SCC.
/// ///
/// This property ensures that a word can be accepted as soon as /// This property ensures that a word can be accepted as soon as
/// on of its prefixes move through an accepting edge. /// one of its prefixes moves through an accepting edge.
/// ///
/// \see prop_weak() /// \see prop_weak()
/// \see prop_inherently_weak() /// \see prop_inherently_weak()
@ -1274,7 +1274,7 @@ namespace spot
/// ///
/// Marking an automaton as "weak" automatically marks it as /// Marking an automaton as "weak" automatically marks it as
/// "inherently weak". Marking an automaton as "not weak" /// "inherently weak". Marking an automaton as "not weak"
/// automatically marks are as "not terminal". /// automatically marks it as "not terminal".
/// ///
/// \see prop_terminal() /// \see prop_terminal()
/// \see prop_inherently_weak() /// \see prop_inherently_weak()
@ -1315,7 +1315,7 @@ namespace spot
} }
/// \brief Whether the automaton is complete.. /// \brief Whether the automaton is complete.
/// ///
/// An automaton is complete if for each state the union of the /// An automaton is complete if for each state the union of the
/// labels of its outgoing transitions is always true. /// labels of its outgoing transitions is always true.
@ -1370,7 +1370,7 @@ namespace spot
is.unambiguous = is.semi_deterministic = val.val(); is.unambiguous = is.semi_deterministic = val.val();
} }
// Starting with Spot 2.4, and automaton is deterministic if it is // Starting with Spot 2.4, an automaton is deterministic if it is
// both universal and existential, but as we already have // both universal and existential, but as we already have
// twa::is_existential(), we only need to additionally record the // twa::is_existential(), we only need to additionally record the
// universal property. Before that, the deterministic property // universal property. Before that, the deterministic property
@ -1406,7 +1406,7 @@ namespace spot
return is.unambiguous; return is.unambiguous;
} }
/// \brief Sets the unambiguous property /// \brief Set the unambiguous property
/// ///
/// Marking an automaton as "non unambiguous" automatically /// Marking an automaton as "non unambiguous" automatically
/// marks it as "non universal". /// marks it as "non universal".
@ -1436,7 +1436,7 @@ namespace spot
return is.semi_deterministic; return is.semi_deterministic;
} }
/// \brief Sets the semi-deterministic property /// \brief Set the semi-deterministic property
/// ///
/// Marking an automaton as "non semi-deterministic" automatically /// Marking an automaton as "non semi-deterministic" automatically
/// marks it as "non universal". /// marks it as "non universal".
@ -1453,11 +1453,11 @@ namespace spot
/// ///
/// An automaton is stutter-invariant iff any accepted word /// An automaton is stutter-invariant iff any accepted word
/// remains accepted after removing a finite number of duplicate /// remains accepted after removing a finite number of duplicate
/// letters, or after duplicating finite number of letters. /// letters, or after duplicating a finite number of letters.
/// ///
/// Note that this method may return trival::maybe() when it is /// Note that this method may return trival::maybe() when it is
/// unknown whether the automaton is stutter-invariant or not. If /// unknown whether the automaton is stutter-invariant or not. If
/// you need a true/false answer, prefer one using of the the /// you need a true/false answer, prefer the
/// is_stutter_invariant() function. /// is_stutter_invariant() function.
/// ///
/// \see is_stutter_invariant /// \see is_stutter_invariant
@ -1505,19 +1505,19 @@ namespace spot
/// only copied if they are positive. /// only copied if they are positive.
/// ///
/// The reason there is no default value for these flags is that /// The reason there is no default value for these flags is that
/// whenever we add a new property that do not fall into any of /// whenever we add a new property that does not fall into any of
/// these groups, we will be forced to review all algorithm to /// these groups, we will be forced to review all algorithms to
/// decide if the property should be preserved or not. /// decide if the property should be preserved or not.
/// ///
/// \see make_twa_graph_ptr /// \see make_twa_graph_ptr
/// \see prop_copy /// \see prop_copy
struct prop_set struct prop_set
{ {
bool state_based; ///< preserve state-based acceptnace bool state_based; ///< preserve state-based acceptance
bool inherently_weak; ///< preserve inherently weak, weak, & terminal bool inherently_weak; ///< preserve inherently weak, weak, & terminal
bool deterministic; ///< preserve deterministic, semi-det, unambiguous bool deterministic; ///< preserve deterministic, semi-det, unambiguous
bool improve_det; ///< improves deterministic, semi-det, unambiguous bool improve_det; ///< improve deterministic, semi-det, unambiguous
bool complete; ///< preserves completeness bool complete; ///< preserve completeness
bool stutter_inv; ///< preserve stutter invariance bool stutter_inv; ///< preserve stutter invariance
prop_set() prop_set()
@ -1586,7 +1586,7 @@ namespace spot
/// \brief Copy the properties of another automaton. /// \brief Copy the properties of another automaton.
/// ///
/// Copy the property speciefied with \a p from \a other to the /// Copy the property specified with \a p from \a other to the
/// current automaton. /// current automaton.
/// ///
/// There is no default value for \a p on purpose. This way any /// There is no default value for \a p on purpose. This way any

2
spot/twa/twagraph.hh
View file

@ -616,7 +616,7 @@ namespace spot
return 0U; return 0U;
} }
/// \brief Tell if a state is acceptince. /// \brief Tell if a state is accepting.
/// ///
/// This makes only sense for automata using state-based /// This makes only sense for automata using state-based
/// acceptance, and a simple acceptance condition like Büchi or /// acceptance, and a simple acceptance condition like Büchi or

6
spot/twaalgos/remfin.cc
View file

@ -165,10 +165,10 @@ namespace spot
return remove_fin_impl(sccaut, skip)->is_empty(); return remove_fin_impl(sccaut, skip)->is_empty();
} }
// Remaining infs corresponds to I₁s that have been seen with seeing // Remaining infs corresponds to I₁s that have been seen without seeing
// the mathing F₁. In this SCC any edge in these I₁ is therefore // the matching F₁. In this SCC any edge in these I₁ is therefore
// final. Otherwise we do not know: it is possible that there is // final. Otherwise we do not know: it is possible that there is
// a non-accepting cycle in the SCC that do not visit Fᵢ. // a non-accepting cycle in the SCC that does not visit Fᵢ.
std::set<unsigned> unknown; std::set<unsigned> unknown;
for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e) for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e)
{ {

6
spot/twaalgos/toweak.cc
View file

@ -50,9 +50,9 @@ namespace spot
operator()(const rc_state& s) const noexcept operator()(const rc_state& s) const noexcept
{ {
using std::hash; using std::hash;
return ((hash<int>()(s.id) return ((hash<unsigned>()(s.id)
^ (hash<int>()(s.rank))) ^ (hash<unsigned>()(s.rank)))
^ (hash<int>()(s.mark.id))); ^ (hash<acc_cond::mark_t>()(s.mark)));
} }
}; };