什么是 promela 中的无条件自循环？

Question

我正在从事一个涉及 SPIN 模型 checker.SPIN 版本 6.4.7 和 ispin 版本 1.1.4 的项目，我在 ispin 上收到此错误说

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 }

第 57.I 行出现错误，我不确定这是什么意思。当我运行我的代码在终端上工作正常 bt 与 ispin 接口它抛出这个错误。有人遇到过这个错误吗？

Answer 1

在花了很多时间浏览代码之后。我尝试了 hit 和 trial，并从模型中删除了最后一个 skip 语句。似乎许多可能的替代 guard 语句以及额外的 skip 语句使它成为一个无条件的自循环。当我从 do loop.

中删除最后一个 ::skip 语句时它起作用了

看来 Spin 有一些非常简单的机制来检测 无条件自循环 由某些循环守卫等于 skip 或 [=16] =] 没有后续指令被执行，例如:

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

有趣的是，例程没有考虑其他明显的情况，在这些情况下会出现无条件自循环，例如当守卫是编号与 0 不同，并且没有可重入指令块。

什么是 promela 中的无条件自循环？

what is unconditional self loop in promela?

distributed-computing

model-checking

promela

spin