A.F. Donaldson - TopSPIN Version 2.2. Automatic symmetry reduction for the SPIN model checker. User Manual (798531), страница 5
Текст из файла (страница 5)
This is illustrated in Figures 4.3 and 4.4. Processes in Figure 4.3 areparameterised by a byte identifier, which they use to index the st array. SymmExtractor is not yet sophisticated enough to work out the correspondence between the id parameter and the built-in identifierfor each process. However, the specification can be converted into a form which SymmExtractor can handle, as shown in Figure 4.4. The disadvantage here is that position 0 of the array st is un-used, meaningthat an array of size three rather than two is required, increasing the state-vector size by one byte. Onthe other hand, eliminating the id variables reduces the state-vector by two bytes, so the re-modellingworks well for this example.4.4Restrictions on channels∗For simplicity, TopSPIN does not allow channel initialisers to be associated with channels which aredeclared locally to a proctype, and does not currently support arrays of channels.4.5Never claims, trace/notrace constructs,acceptandprogresslabelsThese are method for specifying liveness properties in a Promela model.
TopSPIN is not yet compatible with verification of liveness properties, so you will get an error if you try to apply TopSPIN to aspecification containing one of these constructs.Symmetry detection is still possible with liveness verification constructs. It is OK to applyTopSPINto a specification containing a liveness construct with the -detect option (see §6.4). Thetool will tell you any symmetries it detects; it’s just not yet possible to exploit these symmetries whenmodel checking.4.6Exclusive send/recieve (xs/xr) channel assertionsThis is not actually a restriction, rather a warning for users wishing to use these keywords.Promela includes keywords xr and xs, which stand for exclusive receive and exclusive send respectively.
A process can include a declaration ‘xr name’, where ‘name’ is the name of a previouslydeclared channel, to indicate that only this process can receive messages on the channel. The xs keyword is used similarly. Providing SPIN with this information can lead to more efficient partial-orderreduction.
It is not possible to check, statically, whether xs and xr are used correctly, but incorrect usesare flagged by SPIN during verification. These keywords do not affect the presence of symmetry in themodel associated with a specification, so are no problem for symmetry detection.However, there is a potential problem with exploiting xs/xr information in conjunction withsymmetry reduction, described in Appendix C.1.1 of Donaldson’s thesis.
In practice, the problem withthese keywords is unlikely to cause problems: there is a slim chance that if the keywords are usedincorrectly, symmetry reduction will prevent this from being flagged up during verification. Therefore,TopSPIN does allow these features to be used, but it is the user’s responsibility to use them with care.4.7Unsigned data type∗Promela supports an unsigned numeric type. A declaration of the form unsigned x : y declares aninteger variable x which takes non-negative values which can be represented using y bits.
Clearly the useof this data type will have no effect on our symmetry detection/reduction techniques. However, TopSPINis integrated with an enhanced Promela type checker which does not currently support the unsigneddata type. A temporary fix for this omission is to replace each occurrence of the unsigned keyword withone of the other numeric types during symmetry detection.4.8Sorted send, random receive (!! and??operators)Promela provides alternative channel operators: !! (sorted send) and ?? (random receive). Sending dataon a buffered channel using !! causes messages to be queued on the channel in sorted order.
Messagescan be retrieved from the buffer in a random order using ??. These operators provide a useful alternativeto FIFO channel semantics. They also aid state-space reduction: storing channel contents in a sortedmanner can be seen as a form of state canonicalisation. However, storing pid messages in a sortedqueue imposes an ordering on the set of process identifiers. It is not immediately clear whether thisordering has an effect on symmetry.For the time being, TopSPIN allows the !! and ?? operators to be used, but they should be usedwith care.
If you get weird symmetry reduction results using these operators then please get in touch(§6.4).4.9Embedded C codeRecent versions of SPIN allow C code to be embedded in a Promela specification, and certain variablesfrom the C part of the specification to be included in the SPIN state-vector. Automatic symmetry detectionfor this mix of C and Promela is beyond the scope of TopSPIN at present.4.10 Breadth-first search∗TopSPIN has not been tested with breadth-first search, and will give an error message if sympan.c iscompiled with -DBFS.(5.1Compiling from SourceDownloading TopSPIN source codeThe TopSPIN source code is stored in a Subversion repository, hosted by the Department of ComputingScience at the University of Glasgow at the following URL:https://ouen.dcs.gla.ac.uk/repos/symmetry/Use subversion to check out the TopSPIN source code to an appropriate location:C:\prog>svn checkout https://ouen.dcs.gla.ac.uk/repos/symmetry/trunk TopSPINSourceA TopSPINSource/TestModelsA TopSPINSource/TestModels/EtchTestingA TopSPINSource/TestModels/EtchTesting/ParsePassTestsA TopSPINSource/TestModels/EtchTesting/ParsePassTests/petersonA TopSPINSource/TestModels/EtchTesting/ParsePassTests/helloA TopSPINSource/TestModels/EtchTesting/ParsePassTests/pathfinderA TopSPINSource/TestModels/EtchTesting/ParsePassTests/snoopyA TopSPINSource/TestModels/EtchTesting/ParsePassTests/mobile1A TopSPINSource/TestModels/EtchTesting/ParsePassTests/mobile2A TopSPINSource/TestModels/EtchTesting/ParsePassTests/pftpA TopSPINSource/TestModels/EtchTesting/ParsePassTests/leaderA TopSPINSource/TestModels/EtchTesting/ParsePassTests/loops...A TopSPINSource/Common/Minimising.gapA TopSPINSource/Common/parallel_symmetry_cell_ppu.cA TopSPINSource/Common/Verify.gapA TopSPINSource/Common/WorkspaceGenerator.gapA TopSPINSource/Common/parallel_symmetry_cell_spu.cA TopSPINSource/Common/parallel_symmetry_cell_ppu.hA TopSPINSource/symmextractor_common_config.txtChecked out revision 75.5.2Generating the Promela parserTopSPIN is based on a Promela parser which is constructed using the SableCC parser generator.
Download SableCC version 3.2 from the Sable website1 , and generate the parser as follows (adapting thecommand according to where you have installed SableCC):java -jar C:\sablecc-3.2\lib\sablecc.jar promela.grammarThis command should result in output similar to the following:C:\prog\TopSPINSource>java -jar C:\sablecc-3.2\lib\sablecc.jarpromela.grammarSableCC version 3.2 Copyright (C) 1997-2003 Etienne M.
Gagnon <etienne.gagnon@uqam.ca>and others. All rights reserved.This software comes with ABSOLUTELY NO WARRANTY. This is free software,and you are welcome to redistribute it under certain conditions.Type ’sablecc -license’ to view the complete copyright notice and license.-- Generating parser for promela.grammar in C:\prog\TopSPINSourceAdding productions and alternative of section AST.Verifying identifiers.Verifying ast identifiers.Adding empty productions and empty alternative transformation if necessary.Adding productions and alternative transformation if necessary.computing alternative symbol table identifiers.1.http://sablecc.org/Verifying production transform identifiers.Verifying ast alternatives transform identifiers.Generating token classes.Generating production classes.Generating alternative classes.Generating analysis classes.Generating utility classes.Generating the lexer.State: INITIAL- Constructing NFA.............................................................................................................................................................- Constructing DFA.............................................................................................................................................................- resolving ACCEPT states.Generating the parser.............................................................................................................................................................Due to a bug in SableCC, it is then necessary to apply a patch file to the generated parser.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
