A forum for Spin users
You are not logged in.
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
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
Thank you very much for the explanation.
Offline
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
Thanks :-)
Offline