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