diff --git a/org.rodinp.handbook.feature/latex/tutorial-08.tex b/org.rodinp.handbook.feature/latex/tutorial-08.tex index ea7a74f0404649c5438417b9f97d846f2c72b1e8..0518d042a15e5b763a63a679059d3a91327f4c39 100644 --- a/org.rodinp.handbook.feature/latex/tutorial-08.tex +++ b/org.rodinp.handbook.feature/latex/tutorial-08.tex @@ -9,7 +9,7 @@ In this section, we will work with the model of the so-called celebrity problem. -\ifinprint\pagebreak\fi %TODO: remove this +%\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. @@ -31,7 +31,7 @@ Rather than creating the model step by step, we have provided the model as an ar \warning{Make sure that you have no existing Project named ``Celebrity'', before importing the project. If you have, then rename it by right clicking the project and selecting \textsf{Rename...}} -Import the archive file \file{Celebrity.zip}{Celebrity.zip} to you Event-B Explorer. To do this, select \textsf{File $\rangle $ Import $\rangle $ General $\rangle $ Existing Projects into Workspace}. Then select the option to import an existing archive file. Use the browse function to find your archive file and import it. After you have selected the appropriate archive file, click on \textsf{Finish}. +Import the archive file \file{Celebrity.zip}{Celebrity.zip} to your Event-B Explorer. To do this, select \textsf{File $\rangle $ Import $\rangle $ General $\rangle $ Existing Projects into Workspace}. Then select the option to import an existing archive file. Use the browse function to find your archive file and import it. After you have selected the appropriate archive file, click on \textsf{Finish}. It will take a few seconds for Rodin to extract and load all the files. Once this is done, a few problems will be displayed in the Rodin Problems view (compare with Figure \ref{fig_tut_08_rodin_problemview}).