A.F. Donaldson - TopSPIN Version 2.2. Automatic symmetry reduction for the SPIN model checker. User Manual (798531), страница 6
Текст из файла (страница 6)
Dothis by executing the following command (you will need to have PERL installed: if you don’t, you couldeasily re-write the PERL script in your favourite language!).C:\prog\TopSPINSource>perl apply_patch.pl5.3Compiling and creating a jarYou have now downloaded and generated all the Java source code for TopSPIN, and can proceed tocompile this source code. The javac compiler and jar utility are required to compile the source andcreate an executable jar file respectively.
The source code is all contained in directories within src.5.3.1 CompilingThere are two options for compilation:1. Create an Eclipse project from the TopSPIN source code, in which case Eclipse will automaticallycompile the code.2. Use the make utility and the supplied Makefile to compile the source code, by typing the command make classes in the TopSPIN root directory. The provided Makefile uses the sed andfind utilities, which are provided as standard with Linux, and are available on Windows viaCygwin.Compiling the source code using the Makefile gives output along the following lines:C:\prog\TopSPINSource>make classesjavac src/etch/checker/Check.javaNote: .\src\promela\parser\Parser.java uses unchecked or unsafe operations.Note: Recompile with -Xlint:unchecked for details.javac src/etch/checker/CheckerTest.javajavac src/etch/testing/EtchTestCase.javajavac src/etch/testing/EtchTester.javajavac src/group/Group.javajavac src/promela/analysis/ReversedDepthFirstAdapter.javajavac src/symmextractor/InlineReplacer.javajavac src/symmextractor/SymmExtractor.javajavac src/symmextractor/testing/SymmExtractorFailTestOutcome.javajavac src/symmextractor/testing/SymmExtractorRunTestOutcome.javajavac src/symmextractor/testing/SymmExtractorTestCase.javajavac src/symmextractor/testing/SymmExtractorTester.javajavac src/symmreducer/testing/ModelCheckingResult.javajavac src/symmreducer/testing/SymmReducerFailTestOutcome.javajavac src/symmreducer/testing/SymmReducerTestCase.javajavac src/symmreducer/testing/SymmReducerTester.javajavac src/testing/RunAllTests.javaNote the compile warnings generated for Parser.java: these are due to code generated by SableCC.All other files should compile without warnings.5.3.2 Creating a jar fileIf you are using Eclipse then you can create an executable jar file for TopSPIN by exporting your TopSPINproject as a jar, and selecting src.TopSpin as the main class.If using the supplied Makefile, typing make jars will produce two jar files:C:\prog\TopSPINSource>make jarsjar cmf manifest.txt TopSPIN.jar src/etch/checker/Check.class src/etch/checker/Checker.class...
<many .class files> ...src/utilities/Strategy.class src/utilities/StringHelper.class src/promela/lexer/lexer.datsrc/promela/parser/parser.dat && echo "TopSPIN.jar built successfully."TopSPIN.jar built successfully.jar cmf tests_manifest.txt TopSPINTests.jar src/etch/checker/Check.classsrc/etch/checker/Checker.class... <many .class files> ...src/utilities/Strategy.class src/utilities/StringHelper.class src/promela/lexer/lexer.datsrc/promela/parser/parser.dat && echo "TopSPINTests.jar built successfully."TopSPINTests.jar built successfully.Note that you can skip the make classes step, and type make jars to both compile the Java files andproduce jar files. To delete all jar and class files, use make clean.5.4Try your compiled version on an exampleNow that you have successfully compiled a jar file from the TopSPIN source, you are effectively in thesame position as a user who has downloaded the TopSPIN jar file using the instructions given in §1.2.
Ofcourse, you have the advantage of being able to modify TopSPIN to suit your purposes!The next steps involve compiling saucy, creating a GAP workspace, and testing TopSPIN on asimple example. Therefore you should work your way through Chapters 1 and 2, using your compiledjar file in place of the downloaded jar file.5.5Acceptance TestsThe TopSPIN source checkout includes a reasonably large set of acceptance tests. It is highly recommended that you run these tests using the instructions below before commencing any development workon TopSPIN – passing the acceptance tests confirms that you are starting from a stable base. The acceptance tests can also be run regularly during development, to ensure that the addition of new features toTopSPIN does not adversely affect the tool’s existing features.Important Before running the acceptance tests, make sure that the GCC tool is installed in such a waythat it can be invoked by name from a command prompt, i.e.
so that typing gcc will launch GCC. Tocheck this, try typing gcc from a fresh prompt. You should see something like:C:\>gccgcc: no input files5.5.1 Setting up a configuration file for testingThe TopSPIN test suite uses a called symmextractor_common_config.txt for some configuration options which apply to most tests. Open this file, and edit the gap line to use the appropriate commandfor your setup. You should not have to change the Common or saucy lines: the source code checkoutis organised so that the saucy and Common directories are sub-directories of the directory in whichsymmextractor_common_config.txt is contained.5.5.2 Running the testsYou can now run the acceptance tests via the TopSPINTests.jar file:java -ea -jar TopSPINTests.jar 2> temp.txtThe -ea argument switches on assertion checking, which is useful for finding potential problems withTopSPIN.
The final part of the command, 2> temp.txt, pipes error messages generated during testingto the file temp.txt. This is useful since many of the tests are fail tests, which check that the TopSPINtypechecker correctly rejects Promela specifications which are not suitable for processing by TopSPIN.Redirecting these error messages to a text file means that the screen is not cluttered with error messages.You should see something like this when you run the tests:ETCH TESTS==========[PASS] expected[PASS] expected[PASS] expected[PASS] expected[PASS] expected[PASS] expected...andandandandandandSYMMEXTRACTOR TESTS===================[PASS] expected and[PASS] expected and[PASS] expected and[PASS] expected and[PASS] expected and...SYMMREDUCER TESTS=================[PASS] expected[PASS] expected[PASS] expected[PASS] expected[PASS] expected...andandandandandactual:actual:actual:actual:actual:actual:BadlyTyped, file: TestModels/EtchTesting/FailTests/failrec...WellTyped, file: TestModels/EtchTesting/PassTests/testtele...WellTyped, file: TestModels/EtchTesting/PassTests/test_ex_...WellTyped, file: TestModels/EtchTesting/PassTests/testtele...BadlyTyped, file: TestModels/EtchTesting/FailTests/faildup...ParsePass, file: TestModels/EtchTesting/ParsePassTests/pet...actual:actual:actual:actual:actual:(well typed, group size =(well typed, group size =BreaksRestrictions, file:(well typed, group size =BreaksRestrictions, file:actual:actual:actual:actual:actual:((well((well((well((well((welltyped,typed,typed,typed,typed,groupgroupgroupgroupgroupsizesizesizesizesize72, coset search: no), file: Tes...1296, coset search: no), file: T...TestModels/SymmExtractorTests/Ba...3628800, coset search: no), file...TestModels/SymmExtractorTests/Ba...=====120, coset search: no), no.
sta...3628800, coset search: no), no....6, coset search: no), no. state...5040, coset search: no), no. st...720, coset search: no), no. sta...Summary:238 passes0 failsAcceptance tests passed - you may commit your changes!There are in the order of 250 test cases. These are divided into ETCH tests, which test the typechecking component of TopSPIN; SymmExtractor tests, which check the symmetry detection capabilities ofthe tool, and SymmReducer tests, which perform symmetry reduction on Promela examples, checkingthat verification results for these examples are as expected. The ETCH tests run very quickly, the SymmExtractor tests run at a moderate speed, and the SymmReducer tests run fairly slowly. Testing takesapproximately 10 minutes on an average PC.5.5.3 Problems running the testsIf you have compiled a fresh checkout of TopSPIN then all of the acceptance tests should pass, sincetheir passing is a condition for committing changes to the source code repository. Therefore, if you haveany problems running the tests this is likely due to a problem with the way you have set up GAP, saucy,SPIN, or GCC.
Have a look at §6.1 which details common problems encountered when using TopSPIN. Iftest cases continue to fail then please send a bug report to the TopSPIN development team: see §6.2 fordetails.6Troubleshootingand Bug ReportingThis section includes a list of common problems with the use of TopSPIN. Please also refer to currentlimitations of TopSPIN, in Chapter 4.6.1Common problems6.1.1 Missing configuration fileProblem: There is no file named config.txt in your working directory when you run TopSPIN.Example error message:Error opening configuration file "config.txt", which should belocated in the directory from which you run TopSPIN.Solution: Follow the instructions in §2.3 on how to create config.txt.6.1.2 Incomplete configuration fileProblem: The file config.txt does not contain entries for all of the mandatory options, gap, saucy andcommon.Example error message:No configuration specified for GAP.No configuration specified for saucy.No common directory specified.Solution: Follow the instructions in §2.3 on how to create config.txt with these mandatory options.6.1.3 The saucy program is not correctly installedProblem: You may not have correctly installed and compiled saucy, the graph automorphism programon which TopSPIN relies.Example error message:Error launching saucy with command: C:\Program Files\TopSPIN\saucy\saucy.exe -d"C:\Program Files\TopSPIN\Common\graph.saucy"java.io.IOException: CreateProcess: C:\Program Files\TopSPIN\saucy\saucy.exe -d"C:\Program Files\TopSPIN\Common\graph.saucy" error=2at java.lang.ProcessImpl.create(Native Method)...
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
