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   
Attachments: model

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

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


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

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.