Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-13 18:45:58

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Installing Spin on Mac

Hello Dears,

I am trying to install Spin on my Macbook since last week and not getting it installed yet. I am really frustrated and want your help. I am bit new to Spin and want to use it learn its basic modeling. Please provide me a stepwise manual / procedure to install the Spin on macbook. I am following the instructions provided on the Spin read me page "[url]http://spinroot.com/spin/Man/README.html#S2[/url]" but it doesn't work at all. after extracting the distribution file when i try for the make command it doesn't work and responds as "No such (make) file found". I have gone through the google and searched about it but couldn't found and suitable solution. Please any of you is using the Spin on his mac, provide me help to install it on my one as well.

I am eagerly waiting for the response and kind help in this regard.

Thanks

Imran

Offline

#2 2011-02-13 21:23:20

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Installing Spin on Mac

it seems like you do not have the 'make' command installed on your Mac
you'll need the commands make, yacc, and gcc to be able to compile Spin from its sources.

Offline

#3 2011-02-14 10:55:25

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: Installing Spin on Mac

You first have to install Apple's Xcode (Tools). As part of this installation, several command line utilities (e.g., gcc, make, yacc, lex) will get installed.

The latest version of Xcode can be downloaded from [url]http://developer.apple.com[/url]/ (you might need to register first). Your Mac OS X Install DVD also contains a version of Xcode (although it doesn't get installed by default).

Last edited by theo.ruys (2011-02-14 10:55:59)

Offline

#4 2011-02-14 12:07:03

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Dear Theo and spinroot, thanks for your kind response. Actually I have xcode installed on my system and all the commands make, yacc and gcc are there as well. Can you please tell me the procedure how to use/set them to install the Spin on mac?

Hope that you will provide me a positive response.
Apologies for any inconveniences caused.

Thanks

Imran

Offline

#5 2011-02-14 14:25:52

jlb
Member
Registered: 2011-02-14
Posts: 1

Re: Installing Spin on Mac

Hello

I compiled spin 6.0.1 without problem on my MacBook with Mac OS X 10.6.6:

unzip untar as stated in the documentation then

cd Downloads/Spin/Src6.0.1
make

that's all

Contrary to what is said in step 2c, the C preprocessor is found withour modifying the makefile

Regards

Offline

#6 2011-02-14 16:21:52

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Dear jlb, Thanks for posting, but when I run the commmands

cd Downloads/Spin/Src6.0.1
make

Then Terminal prompts me the following error:

"-bash: make: command not found"

I am not sure why, although I have installed the xcode and other compilers such as yacc, gcc and makefile in the following location:

/Developer/usr/bin

Can you please tell me the path or location of your cpp, yacc and make file?

regards

Offline

#7 2011-02-14 16:37:02

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Installing Spin on Mac

'make' is not in your search path, and likely that means that 'yacc' or 'gcc' aren't either.
you could try:
export PATH=$PATH:/Developer/usr/bin
and then try to execute the make command again
it may work, but i'm not familiar with the Mac environment

Offline

#8 2011-02-15 18:56:33

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Dears,

Apologies for interrupting once again. Actually I am really struggling to install the Spin on my mac and still couldn't get it. I have installed the latest versions of developers tools and the problem of make file is solved now, but when I run it , the following trail is prompted by the Terminal:


Imrans-MacBook-Pro:Src6.0.1 imran$ make
yacc         -v -d          spin.y
gcc -c y?tab.c
rm -f y?tab.c
mv y?tab.o spin.o
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o spinlex.o spinlex.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o sym.o sym.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o vars.o vars.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o main.o main.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o ps_msc.o ps_msc.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o mesg.o mesg.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o flow.o flow.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o sched.o sched.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o run.o run.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen1.o pangen1.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen2.o pangen2.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen3.o pangen3.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen4.o pangen4.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen5.o pangen5.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o guided.o guided.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o dstep.o dstep.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o structs.o structs.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pc_zpp.o pc_zpp.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen6.o pangen6.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o pangen7.o pangen7.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o reprosrc.o reprosrc.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_parse.o tl_parse.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_lex.o tl_lex.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_main.o tl_main.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_trans.o tl_trans.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_buchi.o tl_buchi.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_mem.o tl_mem.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_rewrt.o tl_rewrt.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security       -c -o tl_cache.o tl_cache.c
gcc -O2 -ansi -DNXT -D_POSIX_SOURCE -Wno-format-security     -o spin spin.o spinlex.o sym.o vars.o main.o ps_msc.o mesg.o flow.o sched.o run.o pangen1.o pangen2.o pangen3.o pangen4.o pangen5.o guided.o dstep.o structs.o pc_zpp.o pangen6.o pangen7.o reprosrc.o tl_parse.o tl_lex.o tl_main.o tl_trans.o tl_buchi.o tl_mem.o tl_rewrt.o tl_cache.o
Imrans-MacBook-Pro:Src6.0.1 imran$

I don't know what's going there, but when I check for Spin from terminal whether it has been installed or not, it prompts me nothing. I don't know how to properly install it and check it whether it has been installed or not?

Another thing is that when I try to install Spin again from the same directory the terminal prompts me the following line on running the make command:

"make: `spin' is up to date."

Kindly help me to solve this problem by providing me a stepwise guidance to get installed Spin on my mac and to start my work with it. I am really struggling and looking for you supportive response.

Looking for your kind response,

Imran

Offline

#9 2011-02-15 19:11:04

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Installing Spin on Mac

it compiled correctly -- all you need to do is to move spin into the bin directory that's in your path:
mv spin /Developer/usr/bin
(for which you may need root privileges)

Offline

#10 2011-02-15 19:51:48

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Thanks for kind response. I have moved the spin directory to the bin according to the given command. But don't know how to start spin now or to run my first simple program to check that its working now. I am sorry for this foolish asking but i am completely new to spin. Hope that you will not mind. Please provide me a couple of instructions to open and test the spin now. I checked the command "$ spin -V" in terminal but it prompts invalid command. Please push me forward as i think that I am just near to my destination to run spin on my mac.

Thanks once again.

Imran

Offline

#11 2011-02-15 19:56:30

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Installing Spin on Mac

I think you misunderstood. You should move the spin executable produced by the make command to the /Developer/usr/bin directory, not the entire directory with the spin sources...
you start spin by typing 'spin' and then you give it the name of a file with a spin model as an argument, together with any other options you want to use
for instance:  spin -p leader.pml
It would probably save you time if you first read through some of the online tutorials or the book for basic spin usage, but feel free to ask questions

Offline

#12 2011-02-15 20:29:55

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Thanks sir for correction, but I put back the spin directory to the home directoery and moved the "spin executable" to the bin, but still on command 'spin' in terminal it prompts "-bash: spin: command not found". I don't know why? I want to just run the spin successfully then you are right that i have to go through the tutorials, but at the moment, want spin to be installed on mac.

Thanks alot for such a great help. Hope that you will continue it.

Imran

Offline

#13 2011-02-15 21:10:46

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Installing Spin on Mac

one thing you can try:
type:
   which gcc
at the shell prompt
and move the spin executable into the directory that this prints (i.e., the same directory where gcc is located)

Offline

#14 2011-02-15 22:07:14

gozonetoo
Member
Registered: 2011-02-15
Posts: 6

Re: Installing Spin on Mac

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.

Offline

#15 2011-02-16 00:28:34

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Dear gozonetoo,

Thank you very much for your support in this regard. I am not very much familier with the Terminal but just use it for some extent to run the mac properly. I am very happy with your comments and hope that in a while I will be able to run Spin on my mac. Actually the gcc, yacc, cpp files are in the location (/Developer/usr/bin) i.e bin directory contains all these files and I moved the spin exec to this directory as well. When I test for gcc and yacc these are show in the given path ie (gcc is /usr/bin/gcc) but the command to check for spin ($ type spin) prompts (-bash: type: spin: not found).

I want to tell you that there is another bin directory in the (/Developer/usr/local/bin) as well and i don't know whether this is the directory to put spin or not?

Anyway on executing the 'echo $PATH'  commands my terminal shows the following:

Imrans-MacBook-Pro:~ imran$ echo $PATH
/Library/Frameworks/Python.framework/Versions/Current/bin:/Library/Frameworks/Python.framework/Versions/2.6/bin:/Library/Frameworks/Python.framework/Versions/2.6/bin:/Library/Frameworks/Python.framework/Versions/Current/bin:/Library/Frameworks/Python.framework/Versions/Current/bin:/Library/Frameworks/Python.framework/Versions/Current/bin:/Library/Frameworks/Python.framework/Versions/2.6/bin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/bin:/usr/X11/bin:/usr/local/bin:/usr/local/bin

Hope that you will depict the issue I am having at the moment and will provide me better suggestions to solve it.

Once again many thanks.

Imran

Offline

#16 2011-02-16 00:50:59

gozonetoo
Member
Registered: 2011-02-15
Posts: 6

Re: Installing Spin on Mac

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.

Offline

#17 2011-02-16 01:38:32

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Dear gozonetoo,

its unbelievable for me! Great its working now. I am so much happy that I cann't explain it to you, really. Thank you very very much. I have copied the spin to (/usr/local/bin) and executed it in terminal, I got the response (Spin Version 6.0.1 -- 16 December 2010). The type spin command prompted me with (spin is hashed (/Developer/usr/local/bin/spin)). That's great.

I have installed the ispin as well and it is working well but when I try to open a sample promela program (leader.pml) saved in the Tests directory inside the Spin folder in local, then on syntex check command it generates the error:

3 syntax check
spin: preprocessing failed
sh: /lib/cpp: No such file or directory

can you tell me, why this error is happening , please don't mind that, I am asking another question!

Anyway I am really thankful to you and all others in this forum who helped me alot.

wishing you alot pf goodluck!

Regards

Imran

Offline

#18 2011-02-16 01:52:16

gozonetoo
Member
Registered: 2011-02-15
Posts: 6

Re: Installing Spin on Mac

What is the result of 'type cpp'?

Offline

#19 2011-02-16 01:57:52

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

The result of type cpp is :

"cpp is /usr/bin/cpp"

Offline

#20 2011-02-16 02:09:28

gozonetoo
Member
Registered: 2011-02-15
Posts: 6

Re: Installing Spin on Mac

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.

Offline

#21 2011-02-16 02:27:46

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Aplogies for interuppting again!

Actually I followed the procedure 1 as described by you, but still the same error is displayed. i.e
spin: preprocessing failed
sh: /lib/cpp: No such file or directory

can you tell me the second way...Please

Thanks

Offline

#22 2011-02-16 02:56:27

gozonetoo
Member
Registered: 2011-02-15
Posts: 6

Re: Installing Spin on Mac

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.

Offline

#23 2011-02-16 12:14:07

imran_ali
Member
Registered: 2011-02-13
Posts: 11

Re: Installing Spin on Mac

Dear gozonetoo,

That's done. Now the spin is running correctly and the examples are executed as well. I have edited, modified and rebuild the makefile as described by you and all is going well now. I am very happy and thankful to you for such a great response and continuos support in this regard.

A little query I had in my mind that the ispin version installed by me is old one (came along with the Spin distribution) but I came to know from the forum that a new version has been released for ispin that is most suitable for laptops. As the current ispin is very messy in interface that is alot of windows are messed up on the screen and it is difficult to read the output during simulation phase.

Sorry for this long illustration, but just wanted to ask that how can I uninstall the current ispin from mac terminal and install the new one? I made an effort by removing the "ispin.tcl" file from the spin directory but it is still running when i use "ispin" command in terminal.

Apologies for any inconveniences caused and Thank you very much once again.

Imran

Offline

#24 2011-02-16 15:59:28

gozonetoo
Member
Registered: 2011-02-15
Posts: 6

Re: Installing Spin on Mac

Great.  Welcome to the world of Promela and Spin! 

But, as regards ispin, I can't help as I've not used it.

Offline

#25 2011-02-17 01:23:02

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Installing Spin on Mac

Re ispin -- the latest version is 1.0.4 from 11 February 2011
you can retrieve this from: [url]http://spinroot.com/spin/Src[/url] -- see ispin.tcl
(actually, the webpage says 6.0.3 but it's really 6.0.4)
to install it, just copy it to /usr/local/bin -- without the tcl suffix -- as follows:
   cp ispin.tcl /usr/local/bin/ispin
(and you may need sudo to do this, like you did or didn't do with spin itself)

But, this will not solve the problem you described -- the only difference is in the appearance of some of the sub-panels under the Verification tab (Error trapping options and Advanced Parameter Settings)

Let me know what seems to be wrong with the version of ispin you're using -- especially what you mean with "alot of windows are messed up on the screen"
The simulation panel is adjustable, but not directly the fontsize. Is it that the fontsize is too small?  You can adjust the size of each sub-panel in the Simulate/Replay view by dragging the separators on the little buttons that show.  Let me know what the problem is that you're seeing.

Offline

Board footer

Powered by FluxBB