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

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

1 голос
/ 12 июня 2019

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

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

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.

1 Ответ

0 голосов
/ 13 июня 2019

Строка 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 для первых двух случаев.

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

...