diff --git a/src/docs/chapter/user/10_General/00_section_header.adoc b/src/docs/chapter/user/10_General/00_section_header.adoc deleted file mode 100644 index de736a0c9b12dc464bd0dea2640b3f5b1d212729..0000000000000000000000000000000000000000 --- a/src/docs/chapter/user/10_General/00_section_header.adoc +++ /dev/null @@ -1,4 +0,0 @@ - -[[general]] -= General -:leveloffset: +1 diff --git a/src/docs/chapter/user/10_General/01_Installation.adoc b/src/docs/chapter/user/10_General/01_Installation.adoc deleted file mode 100644 index c050d8ce70a63cf53d2f400531e6d814e460c314..0000000000000000000000000000000000000000 --- a/src/docs/chapter/user/10_General/01_Installation.adoc +++ /dev/null @@ -1,121 +0,0 @@ - -[[installation]] -= Installation - -[[what-are-the-available-versions]] -== What are the available versions? - -* The standalone Tcl/Tk Version of ProB (ProB Tcl/Tk) -* The standalone command-line version of ProB -(<<using-the-command-line-version-of-prob,probcli>>) -* The <<tutorial-rodin-first-step,ProB Plugin for Rodin/Eclipse>> -* The online <<prob-logic-calculator,ProB Logic Calculator>> - -Both the standalone ProB Tcl/Tk and probcli can be downloaded together -(within a Zip archive or tarball together with examples) from our -<<downloads, Download Page>>. The online -<<prob-logic-calculator,ProB Logic Calculator>> requires no -installation; just type in predicates and expressions into the web page. - -There is also a -https://tools.clearsy.com/index.php5?title=ProB_etool_generation[plugin -for Atelier B], in order to use the standalone ProB Tcl/Tk Version on -https://www.atelierb.eu/[Atelier B] projects. It comes bundled with ProB -Tcl/Tk. - -ProB is used within a few other tools, such as -http://wiki.event-b.org/index.php/IUML-B[iUML-B] or -http://safecap.sourceforge.net/index.shtml[SafeCap]. - -We are also developing a new Java-based API called -<<prob_2.0-tutorial,ProB 2.0>>, which is a high-level wrapper for the -command-line version and <<using-the-command-line-version-of-prob, here>> is how to use it. - -[[which-version-should-i-use]] -== Which version should I use? - -The standalone version Tcl/Tk of ProB contains a richer set of features -than the Rodin version and also works on other formalisms than Event-B -(e.g., classical B, Z, CSP, B||CSP, Promela, ...). If you want to do -animation and model checking of Event-B models, the Rodin version might -be enough. The Rodin version contains a translation tool from Rodin into -Event-B package files that can be used within the standalone version of -ProB. Use the probcli version if you want to write batch scripts or -prefer working from the command-line. - -[[installation-instruction-for-prob-standalone]] -== Installation Instruction for ProB (Standalone) - -NOTE: We have specific <<windows-installation-instructions, Windows installation instructions>>. -These here are the generic instructions. - -* Obtain your platform specific ProB distribution from <<downloads, Downloads>>. -Decompress and expand the ProB directory if -necessary. Do not change the location and structure of the files and -directories within ProB (apart from the Machines directory)! On Windows -you just have to double-click the installer. The contents of the ProB -directory should look something like this: - -`examples lib prob` + -`StartProB.sh tcl` - -On Windows, you will also have a subfolder called "Microsoft.VC80.CRT" -containing the DLLs for the C runtime. Also, the binary is called -"ProBWin" and not "prob". - -* Be sure that you have Tcl/Tk installed (see, e.g., -http://www.tcl.tk/software/tcltk/). With the latest version of ProB, you -have to install Tcl/Tk version 8.5. -For example, you can find a correct version of Tcl/Tk at -http://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/. -* To load your own B machines you also need Java 7 or newer runtime or better JDK. - -NOTE: you can skip this step if you do not wish to use the -visualization commands. Install the "dot" program and "dotty" viewer -from AT&T's Graphviz package (http://www.graphviz.org/ or -http://www.research.att.com/sw/tools/graphviz/). -By default, ProB will -open the "dotty" program to visualize the graphs, but postscript -viewers (such as gv) are also supported. So, you do not need to install -dotty if you don't want to; but it is probably easiest to install the -entire Graphviz package. - -* Change to the ProB directory and then start up prob. In Windows you -can simply double-click on the ProBWin Application. On Mac OS X you may -have to type 'limit data unlimited' (in tcsh) or 'ulimit -d unlimited' -(in bash) before launching ProB using the Terminal Application. The -distribution contains a script StartProB.sh which does this for you -(note you may have to do `chmod u+x StartProB.sh` before launching it from -the command-line). -* Now you should be able to open some of the B Machines in the Machines -directory. You should then be able to initialize the machines and -animate them. Have a look at the supplied Machines in the examples -directory. Have fun! Please report bugs! - -[[checklisttroubleshooting]] -=== Checklist/Troubleshooting - -* Java: be sure to have Java 7 or newer installed. Otherwise you will -not be able to parse your own classical B machines as our parser is -written in Java. - -* Tcl/Tk: be sure to have a suitable version of TclTk installed. In -general you should install at least 8.5. -You also need the 64 bit version of Tcl/Tk for 64 bit -versions of ProB. - -* GraphViz: in order to make use of the graphical visualization -features, you need to install a version of GraphViz suitable for your -architecture. Then use the command "Graphical Viewer Preferences..." -in the Preferences Menu to set or check the following preferences: -** Path/Command for dot program -** Path/Command for dot viewer (e.g., dotty) - -NOTE: you can use the "Pick" button to locate the dot program and the -dot viewer. See more information about the -<<graphical-viewer,Graphical Viewer here>>. - -[[installation-instruction-for-prob-rodin-plugin]] -== Installation Instruction for ProB (Rodin Plugin) - -<<tutorial-rodin-first-step,This>> tutorial shows how to properly install ProB for Rodin. diff --git a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc deleted file mode 100644 index bd38149f2ecc0e18c9cb7544272b8447af90c119..0000000000000000000000000000000000000000 --- a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc +++ /dev/null @@ -1,96 +0,0 @@ - -[[windows-specific-download-instructions]] -= Windows Specific Download Instructions - -[[go-to-the-prob-downloads-site]] -== Go to the ProB Downloads site - -* Go to the page -https://www3.hhu.de/stups/prob/index.php/Download[Download], -this should look as follows: - -image::ProBWindowsDownload.png[] - -[[install-tcltk-8.5]] -== Install Tcl/Tk 8.5 - -If Tcl/Tk 8.5 is already installed you can skip this step. - -* Click on the http://downloads.activestate.com/ActiveTcl/releases/[Tcl/Tk 8.5 for -Windows] link provided in the `Dependencies` column and the -`Windows` row above -* Choose the most recent Tcl/Tk 8.5 distribution available for windows; -be sure to choose a version matching ProB, e.g. a 32-bit version (the -file highlighted in blue below) if you want to use the 32-bit version of -ProB. -* Download and follow the installation instructions - -image::TkWindowsDownload.png[] - -[[install-java]] -== Install Java - -If Java 7 or newer is already installed you can skip this step. - -* Click on the http://java.com/en/[Java Runtime Environment (7.0 or -newer)] link provided in the `Dependencies` column and the `Windows` row above -* Follow the installation instructions - -[[download-the-prob-for-windows-zipfile]] -== Download the ProB for Windows Zipfile - -* Click on the https://www3.hhu.de/stups/downloads/[Zipfile -(with probcli)] link in the `Downloads` column and `Windows` row -* Decompress and expand the ProB directory if necessary. Do not change -the location and structure of the files and directories within ProB -(apart from the Machines directory)! The contents of the ProB directory -should look something like this: - -image::ProBWindowsFolder.png[] - -The subfolder called `Microsoft.VC80.CRT` contains the DLLs for the -Microsoft C runtime. - -[[optionally-download-graphviz]] -== Optionally Download GraphViz - -* Install the `dot` program and `dotty viewer` from -http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/[AT&T's Graphviz package] - -[[start-prob]] -== Start ProB - -* Start ProB by double-clicking on the ProBWin icon above -* Try to open some of the examples provided in the Examples folder shown above -* Contact us if you have problems - -[[checklist-troubleshooting]] -== Checklist/Troubleshooting - -* Java: be sure to have Java 1.7 or newer installed. Otherwise you will -not be able to parse your own classical B machines as our parser is -written in Java. - -* Tcl/Tk: be sure to have a matching version of TclTk 8.5 installed - -* In case you cannot start neither ProBWin nor probcli, you should to -install the -https://www.microsoft.com/en-us/download/details.aspx?id=3387[Microsoft -Visual C++ 2005 Redistributable Package (x86)] for yourself (rather than -rely on the ones we provide in the `Microsoft.VC80.CRT` folder -mentioned above). - -* Try starting ProBWin or probcli from the Windows Command Prompt; the -error messages may help you or us uncover the problem - -* You can also try and obtain information from the main Windows -Event/Error Log, by following these steps: -** Click Start, and then click Control Panel. -** Click Performance and Maintenance, then click Administrative Tools, -and then double-click Computer Management. Or, open the MMC containing -the Event Viewer snap-in. -** In the console tree, expand Event Viewer, and then click the log that -contains the event that you want to view. -** In the details pane, double-click the event that you want to view. -** The Event Properties dialog box containing header information and a -description of the event is displayed. diff --git a/src/docs/chapter/user/10_General/Editors_for_ProB.adoc b/src/docs/chapter/user/10_General/Editors_for_ProB.adoc deleted file mode 100644 index 532490ca1612f4d896bafb40a207c17e34285c94..0000000000000000000000000000000000000000 --- a/src/docs/chapter/user/10_General/Editors_for_ProB.adoc +++ /dev/null @@ -1,70 +0,0 @@ - -[[editors-for-prob]] -= Editors for ProB - -[[prob-tcltk-editor]] -== ProB Tcl/Tk Editor - -ProB Tcl/Tk contains an editor in which syntax errors are displayed and -which can be used to edit B, CSP, Z and TLA+ models. The editor of -Tcl/Tk, however, has a few limitations: - -* it can become very slow with long or very long lines -* the syntax highlighting can become slow with very large files. Hence, -syntax highlighting is automatically turned off in some circumstances -(when more than 50,000 characters are encountered or when a line is -longer than 500 characters). - -It is possible to open the files in an external editor. You can setup -the editor to be used by modifying the preference ''Path to External -Text Editor'' in the Advanced Preferences list (available in the -_Preferences_ menu). You can then use the command ''Open FILE in -external editor'' in the _File_ menu to open your main specification -file with this editor. You can also use the command-key shortcut -"Cmd-E" for this. - -[[launching-the-editor-in-probcli]] -== Launching the editor in probcli - -The <<using-the-command-line-version-of-prob,probcli>> REPL -(read-eval-print-loop) supports the command `:e` to open the current -file in the external editor, as specified in the "EDITOR" preference. -You can set this preference using: - -`probcli -repl -p EDITOR PATH` - -In case errors occurred with the last command, this will also try and -move the cursor to the corresponding location in the file. - -[[external-editors]] -== External Editors - -[[vim]] -=== VIM - -A https://github.com/bivab/prob.vim[VIM plugin for ProB is available]. -It shows a quick fix list of parse and type errors for classical B -machines (.mch) using the -<<using-the-command-line-version-of-prob,command line tool probcli>>. -VIM has builtin syntax highlighting support for -https://github.com/vim/vim/blob/master/runtime/syntax/b.vim[B]. - -[[atom]] -=== Atom - -There is a package -https://atom.io/packages/language-b-eventb[language-b-eventb] available -for the Atom editor. It adds syntax highlighting and snippets for the -specification languages B and Event-B to Atom. It integrates with -probcli to obtain error markers for syntax and type errors. - -[[bbedit]] -=== BBEdit - -Some https://github.com/leuschel/bbedit-prob[BBedit Language modules for -B, TLA+, CSP and Prolog] are available. - -[[emacs]] -=== Emacs - -A package is available. //TODO: Downloadlink b-mode.el.zip[] diff --git a/src/docs/chapter/user/10_General/ZZ_section_footer.adoc b/src/docs/chapter/user/10_General/ZZ_section_footer.adoc deleted file mode 100644 index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000 --- a/src/docs/chapter/user/10_General/ZZ_section_footer.adoc +++ /dev/null @@ -1,2 +0,0 @@ - -:leveloffset: -1