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