diff --git a/org.rodinp.handbook.feature/latex/config.tex b/org.rodinp.handbook.feature/latex/config.tex
index b719fb7397e42f9f542a7153c96c8d262ad6a031..a99efae01709b13f9c758890d56ce25a9fa5d5bf 100644
--- a/org.rodinp.handbook.feature/latex/config.tex
+++ b/org.rodinp.handbook.feature/latex/config.tex
@@ -1,5 +1,5 @@
% Rodin Handbook Version
-\newcommand{\versionnr}{2.5}
+\newcommand{\versionnr}{2.7}
% Rodin Handbook Version Path. "current" is the newest version of the handbook. This should be changed if we want to build a handbook for another (i.e. older version)
\newcommand{\versionpath}{current}
diff --git a/org.rodinp.handbook.feature/latex/faq.tex b/org.rodinp.handbook.feature/latex/faq.tex
index aef716b58417b9666cbbb701d0812b298068c1d2..1aa884a65b54506e807a505d81017c1efa312855 100644
--- a/org.rodinp.handbook.feature/latex/faq.tex
+++ b/org.rodinp.handbook.feature/latex/faq.tex
@@ -205,7 +205,7 @@ In order to remove a project, first select it on the \textsf{Project Explorer} a
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/faq/faq_removeproject.png}
+ \includerodinimg{faq/faq_removeproject.png}
\caption{Removing a Event-B Project}
\label{fig_faq_removeproject}
\end{center}
@@ -219,7 +219,7 @@ Exporting a project is the operation by which you can construct automatically a
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/faq/faq_exportproject.png}
+ \includerodinimg{faq/faq_exportproject.png}
\caption{Export a Event-B Project}
\label{fig_faq_exportproject}
\end{center}
@@ -271,7 +271,7 @@ Once a machine or context is (partially) edited, you can save it by using the sa
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/faq/faq_saveaction.png}
+ \includerodinimg{faq/faq_saveaction.png}
\caption{Save a context or a machine}
\label{fig_faq_saveaction}
\end{center}
diff --git a/org.rodinp.handbook.feature/latex/img/bw/info_64.png b/org.rodinp.handbook.feature/latex/img/bw/info_64.png
new file mode 100644
index 0000000000000000000000000000000000000000..2236d15b418db3b33bababa23a82bf279a4d22e5
Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/bw/info_64.png differ
diff --git a/org.rodinp.handbook.feature/latex/img/bw/tick_64.png b/org.rodinp.handbook.feature/latex/img/bw/tick_64.png
new file mode 100644
index 0000000000000000000000000000000000000000..d664007ba92ad44693cc18d9c2a14d85313a4227
Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/bw/tick_64.png differ
diff --git a/org.rodinp.handbook.feature/latex/img/bw/warning.pdf b/org.rodinp.handbook.feature/latex/img/bw/warning.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..a17118ecd38b47ecda406599a3caf5325b75a40b
Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/bw/warning.pdf differ
diff --git a/org.rodinp.handbook.feature/latex/makros.tex b/org.rodinp.handbook.feature/latex/makros.tex
index 81f775c15dfe9ed22011d5acef78759ddd73309b..b0e30d4733ab30da6773bcfbcd3f26b2dfbad723 100644
--- a/org.rodinp.handbook.feature/latex/makros.tex
+++ b/org.rodinp.handbook.feature/latex/makros.tex
@@ -2,6 +2,32 @@
\newif\ifplastex
\plastexfalse
+% defining a if(isinprint) environment
+\newif\ifinprint
+\ifdefined\isinprint
+\inprinttrue
+\else
+\inprintfalse
+\fi
+
+% for the print, we use an extra b&w directory
+\ifinprint
+\newcommand{\rodinimgdir}{bwimg}
+\else
+\newcommand{\rodinimgdir}{img}
+\fi
+
+\ifinprint
+\def\doculist#1#2{
+\begin{quote}
+\hspace{-10mm}
+\includegraphics[height=4ex]{#2}
+\vspace{-8mm}
+
+#1
+\end{quote}
+}
+\else
\def\doculist#1#2{
\begin{quote}
\hspace{-10mm}
@@ -11,15 +37,47 @@
#1
\end{quote}
}
+\fi
-\def\tick#1{\doculist{#1}{img/tick_64.png}}
-\def\info#1{\doculist{#1}{img/info_64.png}}
-\def\warning#1{\doculist{#1}{img/warning_64.png}}
-\def\pencil#1{\doculist{#1}{img/pencil_64.png}}
+% dimensions on the title page
+\newlength{\titletop}
+\newlength{\titlesubtitledistance}
+\newlength{\titlebottom}
+\newlength{\titlesecdistance}
+\ifinprint
+\def\titledimrodin{\fontsize{58}{71}}
+\def\titledimhandbook{\fontsize{20.5}{25}}
+\def\titledimsubtext{\fontsize{13}{16}}
+\def\titledimsponsor{\fontsize{11}{15}}
+\setlength{\titletop}{120mm}
+\setlength{\titlesubtitledistance}{2mm}
+\setlength{\titlebottom}{-30mm}
+\setlength{\titlesecdistance}{8mm}
+\else
+\def\titledimrodin{\fontsize{70}{85}}
+\def\titledimhandbook{\fontsize{24.5}{30}}
+\def\titledimsubtext{\fontsize{16}{19}}
+\def\titledimsponsor{\fontsize{11}{15}}
+\setlength{\titletop}{145mm}
+\setlength{\titlesubtitledistance}{2mm}
+\setlength{\titlebottom}{-22mm}
+\setlength{\titlesecdistance}{10mm}
+\fi
+
+\ifinprint
+\def\tick#1{\doculist{#1}{img/bw/tick_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\warnging#1{\doculist{#1}{\rodinimgdir/warning_64.png}}
+\fi
+\def\pencil#1{\doculist{#1}{\rodinimgdir/pencil_64.png}}
% macro for icons
\def\icon#1{
-\includegraphics[height=2ex]{img/icons/#1}
+\includegraphics[height=2ex]{\rodinimgdir/icons/#1}
}
% macro for image versions (pdf version + html version)
@@ -39,7 +97,7 @@
\else
\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=#2]{#1}
+ \includegraphics[width=#2]{\rodinimgdir/#1}
\caption{#4}
\label{#5}
\end{center}
@@ -47,6 +105,9 @@
\fi
}
+\newcommand{\includerodinimg}[1]{\includegraphics{\rodinimgdir/#1}}
+\newcommand{\includerodintwimg}[2]{\includegraphics[width=#1\textwidth]{\rodinimgdir/#2}}
+
% different method to write an ASCII backslash for plastex and normal pdflatex
\ifplastex
\newcommand{\mybackslash}{\textbackslash}
@@ -86,7 +147,7 @@
\renewcommand{\tmpName}{#2}
\begin{verse}
\begin{wrapfigure}{l}{}
- \includegraphics{#1}
+ \includegraphics{\rodinimgdir/#1}
\end{wrapfigure}
}
{
@@ -103,7 +164,7 @@
\begin{shaded}
\begin{wrapfigure}{l}{10mm}
\vspace{-5mm}
-\includegraphics[width=10mm]{#1}
+\includegraphics[width=10mm]{\rodinimgdir/#1}
\vspace{-5mm}
\end{wrapfigure}
\noindent
diff --git a/org.rodinp.handbook.feature/latex/reference-01.tex b/org.rodinp.handbook.feature/latex/reference-01.tex
index 488324891fd782eb4c7749a7b59dc8f4f1690778..a32000e1ad5b147720514a6bf1f10d6ab024fb89 100644
--- a/org.rodinp.handbook.feature/latex/reference-01.tex
+++ b/org.rodinp.handbook.feature/latex/reference-01.tex
@@ -24,7 +24,18 @@ The primary concept in doing formal developments with the Rodin Platform is that
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_10_project1.png}
+ \framebox{\parbox{0.3\textwidth}{{\large Machine}
+ \begin{itemize}
+ \item[] variables
+ \item[] invariants
+ \item[] events
+ \end{itemize}}}
+ \hspace*{5em}\framebox{\parbox{0.3\textwidth}{{\large Context}
+ \begin{itemize}
+ \item[] carrier sets
+ \item[] constants
+ \item[] axioms
+ \end{itemize}}}
\caption{Overview Machine and Context}
\label{fig_ref_10_project1}
\end{center}
@@ -35,7 +46,7 @@ Various relationships exist between machines and contexts. This is illustrated i
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_10_project2.png}
+ \includerodinimg{reference/ref_10_project2.png}
\caption{A typical example of machine and context relationship}
\label{fig_ref_10_project2}
\end{center}
@@ -58,7 +69,7 @@ Eclipse Projects can have one or more natures to describe their purpose. The GU
Figure \ref{fig_ref_01_eventb_perspective1} shows an overview of the opening window of the Event-B Perspective. The following subsections identify the different Rodin GUI elements (i.e. views) which are visible and explain their functions.
-\imagedpi{img/reference/ref_01_eventb_perspective1.pdf}{150mm}{img/reference/ref_01_eventb_perspective1.png}{Overview of the Event-B Perspective}{fig_ref_01_eventb_perspective1}
+\imagedpi{reference/ref_01_eventb_perspective1.pdf}{\textwidth}{img/reference/ref_01_eventb_perspective1.png}{Overview of the Event-B Perspective}{fig_ref_01_eventb_perspective1}
\subsubsection{Menu bar}
\label{menu_bar}
@@ -77,7 +88,7 @@ One action is available when editing context files (see Figure \ref{fig_ref_01_m
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_menubar2.png}
+ \includerodinimg{reference/ref_01_menubar2.png}
\caption{Automatic rename actions for context files}
\label{fig_ref_01_menubar2}
\end{center}
@@ -93,7 +104,7 @@ Three actions are available for machine files (see Figure \ref{fig_ref_01_menuba
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_menubar1.png}
+ \includerodinimg{reference/ref_01_menubar1.png}
\caption{Automatic rename actions for machine files}
\label{fig_ref_01_menubar1}
\end{center}
@@ -137,7 +148,7 @@ The ASCII code corresponding to the symbol over which the mouse hovers is also d
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_symbol_table1.png}
+ \includerodintwimg{1.0}{reference/ref_01_symbol_table1.png}
\caption{Clicking a symbol inserts it at the current position}
\label{fig_ref_01_symbol_table1}
\end{center}
@@ -155,7 +166,7 @@ When expanding a machine or a context, you can explore its elements. Double clic
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_project_explorer1.png}
+ \includerodintwimg{1.0}{reference/ref_01_project_explorer1.png}
\caption{Double clicking on an element opens the Event-B editor and marks the corresponding position}
\label{fig_ref_01_project_explorer1}
\end{center}
@@ -174,7 +185,7 @@ For the most part, the perspectives can be customized by dragging and dropping t
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_customizing2.png}
+ \includerodinimg{reference/ref_01_customizing2.png}
\caption{Show View as a Fast View}
\label{fig_ref_01_customizing2}
\end{center}
@@ -193,7 +204,7 @@ All of the windows that you cannot create directly when clicking on \textsf{Show
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_10_customizing.png}
+ \includerodintwimg{1.0}{reference/ref_10_customizing.png}
\caption{Our self-made Quick perspective}
\label{fig_ref_10_customizing}
\end{center}
@@ -209,7 +220,7 @@ Once a context or a machine is created, a window appears in the editing area as
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor1_neweditor.png}
+ \includerodintwimg{1.0}{reference/ref_01_eventb_editor1_neweditor.png}
\caption{The Event-B editor}
\label{fig_ref_01_eventb_editor1_neweditor}
\end{center}
@@ -221,7 +232,7 @@ Machine elements can also be added in the same way.
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_neweditor_add_element.png}
+ \includerodintwimg{1.0}{reference/ref_01_neweditor_add_element.png}
\caption{Adding a new modelling element}
\label{fig_ref_01_neweditor_add_element}
\end{center}
@@ -241,7 +252,7 @@ Once a context or a machine is created, a window appears in the editing area as
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor1.png}
+ \includerodinimg{reference/ref_01_eventb_editor1.png}
\caption{The Structured Event-B editor}
\label{fig_ref_01_eventb_editor1}
\end{center}
@@ -252,7 +263,7 @@ by pressing the triangle (\icon{rodin/collapsed.png}) next to each keyword, you
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor2.png}
+ \includerodinimg{reference/ref_01_eventb_editor2.png}
\caption{By pressing the triangle you can collapse/expand context sections}
\label{fig_ref_01_eventb_editor2}
\end{center}
@@ -262,7 +273,7 @@ By pressing the \icon{rodin/add.png} button, you can add a new modelling element
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor3.png}
+ \includerodintwimg{1.0}{reference/ref_01_eventb_editor3.png}
\caption{Adding a new modelling element}
\label{fig_ref_01_eventb_editor3}
\end{center}
@@ -277,7 +288,7 @@ By selecting the \textsf{Dependencies} tab at the bottom of the Event-B editor,
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor8.png}
+ \includerodinimg{reference/ref_01_eventb_editor8.png}
\caption{Dependencies tab of the Event-B editor}
\label{fig_ref_01_eventb_editor8}
\end{center}
@@ -289,7 +300,7 @@ There is also another way to create a new context as an extension existing one.
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor9.png}
+ \includerodinimg{reference/ref_01_eventb_editor9.png}
\caption{New EXTENDS Clause window}
\label{fig_ref_01_eventb_editor9}
\end{center}
@@ -309,7 +320,7 @@ Selecting the \textsf{Synthesis} tab brings up a global view of your context's e
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor11.png}
+ \includerodinimg{reference/ref_01_eventb_editor11.png}
\caption{The Synthesis tab of the Event-B editor}
\label{fig_ref_01_eventb_editor11}
\end{center}
@@ -333,7 +344,7 @@ Selecting the \textsf{Pretty Print} tab gives you a global view of your context
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor10.png}
+ \includerodinimg{reference/ref_01_eventb_editor10.png}
\caption{The Pretty Print tab of the Event-B editor}
\label{fig_ref_01_eventb_editor10}
\end{center}
@@ -347,7 +358,7 @@ You can activate the different wizards by using the buttons in the tool bar as s
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor12.png}
+ \includerodinimg{reference/ref_01_eventb_editor12.png}
\caption{Wizards for context specific elements located in the tool bar}
\label{fig_ref_01_eventb_editor12}
\end{center}
@@ -355,7 +366,7 @@ You can activate the different wizards by using the buttons in the tool bar as s
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor13.png}
+ \includerodinimg{reference/ref_01_eventb_editor13.png}
\caption{Wizards for machine specific elements located in the tool bar}
\label{fig_ref_01_eventb_editor13}
\end{center}
@@ -370,7 +381,7 @@ To activate the \textsf{New Carrier Sets Wizard}, press the \icon{rodin/newset_e
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor4.png}
+ \includerodinimg{reference/ref_01_eventb_editor4.png}
\caption{New Carrier Sets Wizard}
\label{fig_ref_01_eventb_editor4}
\end{center}
@@ -386,13 +397,14 @@ To activate the \textsf{New Enumerated Set Wizard}, press the \icon{rodin/newenu
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor5.png}
+ \includerodinimg{reference/ref_01_eventb_editor5.png}
\caption{New Enumerated Set Wizard}
\label{fig_ref_01_eventb_editor5}
\end{center}
\end{figure}
-Enter the name of the new enumerated set as well as the names of its elements. By pressing the \textsf{More Elements} button, you can enter additional elements. When you're finished, press the \textsf{OK} button. The benefit of using this wizard is that in addition to creating the set and its elements, the wizard automatically creates the axiom that is necessary for the context to work. For example, when you add the new carrier set \texttt{COLOUR} and the three constants \texttt{red}, \texttt{green}, and \texttt{orange}, the wizard automatically creates the following axiom $partition(COLOUR , \{red\}, \{green\}, \{orange\})$.
+Enter the name of the new enumerated set as well as the names of its elements. By pressing the \textsf{More Elements} button, you can enter additional elements. When you're finished, press the \textsf{OK} button. The benefit of using this wizard is that in addition to creating the set and its elements, the wizard automatically creates the axiom that is necessary for the context to work. For example, when you add the new carrier set \texttt{COLOUR} and the three constants \texttt{red}, \texttt{green}, and \texttt{orange}, the wizard automatically creates the following axiom
+\[partition(COLOUR , \{red\}, \{green\}, \{orange\})\].
\subsubsection{New Constants Wizard}
\index{wizard!New Constants Wizard}
@@ -402,7 +414,7 @@ To activate the \textsf{New Constants Wizard}, press the \icon{rodin/newcst_edit
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor6.png}
+ \includerodinimg{reference/ref_01_eventb_editor6.png}
\caption{New Constants Wizard}
\label{fig_ref_01_eventb_editor6}
\end{center}
@@ -418,7 +430,7 @@ To activate the \textsf{New Axioms Wizard}, press the \icon{rodin/newaxm_edit.pn
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor7.png}
+ \includerodinimg{reference/ref_01_eventb_editor7.png}
\caption{New Axioms Wizard}
\label{fig_ref_01_eventb_editor7}
\end{center}
@@ -435,7 +447,7 @@ To activate the \textsf{New Variable Wizard}, press the \icon{rodin/newvar_edit.
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor14.png}
+ \includerodinimg{reference/ref_01_eventb_editor14.png}
\caption{New Variable Wizard}
\label{fig_ref_01_eventb_editor14}
\end{center}
@@ -451,7 +463,7 @@ To activate the \textsf{New Invariants Wizard}, press the \icon{rodin/newinv_edi
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor15.png}
+ \includerodinimg{reference/ref_01_eventb_editor15.png}
\caption{New Invariants Wizard}
\label{fig_ref_01_eventb_editor15}
\end{center}
@@ -467,7 +479,7 @@ To activate the \textsf{New Events Wizard}, press the \icon{rodin/newevt_edit.pn
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_eventb_editor16.png}
+ \includerodintwimg{1.0}{reference/ref_01_eventb_editor16.png}
\caption{New Event Wizard}
\label{fig_ref_01_eventb_editor16}
\end{center}
@@ -486,7 +498,7 @@ When proof obligations (POs) (\ref{generated_proof_obligations}) are not dischar
The Proving Perspective consists of a number of views: the \textsf{Proof Tree}, the \textsf{Goal}, the \textsf{Selected Hypotheses}, the \textsf{Proof Control}, the \textsf{Search Hypotheses}, the \textsf{Cache Hypotheses} and the \textsf{Proof Information}. In the discussion that follows we look at each of these views individually. Figure \ref{fig_ref_01_proving_perspective1} shows an overview of the Proving Perspective.
-\imagedpi{img/reference/ref_01_proving_perspective1.pdf}{150mm}{img/reference/ref_01_proving_perspective1.png}{Overview of the Proving Perspective}{fig_ref_01_proving_perspective1}
+\imagedpi{reference/ref_01_proving_perspective1.pdf}{\textwidth}{img/reference/ref_01_proving_perspective1.png}{Overview of the Proving Perspective}{fig_ref_01_proving_perspective1}
\subsubsection{Loading a Proof}
@@ -502,7 +514,7 @@ The proof tree view provides a graphical representation of each individual proof
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective2.png}
+ \includerodinimg{reference/ref_01_proving_perspective2.png}
\caption{The Proof Tree}
\label{fig_ref_01_proving_perspective2}
\end{center}
@@ -566,7 +578,7 @@ Each sequent in the proof tree have corresponding hypotheses and goals. A user w
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective3.png}
+ \includerodintwimg{0.7}{reference/ref_01_proving_perspective3.png}
\caption{Open proof obligation}
\label{fig_ref_01_proving_perspective3}
\end{center}
@@ -589,7 +601,7 @@ Other proof rules can be applied when green buttons appear in the \textsf{Goal}
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective4.png}
+ \includerodintwimg{0.8}{reference/ref_01_proving_perspective4.png}
\caption{Applying a rule}
\label{fig_ref_01_proving_perspective4}
\end{center}
@@ -599,7 +611,7 @@ To instantiate a quantifier, the user enters the desired expression in the yello
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective5.png}
+ \includerodinimg{reference/ref_01_proving_perspective5.png}
\caption{Instantiating a quantifier}
\label{fig_ref_01_proving_perspective5}
\end{center}
@@ -614,7 +626,7 @@ The \textsf{Proof Control} view contains the buttons with which you can perform
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective6.png}
+ \includerodintwimg{1.1}{reference/ref_01_proving_perspective6.png}
\caption{The Proof Control View}
\label{fig_ref_01_proving_perspective6}
\end{center}
@@ -685,7 +697,7 @@ The auto prover can be run by clicking the \icon{rodin/auto_prover.png}. This pr
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics{img/reference/ref_10_auto_prover_pref.png}
+% \includerodinimg{reference/ref_10_auto_prover_pref.png}
% \caption{Auto Prover Preferences}
% \label{fig_ref_10_auto_prover_pref}
%\end{center}
@@ -702,7 +714,7 @@ By typing a string in the \textsf{Proof Control} view and pressing the \textsf{S
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective7.png}
+ \includerodinimg{reference/ref_01_proving_perspective7.png}
\caption{The Search Hypotheses View}
\label{fig_ref_01_proving_perspective7}
\end{center}
@@ -732,8 +744,8 @@ Operations similar to those in the \textsf{Selected Hypotheses} and \textsf{Sear
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective15.png}
- \caption{Proof Information View}
+ \includerodintwimg{0.7}{reference/ref_01_proving_perspective15.png}
+ \caption{Type Environment View}
\label{fig_ref_01_proving_perspective15}
\end{center}
\end{figure}
@@ -746,7 +758,7 @@ This view displays information so that the user can relate a proof obligation to
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective8.png}
+ \includerodinimg{reference/ref_01_proving_perspective8.png}
\caption{Proof Information View}
\label{fig_ref_01_proving_perspective8}
\end{center}
@@ -759,7 +771,7 @@ This information can be viewed by right clicking on any node in the proof tree a
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective9.png}
+ \includerodinimg{reference/ref_01_proving_perspective9.png}
\caption{Open Rule Details View}
\label{fig_ref_01_proving_perspective9}
\end{center}
@@ -771,7 +783,7 @@ Figure \ref{fig_ref_01_proving_perspective10} gives an overview of the \textsf{R
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective10.png}
+ \includerodinimg{reference/ref_01_proving_perspective10.png}
\caption{Rule Details View}
\label{fig_ref_01_proving_perspective10}
\end{center}
@@ -789,7 +801,7 @@ The auto-tactic automatically applies a combination (i.e. ordered list) of rewri
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective11.png}
+ \includerodinimg{reference/ref_01_proving_perspective11.png}
\caption{Toggle auto-prover via project menu}
\label{fig_ref_01_proving_perspective11}
\end{center}
@@ -801,7 +813,7 @@ Note that the post-tactic can be disabled quickly by clicking on the \textsf{rod
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_proving_perspective12.png}
+ \includerodinimg{reference/ref_01_proving_perspective12.png}
\caption{Proof Control view menu}
\label{fig_ref_01_proving_perspective12}
\end{center}
@@ -836,7 +848,7 @@ The colour and fonts preference page allows you to set the text and comment colo
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences13.png}
+ \includerodinimg{reference/ref_01_preferences13.png}
\caption{Colours and Fonts preferences}
\label{fig_ref_01_preferences13}
\end{center}
@@ -870,11 +882,11 @@ This page describes the default values that are used for the prefixes of the dif
Figure \ref{fig_ref_01_preferences1} shows that modifying prefixes on the workspace level or on the project level will affect the names used at creation of new Event-B elements. One can see that the prefixes for variables and invariants, which were originally set to ``var" or ``inv'', have been replaced by ``variable" and ``invariant". New elements are then named using those prefixes.
-\imagedpi{img/reference/ref_01_preferences1.pdf}{135mm}{img/reference/ref_01_preferences1.png}{Prefix Settings}{fig_ref_01_preferences1}
+\imagedpi{reference/ref_01_preferences1.pdf}{\textwidth}{img/reference/ref_01_preferences1.png}{Prefix Settings}{fig_ref_01_preferences1}
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics{img/reference/ref_01_preferences1.png}
+% \includerodinimg{reference/ref_01_preferences1.png}
% \caption{Prefix Settings}
% \label{fig_ref_01_preferences1}
%\end{center}
@@ -892,7 +904,7 @@ A window (see Figure \ref{fig_ref_01_preferences2}) appears that allows a user t
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences2.png}
+ \includerodinimg{reference/ref_01_preferences2.png}
\caption{Project specific prefix settings}
\label{fig_ref_01_preferences2}
\end{center}
@@ -923,13 +935,13 @@ The \textsf{Proof Control} view menu shows whether there are sequent prover pref
Indeed, the command label in the menu tells if project specific settings are set, or if the workspace settings are considered. The command opens the corresponding \textsf{Auto/Post Tactic} page.
\begin{figure}
-\begin{minipage}[t]{.40\linewidth}
- \centering \includegraphics{img/reference/ref_01_proving_perspective13.png}
+\begin{minipage}[t]{.45\linewidth}
+ \centering \includerodintwimg{1.0}{reference/ref_01_proving_perspective13.png}
\caption{(a) direct access to the Celebrity project specific settings}
\label{fig_ref_01_proving_perspective13}
\end{minipage}\hfill
-\begin{minipage}[t]{.40\linewidth}
-\centering \includegraphics{img/reference/ref_01_proving_perspective14.png}
+\begin{minipage}[t]{.45\linewidth}
+\centering \includerodintwimg{1.0}{reference/ref_01_proving_perspective14.png}
\caption{(b) no project settings exist for the current PO, direct access to workspace settings}
\label{fig_ref_01_proving_perspective14}
\end{minipage}
@@ -945,7 +957,7 @@ Figure \ref{fig_ref_01_preferences7} shows the \textsf{Auto/Post Tactic} prefere
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences7.png}
+ \includerodintwimg{1.0}{reference/ref_01_preferences7.png}
\caption{The ``Auto/Post Tactic" preference page}
\label{fig_ref_01_preferences7}
\end{center}
@@ -957,7 +969,7 @@ The options shown by (1) and (2) allow you to activate/deactivate the automatic
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics{img/reference/ref_01_preferences8.png}
+% \includerodinimg{reference/ref_01_preferences8.png}
% \caption{Selecting a profile for the Auto-Tactics}
% \label{fig_ref_01_preferences8}
%\end{center}
@@ -972,7 +984,7 @@ Figure \ref{fig_ref_01_preferences9} shows the contents of the profile tab. Ther
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences9.png}
+ \includerodintwimg{1.0}{reference/ref_01_preferences9.png}
\caption{Selecting a profile for the Auto-Tactics}
\label{fig_ref_01_preferences9}
\end{center}
@@ -992,7 +1004,7 @@ Default profiles can not be edited nor removed. That is why these options are co
Figure \ref{fig_ref_01_preferences10} shows the dialog available to edit or create a profile. For instance, here we create a profile named ``MyFirstTacticProfile".
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences10.png}
+ \includerodintwimg{1.0}{reference/ref_01_preferences10.png}
\caption{Selecting a profile for the Auto-Tactics}
\label{fig_ref_01_preferences10}
\end{center}
@@ -1006,7 +1018,7 @@ The user can select profiles locally for each project. To do so, select the \tex
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences11.png}
+ \includerodintwimg{1.0}{reference/ref_01_preferences11.png}
\caption{Auto/Post Tactic Tab for project specific settings for Auto/Post Tactic}
\label{fig_ref_01_preferences11}
\end{center}
@@ -1016,7 +1028,7 @@ Note that the enablement of automatic use of post and auto tactics is decided at
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/reference/ref_01_preferences12.png}
+ \includerodintwimg{1.0}{reference/ref_01_preferences12.png}
\caption{Profiles Tab for project specific settings for Auto/Post Tactic}
\label{fig_ref_01_preferences12}
\end{center}
@@ -1060,7 +1072,7 @@ One may notice the absence of child-specific combinator (i.e. combinators that a
A composer combinator applies its given tactic(s) to the given node. The given node may be open or closed. It succeeds if at least 1 tactic application is successful.
\begin{center}
- \begin{tabular}{ | l | l | p{4.5cm} | p{4.5cm} |}
+ \begin{tabular}{ | p{0.18\textwidth} | l | p{0.28\textwidth} | p{0.28\textwidth} |}
\hline
Name & Arity & Description & Stops when \\ \hline
Sequence & 1..n & applies given tactics in given order & all tactics have been applied \\ \hline
@@ -1075,7 +1087,7 @@ A composer combinator applies its given tactic(s) to the given node. The given n
A selector combinator applies its given tactic to the set of nodes it selects. Selected nodes are computed from the given node. The given node may be open or closed. It succeeds if the tactic application is successful for at least 1 selected node.
\begin{center}
- \begin{tabular}{ | l | l | p{10cm} |}
+ \begin{tabular}{ | l | l | p{0.55\textwidth} |}
\hline
Name & Arity & Selects \\ \hline
On all pending & 1 & all pending children of the given node (the given node itself if it is open) \\ \hline
@@ -1087,7 +1099,7 @@ A selector combinator applies its given tactic to the set of nodes it selects. S
A post actions applies its given tactic to the given node. The given node must be open (otherwise it fails). Then it performs a specific treatment which is guarded by a trigger condition.
\begin{center}
- \begin{tabular}{ | p{1,5cm} | p{1cm} | p{6cm} | p{5cm} |}
+ \begin{tabular}{ | l | l | p{0.3\textwidth} | p{0.3\textwidth} |}
\hline
Name & Arity & Trigger Condition & Post Action \\ \hline
Attempt & 1 & the given node still has pending children (subtree not closed) & prune proof tree at given node \\ \hline
@@ -1095,7 +1107,12 @@ A post actions applies its given tactic to the given node. The given node must b
\end{center}
\subparagraph{Loop on All pending}
-\[loopOnAllPending(T_1 \ldots T_n) \;\;\defi\;\; loop(onAllPending(composeUntilSuccess(T_1 \ldots T_n)))\]
+\[
+\begin{array}{rl}
+ & loopOnAllPending(T_1 \ldots T_n) \\
+ \defi & loop(onAllPending(composeUntilSuccess(T_1 \ldots T_n)))
+\end{array}
+\]
\paragraph{Other Ideas}
diff --git a/org.rodinp.handbook.feature/latex/reference-02.tex b/org.rodinp.handbook.feature/latex/reference-02.tex
index 2e32e4f1abf1a655277093c7c5ddd9d5af8f2f9b..8c5bd920e4898d95ed752288537db16a4d94f66d 100644
--- a/org.rodinp.handbook.feature/latex/reference-02.tex
+++ b/org.rodinp.handbook.feature/latex/reference-02.tex
@@ -9,13 +9,6 @@
\newcommand{\absbeforeafter}{\mathcal{S}}
\newcommand{\concbeforeafter}{\mathcal{T}}
-\newcommand{\axioms}{A(\allconstants)}
-\newcommand{\absinvariants}{I(\allconstants,\absvariables)}
-\newcommand{\concinvariants}{J(\allconstants,\absvariables,\concvariables)}
-\newcommand{\absguards}{G(\allconstants,\absvariables,\absparameters)}
-\newcommand{\concguards}{H(\allconstants,\concvariables,\concparameters)}
-\newcommand{\witnesspred}{W(\allconstants,\allvariables,\absvariables',\concvariables',\allparameters)}
-\newcommand{\bapred}{\concbeforeafter(\allconstants,\concparameters,\concvariables,\concvariables')}
% The screenshots from the previous section should not appear in this section
\clearpage
@@ -64,6 +57,27 @@ As a convention, we use
\item $G$ and $H$ for the guards of the abstract events or concrete event respectively
\end{itemize}
+\subsection{Substitutions}
+We use the notation $P[E/x]$ for a substitution of all free occurrences of the variable $x$ in
+$P$ by the expression $E$.
+Several substitutions can be performed simultaneously with $P(E_1/x_1,\ldots,E_n/x_n)$.
+In particular, we use the syntax $P[\varlist{x}'/\varlist{x}]$ to denote the substitution of
+each identifier $x$ in the sequence $\varlist{x}$ by $x'$.
+For more information on free identifiers, see Section~\ref{free_identifiers}.
+
+Examples:
+\begin{itemize}
+\item $(x>y)[5+2/y]$ corresponds to the predicate $(x>5+2)$.
+\item $(x>y)[2\cdot y/x,5+2/y]$ corresponds to the predicate $(2\cdot y>5+2)$.
+\item $(\exists x \qdot x\in S \land x>y)[2\cdot y/x,5+2/y]$ corresponds to the predicate
+ $(\exists x \qdot x\in S \land x>5+2)$, because the $x$ is a quantified variable
+ (i.e. it is not a free variable).
+\item For a sequence $\varlist{v}=v_1,v_2,v_3$ the predicate
+ $(v_1\subseteq v_2\land v_3\in v_1)[\varlist{v}'/\varlist{v}]$ corresponds to
+ $(v_1'\subseteq v_2'\land v_3'\in v_1')$.
+\end{itemize}
+
+
\subsection{Contexts}
\label{context}
\index{context}
@@ -106,7 +120,8 @@ An axiom must also be in place from which the type of the constant can be inferr
We denote the sequence of all constants with $\varlist{c}$.
An axiom is a statement that is assumed to be true in the rest of the model.
-Each axiom consists of a label and a predicate $A(\varlist{c})$.
+Each axiom consists of a label and a predicate $A$.
+All free identifiers in $A$ must be constants.
Axioms can be marked as theorems. The proof obligation that are then generated are described in Section \ref{axioms_as_theorems}.
The validity of a theorem can be proven from the axioms that have already been declared.
@@ -158,7 +173,7 @@ The invariants are accumulated during refinements.
\label{seeing_a_context}
If the machine sees a context, the sets and constants declared in the context can be used in
all predicates and expressions.
-The conjunction of axioms $A(\allconstants)$ can be used as hypotheses in the proofs.
+The conjunction of axioms $A$ can be used as hypotheses in the proofs.
\subsubsection{Variables and invariants}
\label{variables_and_invariants}
@@ -169,11 +184,11 @@ We denote the variables of the abstract machines $M_1,\ldots,M_{n-1}$ with a $\a
\index{invariant}
An invariant is a statement that must be valid at each state of the machine.
-Each invariant $i$ consists of a label and a predicate $I_i(\allconstants,\absvariables,\concvariables)$.
+Each invariant $i$ consists of a label and a predicate $I_i$.
An invariant can refer to the constants as well as the variables of the concrete and all abstract machines.
-We write $\absinvariants$ to denote the conjunction of all invariants
-of the abstract machines and $\concinvariants$ for the conjunction of the concrete machine's invariant.
+We write $I$ to denote the conjunction of all invariants
+of the abstract machines and $J$ for the conjunction of the concrete machine's invariant.
Invariants that are marked as theorems derive their correctness from the preservation
of other invariants, so their preservation does not need to be proven.
@@ -233,16 +248,19 @@ parameters of the concrete event with $\concparameters$.
Similarly to variables, an event can have parameters in common with the event it refines.
If the refined event has a parameter $t$ which is not a parameter of the refinement,
- a witness $W_t(\allconstants,\allvariables,\concvariables',\concparameters,t)$ for
+ a witness $W_t$ for
the abstract parameter must be specified (\ref{witness}).
+All free identifiers in $W_t$ must be either constants, concrete or abstract variables, concrete
+ parameters or the abstract parameter $t$.
\paragraph{Guards}
\label{guards}
\index{guard}
-Each \emph{guard} consist of a label and a predicate $H(\allconstants,\concvariables,\concparameters)$.
+Each \emph{guard} consist of a label and a predicate $H$.
+All free identifiers in $H$ must be constants, concrete variables or concrete parameters.
Variables or parameters of abstract machines are not accessible in a guard.
-We write $G(\allconstants,\absvariables,\absparameters)$ for the conjunction of all guards of all abstract events.
+We write $G$ for the conjunction of all guards of all abstract events.
Like axioms and invariants, guards can also be marked as theorems.
The proof obligation can be found in Section \ref{guards_as_theorems}.
@@ -269,11 +287,11 @@ Let $x_1,\ldots,x_k$ be the variables that are assigned by any action of the eve
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
- $\bapred = Q_1 \land \ldots \land Q_n \land y_1 = y_1' \land \ldots \land y_l=y_l'$.
+ $\concbeforeafter = Q_1 \land \ldots \land Q_n \land y_1 = y_1' \land \ldots \land y_l=y_l'$.
Please note that Rodin optimizes proof obligations when a before-after-predicate is a hypothesis.
-$x'$ is replaced directly by $x$ when $x$ is not changed by the event and replaced by $E(\allconstants,\concvariables,\concparameters)$
- when $E(\allconstants,\concvariables,\concparameters)$ is assigned to $x$ deterministically.
+$x'$ is replaced directly by $x$ when $x$ is not changed by the event and replaced by $E$
+ when $E$ is assigned to $x$ deterministically.
\paragraph{Witnesses}
\label{witness}
@@ -289,27 +307,32 @@ If the user does not specify a witness, Rodin uses the default witness $\btrue$.
Witnesses are necessary in the following circumstances:
\begin{itemize}
\item The abstract event has a parameter $p$ that is not a parameter of the concrete event.
- In this case, the label of the witness must be $p$, and the witness has the form
- $W_p(\allconstants,\allvariables,\concvariables',\concparameters,p)$.
+ In this case, the label of the witness must be $p$, and the witness has the form $W_p$.
+ All identifiers of $W_p$ must be either constants, concrete or abstract variables,
+ primed concrete variables (i.e.~$v'$ for each concrete variable $v$),
+ concrete parameters or the abstract parameter $p$.
\item The abstract event assigns non-deterministically (using $\bcmin$ or $\bcmsuch$)
a value to a variable $x$ that is not a variable of the concrete machine.
- In this case, the label of the witness must be $x'$, the witness has the form
- $W_{x'}(\allconstants,\allvariables,\concvariables',\allparameters,x')$.
+ In this case, the label of the witness must be $x'$, the witness has the form $W_{x'}$.
+ All identifiers of $W_p$ must be either constants, concrete or abstract variables,
+ primed concrete variables (i.e.~$v'$ for each concrete variable $v$),
+ concrete parameters or the primed abstract variable $x'$.
+ $x'$ denotes the new value of $x$.
\end{itemize}
-We denote the conjunction of all witnesses of an event with $\witnesspred$.
+We denote the conjunction of all witnesses of an event with $W$.
\index{feasibility!of witnesses}
The feasibility of the witness must be proven, i.e. that there is actually a value for which the predicate holds.
\index{proof obligation!witness feasibility@witness feasibility (\eventbpo{WFIS})}
\pode{Witness feasibility for a parameter $p$}{\eventbpo{eventlabel/$p$/WFIS}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land \bapred \\
- \limp & \exists p \qdot W(\allconstants,\allvariables,\concvariables',\concparameters,p)
+ & A \land I \land J \land H \\
+ \limp & \exists p \qdot W_p
\end{array}$}
\pode{Witness feasibility for an abstract variable $x$}{\eventbpo{eventlabel/$x'$/WFIS}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land \bapred \\
- \limp & \exists x' \qdot W(\allconstants,\allvariables,\concvariables',\allparameters,x')
+ & A \land I \land J \land H \land \concbeforeafter \\
+ \limp & \exists x' \qdot W_{x'}
\end{array}$}
A witness may contain well-definedness conditions. See \ref{well_definedness_of_witnesses}
for the corresponding proof obligation.
@@ -339,33 +362,32 @@ If the event's guard is enabled, every action must be feasible.
\index{proof obligation!action feasibility@action feasibility (\eventbpo{FIS})}
\pode{Action feasibility}{\eventbpo{eventlabel/actionlabel/FIS}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants
- \land \absguards \land \concguards \\
- \limp & \actfis(a)
+ & A \land I \land J \land H \land W_p \land \absbeforeafter \\
+ \limp & \actfis(a)
\end{array}$}
-For each invariant $I_i$ with the label \eventbpo{invlabel}
+For each invariant $J_i$ with the label \eventbpo{invlabel}
that contains a variable affected by the assignment, it must be proven
that the invariant still is still valid for the new values.
+
\index{proof obligation!invariant preservation@invariant preservation (\eventbpo{INV})}
\pode{Invariant preservation}%
{\eventbpo{eventlabel/invlabel/INV}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants
- \land \absguards \land \concguards \\
- \limp & I_i(\allconstants,\allvariables')
+ & A \land I \land J \land H \land W_{v} \land \concbeforeafter \\
+ \limp & J_i[\absvariables'/\absvariables,\concvariables'/\concvariables]
\end{array}$}
Rodin simplifies this proof obligations by replacing $x'$ with $x$ for variables that are not
- changed and $x'$ by $E(\allconstants,\concvariables,\concparameters)$
+ changed and $x'$ by $E$
for variables that are assigned by a deterministic ($x \bcmeq E$) assignment.
\index{establishment of the invariant}
There are special proof obligations generated for the initialisation event:
\pode{Action feasibility (in the initialisation)}{\eventbpo{INITIALISATION/actionlabel/FIS}}%
- {$\axioms \limp \actfis(a)$}
+ {$A \land W \land \concbeforeafter \limp \actfis(a)$}
\pode{Invariant establishment}%
{\eventbpo{INITIALISATION/invlabel/INV}}%
- {$\axioms \limp I_i(\allconstants,\allvariables')$}
+ {$A \land W \land \concbeforeafter \limp I_i[\absvariables'/\absvariables,\concvariables'/\concvariables]$}
\subsubsection{Ensuring a correct refinement}
\label{refinement_proof_obligations}
@@ -390,29 +412,25 @@ proof obligation is generated:
\pode{Guard strengthening}%
{\eventbpo{eventname/guardlabel/GRD}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants
- \land \concguards \land \\
- & \witnesspred \land \bapred \\
- \limp & G_i(\allconstants,\absvariables,\absparameters)
+ & A \land I \land J \land H \land W_p \\
+ \limp & G_i
\end{array}$}
\paragraph{Action simulation}
\label{action_simulation}
-If an abstract event's action $i$ (with before-after predicate $Q_i(\allconstants,\absvariables,\absparameters,\absvariables')$)
+If an abstract event's action $i$ (with before-after predicate $Q_i$)
assigns a value to a variable that is also declared in the concrete machine,
it must be proven that the abstract event's behaviour
corresponds to the concrete behaviour.
-The behaviour of the concrete event is given by the concrete before-after-predicate $\bapred$, and
-the relevant abstract behaviour is given by the before-after-predicate $Q_i(\allconstants,\absvariables,\absparameters,\absvariables')$.
+The behaviour of the concrete event is given by the concrete before-after-predicate $\concbeforeafter$,
+and the relevant abstract behaviour is given by the before-after-predicate $Q_i$.
The relation between abstract and concrete event is specified by witnesses.
\index{proof obligation!action simulation@action simulation (\eventbpo{SIM})}
\pode{Action simulation}%
{\eventbpo{eventname/actionlabel/SIM}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants
- \land \concguards \land \\
- & \witnesspred \land \bapred \\
- \limp & Q_i(\allconstants,\absvariables,\absparameters,\absvariables')
+ & A \land I \land J \land H \land W \land \concbeforeafter \\
+ \limp & Q_i
\end{array}$}
When the assignments are deterministic or the witnesses are equations, the proof obligation can usually
be simplified by Rodin.
@@ -420,18 +438,15 @@ be simplified by Rodin.
\paragraph{Preserved variables}
\label{preserved_variables}
If $x$ is a variable of both the abstract and concrete machine and
- the concrete event assigns a value $x$ but the abstract event does not,
+ the concrete event assigns a value to $x$ but the abstract event does not,
it must be proven that the variable's value does not change.
-Let $Q_i(\allconstants,\concvariables,\concparameters,\concvariables')$ be the before-after-predicate
- of the action that changes $x$.
+Let $Q_i$ be the before-after-predicate of the action that changes $x$.
\index{proof obligation!equality of a preserved variable@equality of a preserved variable (\eventbpo{EQL})}
\pode{Equality of a preserved variable $x$}%
{\eventbpo{eventname/$x$/EQL}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants
- \land \concguards
- \land Q_i(\allconstants,\concvariables,\concparameters,\concvariables') \\
- \limp & x'=x
+ & A \land I \land J \land H \land Q_i \\
+ \limp & x'=x
\end{array}$}
\subsubsection{Merging events}
@@ -450,10 +465,8 @@ created with $G_1,\ldots,G_n$ as the abstract guards of the merged events
\index{proof obligation!merging events@merging events (\eventbpo{MRG})}
\pode{Guard strengthening (merge)}{\eventbpo{eventlabel/MRG}}%
{$\begin{array}{l@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land
- \concguards \land \\
- & \witnesspred \land \bapred \\
- \limp & G_1(\allconstants,\absvariables,\absparameters_1)\lor\ldots\lor G_n(\allconstants,\absvariables,\absparameters_n)
+ & A \land I \land J \land H \land W \land \concbeforeafter \\
+ \limp & G_1\lor\ldots\lor G_n
\end{array}
$}
The other proof obligations are the same as for refining a single event.
@@ -479,10 +492,11 @@ This is especially useful when additional features are gradually introduced
Event-B makes it possible to prove how an event will terminate.
Termination means that a chosen set of events are enabled only a finite number
of times before an event that is not marked as terminating occurs.
-To support proofs for termination, a \emph{variant} $V(\allconstants,\concvariables)$ can be specified in a model.
+To support proofs for termination, a \emph{variant} $V$ can be specified in a model.
+ All free identifiers in $V$ must be constants or concrete variables.
A variant is an expression that is either numeric
- ($V(\allconstants,\concvariables)\in\intg$) or
- a finite set ($V(\allconstants,\concvariables)\in\pow(\alpha)$,
+ ($V\in\intg$) or
+ a finite set ($V\in\pow(\alpha)$,
where $\alpha$ is an arbitrary type).
Events can be marked as:
@@ -514,43 +528,41 @@ The following other proof obligations are generated:
must only be enabled when the variant is non-negative.
\pode{Numeric variant is a natural number}{\eventbpo{eventlabel/NAT}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land
- \absguards \land \concguards \\
- \limp & V(\allconstants,\concvariables)\in\nat
+ & A \land I \land J \land G \land H \\
+ \limp & V\in\nat
\end{array}$}
A convergent event must decrease the variant
\pode{Decreasing of a numeric variant (convergent event)}{\eventbpo{eventlabel/VAR}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land \\
- & \absguards \land \concguards \land \bapred \\
- \limp & V(\allconstants,\concvariables')<V(\allconstants,\concvariables)
+ & A \land I \land J \land G \land H \land \concbeforeafter \\
+ \limp & V[\varlist{w}'/\varlist{w}]<V
\end{array}$}
and an anticipated event must not increase the variant.
\pode{Decreasing of a numeric variant (anticipated event)}{\eventbpo{eventlabel/VAR}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land \\
- & \absguards \land \concguards \land \bapred \\
- \limp & V(\allconstants,\concvariables')\leq V(\allconstants,\concvariables)
+ & A \land I \land J \land G \land H \land \concbeforeafter \\
+ \limp & V[\varlist{w}'/\varlist{w}]\leq V
\end{array}$}
\paragraph{Set variant}
\label{set_variant}
If the variant is a set t, it must be proven that the set is always finite:
\pode{Decreasing of a variant (anticipated event)}{\eventbpo{FIN}}%
- {$\axioms \land \absinvariants \land \concinvariants \limp \bfinite(V(\allconstants,\concvariables))$}
+ {$\begin{array}{r@{\ }l}
+ & A \land I \land J \\
+ \limp & \bfinite(V)
+ \end{array}$}
A convergent event must remove elements from the set
\pode{Decreasing of a set variant (convergent event)}{\eventbpo{eventlabel/VAR}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land \\
- & \absguards \land \concguards \land \bapred \\
- \limp & V(\allconstants,\concvariables')\subset V(\allconstants,\concvariables)
+ & A \land I \land J \land G \land H \land \concbeforeafter \\
+ \limp & V[\varlist{w}'/\varlist{w}]\subset V
\end{array}$}
and an anticipated event must not add elements.
\pode{Decreasing of a set variant (anticipated event)}{\eventbpo{eventlabel/VAR}}%
{$\begin{array}{r@{\ }l}
- & \axioms \land \absinvariants \land \concinvariants \land \\
- & \absguards \land \concguards \land \bapred \\
- \limp & V(\allconstants,\concvariables')\subseteq V(\allconstants,\concvariables)
+ & A \land I \land J \land G \land H \land \concbeforeafter \\
+ \limp & V[\varlist{w}'/\varlist{w}]\subseteq V
\end{array}$}
\subsection{Well-definedness proof obligations}
@@ -569,7 +581,7 @@ For an axiom $A_w$, $A_b$ denotes (the conjunction of) all axioms declared
the current context before the axiom in question.
\index{proof obligation!well-definedness of an axiom@well-definedness of an axiom (\eventbpo{WD})}
\pode{Well-definedness of an axiom}{\eventbpo{label/WD}}%
- {$A_b(\allconstants) \limp \wdl(A_w(\allconstants))$}.
+ {$A_b \limp \wdl(A_w)$}
\paragraph{Invariants}
\label{well_definedness_of_invariants}
@@ -577,8 +589,8 @@ For an invariant $J_w$, $J_b$ denotes (the conjunction of) all the model's
invariants declared before the theorem.
\index{proof obligation!well-definedness of an invariant@well-definedness of an invariant (\eventbpo{WD})}
\pode{Well-definedness of an invariant}{\eventbpo{label/WD}}%
- {$\axioms \land \absinvariants \land J_b(\allconstants,\absvariables,\concvariables)
- \limp \wdl(J_w(\allconstants,\absvariables,\concvariables))$}
+ {$A \land I \land J_b
+ \limp \wdl(J_w)$}
\paragraph{Guards}
\label{well_definedness_of_guards}
@@ -586,17 +598,15 @@ For an invariant $H_w$, $H_b$ denotes (the conjunction of) all the model's
invariants declared before the theorem.
\index{proof obligation!well-definedness of a guard@well-definedness of a guard (\eventbpo{WD})}
\pode{Well-definedness of a guard}{\eventbpo{eventname/guardlabel/WD}}%
- {$\axioms \land \absinvariants \land \concinvariants \land
- H_b(\allconstants,\concvariables,\concparameters)
- \limp \wdl(H_w(\allconstants,\concvariables,\concparameters))$}
+ {$A \land I \land J \land H_b
+ \limp \wdl(H_w)$}
\paragraph{Witnesses}
\label{well_definedness_of_witnesses}
A witness $W$ may contain well-definedness conditions.
\index{proof obligation!well-definedness of a witness@well-definedness of a witness (\eventbpo{WWD})}
\pode{Well-definedness of a witness}{\eventbpo{eventlabel/witnesslabel/WWD}}%
- {$\axioms \land \absinvariants \land \concinvariants \land
- \bapred
+ {$A \land I \land J \land \concbeforeafter
\limp \wdl(W)$}
\paragraph{Actions}
@@ -606,15 +616,14 @@ The assignment $a$ of each action with the label $\eventbpo{actionlabel}$ in
\index{proof obligation!well-definedness of an action@well-definedness in an action (\eventbpo{WD})}
\pode{Well-definedness of an action}%
{\eventbpo{eventlabel/actionlabel/WD}}%
- {$\axioms \land \absinvariants \land \concinvariants \land
- \absguards \land \concguards \limp \wdl(~a~)$}
+ {$A \land I \land J \land G \land H \limp \wdl(~a~)$}
\paragraph{Variants}
\label{well_definedness_of_variants}
-A variant $V(\allconstants,\concvariables)$ must be well-defined.
+A variant $V$ must be well-defined.
\index{proof obligation!well-definedness of a variant@well-definedness of a variant (\eventbpo{VWD})}
\pode{Well-definedness of a variant}{\eventbpo{VWD}}%
- {$\axioms \land \concinvariants \limp \wdl(V(\allconstants,\concvariables))$}
+ {$A \land J \limp \wdl(V)$}
\subsection{Theorems}
@@ -633,26 +642,23 @@ For an axiom $A_{thm}$, $A_b$ denotes (the conjunction of) all axioms declared
the current context before the axiom in question.
\index{proof obligation!axiom as theorem@axiom as theorem (\eventbpo{THM})}
\pode{An axiom as theorem}{\eventbpo{label/THM}}%
- {$A_b(\allconstants) \limp A_{thm}(\allconstants)$}
+ {$A_b \limp A_{thm}$}
\paragraph{Invariants}
\label{invariants_as_theorems}
-For an invariant $I_{thm}$, $I_b$ denotes (the conjunction of) all the model's
+For an invariant $J_{thm}$, $J_b$ denotes (the conjunction of) all the model's
invariants declared before the theorem.
\index{proof obligation!invariant as theorem@invariant as theorem (\eventbpo{THM})}
\pode{An invariant as theorem}{\eventbpo{label/THM}}%
- {$\axioms \land \absinvariants \land I_b(\allconstants,\absvariables,\concvariables)
- \limp I_{thm}(\allconstants,\absvariables,\concvariables)$}
+ {$A \land I \land J_b \limp J_{thm}$}
\paragraph{Guards}
\label{guards_as_theorems}
-For an invariant $H_{thm}$, $H_b$ denotes (the conjunction of) all the event's
+For a guard $H_{thm}$, $H_b$ denotes (the conjunction of) all the event's
guards declared before the theorem.
\index{proof obligation!guard as theorem@guard as theorem (\eventbpo{THM})}
\pode{A guard as theorem}{\eventbpo{label/THM}}%
- {$\axioms \land \absinvariants \land \concinvariants \land
- H_b(\allconstants,\concvariables,\concparameters)
- \limp H_{thm}(\allconstants,\concvariables,\concparameters)$}
+ {$A \land I \land J \land H_b \limp H_{thm}$}
\subsection{Generated proof obligations}
\label{generated_proof_obligations}
@@ -673,10 +679,14 @@ For an invariant $H_{thm}$, $H_b$ denotes (the conjunction of) all the event's
\index{NAT (natural number proof obligation)}
\index{VAR (decreasing of variant proof obligation)}
-This is a brief overview about the different proof obligations that are generated.
-The user can use this table to identify a specific proof obligation. For further information, a link to the relevant reference section is provided.
+Table \ref{tab:generated_pos} shows
+ a brief overview about the different proof obligations that are generated.
+The user can use this table to identify a specific proof obligation. For further information,
+a reference to the relevant reference section is provided.
-\begin{tabular}{lll}
+\begin{table}
+ \centering
+\begin{tabular}{p{0.4\textwidth}ll}
\hline
\multicolumn{3}{l}{\textbf{generated in contexts}} \\
well-definedness of an axiom & \eventbpo{label/WD} & \ref{well_definedness_of_axioms} \\
@@ -692,8 +702,8 @@ The user can use this table to identify a specific proof obligation. For further
invariant preservation & \eventbpo{event/invariantlabel/INV} & \ref{consistency_proof_obligations} \\
\hline
\multicolumn{3}{l}{\textbf{generated for refinements}} \\
- guard strengthening & \eventbpo{event/abstract\_guard\_label/GRD} & \ref{guard_strengthening} \\
- action simulation & \eventbpo{event/abstract\_action\_label/SIM} & \ref{action_simulation} \\
+ guard strengthening & \eventbpo{event/abstract\_grd\_label/GRD} & \ref{guard_strengthening} \\
+ action simulation & \eventbpo{event/abstract\_act\_label/SIM} & \ref{action_simulation} \\
equality of a preserved variable & \eventbpo{event/variable/EQL} & \ref{preserved_variables} \\
guard strengthening (merge) & \eventbpo{event/MRG} & \ref{merging_events} \\
well definedness of a witness & \eventbpo{event/identifier/WWD} & \ref{well_definedness_of_witnesses} \\
@@ -705,7 +715,10 @@ The user can use this table to identify a specific proof obligation. For further
natural number for a numeric variant & \eventbpo{event/NAT} & \ref{numeric_variant} \\
decreasing of variant & \eventbpo{event/VAR} &\ref{numeric_variant} \\
\hline
-\end{tabular}
+\end{tabular}
+ \caption{Generated Proof Obligations}
+ \label{tab:generated_pos}
+\end{table}
\subsection{Visibility of identifiers}
\label{visibility_of_identifiers}
@@ -715,10 +728,10 @@ Expressions and predicates are comprised of certain Event-B elements. The follow
\begin{center}
\newcommand{\markcell}{$\times$}
- \begin{tabular}{lcccccc}
+ \begin{tabular}{l*{6}{@{\hspace{0.8em}}c}}
\hline
- & & & concrete & abstract & concrete & abstract \\
- & sets & constants & variables & variables & parameters & parameters \\
+ & sets & constants & \multicolumn{2}{c}{variables} & \multicolumn{2}{c}{parameters} \\
+ & & & concrete & abstract & concrete & abstract \\
\hline
axiom & \markcell & \markcell & & & & \\
invariant & \markcell & \markcell & \markcell & \markcell & & \\
diff --git a/org.rodinp.handbook.feature/latex/reference-03.tex b/org.rodinp.handbook.feature/latex/reference-03.tex
index 7fb1f3046be509c22c13d46535447034187ef3cc..1f54367e9a0ee7547d81cdcaa63e2ab25ae693a1 100644
--- a/org.rodinp.handbook.feature/latex/reference-03.tex
+++ b/org.rodinp.handbook.feature/latex/reference-03.tex
@@ -59,7 +59,7 @@ For an expression $\vexpr{E}$, we write $\expre\in\alpha$ to state that $\expre$
In the following descriptions of Event-B's mathematical constructs, we will describe the
types of all constructs and their components.
-For example, we will describe the maplet $\expre\mapsto \exprf$ which is defined as $\expre\mapsto \exprf\in\alpha\cprod\beta$ with
+For example, we will describe the maplet $\expre\mapsto \exprf$ whose type is defined by $\expre\mapsto \exprf\in\alpha\cprod\beta$ with
$\expre\in\alpha$ and $\exprf\in\beta$. We do not restrict the types of $\alpha$ and $\beta$.
For predicates, we simply describe the data types of their components.
@@ -93,7 +93,8 @@ In many cases, this is just the conjunction of the well-definedness conditions f
Free identifiers in predicates and expressions are those identifiers which are used but not introduced by quantifiers.
More formally, we define the set of free identifiers $\freeids{\expre}$ of an expression or predicate $E$ recursively as follows:
-\begin{tabular}{|l|l|}
+\begin{center}
+\begin{tabular}{ll}
\hline
\textbf{Expression / Predicate} & \textbf{Free identifiers} \\
\hline
@@ -109,9 +110,10 @@ More formally, we define the set of free identifiers $\freeids{\expre}$ of an ex
& $\emptyset$ \\
\hline
$\begin{array}{lllll}
- \lnot \expra & \bool(\expra) & \pow(\expra) & \pow_1(\expra) & \bfinite(\expra) \\
- \card(\expra) & \bunaryunion(\expra) & \bunaryinter(\expra) & \expra^{-1} & \dom(\expra) \\
- \ran(\expra) & -\expra & \min(\expra) & \max(\expra)
+ \lnot \expra & \bool(\expra) & \pow(\expra) & \pow_1(\expra) \\
+ \bfinite(\expra) & \card(\expra) & \bunaryunion(\expra) & \bunaryinter(\expra) \\
+ \expra^{-1} & \dom(\expra) & \ran(\expra) & -\expra \\
+ \min(\expra) & \max(\expra)
\end{array}$
& $\freeids{\expra}$ \\
\hline
@@ -154,7 +156,8 @@ More formally, we define the set of free identifiers $\freeids{\expre}$ of an ex
\end{array}$
& $\freeids{\predp}\setminus\freeids{\expre}$\\
\hline
-\end{tabular}
+\end{tabular}
+\end{center}
\subsubsection{Structure of the subsections}
The following reference subsections will have the form the form: \\[2em]
@@ -1252,31 +1255,28 @@ The following reference subsections will have the form the form: \\[2em]
\end{rrnames}
\begin{rodinrefentry}
\rrdesc
- $x_1,\ldots,x_n \bcmsuch Q(x_1',\ldots,x_n')$
+ $x_1,\ldots,x_n \bcmsuch Q$
assigns any value to the variables $x_1\ldots,x_n$ such that the the
before-after-predicate $Q$ is fulfilled.
Each $x_i$ is an identifier that refers to a variable of the concrete machine.
- %$\allconstants,\concvariables,\concparameters$ represent the sequence of all constants,
- %variables of the concrete machine and parameters of the concrete event.
- %$x_1,\ldots,x_n$ are in $\concvariables$.
- We write $Q(x_1',\ldots,x_n')$ to emphasise the fact that the identifiers $x_1',\ldots,x_n'$
-%can be used additionally to the constants
- can also be used for the constants, concrete variables and parameters in the predicate $Q$.
+
+ All free identifiers in $Q$ must be constants, concrete parameters,
+ concrete variables or primed versions of the modified variables ($x_1',\ldots,x_n'$).
This is the most general form of assignment. All other assignments can be converted to this.
\rrdef
- The before-after-predicate is $Q(x_1',\ldots,x_n')$.
+ The before-after-predicate is $Q$.
\rrtypes
- $Q(x_1',\ldots,x_n')$ is a predicate and all $x_i$ and $x'_i$ must have the same type:
+ $Q$ is a predicate and all $x_i$ and $x'_i$ must have the same type:
$x_1\in\alpha_i$ and $x'_1\in\alpha_i$ for $i\in 1\upto n$.
\rrwd
- $\wdl(~x_1,\ldots,x_n \bcmsuch Q(x_1',\ldots,x_n')~)
+ $\wdl(~x_1,\ldots,x_n \bcmsuch Q~)
\quad\defi\quad
- \wdl(x_1,\ldots,x_n \bcmsuch Q(x_1',\ldots,x_n'))$
+ \forall x_1',\ldots,x_n' \qdot \wdl(~Q~)$
\rrfis
- $\actfis(~x_1,\ldots,x_n \bcmsuch Q(x_1',\ldots,x_n')~)
- \quad\defi\quad
- \exists x_1',\ldots,x_n' ~\qdot~ Q(x_1',\ldots,x_n')$
+ $\actfis(~x_1,\ldots,x_n \bcmsuch Q(x_1',\ldots,x_n')~)$ \\
+ $\quad\defi\quad$
+ $\exists x_1',\ldots,x_n' ~\qdot~ Q(x_1',\ldots,x_n')$
\end{rodinrefentry}
\end{samepage}
@@ -1293,8 +1293,8 @@ The following reference subsections will have the form the form: \\[2em]
$x \bcmin \expre$ assigns any value of the
set $\expre$ to the variable $x$. $x$ is an identifier that refers to a variable
of the concrete machine.
- %$\allconstants,\concvariables,\concparameters$ represent the sequence of all constants,
- %variables of the concrete machine and parameters of the concrete event.
+
+ All free identifiers in $E$ must be constants, concrete variables or concrete parameters.
\rrdef
The before-after-predicate is $x' \in \expre$. \\
The assignment is equivalent to
diff --git a/org.rodinp.handbook.feature/latex/reference-04.tex b/org.rodinp.handbook.feature/latex/reference-04.tex
index b283249cfc66368c48ac7591b7acdea4ee20df71..ab4ad1090155e8acaf7d6b77fe153cd3ad8faae6 100644
--- a/org.rodinp.handbook.feature/latex/reference-04.tex
+++ b/org.rodinp.handbook.feature/latex/reference-04.tex
@@ -277,7 +277,7 @@ Firstly, the proof purger tries to find obsolete proofs in the selection. If no
\begin{figure}[h!t]
\begin{center}
- \includegraphics{img/reference/ref_10_proof_purger.png}
+ \includerodinimg{reference/ref_10_proof_purger.png}
\caption{Proof Purger Selection Window}
\label{fig_ref_10_proof_purger}
\end{center}
diff --git a/org.rodinp.handbook.feature/latex/rodin-doc.tex b/org.rodinp.handbook.feature/latex/rodin-doc.tex
index 4e03501180c30081149345888bb5fb574e76d349..9c1294a3fb400440e6d746dc9c828b75c1a9bde0 100644
--- a/org.rodinp.handbook.feature/latex/rodin-doc.tex
+++ b/org.rodinp.handbook.feature/latex/rodin-doc.tex
@@ -1,3 +1,17 @@
+\ifdefined\isinprint
+\documentclass[10pt]{book}
+\usepackage[paperwidth=155.93mm,paperheight=233.89mm]{geometry}
+\usepackage[colorlinks=false,
+ pdfborder={0 0 0}
+ pdftex,
+ plainpages=false,
+ pdfauthor={Michael Jastram (Ed.)},
+ pdftitle={Rodin User's Handbook},
+ pdfsubject={Rodin is a platform for Event-B based formal modelling},
+ pdfkeywords={Rodin, Event-B},
+ pdfproducer={http://handbook.event-b.org},
+ pdfcreator={plastex-based tool chain}]{hyperref}
+\else
\documentclass[12pt]{book}
\usepackage[left=2.5cm,top=3cm,right=2.5cm,bottom=3cm]{geometry}
\usepackage[colorlinks=true,
@@ -9,6 +23,7 @@
pdfkeywords={Rodin, Event-B},
pdfproducer={http://handbook.event-b.org},
pdfcreator={plastex-based tool chain}]{hyperref}
+\fi
\usepackage{graphicx}
\usepackage{bsymb}
\usepackage{b2latex}
@@ -39,29 +54,27 @@ Handbook $ $Rev$ $ \\
\else
\begin{titlepage}
\AddToShipoutPicture*{\BackgroundPic}
-\vspace*{14.5cm}
-{\fontsize{70}{85}\selectfont \bfseries Rodin}
-
-\vspace*{0.2cm}
-{\fontsize{24.5}{30}\selectfont \bfseries User's Handbook}
+\vspace*{\titletop}
+{\titledimrodin\selectfont \bfseries Rodin}
-\vspace*{1cm}
-{\fontsize{16}{19}\selectfont \textbf{\textsf{Covers Rodin v.\versionnr}}}
+\vspace*{\titlesubtitledistance}
+{\titledimhandbook\selectfont \bfseries User's Handbook}
-\vspace*{1cm}
-{\fontsize{16}{19}\selectfont \textsf{Michael Jastram (Ed.)}}
+\vspace*{\titlesecdistance}
+{\titledimsubtext\selectfont \textbf{\textsf{Covers Rodin v.\versionnr}}}
-\vspace*{0.2cm}
-{\fontsize{16}{19}\selectfont \textsf{Foreword by Prof. Michael Butler}}
+\vspace*{\titlesecdistance}
+{\titledimsubtext\selectfont \textsf{Michael Jastram (Ed.)}}
-\vspace*{1cm}
-\includegraphics[width=12mm]{img/deploy-logo.png}
+\vspace*{\titlesubtitledistance}
+{\titledimsubtext\selectfont \textsf{Foreword by Prof. Michael Butler}}
-\vspace*{-8.4mm}
-\hspace*{12mm}
-{ \fontsize{11}{15}\selectfont \textsf{This work is sponsored by the Deploy Project}}
+\vspace*{\titlesecdistance}
+{\titledimsponsor\selectfont %
+ $\vcenter{\hbox{\includegraphics[height=4ex]{img/deploy-logo.png}}}$
+ \textsf{This work is sponsored by the Deploy Project}}
-\vspace*{-22mm}
+\vspace*{\titlebottom}
\end{titlepage}
\phantomsection
@@ -145,7 +158,9 @@ The handbook is stored in the Rodin SVN repository and is authored in \LaTeX. C
Each page of the online version also has a feedback button, where feedback can be left using an online form. This feedback will be processed on a regular basis by volunteers.
-There is also a mailing list for handbook authors at \texttt{rodin-b-sharp-handbook@lists.\-sourceforge.net}.
+There is also a mailing list for handbook authors at
+\ifinprint \\ \fi
+\texttt{rodin-b-sharp-handbook@lists.\-sourceforge.net}.
You can also submit feedback via email to \texttt{rodin-hand\-book@formal\-mind.com}.
diff --git a/org.rodinp.handbook.feature/latex/style-guide.tex b/org.rodinp.handbook.feature/latex/style-guide.tex
index 92050042c545ba594e2373c756d5792303e1320b..f97b86add4698faf465bb967d1700babf450e83b 100644
--- a/org.rodinp.handbook.feature/latex/style-guide.tex
+++ b/org.rodinp.handbook.feature/latex/style-guide.tex
@@ -129,7 +129,7 @@ The \LaTeX-command to do this is \verb#\index{#\textit{word}\verb#}#.
\subsubsection{Contributions from Plugin Developers}
\label{sec:plugin_contributions}
-\begin{rodin-plugin}{img/prob.png}{ProB}
+\begin{rodin-plugin}{prob.png}{ProB}
We want to encourage Plugin developers to contribute to the Handbook, but we have to make it clear that we cannot maintain that documentation. Therefore, it has to be clearly marked. We use a custom environment for that purpose that
(1) provides the Plugin's icon, (2) adds a disclaimer to the end of the custom documentation and (3) puts the content into a gray box (like this one).
diff --git a/org.rodinp.handbook.feature/latex/tutorial-02.tex b/org.rodinp.handbook.feature/latex/tutorial-02.tex
index 1d55d728bb1bdb536284a901155ea93a36b5fadb..8248e460d880a094882b6bd13ae8a2b0cf0fcd0a 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-02.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-02.tex
@@ -38,7 +38,7 @@ After dismissing the welcome screen, you should see the window shown in Figure \
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_02_install1.png}
+ \includerodintwimg{0.7}{tutorial/tut_02_install1.png}
\caption{Eclipse Workspace Launcher}
\label{fig_tut_02_workspace_launcher}
\end{center}
@@ -50,7 +50,7 @@ After specifying a path click the \textsf{OK} button. Rodin will start and the w
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_02_install2.png}
+ \includerodintwimg{1.0}{tutorial/tut_02_install2.png}
\caption{Rodin GUI}
\label{fig_tut_02_rodin_gui}
\end{center}
@@ -79,9 +79,14 @@ Open the Install Manager \textsf{Help $\rangle$ Install New Software\ldots}. Cli
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_02_install3.png}
+ \includerodintwimg{1.0}{tutorial/tut_02_install3.png}
\caption{Eclipse Install Manager}
\label{fig_tut_02_install_manager}
\end{center}
\end{figure}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rodin-doc"
+%%% End:
diff --git a/org.rodinp.handbook.feature/latex/tutorial-03.tex b/org.rodinp.handbook.feature/latex/tutorial-03.tex
index 7b9b5bf640a56a78ce4bece3f6f8ef99ca404735..8704d03df388f2f03cd3194be80a59d141461812 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-03.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-03.tex
@@ -11,7 +11,7 @@ In this tutorial, we will create a model of a traffic light controller. We will
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_trafficlight.png}
+ \includerodintwimg{1.0}{tutorial/tut_03_trafficlight.png}
\caption{The traffic light controller}
\label{fig_tut_03_traffic_light}
\end{center}
@@ -40,7 +40,7 @@ Models typically consist of multiple files that are managed in a project. Creat
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_tutorial-3.png}
+ \includerodinimg{tutorial/tut_03_tutorial-3.png}
\caption{New Event-B Project Wizard}
\label{fig_tut_03_new_project_wizard}
\end{center}
@@ -54,7 +54,7 @@ Next, create a new Event-B Component. Either use \textsf{File $\rangle$ New $\r
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_mac.png}
+ \includerodinimg{tutorial/tut_03_mac.png}
\caption{New Event-B Component Wizard}
\label{fig_tut_03_new_component_wizard}
\end{center}
@@ -68,7 +68,7 @@ You can also edit the machine using the Event-B Machine Editor. This was the def
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics[]{img/tutorial/tut_03_interface.png}
+% \includerodinimg{tutorial/tut_03_interface.png}
%\end{center}
%\end{figure}
@@ -80,7 +80,7 @@ This editor is \textit{form-based}. This means that it can be modified by using
\label{tut_camille}
\index{editor!Camille text editor}
-\begin{rodin-plugin}{img/camille.png}{Camille}
+\begin{rodin-plugin}{camille.png}{Camille}
Camille is a ``real'' text editor that provides the same feel as a typical Eclipse text editor and provides all of the functions that most text editors provide (i.e. copy, paste, undo, redo, etc.) However, please note that at this time not all Rodin plugins are compatible with Camille. For more information, please consult the extensive documentation in the Rodin Wiki (\ref{rodin_wiki}).
Camille can be installed via its update site, which is preconfigured in Rodin. Once installed, Camille will be set as the default editor. The rodin editor or structural editor can still be used by selecting it from the context menu of a file in the project browser.
@@ -114,7 +114,7 @@ Create the second variable (\texttt{peds\_go}) in the same way, or place your cu
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics[]{img/tutorial/tut_03_new-variable.png}
+% \includerodinimg{tutorial/tut_03_new-variable.png}
%\end{center}
%\end{figure}
@@ -122,7 +122,7 @@ Upon saving, the variables will be underlined in red which indicates that an err
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_error_neweditor.png}
+ \includerodintwimg{1.0}{tutorial/tut_03_error_neweditor.png}
\caption{Red highlighted elements indicate errors}
\label{fig_tut_03_error}
\end{center}
@@ -136,7 +136,7 @@ Event-B provides the build-in datatype \texttt{BOOL} among others (\ref{data_typ
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics[width=0.7\textwidth]{img/tutorial/tut_03_invariants.png}
+% \includerodintwimg{0.7}{tutorial/tut_03_invariants.png}
%\end{center}
%\end{figure}
@@ -149,7 +149,7 @@ After saving, you should see that the \textsf{INITIALISATION} event is underline
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_yellow_neweditor.png}
+ \includerodintwimg{1.0}{tutorial/tut_03_yellow_neweditor.png}
\caption{Yellow highlighted elements indicate warnings}
\label{fig_tut_03_warning}
\end{center}
@@ -161,7 +161,7 @@ To fix this problem, place your cursor to the left of the small green arrow next
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics[]{img/tutorial/tut_03_events.png}
+% \includerodinimg{tutorial/tut_03_events.png}
%\end{center}
%\end{figure}
@@ -258,7 +258,7 @@ To prevent the invariant from being violated (and therefore to allow all proof o
\subsubsection{Finding Invariant Violations with ProB}
\label{tut:prob}
\index{ProB}
-\begin{rodin-plugin}{img/prob.png}{ProB}
+\begin{rodin-plugin}{prob.png}{ProB}
A useful tool for understanding and debugging a model is a model checker like ProB. You can install ProB directly from Rodin by using the ProB Update Site. Just select \textsf{Install New Software...} from the \textsf{Help} menu and select ``ProB'' from the dropdown. You should see ``ProB for Rodin2`` as an installation option, which you can then install using the normal Eclipse mechanism.
We will continue the example at the point where we added the safety invariant (REQ-1), but didn't add guards yet to prevent the invariants from being violated.
@@ -269,7 +269,7 @@ We launch ProB by right-clicking on the machine we'd like to animate and select
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_prob_perspective.png}
+ \includerodintwimg{1.0}{tutorial/tut_03_prob_perspective.png}
\caption{The ProB Perspective}
\label{fig_tut_prob_perspective}
\end{center}
@@ -277,7 +277,7 @@ We launch ProB by right-clicking on the machine we'd like to animate and select
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_03_prob_invariant_violation.png}
+ \includerodintwimg{1.0}{tutorial/tut_03_prob_invariant_violation.png}
\caption{An invariant violation, found by ProB}
\label{tut_03_prob_invariant_violation}
\end{center}
diff --git a/org.rodinp.handbook.feature/latex/tutorial-04.tex b/org.rodinp.handbook.feature/latex/tutorial-04.tex
index c91770c7c483479373de48dd94b7f182de483e30..b7a23a54125a544cb860d1bbd699a21b45304b6c 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-04.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-04.tex
@@ -1,3 +1,4 @@
+\newcommand{\dascii}[1]{\textrm{ASCII: } \texttt{#1}}
\newcommand{\lascii}[1]{\qquad\quad \textrm{ASCII: } \texttt{#1}}
\newcommand{\inascii}[1]{(ASCII: \texttt{#1})}
@@ -36,7 +37,8 @@ When a variable is introduced by a quantifier, the type of the variable must be
$a$ and $b$ could be integers, Boolean values or some other type.
In this case, we must make the type of the variables explicit by stating that $a$ and $b$ are elements
of the appropriate sets. Let's use integers again to correct the previous expression:
-\[ \forall a,b \qdot a\in\intg \land b\in\intg \land a\neq b \limp b\neq a \lascii{!a,b.\ a:INT \& b:INT \& a/=b => b/=a} \]
+\[ \forall a,b \qdot a\in\intg \land b\in\intg \land a\neq b \limp b\neq a\]
+\[ \dascii{!a,b.\ a:INT \& b:INT \& a/=b => b/=a} \]
The conjunction operator ($\land$) has a stronger binding that the implication $\limp$, so the above expression is equivalent to
\[ \forall a,b \qdot (a\in\intg \land b\in\intg \land a\neq b) \limp b\neq a\]
@@ -71,7 +73,7 @@ give an overview about all types you might encounter.
\index{Boolean!as type}
\index{data type!Boolean}
We have already seen the Boolean type ($\Bool$) in the previous section (\ref{tut_first_machine}).
- It has exactly two elements, $\Bool = \{\True,\False\}$.
+ It has exactly two elements, $\Bool = \{\True,$ $\False\}$.
\item[Carrier sets]
\index{carrier set}
\index{data type!carrier set}
@@ -151,7 +153,8 @@ Additionally, we have to say that $working$ and $broken$ are not the same by $wo
If the enumerated sets gets larger, we need to state for every two element of the set that they are
distinct. Thus, for a set of 10 constants, we'll need $(10^2-10)\div 2 = 45$ predicates.
-Again, we can use the partition operator to express this in a more concise way: $partition(STATUS,\{working\},\{broken\})$.
+Again, we can use the partition operator to express this in a more concise way:
+\[partition(STATUS,\{working\},\{broken\})\]
\subsection{Relations}
\label{tut_relations}
diff --git a/org.rodinp.handbook.feature/latex/tutorial-05.tex b/org.rodinp.handbook.feature/latex/tutorial-05.tex
index 712303bb80ea292d487f1682f6f30c7f5a96a55d..bac5a16dc7a3f869a6694d617ff70f6b82f7c7ce 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-05.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-05.tex
@@ -25,7 +25,7 @@ Next, create a new Event-B Component. The process for creating a context is simi
%\begin{figure}[h!t]
%\begin{center}
-% \includegraphics{img/tutorial/tut_05_agatha1.png}
+% \includerodinimg{tutorial/tut_05_agatha1.png}
% \caption{New Event-B Component Wizard}
% \label{fig_tut_05_new_component}
%\end{center}
@@ -35,7 +35,7 @@ Click the \textsf{Finish} button. Rodin should start the editor with the created
\begin{figure}[h!t]
\begin{center}
- \includegraphics{img/tutorial/tut_05_agatha2_neweditor.png}
+ \includerodintwimg{1.0}{tutorial/tut_05_agatha2_neweditor.png}
\caption{Context file opened with Rodin Editor}
\label{fig_tut_05_context_file}
\end{center}
@@ -80,7 +80,7 @@ Now the constants themselves are not very useful since they have no type (after
\begin{description}
\AXIOMS
\begin{description}
- \nItemX{ person\_partition }{ partition(persons, \{ Agatha\} , \{ butler\} , \{ Charles\} ) }
+ \nItemX{ person\_partition }{ \\ partition(persons, \{ Agatha\} , \{ butler\} , \{ Charles\} ) }
\end{description}
\end{description}
}
@@ -219,7 +219,7 @@ All axioms are set to ``not theorem'' when they are created. But we need the sol
\begin{figure}[h!t]
\begin{center}
- \includegraphics{img/tutorial/tut_05_agatha3_neweditor.png}
+ \includerodinimg{tutorial/tut_05_agatha3_neweditor.png}
\caption{Mark an Axiom as Theorem}
\label{fig_tut_05_mark_theorem}
\end{center}
@@ -232,8 +232,8 @@ Thus Rodin generates a proof obligation called \eventbpo{solution/THM}.
However, at this point of the tutorial we do not want to go into more detail about proving yet.
\index{ProB}
-\begin{rodin-plugin}{img/prob.png}{ProB}%
- You can use ProB to animate contexts, too. Just right-click on the context in the explorer and select \textsf{Start Animation / Model Checking}. If ProB finds solutions for the specified constants that fulfil the axioms, an event ``\texttt{SETUP\_CONTEXT}'' is enabled that assigns values to the constants. In our example, ProB should find a solution where Agatha is the murder. You can actually inspect the axioms and the theorem in the state view to see why they are fulfilled.
+\begin{rodin-plugin}{prob.png}{ProB}%
+ You can use ProB to animate contexts, too. Just right-click on the context in the explorer and select \textsf{Start Animation / Model Checking}. If ProB finds solutions for the specified constants that fulfil the axioms, an event ``\texttt{SETUP\_CONTEXT}'' is enabled that assigns values to the constants. In our example, ProB should find a solution where Agatha is the murderer. You can actually inspect the axioms and the theorem in the state view to see why they are fulfilled.
\end{rodin-plugin}
This concludes the tutorial about contexts. The following section shows the complete Context.
@@ -261,17 +261,18 @@ This concludes the tutorial about contexts. The following section shows the comp
\nItemX{ person\_partition }{ partition(persons, \{ Agatha\} , \{ butler\} , \{ Charles\} ) }
\nItemX{ hate\_relation }{ hates \in persons \rel persons }
\nItemX{ richer\_relation }{ richer \in persons \rel persons \land
- \\\hspace*{3,4 cm} richer \binter id = \emptyset \land
- \\\hspace*{3,4 cm} (\forall x,y,z \qdot ( x\mapsto y\in richer \land y\mapsto z\in richer)
- \\\hspace*{4,4 cm}\limp x\mapsto z\in richer) \land
- \\\hspace*{3,4 cm} (\forall x,y \qdot x\in persons \land y\in persons \land x\neq y
- \\\hspace*{4,4 cm}\limp (x\mapsto y\in richer \leqv y\mapsto x \notin richer)) }
+ \\\hspace*{2.5 cm} richer \binter id = \emptyset \land
+ \\\hspace*{2.5 cm} (\forall x,y,z \qdot ( x\mapsto y\in richer \land y\mapsto z\in richer)
+ \\\hspace*{3.2 cm}\limp x\mapsto z\in richer) \land
+ \\\hspace*{2.5 cm} (\forall x,y \qdot x\in persons \land y\in persons \land x\neq y
+ \\\hspace*{3.2 cm}\limp (x\mapsto y\in richer \leqv y\mapsto x \notin richer)) }
\nItemX{ killer\_type }{ killer \in persons }
\nItemX{ killer\_hates }{ killer \mapsto Agatha \in hates }
\nItemX{ killer\_not\_richer }{ killer \mapsto Agatha \notin richer }
\nItemX{ charles\_hates }{ hates[\{ Agatha\} ] \binter hates[\{ Charles\} ] = \emptyset }
\nItemX{ agatha\_hates }{ hates[\{ Agatha\} ] = persons \setminus \{ butler\} }
- \nItemX{ butler\_hates\_1 }{ \forall x\qdot ( x\mapsto Agatha \notin richer \limp butler\mapsto x \in hates) }
+ \nItemX{ butler\_hates\_1 }{ \forall x\qdot ( x\mapsto Agatha \notin richer
+ \\\hspace*{3.5 cm}\limp butler\mapsto x \in hates) }
\nItemX{ butler\_hates\_2 }{ hates[\{ Agatha\} ] \subseteq hates[\{ butler\} ] \land
\\\hspace*{3,2 cm} (\forall x\qdot x\in persons \limp hates[\{ x\} ] \neq persons) }
\nItemX{ noone\_hates\_everyone }{ \forall x \qdot x \in persons \land hates[\{ x\} ] \neq persons }
diff --git a/org.rodinp.handbook.feature/latex/tutorial-07.tex b/org.rodinp.handbook.feature/latex/tutorial-07.tex
index 1e46ece9df8412a31922a157a28392ad47bbd7b3..66b951bfd6133e4143a1b9cd0880be50e1c2f46f 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-07.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-07.tex
@@ -1,4 +1,4 @@
-\section{Expanding the Traffic Light System: Contexts and Refinement}
+\section[Contexts and Refinement]{Expanding the Traffic Light System:\\ Contexts and Refinement}
\label{tut_expanding_traffic_light_system}
\tick{\textbf{Goals:} We apply what we learned in the previous section by introducing a context with traffic light colours and a refinement to integrate them. We will also introduce another refinement for the push buttons.}
@@ -12,7 +12,7 @@ We will introduce data refinement in this section. The objective is to create a
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tl-colors.png}
+ \includerodintwimg{0.7}{tutorial/tl-colors.png}
\caption{Mapping between Abstract and Concrete Events}
\label{fig_tut_07_tl_colours}
\end{center}
@@ -134,7 +134,7 @@ In its current state, this gluing invariant can be violated: if the event \texts
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/undischarged1.png}
+ \includerodinimg{tutorial/undischarged1.png}
\caption{Mapping between Abstract and Concrete Events}
\label{fig_tut_07_undischarged}
\end{center}
@@ -144,7 +144,7 @@ To fix this, we have to modify the two events in question. Let's start with \te
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_07_event_refinement.png}
+ \includerodinimg{tutorial/tut_07_event_refinement.png}
\caption{Switch from extended to not extended}
\label{fig_tut_07_event_refinement}
\end{center}
@@ -159,6 +159,7 @@ Once all references to \textsf{peds\_go} have been replace, we can remove the va
\warning{If you get the error message ``Identifier peds\_go has not been declared'', then there are references to the refined variable left somewhere in the model. %It can be helpful to use the \textsf{Pretty Print} view, as it will show the ``inherited'' elements from the abstract machine as well.
}
+\ifinprint\pagebreak\fi %TODO: remove this
\subsection{The refined machine with data refinement for peds\_go}
\label{tut_refined_machine}
diff --git a/org.rodinp.handbook.feature/latex/tutorial-08.tex b/org.rodinp.handbook.feature/latex/tutorial-08.tex
index 8d83677e0a1fa1a055868c04c12d72acbc803930..ea7a74f0404649c5438417b9f97d846f2c72b1e8 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-08.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-08.tex
@@ -9,6 +9,7 @@
In this section, we will work with the model of the so-called celebrity problem.
+\ifinprint\pagebreak\fi %TODO: remove this
\warning{We are using a new model instead of the traffic light because it provides us with some proofs where manual interaction is necessary.}
In the setting for this problem, we have a ``knows'' relation between persons.
@@ -36,7 +37,7 @@ It will take a few seconds for Rodin to extract and load all the files. Once thi
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_08_rodin_problems.png}
+ \includerodintwimg{1.0}{tutorial/tut_08_rodin_problems.png}
\caption{Warnings in the Rodin Problems View}
\label{fig_tut_08_rodin_problemview}
\end{center}
@@ -335,7 +336,7 @@ In this section, we will carry out proofs for the model of the Celebrity Problem
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_08_switch_perspective.png}
+ \includerodinimg{tutorial/tut_08_switch_perspective.png}
\caption{Switch Perspective}
\label{fig_tut_08_switch_perspective}
\end{center}
@@ -347,7 +348,7 @@ We should now see the window in Figure \ref{fig_tut_08_proving_perspective}.
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_08_proving_perspective.png}
+ \includerodintwimg{1.0}{tutorial/tut_08_proving_perspective.png}
\caption{Rodin Proving Perspective}
\label{fig_tut_08_proving_perspective}
\end{center}
@@ -372,7 +373,7 @@ We should now see the window as shown in Figure \ref{fig_tut_08_proof_obligation
%\begin{figure}[!ht]
%\begin{center}
-% \includegraphics{img/tutorial/tut_08_proof1.png}
+% \includerodinimg{tutorial/tut_08_proof1.png}
% \caption{Rodin Proving Perspective}
% \label{fig_tut_08_proving_perspective}
%\end{center}
@@ -380,7 +381,7 @@ We should now see the window as shown in Figure \ref{fig_tut_08_proof_obligation
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_08_proof2.png}
+ \includerodintwimg{1.0}{tutorial/tut_08_proof2.png}
\caption{Proof Obligation}
\label{fig_tut_08_proof_obligation}
\end{center}
@@ -390,10 +391,11 @@ We should now see the window as shown in Figure \ref{fig_tut_08_proof_obligation
Here we need to prove that the event \texttt{remove\_1} preserves the invariant \texttt{inv2},
$c\in Q$.
-The event's action assigns the new value $Q\setminus \{x\} $to $Q$.
+The event's action assigns the new value $Q\setminus \{x\}$ to $Q$.
Because we know that invariant $c\in Q$ was valid before the assignment,
it is sufficient to prove that we do not remove $c$ from $Q$, i.e. \textsf{$x \neq c$}. Type this into the \textsf{Proof Control View} (\ref{proof_control_view}) and press the \textsf{\icon{rodin/ah_prover.png} button}.
+\ifinprint\pagebreak\fi %TODO: remove this
\info{In order to undo a step, click on a node in the \texttt{Proof Tree View} and click on the \icon{rodin/pn_prover.png} button in the \texttt{Proof Control View} or open the context menu of a node and select \texttt{Prune}.}
Take a look at the Proof Tree View. The root node should now be labelled with \texttt{ah ($x\neq c$)},
@@ -408,7 +410,7 @@ The new goal is $\lnot x = c$. Now, try selecting the right hypotheses by yourse
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_08_search_hypothesis.png}
+ \includerodinimg{tutorial/tut_08_search_hypothesis.png}
\caption{Search Hypothesis View}
\label{fig_tut_08_search_hypothesis}
\end{center}
@@ -418,7 +420,7 @@ The correct hypothesis for this proof was $k \in (P \setminus \{ c\} ) \rel P
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_08_proof_final.png}
+ \includerodintwimg{1.0}{tutorial/tut_08_proof_final.png}
\caption{The green smiley indicates that all sequents of the proof tree are discharged}
\label{fig_tut_08_proof_final}
\end{center}
diff --git a/org.rodinp.handbook.feature/latex/tutorial-10.tex b/org.rodinp.handbook.feature/latex/tutorial-10.tex
index d96b0407089e44b7bf69181682e7d0e08d391fd2..39c855aa036e11df73af25c3a6b3caf2fc58aa8f 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-10.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-10.tex
@@ -82,7 +82,7 @@ The difference between a ``normal'' invariant and one that is marked as theorem
\warning{ Make sure that when you add your DLF invariant, you add it after the other two invariants in \textsf{doors\_0}. The auto prover uses these invariants to prove that the DLF invariant is well defined, and if they aren't in the right order, the proof obligation \textsf{DLF/WD} will not be discharged
}
-\begin{rodin-plugin}{img/prob.png}{ProB}%
+\begin{rodin-plugin}{prob.png}{ProB}%
You can also use ProB to search for deadlocks (after ensuring that ProR is installed).
Right-click on the machine you want to check and start the animation with the
``Start Animation / Model Checking'' menu entry.
@@ -116,7 +116,7 @@ By doing this we want to assure that you have the same proof as in this tutorial
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_10_post_tactics.png}
+ \includerodinimg{tutorial/tut_10_post_tactics.png}
\caption{Disabling the proof post-tactics in the Proof Controlling View}
\label{fig_tut_10_post_tactics}
\end{center}
@@ -162,7 +162,7 @@ We can prove an existential quantification by giving an example for the variable
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_10_instantiate_x.png}
+ \includerodinimg{tutorial/tut_10_instantiate_x.png}
\caption{Click on the existential quantifier in order to ...}
\label{fig_tut_10_instantiate_x}
\end{center}
@@ -170,7 +170,7 @@ We can prove an existential quantification by giving an example for the variable
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_10_instantiate_p.png}
+ \includerodinimg{tutorial/tut_10_instantiate_p.png}
\caption{... instantiate it, in this case by substituting $x$.}
\label{fig_tut_10_instantiate_p}
\end{center}
@@ -185,7 +185,7 @@ You can see the the current proof tree in Figure~\ref{fig_tut_10_proof_tree}. Th
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_10_proof_tree.png}
+ \includerodinimg{tutorial/tut_10_proof_tree.png}
\caption{The proof tree after instantiating $p$ with $x$.}
\label{fig_tut_10_proof_tree}
\end{center}
@@ -211,7 +211,7 @@ to instantiate $l$.
Now we have $l$ as an example for a location which is not outside and where everybody can go.
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_10_search_hyp.png}
+ \includerodinimg{tutorial/tut_10_search_hyp.png}
\caption{Searching hypothesis for $outside$: The third one is \textsf{axm4}.}
\label{fig_tut_10_search_hypotheses}
\end{center}
@@ -253,21 +253,22 @@ Figure~\ref{fig_tut_10_final_proof_tree}).
\quad\qquad well-definedness condition $\btrue$: automatically proven\\
\quad\qquad case distinction $sit(x)=outside$ \\
\qquad\qquad well-definedness condition
- ($sit$ is a function with $x$ in its domain): \\
- \qquad\qquad\qquad\qquad\qquad\qquad proven using the \textsf{p1} provers\\
+ ($sit$ is a function with $x$ in its \\
+ \qquad\qquad\qquad\qquad\qquad\qquad domain): proven using the \textsf{p1} provers\\
\qquad\qquad first case: instantiation of $l$ from axiom \textsf{axm4}\\
\quad\qquad\qquad using $l$ as an example for the $\exists l \ldots$ in the goal\\
\qquad\qquad\qquad well-definedness condition $\btrue$: automatically proven\\
- \qquad\qquad\qquad automatically proven\\
- \qquad\qquad second case: using $outside$ as an example for the $\exists l \ldots$ in the goal\\
+ \qquad\qquad\qquad remaining goal: automatically proven\\
+ \qquad\qquad second case: using $outside$ as an example \\
+ \qquad\qquad\qquad\qquad\qquad\qquad for the $\exists l \ldots$ in the goal \\
\quad\qquad\qquad well-definedness condition $\btrue$: automatically proven\\
\quad\qquad\qquad hypotheses $P\cprod\{outside\}$ selected\\
- \qquad\qquad\qquad automatically proven\\
+ \qquad\qquad\qquad remaining goal: automatically proven\\
\hline
\end{tabular}
\begin{figure}[!ht]
\begin{center}
- \includegraphics{img/tutorial/tut_10_proof_tree_final.png}
+ \includerodinimg{tutorial/tut_10_proof_tree_final.png}
\caption{Searching hypothesis for $outside$: The third one is \textsf{axm4}.}
\label{fig_tut_10_final_proof_tree}
\end{center}
@@ -308,7 +309,7 @@ First we need a variable denoting a location in order to distinguish between the
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_10_ref_proof1.png}
+ \includerodinimg{tutorial/tut_10_ref_proof1.png}
\caption{Adding a hypothesis to instantiate a variable for a case distinction.}
\label{tut_10_ref_proof1}
\end{center}
@@ -320,7 +321,7 @@ $$ sit(p) = outside $$
Now press the \icon{rodin/dc_prover.png} button. This will create three new nodes in the proof tree: The first one is once again the well-definedness condition, followed by the two cases that we have just defined. As always, use the \icon{rodin/auto_prover.png} button to verify the well-definedness condition.
-The first case is dealing with $sit(p) = outside$. To verify this case, we need to use\textsf{axm7}, which states that at least one authorized room is connected to the outside:
+The first case is dealing with $sit(p) = outside$. To verify this case, we need to use \textsf{axm7}, which states that at least one authorized room is connected to the outside:
\pencil{
\begin{description}
@@ -336,7 +337,7 @@ Now we have variables to instantiate our goal as well. We enter the value $p$ i
\begin{figure}[!ht]
\begin{center}
- \includegraphics[]{img/tutorial/tut_10_ref_proof2.png}
+ \includerodinimg{tutorial/tut_10_ref_proof2.png}
\caption{Preparing the instantiation by providing values for $p$ and $l0$.}
\label{tut_10_ref_proof2}
\end{center}
diff --git a/org.rodinp.handbook.feature/latex/tutorial-outline.tex b/org.rodinp.handbook.feature/latex/tutorial-outline.tex
index 816e3e7a6f5b4b1c01cea9ef3c0bef565b1fcaa4..d98e76826da23252bc21ee353c92183d30275968 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-outline.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-outline.tex
@@ -17,10 +17,15 @@ If something is unclear, remember to check the Reference chapter (Chapter \ref{r
\item[Mathematical notation (\ref{tut_mathematical_notation})] At this point we quickly go through the most important aspects of predicate calculus and provide links to the reference chapter and to external literature. We explain everything used by the traffic light system, we introduce all data types and we provide a brief intoduction of sets and relations. We also explain the difference between predicates and expressions. For example, this is where we explain the difference between TRUE and $\top$.
\item[Introducing Contexts (\ref{tut_contexts})] We introduce contexts to apply the theoretical concepts that were introduced in the previous section. We use the Agatha-Puzzle as an example to step by step introduce more and more complex elements. We cover theorems and also mention well-definedness.
\item[Event-B Concepts (\ref{tut_eventb_concepts})] This is another theoretical section that provides more background information about the previous examples. We analyze the anatomy of a machine and introduce all the elements that a machine or context may have. We describe the sees and refines concepts which will be applied in the next section, and we briefly mention concepts like data refinement and witnesses although we do not explain them in detail.
- \item[Expanding the Traffic Light System (\ref{tut_expanding_traffic_light_system})] We apply what we learned in the previous section by introducing a context with traffic light colors and a refinement to integrate them. We will introduce another refinement to model the push buttons.
+ \item[Expanding the Traffic Light System (\ref{tut_expanding_traffic_light_system})] We apply what we learn\-ed in the previous section by introducing a context with traffic light colors and a refinement to integrate them. We will introduce another refinement to model the push buttons.
\item[Proving (\ref{tut_proving})] So far all proof obligations have been discharged automatically. Now we switch to the proving perspective and explore it for the first time.
We edit the configuration for the auto prover, invalidate proofs and show that with the new configuration they will not be discharged any more. We carry out a simple proof manually and describe the provers available.
\item[Proving Deadlock Freeness (\ref{tut_location_access_controller})] In this section we define what it means for a machine to be deadlock free. We use a more complex example to explore how much the Rodin provers can accomplish.
\item[Outlook (\ref{tut_outlook})] This concludes the tutorial. We provide many links here for further reading. In particular, we reference the documentation from the Deploy project and the Rodin Wiki.
\end{description}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rodin-doc"
+%%% End:
diff --git a/org.rodinp.handbook.feature/latex/tutorial.tex b/org.rodinp.handbook.feature/latex/tutorial.tex
index 7e62ca4e89b13b398ffd8034b171b0625cd2e207..8a5a4ad552417c86556a47f1801f142044893580 100644
--- a/org.rodinp.handbook.feature/latex/tutorial.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial.tex
@@ -15,3 +15,8 @@
\input{tutorial-11}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rodin-doc"
+%%% End: