[SOLVED] nuXmv syntax error when using variable instead of integer

nuXmv syntax error when using variable instead of integer

I have a model in muXmv, where I initialize with a range of values like -

VAR 
  x : 0..100;
ASSIGN
  init(x) := 10..50;

this works perfectly fine.

However, when I use variable instead of values,

ASSIGN 
  init(x) := LB..UB;

DEFINE
  LB := 10;
  UB := 50;

it throw syntax error -

line 14: at token "..": syntax error

line 14: Parser error

Not sure where I am going wrong?

Also is there a better way to declare constants in nuxmv?

Solution

A definition is not necessarily a constant, it is just a name for an expression (whose value may change after each transition). e.g.

MODILE main()
VAR
    x : 0..100;
    y : 0..100;
DEFINE
    sum := x + y;

...

I don't know the reason why the Grammar of NuSMV/nuXmv specifically disallows writing an interval using a pair of identifiers instead of a pair of constants.

One alternative is:

MODULE main()
VAR
    x : 0..100;

ASSIGN
  init(x) := INTERVAL;

DEFINE
  INTERVAL := 10 .. 50;

Another alternative is to use the constraint-style approach:

MODULE main()
VAR
    x : 0..100;

DEFINE
    LB := 10;
    UB := 50;

INIT
    LB <= x & x <= UB;

If you really find yourself struggling with many constant values, one option is to write a generic TEMPLATE model and then use regular expressions + scripting tools to generate automatically the various concrete models you need.