From eb91ecf66f5f03242728c7dab9574282e73b9898 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Fri, 18 Aug 2017 09:35:40 +0200 Subject: [PATCH] Typos * NEWS, doc/org/concepts.org, doc/org/hierarchy.org, spot/misc/optionmap.hh, spot/twa/acc.hh, spot/twaalgos/ltl2tgba_fm.hh, spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.cc: fix typos --- NEWS | 10 +++++----- doc/org/concepts.org | 2 +- doc/org/hierarchy.org | 34 +++++++++++++++++----------------- spot/misc/optionmap.hh | 6 +++--- spot/twa/acc.hh | 8 ++++---- spot/twaalgos/ltl2tgba_fm.hh | 6 +++--- spot/twaalgos/sccinfo.hh | 2 +- spot/twaalgos/translate.cc | 2 +- 8 files changed, 35 insertions(+), 35 deletions(-) diff --git a/NEWS b/NEWS index 9529a3dfe..0a403b473 100644 --- a/NEWS +++ b/NEWS @@ -22,8 +22,8 @@ New in spot 2.3.5.dev (not yet released) LTL translators). - autfilt learned to build the union (--sum) or the intersection - (--sum-and) of two language by putting two automata side-by-side - and fiddling with the initial states. This complement the already + (--sum-and) of two languages by putting two automata side-by-side + and fiddling with the initial states. This complements the already implemented intersection (--product) and union (--product-or), both based on a product. @@ -57,7 +57,7 @@ New in spot 2.3.5.dev (not yet released) - twa objects have a new property: prop_complete(). This obviously acts as a cache for the is_complete() function. - - spot::dualize() completements any alternating automaton. Since + - spot::dualize() complements any alternating automaton. Since the dual of a deterministic automaton is still deterministic, the function spot::dtwa_complement() has been deprecated and simply calls spot::dualize(). @@ -198,7 +198,7 @@ New in spot 2.3.5.dev (not yet released) been adjusted to these new semantics, see "Backward-incompatible changes" below. - - The parser for HOA now recognize and verifies correct use of the + - The parser for HOA now recognizes and verifies correct use of the "univ-branch" property. This is known to be a problem with option -H1 of ltl3ba 1.1.2 and ltl3dra 0.2.4, so the environment variable SPOT_HOA_TOLERANT can be set to disable the diagnostic. @@ -212,7 +212,7 @@ New in spot 2.3.5.dev (not yet released) - When the remove_fin() function was called on some automaton with Inf-less acceptance involving at least one disjunction (e.g., - generalized co-Büchi), it would sometime output an automaton with + generalized co-Büchi), it would sometimes output an automaton with transition-based acceptance but marked as state-based. Backward-incompatible changes: diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 46925c18f..22933274d 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -771,7 +771,7 @@ Both extensions are supported by Spot. :END: The DSTAR format is the native format of [[http://ltl2dstar.de/][=ltl2dstar=]]. It allows -representing Deterministic STreett And Rabin automata, hence the +representing Deterministic Streett And Rabin automata, hence the name. Spot can read the DSTAR format, but it does not output it. Adding diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index 109e02b08..5d942eef8 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -31,7 +31,7 @@ this picture for a moment. recognized by a deterministic Büchi automaton. - The dual class, /persistence/ properties, are those that can be - reresented by a weak Büchi automaton (i.e., in each SCC either all + recognized by a weak Büchi automaton (i.e., in each SCC either all states are accepting, or all states are rejecting). - The intersection of /recurrence/ and /persistence/ classes form the @@ -43,15 +43,15 @@ this picture for a moment. reaching an accepting state, any suffix will be accepted). - /Safety/ properties are the dual of /Guarantee/ properties: they can - be recognized by an ω-automata that accept all their runs (i.e., the + be recognized by ω-automata that accept all their runs (i.e., the acceptance condition is "true"). Note that since these automata are - not necessary complete, it is still possible for some words to not + not necessary complete, it is still possible for some words not to be accepted. If we interpret the ω-automata with "true" acceptance as finite automata with all states marked as final, we obtain monitors, i.e., finite automata that recognize all finite prefixes that can be extended into valid ω-words. -- Finally, at the very bottom is an unnamed class that is contains +- Finally, at the very bottom is an unnamed class that contains /Safety/ properties that are also /Guarantee/ properties: those are properties that can be represented by monitors in which the only cycles are self-loops labeled by true. @@ -124,9 +124,9 @@ genltl --dac-patterns --format='%[v]h' | sort | uniq -c : 12 recurrence : 37 safety -In this output, the most precise class is given for each formula, an +In this output, the most precise class is given for each formula, and the count of formulas for each subclass is given. We have to remember -that the recurrence class also include obligation, safety, and +that the recurrence class also includes obligation, safety, and guarantee properties. In this list, there are no formulas that belong to the intersection of the /guarantee/ and /safety/ classes (it would have been listed as =guarantee safety=). @@ -150,7 +150,7 @@ genltl --dac-patterns | : reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5)))))) Similar filtering options exist for other classes. Since these tests -are automata-based, they work with PSL formulas as weil. For instance, +are automata-based, they work with PSL formulas as well. For instance, here is how to generate 10 random recurrence PSL formulas that are not LTL formulas, and that are not obligations: @@ -226,7 +226,7 @@ is in class syntactic-C). =ltlfilt= has options like =--syntactic-guarantee=, =--syntactic-persistence=, etc. to match formulas from this classes. -Here is how to generate 10 random LTL formula that describe safety +Here is how to generate 10 random LTL formulas that describe safety properties but that are not in the syntactic-safety class: #+BEGIN_SRC sh :results verbatim :exports both @@ -250,7 +250,7 @@ b M Gb #+end_example Since all those formulas describe safety properties, an exercise would -be suggest equivalent formulas that are in the syntactic-safety +be to suggest equivalent formulas that are in the syntactic-safety fragment. For instance =b M Gb= can be rewritten as just =Gb=, which belongs to this fragment. In this particular case, =ltlfilt --simplify= recognizes this: @@ -274,14 +274,14 @@ the powerset constructions for restricted classes of ω-automata/, ATVA'07]]) in order to detect obligation properties, and produce minimal weak deterministic automata for them. -When running =ltl2tgba -D= on an formula that represents and +When running =ltl2tgba -D= on a formula that represents an obligation property, you are guaranteed to obtain a minimal (in the number of states) deterministic weak Büchi automaton that recognizes it. Note that since the /obligation/ class includes the /safety/ and /guarantee/ classes, minimal deterministic automata will also be -produced for those classes. Dax et al.'s determinization of obligations +produced for those classes. Dax et al.'s determinization of obligation properties combined with Löding's minimization renders obsolete -older algorithms (and tools) that produced minimial deterministic +older algorithms (and tools) that produced minimal deterministic automata but only for the subclasses of /safety/ or /guarantee/. If =ltl2tgba= is run without =-D= (but still with the default =--high= @@ -440,7 +440,7 @@ However, the /safety/ class corresponds to what can be represented faithfully by monitors, i.e., automata that accept all their infinite runs. -For most safety formula, the acceptance output by =ltl2tgba= will +For most safety formulas, the acceptance output by =ltl2tgba= will already be =t= (meaning that all runs are accepting). However since the translator does not do anything particular about safety formulas, it is possible to find some pathological formulas for which the @@ -490,7 +490,7 @@ If you are working with safety formula, and know you want to work with monitors, you can use the =-M= option of =ltl2tgba=. In this case this will output the same automaton, but using the universal acceptance (i.e. =t=). You can interpret this output as a monitor -(i.e., a finite automaton that accept all prefixes that can be +(i.e., a finite automaton that accepts all prefixes that can be extended into valid ω-words). #+NAME: hier-safety-1m @@ -571,7 +571,7 @@ $txt [[file:hier-recurrence-2.png]] -Here is an example of formula for which =ltl2tgba= does not produce a +Here is an example of a formula for which =ltl2tgba= does not produce a deterministic automaton, even with =-D=. #+BEGIN_SRC sh :results verbatim :exports both @@ -630,8 +630,8 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot: (The only change here is in the acceptance condition.) 3. In step 4 we are going to convert the automaton to state-based - Büchi, and this sometimes work better if the input Rabin automaton - also use state-based acceptance. So let us add =-S= to the + Büchi, and this sometimes works better if the input Rabin automaton + also uses state-based acceptance. So let us add =-S= to the previous command: #+NAME: hier-recurrence-6 diff --git a/spot/misc/optionmap.hh b/spot/misc/optionmap.hh index 18a220515..ea06c62f9 100644 --- a/spot/misc/optionmap.hh +++ b/spot/misc/optionmap.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013, 2015, 2016-2017 Laboratoire de Recherche et // Developpement de l'Epita (LRDE) // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -40,7 +40,7 @@ namespace spot /// \brief Add the parsed options to the map. /// /// \a options are separated by a space, comma, semicolon or tabulation and - /// can be optionnaly followed by an integer value (preceded by an equal + /// can be optionally followed by an integer value (preceded by an equal /// sign). If not specified, the default value is 1. /// /// The following three lines are equivalent. @@ -87,7 +87,7 @@ namespace spot std::string set_str(const char* option, std::string val, std::string def = {}); - /// \brief Raise a runtime_error if some option haven't been used. + /// \brief Raise a runtime_error if some options have not been used. void report_unused_options() const; /// Acquire all the settings of \a o. diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 0b14c4112..7aaf07c0d 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1081,7 +1081,7 @@ namespace spot /// /// An acceptance condition is Streett-like if it can be transformed into /// a Streett acceptance with little modification to its automaton. - /// A Streett-like acceptance condition follow one of those rules: + /// A Streett-like acceptance condition follows one of those rules: /// -It is a conjunction of disjunctive clauses containing at most one /// Inf and at most one Fin. /// -It is true (with 0 pair) @@ -1093,7 +1093,7 @@ namespace spot /// /// An acceptance condition is Rabin-like if it can be transformed into /// a Rabin acceptance with little modification to its automaton. - /// A Rabin-like acceptance condition follow one of those rules: + /// A Rabin-like acceptance condition follows one of those rules: /// -It is a disjunction of conjunctive clauses containing at most one /// Inf and at most one Fin. /// -It is true (1 pair [0U, 0U]) @@ -1112,8 +1112,8 @@ namespace spot bool is_parity() const { bool max; - bool min; - return is_parity(max, min); + bool odd; + return is_parity(max, odd); } // Return (true, m) if there exist some acceptance mark m that diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index f66d61c16..6a1d2be2a 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -58,7 +58,7 @@ namespace spot /// \param exprop When set, the algorithm will consider all properties /// combinations possible on each state, in an attempt to reduce /// the non-determinism. The automaton will have the same size as - /// without this option, but because the transition will be more + /// without this option, but because the transitions will be more /// deterministic, the product automaton will be smaller (or, at worse, /// equal). /// @@ -68,7 +68,7 @@ namespace spot /// /// \param branching_postponement When set, several transitions leaving /// from the same state with the same label (i.e., condition + acceptance - /// conditions) will be merged. This correspond to an optimization + /// conditions) will be merged. This corresponds to an optimization /// described in the following paper. /** \verbatim @InProceedings{ sebastiani.03.charme, diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 2ce129377..0b2d18e37 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -441,7 +441,7 @@ namespace spot /// states of an SCC. /// /// The difference with edges_of() is that inner_edges_of() - /// ignores edges leaving the SCC are ignored. In the case of + /// ignores edges leaving the SCC. In the case of an /// alternating automaton, an edge is considered to be part of the /// SCC of one of its destination is in the SCC. internal::scc_edges diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 10f1947fa..d5be53d4d 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -85,7 +85,7 @@ namespace spot // // This rewriting is enabled only if the formula // 1) has some Boolean subformula - // 2) has more than relabel_bool_ atomic propisition (the default + // 2) has more than relabel_bool_ atomic propositions (the default // is 4, but this can be changed) // 3) relabel_bse() actually reduces the number of atomic // propositions.