A.F. Donaldson - TopSPIN Version 2.2. Automatic symmetry reduction for the SPIN model checker. User Manual (798531), страница 4
Текст из файла (страница 4)
short) to a “smaller” integer type(e.g. bit). This is to prevent arithmetic overflow where possible.So, for example, the following code snippet will cause a type error:byte k;k = -1;due to the fact that -1 has type short, which is a larger type than byte.Because SPIN is not as strict as this, practical examples may rely on this kind of assignment. Forthis reason, specifying -relaxedassignment on the command line tells TopSPIN to allow a variableof any numeric type to be assigned the result of an expression of any numeric type.As in §3.2.3, note that where possible, smaller numeric types should be used for reasons ofefficiency.
If you find you need the -relaxedassignment option then consider whether you couldrefactor your specification to use smaller types, removing the need for this option and reducing the sizeof the state-vector.3.3Mandatory configuration file options3.3.1 saucyString option specifying path to the saucy program. This option must be set by the user.3.3.2 commonString option specifying path to the Common directory, which is part of the TopSPIN distribution. Thisoption must be set by the user.3.3.3 gapString option specifying path to the GAP program. This option must be set by the user.3.4Configuration file options for symmetry detection3.4.1 explainTopSPIN detects symmetry by finding the static channel diagram for the input specification, computingits symmetries, and checking these symmetries for validity against the Promela specification.
Somesymmetries may not be valid: TopSPIN will try to compute the largest valid set of static channel diagramsymmetries.If you have written a specification which you expect to be symmetric, but for which TopSPINreports invalid symmetries, it may be interesting to inspect the reason for this invalidity: it could indicatea typo in the specification, a misunderstanding on the part of the user, or a limitation of TopSPIN.Setting explain to a positive integer n tells TopSPIN to output explanations for the first ninvalid symmetries. An “explanation” for an invalid symmetry α consists of a pair of text files, onecalled m original.txt, the other m permuted.txt (where m < n). The original file showsthe input specification before α is applied, then shows the specification after normalization has takenplace. The permuted file shows the input specification after α has been applied, then shows the permutedspecification after normalization.
TopSPIN regards a symmetry as valid if these normalized specificationsare the same, so obviously they will not be identical for α.The two text files can be compared with a diff tool (e.g. the excellent WinMerge1 ). Looking atthe differences in the normalized parts should be instructive as to why the given symmetry is not valid.By way of example, here is a mutual exclusion specification with five processes:mtype = {N,T,C}mtype st[6]=Nproctype user() {do:: d_step { st[_pid]==N -> st[_pid]=T }:: d_step { st[_pid]==T &&(st[1]!=C && st[2]!=C && st[1]!=C && st[4]!=C && st[5]!=C)-> st[_pid]=C}:: d_step { st[_pid]==C -> st[_pid]=N }od}init {atomic {run user();run user();run user();run user();run user();}}Running TopSPIN on this example, in verbose mode and with explain=1, produces outputincluding the following:Saucy computed the following generators for Aut(SCD(P)):Aut(SCD(P)) = <(3 2),(2 1),(3 4),(5 4)>-------------------------------------Computing valid generators:(3 2) : not validgenerating explanation in files 0_original.txt and 0_permuted.txt(2 1) : not valid(3 4) : not valid(5 4) : valid--------------------------------------The tool has determined that the symmetry (3 2) which swaps user processes 3 and 2 is notvalid, and has written an explanation to the files 0_original.txt and 0_permuted.txt.Figure 3.1 shows the results of comparing these files with WinMerge.
This should alert the userto the fact that the operand st[1] != C appears twice in the highlighted boolean expression: this isclearly a mistake – one of these operands should be changed to st[2] != C to restore full symmetryand presumably correct the model.This illustrates the idea that presence of symmetry can actually be a correctness requirement inits own right.Default value: 0, i.e. no explanations will be given.3.4.2 timeboundWhen detecting symmetry, TopSPIN may use a coset search to try to improve upon the initially computedgroup of symmetries. This search can be time-consuming on particular examples.
The timeboundinteger option limits the length of time dedicated to this search to a maximum number of seconds.Default value: 0, which is used to specify that the coset search should be unbounded.3.4.3 conjugatesIf the coset search is taking a long time, it is sometimes possible to speed things up by picking a number of candidate symmetries at random, finding the conjugate of each known valid generator by these1.http://www.winmerge.org/Figure 3.1: Comparing text files output by the explain option to see why symmetry (3 2) is not valid.random elements, and then testing the conjugates for validity.
This is based on the practical observationthat valid symmetries are often conjugate to other valid symmetries. The conjugates integer optionis used to specify how many conjugates to use.Default value: 0. If symmetry detection is slow, try 5 conjugates.3.4.4 symmetryfileSometimes TopSPIN is unable to automatically detect symmetry from an input specification even thoughthe user knows that symmetry exists.
In this case, it is possible to specify a file containing generators for asymmetry group. The name of this file is specified via the symmetryfile option. If symmetryfileis set, TopSPIN will not attempt automatic symmetry detection, and will use the given group of symmetries for symmetry reduction.Default value: no file specified, automatic symmetry detection will be attempted..3.5Configuration file options for symmetry reduction3.5.1 strategyString option specifying the strategy to use for symmetry reduction. Options are: fast, enumerate, hillclimbing, segment, flatten, exactmarkers, approxmarkers.Default value: fast.3.5.2 transpositionsBoolean option stating whether to apply group elements as transpositions.Default value: true.3.5.3 stabiliserchainBoolean option stating whether to use a stabiliser chain for enumeration.Default value: true.3.5.4 vectoriseBoolean option stating whether to use vector SIMD instructions for symmetry reduction.
The nature ofthe resulting vector code depends on the target configuration file option (see §3.5.7).Default value: false.3.5.5 paralleliseBoolean option stating whether to parallelise symmetry reduction using pthreads.Default value: false.3.5.6 coresInteger option stating the number of cores available for parallel symmetry reduction.Default value: 1.3.5.7 targetString option specifying the target to use for vector and parallel symmetry reduction.
Options are: PC,CELL, POWERPC.Default value: not set by default.3.6Configuration file options for usability3.6.1 profileProfile the performance of TopSPIN?Default value: false.3.6.2 verboseDisplay progress of TopSPIN in detail?Default value: false.3.6.3 quietSuppress non-vital output?Default value: false.4LimitationsBefore using TopSPIN for advanced verification it is important to understand what can and cannot bedone with the tool.
TopSPIN places various restrictions on the form a Promela specification may have.Also, certain SPIN options are not (yet) compatible with symmetry reduction.This section briefly described the limitations of TopSPIN. Limitations marked with an asteriskcould be removed with relative ease: they just haven’t been dealt with yet.
If you’re working with SPINand TopSPIN and are being hindered by these restrictions then please get in tough (see §6.4) and effortswill be made to add appropriate features to TopSPIN.4.1Process instantiation and dynamic process creationTopSPIN requires all processes to be instantiated using run statements within an init process. The formof the init process must be:init {atomic {run ...;run ...;...run ...;<other statements>}}i.e. all process must be started atomically, and must come before any other statements in the init process(e.g.
initialisation code), which must also appear within the atomic block.In particular, TopSPIN does not support process instantiation using the active keyword, or viarun statements outside the init process.If a specification relies on dynamic process creation then it may be possible to re-model theprocesses as shown in Figures 4.1 and 4.2. Figure 4.1 shows a specification which instantiates copiesof proctype P dynamically. Assuming that 3 is an upper bound for the number of instances of P whichshould be running at any time, Figure 4.2 shows an alternative way of expressing the specification.
Theproctype P now includes a channel parameter, and an instance of P waits until it can receive on thischannel before executing its body. Its body is identical to the original, except that it includes a final gotoproctype P() {/* body */}proctype Q() {...run P();...}Figure 4.1: Skeleton Promela specification with dynamic process creation.chan wakeup_P_1 = [0] of {bit};chan wakeup_P_2 = [0] of {bit};chan wakeup_P_3 = [0] of {bit}proctype P(chan start) {sleep:start?1;/* body */goto sleep}proctype Q() {...if :: wakeup_P_1!1:: wakeup_P_2!1:: wakeup_P_3!1fi;...}init {atomic {/* original ‘run’ statements */run P(wakeup_P_1);run P(wakeup_P_2);run P(wakeup_P_3)}}Figure 4.2: Re-modelled Promela specification without dynamic process creation.statement after which it returns to its initial configuration.1 The init process instantiates three copiesof P , each with a distinct synchronous channel.
Instead of instantiating a copy of P , the proctype Qnow offers the literal value 1 to all channels on which instances of P may be listening. The exampleof Figures 4.1 and 4.2 can be adapted to handle multiple process types, with any fixed upper bound foreach process type.4.2Process terminationTechnically, process termination destroys symmetry in a Promela specification. SPIN only allows processes to terminate in reverse order. So, if five identical, terminating client proctypes are launchedsimultaneously with process identifiers in the range {1, 2, 3, 4, 5}, the processes will terminate one-byone in a fixed order: 5, 4, 3, 2, 1. This ordering on process identifiers breaks symmetry between theprocesses.Furthermore, the way symmetry reduction is implemented in TopSPIN is not strictly compatiblewith process termination.
After the initial state, TopSPIN assumes a fixed set of running processes. Ifa process dies, TopSPIN may try to exchange this processes’s state with that of another process whencomputing symmetry representatives, and this can (very occasionally) lead to verification-time errors(see §6.1.15).If you want to work with terminating processes, you can insert a dummy termination state at theend of each proctype using a line like the following:end_ok: false1. This goto statement should really be part of an atomic block which also resets any local variables of the proctype to theirinitial values.mtype = {N,T,C}mtype st[2]=Nproctype user(byte id) {do:: d_step { st[id]==N -> st[id]=T }:: d_step { st[id]==T && st[0]!=C && st[1]!=C -> st[id]=C }:: d_step { st[id]==C -> st[id]=N }od}init {atomic {run user(0);run user(1);}}Figure 4.3: Promela specification which uses user-defined process identifiers.mtype = {N,T,C} mtype st[3]=N;proctype user()do:: d_step {:: d_step {:: d_step {od}{st[_pid]==N -> st[_pid]=T }st[_pid]==T && st[1]!=C && st[2]!=C -> st[_pid]=C }st[_pid]==C -> st[_pid]=N }init {atomic {run user();run user();}}Figure 4.4: Re-modelled specification which uses the _pid variable.The end label ensures that SPIN will not complain about instances of the proctype blocking atthis label, and the false statement ensures that proctype instances will never truly terminate.4.3The_pidvariable should be usedFor symmetry to be detected, it is important for proctypes to use their built-in _pid variable rather thana user-defined process identifier.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
