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

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

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

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.