Stack Overflow
Stack Overflow

Questions tagged [spin]

Spin is a popular open-source software tool, that can be used for the formal verification of distributed software systems. The tool was developed at Bell Labs in the original Unix group of the Computing Sciences Research Center, starting in 1980.

Spin is a popular open-source software tool that can be used for the formal verification of distributed software systems. The tool was developed at Bell Labs in the original Unix group of the Computing Sciences Research Center, starting in 1980.

References

158 questions
10
votes
2 answers

Spin unreached in proctype "-end-"

I'm pretty new at spin model checking and wanted to know what this error means: unreached in proctype P1 ex2.pml:16, state 11, "-end-" (1 of 11 states) unreached in proctype P2 ex2.pml:29, state 11, "-end-" (1 of 11 states) here is…
Javi
  • 889
  • 1
  • 16
  • 41
6
votes
2 answers

how to show the state space in SPIN

The "Automata View" in iSpin (v. 1.1.4) shows .. exactly what? It seems it is just a graph of the control flow of one process. How would I get the full state space of the system? E.g., in Ben-Ari: Principles of the Spin Model Checker, I want Figure…
d8d0d65b3f7cf42
  • 2,597
  • 15
  • 28
4
votes
1 answer

Spin - Formal Verification

Has anyone have contact with model checking with this tool SPIN, even more any information of model checking (concurrent programs)
edgarmtze
  • 24,683
  • 80
  • 235
  • 386
4
votes
1 answer

PROMELA: Would this be an example of a deadlock?

Would this be an example of a deadlock? active proctype test(){ bool one; byte x; one; x = x+11; }
jdoe
  • 65
  • 4
4
votes
1 answer

Is this model of Peterson's algorithm incorrect?

I have written the following model of Peterson's algorithm: bool want[2], turn ltl { []<>P[0]@cs } active [2] proctype P() { pid me = _pid pid you = 1 - me do :: want[me] = true turn = you !want[you] || turn ==…
isekaijin
  • 19,076
  • 18
  • 85
  • 153
4
votes
1 answer

Producing an automaton image of my Promela model

I'm using the SPIN model checker GUI - iSPIN. The GUI comes with a nice Automaton view generator, however in order to see the full automaton I need to zoom in/out. Also I would like to save that automaton in a nice image (avoid using print screen)…
Anton Belev
  • 11,963
  • 22
  • 70
  • 111
4
votes
1 answer

Pass by-reference in Promela

In my design, I have N global variables and a method, that takes as parameter some of the mentioned parameters, depending on the state. Can I pass global variables as parameters by-reference? This paper explicitly says in Conclusion part that…
Boris Mocialov
  • 3,439
  • 2
  • 28
  • 55
4
votes
1 answer

printf output using Promela and SPIN?

I am a beginner trying to use Promela and SPIN. As I am developing some simple Promela specifications, I want to check the values of variables in my program by using printf(). I have read this man page and am trying to run a simple hello world…
KJ50
  • 765
  • 1
  • 10
  • 27
4
votes
1 answer

Dubious use of 'else' combined with i/o, saw ';' near 'if'

Following is the code causing this. if :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> proc2clk[0] ? fromProc[0]; // Woke up :: (!(fromProc[0] == MSG_SLEEP) && !(fromProc[0] == MSG_FIN)) -> …
MetallicPriest
  • 29,191
  • 52
  • 200
  • 356
4
votes
2 answers

What are the steps to verify LTL with SPIN tool?

I wrote a model in Spin. I want to check some LTL on the model. for example: ltl L1 {<>[]Working} in the Verification window i choose option "use claim" and click "Run": ltl L1: <> ([] (Working)) gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c at…
Junior Fasco
  • 227
  • 2
  • 11
4
votes
1 answer

LTL model checking using Spin and Promela syntax

I'm trying to reproduce ALGOL 60 code written by Dijkstra in the paper titled "Cooperating sequential processes", the code is the first attempt to solve the mutex problem, here is the syntax: begin integer turn; turn:= 1; parbegin …
ymg
  • 1,500
  • 2
  • 22
  • 39
3
votes
1 answer

How to create two dimensional array in Promela?

To create matrix in C we need to write: int[][] a = {{1,2,3},{1,2,3},{1,2,3}} How can I create a matrix in Promela?
Bekzhan
  • 175
  • 1
  • 12
3
votes
1 answer

All possible Knight moving on a chessboard in promela

Is it possible to bypass a chessboard of size N × N with a knight from the initial position (I, J), having visited each square only once? #define A[] = True; A[I,J] = false; active proctype method(){ bit I=4; bit J=3; bit K=1; bit N=8; do ::I>2 &&…
Bekzhan
  • 175
  • 1
  • 12
3
votes
1 answer

Promela channel "??" removal order

Can anyone explain to me the order of what happens in the following? if :: a_channel??5 -> // do A :: value_1 == value_2 -> // do B fi; So basically how I understand it is that for the statement to be executable, 5 needs to be in the channel. I…
Rajdeep
  • 2,246
  • 6
  • 24
  • 51
3
votes
1 answer

Spin: error, the version of spin that generated this pan.c assumed a different wordsize (4 iso 8)

I am using Windows O.S and in Cygwin i type: wish -f ispin.tcl to open the ispin interface. I open a file test.pml which contains: byte state = 2; proctype A() { (state == 1) -> state = 3 } proctype B() { state = state - 1 } init { run A();…
Marialena
  • 817
  • 8
  • 31
1
2 3
…
10 11