spin - 在 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 }

但是，如果我尝试模拟代码，则会收到如下错误消息，

锯：'['，预期'：'旋转：osek_sp2.pml：507，错误：期望选择（名称：常量..常量）靠近'选择'

但是，根据语法定义，我找不到任何问题。

语法
select '(' varref ':' expr '..' expr ')'

varref : 名称 [ '[' any_expr ']' ] [ '.' 变量引用]

此错误消息的原因是什么？

Answer 1

帕特里克是对的。我会说这是一个错误。如果您查看spinlex.c，您会看到它在扫描name之前:只允许使用字母数字字符：

scan_to(':', isalnum, name)

无论如何，select它只是一系列作业的简写。因此，解决方法可能是自己编写作业，例如

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