Нельзя ли в Promela выбрать недетерминированное значение элемента массива?

Ниже приведен код 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 : name [ '[' any_expr ']' ] [ '.' варреф ]

В чем причина этого сообщения об ошибке?


promela spin
person jungyh0218    schedule 26.09.2016    source источник
comment
Похоже, внутренний синтаксический анализатор spin реализован не так, как в онлайн-спецификации. Вы используете последнюю версию Spin? Я бы связался с авторами.   -  person Patrick Trentin    schedule 27.09.2016
comment
Я не использую последнюю версию. Сейчас использую версию 6.4.3. Из версии он управляет оператором select в препроцессоре, а не в грамматике. И в журналах более поздних выпусков нет обновлений или новых функций spinlex.c.   -  person jungyh0218    schedule 29.09.2016

Ответы (1)


arrow_upward
2
arrow_downward

Патрик прав. Я бы сказал, что это ошибка. Если вы посмотрите на spinlex.c, вы увидите, что при сканировании name до : допускаются только буквенно-цифровые символы:

scan_to(':', isalnum, name)

В любом случае, select — это просто сокращение для последовательности присваиваний. Таким образом, обходной путь может состоять в том, чтобы написать задания самостоятельно, например.

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