Skip to content
Snippets Groups Projects
Commit cb24b4d3 authored by dgelessus's avatar dgelessus
Browse files

Remove General section whose content can be found on the wiki

parent 17169add
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/docs/chapter/user/10_General/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 17169add
[[general]]
= General
:leveloffset: +1
src/docs/chapter/user/10_General/01_Installation.adoc deleted 100644 → 0
+ 0
− 121
View file @ 17169add
[[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.
src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc deleted 100644 → 0
+ 0
− 96
View file @ 17169add
[[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.
src/docs/chapter/user/10_General/Editors_for_ProB.adoc deleted 100644 → 0
+ 0
− 70
View file @ 17169add
[[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[]
src/docs/chapter/user/10_General/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 17169add
:leveloffset: -1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment