Spinroot

A forum for Spin users

You are not logged in.

#1 2017-04-14 12:19:48

saqibdola
Member
Registered: 2017-04-11
Posts: 1

Assertion Violation Error

Hi all,

below is the code for Mutual Exclusion Problem.

1	#define N 2
2	bool  choosing[N] = false;
3	byte    num[N]=0;
4	byte mycolor[N] 
5	byte nr_pro;
6	bit color;
7	active [N] proctype P() {
8	byte max, j, i;
9	again:
10	do
11	:: 
12	choosing[_pid] = true;
13	mycolor[_pid]= color;
14	
15	max = 0;
16	    i = 0;
17	    do
18	    :: i > N-1 ->break
19	::else -> if :: max < num[i] -> max = num[i] 
20	:: else ->break
21	             fi;
22	i= i+1;
23		od;
24	
25	num[_pid] = 1 + max;  
26	mycolor[_pid]= mycolor[i];
27	
28	choosing[_pid] = false;
29	    j = 0;
30	    do
31	    :: j > N-1 -> break
32	    :: else -> 
33	if 
34		:: j != _pid -> 
35		choosing[j] ==false
36	if 
37		  ::mycolor[_pid] == mycolor[j] ->
38	(num[j] == 0) || (num[_pid] < num[j]) ||
39	(mycolor[_pid] != mycolor[j])  
40	::else -> (num[j]==0) || (mycolor[_pid] != color) || (mycolor[j] == mycolor[_pid]) 
41	fi; 
42				:: else ->break
43				fi;
44				j= j+1
45			od;
46	    nr_pro++;
47	CS: assert (nr_pro == 1);
48	    nr_pro--;
49	if :: mycolor[_pid] == false -> color= true;
50	::else-> color=false;
51	fi;
52	num[_pid] = false;
53	od;
54	 goto again
55	}

above code works fine without assertion command. However, I am getting an error of assertion violation (line 47) during simulation.
Can someone help me in removing this error? smile

Saqib

Last edited by saqibdola (2017-04-14 12:22:25)

Offline

#2 2017-04-14 19:13:01

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

Re: Assertion Violation Error

use the counter-example to determine the cause
and then fix it
to generate and display a counter-example, you can do this:

spin -run filename.pml
spin -t -p -v -l -g filename.pml

Offline

Board footer

Powered by FluxBB