Bug 574

Summary: Description of meta variables
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: DocumentationAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: minor CC: johnh
Priority: P3    
Version: 4.1.19   
Hardware: All   
OS: All   
Architecture:
Attachments: wrong use of meta by example

Description Marius Mikučionis 2014-09-11 12:36:12 CEST
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).
Comment 1 Marius Mikučionis 2014-09-11 14:11:48 CEST
Created attachment 269 [details]
wrong use of meta by example

A counter-example model showing that the documented use of meta is wrong.
The following property is (mostly) false with meta and obviously true without meta:

E<> forall (i : int[0,2]) edgeVisited[i]

I write "mostly" because 4.0.14 always gives false and 4.1.19 gives false for the first time and true other times (possibly due to state space reuse).
Comment 2 Marius Mikučionis 2014-09-11 16:54:38 CEST
State-space-reuse has nothing to do with meta since 4.1.19:
meta  has been separated from the state space and explicitly preserved across verifications, so that's the reason why second invocation on the attached example returns with true.