NuSMV возвращает неопределенную операцию

Question

Я написал следующий код:

MODULE main

VAR
    status:{empty, no_empty};
    x : 0..3;

ASSIGN
    init(status):= empty;
    init(x):=0;
    next(status):= case
        (status = empty): no_empty;
        (status = no_empty) & (x=0): empty;
        TRUE: status;
        esac;
    next(x):= case
        (status = empty): x+3;
        (status = no_empty) & (x>0): x-1;
        TRUE: x;
        esac;

Однако, когда я выполняю команду «flatten_hierarchy», я получаю следующую ошибку: «x-1» undefined

Я не знаю, почему x-1 не определено.

Answer 1

Это известная проблема.

Анализатор сбивает с толку x-1 идентификатор, когда он должен быть выражением.

Заменить

x-1

с

x - 1