A.F. Donaldson - TopSPIN Version 2.2. Automatic symmetry reduction for the SPIN model checker. User Manual (798531), страница 7
Текст из файла (страница 7)
rest of Java stack traceSolution: Source code for saucy is included with the TopSPIN distribution, which can be downloadedvia the instructions of §1.2. However, you need to compile the saucy source code using GCC. To do this,follow the instructions given in §1.3.1.6.1.4 Path to saucy in configuration file is wrongProblem: From TopSPIN’s point of view this is the same as the previous problem. From your point ofview there is a difference: you may have correctly installed and compiled saucy, but but mistyped thepath to saucy in config.txt.Example error message:Error launching saucy with command: C:\Program Files\TopSPIN\saucy\tsaucy.exe -d"C:\Program Files\TopSPIN\Common\graph.saucy"java.io.IOException: CreateProcess: C:\Program Files\TopSPIN\saucy\tsaucy.exe -d"C:\Program Files\TopSPIN\Common\graph.saucy" error=2at java.lang.ProcessImpl.create(Native Method)... rest of Java stack traceNote that TopSPIN is trying to launch tsaucy.exe rather than saucy.exe, due to a typo in config.txt.Solution: Make sure saucy is correctly downloaded and compiled (§1.3.1), and ensure that config.txtcontains a line for saucy with exactly the absolute path to the tool (§2.3).6.1.5 GAP is not correctly installedProblem: You may not have correctly installed GAP, the computational group theory package on whichTopSPIN relies.Example error message:Starting GAP with command: C:\gap4r4\bin\gap.bat -L"C:\Program Files\TopSPIN\Common\gapworkspace" -qException in thread "main"java.io.IOException: CreateProcess: C:\gap4r4\bin\gap.bat -L"C:\Program Files\TopSPIN\Common\gapworkspace" -q error=2at java.lang.ProcessImpl.create(Native Method)...
rest of Java stack traceSolution: Download and install GAP from the GAP website. The URL for this website and the version ofGAP which TopSPIN supports are given in Figure 1.1 (§1.1).6.1.6 Path to GAP in configuration file is wrongProblem: From TopSPIN’s point of view this is the same as the previous problem. From your pointof view there is a difference: you may have correctly installed GAP, but mistyped the path to GAP inconfig.txt.Example error message:Starting GAP with command: C:\gap4r4\bin\tgap.bat -L"C:\Program Files\TopSPIN\Common\gapworkspace" -qException in thread "main"java.io.IOException: CreateProcess: C:\gap4r4\bin\tgap.bat -L"C:\Program Files\TopSPIN\Common\gapworkspace" -q error=2at java.lang.ProcessImpl.create(Native Method)...
rest of Java stack traceNote that TopSPIN is trying to launch tgap.bat rather than gap.bat, due to a typo in config.txt.Solution: Make sure you have correctly downloaded and installed GAP(§1.1), and ensure that config.txtcontains a line for GAP with exactly the absolute path to the tool (§2.3).6.1.7 Common directory does not exist, or user does not have permissions for this directoryProblem: The location of the TopSPIN Common directory has been specified incorrectly in commmon.txt.Example error message:Error while trying to create file "C:\Program Files\TopSPIN\Common\graph.saucy".Make sure that the directory C:\Program Files\TopSPIN\Common\ exists,and that you have write permission.Solution: Make sure that config.txt contains a line of the form common=name, where name is theabsolute path to the Common directory provided with the TopSPIN distribution.
Make sure this path hasnot been mistyped, and that the path includes a terminating slash.6.1.8 Path to Common directory does not have terminating slashProblem: The location of the TopSPIN Common directory has been specified without a final forward(Linux) or back- (Windows) slash.Example error message:Solution: Make sure that config.txt contains a line of the form common=name, where name is theabsolute path to the Common directory provided with the TopSPIN distribution. Make sure this path hasnot been mistyped, and that the path includes a terminating slash.6.1.9 Missing or corrupt GAP workspaceProblem: The file gapworkspace in the Common directory is either missing or corrupted.Example error message:Starting GAP with command: C:\gap4r4\bin\gap.bat -L"C:\Program Files\TopSPIN\Common\gapworkspace" -qError -- bad GAP workspace specified in configuration file.GAP produced errors:====================gap: Press <Enter> to end programEnd of GAP errorsSolution: Check that:1.
You have followed the instructions in §1.3.2 on creating a GAP workspace2. This workspace has been successfully saved in the Common directory3. You have not changed the version of GAP you are using since creating the workspace4. The workspace was created exactly the same machine, with the same operating system, on whichyou are running TopSPIN.6.1.10 GAP executable specified in configuration file, instead of shell script/batch fileProblem: You have specified the path to the GAP executable as the gap option in config.txt.Example error message:GAP produced errors:====================Error, the library file ’system.g’ must exist and be readable called fromCallFuncList( func, arg ); called fromRereadLib( "system.g" ); called from<function>( <arguments> ) called from read-eval-loopEntering break read-eval-print loop ...you can ’quit;’ to quit to outer loop, oryou can ’return;’ to continuebrk>Solution: Open config.txt and change the gap option to refer to the shell script (gap.sh) or batch file(gap.bat).6.1.11 SPIN is not correctly installedProblem: You have not correctly installed SPIN in such a way that the tool can be invoked by simplytyping spin, as discussed in §1.1.Example error message:An error occurred while constructing the "sympan" files.java.io.IOException: CreateProcess: spin -a loadbalancer.p error=2at java.lang.ProcessImpl.create(Native Method)...
rest of Java stack traceSolution: Make sure SPIN is correctly installed, and that the directory containing the SPIN executableis part of your path environment variable. Perhaps you have renamed spin to spin-linux or spin516;maybe you do not have execute permission for SPIN, or perhaps you have another application called spininstalled on your machine. Resolve these issues so that spin is all that needs to be typed to launch theSPIN tool.6.1.12 C preprocessor,cpp,unavailableProblem: TopSPIN uses the cpp program to expand #define and #include macros before processing aspecification.
If cpp is not available then TopSPIN can still be invoked, but cannot handle specificationswhich include these directives.Example error message:C preprocessor (cpp) not available - TopSPIN will not work correctly on files which use#define or #include.src.promela.lexer.LexerException: [1,1] Unknown token: #... rest of Java stack traceSolution: Install the cpp program on your system. Linux distributions provide cpp as standard; underWindows the cpp program is provided as part of Cygwin.
Make sure cpp is in your path.6.1.13 Typechecking error: problem with array indexProblem: By default, TopSPIN performs strict typechecking and only allows arrays to be accessed usingbyte or pid types.Example error message:Error at line 8: Type "int" cannot be used as an array index, it is not a subtype of "byte".Solution: You can use the -relaxedarrayindexing option to make this error go away (see §3.2.3),or refactor your specification so that arrays are indeed only indexed by byte or pid expressions: thismay make the associated state-vector smaller.6.1.14 Typechecking error: problem with assignment to numeric variableProblem: By default, TopSPIN performs strict typechecking and only allows a variable to be assigneda value of a “smaller” type, e.g.
assignment of byte to short is OK, but not the other way round.Sometimes this is too restrictive.Example error message:Error at line 8: invalid assignment -- Type "short" occurs in a context where it is required to be a subtype oSolution: You can use the -relaxedassignment option to make this error go away (see §3.2.4), orrefactor your specification so that assignments to numeric variables are always from expressions with asmaller type: this may make the associated state-vector more compact.6.1.15 Error during verification: “bad proctype”Problem: Verification quits with a “bad proctype” error message.Example error message:pan: bad proctype - collapse (at depth 1023)Solution: This error can occur if your specification involves proctypes which terminate.
See §4.2 for details of this, and for a technique to prevent SPIN processes from terminating by providing an inescapablefinal state. This error message will only be generated if COLLAPSE compression is used. Nevertheless,for reasons explained in §4.2 it is best to apply TopSPIN to systems of non-terminating processes.6.2Reporting bugs in TopSPINIf you have a problem using TopSPIN, first check to see if your problem is covered by one of the commonproblems in §6.1.
If this is not the case, then please take the time to report your bug to the TopSPINdevelopers, so that it can be immediately documented and ultimately fixed, for the benefit of you andother TopSPIN users.Bug reports should be submitted using the contact details in §6.4. Please provide the followingwhen reporting a bug:••••A description of the problemA test-case (example Promela specification and config.txt file) which exposes the problemThe TopSPIN version you are using, the approximate date on which you downloaded TopSPINDetails as to whether you are using a pre-compiled version of TopSPIN, or a version you havecompiled from source• Any ideas you have as to what may have gone wrong!Please note that bugs do not have to relate to the correctness of TopSPIN – a valuable bug reportcould be in response to a misleading error message generated by TopSPIN, where there is somethingwrong with the input specification, but the problem is not what the error message indicates.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
