A forum for Spin users
You are not logged in.
I'd really love the opportunity to pitch my idea to someone who has been using Spin in real life industrial applications.
Hi everyone!
I have a business idea I call Model Checking as a Service. I'm trying to validate it and I'm looking for people to give a short pitch to. If you're interested in hearing what I have to say and giving (brutal) honest feedback or know someone else who might be interested, please feel free to contact me. I'd greatly appreciate it.
Okay, thanks.
I think it would be a little bit more obvious to the user if the line ended with `[d_step]` instead of `[sub-sequence]`. Anyway, thanks!
I've also encountered lines containing `DO`, `IF`, and `.(goto)` as the statement. I presume `DO` and `IF` mean that the process is choosing between possible branches in a `do` or `if` statement. Is `.(goto)` a goto statement that was generated from a `for` loop?
I'm looking for a piece of real life software to model using Spin. I'm developing a tool for displaying information from counterexample traces. It'd be interesting to see my tool in action. Does anybody have suggestions on where to look for a system to model?
For instance, I have the following line in one of the traces outputted by Spin:
84: proc 1 (Engine:1) ./Engine.pml:146 (state 90) [sub-sequence]
The line number seems to point to the beginning of a `d_step` block.
I mean the statements that can occur in transitions in a trace.
Is it possible that channel identification numbers change during execution?
Is it possible to uniquely determine a channel by its name, which should suffice for global channels, and possibly also by the name and PID of the process owning the channel in case it's a local channel? Especially, do we need channel identification numbers?
What are the transitions whose statements are marked as "sub-sequences" in traces? Do they contain useful information to the end user or can I just ignore them?
I wonder what are state numbers? The traces printed by Spin have a column for state numbers. Are they meant mainly for Spin developers or are they useful to the user?
Is the sublanguage that can occur in traces documented?
It turns out that the combination of the -p and -b flags of spin (not pan) was what I was looking for.
Is it possible to obtain the trace of an execution with pan, excluding the messages printed by processes? It seems that `grep -E "^[ 0-9]+:"` might find all steps in the trace produced by `pan -r`. The regular expression could also match lines printed by processes, which is my problem.
Macro expansion and/or preprocessing seems to change the line numbers of my PROMELA models. Is there any way to see the exact PROMELA source code that goes to pan when I compile my model using `spin -a`? I'm planning to write a debugger-like trace analyzer tool. I need to be able to connect the line numbers occurring in traces reported by pan to those occurring in the true model. In the future, I might also want to be able to expand d_steps.
It seems that there are some differences between the documented syntax of PROMELA and the syntax accepted by Spin. I made some findings while developing my own parser for PROMELA. I wrote my own EBNF for the dialect accepted by my tool along with some comments on the PROMELA syntax. I'd appreciate comments very much. My EBNF is available at GitHub: https://gist.github.com/jllang/54ff523beafa82058d05dd829ccc2671
According to the grammar, Boolean expressions belong to the syntactic category `expr`, so a variable declaration such as `bool b = true || false` should be rejected by Spin, but it is accepted. However, `bool b = full(c)` is rejected. I guess the difference between `any_expr` and `expr` is really the presence of `chanpoll`.
Interesting, the syntax produced by the -I flag contains undocumented features, such as anonymous blocks and labels starting with a colon. Additionally, Spin refuses to digest its own output, because the -I flag generates syntax errors...
Is that project still alive? I'm interested.
By the way, does the -I flag produce the final PROMELA model that goes to the verifier executable? I sometimes get really strange line numbers in error messages produced by pan. They don't seem to correspond with the line numbers in my PROMELA source code.
The help command of spin lists the following flag: "-I show result of inlining and preprocessing". This flag seems to be missing from the online documentation at https://spinroot.com/spin/Man/Spin.html
What would go wrong if any_expr and expr were combined under a single expression definition?
I don't understand the division of expressions into any_expr and expr. The assign rule says that a varref may be assigned with an any_expr. This means that for instance the model "init { bool x; x = true || false; }" is malformed because "true || false" is an expr (of the form expr andor expr) that is not an any_expr. What is the point of having any_expr and expr?
I'm working on a PROMELA parser. I have a simple question: Do LTL operators take precedence over Boolean connectives, or is it the other way around? What about the precedence between LTL operators? I read these manual pages, but they don't seem to give an answer: https://spinroot.com/spin/Man/operators.html https://spinroot.com/spin/Man/ltl.html