Promela에서 배열 요소의 비 결정적 값을 선택할 수 있습니까?

Question

다음은 내가 작성중인 Promela 코드입니다. 내가 코드를 시뮬레이션하려고하면

491  byte api1[5]; 
492  byte api2[5]; 
493  byte api3[5]; 
494  byte reftask1[5] 
495  byte reftask2[5]; 
496  byte reftask3[5]; 
497  byte rid1[5]; 
498  byte rid2[5]; 
499  byte rid3[5]; 
500 
501 
502 proctype init_call(){ 
503  byte i1 = 0; 
504  do 
505  :: (i1 == 5) -> break 
506  :: else -> 
507   select (api1[i1]: 2 .. 9); 
508   select (api2[i1] : 2 .. 9); 
509   select (api3[i1] : 2 .. 9); 
510   select (reftask1[i1] : 1 .. 3); 
511   select(reftask2[i1] : 1 .. 3); 
512   select (reftask3[i1] : 1 .. 3); 
513   select (rid[i1] : 0 .. 1); 
514   select (rid[i1] : 0 .. 1); 
515   select (rid[i1] : 0 .. 1); 
516   i1++; 
517  od 
518 } 

는, 나는

saw: '[', expected ':' spin: osek_sp2.pml:507, Error: expecting select (name : constant .. constant) near 'select'

그러나, 구문 정의에 따라, 내가 어떤 문제를 찾을 수 없습니다, 다음과 같은 오류 메시지가 나타납니다.

SYNTAX
select '(' varref ':' expr '..' expr ')'

varref : name [ '[' any_expr ']' ] [ '.' varref ]

이 오류 메시지의 이유는 무엇입니까?

Answer 1

패트릭이 맞습니다. 나는 이것이 벌레라고 말하고 싶다. 당신이 spinlex.c으로 보면, 당신은 name: 전에 영숫자 문자를 검색 할 때 허용되는 것을 볼 수 있습니다 :

scan_to(':', isalnum, name) 

어쨌든, select이 과제의 순서 단지 속기이다. 따라서 과제를 직접 작성하는 것이 좋습니다.

api1[i1] = 2; 
do 
:: (api1[i1] < 9) -> api1[i1]++ 
:: break 
od