Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2012-04-18 14:35:57
- NubianSpinner
- Member
- Registered: 2012-04-18
- Posts: 5
Help!! Getting Started and I am stuck already
Hello everyone, VERY new here; trying to follow the steps in GettingStarted.html and running into an issue.
Ref (http://spinroot.com/spin/Man/GettingStarted.html)
In Step Seven, I selected "use claim" and entered claim name of p0 and this is what I get
spin -a leader.pml
ltl p0: <> ((nr_leaders>0))
ltl p1: <> ([] ((nr_leaders==1)))
ltl p2: [] (((nr_leaders==0)) U ((nr_leaders==1)))
ltl p3: ! ([] ((nr_leaders==0)))
the model contains 4 never claims: p3, p2, p1, p0
only one claim is used in a verification run
choose which one with ./pan -N name (defaults to -N p0)
gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
In Step Eight, I introduced the artificial error as stated in the document(put mine on line 52), and saved the model and I still get the same print out as above when i do a verification run.
Here are my versions
Spin Version 6.1.0 -- 4 May 2011
iSpin Version 1.0.3 -- 4 January 2011
TclTk Version 8.5/8.5
1 D:/Data/Spin/leader.pml:1
What am I missing here? The outcome for step 7 and 8 are not as expected
Thanks much
Offline
#3 2012-04-18 16:07:59
Re: Help!! Getting Started and I am stuck already
ah i see, i didn't realize this was for iSpin
if nothing happens after the gcc line, then this probably means that
there is a problem with the gcc compiler -- or that ispin cannot find it?
can you try those steps from a command line and see if they work that way?
spin -a leader.pml
gcc -o pan pan.c
./pan
Offline
#4 2012-04-18 16:38:40
- NubianSpinner
- Member
- Registered: 2012-04-18
- Posts: 5
Re: Help!! Getting Started and I am stuck already
seems iSpin cannot find the compiler. I will fix that and try again
Thanks a lot!
Offline
#5 2012-04-20 16:12:07
- NubianSpinner
- Member
- Registered: 2012-04-18
- Posts: 5
Re: Help!! Getting Started and I am stuck already
I installed cygwin and with that the gcc compiler.
I also updated ispin.tcl to have
set CC c:/cygwin/bin/gcc-4
From the cygwin terminal, I am able to do
spin -a leader.pml
gcc -o pan pan.c
./pan
and with the execution I can select never claims p0-p4
However from ispin, when I enter the claim name and click run in the verification window, I see
spin -a leader.pml
ltl p0: <> ((nr_leaders>0))
ltl p1: <> ([] ((nr_leaders==1)))
ltl p2: [] (((nr_leaders==0)) U ((nr_leaders==1)))
ltl p3: ! ([] ((nr_leaders==0)))
the model contains 4 never claims: p3, p2, p1, p0
only one claim is used in a verification run
choose which one with ./pan -N name (defaults to -N p0)
c:/cygwin/bin/gcc-4 -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -w -o pan pan.c
and nothing else seems to happen.
when I do ./pan from the wish console I get an error
(Spin) 10 % ./pan
child killed: unknown signal
(Spin) 11 %
I cant seem to figure out what I am doing wrong with configuring ispin to use the compiler; please help
Offline
#7 2012-04-21 03:20:26
- NubianSpinner
- Member
- Registered: 2012-04-18
- Posts: 5
Re: Help!! Getting Started and I am stuck already
No it is not. I only get pan.exe after I compile on the command line in the cygwin terminal
Offline
#8 2012-04-21 06:17:52
Re: Help!! Getting Started and I am stuck already
then for some reason it still doesn't find the gcc executable.
how do you start ispin? by double-clicking on it or with a commandline
wish -f ispin.tcl
you can try to do the latter -- and if it works it just means that Windows cannot find the cygwin binaries
to fix that you need to edit your environment variables in Windows to add the path
Offline
#9 2012-04-23 16:21:24
- NubianSpinner
- Member
- Registered: 2012-04-18
- Posts: 5
Re: Help!! Getting Started and I am stuck already
The latter still did not work; It turns out I had to update the env variable to add the cygwin path as you stated above.
Thank you very much for your help!
Last edited by NubianSpinner (2012-04-23 16:40:37)
Offline