Вопрос:

синтаксические ошибки при проверке модели с помощью nuXmv

model-checking

9 просмотра

1 ответ

6 Репутация автора

Теперь есть два варианта для клиента, телефонный звонок и смс в клинику, чтобы записаться на прием к врачу. Телефонный звонок или смс необходимо доставить посетителю или приемнику телефона, а затем сделать следующее .... Ну, как мы знаем, телефонный звонок и смс могут успешно доставить или не доставить, решение сбой доставки будет продолжать пытаться снова тот же способ выбора пользователя или другой.

Исходя из вышеизложенного, я пишу несколько кодов для проверки поведения модели для ее реализации. Я довольно новичок в классе, любой может помочь найти что-то не так с моими кодами.

MODULE call
VAR
option:{call,sms};
call:{successful,fail,again};
sms:{successful,fail,again};
phone_attender:{available,unavailable};

ASSIGN
init(option):=call|sms;
next(call):=case
call=successful:successful;
call=successful&phone_attender=available:{successful,available};
call=fail&phone_attender=fail:{fail,unavailable};
call=fail&phone_attender=fail:{again,unavailable};
call=again&phone_attender=successful:{again,available};
1:{successful,fail,again};
esac;

next(sms):=case
sms=successful&phone_attender:successful{successful};
sms=fail&phone_attender=fail:{fail,unavailable};
sms=fail&phone_attender=fail:{again,unavailable};
sms=again&phone_attender=successful:{again,available};
1:{successful,fail,again};

next(phone_attender):=case
phone_attender=available(call=successful|call=again)&(sms=successful|sms=again);
phone_attender=unavailable(call=fail|call=again)&(sms=fail|sms=again);
1:phone_attender;
esac;

Это всегда оставляет меня синтаксическими ошибками и запускается в терминале с nuXmv.

Автор: Michael H Источник Размещён: 12.06.2019 06:47

Ответы (1)


0 плюса

4965 Репутация автора

Строка 20:

file test.smv: line 20: at token "{": syntax error

Проблема задается следующим условием:

sms=successful&phone_attender:successful{successful};

Значение successful{successful}не имеет никакого смысла, выберите между successfulили {succesful}. Оба интерпретируются одинаково.

Строка 26:

file test.smv: line 26: at token ":=": syntax error

Вы не закрыли caseконструкцию предыдущего назначения. Добавьте esac;после последнего условия.

Строки 28/29:

file test.smv: line 28: at token ";": syntax error
file test.smv: line 29: at token ";": syntax error

Вы не указали следующее значение для phone_attenderпервых двух случаев.


Примечание: я не проверял семантику вашей модели, так как она даже синтаксически не верна.

Автор: Patrick Trentin Размещён: 12.06.2019 10:21
32x32