Bug 502 - Trace may not respect strict guards.
Summary: Trace may not respect strict guards.
Status: RESOLVED FIXED
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: 2010-10-13 16:24 CEST by Alexandre David
Modified: 2010-10-13 16:54 CEST (History)
1 user (show)

See Also:
Architecture:


Attachments
Model file. (4.49 KB, text/xml)
2010-10-13 16:25 CEST, Alexandre David
Details
Query file. (297 bytes, application/octet-stream)
2010-10-13 16:25 CEST, Alexandre David
Details

Note You need to log in before you can comment on or make changes to this bug.
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.