Rationale

Numerical state variables that constitute the state descriptor often obey certain constraints that are called variable invariants in this context. The particular invariants that Traviando investigates are the existence of a weighted sum such that for all observed states the result of the weighted sum is constant.
For a particular modeling formalism like an ordinary Petri net (a Place-Transition net), this concept is known as a place invariant or P-invariant).
Why are variable invariants expected to exist?
Many simulation models encode at least in parts finite automata and variables keep track in which state an automaton currently resides. State changes are often encoded with simple increment/decrement operations to variables such that the total value over those variables is always constant, e.g., for a dependability model with a component that can be operational or failed and two state variables UP and DOWN of type short, we often see that the sum of values for UP and DOWN is constant and of value 1. Another example are models of closed queueing networks where the number of customers of a particular class is constant.
For what kind of models and variables can Traviando detect variable invariants?
Traviando computes a generating set of variable invariants based on the algorithms known for computing invariants for Petri nets (Place-Transition nets), which is Farkas' algorithm, a variant of the Fourier-Motzkin method. These methods can be applied for all state variables or a subset of state variables that are of type integer and where all actions that make changes to those variables do so in a linear manner of the form v'=v+c where c is a constant integer value that depends on the particular action.
Any variable that is contained in some invariant, i.e., that is covered by an invariant, will have only a finite set of values that it can obtain. If a variable is not covered, as it is the case for the variable V that caused this warning, it can not be guaranteed with the help of an invariant that the variable has a finite domain.
Note: the fact that Traviando failed to compute an invariant that covers V does not necessarily mean that anything is wrong with the definition of V!
Also note that the length of the trace does not play a major role for this type of analysis. If at least each of the action occurs at least once to observe the corresponding state transformations and given that observing it once is sufficient to recognize the state transformation function, then the derivation of the underlying discrete event system model is complete and analyzing a longer trace would not get more information.

Symptoms

Traviando failed to compute an invariant that has a non-zero weight for variable V.

Diagnosis

• The model contains at least on action A that perform a state transformation to V that is not of the appropriate kind, namely the new value v' in the successor state is not v'=v + c where c is a constant that is specific to A. This implies that V is excluded from the invariant analysis upfront.
• Variable V is not a state variable with a finite domain, e.g., V may describe the in principle unbounded number of customers at a queue in an open queueing network. If this is the case, we cannot expect to see an variable invariant that contains V.
The model is of the kind where an invariant analysis exceeds available hardware resources such that Traviando terminates the calculation and obtains only a subset of a generating set of invariants.

Verification and Therapy

• Is the trace long enough, such that Traviando derives the state transformation function of each action correctly? Check if all action have occurred at least once, there should be no warning of dead actions (type 5). Also, if warnings of type 8 indicate that the state transformation function v'=v+c is obtained from a single observation, convince yourself if that is appropriately. The considered trace may not contain sufficient data to substantiate the analysis and you may want to generate a longer one.
• If you expect an invariant to exist, then this is likely to cover several variables that will all not be covered at this point. Check for all those variables, if there is any action that performs a state transformation function that is not of the appropriate type v'=v+c and thus excludes one variable from consideration which in turn removes the assumed invariant from the overall set. For any of those variables, check all actions that make changes to it to see if adjustments of state transformation functions are necessary. The report generated by Traviando contains detailed information for each variable on which actions perform which state transformation to it. However, keep in mind that existence of an invariant is not(!) a must for the correctness of a model.
• Use Traviando's LTL modelchecking feature to identify locations in the trace where the invariant you expect does not hold. Describe the invariant as a safety property that should hold in general throughout the trace. If the invariant you expect does not hold throughout the trace, check the particular location where it is violated in Traviando's visualization based on Message Sequence Charts and track the reasons for it. On the other hand, if the invariant holds throughout the trace, all the better.