A forum for Spin users
You are not logged in.
It is available on amazon:
https://www.amazon.com/dp/B0FFVZC8F1?ref_=pe_93986420_774957520
for more information (table of contents etc) see:
https://codescrub.com
that is true -- to account of out of order memory access you'd need to extend the model
an example of what it takes to do this is:
https://spinroot.com/spin/Doc/course/x86_tso.pml
a new user guide for the Cobra tool is available as PDF,
with detailed descriptions of Cobra's options and examples.
you can volunteer to be a reviewer for the final draft (december 2024)
The next Caltech course CS118 will be held Jan-Mar 2025, but you can take pretty much the same material in the online course available through the spinroot webpage
https://spin-web.github.io/SPIN2025
The 31st International Symposium on Model Checking Software will be held May 7-8 2025 in Hamilton, Canada, co-located with ETAPS-2025. The Symposium is organized by Kristin Yvonne Rozier and Gidon Ernst.
Available on github (nimble-code) or https://spinroot.com/cobra
A significant extension of Cobra's capabilities, with many new predefined query libraries, options for statistical analysis of code and finding code duplicates and cloned code segments.
A new user manual is currently in review -- if you'd like to help review the draft, send a message.
The latest release of the interactive static source code analyzer Cobra is now available on Githib.
Much new functionality and improvements. Give it a try.
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...)