Spinroot

A forum for Spin users

You are not logged in.

#1 2015-08-25 08:37:09

Ralph Lange
Member
Registered: 2015-08-16
Posts: 2

Checking for invalid end states in full statespace search

The Source process in the following small example contains an infinite loop:

my_example.pml:
01  byte sharedData = 0;
02 
03  init {
04      run Sink();
05      run Source();
06  }
07 
08  proctype Sink() {
09      (sharedData == 3);
10      (sharedData == 2);
11      (sharedData == 1);
12  }
13 
14  proctype Source() {
15      do
16      :: true -> {
17              sharedData = 1;
18              sharedData = 2;
19              sharedData = 3;
20          }
21      od
22  }

When calling spin --search my_example.pml, Spin (Version 6.4.3) correctly reports that line 22 is never reached. However, it does not treat this issue as an error, although it states that the full statespace search includes checking for invalid end states.
Adding the end label ("end:") in line 15 does not make any difference. The report by spin --search my_example.pml is exactly the same as before.

Is this behavior intended? How can I ensure by a full statespace search that each process always reaches one of the defined end states?

Offline

#2 2015-08-27 06:36:19

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Checking for invalid end states in full statespace search

An invalid endstate is the same as a deadlock: it is a state where no process can make any further progress.
Your case is not of that type -- the process can keep running.
This is only an unreachable local process state, and it's reported by Spin as such, so that's as intended.

Offline

#3 2015-08-27 07:16:40

Ralph Lange
Member
Registered: 2015-08-16
Posts: 2

Re: Checking for invalid end states in full statespace search

Thank you very much for the explanation.

Offline

#4 2015-10-05 15:26:26

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: Checking for invalid end states in full statespace search

Hi,

the next model simulates a simple Petri net with a deadlock. The safety verification does not report the invalid state but the
deadlock can be found by adding an invalid assertion or using an ltl formula. Why the default search can't find the invalid state?


1    byte transitionNumber;
2   
3    byte p1=1, p2, p3=1; bit p4=1,p5,p6,p7,f;
4   
5    ltl p { !( (<>[] (f==0)) || (<>[] (f==1)) ) }
6   
7    init{
8    do    :: atomic{ p4>0 && p1 >0 -> /* t1 */
9                        f = !f; transitionNumber = 1;
10                        p4--; p1--; p5++; p2++          }
11            :: atomic{ p6>0 && p2 >0-> /* t2 */
12                        f = !f; transitionNumber = 2;
13                        p6--; p2--; p7++; p1++;         }
14            :: atomic{ p5>0 && p3 >0 -> /* t3 */
15                        f = !f; transitionNumber = 3;
16                        p5--; p3--; p1++;                   }
17            :: atomic{ p1 >0 -> /* t4 */
18                        f = !f; transitionNumber = 4;
19                        p1--; p6++; p3++;                 }
20            :: atomic{ p7>0 && p3 >0 -> /* t5 */
21                        f = !f; transitionNumber = 5;
22                        p7--; p3--; p2++                    }
23            :: atomic{ p2 >0 -> /* t6 */
24                        f = !f; transitionNumber = 6;
25                        p4++; p2--;    p3++;               }
26           /* :: else -> assert(0)  */
27    od
28    }

Offline

#5 2015-10-06 04:28:18

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Checking for invalid end states in full statespace search

omit the ltl formula to locate the deadlock

Offline

#6 2015-10-07 01:00:54

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: Checking for invalid end states in full statespace search

Thanks :-)

Offline

Board footer

Powered by FluxBB