Bug 563

Summary: guards on doubles result in "has a general hybrid guard enabled without urgent channel"
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: normal CC: gvilallo
Priority: P5    
Version: 4.1.18   
Hardware: PC   
OS: All   
Architecture:
Attachments: model

Description Marius Mikučionis 2013-11-13 12:34:15 CET
Created attachment 265 [details]
model

consider the following model:

double a, b, c;

process with location L with exprate 3.
edge loop from L to L with the guard "a+b+c<=1".

Query:

simulate 1 [<=10] {a,b,c}

Verification yields error:
Location Process.L
[ #time=0 ]
a=0 b=0 c=0 
has a general hybrid guard enabled without urgent channel.


I would expect this error on clock variables (since the minimum delay analysis is too complicated), but not on integers (which works) and not on doubles (which gives this error).

Credits:
Original report from Gabriel Domingo Vilallonga.
Comment 1 Gabriel Vilallonga 2013-11-13 18:01:54 CET
The initial values are cE1=0.5, cE2=0.5, cE3=0.0

The original message is:
Location rp1._id20
[ cE1=0.5 cE2=0.5 cE3=0 E1=0.5 E2=0.5 PE2=0 ATPhE1=0 ATPlE2=0 ATPlPE1=0 ATPlPE2=0 PTXE=0 PTXATPhE=0 PTXPE=0 PTXEast=0 PTXATPlEast=0 PTXATPlPE=0 PTX0=0.10000000000000000555111512312578 ADPi=0.25 Pi=0.25 ATPi=0.5 #time=0 ]
N_E1=1 N_E2=1 N_E3=1
has a general hybrid guard enabled without urgent channel.

I hope this can help.

Regards

Gabriel.