model-checkingnusmv

NuSMV: Initialising range constant with parameter

I'm new to NuSMV. I'm trying to define a module, where each state has a duration variable than can range from 0 to the specified bound.

MODULE state(inc, bound)
 VAR 
   duration : 0..bound;
 
 ASSIGN 
  init(duration) := 0;
  next(duration) := inc ? (duration + 1) mod (bound+1) : duration ;

 DEFINE limit := duration = bound;

However, this yields the syntax error: A variable is expected in left-hand-side of assignment: init(duration) := 0. I'm able to fix this by declaring duration to duration : 0..1+bound.

In my main module, I wish to calculate the total_duration (or actually calculate all possible combinations of state's duration and make sure that no combination exceeds e.i. 3 as in the SPEC) of running my model and make sure that variable does not succeed a specific limit.

Here's my main module:

MODULE main
 VAR 
  s0 : state(TRUE, 0);
  s1 : state(s0.limit, 0);
  s2 : state(s1.limit, 3);
  state : {s0, s1, s2};

 DEFINE
  max_duration := s0.bound + s1.bound + s2.bound;

 VAR
  total_duration : 0..max_duration;

 ASSIGN
  init(state) := s0;

  next(state) := 
    case
      state = s0 : s1;
      state = s1 : s2;
      state = s2 : s2;
    esac;

  total_duration := s0.duration + s1.duration + s2.duration;

SPEC
  AG (state = s2 -> AF total_duration <= 3);

My problem is: When I run the model, NuSMV keeps adding to the total_duration variable and thus fails with the message "line 39: cannot assign value 5 to variable total_duration". This is due to the declaration of duration : 0..1+bound, because, in the particular example of s0.duration = 0, s1.duration = 0 and s2.duration = 3, it will try to add 1 + 1 + 4 to total_duration, as that is the state's bound + 1.

However, if I check the trace there's no point where total_duration exceed 3. I have checked the followed specs:

-- specification AG total_duration < 4  is true

-- specification  F total_duration = 4  is false
-- specification EF total_duration >= 4  is false

How can I fix this? Either by declaring duration in another way or changing anything else?

Solution

  • The software does something very simple. It takes the domain of each addend, and checks whether the result variable would be able to hold the result of every possible combination of value. In this case:

    so, in principle, the maximum total_duration could be 6 and its domain should thus be 0..6. Therefore:

    DEFINE
  max_duration := s0.bound + s1.bound + s2.bound + 3

    You may want to run NuSMV with the following option:

    -keep_single_value_vars
  Does not convert variables that have only one
  single possible value into constant DEFINEs

    In this way, you'll be able to run the model without having to add +1 to the domain of bound.