For my modelling needs it would be a very nice UppAal feature if it was possible to ask questions such as: In model state A, what is the largest value of variable B In the current version, the answer is only obtainable through trial-n-error with a true/false answer.
This would most certainly be a nice feature. It fact, it would be nice to do all sorts of queries against the state space of the system. The tricky part is to design a query language for such a purpose. I fixed the summary to better reflect the contents of the bug.
Moving bug to 3.5.7, as this is an enhancement bug and only bug fixes are allowed on 3.4.
John, I understand that your air-prototype addresses this bug. Reassigning bug to John.
An idea we have been looking into is to extend the query syntax, allowing for example: A[] not deadlock using { int sum=0; // Declaration of 'query variables' int count = 0; sum += my_var; // 'Query statements' for updating 'query variables' count++; } compute sum/count; // List of 'query result expressions' This query would either report a deadlock trace, or the average value of 'my_var'. Average values might not be the most interesting as they will be average over the explored *symbolic* states, but still...
SYNTAX: <query> (INIT <decls> TRANS <stmts> RESULTSET <expr-list> ';')? example: E<> false \ init \ int z = 0; \ trans \ z++; \ resultset z; Reports 'z', which is (currently) how many states pass through the 'query filter'
Hm.. making a query stateful is an interesting approach to this problem, but I am thinking to add the syntactic model coverage estimation into verification and have statistics displayed of what syntactic items (locations, edges, variable values) get visited during exploration. I know three ways of how to do this: 1) patch transition filter with model-decorating code ("decorations" could be stored separately, not necessarily embedded into model structure), 2) patch transition filter and have individual symbolic state objects carry the coverage information (similar to CoVer approach, I believe) 3) estimate syntactic model coverage of a specific trace in GUI (I already have a prototype, but not so useful in determining the full ranges) So ultimately I will want 2 in TRON, but before making the symbolic states bloated (which is OK in online testing but very bad for verification) I will have to determine the maximum number of coverable items, so the option 1 would be natural to start with... any comments?