CODEWITHSUNDEEP
model-checkingnusmvmodal-logic
Gold
Gold

Reputation: 189

NuSMV returns undefined operation

I have written the following code:

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;

However, when I execute the command "flatten_hierarchy" I get the following error: "x-1" undefined

I don't know why x-1 is undefined.

Upvotes: 1

Views: 221

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

This is a known issue.

The parser is confusing x-1 for an identifier, when it is supposed to be an expression.

Replace

x-1

with

x - 1

Upvotes: 3

Related Questions