Bug 574

The use of meta variables is not well documented (and not warned about) which misleads users into abusing them and getting inconsistent verification results.

The "meta" variables are not used in state comparison when checking whether the newly reached state is in the passed-list or not.
If it's a new state (not in passed-list) then it is explored and added to the passed-list, else it is just pruned. Since the "meta" variables are not used in comparison, then their value stored in a passed-list depends on the order of exploration: the first reached state gets stored and the other equivalent ones (without meta variables) are pruned, therefore different exploration order lead to different states being explored. Hence different orders yield different results.
Also various versions of Uppaal may also give different results due to minor changes on how the model is parsed, the enumeration order of processes, edges, channels, etc..


While current help file says:

Meta variables
Integers, booleans, and arrays and records over integers and booleans can be marked as meta variables by prefixing the type with the keyword meta.
Meta variables are stored in the state vector, but are sematically not considered part of the state. I.e. two states that only differ in meta variables are considered to be equal. Example:
const int NUM_EDGES = 42;
meta bool edgeVisited[NUM_EDGES];
The example uses meta variables to maintain information about the history of a path, without affecting the state-space exploration. With the declaration above and a system with 42 edges, all with an update assigning true to their corresponding entry in edgeVisited, the query below can be used to determine if there is a path where all edges are visited (and find such a path, if trace generation is enabled).
E<> forall (i : int[0,41]) edgeVisited[i]



This example uses meta variables to track coverage, i.e. some meta information without disturbing the model logic, thus mostly harmless, however it is also misleading as the stored values may not be reliable (i.e. less coverage can be reported).

The only valid use of "meta" variable is to use it for value passing during single synchronization: sending process sets the value and the receiving process reads the value (and the value is never checked again as it can be lost).