A.F. Donaldson - TopSPIN Version 2.2. Automatic symmetry reduction for the SPIN model checker. User Manual (798531), страница 3
Текст из файла (страница 3)
These options have all been set to default values. For now,simply note that the fast strategy is being used.The tool then typechecks the input specification, reporting that the specification is well-typed.After typechecking, the saucy and GAP programs are launched, to perform automatic symmetrydetection. Note that the paths to these tools have been taken from the configuration file.
The saucytool is passed the -d option to indicate that the graph it will operate on is directed. A temporary file,graph.saucy, is also passed to the program: this is a graph generated by TopSPIN from which symmetriesof loadbalancer.p are derived. The GAP package is launched with the -L option to indicate that aworkspace (§1.3.2) should be loaded. The path to this workspace – gapworkspace inside the Commondirectory – is also passed to GAP. The -q operation launches GAP in quiet mode, which improves theefficiency of communication between the GAP and Java components of TopSPIN.1.
For reasons of space, some lines in the TopSPIN output have been wrapped. Also note that the output on your system willvary slightly according to the paths you have specified in config.txt.TopSPIN successfully computes generators for a group of symmetries associated with the loadbalancer specification. From the generators of this group, it can be seen that there is full symmetrybetween the client processes, as well as symmetry between the server processes. TopSPIN then goes onto generate symmetry reduction algorithms for this group, reporting that the number of symmetries is48 (4! symmetries between the clients, and 2 symmetries between the servers, leads to 24 × 2 = 48symmetries overall).The end of the TopSPIN output details how the C files generated by SPIN and TopSPIN should becompiled and executed.2.4.2 Compiling and executing the sympan verifierThe examples directory should now contain a number of files, including sympan.c and group.c. Thesympan.c file is a modified version of the pan.c file produced by SPIN, which includes symmetry reduction algorithms.
The group.c file includes functions for manipulating permutations.Compile and execute this verifier using commands analogous to those shown in §2.2:C:\Program Files\TopSPIN_2.2\examples>gcc -o sympan -O2 -DSAFETY sympan.c group.cC:\Program Files\TopSPIN_2.2\examples>sympan -m100000(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 2323, errors: 04960 states, stored12254 states, matched17214 transitions (= stored+matched)6 atomic stepshash conflicts:35 (resolved)5.735memory 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.369 seconds pan: rate 13441.734 states/secondComparing this model checking result with the result without symmetry reduction (§2.2) shows thatthe fast strategy leads to a state-space reduction factor of 34.5.
The theoretical maximum symmetryreduction factor is 48, which is the size of the symmetry group computed by TopSPIN, so this is areasonably good result. Notice that speedup factor is just 2.2, and as a result the states/second rate forverification is significantly lower when symmetry reduction is applied.2.5Symmetry reduction with the enumerate strategyAlthough the fast strategy provides effective symmetry reduction for the loadbalancer example, thestrategy does not provide space-optimal symmetry reduction.
The enumerate strategy, on the other hand,is guaranteed to provide full symmetry reduction.To use the enumerate strategy, open config.txt in the examples directory, and add the following line:strategy=enumerateThis additional option tells TopSPIN to use the enumerate strategy over the default fast strategy.Now apply TopSPIN to the loadbalancer specification, and compile and run the generated verifier:C:\Program Files\TopSPIN_2.2\examples>java -jar"C:\Program Files\TopSPIN_2.2\TopSPIN.jar" loadbalancer.p...
TopSPIN output ...C:\Program Files\TopSPIN_2.2\examples>gcc -o sympan -O2 -DSAFETY sympan.c group.cC:\Program Files\TopSPIN_2.2\examples>sympan -m100000(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 1916, errors: 04213 states, stored11181 states, matched15394 transitions (= stored+matched)6 atomic stepshash conflicts:23 (resolved)5.638memory 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.647 seconds pan: rate6511.592 states/secondVerification using the enumerate strategy provides a better reduction factor: 40.6 vs.
34.5 with the faststrategy (§2.4). This comes at an expense: the speedup factor is reduced from 2.2 for the fast strategyto 1.3. For specifications with more symmetric components, this time penalty is more significant: theenumerate strategy works by applying every symmetry associated with the input specification to everystate encountered during model checking. Since a specification with n symmetric components has asymmetry group of size at least n!, use of the enumerate strategy quickly becomes infeasible.2.6Summary so farYou should now have successfully installed TopSPIN and its prerequisite components, created a configuration file, and applied the tool to a Promela example. If you have encountered any problems during thisprocess then proceed to Chapter 6 for troubleshooting ideas and information on how to report TopSPINbugs.At this stage, you may have learned all you need to know about TopSPIN for your basic symmetry reduction needs.
Chapters 3 and 5 are for advanced users who wish to explore TopSPIN’s moresophisticated options, and compile the tool from source, respectively.3Overview of OptionsThis chapter will be expanded into a complete reference for the various TopSPIN options. At the moment,every option is listed, but some of the descriptions are minimal.3.1Online helpRunning TopSPIN with a single argument, help, displays a list of command-line switches and configuration file options for which short help messages can be generated.Running TopSPIN with two arguments, help <option>, where <option> is one of theoptions for which help is available, displays a short message describing the function of the option.3.2Command-line options3.2.1 -checkApply this switch to just type-check a specification.
Type checking will be symmetry-aware: the checkerwill report errors if the specification contains features which will cause symmetry detection to fail, e.g.arithmetic on pid variables, or absence of an init process.When using the -check option it is not necessary to use config.txt, as the typecheckingprocess does not depend on other tools or options.3.2.2 -detectApply this switch to type-check and detect symmetry for a specification, but not apply symmetry reduction. TopSPIN will report the symmetries it computes, indicating whether there are problems in detectingsymmetry. This option can be useful if you want to find out the extent to which symmetry is present ina model, but not actually do symmetry reduction.Because this option does not require the output of symmetry reduction algorithms, TopSPINwill detect symmetries for specifications containing features which are not supported for symmetryreduction, e.g.
a never claim. The idea here is that these features could, in principle, be supportedfully, and determining whether symmetry is present may still be of interest.3.2.3 -relaxedarrayindexingTopSPIN is based on the ETCH typechecker, which tries to help modellers improve the quality of theirspecifications by performing relatively strict type-checking. In particular, ETCH does not allow an arrayto be indexed by an expression with a numeric type larger than byte.
This is because the maximumsize of an array in Promela is 255, which is also the largest byte value.So, for example, the following code snippet will cause a type error:mtype myArray[12];int x;x = ...;myArray[x] = ...due to the fact that myArray has been indexed by x, which has type int.Sometimes, in practice, it is useful to index an array using a larger type than byte, e.g. so that anon-byte value like -1 can be used to represent a null index.
For this reason, TopSPIN can be passed the-relaxedarrayindexing command-line option, instructing the tool to allow indexing of arrays byexpressions of any numeric type.Note that the efficiency of a verification model can be improved by using smaller types: anint takes up more state-vector space than a byte, so the user should consider re-modelling theirspecification to use byte variables to index arrays where possible.3.2.4 -relaxedassignmentAs with array indexing, TopSPIN performs strict typechecking of numeric assignments by default, andrejects assignments from an expression of a “large” integer type (e.g.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
