Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » Swarm verification on ispin » 2021-05-31 18:24:17

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...)

#2 Re: General » Swarm verification on ispin » 2021-05-28 21:14:44

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!

#3 Re: General » Swarm verification on ispin » 2021-05-27 17:41:37

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....

#4 Re: General » Swarm verification on ispin » 2021-05-27 00:22:50

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!

#5 Re: General » How to spell Spin and Promela » 2021-05-12 17:55:34

Small capitals is common, but the tool and language are so well known now that many just capitalize only the first letter.

#7 Re: Bug Reports » SPIN does not generate an answer in huge models » 2021-05-04 22:23:19

sorry if this has gone unanswered for so long.
there's really not enough information to see what the issue is
it could be that the search stack is too deep -- can you try with half that size (the -m argument)
and see if that gets further?
it can't be a 32-bit vs 64-bit thing since you're already using over 4GB in this run, but there shouldn't be any other limit than what's available on your system.  does Windows impose a limit per process?
i don't think the gcc warning is an issue here

#8 Spin Symposia » Spin 2021 Symposium » 2020-11-04 19:15:09

spinroot
Replies: 0

The 27th International Spin Symposium will be co-located with ISSTA 2021, and held 12-13 July, 2021 in Aarhus, Denmark. The organizers are Alfons Laarman and Ana Sokolova.

Important dates:
Papers are due: April 20, 2021
Author notifications: May 20, 2021
Camera ready papers: May 30, 2021

#9 Re: General » [SOLVED] Best practice for bounded signed integers? » 2020-08-14 06:08:59

sorry, no there's no mechanism to specify that...

#10 Re: General » [SOLVED] Best practice for bounded signed integers? » 2020-08-08 20:19:38

there's currently no mechanism in the language for specifying this.
the closest you could get would be to use a short, or, as you suggested,
a bitfield of 6 bits -- giving 64 possible values, the first 31 of which
could be treated as negative numbers and the rest 0..31 positive

#11 Re: Bug Reports » Excessive warnings thrown for `spin -run` » 2020-07-31 23:05:08

I've updated the Spin sources on Github (specifically main.c and version.h) to fix this.

#12 Re: Bug Reports » Excessive warnings thrown for `spin -run` » 2020-07-31 21:49:55

ouch, those are new warnings that gcc generates based on more aggressive static analysis.
you could try passing the -Wformat-overflow=0 flag to the gcc call in the Spin sources, which
will suppress these warnings until more of them have been fixed.

#13 Re: General » Model resets of a process » 2020-07-13 17:35:55

did you try using an 'unless' construct?
http://spinroot.com/spin/Man/unless.html

#14 Re: Spin Symposia » Spin 2020 in Chicago July 24-25 » 2020-05-12 19:16:55

Due to the covid-19 quarantine, the event has been canceled for this year.
Hopefully the Symposium can be organized in Chicago in 2022
(since the location for 2021 is already chosen).
More details posted as they are available.

#15 Spin Symposia » Spin 2020 in Chicago July 24-25 » 2020-03-13 19:07:10

spinroot
Replies: 1

SPIN 2020 - 27th International Symposium on Model Checking of Software
Chicago, Illinois, USA, July 24-25, 2020

https://spin2020ui.web.illinois.edu

** CALL FOR PAPERS **

The SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software but does not exclude the analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation.

The SPIN symposium originated as a workshop focusing on explicit state model checking, specifically as related to the Spin model checker. However, over the years it has evolved to a broadly-scoped symposium for software analysis using any automated techniques, including model checking, automated theorem proving, and symbolic execution.

Topics of interest include, but are not limited to:

Formal verification techniques for automated analysis of software
Formal analysis for modeling languages, such as UML/state charts
Formal specification languages, temporal logic, design-by-contract
Model-checking
Automated theorem proving, including SAT and SMT
Verifying compilers
Abstraction and symbolic execution techniques
Static analysis and abstract interpretation
Combination of verification techniques
Modular and compositional verification techniques
Verification of timed and probabilistic systems
Automated testing using advanced analysis techniques
Combination of static and dynamic analyses
Derivation of specifications, test cases, or other useful material via formal analysis
Case studies of interesting systems or with interesting results
Engineering and implementation of software verification and analysis tools
Benchmark and comparative studies for formal verification and analysis tools
Formal methods of education and training
Insightful surveys or historical accounts on topics of relevance to the symposium

#16 Re: General » [SOLVED ... it is deterministic] Make Spin output deterministic » 2020-01-30 18:51:46

Spin verification runs should be deterministic, unless you specify some form of randomization or vary other parameters (like search depth, hashtable size in bitstate hashing, or things like -DT_RAND or -DP_RAND)
So, I suspect there's something else that's happening?

#17 Re: General » [SOLVED] "While not timeout" option? » 2019-12-05 18:13:42

but there are a ton of other options that ./pan recognizes -- it would be hard to list them all ...

#19 Announcements » Spin Version 6.5.1 is now available on GitHub » 2019-12-04 23:34:43

spinroot
Replies: 0

Small changes and one bug fix:

==== Version 6.5.1 -- 3 December 2019 ====

- small updates to prevent warnings from static analyzers, e.g.
  of format specifiers in print statements
- corrected bug reported by Hakan Erdogmus and Zmago Brezocnik
  in the simulation output, introduced in version 6.4.8 - fixed in
  mesg.c line 327 where a wrong parameter was passed. this
  caused lines printed to be truncated in some cases

#20 Announcements » Cobra Version 3.1 now on GitHub » 2019-12-03 21:17:12

spinroot
Replies: 0

This is a larger update, with many fixes and improvements.
The implementation of associative arrays for the scripting language was improved and is much faster now.
Lots of small updates of the query checkers, especially the standalone versions of the cwe checkers.
Cobra also has a new runtime verification mode, and a new -text option to suppress the default categorization of tokens (useful for runtime verification or when scanning anything other than program source texts).

#21 Re: General » [SOLVED] How to step through program? » 2019-10-03 18:29:12

There's no such mode yet -- but it would be great if you built that wrapper!

#22 Re: General » [SOLVED] What is my state size? » 2019-09-22 00:39:38

4 states explore until it found a deadlock
you can use ./pan -c0 to explore all states

#23 Re: General » [Solved] How are states labeled? » 2019-09-16 17:22:27

Spin computes a FSM and does some optimization and minimization, so some of the states that are originally numbered in order of creation are usually eliminated in this process. (Some of this happens in pangen5.c, see fct mkstate(n).

#24 Re: General » Generating System Model using Promela » 2019-08-06 18:18:07

the distribution of modex (spin's model extractor for c-code) contains example files in c for which the tool can extract spin models -- but you can also look at that c-code yourself and manually build models, as an exercise

#25 Re: General » -ltl vs 2 never claims inside » 2019-07-10 16:15:28

spinroot.com/spin/Man/promela.html  has manual pages -- check the one for np_
spin --  will give an overview of the main command-line arguments
pan -- will do the same for the executable analyzer

Board footer

Powered by FluxBB