Spinroot

A forum for Spin users

You are not logged in.

#1 Spin Symposia » Spin 2022 Symposium » 2022-04-02 22:06:33

spinroot
Replies: 0

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

#3 Re: General » The syntax of PROMELA » 2022-03-05 19:24:30

the .(goto) links are generated by the parser. e.g. to encode break statements etc

#4 Re: General » Sub-sequences » 2022-03-04 18:03:49

correct -- the d_step sequences are converted into a single transition.
you can see the automata structure that is used with: $ ./pan -d

#5 Re: General » The syntax of PROMELA » 2022-03-04 18:02:51

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

#6 Re: General » Identifying channels » 2022-03-01 19:16:33

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

#7 Re: General » Sub-sequences » 2022-03-01 19:13:45

where are they marked as sub-sequences?
can you give an example?

#8 Re: General » State Numbers » 2022-03-01 19:12:59

proctypes and never claims are converted into omega-automata, which have numbered states...

#9 Re: General » The syntax of PROMELA » 2022-03-01 19:12:16

not sure what you mean by "the sublanguage that can occur in traces"
you mean the format and syntax of error traces?

#10 Re: General » Obtaining the true model that goes to pan » 2022-03-01 19:10:04

yes, you can run the preprocessor manually (call gcc -E -x c model.pml)
just like spin does internally (main.c line 106)

#11 Re: General » The roles of any_expr and expr in grammar » 2022-03-01 19:08:40

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

#12 Re: General » The -I flag is not documented in Spin online reference » 2022-03-01 19:06:45

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

#13 Re: General » The precedence between LTL operators and Boolean connectives » 2022-03-01 19:05:08

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

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

#15 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!

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

#17 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!

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

#20 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

#21 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

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

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

#23 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

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

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

Board footer

Powered by FluxBB