diff --git a/HACKING b/HACKING index ec7cacf85..9dae74a74 100644 --- a/HACKING +++ b/HACKING @@ -609,7 +609,7 @@ SPOT macros that a compiler might not see as unreachable. * Use SPOT_API in front of functions and class that should be - exported by the shared library. See "Exporting symbolss" above. + exported by the shared library. See "Exporting symbols" above. * Use SPOT_ASSERT(...) if you ever have to put an assertion in some header file. See "Assertions" above. diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 1831e66ab..dbaad34ce 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -206,7 +206,7 @@ Let $\N=\{0,1,2,\ldots\}$ denote the set of natural numbers and $\omega\not\in\N$ the first transfinite ordinal. We extend the $<$ -relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in N,\, +relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in \N,\, n<\omega$. Similarly let us extend the addition and subtraction with $\forall n\in\N,\,\omega+n = \omega-n = \omega+\omega = \omega$. @@ -1323,8 +1323,8 @@ rewriting arrange any PSL formula into negative normal form. \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)& \NOT(\sere{r} \Esuffix f) &\equiv \sere{r} \Asuffix \NOT f \end{align*} -\noindent Recall the that negated weak closure $\nsere{r}$ is actually -implemented as a specific operator, so it not actually prefixed by the +\noindent Recall that the negated weak closure $\nsere{r}$ is actually +implemented as a specific operator, so it is not actually prefixed by the $\NOT$ operator. \begin{align*} f \XOR g & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) & diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 4b299ba58..28c04216e 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -72,7 +72,7 @@ namespace spot G, ///< Globally Closure, ///< PSL Closure NegClosure, ///< Negated PSL Closure - NegClosureMarked, ///< marked version of the Negated PSL Clusure + NegClosureMarked, ///< marked version of the Negated PSL Closure // binary operators Xor, ///< Exclusive Or Implies, ///< Implication