ProB V1.0.6 Installation Manual Document Version 0 . 2 (generated
Contents
1. at http www ecs soton ac uk mal systems ProB_Download INSTALL html A copy of these instructions is in cluded in the appendices of the User Manual in the section Ultra Quick Instructions 1 pages Brief instructions slightly more detail For latest see Full installation instructions at http www ecs soton ac uk mal systems ProB_Download INSTALL html A copy of these instructions is included in the appendices of the User Manual in the section Brief Installation Instructions 9 pages Detailed instructions for PROB only detailed information only about installing PROB not other pieces of third party software used by PROB Includes instructions for Linux non RPM Solaris Mac OSX and Windows with screen shots where necessary Available as PostScript Adobe Acrobat and HTML 15 pages Complete OS edition Includes detailed installation instructions with screen shots for in stalling PROB as well as our guides to how to install other third party software e g GraphViz TclTk Java for use by PROB Separate editions are available for Linux Mac OSX Solaris and Windows Available as PostScript Adobe Acrobat and HTML 44 pages Obscenely verbose edition Includes detailed install guide with screen shots for installing PROB as well as other software that ma y be used by PROB Provides instructions for all editions of PROB and our instructions for additional third party software used by PROB for Solaris AND Linux RPM and other2. Find out more http www ActiveState com ASPN About Tel Please do not forget to extend your PATH and MANPATH vari get access to the applications and manpages distributed with ActiveTcl For a csh or compatible perform ActiveTel setenv PATH usr local ActiveTcl bin PATH N For a sh or similar perform Y PATH usr local ActiveTcl bin PATH export PATH Some shells bash for example allow export PATH usr local ActiveTcl bin PATH Similar changes are required for MANPATH Figure 1 6 Installation Completed including path update information if necessary
3. Download the gzipped tarball from http downloads activestate com ActiveTcl Linux 8 4 5 ActiveTcl8 4 5 0 linux ix86 83070 tar gz Decompress and extract to a temporary directory Execute the script Install sh in the ActiveTcl directory Install using defaults Update PATH settings and possibly LD_LIBRARY_PATH Sources for ActiveTcl for Linux Linux users currently require Tcl 8 3 or greater Note that almost all Linux distributions include a Tcl Tk distribution RedHat 9 0 tcl 8 3 5 88 1386 rpm and tk 8 3 5 88 1386 rpm Debian Woody stable packages tcl8 3 tk8 3 unstable packages tcl8 4 and tk8 4 If Tcl Tk is not installed Active Tcl Tk is recommended http www activestate com Products ActiveTcl At the current time the installation binary is located at is at http downloads activestate com ActiveTcl Linux 8 4 5 ActiveTcl8 4 5 0 linux ix86 83070 tar gz e An installation guide specifically for Linux from Active http aspn activestate com ASPN docs ActiveTcl at install html e A frequently asked questions document FAQ from Active http www activestate com Products Download ShowSysReqs plex req ActiveTcl e Official user manual for Active Tel http downloads activestate com ActiveTc1 htm1 8 4 5 ActiveTc18 4 5 0 html tar gz Detailed guide to the installation process The process of installing Active Tcl for Linux is straight forward if you do not change the default installation location i e where the Active Tc
4. Installing ProB on Linux Quick Install Download that gzipped tarball from http www ecs soton ac uk mal systems ProB_ Download ProB_Linux tar gz Decompress and unpack the tarball into the desired target installation directory files in the tar are in ProB ProB can only be started when the current directory is the one created by the tar i e ProB Start ProB by running ProBLinux sh On first use run the self check command from the debug menu Sources of ProB for Linux ProB may be obtained from the Declarative Systems and Software Engineering Group of the School of Electronics and Computer Science University of Southampton UK http www dsse ecs soton ac uk The official homepage of ProB is at http www ecs soton ac uk mal systems prob html At the current time the installation binary is located at http www ecs soton ac uk mal systems ProB_Download ProB_Linux tar gz e Installation Guides and the User Manual can be obtained from the PROB homepage e A frequently asked questions document FAQ is available here http www ecs soton ac uk mal systems ProB_Download FAQ txt Detailed guide to the installation process 1 Download the installation binary from http www ecs soton ac uk mal systems ProB_Download ProB_Linux tar gz Change to the directory into which you want to install ProB Decompress and extract the contents of the tar For example mkdir p bin Linux cd bin Linux gzip dc ProBLi
5. X This is a problem with the latex pdf generator Convert the postscript versions of the documents using the tools that come with OS X 1 Installing ProB 6 1 2 2 Student Edition CDROM Frequently Asked Questions e Java VM installation Broken links from Local Copies in Installation Manual If you are using the Southampton University ECS distribution of ProB we have attempted to put all the software you will need onto CD However some URLs do not translate well to local file systems such as on the CDROM Invariably the software will be on the CDROM in the directory referred to by the local copy reference but may contain characters in the file name that cause your browser to become confused for example question marks and tildes Currently this problem only affects the Java installation programs from Sun You will find the them in the cached java sun com webapps directory of the CDROM Note that MAC OS X users should use the software update facility in preference e Windows Java VM Installer Should 1 choose the on line or offline installer Preferably use the on line installer that is available from http java sun com Go to the Java VM Link on the right hand side Select Get it Now If you intend to download the installer for later use or are using the CDROM use the offline installer The offline version is in the directory cached java sun com webapps download on the CDROM 1 Installing ProB 1 2 3
6. binary is located at http ftp uk debian org debian pool non free g graphviz graphviz_1 10 20030915 0415 2_i386 deb e An installation guide from AT amp T http www research att com sw tools graphviz download html e A frequently asked questions document FAQ from AT amp T http www research att com sw tools graphviz doc gvizfaq html e An official user manual http www research att com sw tools graphviz dottyguide pdf 1 Installing ProB 12 1 5 Installing a Java Run time Environment 1 5 1 Frequently asked questions e Do I need the Java Run time Environment If you wish to edit the provided sample machines or create compile your own yes ProB will run without a Java distribution installed but you will only be able to use the sample machines we have pre compiled If you edit them they will cease to load e Can I use an alternative Java VM or SDK Yes However if ProB fails to work correctly because of differences between the Sun Java VM and your particular installation we may not be able to help resolve the problem 1 Installing ProB 13 1 5 2 Installing the Java Run time Environment on Linux RPM Quick Installation Download the self extracting install script from http java sun com webapps download AutoDL Bundleld 9561 Run the script to view agree to the Sun Binary Code Licence Agreement and create the RPM j2re 14_2_03 linux i586 rpm As root install with rpm Uvh j2re 1_4_2_03 linux i586 rpm A
7. then unpack the distribution resulting in an RPM package file 4 Install the RPM using the upgrade options rpm Uvh j2re 1_4_2_03 linux i586 rpm The RPM will install the files into usr java j2re1 4 2 03 5 You will need to add usr java j2re1 4 203 bin to your PATH and also append usr java j2re1 4 2 03 man to your MANPATH Alternatively if your default shell it tesh or csh copy and paste the following into a file in your file space e g bin Java_RTE csh 1 Installing ProB bin csh if 7 MANPATH then setenv MANPATH MANPATH usr java j2re1 4 2_03 man else setenv MANPATH usr java j2re1 4 2_03 man end setenv PATH PATH usr java j2re1 4 2_03 bin Add the following entry to chsrc source bin Java_RTE csh 14 1 Installing ProB 15 1 5 3 Installing the Java Run time Environment on Linux Non RPM Quick Installation Download the self extracting install script from http java sun com webapps download AutoDL Bundleld 9562 Make and or change into the desired installation directory root Run the script to view agree to the Sun Binary Code Licence Agreement and extract the installation to j2re1 4 2 03 Append InstallDirectory j2re1 4 203 bin and Install_Directory j2re1 4 2 03 man to PATH and MANPATH respectively Sources for Java Run time Environment for Linux non rpm variant The Sun Java Run time Environment can be obtained from the official Sun Java web site http java sun com
8. ProB V1 0 6 Installation Manual Document Version 0 2 generated June 29 2004 http www ecs soton ac uk mal systems prob html University of Southampton UK Declarative Systems and Software Engineering Contents 1 Installing ProB 2 1 1 ProB LICENCE sie ee a sels ME WORE A ee ee Be i ecto 3 1 2 Installation Requirements 0 20202 eee ee eee 4 1 2 1 Frequently Asked Questions o e eee eee eee 4 1 2 2 Student Edition CDROM Frequently Asked Questions 6 1 2 3 Installing ProB on Linux 7 1 3 Keeping PROB Up todate sx s sa qaa 0 2 0 0 a a a a a eee eee 8 1 4 Installing Graph Viz e 9 1 4 1 Frequently Asked Questions o e e 2 9 1 4 2 Installing GraphViz on Linux RPM 10 1 43 Installing GraphViz on Linux Debian 11 1 5 Installing a Java Run time Environment e e 12 1 5 1 Frequently asked questions eee 12 1 5 2 Installing the Java Run time Environment on Linux RPM 13 1 5 3 Installing the Java Run time Environment on Linux Non RPM 15 1 6 Installing EclTk seage e ymma EA A a we 17 1 6 1 Frequently Asked Questions o e e e eee 17 1 6 2 Installing Active Tcl Tk for Linux Non RPM 18 1 Installing ProB Available Editions Thank you for your interest in PROB Please ens
9. The remainder of this section assumes you are installing the Sun version of the Java Run time Environment At the current time the installation self extracting script is located at http java sun com webapps download AutoDL BundleId 9562 e The installation guide http java com en download help linux_install jsp e A frequently asked questions document FAQ http java com en download faq index jsp e An official user manual has not yet been located Detailed installation instructions The non rpm distribution of the Java Run time Environment from Sun is self extracting script It extracts into j2re1 4 2_03 in the directory in which the installation script is invoked This installation method is suitable for users without permissions to use RPM 1 Download the self extracting Bourne shell script from http java sun com webapps download AutoDL Bundleld 9562 Make and or change directory to the desired installation location e g bin LINUX and invoke the script using sh For example if you saved the download as XYZ sh in mkdir p bin LINUX cd bin LINUX sh XYZ sh You will be presented with the Sun Binary Code Licence agreement To proceed you must agree to the conditions use space to page through the licence and enter yes when prompted The install script will now automatically extract to the current directory in j2re1 4 2_03 For example bin LINUX j2re1 4 2_03 You must updat
10. demonstration programs Default should be okay Figure 1 4 Specify Run time directory Unless you have a very good reason do not change this setting from the one suggested by the installer Select Next to proceed Figure 1 5 Select Next Installation should now complete by itself Note that if you have installed ActiveTcl to a directory not on the default path make note of the settings changes it presents when setup completes This information will allow you to update your PATH and other settings Figure 1 6 Note if ProB reports that it cannot find the Tcl libraries but they are in the lib directory of the Tcl installation you will need to append this directory to LD_LIBRARY_PATH For example setenv LD_LIBRARY_PATH LD_LIBRARY_PATH bin ActiveTcl lib d Ha ESTEE A Pr Eie ween E E a eee 8 4 5 0 distribution a or Linux xt Bui STATE Packages Tel 8 4 TkTable 2 8 Tk 8 4 Tellib 15 Telx 8 3 TELL 26 incr Tcl 3 2 Blidgets 1 6 incr Tk 3 2 Tenn 2 6 IWidgets 4 0 2 TolsoaP 1 6 7 A TkCon 24 Ting 13 CUVeIc Snack 22 TEML 2 0 Expect 5 39 Unix only Toon 3 8 Windows only Next gt Cancel Figure 1 1 Proceed with Installation ActiveState ActiveTcl 8 4 5 0 Installer 7 ActiveState Community License Preamble The intent of this document is to state the conditions under which the Package ActiveTcl may be copied and distributed such that ActiveState maintai
11. e installed version must provide command line versions of dot dotty and lefty Note that some Linux distributions already include GraphViz The GraphViz utilities dot dotty and lefty must all be on your path To determine if GraphViz is installed using RPM run rpm qa grep i graphviz Alternatively use either which which dot which dotty which lefty or locate dot grep bin to determine if they are already installed GraphViz may be obtained from the official AT amp T web site or from an alternative source The official web site http www research att com sw tools graphviz Note that to perform an installation using RPM you need root access If you do not with to install using RPM or do not have permissions to do so see section on general Unix installation for instructions The remainder of this section assumes you are installing the official GraphViz distribution from AT amp T and that you have permission to use rpm to install GraphViz At the current time the installation binary is located at http www graphviz org pub graphviz ARCHIVE graphviz 1 10 1 i386 rpm e An installation manual is available from AT amp T http www research att com sw tools graphviz download html e A frequently asked questions document FAQ from AT amp T http www research att com sw tools graphviz doc gvizfaq html e An official user manual http www research att com sw tools graphviz dottyguide pdf Detailed guide to the installation
12. e your PATH and MANPATH settings with 2re1 4 2_03 bin and j2re1 4 2_03 man respectively If your default shell is csh or tesh copy and paste the following into a file in your file space e g bin Java_RTE csh and modify the definition of Java_RTE_HOME to match the directory in which you invoked the install script bin csh setenv Java_RTE_HOME bin LINUX if 7 MANPATH then setenv MANPATH MANPATH Java_RTE_HOME j2re1 4 2_03 man 1 Installing ProB else setenv MANPATH Java_RTE_HOME j2re1 4 2_03 man end setenv PATH PATH Java_RTE_HOME j2re1 4 2_03 bin Add the following entry to cshrc source bin Java_RTE csh 16 1 Installing ProB 17 1 6 Installing TclTk 1 6 1 Frequently Asked Questions e Do I need to install Tcl Tk At present you cannot use ProB without Tcl Tk installed However a version of ProB with a Java interface is currently being written Tf you subscribe to the ProB users email list you will be notified when it becomes available e Can I use a different version or distribution of Tcl Tk Maybe The only limitations we know of at present are those inherent to Sicstus Prolog This means that windows users require version 8 3 of Tcl Tk Linux Unix users should use at least version 8 3 Sicstus recommends 8 4 for Unix environments ProB is developed using both Active and Aqua Tcl 1 Installing ProB 18 1 6 2 Installing Active Tcl Tk for Linux Non RPM Quick Installation
13. er Manual for more information My state spaces are large and both dotty and PostScript viewers are cumbersome for visu alisation We are working on an alternative viewer for large state spaces I m using Unix and I cannot access the menus in dotty This almost certainly means you have num lock on The graphs that dotty or the PostScript viewer generate do not look like those in the manual Firstly dotty and PostScript viewing support different shapes colours and viewing options Secondly the shapes colours text on nodes visibility and colour fill characteristics used during viewing are all user defined Most likely you have settings different from those used during the generation of the manual See the Typical Settings sub section of the Preferences Settings section of the User Manual for more information On Unix dotty complains that it cannot find lefty Unlike dot and lefty dotty is a script Tf dotty cannot find lefty You have to set the envi ronmental variable LEFTYPATH to the directory that contains the file dotty lefty See the detailed installation notes for GraphViz in this document 1 Installing ProB 10 1 4 2 Installing GraphViz on Linux RPM Quick installation Download http www graphviz org pub graphviz ARCHIVE graphviz 1 10 1 i386 rpm As root do rpm Uvh graphviz 1 10 1 i386 rpm Sources for Linux GraphViz RPM variant There are no restrictions on the version of GraphViz used by ProB However th
14. installation of ProB If you are using PROB V1 0 6 or later you only need to download a replacement binary file ProBSolaris sh or ProBLinux sh or ProBMac sh or ProBWin exe as appropriate Fresh Install If you do not want to risk losing change from the preference defaults please make a backup of the file ProB_ Preferences p1 before removing over writing your old installation Simply copy this file back to directory into which the binary ProBSolaris sh or ProBLinux sh or ProBMac sh or ProBWin exe as appropriate resides after re installing Alternatively install the new version of PROB to another directory Windows users can run the new installer and answer yes to the prompt for over writing files The windows installer un packer should automatically attempt to re install PROB into the directory where the existing version is installed UNIX Solaris Linux and Mac OS X users may simply decompress and untar the in stallation tar gz over their existing installation Over writing ProB Binary Users with version 1 0 6 or later should obtain the appropriate file i e ProBSolaris sh ProBLinux sh ProBMac ProBWin exe or ProB sav as appropriate from http www ecs soton ac uk mal systems ProB_Download Updates and over write their existing binary with the new copy PROB will need to be restarted Solaris Linux and Mac OS X users with wget installed need only change to the installation directory of PROB and run wget http www ecs
15. l installer places its files in the file system Because Tcl is integral to many Linux distributions we do not recommend that you replace versions installed during the installation of your Linux workstation Instead install ActiveTcl to a directory not on the default path and adjust PATH and MANPATH as required detailed below Note that you may also have to append the lib directory to LD_LIBRARY_PATH for ProB usage 1 Download the installation binary http downloads activestate com ActiveTcl Linux 8 4 5 ActiveTc18 4 5 0 linux ix86 83070 tar gz 2 Create a temporary directory uncompress and unpack the gzipped tarball For example if you downloaded the installation file into mkdir temptcl gzip dc ActiveTcl8 4 5 linux ix86 83070 tar gz tar xvf 3 Change into the directory created during the extract process e g cd ActiveTc18 4 5 0 linux ix86 and invoke the installation script provided by ActiveTcl install sh The graphical installer should now start 4 Select Proceed to continue Figure 1 1 5 To continue with the installation read and accept the Licence Agreement then select Next Figure 1 2 1 Installing ProB 10 19 Choose the base directory for the installation of ActiveTcl The default is usr local If you do not have permission to install into usr local ActiveTcl can be installed suc cessfully in local file space e g bin Figure 1 3 Specify base directory for installation of TclTk
16. ns control over the development and distribution A of the Package while allowing the users of the Package to ctiveTel Package in a variety of ways The Package may contain software covered by other licenses TCL LICENSE AGREEMENT 4 laccept the terms in the License Agreement do not accept the terms in the License Agreement lt Back Ged Cancel Figure 1 2 Accept Licence or decline to exit 1 Installing ProB ActiveState ActiveTcl 8 4 5 0 Installer Please specify the installation directory www ActiveState com usmocavactivetet wl lt Back Please specify the demos directory ActiveTcl www ActiveState com ustiocavActiveTevdemos R S lt Back Next gt Cancel Figure 1 4 Specify base directory for installation of TclTk demonstrations ActiveState ActiveTc 8 4 5 0 Installer BDE Actie Please specify the runtime installation directory Active STATE This is the directory the applications will see as their installation directory when searching for packages and libraries instead of the directory the files were copied to In most circumstances this is the same as the installation directory chosen before ActiveTcl www ActiveState com usrrocaracivetel 4 lt Back Nay gt Cancel Figure 1 5 Specify Run time directory do not change ActiveState ActiveTcl 8 4 5 0 Installer EES
17. nt state Source URLs and installation instructions for TclTk Java and GraphViz may be found in the Verbose edition of the installation instructions referred to below 1 2 1 Frequently Asked Questions e How do I get assistance with problems with ProB Non members of Southampton University Please send you comments suggestions or problems to the ProB mailing list You can subscribe by sending an email with subscribe prob users in the body to majordomo ecs soton ac uk Members of Southampton University If you are a member of Southampton University you should use the problem tracker located at https secure ecs soton ac uk cgi bin jbug systems ProB Unresolved problems remain active on the problem tracker Please do not submit a request for help or report problems that already occur on the list The student edition of the documentation will be updated regularly so please also check the on line version before submitting requests for help Tf you find a problem with ProB as opposed to third party software please let us know as soon as possible We are happy to receive suggestions for improvements to ProB or the documentation e Where can I get an up to date FAQ Please check on the official ProB web page http www ecs soton ac uk mal systems prob html Updates will be posted there Tf you subscribe to the ProB mail list you will be notified when updates become available e Windows Do I have to install ProB to C Pr
18. nux tar gz tar xvf To start ProB on Linux locate and run the extracted file ProBLinux sh Your current directory must be the same as the directory in which this file resides Appending the extracted ProB directory to your PATH will not work To simplify invocation of ProB the simplest solution is to add an alias to your login or cshre For example add the following to login replace the path as appropriate alias ProB cd lt directory_containing_ProBLinux sh gt ProBLinux sh For example alias ProB cd bin Linux ProB ProBLinux sh To check that ProB has been successfully installed run the Perform Self Check option from the Debug menu A popup will appear stating whether the self check has passed or not In the unlikely event that the self check fails consult the section on Trouble Shooting in the ProBUser Manual 1 Installing ProB 8 1 3 Keeping ProB up to date PROB is regularly updated See the release notes in the User Manual to get some idea of the frequency of update releases If you would like to be notified of new updates please register with the PROB mailing list To determine if your installation of PROB is out of date use About gt Check for Updates A pop up will state if a more recent release of PROB is available A more efficient method of updating PROB came into being with version 1 0 6 Therefore if you are using PROB version 1 0 5 or earlier you will need to perform a fresh
19. o Prolog Parser Compiler amp Further Extensions Michael Butler Carla Ferreira Michael Leuschel Stephane Lo Presti Leonid Mikhailov Ed Turner Phil Turner Open Source B to XML Java Parser Type Checker Bruno Tatibouet see http lifc univ fcomte fr tatibouet JBTOOLS for more details Known limitations Many Unsupported features complex definitions some operators WHILE loops see included machines for which features are actually supported not yet optimised for speed using partial evaluation recursive set comprehension ss xx xx ss may not always work properly To visualize state space dot from AT amp T s GraphViz package has to be installed See the FAQ txt file for troubleshooting and frequently asked questions 1 Installing ProB 4 1 2 Installation Requirements This manual is concerned with the TclTk version of PROB The prototype alpha Java GUI version has no accompanying documentation at this time Please do not attempt to install ProB before ensuring you have a valid and correctly installed version of Tcl Tk Mac OS X Version 8 3 or 8 4 preferred To get the most benefit from ProB we strongly recommend that you install GraphViz and Java if they are not already installed Requires Modification of sample machines and or authoring Java Run time or SDK of new machines Visualisation of State Spaces current state vis GraphViz ited shortest path to curre
20. oB No You can install ProB wherever you like Note however that it is a good idea to avoid placing ProB or B machines in directories whose complete path contain spaces e Why is the installation manual so large so small The documentation is available in multiple editions ranging from large and verbose to half a page You probably have the wrong edition for your needs Please read the first section of this document 1 Installing ProB The Postscript manuals won t print This is likely to be due to the large colour images contained in the documentation If you are using Windows try to print from the Acrobat version If we receive enough requests we will create monochrome versions of the documentation Some of the figures int the html version of the manual look strange or are grey This is by produce of latex2html We are attempting to resolve this issue Why aren t there installation instructions for operating system machine architecture XYZ There are limitations on which distributions of ProB we can produce either Sicstus Prolog isn t available for that platform or we do not have access to the relevant hardware We won t write installation instructions for third party software if ProB cannot be compiled for that workstation or operating system How can I keep my version of ProB up to date Launch ProB and select Check for Updates in the About menu The Adobe Acrobat version of the documentation looks awful on Macintosh OS
21. ppend usr java j2re1 4 2 03 bin and usr java j2re1 4 2 03 man to PATH and MANPATH respectively Sources for Java RTE for Linux RPM variant The Sun Java Run time Environment can be obtained from the official Sun Java web site http java sun com The remainder of this section assumes you are installing the Sun version of the Java Run time Environment At the current time the installation binary is located at http java sun com webapps download AutoDL BundleId 9561 e An installation guide specifically for windows http java com en download help linux_install jsp e A frequently asked questions document FAQ from http java com en download faq index jsp e An official user manual has not yet been located If you do not have permission to install from RPM obtain the non RPM installation for Linux from Sun see 1 5 3 Alternatively install the Java SDK which can be installed into an arbitrary directory Detailed guide to the installation process 1 Download the installation script from http java sun com webapps download AutoDL BundleId 9561 2 The file downloaded is a Bourne script Use sh to invoke it sh filename For example if you downloaded from the www and saved the file as XYZ sh sh XYZ sh 3 You will be presented with the Sun Binary Code Licence agreement To proceed with the installation you must agree to the terms laid out Scroll down with space and enter yes or no The installer will
22. process The process of installing GraphViz for Linux using RPM is trivial unless you have unfulfilled dependencies 1 Download the installation binary from http www graphviz org pub graphviz ARCHIVE graphviz 1 10 1 i386 rpm 2 Install the package using the update options GraphViz is included in some distributions of Linux rpm Uvh graphviz 1 10 1 i386 rpm 3 The GraphViz i386 binaries are placed by default into usr bin Either logout login or rehash your path 4 Check that the dot dotty and lefty utilities are now on your path and are executable dot and lefty should be binaries i386 ELF 32 bit LSB non stripped executables and dotty is a Bourne shell script 1 Installing ProB 11 1 4 3 Installing GraphViz on Linux Debian Quick installation Download and install the Debian package from http ftp uk debian org debian pool non free g graphviz graphviz_1 10 20030915 0415 2_i386 deb using dpkg i Sources for Linux Debian variant There are no restrictions on the version of GraphViz used by ProB However the installed version must provide command line versions of dot dotty and lefty and these must be on your path GraphViz may be obtained either from the official AT amp T web site or using apt get The official web site http www research att com sw tools graphviz The remainder of this section assumes you are installing the deb GraphViz distribution from AT amp T At the current time the installation
23. soton ac uk mal systems ProB_Download Updates XXX where XXXX is either ProBSolaris sh or ProBLinux sh or ProBMac sh as appropriate You will need to change the permissions on the downloaded file to allow execution e g using chmod u x Important Notes on Upgrading ProB 1 Updates are the latest public releases Older versions of updates and installation binaries tars are not currently available Unless you retain the previous installation update files in separate directories locations you will not be able to down grade PROB to a previous version However if you would like a previous release of PROB please contact us 1 Note that you don t need to update PROB Check the release file at http www ecs soton ac uk mal systems ProB_Download Updates RELEASE_HISTORY txt to see the recent changes 1 Installing ProB 1 4 Installing GraphViz GraphViz is a set of graph drawing tools We strongly recommend that you install them ProB is much easier to use with visualisation functionality than without 1 4 1 Frequently Asked Questions Do I have to install GraphViz No You can use ProB without visualisation However if you attempt to use the commands in the animation visualisation menu without GraphViz installed you may cause an error in ProB Should I use dotty or a PostScript viewer There is no simple answer to this question See the Graphical Viewer Preference sub section in the section on Beginner Mode Settings of the Us
24. ure that you are using the correct edition of the installation instructions appropriate to your needs and expertise Installation instructions are available in a range of levels of detail This is not a mistake some people only require one page others quite a few more If you cannot follow the instructions or have problems installing we suggest you look to the installation documentation with the next highest level of detail See edition list below If you are having problems installing third party software for use with PROB in the first instance please see the FAQs that accompany the Complete OS and Verbose editions of the installation instructions below If your problem is not addressed in these editions please see the Trouble Shooting chapter in the User Manual You may also like to consult the instructions that came with the software causing difficulty Requests for help may also be sent to the PROB mail list If you are unfamiliar with installing software or fixing problems that may occur when installing third party software it isn t a good idea to work your way through the different versions of the installation instructions starting with Ultra brief and working up stick to the most detailed it will be quicker in the end All versions of the installation instructions are available from the PROB homepage http www ecs soton ac uk mal systems prob 0 5 page Ultra quick instructions See the Quick Install Instructions
25. wise AND Windows AND Mac OSX Available as PostScript Adobe Acrobat and HTML 1 Installing ProB 3 1 1 ProB Licence The latest version of this information can be obtained via About gt About ProB Version 1 0 6 Released on June 16 2004 ProB A B animator and model checker C 2000 2004 Michael Leuschel DSSE University of Southampton All rights reserved Free for non commercial academic use or evaluation purposes For commercial use contact the author http www ecs soton ac uk mal ProB comes with ABSOLUTELY NO WARRANTY OF ANY KIND This software is distributed in the hope that it will be useful but WITHOUT ANY WARRANTY The author s do not accept responsibility to anyone for the consequences of using it or for whether it serves any particular purpose or works at all No warranty is made about the software or its performance For updates and news check http www ecs soton ac uk mal systems prob html http www ecs soton ac uk mal systems ProB_Download Updates ProB uses state of the art Prolog technology co routining finite domain constraint solvers PILLOW XML package to achieve symbolic debugging constraint based and temporal logic based model checking The tool is partly being developed within the EPSRC grants iMoc and ABCD Development Copyright and Intellectual Property Rights B Kernel amp Model Checker Michael Leuschel TCL TK Interface Michael Leuschel Laksono Adhianto XML t
Download Pdf Manuals
Related Search