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

Bug 502

Summary: Trace may not respect strict guards.
Product: UPPAAL Reporter: Alexandre David <adavid>
Component: EngineAssignee: Alexandre David <adavid>
Status: RESOLVED FIXED    
Severity: normal CC: kyrke
Priority: P2    
Version: unspecified   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: Model file.
Query file.

Description Alexandre David 2010-10-13 16:24:41 CEST
This affects only 4.1.x, reported by Kenneth.
There are a problem in the following part of the trace:

Delay: 0.5

State:
( Control.finish Lock.P_lock P(1).P1 P(2).P1 P(3).P_capacity
P(4).P_capacity P(5).P_capacity P(6).P_capacity P(7).P_capacity )
P(1).x=0.5 P(2).x=0.5 P(3).x=0.5 P(4).x=0.5 P(5).x=0.5 P(6).x=0.5
P(7).x=0.5 lock=0

Transitions:
  P(1).P1->P(1).P2 { lock == 0 && x > 0, T1!, x := 0 }

State:
( Control.finish Lock.P_lock P(1).P2 P(2).P1 P(3).P_capacity
P(4).P_capacity P(5).P_capacity P(6).P_capacity P(7).P_capacity )
P(1).x=0 P(2).x=0.5 P(3).x=0.5 P(4).x=0.5 P(5).x=0.5 P(6).x=0.5
P(7).x=0.5 lock=0

Transitions:
  P(2).P1->P(2).P2 { lock == 0 && x > 0, T1!, x := 0 }

State:
( Control.finish Lock.P_lock P(1).P2 P(2).P2 P(3).P_capacity
P(4).P_capacity P(5).P_capacity P(6).P_capacity P(7).P_capacity )
P(1).x=0 P(2).x=0 P(3).x=0.5 P(4).x=0.5 P(5).x=0.5 P(6).x=0.5 P(7).x=0.5 lock=0

Transitions:
  P(3).P_capacity->P(3).P1 { lock == 0, T2!, x := 0 }
  P(1).P2->P(1).P0 { x > 0, T2?, x := 0 }

Now the trace claims that the above transitions can be fired, but it
has a guard saying " x > 0 " and if you look
at the age of P(1).x=0 it is zero, so its should not be possible to
fire the transition.
Comment 1 Alexandre David 2010-10-13 16:25:30 CEST
Created attachment 234 [details]
Model file.
Comment 2 Alexandre David 2010-10-13 16:25:44 CEST
Created attachment 235 [details]
Query file.
Comment 3 Alexandre David 2010-10-13 16:54:01 CEST
Fixed in rev. 4596.