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

Bug 530 - Hypothesis testing fails
Summary: Hypothesis testing fails
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Linux
: P2 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2012-01-09 15:42 CET by Danny Bøgsted Poulsen
Modified: 2012-01-09 15:44 CET (History)
0 users

See Also:
Architecture:


Attachments
Model for reproducing the behaviour (1.05 KB, text/xml)
2012-01-09 15:44 CET, Danny Bøgsted Poulsen
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Danny Bøgsted Poulsen 2012-01-09 15:42:01 CET
Hypothesis test queries reports "roperty not satisfied" even though the property is satisfied. 

To reproduce: 
1. Create automaton (Process) with two locations and one clock x
2. Set invariant of initial location to x<=10
3. add edge from initial location to second location (A)

Run query "Pr[<=100] (<> Process.A) >= 0.7 "

Uppaal should report "property satisfied", but returns "property not satisfied"
Comment 1 Danny Bøgsted Poulsen 2012-01-09 15:44:42 CET
Created attachment 251 [details]
Model for reproducing the behaviour