Bug 120 - Determining the actual range of variables
Summary: Determining the actual range of variables
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.5.7
Hardware: PC Linux
: P2 enhancement
Assignee: John Håkansson
URL:
Depends on:
Blocks:
 
Reported: 2004-12-07 11:17 CET by Troels Smit
Modified: 2006-12-05 13:28 CET (History)
1 user (show)

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
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?