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

Typos

Browse source 
* 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
This commit is contained in:
Maximilien Colange 2017-08-18 09:35:40 +02:00
parent f5dce597c6
commit eb91ecf66f
8 changed files with 35 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

10
NEWS
View file

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

2
doc/org/concepts.org
View file

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

34
doc/org/hierarchy.org
View file

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

6
spot/misc/optionmap.hh
View file

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

8
spot/twa/acc.hh
View file

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

6
spot/twaalgos/ltl2tgba_fm.hh
View file

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

2
spot/twaalgos/sccinfo.hh
View file

@ -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<const twa_graph::graph_t, internal::keep_inner_scc>

2
spot/twaalgos/translate.cc
View file

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