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

Bug 563 - guards on doubles result in "has a general hybrid guard enabled without urgent channel"
Summary: guards on doubles result in "has a general hybrid guard enabled without urgen...
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.18
Hardware: PC All
: P5 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2013-11-13 12:34 CET by Marius Mikučionis
Modified: 2013-11-13 18:01 CET (History)
1 user (show)

See Also:
Architecture:


Attachments
model (953 bytes, text/xml)
2013-11-13 12:34 CET, Marius Mikučionis
Details

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