A forum for Spin users
You are not logged in.
Pages: 1
Thank you for help, your reactivity and your advices.
If it may be of any help regarding the third issue, here is what happens when I try to add the -a flag:
$ swarm -f leader.pml -c2 -m1G -a
swarm: error, unrecognized parameter '-a'
$ ./leader.swarm -a
bad arg -a, should be prep or execI will watch for updates and remain at your disposal if you need any information.
[quote=spinroot]iSpin and Spin are copyright Bell Labs and/or Caltech but available without charge or limitation. you can do anything with it, including modify it, sell it, repost it, as long as you acknowledge the original source and make your changes available to everyone as well.[/quote]OK. So just to be sure that I got it right, I will rephrase it.
iSpin and Spin are not covered by any specific license except the few conditions quoted previously, as long as they are used for research or educational purposes. As for commercial purposes, they are covered by [url=http://www.spinroot.com/spin/spin_license.html]this license[/url] instead.
Is this correct?
[quote=spinroot]Re swarm: if you get that grep error, this means that swarm didn't run at all. Did you see other messages in the iSpin log-view to indicate what it was trying to do?[/quote]Sorry, I forgot to add the content of the frame up above the swarm run output's one. Here it is:
generated configuration file
done:: swarm: reading settings from 'swarm_cfg.tmp'
swarm debug: local with 2 cpus
swarm: 31 runs, avg time per cpu 3598.7 sec
swarm: script written to leader.swarm
----Running----
run completed
sh: ./leader.pml.swarm: No such file or directory[quote=spinroot]You can first try to run swarm from a shell prompt and make sure that it all works correctly on your system. That'll make it easier to find out what's going on when you try to run it from within iSpin.[/quote]Here is what I did in my shell:
$ swarm -f leader.pml -c2 -m1G
swarm: 22 runs, avg time per cpu 3598.7 sec
swarm: script written to leader.swarm
$ ./leader.swarm
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)
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verifyThis time, running swarm took several seconds whereas it stopped almost instantaneously when run from iSpin.
Regarding the warning message, I unsuccessfully tried adding a "-a" flag when generating the swarm script as well as when running the generated script.
Sorry if I am not seeing the solution where it is obvious, I am new to model checking and Spin (My first lab work should be next week).
P.S.: I will try to package swarm for Arch Linux too, if I manage to make it run of course ^_^
Hello,
First, I have questions related to iSpin. I want to make PKGBUILD for Arch Linux (similar to BSD ports or Gentoo's ebuilds), this is why I would like to know:
- What is the actual version numbering of iSpin? Is it 1.0.x as in the source code of iSpin or is it 6.0.x as in the release announcements on the forum?
- What is the license covering iSpin? Is it the same as Spin's one or the BWidget Toolkit's one or another one? (Sorry if I am asking a stupid question but it was not clear to me which license was applied when I read the source code)
Then, I followed the [url=http://spinroot.com/spin/Man/GettingStarted.html]Getting Started guide[/url] but I failed to run Swarm from iSpin's corresponding tab (before you ask, yes I compiled and installed Swarm in the first place). I get an error like:
"grep: script*.out: No such file or directory
ls: unable to access *.trail: No such file or directory"
Would this error come from the fact that, in the man page of Swarm 2.3 it is written that Swarm assumes I run Spin 5.2, and yet I run Spin 6.0.1?
Thanks in advance for your help.
Pages: 1