что такое безусловный цикл в промеле?

Я работаю над проектом, в котором используется SPIN Model 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 %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. Я не уверен, что это значит. когда я запускаю свой код на терминале, он отлично работает, но с интерфейсом ispin выдает эту ошибку. Кто-то сталкивался с этой ошибкой?


distributed-computing promela spin model-checking
person Neha    schedule 04.12.2017    source источник
comment
Какая версия дистрибутива SPIN вызвала эту ошибку? Поиск безусловного цикла в файлах spin647.tar.gz не дал никаких результатов.   -  person Ioannis Filippidis    schedule 05.12.2017

Ответы (1)


arrow_upward
1
arrow_downward

после долгих часов блуждания по коду. я попробовал хит и пробную версию и удалил последний оператор пропуска из модели. Похоже, что многие возможные альтернативные операторы защиты вместе с дополнительным оператором пропуска сделали его безусловным циклом. Это сработало, когда я удалил последний оператор ::skip из цикла выполнения.

Похоже, что 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

Интересно, что подпрограмма не учитывает другие очевидные случаи, в которых возникает безусловная петля, например, когда охранником является число, отличное от 0, и нет повторного входа. блок инструкций.

person Neha    schedule 07.12.2017