A forum for Spin users
You are not logged in.
i am trying to extract a state machine from c code. I am following the manuals but having some problem. can anyone tell me how to install FeaVer/modex and spin in ubuntu or windows?
thanks in advance.
Offline
u gave the link for Spin. i have done exactly like this website. but after installing when i run spin -V it said it doesnot find the command spin.
I have seen in a document that FeaVer/modex have a GUI version. do u know anything about it?
Offline
i have install it in /usr/local/bin/spin
inside spin i have,
Doc, iSpin,Man,Samples,Src6.1.0,Test, directory....
when ever i try to run:
spin -V
it give the following mgs:
milon@milon-VirtualBox:~$ spin -V
No command 'spin' found, did you mean:
Command 'spim' from package 'spim' (universe)
Command 'spine' from package 'cacti-spine' (universe)
spin: command not found
Offline
The only thing that should be installed in /usr/local/bin/ is the executable 'spin' command itself, not the entire distribution directory.
(i.e., you compile spin somewhere else and just copy 'spin' itself into this directory).
Please ask a system administrator for your system for help if this looks mysterious.
Offline
finally i have done it.
spin is oki. modex is oki.now i have to go on...
thanks for ur help.
Offline
hello admin, i think u r the only one who can help me. actually i am trying to test a c code. so what ever i studied i am sharing with you.tell me am i right or wrong.i am not so clear what i have studied.
at first i am taking a C file.i want to extract a model using modex. for this i need 2 file. 1 is c file and another one is test harness(.prx) file.then i am extracting a model and then i use spin.
i have some question.
1.what should .prx will include?
2. the model generated from modex represent what?
3 what is the role of spin here?
i am following this link:
spinroot.com/spin/Workshops/ws05/modex_tutorial.pdf
if u have time pls see this.
Offline
In the Doc directory of the Feaver/Modex distribution you will find a very detailed manual that explains all the options and the contents of the .prx file
but again, i would warn agains attempting to use modex before you know how to use spin really well. you're very unlikely to succeed if you take this route.
even for advanced and very experienced spin users, the use of modex can be challening....
Offline
thanks for ur reply. I am working on spin.
another thing is, in some tutorial i have seen they use GUI for FeaVer/modex.but i didnot find it anywhere. is there any GUI for it? for example i have used a little iSpin with graphical user interface for promela code.
Offline
1). in installing of modex how to edit the makefile of it contained in Src folder. give any example. i m using cygwin in C: drive i.e c:\cygwin.
2).when i enter the command (make install) in installing of modex the following message appear.
bash:make command not found
Offline
re 1: you should not have to edit the makefile
re 2: it looks like you do not have the 'make' command installed -- you can download it from cygwin
also make sure that you have the complete gcc tool suite installed so that you can compile c programs
Offline
I just want to share this;
To run iSpin you'll need Tcl/Tk. Tcl/Tk was written by John Ousterhout ([email protected]) and is public domain. It can be obtained (for PCs or Unix) from cygwin, or from: [url]http://www.tcl.tk[/url]/ or also (a more recent extension): [url]http://www.activestate.com/Products/ActiveTcl/[/url]
More details can be found in netnews-group: comp.lang.tcl
maybe this will also help you, new extensions added )
Offline