Spinroot

A forum for Spin users

You are not logged in.

#1 2010-11-29 08:40:47

faisal2000
Member
Registered: 2010-11-29
Posts: 9

basic spin

i m new in using spin. if any body help me for guiding about how check properties in spin.

Offline

#2 2010-11-29 17:09:56

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

Re: basic spin

check out some of the tutorials that are online: [url]http://spinroot.com/spin/Man/[/url]
or find one of the books listed on the main spin page in your local library (or at amazon.com) -- it'll help you get started quickly.

Offline

#3 2010-12-22 06:18:24

faisal2000
Member
Registered: 2010-11-29
Posts: 9

Re: basic spin

i m unable to install spin in ubantu system. the error which i m facing is "*.tar.gz is directory" and unable to make a make file.

Offline

#4 2010-12-22 06:31:01

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

Re: basic spin

you should first unzip the file and then untar it -- for instance as follows:
gunzip *.tar.gz
tar -xvf *.tar
this will create the directory Spin/Src6.0.1/ and it will have the makefile in it.
alternatively, just download the precompiled linux executable for your system, and install that in ~/bin or in /usr/local/bin and you'll be off and running right away

Offline

#5 2010-12-22 13:36:37

faisal2000
Member
Registered: 2010-11-29
Posts: 9

Re: basic spin

thanks sir,
gunzip *.tar.gz
tar -xvf *.tar    (these above command is working)
but the problem is still there when i go in directory Spin/Src6.0.1/ and give make command "error unable to find make file".
also tell me the link to download the precompiled linux executable.

Offline

#6 2010-12-22 18:22:12

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

Re: basic spin

the link is: [url]http://spinroot.com/spin/Bin/[/url]
you'll see a couple of different precompiled executables there, one for Windows, one for Sun Solaris, and one for 32-bit and 64-bit Linux systems.
So, you'll need one of the two Linux versions, depending on your system.

By the way: you can see that the makefile is there by executing the "ls -l" command inside that source directory (Spin/Src6.0.1) so I'm not sure what's happening on your system...

Offline

#7 2010-12-23 06:13:36

faisal2000
Member
Registered: 2010-11-29
Posts: 9

Re: basic spin

thanks sir,
1-i have download the precompiled executables from the link u have provided.i download it for windows and for linux i copy it into my directory and rename it as "spin" for both (windows and Linux).

2-In windows it is working well and i can make "pan.c" but when i want to make the "pan.exe" file from c compiler which u have provided. it gives many errors e.g "Stdio.h: No such file or directory" but it makes pan.exe file and when i run pan.exe to produce trail error:comes "program to big to fit into memory".

3-In linux when i give the command "spin -a my_prog.prom" the error: No command 'spin' found. but in linux i can compile pan.c file which i produce from windows.

kindly tell me the solution so i can ovoid this problem of switches between windows and linux.

Offline

#8 2010-12-23 18:37:10

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

Re: basic spin

both on linux and on windows the executable spin must be in your 'search path'
let's first look at the linux installation
to make sure spin is in your search path, copy it as follows:
    sudo cp spin /usr/local/bin
note that for this you have to have root privileges on your machine.
if you don't, then you can do this:
    mkdir ~/bin
    mv ~/spin ~/bin/spin
and then add ~/bin to your search path:
    export PATH=$PATH:~/bin
(this is assuming that you use bash has your command shell)
now spin will be found

if you can't do this for any reason, you can always execute spin by giving the full path name of where you stored the executable -- for instance if it is in your home directory, and your're executing the command in the same directorry, you can use:
     ./spin -a my_prog.pml
or if you're in some other directory
     ~/spin -a my_prog.pml
or if you stored spin in ~/bin then you'd say:
     ~/bin/spin -a my_prog.pml

but it is really much more convenient to setup your search path to include the directory where spin is installed. (the right place to do that is in your profile, or in .bashrc)

on windows it seems that you either have very little memory available or a non-standard environment. do you have cygwin installed?
i'd be happy to help you pin down better what is going on on your windows system if you give more information

Offline

#9 2011-02-21 06:18:42

faisal2000
Member
Registered: 2010-11-29
Posts: 9

Re: basic spin

can you provide me the c code for H.Hyman mutual exclusion solution whose pseudo Algo is written in your manual.

Offline

#10 2011-02-21 07:28:16

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

Re: basic spin

the pseudo algol comes from the article written by Hyman in the Communications of the ACM, Volume 9, Number 1, from 1966. I don not have a version in C -- also note that the algorithm itself predates the C language :-)

Offline

#11 2011-02-22 10:45:44

faisal2000
Member
Registered: 2010-11-29
Posts: 9

Re: basic spin

then send any other complete example wich incldes (c code,promela model for spin).and compilation results.

Offline

#12 2011-02-22 16:49:15

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

Re: basic spin

please look at the online examples and tutorials:
[url]http://spinroot.com/spin/Man/index.html[/url]
or check out the book:
[url]http://spinroot.com/spin/Doc/Book_extras/index.html[/url]
or
[url]http://www.amazon.com/Principles-Model-Checker-Mordechai-Ben-Ari/dp/1846287693?ie=UTF8&s=books&qid=1199150125&sr=8-1[/url]

Offline

Board footer

Powered by FluxBB