ProB V1.0.6 Installation Manual Document Version 0 . 2 (generated
Contents
1. 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 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 utx 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 changes2. ProB 3 Recycle Bin E ProB Licence ProB_Windo Michael Leuscher Stephane Lo Prest Leonid Mikhailov Ed T Turer Phil Turner Open Source B to XML Java Parser Type Checker Bruno Tatibouet see http W life univ feomte fri tatibouetJBTOOLS 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 px 30 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 bt file for troubleshooting and frequently asked questions ae TSA T Data 2 Start si t ProB V1 0 0 for Windows ProB_Windo o Press Install button to start extraction o Use Browse button to select the destination folder from the folders tree It can be also entered manually e Ifthe destination folder does not exist it will be created automatically before extraction Destination folder Installation progress TSA T sii t ProB V1 0 0 for Windows ProB_Windo Extracting Machines LessSimple Game Extracting Machines LessSimple Extracting Machines Laws FunLaws mch Extracting Machines Laws FunLaws xml Extracting Machines Laws SeqLaws mch Extracting Machines Laws SeqLaws xml Extracting Machines L
3. 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 current 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
4. 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 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 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
5. 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 1 1 ProB Licence 1 2 Installation Requirements 1 2 1 Frequently Asked Questions 1 2 2 Student Edition CDROM Frequently Asked Questions 1 2 3 Installing ProB for Windows 1 3 Keeping PROB up to date 1 Installing ProB Available Editions Thank you for your interest in PROB Please ensure 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
6. awe SetLaws mch Extracting Machines Laws SetL_aws xml Extracting Machines Laws Setl_awsNat mch Extracting Machines Laws SetLawsNat xml Extracting Machines Laws Extracting Machines Extracting MyConsoleParser ConsoleParser jar frea MyConsoleParser ConsoleTypeChecker jar Destination folder C PioB Installation progress m cl ne TSA T me Data z Figure 1 3 ProB will install into the selected directory window will exit when complete 1 Installing ProB Recycle Bin ProB_Windo TSA T ae Data 2 Wstart a 2 oo ie Figure 1 4 Locate and open the ProB shortcut that will have appeared on the desktop 4 ProB 1 0 1 c Michael Leuschel Eile Animate Verify Analyse Preferences ProB Version 1 0 x First released on March 9 2004 Jeiz StateProperties EnabledOperations initialise_machinef History DEE Figure 1 5 File Animate Verify Analyse Preferences Debug erOperation dc king global op f d n_argunent _print_funetion olors dot_print_root dot_pi p nt_node_ids dot_print_nod path_to_ps dot_root_s info dot_use_ps path_to_dot path_to_dot dot_normal e nt_node_shape d colour pi i Figure 1 6 Un iconify ProB command window to verify Self Check has passed 1 Installing ProB 10 1 3 Keeping ProB up to date PROB is regularly updated See the release notes in the User
7. e CDROM Note that MAC OS X users should use the software update facility in preference e Windows Java VM Installer Should I 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 Installing ProB for Windows Quick Install Download and install using default settings ProB from http www ecs soton ac uk mal systems ProB_Download ProB_Windows_Installer exe Sources of ProB for Windows 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_Windows_Installer exe e The latest version of the installation guide can be obtained from is not applicable e A continually updated frequently asked questions document FAQ is available here http www ecs soton ac uk mal systems ProB_Download FAQ txt e The user manual fo
8. line version before submitting requests for help If 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 If 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 ProB 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 instructi
9. ons 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 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 th
10. oton 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 to 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
11. r ProB is available at is not applicable Detailed guide to the installation process The process of installing ProB for windows should be straight forward if you do not change the default installation location 1 Download the installation binary from http www ecs soton ac uk mal systems ProB_Download ProB_Windows_Installer exe Open Run the ProB installer The ProB Licence and general release notes will be dispayed You must accept the Licence conditions to proceed with installatioh Figure 1 1 Specify the directory into which ProB should be installed Note that installing to a directory that contains spaces e g ProgramVFiles is not recommended Select Install to unpack and install ProB Figure 1 2 Once ProB has decompressed Figure 1 3 to the specified directory the install window will disapper and a shortcut icon will appear on the desktop Figure 1 4 To confirm that ProB has succesfully installed double click on the short cut Perform a self check Menus bar Debug Perform Self Check Figure 1 5 A pop up 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 PROB User Manual You will need to un iconify the ProB command window and examine the output It should look like Figure 1 6 If there is an error the text of the error will appear in the command window as well as in a po pup 1 Installing
12. 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 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
13. 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 otherwise 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 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 s
Download Pdf Manuals
Related Search