A forum for Spin users
You are not logged in.
Pages: 1
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!
No it is not. I only get pan.exe after I compile on the command line in the cygwin terminal
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
seems iSpin cannot find the compiler. I will fix that and try again
Thanks a lot!
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
Pages: 1