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
Depends on:
Reported: 2013-06-21 16:19 CEST by Alessandro Palermo
Modified: 2013-06-21 16:19 CEST (History)
0 users

See Also:

Uppaal Model With Single Query (2.99 KB, application/x-rar-compressed)
2013-06-21 16:19 CEST, Alessandro Palermo

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];