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

Bug 530

Summary: Hypothesis testing fails
Product: UPPAAL Reporter: Danny Bøgsted Poulsen <dannybp>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: normal    
Priority: P2    
Version: unspecified   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: Model for reproducing the behaviour

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