Spinroot

A forum for Spin users

You are not logged in.

#1 2021-05-23 03:25:09

Moon
Member
Registered: 2021-05-22
Posts: 5

Swarm verification on ispin

Hi,

I am having trouble using the swarm verification on iSPIN.

When I go to the Swarm Run tab and click Run, the following ispin prompts the following messages. (for some reason I can not load an image. It says [img]tag: off so I will paste the message directly.)


swarm setup output
generated configuration file
done:: swarm: reading settings from 'swarm_cfg.tmp'
swarm: 49 runs, avg time per cpu 3598.7 sec
swarm: script written to leader.pml.swarm
----Running----
run completed
sh: ./leader*.swarm: No such file or directory

and on the terminal windows:
swarm run output
Swarm Version 3.2 -- 5 June 2017
grep: script*.out: No such file or directory
ls: cannot access '*.trail': No such file or directory

I am using leader.pml in the source code as an example. The results I get from using my own models are same.


when I run the swarm verification with command lines without using iSPIN, I get the followings:
$ ./leader.pml.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 -a -N name (defaults to -N p0)
  or use e.g.: spin -search -ltl p0 leader.pml
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
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
warning: never claim + accept labels requires -a flag to fully verify
warning: never claim + accept labels requires -a flag to fully verify

and I can not add the -a flag in the verification.

Currently, I am using Cygwin64, spin version 6.5.1, ispin version 1.1.4 and swarm version 3.2.

Could you let me know what I am doing wrong?

Thanks,

Offline

#2 2021-05-27 00:22:50

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

Re: Swarm verification on ispin

In the ispin tab for "Swarm Run"  where you setup the configuration for the swarm run, there is an option under "Model Generation" (middle collumn) where you can provide additional arguments for each of the verification runs.
Here, because you have LTL formula embedded in the .pml file, you can select which formula you want to check by adding to the default arguments listed there (-c1 -x -n) the extra arguments -ltl p0  or -ltl p1  etc.
or if you just want to verify the first property (p0) by default, you add the runtime flag -a in the same place.
hope this helps!

Offline

#3 2021-05-27 04:30:06

Moon
Member
Registered: 2021-05-22
Posts: 5

Re: Swarm verification on ispin

Thanks for your reply.

The problem is that I can not run the swarm verification on ispin at all.

With or without the ltl arguments, ispin complains that there is no such file as model*.swarm.


The following is the error that I get when using the leader.pml file.

swarm setup output
generated configuration file
done:: swarm: reading settings from 'swarm_cfg.tmp'
swarm: 49 runs, avg time per cpu 3598.7 sec
swarm: script written to leader.pml.swarm
----Running----
run completed
sh: ./leader*.swarm: No such file or directory

and

swarm run output
Swarm Version 3.2 -- 5 June 2017
grep: script*.out: No such file or directory
ls: cannot access '*.trail': No such file or directory


For this example with leader.pml, ispin does creates leader.pml.swam file but it fails to load the file during the run.
I am not too sure how it creates the file but can not locate the file.

Offline

#4 2021-05-27 17:41:37

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

Re: Swarm verification on ispin

that's odd -- if the file is in fact created -- could you go outside ispin to a shell prompt
and then manually execute "sh ./leader*.swarm" ?  if that doesn't work, it may point
to the real problem -- if it does work, I've no idea what could cause the ispin call to fail....

Offline

#5 2021-05-28 02:01:49

Moon
Member
Registered: 2021-05-22
Posts: 5

Re: Swarm verification on ispin

Thanks for your reply.

I have done more play-around and here are the results. I think there is bug in iSPIN and you might be interested looking more closer to it.


So the first step I did was exiting iSPIN and running swarm verification on a shell prompt. I set the -a flag by creating swarm.lib file (swarm -l > swarm.lib) and adding the -a in the runtime options line in the .lib file.
Then loaded the setting by typing "swarm swarm.lib" and ran the swarm verification by "sh ./leader*.swarm". The results are following.

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 -a -N name (defaults to -N p0)
  or use e.g.: spin -search -ltl p0 leader.pml

BTW: It looks like it ran the verification but I am surprised that it doesn't give out any results. Is this normal for the swarm verification?

Going back to the iSPIN problem, clearly swarm is able to read the file and run the scripts on the shell prompt. So I thought the problem must be within the iSPIN file.

In the iSPIN file I found this part:

    $so insert end "----Running----\n"
    $so yview end
    update

    set nxn [string first "." $Fname]
    if {$nxn > 0} {
        incr nxn -1
        set sFname [string range $Fname 0 $nxn]
    } else {
        set sFname $Fname
    }
## untested:
    if {[string first "C:" $sFname] >= 0 || [string first "/" $sFname] == 0} {
        catch { set fd [open "|sh $sFname*.swarm" r] } errmsg
    } else {
        catch { set fd [open "|sh ./$sFname*.swarm" r] } errmsg
    }

and I changed the lines
catch { set fd [open "|sh $sFname*.swarm" r] } errmsg into catch { set fd [open "|sh $sFname.pml.swarm" r] } errmsg
and
catch { set fd [open "|sh ./$sFname*.swarm" r] } errmsg into catch { set fd [open "|sh ./$sFname.pml.swarm" r] } errmsg



After this, iSPIN was able to read the file and here are the results from iSPIN (with -a flag):

generated configuration file
done:: swarm: reading settings from 'swarm_cfg.tmp'
swarm: 49 runs, avg time per cpu 3598.7 sec
swarm: script written to leader.pml.swarm
----Running----
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 -a -N name (defaults to -N p0)
  or use e.g.: spin -search -ltl p0 leader.pml
run completed

and on the bottom windows (one with the black background):
swarm run output
Swarm Version 3.2 -- 5 June 2017
grep: script*.out: No such file or directory
ls: cannot access '*.trail': No such file or directory

Similar to running with the shell prompt, I did not get any results. Having said that, iSPIN can now read the swarm file at least.
Also those messages regarding the script*.out and the *.trail files, are they normal or would there be more bug in iSPIN currently?


Thanks,

Offline

#6 2021-05-28 21:14:44

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

Re: Swarm verification on ispin

thanks for checking this out.  somehow the shell command fails to expand the * properly, which is unexpected.
I've updated the ispin.tcl source on github to include the correction you propose (but it tries that only if the regular version with * failed).  it may be a specific issue on Windows/cygwin system -- should not need the change on Linux or Macs, but I could be wrong
thanks for reporting it and solving it!

Offline

#7 2021-05-31 04:53:44

Moon
Member
Registered: 2021-05-22
Posts: 5

Re: Swarm verification on ispin

Thanks for that.

Could I ask one more question.

As you can see, even with the shell command or with iSPIN, although the scripts were run, I did not see any verification results with the swarm versification.
It just says the run completed and that's it.

Is this normal for the swarm verfication?
What would be the output of the swarm verification?

Thanks,

Offline

#8 2021-05-31 18:24:17

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

Re: Swarm verification on ispin

typically the only feedback from a run is some statistics on number of states explored and depth reached etc.
for a swarm run it would be impractical to list all of that, so the main feedback you get is if violations were found (leading to one or more trail files) -- in which case you can use the standard options to rerun the error trail
so that is the expected result for a swarm run (imagine if you have 10,000 parallel runs -- the only thing that matters is really if any one of them found a violation...)

Offline

#9 2021-06-02 05:05:13

Moon
Member
Registered: 2021-05-22
Posts: 5

Re: Swarm verification on ispin

ah that makes sense.

Thanks!

Offline

Board footer

Powered by FluxBB