Installation: Difference between revisions

m (Moved category to bottom)
 
(19 intermediate revisions by 4 users not shown)
Line 1: Line 1:
[[Category:User Manual]]__NOTOC__
__NOTOC__
== What are the available versions? ==
== Which version should I use? ==
 
* The standalone Tcl/Tk Version of ProB
* The ProB Plugin for Rodin/Eclipse
* The standalone command-line version of ProB (probcli)
 
There is also a [http://www.tools.clearsy.com/index.php5?title=ProB_etool_generation plugin for Atelier B], in order to use the standalone Tcl/Tk Version on [http://www.atelierb.eu/ Atelier B] projects.


== Which version should I use? ==
See [[The ProB Animator and Model Checker#Versions of ProB|our homepage]] for an overview of the available versions of ProB.
All ProB tools can be downloaded from our [[Download]] page.


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.
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.
Line 14: Line 9:


== Installation Instruction for ProB (Standalone) ==
== Installation Instruction for ProB (Standalone) ==
*  Obtain your platform specific ProB distribution from 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:
Note: we have specific [[Windows_Installation_Instructions]]. These here are the generic instructions.
 
*  Obtain your platform specific ProB distribution from [[Download|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
  examples            lib    prob
  StartProB.sh        tcl
  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".
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.4 (for some versions of ProB even 8.5)! For Windows you can find a correct version of Tcl/Tk at http://downloads.activestate.com/ActiveTcl/Windows/8.4.19/ . The Mac version needs Tcl/Tk 8.5 or higher (http://www.tcl.tk/software/tcltk/8.5.html/).
* Be sure that you have Tcl/Tk installed (see, e.g., http://www.tcl.tk/software/tcltk/).  
* To load your own B machines you also need Java runtime installed (http://java.sun.com/j2se/index.jsp or directly to http://java.sun.com/javase/downloads/index.jsp to download the standard edition 5.0; on Mac and Linux Java is probably already installed).
With the latest version of ProB, you
* 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 visualise 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.
have to install Tcl/Tk version 8.5.
For example, you can find a correct version of Tcl/Tk athttp://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).
* 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 initialise the machines and animate them. Have a look at the supplied Machines in the examples directory. Have fun ! Please report bugs!
* 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!


=== Checklist/Troubleshooting ===
=== Checklist/Troubleshooting ===


* Java: be sure to have Java 1.5 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.
* 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.4.14 in general and at least 8.5 on the Mac.
* 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:
* 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:
Line 36: Line 39:
See more information about the [[Graphical Viewer|Graphical Viewer here]].
See more information about the [[Graphical Viewer|Graphical Viewer here]].


== Installation Instruction for ProB (Rodin Plugin) ==
[[Category:User Manual]]
 
The interactive movie shows how to install the ProB Rodin Plugin.
 
<swf width="800" height="600">Install.swf</swf>

Latest revision as of 08:21, 24 March 2022

Which version should I use?

See our homepage for an overview of the available versions of ProB. All ProB tools can be downloaded from our Download page.

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)

Note: we have specific Windows_Installation_Instructions. These here are the generic instructions.

  • Obtain your platform specific ProB distribution from 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".

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 athttp://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!

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 here.