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