Skip to content
Snippets Groups Projects
Commit 7b56e49f authored by Michael Jastram's avatar Michael Jastram
Browse files

Various fixes (hyphenation, etc.)

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@16259 1434b563-b632-4741-aa49-43a3a8374d2e
parent 01220c25
No related branches found
No related tags found
No related merge requests found
...@@ -8,6 +8,6 @@ it under the Creative Commons Share-Alike License. ...@@ -8,6 +8,6 @@ it under the Creative Commons Share-Alike License.
This work, except the cover image, is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License. To view a copy of this license, visit \href{http://creativecommons.org/licenses/by-sa/3.0/}{creative\-com\-mons.org/\-licenses/\-by-sa/3.0/} or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA. This work, except the cover image, is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License. To view a copy of this license, visit \href{http://creativecommons.org/licenses/by-sa/3.0/}{creative\-com\-mons.org/\-licenses/\-by-sa/3.0/} or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA.
The cover image of a Rodin statue was created by Miikka Skaffari (\href{http://www.skaffari.fi/}{www.skaffari.fi}). It is licensed under a Creative Commons Attribution-NonCommercial 3.0 Unported License. To view a copy of this license, visit \href{http://creativecommons.org/licenses/by-sa/3.0/}{creative\-com\-mons.org/\-licenses/\-by-sa/3.0/} or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA. The cover image of a Rodin statue was created by Miikka Skaffari (\href{http://www.skaffari.fi/}{www.skaf\-fari.fi}). It is licensed under a Creative Commons Attribution-NonCommercial 3.0 Unported License. To view a copy of this license, visit \href{http://creativecommons.org/licenses/by-sa/3.0/}{creative\-com\-mons.org/\-licenses/\-by-sa/3.0/} or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA.
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
In addition to this handbook, consider looking in the Rodin Wiki (\ref{rodin_wiki}) for an answer. In addition to this handbook, consider looking in the Rodin Wiki (\ref{rodin_wiki}) for an answer.
There is also a vibrant community that is helpful and responsive. You can contact it via the Rodin user mailing list at \href{mailto:rodin-b-sharp-user@lists.sourceforge.net}{rodin-b-sharp-user@lists.sourceforge.net}. There is also a vibrant community that is helpful and responsive. You can contact it via the Rodin user mailing list at \href{mailto:rodin-b-sharp-user@lists.sourceforge.net}{rodin-b-sharp-user@lists.source\-forge\-.net}.
\subsection{What is Event-B?} \subsection{What is Event-B?}
\index{Event-B} \index{Event-B}
......
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
% for the print, we use an extra b&w directory % for the print, we use an extra b&w directory
\ifinprint \ifinprint
\newcommand{\rodinimgdir}{img} \newcommand{\rodinimgdir}{img-print}
\else \else
\newcommand{\rodinimgdir}{img} \newcommand{\rodinimgdir}{img}
\fi \fi
...@@ -64,15 +64,9 @@ ...@@ -64,15 +64,9 @@
\setlength{\titlesecdistance}{10mm} \setlength{\titlesecdistance}{10mm}
\fi \fi
\ifinprint \def\tick#1{\doculist{#1}{img/tick_64.png}}
\def\tick#1{\doculist{#1}{img/bw/tick_64.png}} \def\info#1{\doculist{#1}{img/info_64.png}}
\def\info#1{\doculist{#1}{img/bw/info_64.png}}
\def\warning#1{\doculist{#1}{img/bw/warning.pdf}}
\else
\def\tick#1{\doculist{#1}{\rodinimgdir/tick_64.png}}
\def\info#1{\doculist{#1}{\rodinimgdir/info_64.png}}
\def\warning#1{\doculist{#1}{\rodinimgdir/warning_64.png}} \def\warning#1{\doculist{#1}{\rodinimgdir/warning_64.png}}
\fi
\def\pencil#1{\doculist{#1}{\rodinimgdir/pencil_64.png}} \def\pencil#1{\doculist{#1}{\rodinimgdir/pencil_64.png}}
% macro for icons % macro for icons
......
...@@ -588,7 +588,7 @@ For an axiom $A_w$, $A_b$ denotes (the conjunction of) all axioms declared ...@@ -588,7 +588,7 @@ For an axiom $A_w$, $A_b$ denotes (the conjunction of) all axioms declared
\label{well_definedness_of_invariants} \label{well_definedness_of_invariants}
For an invariant $J_w$, $J_b$ denotes (the conjunction of) all the model's For an invariant $J_w$, $J_b$ denotes (the conjunction of) all the model's
invariants declared before the theorem. invariants declared before the theorem.
\index{proof obligation!well-definedness of an invariant@well-definedness of an invariant (\eventbpo{WD})} \index{proof obligation!well-definedness of an invariant@well-def. of an invariant (\eventbpo{WD})}
\pode{Well-definedness of an invariant}{\eventbpo{label/WD}}% \pode{Well-definedness of an invariant}{\eventbpo{label/WD}}%
{$A \land I \land J_b {$A \land I \land J_b
\limp \wdl(J_w)$} \limp \wdl(J_w)$}
......
...@@ -270,7 +270,7 @@ Let's get started. We first provide the new variable, gluing invariant, typing ...@@ -270,7 +270,7 @@ Let's get started. We first provide the new variable, gluing invariant, typing
We also have to modify the guard on \textsf{set\_peds\_green}, which is something that you should now be able to figure out yourself (just replace \textsf{cars\_go = FALSE} with \textsf{green} $\notin$ \textsf{cars\_colours}). We also have to modify the guard on \textsf{set\_peds\_green}, which is something that you should now be able to figure out yourself (just replace \textsf{cars\_go = FALSE} with \textsf{green} $\notin$ \textsf{cars\_colours}).
The interesting piece is the last event, \textsf{set\_cars}, which we rename as \textsf{set\_cars\_colours}. We change the parameter to \textsf{new\_value\_colours} and type it as a subset of \textsf{COLOURS}. The interesting piece is the last event, \textsf{set\_cars}, which we rename as \textsf{set\_cars\-\_colours}. We change the parameter to \textsf{new\_value\_colours} and type it as a subset of \textsf{COLOURS}.
The witness appears in the \textsf{with} section of the event. The label \textbf{must} be \textsf{new\_value}. The value itself must describe the relationship between the abstract parameter \textsf{new\_value} and the new parameter \textsf{new\_value\_colours}. As we use the parameter as the new value for the variable \textsf{cars\_colours}, the witness is an adaptation of the gluing invariant (we just replace \textsf{cars\_colours} with \textsf{new\_value\_colours}). The witness appears in the \textsf{with} section of the event. The label \textbf{must} be \textsf{new\_value}. The value itself must describe the relationship between the abstract parameter \textsf{new\_value} and the new parameter \textsf{new\_value\_colours}. As we use the parameter as the new value for the variable \textsf{cars\_colours}, the witness is an adaptation of the gluing invariant (we just replace \textsf{cars\_colours} with \textsf{new\_value\_colours}).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment