Imagine the situation when there is a cycle in the specification and that there are two events in race. First event is in the first occurrence of node C and the second event is in the second occurrence of the node C. Currently the race checker highlights both events in one BMSC, even though the race happened in two different instances of this BMSC. This is confusing, because user can think that race is directly in the BMSC and not even look in HMSC, which is one part of design causing this race.
I think it might help to unfold the path in which we found race, make as many instances of BMSCs as reference nodes in the path, and highlights the events in the corresponding BMSCs.
Log in to post a comment.