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

Bug 554 - Query Check
Summary: Query Check
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Windows NT
: P5 major
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2013-06-21 16:19 CEST by Alessandro Palermo
Modified: 2013-06-21 16:19 CEST (History)
0 users

See Also:
Architecture:

Attachments
Uppaal Model With Single Query (2.99 KB, application/x-rar-compressed)
2013-06-21 16:19 CEST, Alessandro Palermo 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Alessandro Palermo 2013-06-21 16:19:34 CEST 
Created attachment 261 [details]
Uppaal Model With Single Query

In the attachment model a query result Satisfied if clock order in global declaration is:

clock time[TASK];
clock x[TASK];

Same query result May Not Be Satisfied if the clock order is:

clock x[TASK];
clock time[TASK];