A forum for Spin users
You are not logged in.
The next Spin Symposium will be held April 26-27, 2023, co-located with ETAPS 2023.
For more information:
https://easychair.org/cfp/SPIN-2023
or
https://spin-web.github.io/SPIN2023/
The current version of the Cobra static analyzer is now on Github, and includes a new GUI, iCobra.
Many new query libraries and expanded capabilities to work with search pattern sets.
The Caltech course CS118 is offered again this winter-term (Jan-Mar 2023).
The 28th International Spin Symposium will be held May 21-22, 2022, in Chicago Illinois, organized by Owolabi Legunsen and Grigore Rosu.
Papers were due: March 25, 2022
Author notifications: April 29, 2022
Camera ready papers: May 9, 2022
good point
the .(goto) links are generated by the parser. e.g. to encode break statements etc
correct -- the d_step sequences are converted into a single transition.
you can see the automata structure that is used with: $ ./pan -d
they should be basic statements from the model
so it's mostly Promela syntax -- d_steps are special though
since they are converted into a single transition
a channel name is a variable that can hold the id of an instantiated channel
the same channel name could, for instance, be reassigned the id of different channels
at different points in a run
for a given instantiated channel, the id number does not change, but a channel variable
can hold any channel id at different points in it's use
where are they marked as sub-sequences?
can you give an example?
proctypes and never claims are converted into omega-automata, which have numbered states...
not sure what you mean by "the sublanguage that can occur in traces"
you mean the format and syntax of error traces?
yes, you can run the preprocessor manually (call gcc -E -x c model.pml)
just like spin does internally (main.c line 106)
it has to do with the implementation of partial order reduction
where we want to make it impossible to negate expressions
that can be used to optimize the verification
the output of the -I flag is not a valid Promela model -- it's mostly a debugging aid to see how inlines and macros are expanded internally
the temporal operators have lower precedence than the arithmetic operators, but higher than logical or or and
X is highest, then U then [] and <>
you can see this in the grammar description in spin.y
(sorry for the slow response!)
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...)
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...