A forum for Spin users
You are not logged in.
Pages: 1
Great. Welcome to the world of Promela and Spin!
But, as regards ispin, I can't help as I've not used it.
Okay. You will need to edit the 'makefile'. Go to the directory (aka folder) where you built spin. In that directory there is a makefile. Edit the makefile as follows:
1) Find the line that starts with: CFLAGS=-O2 ...
2) After the word 'security' add a space and the following, exactly: -DCPP="\"/usr/bin/cpp\""
Make sure it is exact.
3) Save the edited makefile
Next, build spin again as:
$ make clean
$ make
During the make print out you should see '/usr/bin/cpp' (and other stuff) being printed out. Once the build is complete install the new 'spin' into /usr/local/bin as:
$ sudo cp spin /usr/local/bin
Try running spin again.
Okay. There are two ways to do it. #1 is the easy way; #2 is the right way. Let's do #1 because it is easy. Try this:
# sudo mkdir /lib
# sudo ln -s /usr/bin/cpp /lib/cpp
Now try running spin again on the leader.pml.
What is the result of 'type cpp'?
Your executables path includes '/usr/local/bin' - this is the best place to put 'spin'.
Go to the directory (aka folder) where you build spin. Do the following:
$ make
$ cp spin /usr/local/bin
If the 'cp' command fails it would likely be because of permission problems. If it does fail try:
$ sudo cp spin /usr/local/bin
and they, when prompted, type your password. The 'sudo' program allows you permission if your account is configured as a Mac 'Admin' account.
Once spin is copied into /usr/local/bin you should be able to execute it. Try
$ type spin
spin is /usr/local/bin/spin
and then
$ spin -V
Spin Version 5.2.2 -- 7 September 2009
Let me know when you see the spin version reported as above.
Imran -- I'll explain in some detail; sorry if this is too much detail. I've used Spin successfully on Macs for a long time.
You are using the 'Terminal' application; which is the proper thing to do when using Spin.
When you built spin with 'make' it produced an executable file; that executable file needs to be in Bash's executables path. Check your executables path with 'echo $PATH'. Where is what mine shows:
$ echo $PATH
/usr/local/scheme/bin:/usr/local/lisp/bin:/Users/ebg/Unix/bin:/opt/local/bin:/opt/local/sbin:/usr/local/bin:/usr/local/sbin:/usr/X11R6/bin:/usr/local/prevent/bin:/usr/bin:/bin:/usr/sbin:/sbin:/etc:/usr/local/git/bin:/usr/local/mysql/bin
Yours will look different and that it okay. Now you can find out where 'gcc' is located with:
$ type gcc
gcc is /usr/bin/gcc
and you can check 'spin' with:
$ type spin
spin is /usr/local/bin/spin
(Yours will be different) If the above command does not find 'spin' ; then it means spin is not in Bash's executables path. Before you can use spin is must be in your executable path. There are two ways to get 'spin' in your executables path: 1) move 'spin' into a directory (aka folder) that is already in your executable path or 2) change you executable path. Probably #1 is the easiest.
For #1, do the following. Go to the place where you made spin with 'make'. Here is what mine looks like:
$ cd /usr/local/src/Spin/Src5.2.2
$ pwd
/usr/local/src/Spin/Src5.2.2
$ ls spin
spin*
if spin is not there then make it again with 'make'. Next we will move it. Please perform the above, show me the result of 'echo $PATH' - I will post the additional instructions including your first spin program.
Pages: 1