diff --git a/bin/README b/bin/README index 84f574a55..9fe810e82 100644 --- a/bin/README +++ b/bin/README @@ -12,7 +12,7 @@ whose purpose is just to generate a man-page with the same format as the other man pages (this includes keeping the version number up-to-date). -There is also a script called 'options.py' that summerizes how the +There is also a script called 'options.py' that summarizes how the different short options are used among the tools. Routines that are shared by multiple command-line tools are stored in diff --git a/bin/common_conv.hh b/bin/common_conv.hh index a3a43f8eb..304c5fc99 100644 --- a/bin/common_conv.hh +++ b/bin/common_conv.hh @@ -27,5 +27,5 @@ unsigned to_unsigned (const char *s, const char* where); float to_float(const char* s, const char* where); float to_probability(const char* s, const char* where); -// Parse the comma or space seperate string of numbers. +// Parse the comma or space separated string of numbers. std::vector to_longs(const char* s); diff --git a/bin/common_trans.cc b/bin/common_trans.cc index dd7ccc0ba..05a75a0c5 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -980,9 +980,9 @@ static const argp_option options[] = "atomic proposition that compatible with Spin's syntax. You can " "force this relabeling to always occur with option --relabel.\n" "The sequences %f,%s,%l,%w,%F,%S,%L,%W can optionally be \"infixed\"" - " by a bracketed sequence of operators to unabbreviate before outputing" + " by a bracketed sequence of operators to unabbreviate before outputting" " the formula. For instance %[MW]f will rewrite operators M and W" - " before outputing it.\n" + " before outputting it.\n" "Furthermore, if COMMANDFMT has the form \"{NAME}CMD\", then only CMD " "will be passed to the shell, and NAME will be used to name the tool " "in the output.", 4 }, diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 2062b6340..e113bf205 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -757,7 +757,7 @@ namespace } // Takes a set of the atomic propositions appearing in the formula, - // and seperate them into two vectors: input APs and output APs. + // and separate them into two vectors: input APs and output APs. static std::pair, std::vector> filter_list_of_aps(const std::unordered_set& aps, const char* filename, int linenum) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index eca2a945c..d29432a36 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -47,7 +47,7 @@ depends on the --low, --medium, or --high settings.") }, "Maximum number of states of automata involved in automata-based \ implication checks for formula simplifications. Defaults to 64.") }, { DOC("tls-max-ops", - "Maximum number of operands in n-ary opertors (or, and) on which \ + "Maximum number of operands in n-ary operators (or, and) on which \ implication-based simplifications are attempted. Defaults to 16.") }, { nullptr, 0, nullptr, 0, "Translation options:", 0 }, { DOC("ltl-split", "Set to 0 to disable the translation of automata \ @@ -83,7 +83,7 @@ used when comp-susp=1 and default to 1 or 2 depending on whether --small \ or --deterministic is specified.") }, { nullptr, 0, nullptr, 0, "Postprocessing options:", 0 }, { DOC("acd", "Set to 1 (the default) to use paritize automata using \ -the alternatinc cycle decomposition. Set to 0 to use paritization based \ +the alternating cycle decomposition. Set to 0 to use paritization based \ on latest appearance record variants.") }, { DOC("scc-filter", "Set to 1 (the default) to enable \ SCC-pruning and acceptance simplification at the beginning of \ @@ -91,7 +91,7 @@ post-processing. Transitions that are outside accepting SCC are \ removed from accepting sets, except those that enter into an accepting \ SCC. Set to 2 to remove even these entering transition from the \ accepting sets. Set to 0 to disable this SCC-pruning and acceptance \ -simpification pass.") }, +simplification pass.") }, { DOC("degen-reset", "If non-zero (the default), the \ degeneralization algorithm will reset its level any time it exits \ an SCC.") }, @@ -121,7 +121,7 @@ level, as it might favor finding accepting cycles earlier. If \ degen-lowinit is non-zero, then level L is always used without looking \ for the presence of an accepting self-loop.") }, { DOC("degen-remscc", "If non-zero (the default), make sure the output \ -of the degenalization has as many SCCs as the input, by removing superfluous \ +of the degeneralization has as many SCCs as the input, by removing superfluous \ ones.") }, { DOC("det-max-states", "When defined to a positive integer N, \ determinizations will be aborted whenever the number of generated \ @@ -180,7 +180,7 @@ attempting simulation-based reductions. Defaults to 128. Set to 0 to \ never merge states.") }, { DOC("simul-max", "Number of states above which simulation-based \ reductions are skipped. Defaults to 4096. Set to 0 to disable. This \ -applies to all simulation-based optimization, including thoses of the \ +applies to all simulation-based optimization, including those of the \ determinization algorithm.") }, { DOC("simul-trans-pruning", "Number of equivalence classes above which \ simulation-based transition-pruning for non-deterministic automata is \ @@ -259,7 +259,7 @@ sets. By default, this is only enabled when options -B or -S are used.") }, { DOC("simul-method", "Chose which simulation based reduction to use: 1 force the \ signature-based BDD implementation, 2 force matrix-based and 0, the default, \ -is a heristic wich choose which implementation to use.") }, +is a heuristic which chooses which implementation to use.") }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index 7b60b5269..94e0b987a 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -81,7 +81,7 @@ namespace spot /// \brief An NBA with (n+2) states derived from a Cyclic test /// case. /// - /// This familly of automata is derived from a couple of + /// This family of automata is derived from a couple of /// examples supplied by Reuben Rowe. The task is to /// check that the automaton generated with AUT_CYCLIST_TRACE_NBA /// for a given n contain the automaton generated with @@ -90,7 +90,7 @@ namespace spot /// \brief A DBA with (n+2) states derived from a Cyclic test /// case. /// - /// This familly of automata is derived from a couple of + /// This family of automata is derived from a couple of /// examples supplied by Reuben Rowe. The task is to /// check that the automaton generated with AUT_CYCLIST_TRACE_NBA /// for a given n contain the automaton generated with diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 4f62f3dcd..04d0a8421 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -757,7 +757,7 @@ namespace spot ///@} ///@{ - /// \brief return the Edgeg_Data of an edge. + /// \brief return the Edge_Data of an edge. /// /// This does not use Edge_Data& as return type, because /// Edge_Data might be void. @@ -818,7 +818,7 @@ namespace spot && (dests_.capacity() - dests_.size()) < (sz + 1)) { // If dst_begin...dst_end points into dests_ and dests_ risk - // being reallocated, we have to savea the destination + // being reallocated, we have to save the destination // states before we lose them. std::vector tmp(dst_begin, dst_end); dests_.emplace_back(sz); @@ -955,7 +955,7 @@ namespace spot /// @{ /// - /// \brief Return a fake container with all edges (exluding erased + /// \brief Return a fake container with all edges (excluding erased /// edges) internal::all_trans edges() const { diff --git a/spot/ltsmin/ltsmin.hh b/spot/ltsmin/ltsmin.hh index 1611375fe..41369c653 100644 --- a/spot/ltsmin/ltsmin.hh +++ b/spot/ltsmin/ltsmin.hh @@ -73,7 +73,7 @@ namespace spot int compress = 0) const; // \brief The same as above but returns a kripkecube, i.e. a kripke - // that can be use in parallel. Moreover, it support more ellaborated + // that can be use in parallel. Moreover, it supports more elaborated // atomic propositions such as "P.a == P.c" ltsmin_kripkecube_ptr kripkecube(std::vector to_observe, formula dead = formula::tt(), diff --git a/spot/ltsmin/spins_interface.hh b/spot/ltsmin/spins_interface.hh index de64a5c99..24792a6c1 100644 --- a/spot/ltsmin/spins_interface.hh +++ b/spot/ltsmin/spins_interface.hh @@ -38,7 +38,7 @@ namespace spot /// \brief Implementation of the PINS interface. This class /// is a wrapper that, given a file, will compile it w.r.t - /// the PINS interface. The class can then be menipulated + /// the PINS interface. The class can then be manipulated /// transparently whatever the input format considered. class SPOT_API spins_interface { diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh index c122913ee..42c7cc36f 100644 --- a/spot/ltsmin/spins_kripke.hh +++ b/spot/ltsmin/spins_kripke.hh @@ -116,7 +116,7 @@ namespace spot /// All successors are computed once when an iterator is recycled or /// created. /// - /// Note: Two threads will explore sucessors with two different orders + /// Note: Two threads will explore successors with two different orders class cspins_iterator final { public: diff --git a/spot/mc/bloemen.hh b/spot/mc/bloemen.hh index 995f5a00b..7b9c5ba7b 100644 --- a/spot/mc/bloemen.hh +++ b/spot/mc/bloemen.hh @@ -63,7 +63,7 @@ namespace spot std::atomic list_status_; }; - /// \brief The haser for the previous uf_element. + /// \brief The hasher for the previous uf_element. struct uf_element_hasher { uf_element_hasher(const uf_element*) diff --git a/spot/mc/bloemen_ec.hh b/spot/mc/bloemen_ec.hh index b91e0bbf8..89756cf4f 100644 --- a/spot/mc/bloemen_ec.hh +++ b/spot/mc/bloemen_ec.hh @@ -70,7 +70,7 @@ namespace spot std::atomic list_status_; }; - /// \brief The haser for the previous uf_element. + /// \brief The hasher for the previous uf_element. struct uf_element_hasher { uf_element_hasher(const uf_element*) diff --git a/spot/mc/cndfs.hh b/spot/mc/cndfs.hh index 5cec44471..ca52c93bf 100644 --- a/spot/mc/cndfs.hh +++ b/spot/mc/cndfs.hh @@ -361,7 +361,7 @@ namespace spot todo_blue_.back().it_prop, true, tid_); else if (acc) { - // The state cyan and we can reach it throught an + // The state cyan and we can reach it through an // accepting transition, a accepting cycle has been // found without launching a red dfs if (tmp.second.colors->l[tid_].cyan) @@ -499,7 +499,7 @@ namespace spot } kripkecube& sys_; ///< \brief The system to check - twacube_ptr twa_; ///< \brief The propertu to check + twacube_ptr twa_; ///< \brief The property to check std::vector todo_blue_; ///< \brief Blue Stack std::vector todo_red_; ///< \ brief Red Stack unsigned transitions_ = 0; ///< \brief Number of transitions @@ -514,7 +514,7 @@ namespace spot std::atomic& stop_; ///< \brief Stop-the-world boolean std::vector Rp_; ///< \brief Rp stack std::vector Rp_acc_; ///< \brief Rp acc stack - product_state cycle_start_; ///< \brief Begining of a cycle + product_state cycle_start_; ///< \brief Beginning of a cycle bool finisher_ = false; }; } diff --git a/spot/mc/deadlock.hh b/spot/mc/deadlock.hh index 3ce4d0ade..63b2dc273 100644 --- a/spot/mc/deadlock.hh +++ b/spot/mc/deadlock.hh @@ -37,7 +37,7 @@ namespace spot /// \brief This class aims to explore a model to detect wether it /// contains a deadlock. This deadlock detection performs a DFS traversal /// sharing information shared among multiple threads. - /// If Deadlock equals std::true_type performs dealock algorithm, + /// If Deadlock equals std::true_type performs deadlock algorithm, /// otherwise perform a simple reachability. template& stop_; ///< \brief Stop-the-world boolean /// \brief Stack that grows according to the todo stack. It avoid multiple - /// concurent access to the shared map. + /// concurrent access to the shared map. std::vector refs_; bool finisher_ = false; }; diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh index e34c8dc2d..fbc90f32b 100644 --- a/spot/mc/intersect.hh +++ b/spot/mc/intersect.hh @@ -25,9 +25,9 @@ namespace spot { /// \brief Find the first couple of iterator (from a given pair of - /// interators) that intersect. This method can be used in any + /// iterators) that intersect. This method can be used in any /// DFS/BFS-like exploration algorithm. The \a parameter indicates - /// wheter the state has just been visited since the underlying job + /// whether the state has just been visited since the underlying job /// is slightly different. template static void forward_iterators(kripkecube& sys, diff --git a/spot/mc/lpar13.hh b/spot/mc/lpar13.hh index 1abbd9faf..5a1283eb9 100644 --- a/spot/mc/lpar13.hh +++ b/spot/mc/lpar13.hh @@ -195,7 +195,7 @@ namespace spot /// that a state will be popped. If the method return false, then /// the state will be popped. Otherwise the state \a newtop will /// become the new top of the DFS stack. If the state \a top is - /// the only one in the DFS stak, the parameter \a is_initial is set + /// the only one in the DFS stack, the parameter \a is_initial is set /// to true and both \a newtop and \a newtop_dfsnum have inconsistency /// values. bool pop_state(product_state, unsigned top_dfsnum, bool, diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh index aef392738..0bf5492ce 100644 --- a/spot/mc/mc_instanciator.hh +++ b/spot/mc/mc_instanciator.hh @@ -38,8 +38,8 @@ namespace spot { /// \brief This class allows to ensure (at compile time) if - /// a given parameter can be compsidered as a modelchecking algorithm - /// (i.e., usable by instanciate) + /// a given parameter can be considered as a modelchecking algorithm + /// (i.e., usable by instantiate) template class SPOT_API is_a_mc_algorithm { @@ -123,7 +123,7 @@ namespace spot } #endif - // Wait all threads to be instanciated. + // Wait all threads to be instantiated. while (barrier) continue; swarmed[i]->run(); @@ -169,8 +169,8 @@ namespace spot bool go_on = true; for (unsigned i = 0; i < nbth && go_on; ++i) { - // Enumerate cases where a trace can be extraced - // Here we use a switch so that adding new algortihm + // Enumerate cases where a trace can be extracted + // Here we use a switch so that adding new algorithm // with new return status will trigger an error that // should the be fixed here. switch (result.value[i]) diff --git a/spot/misc/bareword.cc b/spot/misc/bareword.cc index a64d11511..c6b66e3b8 100644 --- a/spot/misc/bareword.cc +++ b/spot/misc/bareword.cc @@ -47,7 +47,7 @@ namespace spot } // This is for Spin 5. Spin 6 has a relaxed parser that can - // accept any parenthesized block as an atomic propoistion. + // accept any parenthesized block as an atomic proposition. bool is_spin_ap(const char* str) { if (!str || !islower(*str)) diff --git a/spot/misc/fixpool.hh b/spot/misc/fixpool.hh index 30b8a9b3e..3ad83be39 100644 --- a/spot/misc/fixpool.hh +++ b/spot/misc/fixpool.hh @@ -34,10 +34,10 @@ namespace spot /// - Safe: ensure (when used with memcheck) that each allocation /// is deallocated one at a time /// - Unsafe: rely on the fact that deallocating the pool also release - /// all elements it contains. This case is usefull in a multithreaded + /// all elements it contains. This case is useful in a multithreaded /// environnement with multiple fixed_sized_pool allocating the same - /// ressource. In this case it's hard to detect wich pool has allocated - /// some ressource. + /// resource. In this case it's hard to detect which pool has allocated + /// some resource. enum class pool_type { Safe , Unsafe }; /// A fixed-size memory pool implementation. diff --git a/spot/misc/formater.hh b/spot/misc/formater.hh index 2e387fe55..0f3a25d57 100644 --- a/spot/misc/formater.hh +++ b/spot/misc/formater.hh @@ -124,7 +124,7 @@ namespace spot { } - /// \brief Scan the %-sequences occuring in \a fmt. + /// \brief Scan the %-sequences occurring in \a fmt. /// /// Set has['c'] for each %c in \a fmt. \a has must /// be 256 wide. diff --git a/spot/misc/minato.hh b/spot/misc/minato.hh index 26bb631c8..9fdbe87bb 100644 --- a/spot/misc/minato.hh +++ b/spot/misc/minato.hh @@ -33,14 +33,14 @@ namespace spot class SPOT_API minato_isop { public: - /// \brief Conctructor. + /// \brief Constructor. /// \arg input The BDD function to translate in ISOP. minato_isop(bdd input); - /// \brief Conctructor. + /// \brief Constructor. /// \arg input The BDD function to translate in ISOP. /// \arg vars The set of BDD variables to factorize in \a input. minato_isop(bdd input, bdd vars); - /// \brief Conctructor. + /// \brief Constructor. /// /// This version allow some flexibility in computing the ISOP. /// the result must be within \a input_min and \a input_max. diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh index 83d24d86c..280158d1f 100644 --- a/spot/misc/satsolver.hh +++ b/spot/misc/satsolver.hh @@ -69,7 +69,7 @@ namespace spot class SPOT_API satsolver { public: - /// \brief Construct the sat solver and itinialize variables. + /// \brief Construct the sat solver and initialize variables. /// If no satsolver is provided through SPOT_SATSOLVER env var, a /// distributed version of PicoSAT will be used. satsolver(); @@ -116,7 +116,7 @@ namespace spot template void comment(T first, Args... args); - /// \brief Assume a litteral value. + /// \brief Assume a literal value. /// Must only be used with distributed picolib. void assume(int lit); @@ -159,7 +159,7 @@ namespace spot int nassumptions_vars_; // Surplus of vars (for 'assume' algorithm). /// \brief Number of solutions to obtain from the satsolver - /// (without assuming litterals). + /// (without assuming literals). int nsols_; /// \brief Picosat satsolver instance. diff --git a/spot/misc/timer.hh b/spot/misc/timer.hh index e2a607376..fc1b6ada8 100644 --- a/spot/misc/timer.hh +++ b/spot/misc/timer.hh @@ -147,7 +147,7 @@ namespace spot return total_.cutime; } - /// \brief Return the system time of the current process (whithout children) + /// \brief Return the system time of the current process (without children) /// of all accumulated interval. /// /// Any time interval that has been start()ed but not stop()ed diff --git a/spot/parseaut/public.hh b/spot/parseaut/public.hh index ee9a0e671..960592ac3 100644 --- a/spot/parseaut/public.hh +++ b/spot/parseaut/public.hh @@ -68,7 +68,7 @@ namespace spot /// want_kripke. kripke_graph_ptr ks; - /// Whether an HOA file was termined with --ABORT + /// Whether an HOA file was terminated with --ABORT bool aborted = false; /// Location of the automaton in the stream. spot::location loc; diff --git a/spot/priv/partitioned_relabel.cc b/spot/priv/partitioned_relabel.cc index 0e415d944..fc19bdd45 100644 --- a/spot/priv/partitioned_relabel.cc +++ b/spot/priv/partitioned_relabel.cc @@ -88,7 +88,7 @@ bdd_partition::to_relabeling_map(twa_graph& for_me) const bdd_partition try_partition_me(const std::vector& all_cond, unsigned max_letter) { - // We create vector that will be succesively filled. + // We create vector that will be successively filled. // Each entry corresponds to a "letter", of the partition const size_t Norig = all_cond.size(); diff --git a/spot/priv/satcommon.hh b/spot/priv/satcommon.hh index ce3fcffde..e91c11745 100644 --- a/spot/priv/satcommon.hh +++ b/spot/priv/satcommon.hh @@ -111,12 +111,12 @@ public: unsigned size_nacc, unsigned size_path, bool state_based, bool dtbasat); - /// \brief Compute min_t litteral as well as min_ta, min_p and max_p. - /// After this step, all litterals are known. + /// \brief Compute min_t literal as well as min_ta, min_p and max_p. + /// After this step, all literals are known. void declare_all_vars(int& min_t); - /// \brief Return the transition's litteral corresponding to parameters. + /// \brief Return the transition's literal corresponding to parameters. inline int get_t(unsigned src, unsigned cond, unsigned dst) const { @@ -134,12 +134,12 @@ public: return min_t_ + src * cd_mult_ + cond * size_dst_ + dst; } - /// \brief Return the transition_acc's litteral corresponding to parameters. + /// \brief Return the transition_acc's literal corresponding to parameters. /// If (state_based), all outgoing transitions use the same acceptance /// variable. Therefore, for each combination (src, nacc) there is only one - /// litteral. + /// literal. /// Note that with Büchi automata, there is only one nacc, thus, only one - /// litteral for each src. + /// literal for each src. inline int get_ta(unsigned src, unsigned cond, unsigned dst, unsigned nacc = 0) const { @@ -162,7 +162,7 @@ public: : min_ta_ + src * cdn_mult_ + cond * dn_mult_ + dst * size_nacc_ + nacc; } - /// \brief Return the path's litteral corresponding to parameters. + /// \brief Return the path's literal corresponding to parameters. inline int get_p(unsigned path, unsigned src, unsigned dst) const { @@ -181,9 +181,9 @@ public: return min_p_ + path * sd_mult_ + src * size_dst_ + dst; } - /// \brief Return the path's litteral corresponding to parameters. + /// \brief Return the path's literal corresponding to parameters. /// Argument ref serves to say whether it is a candidate or a reference - /// litteral. false -> ref | true -> cand + /// literal. false -> ref | true -> cand inline int get_prc(unsigned path, unsigned src, unsigned dst, bool cand) const { @@ -238,7 +238,7 @@ public: int target_state_number, const twa_graph_ptr& res, const satsolver& solver); - /// \brief Returns the number of distinct values containted in a vector. + /// \brief Returns the number of distinct values contained in a vector. int get_number_of_distinct_vals(std::vector v); } diff --git a/spot/ta/ta.hh b/spot/ta/ta.hh index cd3024ff6..2f8a75973 100644 --- a/spot/ta/ta.hh +++ b/spot/ta/ta.hh @@ -111,7 +111,7 @@ namespace spot /// \brief Get an iterator over the successors of \a state. /// /// The iterator has been allocated with \c new. It is the - /// responsability of the caller to \c delete it when no + /// responsibility of the caller to \c delete it when no /// longer needed. /// virtual ta_succ_iterator* @@ -121,7 +121,7 @@ namespace spot /// filtred by the changeset on transitions /// /// The iterator has been allocated with \c new. It is the - /// responsability of the caller to \c delete it when no + /// responsibility of the caller to \c delete it when no /// longer needed. /// virtual ta_succ_iterator* @@ -142,7 +142,7 @@ namespace spot /// \brief Format the state as a string for printing. /// - /// This formating is the responsability of the automata + /// This formatting is the responsibility of the automata /// that owns the state. virtual std::string format_state(const spot::state* s) const = 0; @@ -190,7 +190,7 @@ namespace spot /// /// This class provides the basic functionalities required to /// iterate over the successors of a state, as well as querying - /// transition labels. Because transitions are never explicitely + /// transition labels. Because transitions are never explicitly /// encoded, labels (conditions and acceptance conditions) can only /// be queried while iterating over the successors. class ta_succ_iterator : public twa_succ_iterator diff --git a/spot/ta/taexplicit.cc b/spot/ta/taexplicit.cc index 6a842ad1f..5eb995738 100644 --- a/spot/ta/taexplicit.cc +++ b/spot/ta/taexplicit.cc @@ -106,7 +106,7 @@ namespace spot return transitions_; } - // return transitions filtred by condition + // return transitions filtered by condition state_ta_explicit::transitions* state_ta_explicit::get_transitions(bdd condition) const { @@ -279,7 +279,7 @@ namespace spot bool dest_is_livelock_accepting = dest->is_livelock_accepting_state(); - //Before deleting stuttering transitions, propaged back livelock + //Before deleting stuttering transitions, propagated back livelock //and initial state's properties if (is_stuttering_transition) { diff --git a/spot/ta/taproduct.hh b/spot/ta/taproduct.hh index ba0cf4cf3..66dc152ab 100644 --- a/spot/ta/taproduct.hh +++ b/spot/ta/taproduct.hh @@ -158,7 +158,7 @@ namespace spot virtual bool is_initial_state(const spot::state* s) const override; - /// \brief Return true if the state \a s has no succeseurs + /// \brief Return true if the state \a s has no successor /// in the TA automaton (the TA component of the product automaton) bool is_hole_state_in_ta_component(const spot::state* s) const; diff --git a/spot/ta/tgta.hh b/spot/ta/tgta.hh index bed332805..81f06ad0f 100644 --- a/spot/ta/tgta.hh +++ b/spot/ta/tgta.hh @@ -9,9 +9,9 @@ // (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 MERCHANta_explicitBILITY +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more deta_explicitils. +// License for more details. // // You should have received a copy of the GNU General Public License // along with this program. If not, see . @@ -74,7 +74,7 @@ namespace spot /// \a state and his successors /// /// The iterator has been allocated with \c new. It is the - /// responsability of the caller to \c delete it when no + /// responsibility of the caller to \c delete it when no /// longer needed. /// virtual twa_succ_iterator* diff --git a/spot/taalgos/reachiter.hh b/spot/taalgos/reachiter.hh index 733bc7b68..935eae7a5 100644 --- a/spot/taalgos/reachiter.hh +++ b/spot/taalgos/reachiter.hh @@ -78,7 +78,7 @@ namespace spot /// /// \param in The source state number. /// \param out The destination state number. - /// \param si The spot::twa_succ_iterator positionned on the current + /// \param si The spot::twa_succ_iterator positioned on the current /// transition. virtual void process_link(int in, int out, const ta_succ_iterator* si); diff --git a/spot/taalgos/tgba2ta.hh b/spot/taalgos/tgba2ta.hh index 99240893b..fa5f035c0 100644 --- a/spot/taalgos/tgba2ta.hh +++ b/spot/taalgos/tgba2ta.hh @@ -37,7 +37,7 @@ namespace spot /// \param degeneralized When false, the returned automaton is a generalized /// form of TA, called GTA (Generalized Testing Automaton). /// Like TGBA, GTA use Generalized Büchi acceptance - /// conditions intead of Buchi-accepting states: there are several acceptance + /// conditions instead of Buchi-accepting states: there are several acceptance /// sets (of transitions), and a path is accepted if it traverses /// at least one transition of each set infinitely often or if it contains a /// livelock-accepting cycle (like a TA). The spot emptiness check algorithm diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc index 504f624ae..6cea88ea6 100644 --- a/spot/tl/apcollect.cc +++ b/spot/tl/apcollect.cc @@ -69,7 +69,7 @@ namespace spot { atomic_prop_set res; - // polirity: 0 = negative, 1 = positive, 2 or more = both. + // polarity: 0 = negative, 1 = positive, 2 or more = both. auto rec = [&res](formula f, unsigned polarity, auto self) { switch (f.kind()) diff --git a/spot/tl/apcollect.hh b/spot/tl/apcollect.hh index d35461035..fec68287c 100644 --- a/spot/tl/apcollect.hh +++ b/spot/tl/apcollect.hh @@ -57,7 +57,7 @@ namespace spot atomic_prop_collect_as_bdd(formula f, const twa_ptr& a); - /// \brief Collect the literals occuring in f + /// \brief Collect the literals occurring in f /// /// This function records each atomic proposition occurring in f /// along with the polarity of its occurrence. For instance if the diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 3c5afc8d1..db4b32ec7 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -276,7 +276,7 @@ namespace spot // pointers we should remove. We can do it in the same loop. // // It is simpler to construct a separate vector to do that, but that's - // only needed if we have nested multops or null poiners. + // only needed if we have nested multops or null pointers. if (std::find_if(v.begin(), v.end(), [o](const fnode* f) { return f == nullptr || f->is(o); }) != v.end()) diff --git a/spot/tl/parse.hh b/spot/tl/parse.hh index 5907d2756..3702807b2 100644 --- a/spot/tl/parse.hh +++ b/spot/tl/parse.hh @@ -110,7 +110,7 @@ namespace spot /// field parsed_formula::f in the returned object can be a non-zero /// value even if it encountered error during the parsing of \a /// ltl_string. If you want to make sure \a ltl_string was parsed - /// succesfully, check \a parsed_formula::errors for emptiness. + /// successfully, check \a parsed_formula::errors for emptiness. /// /// \warning This function is not reentrant. SPOT_API @@ -133,7 +133,7 @@ namespace spot /// field parsed_formula::f in the returned object can be a non-zero /// value even if it encountered error during the parsing of \a /// ltl_string. If you want to make sure \a ltl_string was parsed - /// succesfully, check \a parsed_formula::errors for emptiness. + /// successfully, check \a parsed_formula::errors for emptiness. /// /// \warning This function is not reentrant. SPOT_API @@ -154,7 +154,7 @@ namespace spot /// field parsed_formula::f in the returned object can be a non-zero /// value even if it encountered error during the parsing of \a /// ltl_string. If you want to make sure \a ltl_string was parsed - /// succesfully, check \a parsed_formula::errors for emptiness. + /// successfully, check \a parsed_formula::errors for emptiness. /// /// The LBT syntax, also used by the lbtt and scheck tools, is /// extended to support W, and M operators (as done in lbtt), and @@ -191,7 +191,7 @@ namespace spot /// field parsed_formula::f in the returned object can be a non-zero /// value even if it encountered error during the parsing of \a /// ltl_string. If you want to make sure \a ltl_string was parsed - /// succesfully, check \a parsed_formula::errors for emptiness. + /// successfully, check \a parsed_formula::errors for emptiness. /// /// \warning This function is not reentrant. SPOT_API diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh index 99b664b00..d4c52debf 100644 --- a/spot/tl/randomltl.hh +++ b/spot/tl/randomltl.hh @@ -200,7 +200,7 @@ namespace spot class SPOT_API random_sere final: public random_formula { public: - /// Create a random SERE genere using atomic propositions from \a ap. + /// Create a random SERE generator using atomic propositions from \a ap. /// /// The default priorities are defined as follows: /// diff --git a/spot/tl/relabel.hh b/spot/tl/relabel.hh index 1f8e32f22..1d4bbc12d 100644 --- a/spot/tl/relabel.hh +++ b/spot/tl/relabel.hh @@ -35,7 +35,7 @@ namespace spot /// between the new names (keys) and the old names (values). /// /// \see relabel_bse - /// \see relabel_overlaping_bse + /// \see relabel_overlapping_bse SPOT_API formula relabel(formula f, relabeling_style style, relabeling_map* m = nullptr); diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index c670fc730..5ed627c1b 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -948,7 +948,7 @@ namespace spot { } - // if !neg build c&X(c&X(...&X(tail))) with n occurences of c + // if !neg build c&X(c&X(...&X(tail))) with n occurrences of c // if neg build !c|X(!c|X(...|X(tail))). formula dup_b_x_tail(bool neg, formula c, formula tail, unsigned n) @@ -1027,7 +1027,7 @@ namespace spot // // The above usually make more sense when reversed (see // them in the And and Or rewritings), except when we - // try to maximaze the size of subformula that do not + // try to maximize the size of subformula that do not // have EventUniv formulae. if (opt_.favor_event_univ) if (c.is(op::Or, op::And)) @@ -1585,7 +1585,7 @@ namespace spot } } } - // {b[*i..j]} = b&X(b&X(... b)) with i occurences of b + // {b[*i..j]} = b&X(b&X(... b)) with i occurrences of b // !{b[*i..j]} = !b&X(!b&X(... !b)) if (!opt_.reduce_size_strictly) if (c.is(op::Star)) diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 02fc8f5e0..1749e45cd 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1186,7 +1186,7 @@ namespace spot /// \brief Convert the acceptance formula into a BDD /// - /// \a map should be a vector indiced by colors, that + /// \a map should be a vector indexed by colors, that /// maps each color to the desired BDD representation. bdd to_bdd(const bdd* map) const; @@ -1275,7 +1275,7 @@ namespace spot /// Fin(i) changed to true and Inf(i) to false. /// /// If the condition is a disjunction and one of the disjunct - /// has the shape `...&Fin(i)&...`, then `i` will be prefered + /// has the shape `...&Fin(i)&...`, then `i` will be preferred /// over any arbitrary Fin. /// /// The second element of the pair, is the same acceptance @@ -1307,7 +1307,7 @@ namespace spot /// If no disjunct has the right shape, then a random Fin(i) is /// searched in the formula, and the output (i, left, right). /// is such that left contains all disjuncts containing Fin(i) - /// (at any depth), and right contains the original formlula + /// (at any depth), and right contains the original formula /// where Fin(i) has been replaced by false. /// @{ std::tuple @@ -1345,7 +1345,7 @@ namespace spot /// \brief Check potential acceptance of an SCC. /// /// Assuming that an SCC intersects all sets in \a - /// infinitely_often (i.e., for each set in \a infinetely_often, + /// infinitely_often (i.e., for each set in \a infinitely_often, /// there exist one marked transition in the SCC), and is /// included in all sets in \a always_present (i.e., all /// transitions are marked with \a always_present), this returns @@ -1464,7 +1464,7 @@ namespace spot /// "Fin(!x)" and "Inf(!x)" are not supported by this parser. /// /// Or the string could be the name of an acceptance condition, as - /// speficied in the HOA format. (E.g. "Rabin 2", "parity max odd 3", + /// specified in the HOA format. (E.g. "Rabin 2", "parity max odd 3", /// "generalized-Rabin 4 2 1", etc.). /// /// A spot::parse_error is thrown on syntax error. @@ -2190,7 +2190,7 @@ namespace spot /// Fin(i) changed to true and Inf(i) to false. /// /// If the condition is a disjunction and one of the disjunct - /// has the shape `...&Fin(i)&...`, then `i` will be prefered + /// has the shape `...&Fin(i)&...`, then `i` will be preferred /// over any arbitrary Fin. /// /// The second element of the pair, is the same acceptance @@ -2226,7 +2226,7 @@ namespace spot /// If no disjunct has the right shape, then a random Fin(i) is /// searched in the formula, and the output (i, left, right). /// is such that left contains all disjuncts containing Fin(i) - /// (at any depth), and right contains the original formlula + /// (at any depth), and right contains the original formula /// where Fin(i) has been replaced by false. /// @{ std::tuple diff --git a/spot/twa/bddprint.hh b/spot/twa/bddprint.hh index a85acb765..2ed55d333 100644 --- a/spot/twa/bddprint.hh +++ b/spot/twa/bddprint.hh @@ -40,7 +40,7 @@ namespace spot /// This assumes that \a b is a conjunction of literals. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. - /// \return The BDD formated as a string. + /// \return The BDD formatted as a string. SPOT_API std::string bdd_format_sat(const bdd_dict_ptr& dict, bdd b); @@ -50,7 +50,7 @@ namespace spot /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. - /// \return The BDD formated as a string. + /// \return The BDD formatted as a string. SPOT_API std::ostream& bdd_print_accset(std::ostream& os, const bdd_dict_ptr& dict, bdd b); @@ -59,7 +59,7 @@ namespace spot /// This is used when saving a TGBA. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. - /// \return The BDD formated as a string. + /// \return The BDD formatted as a string. SPOT_API std::string bdd_format_accset(const bdd_dict_ptr& dict, bdd b); @@ -73,7 +73,7 @@ namespace spot /// \brief Format a BDD as a set. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. - /// \return The BDD formated as a string. + /// \return The BDD formatted as a string. SPOT_API std::string bdd_format_set(const bdd_dict_ptr& dict, bdd b); @@ -87,7 +87,7 @@ namespace spot /// \brief Format a BDD as a formula. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. - /// \return The BDD formated as a string. + /// \return The BDD formatted as a string. SPOT_API std::string bdd_format_formula(const bdd_dict_ptr& dict, bdd b); @@ -98,7 +98,7 @@ namespace spot /// \brief Format a BDD as an irredundant sum of product. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. - /// \return The BDD formated as a string. + /// \return The BDD formatted as a string. SPOT_API std::string bdd_format_isop(const bdd_dict_ptr& dict, bdd b); diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc index 540426d85..8c1223f93 100644 --- a/spot/twa/formula2bdd.cc +++ b/spot/twa/formula2bdd.cc @@ -25,7 +25,7 @@ namespace spot { namespace { - // Convert a BDD which is known to be a conjonction into a formula. + // Convert a BDD which is known to be a conjunction into a formula. // If dual is true, dualize the result, i.e., negate literals, and // exchange ∧ and ∨. template diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 85a755873..053344cf2 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -630,14 +630,14 @@ namespace spot /// \brief Get the initial state of the automaton. /// /// The state has been allocated with \c new. It is the - /// responsability of the caller to \c destroy it when no + /// responsibility of the caller to \c destroy it when no /// longer needed. virtual const state* get_init_state() const = 0; /// \brief Get an iterator over the successors of \a local_state. /// /// The iterator has been allocated with \c new. It is the - /// responsability of the caller to \c delete it when no + /// responsibility of the caller to \c delete it when no /// longer needed. /// /// \see succ() @@ -785,7 +785,7 @@ namespace spot /// \brief Format the state as a string for printing. /// - /// Formating is the responsability of the automata that owns the + /// Formatting is the responsibility of the automata that owns the /// state, so that state objects could be implemented as very /// small objects, maybe sharing data with other state objects via /// data structure stored in the automaton. @@ -795,7 +795,7 @@ namespace spot /// /// This converts \a s, into that corresponding spot::state for \a /// t. This is useful when you have the state of a product, and - /// want to restrict this state to a specific automata occuring in + /// want to restrict this state to a specific automata occurring in /// the product. /// /// It goes without saying that \a s and \a t should be compatible diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index eb74dd496..2ccc411a9 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -412,7 +412,7 @@ namespace spot // (We will use two hash maps in this case.) auto sp = get_named_prop>("state-player"); - // The hashing is a bit delicat: We may only use the dst if it has + // The hashing is a bit delicate: We may only use the dst if it has // no self-loop. HASH_OF_STATE stores the hash associated to each // state (by default its own number) or some common value if the // state contains self-loop. @@ -505,7 +505,7 @@ namespace spot } // All states that might possible be merged share the same hash // Info hash coll - //std::cout << "Hash collission rate pre merge: " + //std::cout << "Hash collision rate pre merge: " // << ((map0.size()+map1.size())/((float)n_states)) // << '\n'; @@ -561,7 +561,7 @@ namespace spot sl1 = e_chain[sl1]; sl2 = e_chain[sl2]; } - // Since edges are ordered on each side, aadvance + // Since edges are ordered on each side, advance // the smallest side in case there is no match. else if (edge_data_comp(data1, data2)) sl1 = e_chain[sl1]; @@ -747,7 +747,7 @@ namespace spot if (merged) defrag_states(remap, st); // Info hash coll 2 - //std::cout << "Hash collission rate post merge: " + //std::cout << "Hash collision rate post merge: " // << ((map0.size()+map1.size())/((float)num_states())) // << '\n'; return merged; diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 30a023c68..36fa31836 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -600,7 +600,7 @@ namespace spot /// the edges /// \param to_merge_ptr Determines which states are candidates. /// If null, all states are considered - /// The actual implementation differd from merge_states(). + /// The actual implementation differs from merge_states(). /// It is more costly, but is more precise, in the sense that /// more states are merged. unsigned merge_states_of(bool stable = true, diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 659dd281d..95c758ede 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1031,7 +1031,7 @@ namespace spot it2.first.first.id(), it2.first.second.id()); }); if (itm == occur_map.cend()) - throw std::runtime_error("Empty occurence map"); + throw std::runtime_error("Empty occurrence map"); return *itm; }; @@ -1180,7 +1180,7 @@ namespace spot // Create all the bdds/vars // true/false/latches/inputs already exist - // Get the gatenumber corresponding to an output + // Get the gate number corresponding to an output auto v2g = [&](unsigned v)->unsigned { v = circ.aig_pos(v); diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 1fe2ffddf..129f12ad2 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -86,7 +86,7 @@ namespace spot public: - /// \brief Mark the beginning of a test tranlation + /// \brief Mark the beginning of a test translation /// /// Sometimes different encodings produces more or less gates. /// To improve performances, one can "safe" the current status @@ -297,7 +297,7 @@ namespace spot /// \param method How to translate the bdd. 0: If-then-else normal form, /// 1: isop normal form, 2: try both and retain smaller /// \param use_dual Encode the negations of the given bdds and - /// retain the smalles implementation + /// retain the smallest implementation /// \param use_split_off 0: Use base algo /// 1: Separate the different types of input signals /// (like latches, inputs) to increase gate diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index 1e0ba87ed..a03ddc121 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -40,7 +40,7 @@ namespace spot /// /// operator() can be called on states with universal branching /// (that's actually the point), and can be called on state number - /// that designate groupes of destination states (in that case the + /// that designate groups of destination states (in that case the /// conjunction of all those states are taken). class SPOT_API outedge_combiner { diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 454b531c1..26f6f834f 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -549,7 +549,7 @@ namespace spot for (auto& e: aut->edges()) { - // Just avoit the e.acc.sets() loops on marks that we have + // Just avoid the e.acc.sets() loops on marks that we have // just seen. if (e.acc == previous_a) continue; diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 986c982fb..509cb4d88 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -408,7 +408,7 @@ namespace spot // Each state is characterized by a bitvect_array of 2 bitvects: // bv1 -> the set of original states that it represents // bv2 -> a set of marked states (~) - // To do so, we keep a correspondance between a state number and its + // To do so, we keep a correspondence between a state number and its // bitvect representation. dca_st_mapping bv_to_num_; std::vector> num_2_bv_; diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index 3df305379..67791dbac 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -80,14 +80,14 @@ namespace spot bool are_equivalent(const_twa_graph_ptr left, formula right) { - // The first containement check does not involve a + // The first containment check does not involve a // complementation, the second might. return contains(left, right) && contains(right, left); } bool are_equivalent(formula left, const_twa_graph_ptr right) { - // The first containement check does not involve a + // The first containment check does not involve a // complementation, the second might. return contains(right, left) && contains(left, right); } diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index 62cbb7aa1..59efbef16 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -282,7 +282,7 @@ namespace spot const_twa_ptr>::type; // The status of the emptiness-check on success. - // It contains everyting needed to build a counter-example: + // It contains everything needed to build a counter-example: // the automaton, the stack of SCCs traversed by the counter-example, // and the heap of visited states with their indices. template @@ -579,7 +579,7 @@ namespace spot return check_impl(); } - // The following two methods anticipe the future interface of the + // The following two methods anticipate the future interface of the // class emptiness_check. Following the interface of twa, the class // emptiness_check_result should not be exposed. bool diff --git a/spot/twaalgos/cycles.hh b/spot/twaalgos/cycles.hh index bd613a1c2..fda2210e6 100644 --- a/spot/twaalgos/cycles.hh +++ b/spot/twaalgos/cycles.hh @@ -43,7 +43,7 @@ namespace spot /// /// We represent a cycle by a sequence of succ_iterator objects /// positioned on the transition contributing to the cycle. These - /// succ_itertor are stored, along with their source state, in the + /// succ_iterator are stored, along with their source state, in the /// dfs_ stack. Only the last portion of this stack may form a /// cycle. /// diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index fc737e3f7..897062cb3 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -32,7 +32,7 @@ namespace spot { namespace { - // A state in the degenalized automaton corresponds to a state in + // A state in the degeneralized automaton corresponds to a state in // the TGBA associated to a level. The level is just an index in // the list of acceptance sets. typedef std::pair degen_state; @@ -495,7 +495,7 @@ namespace spot levels->emplace_back(ds.second); // Level cache stores one encountered level for each state - // (the value of use_lvl_cache determinates which level + // (the value of use_lvl_cache determines which level // should be remembered). This cache is used when // re-entering the SCC. if (use_lvl_cache) @@ -579,7 +579,7 @@ namespace spot // where 1 is initial and => marks accepting // edges: 1=>1, 1=>2, 2->2, 2->1. This is // already an SBA, with 1 as accepting state. - // However if you try degeralize it without + // However if you try degeneralize it without // ignoring *prev, you'll get two copies of state // 2, depending on whether we reach it using 1=>2 // or from 2->2. If this example was not clear, diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index b04ae7bb8..643c1d219 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -28,7 +28,7 @@ namespace spot /// \brief Degeneralize a generalized (co)Büchi automaton into an /// equivalent (co)Büchi automaton. /// - /// There are two variants of the function. If the generalizd + /// There are two variants of the function. If the generalized /// (co)Büchi acceptance uses N colors, degeneralize() algorithm /// will builds a state-based (co)Büchi automaton that has at most /// (N+1) times the number of states of the original automaton. @@ -38,12 +38,12 @@ namespace spot /// /// Additional options control optimizations described in /// \cite babiak.13.spin . When \a use_z_lvl is set, the level of - /// the degeneralized automaton is reset everytime an SCC is exited. + /// the degeneralized automaton is reset every time an SCC is exited. /// If \a use_cust_acc_orders is set, the degeneralization will /// compute a custom acceptance order for each SCC (this option is /// disabled by default because our benchmarks show that it usually /// does more harm than good). If \a use_lvl_cache is set, - /// everytime an SCC is entered on a state that as already been + /// every time an SCC is entered on a state that as already been /// associated to some level elsewhere, reuse that level (set it to /// 2 to keep the smallest number, 3 to keep the largest level, and /// 1 to keep the first level found). If \a ignaccsl is set, we do @@ -75,7 +75,7 @@ namespace spot /// /// As an alternative method to degeneralization, one may also /// consider ACD transform. acd_transform() will never produce - /// larger automata than degenaralize_tba(), and + /// larger automata than degeneralize_tba(), and /// acd_transform_sbacc() produce smaller automata than /// degeneralize() on the average. See \cite casares.22.tacas for /// some comparisons. diff --git a/spot/twaalgos/dot.hh b/spot/twaalgos/dot.hh index fbf63e641..0483967fb 100644 --- a/spot/twaalgos/dot.hh +++ b/spot/twaalgos/dot.hh @@ -29,7 +29,7 @@ namespace spot /// \brief Print reachable states in dot format. /// /// If \a assume_sba is set, this assumes that the automaton - /// is an SBA and use double elipse to mark accepting states. + /// is an SBA and use double ellipse to mark accepting states. /// /// \param options an optional string of letters, each indicating a /// different option. Presently the following options are diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index 90319bd20..4a95eed8c 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -243,7 +243,7 @@ namespace spot // it is necessary to associate to each path constructed, an ID number. // // Given this ID, src_cand, dst_cand and a boolean that tells we want - // ref or cand var, the corresponding litteral can be retrieved thanks + // ref or cand var, the corresponding literal can be retrieved thanks // to get_prc(...), a vars_helper's method. unsigned path_size = 0; for (unsigned i = 0; i < d.ref_size; ++i) @@ -264,8 +264,8 @@ namespace spot } } - // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's - // corresponding index in alpha_map. This is necessary beacause + // Fill dict's bdd vector (alpha_vect) and save each bdd and it's + // corresponding index in alpha_map. This is necessary because // some loops start from a precise bdd. Therefore, it's useful // to know its corresponding index to deal with vars_helper. unsigned j = 0; @@ -281,7 +281,7 @@ namespace spot d.helper.init(d.cand_size, d.alpha_vect.size(), d.cand_size, 1, path_size, state_based, true); - // Based on all previous informations, helper knows all litterals. + // Based on all previous informations, helper knows all literals. d.helper.declare_all_vars(++d.nvars); } @@ -399,7 +399,7 @@ namespace spot const acc_cond& ra = ref->acc(); - // construction of contraints (4,5) : all loops in the product + // construction of constraints (4,5) : all loops in the product // where no accepting run is detected in the ref. automaton, // must also be marked as not accepting in the cand. automaton for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) @@ -473,7 +473,7 @@ namespace spot } } } - // construction of contraints (6,7): all loops in the product + // construction of constraints (6,7): all loops in the product // where accepting run is detected in the ref. automaton, must // also be marked as accepting in the candidate. for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 64dfbd5f6..93e482a3b 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -459,8 +459,8 @@ namespace spot // refhist, it is necessary to associate to each path constructed, // an ID number. // - // Given this ID, src_cand, dst_cand, the corresponding litteral can be - // retrived thanks to get_prc(...) a vars_helper's method. + // Given this ID, src_cand, dst_cand, the corresponding literal can be + // retrieved thanks to get_prc(...) a vars_helper's method. unsigned path_size = 0; for (unsigned i = 0; i < d.ref_size; ++i) { @@ -493,8 +493,8 @@ namespace spot } } - // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's - // corresponding index in alpha_map. This is necessary beacause + // Fill dict's bdd vector (alpha_vect) and save each bdd and it's + // corresponding index in alpha_map. This is necessary because // some loops start from a precise bdd. Therefore, it's useful // to know its corresponding index to deal with vars_helper. unsigned j = 0; @@ -510,7 +510,7 @@ namespace spot d.helper.init(d.cand_size, d.alpha_vect.size(), d.cand_size, d.cand_nacc, path_size, state_based, false); - // Based on all previous informations, helper knows all litterals. + // Based on all previous informations, helper knows all literals. d.helper.declare_all_vars(++d.nvars); } @@ -909,7 +909,7 @@ namespace spot dout << "--- transition_acc variables ---\n"; if (state_based) { - dout << "In state_based mode, there is only 1 litteral for each " + dout << "In state_based mode, there is only 1 literal for each " "combination of src and nacc, regardless of dst or cond!\n"; for (unsigned i = 0; i < satdict.cand_size; ++i) for (unsigned j = 0; j < satdict.cand_nacc; ++j) diff --git a/spot/twaalgos/dtwasat.hh b/spot/twaalgos/dtwasat.hh index f51ca1405..64e01c7ae 100644 --- a/spot/twaalgos/dtwasat.hh +++ b/spot/twaalgos/dtwasat.hh @@ -85,7 +85,7 @@ namespace spot /// \brief Attempt to minimize a deterministic TωA with a SAT solver. /// - /// It acts like dtwa_sat_synthetisze() and obtains a first minimized + /// It acts like dtwa_sat_synthetize() and obtains a first minimized /// automaton. Then, incrementally, it encodes and solves the deletion of one /// state as many time as param value. /// If param >= 0, this process is fully repeated until the minimal automaton diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index bd0f4767d..f342439d9 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -177,7 +177,7 @@ namespace spot } }; - // Iterating over all mineterms can be very slow when |AP| + // Iterating over all minterms can be very slow when |AP| // is large (see issue #566) . The else branch implements // another approach that should be exponential in the // number of successors instead of in the number of atomic diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index cd9b40c3f..c204e8cc0 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -112,7 +112,7 @@ namespace spot return a_; } - /// Return the options parametrizing how the accepting run is computed. + // / Return the options parameterizing how the accepting run is computed. const option_map& options() const { @@ -153,7 +153,7 @@ namespace spot return a_; } - /// Return the options parametrizing how the emptiness check is realized. + /// Return the options parameterizing how the emptiness check is realized. const option_map& options() const { diff --git a/spot/twaalgos/emptiness_stats.hh b/spot/twaalgos/emptiness_stats.hh index 936929bc3..55df5d621 100644 --- a/spot/twaalgos/emptiness_stats.hh +++ b/spot/twaalgos/emptiness_stats.hh @@ -127,7 +127,7 @@ namespace spot } private : - unsigned states_; /// number of disctint visited states + unsigned states_; /// number of distinct visited states unsigned transitions_; /// number of visited transitions unsigned depth_; /// maximal depth of the stack(s) unsigned max_depth_; /// maximal depth of the stack(s) diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 3c7758161..404fa4778 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -491,7 +491,7 @@ namespace spot bool acc_par, par_t min_win_par, bool respect_sg=true) { // In fix_scc, the attr computation is - // abused so we can not check ertain things + // abused so we can not check certain things // Computes the attractor of the winning set of player p within a // subgame given as rd. // If acc_par is true, max_par transitions are also accepting and @@ -860,7 +860,7 @@ namespace spot // during construction std::vector s_; - // Informations about sccs andthe current scc + // Informations about sccs and the current scc std::unique_ptr info_; par_t max_abs_par_; // Max parity occurring in the current scc // Minimal and maximal parity occurring in the entire graph @@ -1112,7 +1112,7 @@ namespace spot if (owners->size() != arena->num_states()) throw std::runtime_error("set_state_player(): The \"state-player\" " "vector has a different " - "size comparerd to the automaton! " + "size compared to the automaton! " "Called new_state in between?"); (*owners)[state] = owner; @@ -1286,7 +1286,7 @@ namespace spot game->set_named_prop("strategy", strategy); // transposed is a reversed copy of game to compute predecessors - // more easily. It also keep track of the original edge iindex. + // more easily. It also keep track of the original edge index. struct edge_data { unsigned edgeidx; }; diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index 0a6de1040..8854c0ebc 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -114,7 +114,7 @@ namespace spot /// Give the set of transitions contained in /// an accepting cycle of the SCC \a scc of \a aut. /// - /// \param si scc_info used to describle the automaton + /// \param si scc_info used to describe the automaton /// \param scc SCC to consider /// \param aut_acc Acceptance condition used for this SCC /// \param removed_colors A set of colors that can't appear on a transition diff --git a/spot/twaalgos/hoa.hh b/spot/twaalgos/hoa.hh index 9a53f41c9..48d730444 100644 --- a/spot/twaalgos/hoa.hh +++ b/spot/twaalgos/hoa.hh @@ -153,7 +153,7 @@ namespace spot /// \brief Retrieve the list of aliases. /// - /// This points to the same list that the automaton's "aliasaes" + /// This points to the same list that the automaton's "aliases" /// named properties points to. Will return `nullptr` if no /// aliases are defined. /// diff --git a/spot/twaalgos/langmap.hh b/spot/twaalgos/langmap.hh index 98e783f41..4b1a71308 100644 --- a/spot/twaalgos/langmap.hh +++ b/spot/twaalgos/langmap.hh @@ -26,8 +26,8 @@ namespace spot /// \brief Identify states that recognize the same language. /// /// The returned vector is the same size as the automaton's number of state. - /// The number of different values (ignoring occurences) in the vector is the - /// total number of recognized languages, states recognizing the same + // / The number of different values (ignoring occurrences) in the vector is + /// the total number of recognized languages, states recognizing the same /// language have the same value. /// /// The given automaton must be deterministic. diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index 554b8019d..ac7c5645e 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -67,7 +67,7 @@ namespace spot /// for the type of reduction you want, see spot::tl_simplifier. /// This idea is taken from \cite thirioux.02.fmics . /// - /// \param unambiguous When true, unambigous TGBA will be produced + /// \param unambiguous When true, unambiguous TGBA will be produced /// using the trick described in \cite benedikt.13.tacas . /// /// \param aborter When given, aborts the construction whenever the diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index 635bba286..f8e986449 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -211,7 +211,7 @@ namespace spot // the test 'c.get_color() != RED' is added to limit // the number of runs reported by successive // calls to the check method. Without this - // functionnality, the test can be ommited. + // functionality, the test can be omitted. trace << " It is blue and the arc is " << "accepting, start a red dfs" << std::endl; target = f.s; @@ -242,7 +242,7 @@ namespace spot // the test 'c.get_color() != RED' is added to limit // the number of runs reported by successive // calls to the check method. Without this - // functionnality, the test can be ommited. + // functionality, the test can be omitted. trace << " It is blue and the arc from " << a_->format_state(st_blue.front().s) << " to it is accepting, start a red dfs" diff --git a/spot/twaalgos/magic.hh b/spot/twaalgos/magic.hh index c8e3e4261..99f46f3d8 100644 --- a/spot/twaalgos/magic.hh +++ b/spot/twaalgos/magic.hh @@ -33,7 +33,7 @@ namespace spot /// \pre The automaton \a a must have at most one acceptance condition (i.e. /// it is a TBA). /// - /// During the visit of \a a, the returned checker stores explicitely all + /// During the visit of \a a, the returned checker stores explicitly all /// the traversed states. /// The method \a check() of the checker can be called several times /// (until it returns a null pointer) to enumerate all the visited acceptance @@ -88,11 +88,11 @@ namespace spot /// \pre The automaton \a a must have at most one acceptance condition (i.e. /// it is a TBA). /// - /// During the visit of \a a, the returned checker does not store explicitely + /// During the visit of \a a, the returned checker does not store explicitly /// the traversed states but uses the bit-state hashing technic presented in: /// \cite Holzmann.91.book. /// - /// Consequently, the detection of an acceptence cycle is not ensured. + /// Consequently, the detection of an acceptance cycle is not ensured. /// /// The size of the heap is limited to \n size bytes. /// diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 564622bed..5a022bfc0 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -136,7 +136,7 @@ namespace spot /// /// It can modify either the condition or the acceptance sets of /// the edges. Set the condition to bddfalse to remove it. Note that - /// all transtions will be processed. + /// all transitions will be processed. /// \param init The optional new initial state. template void transform_copy(const const_twa_graph_ptr& old, @@ -157,7 +157,7 @@ namespace spot acc_cond::mark_t acc = t.acc; trans(t.src, cond, acc, t.dst); // Having the same number of states should assure that state ids are - // equivilent in old and cpy. + // equivalent in old and cpy. SPOT_ASSERT(t.src < cpy->num_states() && t.dst < cpy->num_states()); if (cond != bddfalse) cpy->new_edge(t.src, t.dst, cond, acc); diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 512848edb..055cb511e 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -99,7 +99,7 @@ namespace { if (!f) throw std::runtime_error("`" + name + - "' could not be oppened for writing."); + "' could not be opened for writing."); } ~fwrapper() { @@ -257,7 +257,7 @@ namespace spot if (!is_deterministic_(ins)) { trace << "is_input_deterministic_mealy(): State number " - << s << " is not input determinisc!\n"; + << s << " is not input determinist!\n"; return false; } } diff --git a/spot/twaalgos/mealy_machine.hh b/spot/twaalgos/mealy_machine.hh index 9fd3c084e..baeca6c4f 100644 --- a/spot/twaalgos/mealy_machine.hh +++ b/spot/twaalgos/mealy_machine.hh @@ -91,7 +91,7 @@ namespace spot /// \brief split a separated mealy machine /// /// In a separated mealy machine, every transitions as a label of - /// the form `(in)&(out)`. This function will turn each transtion + /// the form `(in)&(out)`. This function will turn each transition /// into a pair of consecutive transitions labeled by `in` and /// `out`, and turn the mealy machine into a game (what we call a /// split mealy machine) @@ -197,7 +197,7 @@ namespace spot /// \pre The machines have to be both either split or unsplit, /// input complete and compatible. All of this is checked by assertion. /// \result A mealy machine representing the shared behaviour, - /// with the same tyoe (mealy/separated/split) as the input machines + /// with the same type (mealy/separated/split) as the input machines SPOT_API twa_graph_ptr mealy_product(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right); diff --git a/spot/twaalgos/minimize.hh b/spot/twaalgos/minimize.hh index e9390c6c1..0b5c11bf2 100644 --- a/spot/twaalgos/minimize.hh +++ b/spot/twaalgos/minimize.hh @@ -95,7 +95,7 @@ namespace spot /// returned. Otherwise, if \a aut_neg_f was not supplied but \a f /// was, \a aut_neg_f is built from the negation of \a f. Then we /// check that product(aut,!minimize(aut_f)) and - /// product(aut_neg_f,minize(aut)) are both empty. If they + /// product(aut_neg_f,minimize(aut)) are both empty. If they /// are, the the minimization was sound. (See the paper for full /// details.) /// diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index f3765305f..cf84e7da8 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -133,7 +133,7 @@ namespace spot current_odd = current_odd != toggle_style; bool change_style = false; auto num_sets = old_num_sets; - // If the parity neeeds to be changed, then a new acceptance set is created. + // If the parity needs to be changed, then a new acceptance set is created. // The old acceptance sets are shifted if (output_odd != current_odd) { diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index 4043affc2..5363161fc 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -166,7 +166,7 @@ namespace spot /// When \a layered is true all transition that belong to the same /// layer receive the same color. When layer is `false`, only the /// transition that where used initially to define the layers (i.e, - /// the transition with the maximal color in the previous exemple), + /// the transition with the maximal color in the previous example), /// get their color adjusted. The other will receive either no /// color (if \a colored is false), or a useless color (if \a colored /// is true). Here "useless color" means the smallest color diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 0a5979064..eabde299b 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -365,7 +365,7 @@ namespace spot // However (1) degeneralization is faster if the input is // GBA, and (2) if we want a deterministic parity automaton and the // input is not deterministic, that is useless here. We need - // to determinize it first, and our deterministization + // to determinize it first, and our determinization // function only deal with TGBA as input. if ((via_gba || (want_parity && !a->acc().is_parity())) && !a->acc().is_generalized_buchi()) diff --git a/spot/twaalgos/product.hh b/spot/twaalgos/product.hh index 796e4c23c..39bdad0be 100644 --- a/spot/twaalgos/product.hh +++ b/spot/twaalgos/product.hh @@ -38,7 +38,7 @@ namespace spot /// conjunction of the acceptance conditions of the two input /// automata. /// - /// As an optionmization, in case one of the left or right automaton + /// As an optimization, in case one of the left or right automaton /// is weak, the acceptance condition of the result is made simpler: /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. @@ -69,7 +69,7 @@ namespace spot /// conjunction of the acceptance conditions of the two input /// automata. /// - /// As an optionmization, in case one of the left or right automaton + /// As an optimization, in case one of the left or right automaton /// is weak, the acceptance condition of the result is made simpler: /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. @@ -98,7 +98,7 @@ namespace spot /// disjunction of the acceptance conditions of the two input /// automata. /// - /// As an optionmization, in case one of the left or right automaton + /// As an optimization, in case one of the left or right automaton /// is weak, the acceptance condition of the result is made simpler: /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. @@ -126,7 +126,7 @@ namespace spot /// disjunction of the acceptance conditions of the two input /// automata. /// - /// As an optionmization, in case one of the left or right automaton + /// As an optimization, in case one of the left or right automaton /// is weak, the acceptance condition of the result is made simpler: /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. diff --git a/spot/twaalgos/reachiter.hh b/spot/twaalgos/reachiter.hh index f1faf8b99..f9b45d38a 100644 --- a/spot/twaalgos/reachiter.hh +++ b/spot/twaalgos/reachiter.hh @@ -73,7 +73,7 @@ namespace spot /// \param in The source state number. /// \param out_s The destination state /// \param out The destination state number. - /// \param si The spot::twa_succ_iterator positionned on the current + /// \param si The spot::twa_succ_iterator positioned on the current /// transition. /// /// The in_s and out_s states are owned by the @@ -141,7 +141,7 @@ namespace spot /// \param in The source state number. /// \param out_s The destination state /// \param out The destination state number. - /// \param si The spot::twa_succ_iterator positionned on the current + /// \param si The spot::twa_succ_iterator positioned on the current /// transition. /// /// The in_s and out_s states are owned by the diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index 594b8bdeb..9a34da7c5 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -137,7 +137,7 @@ namespace spot }; - // When split we need to distiguish effectively new and old edges + // When split we need to distinguish effectively new and old edges if (split) { aut.get_graph().remove_dead_edges_(); @@ -381,12 +381,12 @@ namespace spot } - // Save the composed letters? With a special seperator like T/F? + // Save the composed letters? With a special separator like T/F? // Is swapping between formula <-> bdd expensive for (auto& e : aut.edges()) translate(e.cond); - // Remove the new auxilliary variables from the aut + // Remove the new auxiliary variables from the aut bdd c_supp = new_var_supp; while (c_supp != bddtrue) { diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 435fdfa6c..aff736bf0 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -176,7 +176,7 @@ namespace spot // Specialized conversion from transition based Rabin acceptance to // transition based Büchi acceptance. // Is able to detect SCCs that are TBA-type (i.e., they can be - // converted to Büchi acceptance without chaning their structure). + // converted to Büchi acceptance without changing their structure). // // See "Deterministic ω-automata vis-a-vis Deterministic Büchi // Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for @@ -381,7 +381,7 @@ namespace spot { true, // state based true, // inherently weak - true, true, // determinisitic + true, true, // deterministic true, // complete true, // stutter inv. }); @@ -667,7 +667,7 @@ namespace spot << main_add << '\n'; // If the SCC is rejecting, there is no need for clone. - // Pretend we don't interesect any Fin. + // Pretend we don't intersect any Fin. if (si.is_rejecting_scc(n)) intersects_fin = false; diff --git a/spot/twaalgos/remfin.hh b/spot/twaalgos/remfin.hh index 08cb786a4..7d47b6b42 100644 --- a/spot/twaalgos/remfin.hh +++ b/spot/twaalgos/remfin.hh @@ -23,7 +23,7 @@ namespace spot { /// \ingroup twa_acc_transform - /// \brief Check if \a aut is Rablin-like and Büchi-realizable. + /// \brief Check if \a aut is Rabin-like and Büchi-realizable. /// /// This is inspired from rabin_to_buchi_maybe()'s algorithm. The /// main difference is that here, no automaton is built. diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 9ec3f1c0e..5d67f1b1e 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -231,7 +231,7 @@ namespace spot // all acceptance sets, as this edge cannot be part // of any loop. // - If an edge is in an non-accepting SCC, we can only - // remove the Inf sets, as removinf the Fin sets + // remove the Inf sets, as removing the Fin sets // might make the SCC accepting. // // The above rules are made more complex with two flags: diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index ea36e77e0..76dd3ed8b 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -319,7 +319,7 @@ namespace spot /// \brief True if we know that the SCC has an accepting cycle /// /// Note that both is_accepting() and is_rejecting() may return - /// false if an SCC interesects a mix of Fin and Inf sets. + /// false if an SCC intersects a mix of Fin and Inf sets. /// Call determine_unknown_acceptance() to decide. bool is_accepting() const { @@ -329,7 +329,7 @@ namespace spot /// \brief True if we know that all cycles in the SCC are rejecting /// /// Note that both is_accepting() and is_rejecting() may return - /// false if an SCC interesects a mix of Fin and Inf sets. + /// false if an SCC intersects a mix of Fin and Inf sets. /// Call determine_unknown_acceptance() to decide. bool is_rejecting() const { @@ -509,7 +509,7 @@ namespace spot scc_info(const scc_and_mark_filter& filt, scc_info_options options); // we separate the two functions so that we can rename // scc_info(x,options) into scc_info_with_options(x,options) in Python. - // Otherwrise calling scc_info(aut,options) can be confused with + // Otherwise calling scc_info(aut,options) can be confused with // scc_info(aut,initial_state). scc_info(const scc_and_mark_filter& filt) : scc_info(filt, scc_info_options::ALL) diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index a4eb21af5..c74fae427 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -215,7 +215,7 @@ namespace spot // the test 'c.get_color() != RED' is added to limit // the number of runs reported by successive // calls to the check method. Without this - // functionnality, the test can be ommited. + // functionality, the test can be omitted. trace << " It is cyan or blue and the arc is " << "accepting, start a red dfs" << std::endl; c.set_color(RED); @@ -244,7 +244,7 @@ namespace spot // the test 'c.get_color() != RED' is added to limit // the number of runs reported by successive // calls to the check method. Without this - // functionnality, the test can be ommited. + // functionality, the test can be omitted. trace << " The arc from " << a_->format_state(st_blue.front().s) << " to the current state is accepting, start a " diff --git a/spot/twaalgos/se05.hh b/spot/twaalgos/se05.hh index 640d37f0a..e9df0ed38 100644 --- a/spot/twaalgos/se05.hh +++ b/spot/twaalgos/se05.hh @@ -33,7 +33,7 @@ namespace spot /// \pre The automaton \a a must have at most one acceptance condition (i.e. /// it is a TBA). /// - /// During the visit of \a a, the returned checker stores explicitely all + /// During the visit of \a a, the returned checker stores explicitly all /// the traversed states. /// The method \a check() of the checker can be called several times /// (until it returns a null pointer) to enumerate all the visited accepting @@ -92,11 +92,11 @@ namespace spot /// \pre The automaton \a a must have at most one acceptance condition (i.e. /// it is a TBA). /// - /// During the visit of \a a, the returned checker does not store explicitely + /// During the visit of \a a, the returned checker does not store explicitly /// the traversed states but uses the bit-state hashing technic presented in /// \cite holzmann.91.book /// - /// Consequently, the detection of an acceptence cycle is not ensured. + /// Consequently, the detection of an acceptance cycle is not ensured. /// /// The size of the heap is limited to \n size bytes. /// diff --git a/spot/twaalgos/simulation.hh b/spot/twaalgos/simulation.hh index 07f5d8832..01fc1365d 100644 --- a/spot/twaalgos/simulation.hh +++ b/spot/twaalgos/simulation.hh @@ -51,7 +51,7 @@ namespace spot /// The resulting automaton has a named property "simulated-states", /// that is a vector mapping each state of the input to a state of /// the output. Note that some input states may be mapped to -1, as - /// a by-product of transition prunning. + /// a by-product of transition pruning. /// /// \param automaton the automaton to simulate. /// @@ -153,7 +153,7 @@ namespace spot /// then reduce the automaton. /// /// There is no need to call scc_filter() before as it is always applied to - /// remove dead and unreacheable states. + /// remove dead and unreachable states. /// /// \param aut the automaton to simulate. /// \return a new automaton which is at worst a copy of the received @@ -171,7 +171,7 @@ namespace spot /// way as reduce_direct_sim(). /// /// There is no need to call scc_filter() before as it is always applied to - /// remove dead and unreacheable states. + /// remove dead and unreachable states. /// /// \param aut the automaton to simulate. /// \return a new automaton which is at worst a copy of the received @@ -190,7 +190,7 @@ namespace spot /// transitions). /// /// There is no need to call scc_filter() before as it is always applied to - /// remove dead and unreacheable states. + /// remove dead and unreachable states. /// /// \param aut the automaton to simulate. /// \return a new automaton which is at worst a copy of the received diff --git a/spot/twaalgos/split.hh b/spot/twaalgos/split.hh index 54599c388..9b273096d 100644 --- a/spot/twaalgos/split.hh +++ b/spot/twaalgos/split.hh @@ -234,6 +234,6 @@ namespace spot /// /// Using split_edges() also creates an automaton with separated labels, /// but the separation will be much finer since it will result in a much - /// involves all atomtic proposition. + /// involves all atomic proposition. SPOT_API twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut); } diff --git a/spot/twaalgos/stats.hh b/spot/twaalgos/stats.hh index 63aa3c4e9..f2f72fd06 100644 --- a/spot/twaalgos/stats.hh +++ b/spot/twaalgos/stats.hh @@ -51,7 +51,7 @@ namespace spot /// \brief Compute sub statistics for an automaton. SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g); - /// \brief Count all transtitions, even unreachable ones. + /// \brief Count all transitions, even unreachable ones. SPOT_API unsigned long long count_all_transitions(const const_twa_graph_ptr& g); diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index fef412e09..b2c8648ff 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1418,7 +1418,7 @@ namespace spot auto delta = sw.stop(); bv->trans_time += delta; if (vs) - *vs << "tanslating formula done in " << delta << " seconds\n"; + *vs << "translating formula done in " << delta << " seconds\n"; } res->prop_complete(trival::maybe()); diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index d3d5d3271..5174176e9 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -209,7 +209,7 @@ namespace spot }; /// \ingroup synthesis - /// \brief Seeks to decompose a formula into independently synthesizable + /// \brief Seeks to decompose a formula into independently synthetizable /// sub-parts. The conjunction of all sub-parts then /// satisfies the specification /// diff --git a/spot/twaalgos/tau03.hh b/spot/twaalgos/tau03.hh index a4c7ad1e6..6e9f31267 100644 --- a/spot/twaalgos/tau03.hh +++ b/spot/twaalgos/tau03.hh @@ -31,7 +31,7 @@ namespace spot /// /// \pre The automaton \a a must have at least one acceptance condition. /// - /// During the visit of \a a, the returned checker stores explicitely all + /// During the visit of \a a, the returned checker stores explicitly all /// the traversed states. The implemented algorithm is the following: /// /** \verbatim diff --git a/spot/twaalgos/tau03opt.hh b/spot/twaalgos/tau03opt.hh index 2d6f529b2..6e910ab57 100644 --- a/spot/twaalgos/tau03opt.hh +++ b/spot/twaalgos/tau03opt.hh @@ -31,7 +31,7 @@ namespace spot /// /// \pre The automaton \a a must have at least one acceptance condition. /// - /// During the visit of \a a, the returned checker stores explicitely all + /// During the visit of \a a, the returned checker stores explicitly all /// the traversed states. The implemented algorithm is the following: /// /** \verbatim @@ -84,7 +84,7 @@ namespace spot end; \endverbatim */ /// - /// This algorithm is a generalisation to TGBA of the one implemented in + /// This algorithm is a generalization to TGBA of the one implemented in /// spot::explicit_se05_search. It is based on the acceptance set labelling /// of states used in spot::explicit_tau03_search. Moreover, it introduce /// a slight optimisation based on vectors of integers counting for each diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index 5283b637a..648fd29e5 100644 --- a/spot/twaalgos/toparity.hh +++ b/spot/twaalgos/toparity.hh @@ -135,7 +135,7 @@ namespace spot /// This procedure combines many strategies in an attempt to produce /// the smallest possible parity automaton. Some of the strategies /// include CAR (color acceptance record), IAR (index appearance - /// record), partial degenerazation, conversion from Rabin to Büchi + /// record), partial degeneralization, conversion from Rabin to Büchi /// when possible, etc. /// /// The \a options argument can be used to selectively disable some of the @@ -152,7 +152,7 @@ namespace spot /// /// This implements a straightforward adaptation of the LAR (latest /// appearance record) to automata with transition-based marks. We - /// call this adaptation the CAR (color apperance record), as it + /// call this adaptation the CAR (color appearance record), as it /// tracks colors (i.e., acceptance sets) instead of states. /// /// It is better to use to_parity() instead, as it will use better @@ -186,7 +186,7 @@ namespace spot /// \ingroup twa_acc_transform /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton - /// based on the index appearence record (IAR) + /// based on the index appearance record (IAR) /// /// Returns nullptr if the input automaton is neither Rabin-like nor /// Streett-like, and calls spot::iar() otherwise. diff --git a/spot/twaalgos/totgba.hh b/spot/twaalgos/totgba.hh index 51af4d9f6..b437cab8e 100644 --- a/spot/twaalgos/totgba.hh +++ b/spot/twaalgos/totgba.hh @@ -71,7 +71,7 @@ namespace spot /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Streett automaton. /// - /// This works by putting the acceptance condition in cunjunctive + /// This works by putting the acceptance condition in conjunctive /// normal form, and then merging all the /// Inf(x1)|Inf(x2)|...|Inf(xn) that may occur in clauses into a /// single Inf(X). diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index d1dbe5e27..cc5d4f9af 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -36,7 +36,7 @@ namespace spot /// automaton produced (TGBA, BA, Monitor). The default is TGBA. /// /// Method set_pref() may be used to specify whether small automata - /// should be prefered over deterministic automata. + /// should be preferred over deterministic automata. /// /// Method set_level() may be used to specify the optimization level. /// diff --git a/spot/twaalgos/word.cc b/spot/twaalgos/word.cc index bc9f5a52b..7ac3fa598 100644 --- a/spot/twaalgos/word.cc +++ b/spot/twaalgos/word.cc @@ -206,7 +206,7 @@ namespace spot if (word[ind] == '}') word_parse_error(word, ind, "Expected ';' delimiter: " "'}' stands for ending a cycle"); - // Exract formula, convert it to bdd and add it to the prefix sequence + // Extract formula, convert it to bdd and add it to the prefix sequence extract_bdd(tw->prefix); if (i == std::string::npos) word_parse_error(word, ind + 1, "Missing cycle in formula"); diff --git a/spot/twaalgos/word.hh b/spot/twaalgos/word.hh index 171b14ce3..3b5753fb4 100644 --- a/spot/twaalgos/word.hh +++ b/spot/twaalgos/word.hh @@ -39,7 +39,7 @@ namespace spot dict_->unregister_all_my_variables(this); } - /// \brief Simplify a lasso-shapped word. + /// \brief Simplify a lasso-shaped word. /// /// The simplified twa_word may represent a subset of the actual /// words represented by the original twa_word. The typical @@ -79,7 +79,7 @@ namespace spot /// \brief Convert the twa_word as an automaton. /// - /// Convert the twa_word into a lasso-shapred automaton + /// Convert the twa_word into a lasso-shaped automaton /// with "true" acceptance condition. /// /// This is useful to evaluate a word on an automaton. diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 521d9630a..2d8ada12f 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -816,7 +816,7 @@ namespace spot throw std::runtime_error("acd::first_branch(): unknown state " + std::to_string(s)); unsigned scc = si_->scc_of(s); - if (trees_[scc].trivial) // the branch is irrelevant for transiant SCCs + if (trees_[scc].trivial) // the branch is irrelevant for transient SCCs return 0; if (SPOT_UNLIKELY(nodes_.empty())) // make sure we do not complain about this if all SCCs are trivial. diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index e0ec2c3e3..a07dbe65d 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -480,13 +480,13 @@ namespace spot /// /// If \a colored is set, each output transition will have exactly /// one color, and the output automaton will use at most n+1 colors - /// if the input has n colors. If \a colored is unsed (the default), + /// if the input has n colors. If \a colored is unset (the default), /// output transitions will use at most one color, and output /// automaton will use at most n colors. /// - /// The acd_tranform() is the original function producing + /// The acd_transform() is the original function producing /// optimal transition-based output (optimal in the sense of least - /// number of duplicated states), while the acd_tansform_sbacc() variant + /// number of duplicated states), while the acd_transform_sbacc() variant /// produces state-based output from transition-based input and without /// any optimality claim. The \a order_heuristics argument, enabled /// by default activates the ORDER_HEURISTICS option of the ACD. diff --git a/spot/twacube/cube.hh b/spot/twacube/cube.hh index fc46249f0..45edc64b0 100644 --- a/spot/twacube/cube.hh +++ b/spot/twacube/cube.hh @@ -41,18 +41,18 @@ namespace spot /// Warning : a variable cannot be set in both bitset at the /// same time (consistency! cannot be true and false) /// - /// The cube for (a & !b) will be repensented by : + /// The cube for (a & !b) will be represented by: /// - true_var = 1 0 /// - false_var = 0 1 /// /// To represent free variables such as in (a & !b) | (a & b) - /// (wich is equivalent to (a) with b free) + /// (which is equivalent to (a) with b free) /// - true_var : 1 0 /// - false_var : 0 0 - /// This exemple shows that the representation of free variables + /// This example shows that the representation of free variables /// is done by unsetting variable in both vector /// - /// To be memory efficient, these two bitsets are contigous in memory + /// To be memory efficient, these two bitsets are contigious in memory /// i.e. if we want to represent 35 variables, a cube will be /// represented by 4 unsigned int contiguous in memory. The 35 /// first bits represent truth values. The 29 bits following are diff --git a/spot/twacube/twacube.hh b/spot/twacube/twacube.hh index 37ab9abcf..745df56a9 100644 --- a/spot/twacube/twacube.hh +++ b/spot/twacube/twacube.hh @@ -93,7 +93,7 @@ namespace spot } /// \brief Returns the current transition according to a specific - /// \a seed. The \a seed is traditionnally the thread identifier. + /// \a seed. The \a seed is traditionally the thread identifier. inline unsigned current(unsigned seed = 0) const { // no-swarming : since twacube are dedicated for parallelism, i.e. @@ -204,7 +204,7 @@ namespace spot const twacube& twa); private: unsigned init_; ///< The Id of the initial state - acc_cond acc_; ///< The acceptance contidion + acc_cond acc_; ///< The acceptance condition const std::vector aps_; ///< The name of atomic propositions graph_t theg_; ///< The underlying graph cubeset cubeset_; ///< Ease the cube manipulation diff --git a/tests/core/cube.cc b/tests/core/cube.cc index bcd5e8c4c..936c6acae 100644 --- a/tests/core/cube.cc +++ b/tests/core/cube.cc @@ -35,7 +35,7 @@ static bool test_translation(bdd& input, spot::cubeset& cubeset, std::unordered_map& reverse_binder, std::vector& aps) { - // The BDD used to detect if the convertion works + // The BDD used to detect if the conversion works bdd res = bddfalse; bdd initial = input; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index cbc49b1c9..1e0397a5f 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -206,7 +206,7 @@ diff outx exp cat >exp < GFb -tanslating formula done in X seconds +translating formula done in X seconds direct strategy was found. direct strat has 1 states, 2 edges and 0 colors simplification took X seconds @@ -642,7 +642,7 @@ the following signals can be temporarily removed: new formula: GFa <-> GFb there are 1 subformulas trying to create strategy directly for GFa <-> GFb -tanslating formula done in X seconds +translating formula done in X seconds direct strategy was found. direct strat has 1 states, 2 edges and 0 colors simplification took X seconds @@ -658,7 +658,7 @@ for f in "(GFa <-> GFb) & G(c <-> d)" "(GFb <-> GFa) & G(c <-> d)" \ do cat >exp <exp < GFa) & G((a & c) | (!a & !c)) -tanslating formula done in X seconds +translating formula done in X seconds direct strategy was found. direct strat has 1 states, 2 edges and 0 colors simplification took X seconds @@ -701,7 +701,7 @@ diff outx exp cat >exp < FGb -tanslating formula done in X seconds +translating formula done in X seconds direct strategy was found. direct strat has 2 states, 3 edges and 0 colors simplification took X seconds @@ -1043,7 +1043,7 @@ the following signals can be temporarily removed: new formula: GFi <-> GFo1 there are 1 subformulas trying to create strategy directly for GFi <-> GFo1 -tanslating formula done in X seconds +translating formula done in X seconds direct strategy was found. direct strat has 1 states, 2 edges and 0 colors simplification took X seconds diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 2e3949ae9..e7dda99df 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -236,7 +236,7 @@ static bool is_right_parity(spot::const_twa_graph_ptr aut, target_odd = origin_odd; if (!(is_max == target_max && is_odd == target_odd)) { - std::cerr << "======Wrong accceptance======\n"; + std::cerr << "======Wrong acceptance======\n"; std::string kind[] = { "max", "min", "same", "any" }; std::string style[] = { "odd", "even", "same", "any" }; std::cerr << "target: " << kind[target_kind] << ' ' diff --git a/tests/core/safra.cc b/tests/core/safra.cc index d01613d02..b238df92a 100644 --- a/tests/core/safra.cc +++ b/tests/core/safra.cc @@ -44,7 +44,7 @@ static void help() "\t-b\treduce result using bisimulation\n" "\t--scc_opt\tUse an SCC-based Safra\n" "\t--bisim_opt\tUse Simulation info to reduce macro-states size\n" - "\t--stutter\tStutter-invarience optimisation\n"; + "\t--stutter\tStutter-invariance optimisation\n"; exit(1); } diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index 7e33d6748..378d366c2 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -218,7 +218,7 @@ static void f6() // when faced with a more involved problem static void f7() { - // The current mege_states implementation of "next" + // The current merge_states implementation of "next" // needs two successive calls to obtain an automaton with only 3 states // This is especially annoying as this depends on the numbering. // By renumbering 2->1 3->2 1->3 the current version only needs one call too