Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-26 17:22:19

Ghostofkendo
Member
Registered: 2011-02-26
Posts: 3

iSpin (version number, license) and Swarm (compatibility) questions

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.

Offline

#2 2011-02-26 19:49:06

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

Re: iSpin (version number, license) and Swarm (compatibility) questions

yes you're right that some of the references to iSpin have been a little confusing.
the version number of iSpin is 1.x.y and the current version number for Spin itself is 6.x.y
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.
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?
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.

Offline

#3 2011-02-27 17:28:23

Ghostofkendo
Member
Registered: 2011-02-26
Posts: 3

Re: iSpin (version number, license) and Swarm (compatibility) questions

[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 verify

This 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 ^_^

Offline

#4 2011-02-27 20:55:43

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

Re: iSpin (version number, license) and Swarm (compatibility) questions

First re the license: yes you are correct.
Second: there is a mismatch in the version of swarm and ispin in your case -- I'll correct this in the next update of iSpin, to make sure it can work with either version.
(The problem is that your version of swarm names the script filename.swarm after stripping the suffix .pml -- but iSpin still expects the name without the stripping of the suffix .pml -- so it cannot find the script that was generated.)

I'll look into the third issue (why you cannot add the -a flag and make it stick.)

In general, though, I'd recommend first getting the hang of the regular use of Spin and only then advancing to the use of swarm. It's easier to figure out what's going on if you've used Spin itself for a bit and have become comfortable with it.

Offline

#5 2011-02-27 22:19:20

Ghostofkendo
Member
Registered: 2011-02-26
Posts: 3

Re: iSpin (version number, license) and Swarm (compatibility) questions

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 exec

I will watch for updates and remain at your disposal if you need any information.

Offline

Board footer

Powered by FluxBB