Bug 614

Summary: Guarded, not enabled edge with urgent channel enforces urgency
Product: UPPAAL Reporter: Peter Gjøl Jensen <pgj>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: enhancement CC: adavid
Priority: P5    
Version: 4.1.20   
Hardware: PC   
OS: Linux   
Attachments: Model provocating the error

Description Peter Gjøl Jensen 2016-09-27 01:04:49 CEST
Created attachment 293 [details]
Model provocating the error

Even though a warning is produced, the engine accepts the attached model, and produces erroneous results.

It seems that urgency is enforced on all edges, even though it is only present on one - which is not enabled due to a guard.

(Has been fixed in development branch stratego_2016_ndiscrete)
Comment 1 Marius Mikučionis 2017-02-20 10:26:08 CET
Uppaal 4.1.19 implements urgency on all edges.
Stratego 4.1.20-4 does not.