This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 120

Summary:	Determining the actual range of variables
Product:	UPPAAL	Reporter:	Troels Smit <information>
Component:	Engine	Assignee:	John Håkansson <johnh>
Status:	ASSIGNED ---
Severity:	enhancement	CC:	marius
Priority:	P2
Version:	3.5.7
Hardware:	PC
OS:	Linux
Architecture:

Description Troels Smit 2004-12-07 11:17:20 CET

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.

Comment 1 Gerd Behrmann 2005-01-04 12:47:49 CET

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.

Comment 2 Gerd Behrmann 2005-06-29 21:11:36 CEST

Moving bug to 3.5.7, as this is an enhancement bug and only bug fixes are allowed on 3.4.

Comment 3 Gerd Behrmann 2005-09-02 14:42:09 CEST

John, I understand that your air-prototype addresses this bug. Reassigning bug to John.

Comment 4 John Håkansson 2006-02-13 11:32:12 CET

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...

Comment 5 John Håkansson 2006-12-04 09:48:29 CET

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'

Comment 6 Marius Mikučionis 2006-12-05 13:28:07 CET

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?