diff --git a/org.rodinp.handbook.feature/latex/faq.tex b/org.rodinp.handbook.feature/latex/faq.tex index 1aa884a65b54506e807a505d81017c1efa312855..250e80dc1bd74f19875bf97b023e0d787a3a24a4 100644 --- a/org.rodinp.handbook.feature/latex/faq.tex +++ b/org.rodinp.handbook.feature/latex/faq.tex @@ -106,7 +106,8 @@ Configuring Rodin on Linux can be tricky. In particular, the pretty print view Add a property by appending the following code to your \textsf{eclipse/eclipse.ini} or \textsf{rodin/rodin.ini} file: \begin{verbatim} - -Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner/xulrunner-xxx + -Dorg.eclipse.swt.browser.XULRunnerPath= + /usr/lib/xulrunner/xulrunner-xxx \end{verbatim} \subsection{Some mathematical characters are wrong} diff --git a/org.rodinp.handbook.feature/latex/img/bw/pencil_64.png b/org.rodinp.handbook.feature/latex/img/bw/pencil_64.png new file mode 100644 index 0000000000000000000000000000000000000000..1398532e9ecca3829d13d8891b4e9ad8e450fb29 Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/bw/pencil_64.png differ diff --git a/org.rodinp.handbook.feature/latex/img/bw/pror.png b/org.rodinp.handbook.feature/latex/img/bw/pror.png index 383b5ef605959e8bb6b1ee2523364fd434917c1c..127e4ef0d89f801d3369cd9444860d2960eaac10 100644 Binary files a/org.rodinp.handbook.feature/latex/img/bw/pror.png and b/org.rodinp.handbook.feature/latex/img/bw/pror.png differ diff --git a/org.rodinp.handbook.feature/latex/img/tutorial/tl-colors.png b/org.rodinp.handbook.feature/latex/img/tutorial/tl-colors.png index 6b53650347a7c5475edfb7ee7493c83687f28fac..df59b3a8c26e0ceccf9e586a6a9c2f5dc4ed4a1a 100644 Binary files a/org.rodinp.handbook.feature/latex/img/tutorial/tl-colors.png and b/org.rodinp.handbook.feature/latex/img/tutorial/tl-colors.png differ diff --git a/org.rodinp.handbook.feature/latex/makros.tex b/org.rodinp.handbook.feature/latex/makros.tex index 87779ae5a60000927bd3e9918641f28f1f523973..6bb4fe1fb9b5d9cabf3699f6a0d29ad1dd2a4e06 100644 --- a/org.rodinp.handbook.feature/latex/makros.tex +++ b/org.rodinp.handbook.feature/latex/makros.tex @@ -12,7 +12,7 @@ % for the print, we use an extra b&w directory \ifinprint -\newcommand{\rodinimgdir}{bwimg} +\newcommand{\rodinimgdir}{img} \else \newcommand{\rodinimgdir}{img} \fi @@ -180,11 +180,7 @@ } \fi -\ifinprint -\newenvironment{plugin-pror}{\begin{rodin-plugin}{bw/pror.png}{ProR Requirements}}{\end{rodin-plugin}} -\else \newenvironment{plugin-pror}{\begin{rodin-plugin}{pror.png}{ProR Requirements}}{\end{rodin-plugin}} -\fi % Marginpars are cropped - this formats them nicely. \let\oldmarginpar\marginpar diff --git a/org.rodinp.handbook.feature/latex/reference-01.tex b/org.rodinp.handbook.feature/latex/reference-01.tex index 25030855d16115ec9dc94f134d21e1acc1643488..b2de1262d3ad64bcc97d9e291259f867036330dd 100644 --- a/org.rodinp.handbook.feature/latex/reference-01.tex +++ b/org.rodinp.handbook.feature/latex/reference-01.tex @@ -829,7 +829,7 @@ The auto-tactic automatically applies a combination (i.e. ordered list) of rewri The post-tactic is also a combination of rewrite tactics, inference tactics and external provers and is applied automatically after each interactive proof step. However, it can also be invoked manually by clicking on the \icon{rodin/broom_prover.png} button in the \textsf{Proof Control} view. -Note that the post-tactic can be disabled quickly by clicking on the \textsf{rodin/expanded.png} button (marked with an A) of the \textsf{Proof Control} view (right upper corner) and then by deselecting the box next to the \textsf{Enable post-tactic} option (B) as shown in Figure \ref{fig_ref_01_proving_perspective12}. +Note that the post-tactic can be disabled quickly by clicking on the \icon{rodin/expanded.png} button (marked with an A) of the \textsf{Proof Control} view (right upper corner) and then by deselecting the box next to the \textsf{Enable post-tactic} option (B) as shown in Figure \ref{fig_ref_01_proving_perspective12}. \begin{figure}[!ht] \begin{center} diff --git a/org.rodinp.handbook.feature/latex/reference-02.tex b/org.rodinp.handbook.feature/latex/reference-02.tex index 6ab397f9eca9d6faf2e5ae16b2a53115cb4a88c0..0d110b94051281b39aaed1bf3eb8505b2f767bec 100644 --- a/org.rodinp.handbook.feature/latex/reference-02.tex +++ b/org.rodinp.handbook.feature/latex/reference-02.tex @@ -283,7 +283,8 @@ All variables to which no new value is assigned keep the same value in new and o \index{before-after predicate} We now define the before-after-predicate $\concbeforeafter$ of the actions together. Let $Q_1,\ldots,Q_n$ be the before-after-predicate of the event's assignments. -Let $x_1,\ldots,x_k$ be the variables that are assigned by any action of the event. +Let $x_1,\ldots,$ $x_k$ % broke formular for print +be the variables that are assigned by any action of the event. Let $y_1,\ldots,y_l$ be the variables of the concrete machine that are \emph{not} modified by any of the event's actions (i.e. $\concvariables = x_1,\ldots,x_k,y_1,\ldots,y_l$). Then the before-after-predicate of the concrete event is @@ -675,7 +676,7 @@ a reference to the relevant reference section is provided. \index{FIS (feasibility proof obligation)} \index{INV (invariant proof obligation)} \index{GRD (guard-strengthening proof obligation)} -\index{MRG (guard-strengthening (merge) proof obligation)} +\index{MRG (guard-strengthening (merge) pr\-oof obligation)} \index{SIM (simulation proof obligation)} \index{EQL (equality of preserved variable proof obligation)} \index{WWD (well-definedness of witness proof obligation)} diff --git a/org.rodinp.handbook.feature/latex/rodin-doc.tex b/org.rodinp.handbook.feature/latex/rodin-doc.tex index 9b08d62292db148e8a04031ff0e6e72ae6db7080..06d7536c8314c79e819e73406c027dc9a1086645 100644 --- a/org.rodinp.handbook.feature/latex/rodin-doc.tex +++ b/org.rodinp.handbook.feature/latex/rodin-doc.tex @@ -1,11 +1,12 @@ \ifdefined\isinprint \documentclass[twoside,10pt]{book} \usepackage[twoside,paperwidth=155.93mm,paperheight=233.89mm,hmargin={15mm,15mm},vmargin={20mm,20mm},bindingoffset=5mm]{geometry} +\usepackage[hyphens]{url} \usepackage[colorlinks=false, pdfborder={0 0 0} pdftex, plainpages=false, - pdfauthor={Michael Jastram (Ed.)}, + pdfauthor={Michael Jastram (Editor)}, pdftitle={Rodin User's Handbook}, pdfsubject={Rodin is a platform for Event-B based formal modelling}, pdfkeywords={Rodin, Event-B}, @@ -14,6 +15,7 @@ \else \documentclass[12pt]{book} \usepackage[left=2.5cm,top=3cm,right=2.5cm,bottom=3cm]{geometry} +\usepackage[hyphens]{url} \usepackage[colorlinks=true, pdftex, plainpages=false, @@ -64,7 +66,7 @@ Handbook $ $Rev$ $ \\ {\titledimsubtext\selectfont \textbf{\textsf{Covers Rodin v.\versionnr}}} \vspace*{\titlesecdistance} -{\titledimsubtext\selectfont \textsf{Michael Jastram (Ed.)}} +{\titledimsubtext\selectfont \textsf{Michael Jastram (Editor)}} \vspace*{\titlesubtitledistance} {\titledimsubtext\selectfont \textsf{Foreword by Prof. Michael Butler}} @@ -91,7 +93,7 @@ Handbook $ $Rev$ $ \\ \vspace*{\fill} \noindent\textbf{Rodin User's Handbook}\\ ~\\ -\noindent\copyright Formal Mind Gmbh 2013\\ +\noindent\copyright Formal Mind Gmbh 2014\\ 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. 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. diff --git a/org.rodinp.handbook.feature/latex/tutorial-04.tex b/org.rodinp.handbook.feature/latex/tutorial-04.tex index b7a23a54125a544cb860d1bbd699a21b45304b6c..985e8d877ac2d5b78dac539c274ac1a40f4cb195 100644 --- a/org.rodinp.handbook.feature/latex/tutorial-04.tex +++ b/org.rodinp.handbook.feature/latex/tutorial-04.tex @@ -140,7 +140,7 @@ constants and state that $apples \subseteq FRUITS$ and $oranges \subseteq FRUITS If apples and oranges are all fruits we want to model, we can assume $apples \cup oranges = FRUITS$ and if no fruit is both an apple and orange we can write $apples \cap oranges = \emptyset$. A shorter way to express this is to say that apples and oranges constitute a -partition of the fruits: $partition(FRUITS,apples,oranges)$. +partition of the fruits: $partition(FRUITS,$ $apples,$ $oranges)$. % broke formula for print version In general, we can use the partition operator to express that a set $S$ is partitioned by the sets $s_1,\ldots,s_n$ with $partition(S,s_1,\ldots,s_n)$. We use partitions in Section~\ref{tut_modelling_persons}. diff --git a/org.rodinp.handbook.feature/latex/tutorial-06.tex b/org.rodinp.handbook.feature/latex/tutorial-06.tex index 4e2fe0d842784891859fdf4d9fc53b3ed22abb85..68806f2b25bece1c5465a7c51f0b272774a7a70e 100644 --- a/org.rodinp.handbook.feature/latex/tutorial-06.tex +++ b/org.rodinp.handbook.feature/latex/tutorial-06.tex @@ -172,7 +172,8 @@ concrete guards can be used as hypotheses in the proof. The second condition, that the gluing invariant remains true, is just a more general case of the proof obligation which ensures that an event does not violate the invariant. So the proof obligation's label is again -\eventbpo{concrete\_event/concrete\_invariant/INV}. The goal is to prove that the invariant of the concrete machine is valid when each occurrence of a modified variable is replaced by its new value. +\eventbpo{con\-crete\_event/con\-crete\_invariant/INV}. +The goal is to prove that the invariant of the concrete machine is valid when each occurrence of a modified variable is replaced by its new value. The hypotheses we use are: \begin{itemize} \item We assume that the invariant of both the concrete and abstract machines were valid before the event occurred. diff --git a/org.rodinp.handbook.feature/latex/tutorial-07.tex b/org.rodinp.handbook.feature/latex/tutorial-07.tex index ae95b286fb9c29db24044c13bb40445f794b910c..c5bcda8252aef2741b50a3be285b4439a055e791 100644 --- a/org.rodinp.handbook.feature/latex/tutorial-07.tex +++ b/org.rodinp.handbook.feature/latex/tutorial-07.tex @@ -130,7 +130,7 @@ Next, we will create a gluing invariant (\ref{abstract_machine}) that associates \end{description} } -In its current state, this gluing invariant can be violated: if the event \textsf{set\_peds\_go} is triggered, for instance, the variable \textsf{peds\_go} will change but \textsf{peds\_colour} will not. We expect that this will result in undischarged proof obligations (\ref{generated_proof_obligations}). We can check this by expanding the machine in the Event-B Explorer. Indeed, we now see two undischarged proof obligations (compare with Figure \ref{fig_tut_07_undischarged}). +In its current state, this gluing invariant can be violated: if the event \textsf{set\_peds\_go} is triggered, for instance, the variable \textsf{peds\_go} will change but \textsf{peds\_\-colour} will not. We expect that this will result in undischarged proof obligations (\ref{generated_proof_obligations}). We can check this by expanding the machine in the Event-B Explorer. Indeed, we now see two undischarged proof obligations (compare with Figure \ref{fig_tut_07_undischarged}). \begin{figure}[!ht] \begin{center}