以下は、私が書いている 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 }
しかし、コードをシミュレートしようとすると、次のようなエラー メッセージが表示されます。
見た: '['、予想される ':' スピン: osek_sp2.pml:507、エラー: 予想される選択 (名前: 定数 .. 定数) 近くの '選択'
しかし、構文定義によると、問題は見つかりません。
SYNTAX
select '(' varref ':' expr '..' expr ')'varref : 名前 [ '[' any_expr ']' ] [ '.' varref ]
このエラー メッセージの理由は何ですか?