什么是无条件的自我循环

Question

我正在研究一个涉及旋转模型Checker.spin版本6.4.7和ISPIN版本1.1.4我在ISPIN上遇到此错误的项目。

状态76：无条件的自循环

    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 %dn" , 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 %dn" , id, nodeState[id].p);
88                
89          // send TDMA
90            ::nodeState[id].state != ALOHA -> 
91  //          printf("%d --Sending TDMn" , 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 %dn", 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 TDMAn", 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 %dn" , id,  nodeState[id].members, id_j);
133 
134         ::nodeState[id].state !=  ALOHA -> 
135 //      printf("%d reaches TDMAn" , 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 Detectorn", 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 %dn" , 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 }

错误指向第57行。我不确定这是什么意思。当我在终端上运行代码时，它可以使用ISPIN接口进行精细的BT，它会引发此错误。有人遇到这个错误？

Answer 1

花了很多小时在代码周围徘徊。我尝试了命中和试用，并从模型中删除了最后的跳过声明。似乎许多可能的替代后卫声明以及其他跳过声明使其成为无条件的自我循环。当我删除了最后一个 :: Skip 语句 do loop 。

时，它起作用。

---

看来，Spin具有一些非常简单的机制来检测由某些循环卫队等于 skip或 true引起的无条件自我循环，而没有后续指令例如：

init
{
    do
        :: skip            // or true
    od;
}

打印：

~$ 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

可以通过添加额外的空语句来轻松规避例程：

init
{
    do
        :: skip -> skip            // or true -> true
    od;
}

打印：

~$ 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

有趣的是，例程未能考虑其他明显的案例，其中无条件的自loop 出现，例如，当警卫与0有所不同并且没有任何不同指令的重新进入块。