CUDD reports 594 non-zero references

[Abeeha Fatima]

Hey! I want to know how to handle this error in my module

mdp

const int Active = 0;

const int CreatingAttestation = 1;

const int BroadcastingAttestation = 2;

const int MAX_SLOT = 10;

const int MAX_COMMITTEES = 5;

// Define states

module Validator

  // Define variables

  state: [0..2];

  slot: [0..MAX_SLOT] init 0; // Current slot

  index: [0..MAX_COMMITTEES] init 0; // Committee index

 

 

  // Additional variables for attestation_data

  attestation_slot: [0..MAX_SLOT];

  attestation_index: [0..MAX_COMMITTEES];

 

  // Transitions

  // Transition to the first slot

  [] (slot = 0) & (state = Active) ->

    (slot' = 1) & (index' = index) & (state' = CreatingAttestation);

  // Non-deterministic choice for subsequent slots

[] (slot > 0) & (state = Active) ->

    1: (slot' = slot + 1) & (index' = index) & (state' = (slot < MAX_SLOT) ? CreatingAttestation : Active);

  endmodule

Error: Probabilities in command 2 of module "Validator" sum to less than one (e.g. 0.0) for some states. Perhaps some of the updates give out-of-range values. One possible solution is to strengthen the guard (line 32, column 1).

Warning: CUDD reports 594 non-zero references.