Spinroot

A forum for Spin users

You are not logged in.

#2 Re: General » Swarm verification on ispin » 2021-05-31 04:53:44

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,

#3 Re: General » Swarm verification on ispin » 2021-05-28 02:01:49

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,

#4 Re: General » Swarm verification on ispin » 2021-05-27 04:30:06

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.

#5 General » Swarm verification on ispin » 2021-05-23 03:25:09

Moon
Replies: 8

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,

Board footer

Powered by FluxBB