A forum for Spin users
You are not logged in.
Pages: 1
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?
Saqib
Last edited by saqibdola (2017-04-14 12:22:25)
Offline
Pages: 1