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

Bug 468 - Wrong transition selection in systems with process priorities
Summary: Wrong transition selection in systems with process priorities
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.7
Hardware: PC Windows XP
: P2 major
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2009-04-03 08:40 CEST by Yasufumi Suzuki
Modified: 2009-08-12 19:05 CEST (History)
0 users

See Also:
Architecture:


Attachments
Example model (2.71 KB, text/xml)
2009-04-03 08:42 CEST, Yasufumi Suzuki
Details
Example trace (491 bytes, text/plain)
2009-04-03 08:42 CEST, Yasufumi Suzuki
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Yasufumi Suzuki 2009-04-03 08:40:46 CEST
A binary synchronization transition of a low priority process  is 
enabled even if a binary synchronization transition of a higher priority 
process using the same channel is possible.

Problem description:
This problem occurs only when also a delaying transition in a third 
process is enabled.
It is visible in the last transition in the attached  example trace.

Example model: see attachment 1 [details]
Example trace: see attachment 2 [details]
Comment 1 Yasufumi Suzuki 2009-04-03 08:42:04 CEST
Created attachment 214 [details]
Example model
Comment 2 Yasufumi Suzuki 2009-04-03 08:42:45 CEST
Created attachment 215 [details]
Example trace
Comment 3 Alexandre David 2009-08-12 19:05:53 CEST
Fixed in rev. 4378 (4.0.9) and 4379 (trunk).
We have changed the semantics because it was inconsistent.
Before, priority was resolved by comparing the priorities of
the processes involved in two transitions by descending order.
Now, it is resolved by considering the highest priority process,
which is in line with priority ceiling protocols.

In this example, it is normal to have the synchronization with
the new semantics (though not normal with the old one).