A.F. Donaldson - TopSPIN Version 2.2. Automatic symmetry reduction for the SPIN model checker. User Manual (798531), страница 2
Текст из файла (страница 2)
This is usually achieved by adding the folderfor the SPIN executable to your path environment variable. To verify that SPIN is set up appropriately,type spin in a fresh command prompt. You should see something like:C:\>spinSpin Version 5.1.6 -- 9 May 2008reading input from stdin:If you have renamed the SPIN executable from spin to something like spin-linux or spin516 then youwill get errors when you run TopSPIN.1.2DownloadingTo download TopSPIN version 2.2, go to the TopSPIN web page:http://www.allydonaldson.co.uk/topspin/and download the following file:TopSPIN_2.2.tgzUse the tar utility, the WinRAR tool,1 or another suitable program to extract this archive to an appropriate location, e.g.
C:\Program Files\TopSPIN_2.2 under Windows, or /usr/local/TopSPIN_2.2under Linux. This location is referred to as the TopSPIN root directory.The archive should contain the following:• TopSPIN.jar Executable jar for the TopSPIN program• documentation Folder containing this document, some related research papers and a Ph.D.thesis1.http://www.rarlab.com/PackageJava runtime environmentGAP systemSPIN model checkerGNU C Compiler (gcc)URLhttp://java.sun.com/http://gap-system.org/http://www.spinroot.com/http://gcc.gnu.org/Figure 1.1: TopSPIN prerequisites.Version1.5.0 064.4.65.1.73.4.4• examples Folder containing example Promela specifications for use with TopSPIN• Common Folder containing various GAP and C files files used by TopSPIN• saucy Folder containing source code for the saucy program, which must be compiled (asdescribed in §1.3.1) before TopSPIN can be used.1.3Installing1.3.1 Compiling saucyTopSPIN uses a prototype extension of the saucy program, which is used to compute symmetries ofdirected graphs.
A version of saucy with this capability will eventually be available from the saucywebsite.2 For the time being, a source distribution of saucy with the required extended functionality isprovided with TopSPIN.3Before using TopSPIN, you need to compile saucy on your platform. To do this, navigate to thesaucy folder, which is inside the TopSPIN root directory, and type make:C:\Program Files\TopSPIN_2.2>cd saucyC:\Program Files\TopSPIN_2.2\saucy>makegcc -ansi -pedantic -Wall -O3-c -o main.o main.cgcc -ansi -pedantic -Wall -O3-c -o saucy.o saucy.cgcc -ansi -pedantic -Wall -O3-c -o saucyio.o saucyio.cgcc -o saucy main.o saucy.o saucyio.o1.3.2 Creating a GAP workspaceIn order to start GAP efficiently, TopSPIN requires a GAP workspace to be set up.
Essentially, a workspaceis an image of a GAP session with a selection of libraries and files already loaded and ready to beexecuted. For TopSPIN, the workspace consists of the GAP components of TopSPIN which have beendeveloped for automatic symmetry reduction. These are in the Common folder, inside the TopSPIN rootdirectory.Navigate into the Common folder, and start GAP. GAP is usually started via a shell script (underLinux) or batch file (under Windows). If the folder containing this script/batch file is on your path thenyou should be able to start GAP simply by typing gap. Otherwise, start the tool by typing the full pathfor the script/batch file, e.g.C:\gap4r4\bin\gapor/home/username/bin/gapYou should see something like this:C:\Program Files\TopSPIN_2.2>cd CommonC:\Program Files\TopSPIN_2.2\Common>gapC:\Program Files\TopSPIN_2.2\Common>rem sample batch file for GAPC:\Program Files\TopSPIN_2.2\Common>C:\GAP4R4\bin\gapw95.exe -m 14m-l C:\GAP4R4\#####################################################################################2.3.#################################################### ######### ################################################################################################################################################# ################### ####http://vlsicad.eecs.umich.edu/BK/SAUCY/Permission for including the saucy distribution with TopSPIN has been granted by Paul Darga, lead developer of saucy.###############################################################################################################################################################################################################################################Information at: http://www.gap-system.orgTry ’?help’ for help.
See also ’?copyright’ and###############################################################’?authors’Loading the library. Please be patient, this may take a while.GAP4, Version: 4.4.6 of 02-Sep-2005, i686-pc-cygwin-gccComponents: ...gap>Now create a workspace as follows:gap> Read("WorkspaceGenerator.gap");gap> SaveWorkspace("gapworkspace");truegap> quit;Ensure that these commands are typed exactly as shown, ensuring that the semi-colon is included afterthe quit command. When you exit GAP, you should find a file called gapworksapce in the Commondirectory.1.4Executing the TopSPIN jar fileIt should now be possible to run the TopSPIN jar file on no input to display a list of TopSPIN options:C:\>java -jar "C:\Program Files\TopSPIN_2.2\TopSPIN_2.2.jar"Error: no input file specified.To run TopSPIN on an input file:[command-line options] <inputfile>For help on command-line or config file option:help <option>For list of options:helpSuccessfully displaying this message confirms that the Java runtime environment is correctly installedon your system, and that the TopSPIN jar file you have obtained is in working order.
If TopSPIN does notcorrectly display its options, proceed to Chapter 6 to try to deduce what is wrong, and to file a bug reportif necessary.In Chapter 2, instructions for running TopSPIN to perform symmetry reduction on a Promelaspecification are given.2Worked ExampleIn this chapter, the basic workings of TopSPIN are illustrated via a worked example.2.1Loadbalancer specificationThe examples folder in the TopSPIN root directory contains a file, loadbalancer.p.
This is a Promelaspecification for a loadbalancer, which forwards requests from a pool of clients to a pool of servers in afair manner.Components in the loadbalancer are a set of 2 server and 4 client processes with associated communication channels, and a loadbalancer process with a dedicated input channel. The load of a server isthe number of messages queued on its input channel. Client processes send requests to the loadbalancer,and if some server’s channel is not full, the loadbalancer forwards a request nondeterministically to oneof the least-loaded server queues. Each request contains a reference to the input channel of its associatedclient process, and the server designated by the loadbalancer uses this channel to service the request.2.2Applying SPIN to the loadbalancer specificationBefore applying TopSPIN to this example, it is worth checking that SPIN is in good working order bymodel checking the example without symmetry reduction.Navigate to the examples directory, and run the following commands:C:\Program Files\TopSPIN_2.2\examples>spin -a loadbalancer.pC:\Program Files\TopSPIN_2.2\examples>gcc -o pan -O2 -DSAFETY pan.cC:\Program Files\TopSPIN_2.2\examples>pan -m100000SPIN should successfully verify that the model associated with the specification is deadlock-free, producing output similar to:(Spin Version 5.1.6 -- 9 May 2008)+ Partial Order ReductionFull statespace search for:never claimassertion violationscycle checksinvalid end states- (none specified)+- (disabled by -DSAFETY)+State-vector 108 byte, depth reached 73413, errors: 0170903 states, stored413074 states, matched583977 transitions (= stored+matched)6 atomic stepshash conflicts:48755 (resolved)24.974memory usage (Mbyte)unreached in proctype clientline 20, state 6, "-end-"(1 of 6 states)unreached in proctype loadBalancerline 34, state 13, "-end-"(1 of 13 states)unreached in proctype serverline 43, state 7, "-end-"(1 of 7 states)unreached in proctype :init:(0 of 9 states)pan: elapsed time 0.818 seconds pan: rate 208927.87 states/second2.3Setting up a TopSPIN configuration fileYou are almost ready to use TopSPIN for symmetry reduction! When you invoke TopSPIN on a Promelaspecification, the tool requires that a file called config.txt is available in the current directory.
This filetells TopSPIN where to find the GAP and saucy programs, the location of some common source code, andthe values of various runtime options. The file consists of a series of lines, each of which has the form:attribute=valueThree attributes are required in every configuration file:1. gap – the absolute path for the shell script or batch file required to launch GAP. The value forthe gap attribute must be such that typing this value at the command prompt is all that is requiredto launch the GAP program.2. saucy – the absolute path for the saucy executable.
Again, the value for the saucy attributemust be exactly what you type to run saucy from the command line.3. common – the absolute path to the Common directory in the TopSPIN root directory, followed bya (back- or forward-, depending on your operating system) slash.Under Windows, config.txt might look like this:gap=C:\gap4r4\bin\gap.batsaucy=C:\Program Files\TopSPIN_2.2\saucy\saucy.execommon=C:\Program Files\TopSPIN_2.2\Common\whereas a possible Linux version of config.txt could be:gap=/home/username/bin/gapsaucy=/users/grad/ally/TopSPIN_2.2/saucy/saucycommon=/users/grad/ally/TopSPIN_2.2/Common/Note that the gap option should not specify the GAP executable itself, rather the shell script (gap.sh) orbatch file (gap.bat) used to launch GAP.The remainder of config.txt is used to specify TopSPIN options for a particular specification.One of these options is discussed in §2.5, and a complete overview of options is given in Chapter 3.A configuration file must always be present in the directory from where you invoke TopSPIN.
Youwill probably use different configuration files for different specifications, depending on the nature of thesymmetry associated with these specifications. However, since the gap, saucy and common attributes arelikely to be the same in all configuration files, it makes sense to keep a “skeleton” configuration filecontaining just these options, which you can then copy and extend for a given Promela specification.2.4Symmetry reduction with the fast strategyWhen you run TopSPIN, you can specify a symmetry reduction strategy for the tool to use.
The choiceof strategy influences the speed of symmetry reduction and the factor of reduction obtained though theuse of symmetry. Some strategies provide the maximum possible state-space reduction due to symmetry,at the expense of a slow state-space search. Other strategies are more lightweight, providing potentiallysub-optimal reduction, but executing more quickly.By default, TopSPIN uses the fast strategy. In a nutshell, when using this strategy TopSPIN attempts to work out an efficient symmetry reduction algorithm based on the type of symmetry associatedwith the input specification. The symmetry reduction algorithm used is approximate in the sense that itmay result in exploration of more than one state per symmetric equivalence class.2.4.1 Running TopSPINCopy config.txt, the basic configuration file created in §2.3, into the examples directory, and runTopSPIN on loadbalancer.p as follows:1C:\Program Files\TopSPIN_2.2\examples>cp ../config.txt .C:\Program Files\TopSPIN_2.2\examples>java -jar"C:\Program Files\TopSPIN_2.2\TopSPIN.jar" loadbalancer.pFile: loadbalancer.p-------------------------------------TopSPIN version 2.2-------------------------------------Configuration settings:Symmetry detection method: static channel diagram analysisUsing 0 random conjugatesTimeout for finding largest valid subgroup: 0 secondsReduction strategy: FASTUsing transpositions to represent permutations: trueUsing stabiliser chain for enumeration: trueUsing vectorisation: false-------------------------------------Typechecking input specification...Specification is well typed!Launching saucy via the following command: C:\Program Files\TopSPIN_2.2\saucy\saucy.exe -d"C:\Program Files\TopSPIN_2.2\Common\graph.saucy"Starting GAP with command: C:\gap4r4\bin\gap.bat -L"C:\Program Files\TopSPIN_2.2\Common\gapworkspace" -qThe group:G = <(3 4)(clients2 clients1),(3 2)(clients0 clients1),(servers1 servers0)(7 6),(5 4)(clients2 clients3)>is a valid group for symmetry reduction.Generating symmetry reduction algorithmsThe symmetry group has size 48Completed generation of sympan verifier which includes algorithms for symmetry reduction!To generate an executable verifier use the following command:gcc -o sympan sympan.c group.ctogether with SPIN compile-time directives for your specification.Execute the verifier using the following command:sympan.exetogether with SPIN run-time options for your specification.If TopSPIN does not produce output like this, then proceed to Chapter 6 to try to deduce what is wrong,and to file a bug report if necessary.The first part of the TopSPIN output specifies which version of the tool is being used, and howthe various tool options have been configured.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
