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 }
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?
]]>