A forum for Spin users
You are not logged in.
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!
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....
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!
Small capitals is common, but the tool and language are so well known now that many just capitalize only the first letter.
yes they do
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
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
sorry, no there's no mechanism to specify that...
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
I've updated the Spin sources on Github (specifically main.c and version.h) to fix this.
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.
did you try using an 'unless' construct?
http://spinroot.com/spin/Man/unless.html
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.
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
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?
but there are a ton of other options that ./pan recognizes -- it would be hard to list them all ...
you can use an unless statement?
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
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).
There's no such mode yet -- but it would be great if you built that wrapper!
4 states explore until it found a deadlock
you can use ./pan -c0 to explore all states
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).
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
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
does spin -replay -noclaim file.pml not work?