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.
]]>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.
]]>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 ^_^
]]>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.
]]>