I am working on a project which involves SPIN Model checker.SPIN version 6.4.7 and ispin version 1.1.4 I am getting this error on ispin saying
state 76: unconditional self loop
proctype TDMAProtocol(byte id; chan P1, P2, PR)
54 {
55 byte id_j, members_j, r_j;
56 do
57 ::nodeState[id].r == id ->
58 nodeState[id].r = (nodeState[id].r + 1) % 4;
59
60 atomic {
61 // printf("-- %d New round %d member %d cmembers %d\n" , id, nodeState[id].r,nodeState[id].members, nodeState[id].cmembers);
62
63 nodeState[id].r = (nodeState[id].r + 1) % 4;
64 nodeState[id].messageLost[0] = nodeState[id].messageLost[0]+1;
65 nodeState[id].messageLost[1] = nodeState[id].messageLost[1]+1;
66 nodeState[id].messageLost[2] = nodeState[id].messageLost[2]+1;
67 nodeState[id].messageLost[id] = 0;
68 // nodeState[id].round = 1;
69
70 // Send aloha
71 if
72 ::nodeState[id].state == ALOHA && nodeState[id].p == 0 ->
73
74 // printf("%d --Sending \n" , id);
75 P1!id,nodeState[id].members,nodeState[id].r;
76 P2!id,nodeState[id].members,nodeState[id].r;
77 if
78 ::true -> nodeState[id].p = 0;
79 ::true -> nodeState[id].p = 1;
80 ::skip
81 fi;
82 ::nodeState[id].state == ALOHA && nodeState[id].p == 1 ->
83 if
84 ::true -> nodeState[id].p = 0;
85 ::true -> nodeState[id].p = 1
86 fi;
87 // printf("%d --Sending with proabality %d\n" , id, nodeState[id].p);
88
89 // send TDMA
90 ::nodeState[id].state != ALOHA ->
91 // printf("%d --Sending TDM\n" , id)
92
93 P1!id,nodeState[id].members,nodeState[id].r;
94 P2!id,nodeState[id].members,nodeState[id].r
95 ::skip
96
97 fi;
98 }
99
100 :: empty(PR) ->
101 skip
102 :: nempty(PR) ->
103 PR?id_j,members_j,r_j;
104 // printf("%d Size of channel %d\n", id, len(PR));
105 atomic {
106 if
107 ::nodeState[id].state == ALOHA ->
108 nodeState[id].messageLost[id_j] = 0;
109 nodeState[id].members = nodeState[id].members | (1 << id_j);
110 if
111 ::nodeState[id].members == members_j ->
112 nodeState[id].cmembers = nodeState[id].members | (1 << id_j)
113 ::skip
114 fi;
115 if
116 ::nodeState[id].cmembers == members_j ->
117 printf("%d reaches TDMA\n", id);
118 nodeState[id].state = TDMA
119 if
120 ::nodeState[id].leader > members_j ->
121 nodeState[id].leader = members_j
122 ::skip
123 fi;
124 if
125 ::nodeState[id].leader == members_j ->
126 nodeState[id].r = r_j
127 ::skip
128 fi;
129 ::nodeState[id].cmembers != members_j ->
130 skip
131 fi;
132 // printf("%d --Receiving in ALOHA %d from %d\n" , id, nodeState[id].members, id_j);
133
134 ::nodeState[id].state != ALOHA ->
135 // printf("%d reaches TDMA\n" , id);
136 nodeState[id].messageLost[id_j] = 0
137
138 fi;
139 }
140 //round
141 // Failure detector
142 :: nodeState[id].state == TDMA &&
143 (nodeState[id].messageLost[0] > 3 || nodeState[id].messageLost[1] > 3 || nodeState[id].messageLost[2] > 3) ->
144 atomic {
145 printf("%d ALOHA from failure Detector\n", id);
146
147 nodeState[id].state = ALOHA;
148 nodeState[id].members = 1 << id;
149 nodeState[id].cmembers = 1 << id;
150 nodeState[id].leader = id
151 }
152 // :: nodeState[id].round > 0 ->
153 // nodeState[id].round = (nodeState[id].round + 1) % 2
154 :: nodeState[id].r != id ->
155 // printf("%d in round %d\n" , id, nodeState[id].r);
156 nodeState[id].r = (nodeState[id].r + 1) % 4
157
158 //nodeState[id].round = (nodeState[id].round + 1) % 2
159 :: skip
160 od;
161 }
Error is pointed at line 57.I am not sure what does this mean. when i run my code on terminal it works fine bt with ispin interface it throws this error. Someone came across this error?
after spending many hours wandering around the code. i tried hit and trial and removed last skip statement from the model. Seems like many possible alternative guard statements along with additional skip statement made it an unconditional self loop. It worked when i removed the last ::skip statement from do loop.
It appears that Spin has some very simple mechanism for detecting unconditional self loops caused by some loop guard being equal to skip or true with no subsequent instruction to be executed, e.g.:
init
{
do
:: skip // or true
od;
}
prints:
~$ spin -search test.pml
error: proctype ':init:' line 4, state 2: has unconditional self-loop
pan: elapsed time 1.76e+07 seconds
pan: rate 0 states/second
The routine can be easily circumvented by adding an extra empty statement:
init
{
do
:: skip -> skip // or true -> true
od;
}
prints:
~$ spin -search test.pml
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 12 byte, depth reached 1, errors: 0
2 states, stored
1 states, matched
3 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in init
test.pml:6, state 6, "-end-"
(1 of 6 states)
pan: elapsed time 0 seconds
Interestingly, the routine fails to consider other obvious cases in which an unconditional self-loop arises, e.g. when the guard is a number different from 0 and there is no re-entrant block of instructions.